Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Alex Ozdemir, Daniel Larraz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * parsing structured field terms
14 : : *
15 : : * NB: many functions in this file return an empty std::optional if parsing
16 : : * fails.
17 : : */
18 : :
19 : : #include "theory/ff/parse.h"
20 : :
21 : : // external includes
22 : :
23 : : // std includes
24 : : #include <numeric>
25 : : #include <optional>
26 : : #include <unordered_map>
27 : : #include <unordered_set>
28 : :
29 : : // internal includes
30 : : #include "theory/ff/util.h"
31 : : #include "theory/theory.h"
32 : :
33 : : namespace cvc5::internal {
34 : : namespace theory {
35 : : namespace ff {
36 : : namespace parse {
37 : :
38 : : // fwd declarations for Spectrum
39 : : namespace {
40 : :
41 : : /**
42 : : * Characterization of a univariate, degree <= 2 polynomial.
43 : : * The members uniquely determine such a polynomial, up to its leading
44 : : * coefficient.
45 : : *
46 : : * This is a helper class for parsing terms that constrain a variable to be: 0,
47 : : * 1, or both.
48 : : */
49 : : struct Spectrum
50 : : {
51 : : /** the variable; ignore if degree is 0 */
52 : : Node var;
53 : : /** the degree in {0, 1, 2} */
54 : : uint8_t degree;
55 : : /** value at 0 */
56 : : FiniteFieldValue val0;
57 : : /** value at 1 */
58 : : FiniteFieldValue val1;
59 : : };
60 : :
61 : : using SpectrumOpt = std::optional<Spectrum>;
62 : :
63 : : /**
64 : : * Attempt to compute a Spectrum for the polynomial defined by t.
65 : : *
66 : : * @param t a field term
67 : : * @param depth how deep to search in term before giving up; reducing the depth
68 : : * reduces the runtime of this function, but increases the number
69 : : * of terms for which this function returns an empty optional.
70 : : * depth 5 is enough to parse all the patterns I've seen for
71 : : * bit constraints and similar.
72 : : * @return none if t is too deep or mulitvariate or has degreee > 2; otherwise,
73 : : * a Spectrum.
74 : : */
75 : : SpectrumOpt spectrum(const Node& t, uint8_t depth = 5);
76 : :
77 : : } // namespace
78 : :
79 : 0 : bool zeroConstraint(const Node& fact)
80 : : {
81 : 0 : SpectrumOpt r = spectrum(fact);
82 : 0 : return r.has_value() && r->degree == 1 && r->val0.getValue() == 0;
83 : : }
84 : :
85 : 12 : bool oneConstraint(const Node& fact)
86 : : {
87 : 12 : SpectrumOpt r = spectrum(fact);
88 : 24 : return r.has_value() && r->degree == 1 && r->val1.getValue() == 0;
89 : : }
90 : :
91 : 11610 : std::optional<Node> bitConstraint(const Node& fact)
92 : : {
93 : 23220 : SpectrumOpt r = spectrum(fact);
94 [ + + ][ + + ]: 16196 : if (r.has_value() && r->degree == 2 && r->val0.getValue() == 0
[ + + ][ - - ]
95 [ + + ][ + + ]: 16196 : && r->val1.getValue() == 0)
[ + + ][ + + ]
[ - - ]
96 : : {
97 : 705 : return {r->var};
98 : : }
99 : 10905 : return {};
100 : : }
101 : :
102 : : namespace {
103 : :
104 : : /**
105 : : * Given spectra for f and g, compute an (optional) spectrum for f @ g, where @
106 : : * is point-wise operation
107 : : *
108 : : * @param a spectrum for f
109 : : * @param b spectrum for g
110 : : * @param dOp binary operator on uint8_t for computing the degree of f @ g
111 : : * @param fOp the binary point-wise operator @
112 : : *
113 : : * */
114 : : template <typename DegreeOp, typename FieldOp>
115 : 13485 : SpectrumOpt spectrumOp(SpectrumOpt&& a,
116 : : SpectrumOpt&& b,
117 : : DegreeOp dOp,
118 : : FieldOp fOp)
119 : : {
120 [ + + ][ + + ]: 13485 : if (!(a.has_value() && b.has_value()))
[ + + ]
121 : : {
122 : : // failed child
123 : 3502 : return {};
124 : : }
125 [ + + ][ + + ]: 9983 : if (a->degree && b->degree && a->var != b->var)
[ + + ][ + + ]
126 : : {
127 : : // multivariate
128 : 1855 : return {};
129 : : }
130 : 8128 : uint8_t degree = dOp(a->degree, b->degree);
131 [ + + ]: 8128 : if (degree > 2)
132 : : {
133 : : // high-degree
134 : 13 : return {};
135 : : }
136 : 16230 : FiniteFieldValue val0 = fOp(a->val0, b->val0);
137 : 8115 : FiniteFieldValue val1 = fOp(a->val1, b->val1);
138 [ + + ]: 8115 : Node&& var = a->degree ? std::move(a->var) : std::move(b->var);
139 : 8115 : return {{var, degree, val0, val1}};
140 : : };
141 : :
142 : 36322 : SpectrumOpt spectrum(const Node& t, uint8_t depth)
143 : : {
144 [ + + ]: 36322 : if (t.getKind() == Kind::NOT)
145 : : {
146 : 5563 : return {};
147 : : }
148 : 30759 : Assert(t.getType().isFiniteField() || t.getKind() == Kind::EQUAL) << t;
149 [ + + ]: 30759 : if (isFfLeaf(t))
150 : : {
151 [ + + ]: 19083 : if (t.isConst())
152 : : {
153 : : // this is a constant
154 : 7453 : FiniteFieldValue v = t.getConst<FiniteFieldValue>();
155 : 7453 : return {{Node::null(), 0, v, v}};
156 : : }
157 : :
158 : : // this is an (ff) variable
159 : 11630 : const Integer modulus = t.getType().getFfSize();
160 : 11630 : return {{t, 1, {1, modulus}, {0, modulus}}};
161 : : }
162 [ + + ][ + + ]: 11676 : switch (t.getKind())
[ - ]
163 : : {
164 : 2392 : case Kind::FINITE_FIELD_ADD:
165 : : {
166 : 4784 : SpectrumOpt acc = spectrum(t[0], depth - 1);
167 [ + + ]: 6312 : for (size_t i = 1, n = t.getNumChildren(); i < n; ++i)
168 : : {
169 : 7840 : acc = spectrumOp(
170 : 3920 : std::move(acc),
171 : 7840 : spectrum(t[i], depth - 1),
172 : 1225 : [](const uint8_t& x, const uint8_t& y) { return std::max(x, y); },
173 : 2450 : [](const FiniteFieldValue& x, const FiniteFieldValue& y) {
174 : 2450 : return x + y;
175 : 3920 : });
176 : : }
177 : 2392 : return acc;
178 : : }
179 : 6059 : case Kind::EQUAL:
180 : : {
181 : : return spectrumOp(
182 : 12118 : spectrum(t[0], depth - 1),
183 : 12118 : spectrum(t[1], depth - 1),
184 : 4586 : [](const uint8_t& x, const uint8_t& y) { return std::max(x, y); },
185 : 9172 : [](const FiniteFieldValue& x, const FiniteFieldValue& y) {
186 : 9172 : return x - y;
187 : 6059 : });
188 : : }
189 : 2764 : case Kind::FINITE_FIELD_MULT:
190 : : {
191 : 5528 : SpectrumOpt acc = spectrum(t[0], depth - 1);
192 [ + + ]: 6270 : for (size_t i = 1, n = t.getNumChildren(); i < n; ++i)
193 : : {
194 : 7012 : acc = spectrumOp(
195 : 3506 : std::move(acc),
196 : 7012 : spectrum(t[i], depth - 1),
197 : 2317 : [](const uint8_t& x, const uint8_t& y) { return x + y; },
198 : 4608 : [](const FiniteFieldValue& x, const FiniteFieldValue& y) {
199 : 4608 : return x * y;
200 : 3506 : });
201 : : }
202 : 2764 : return acc;
203 : : }
204 : 461 : case Kind::FINITE_FIELD_BITSUM:
205 : : {
206 : : // give up
207 : 461 : return {};
208 : : }
209 : 0 : default: Unreachable() << t.getKind();
210 : : }
211 : : return {};
212 : : }
213 : :
214 : : } // namespace
215 : :
216 : 443 : std::optional<std::pair<Node, FiniteFieldValue>> linearMonomial(const Node& t)
217 : : {
218 : 886 : TypeNode ty = t.getType();
219 [ - + ]: 443 : if (!ty.isFiniteField())
220 : : {
221 : 0 : return {};
222 : : }
223 : 443 : const Integer& p = ty.getFfSize();
224 : :
225 : : // X
226 [ + + ]: 443 : if (t.isVar())
227 : : {
228 : 100 : return {{t, FiniteFieldValue(1, p)}};
229 : : }
230 : :
231 : : // (ff.neg X)
232 [ + + ][ + - ]: 343 : if (t.getKind() == Kind::FINITE_FIELD_NEG && t[0].isVar())
[ + + ][ + + ]
[ - - ]
233 : : {
234 : 2 : return {{t[0], FiniteFieldValue(-1, p)}};
235 : : }
236 : :
237 : : // (ff.mul ? ?)
238 [ + + ][ + + ]: 341 : if (t.getKind() == Kind::FINITE_FIELD_MULT && t.getNumChildren() == 2)
[ + + ]
239 : : {
240 : : // (ff.mul k X)
241 : 143 : if (t[0].isConst() && t[1].isVar())
242 : : {
243 : 77 : return {{t[1], t[0].getConst<FiniteFieldValue>()}};
244 : : }
245 : :
246 : : // (ff.mul X k)
247 : 66 : if (t[1].isConst() && t[0].isVar())
248 : : {
249 : 1 : return {{t[0], t[1].getConst<FiniteFieldValue>()}};
250 : : }
251 : : }
252 : :
253 : 263 : return {};
254 : : }
255 : :
256 : : std::optional<std::pair<std::vector<std::pair<Node, FiniteFieldValue>>,
257 : : std::vector<Node>>>
258 : 151 : extractLinearMonomials(const Node& t)
259 : : {
260 : 302 : TypeNode ty = t.getType();
261 [ - + ]: 151 : if (!ty.isFiniteField())
262 : : {
263 : 0 : return {};
264 : : }
265 [ - + ]: 151 : if (t.getKind() != Kind::FINITE_FIELD_ADD)
266 : : {
267 : 0 : return {};
268 : : }
269 : 302 : std::vector<std::pair<Node, FiniteFieldValue>> monomials{};
270 : 151 : std::vector<Node> otherSummands{};
271 : :
272 [ + + ]: 589 : for (const Node& summand : t)
273 : : {
274 : 876 : auto monomial = linearMonomial(summand);
275 [ + + ]: 438 : if (monomial.has_value())
276 : : {
277 : 176 : monomials.push_back(std::move(monomial.value()));
278 : : }
279 : : else
280 : : {
281 : 262 : otherSummands.push_back(summand);
282 : : }
283 : : }
284 : :
285 : 151 : return {{std::move(monomials), std::move(otherSummands)}};
286 : : }
287 : :
288 : : std::optional<
289 : : std::pair<std::vector<std::pair<FiniteFieldValue, std::vector<Node>>>,
290 : : std::vector<Node>>>
291 : 148 : bitSums(const Node& t, std::unordered_set<Node> bits)
292 : : {
293 : : // 1. get linear monomials
294 : 296 : auto res = extractLinearMonomials(t);
295 [ - + ]: 148 : if (!res.has_value())
296 : : {
297 : 0 : return {};
298 : : }
299 : 148 : auto& [monomials, rest] = res.value();
300 [ + + ]: 148 : if (monomials.empty())
301 : : {
302 : 79 : return {};
303 : : }
304 : :
305 [ + - ]: 69 : Trace("ff::parse::debug") << "bitSums start " << t << std::endl;
306 : :
307 : : // we'll need to build some monomials
308 : 69 : auto nm = t.getNodeManager();
309 : 258 : auto mkMonomial = [&nm](TNode n, const FiniteFieldValue& coeff) {
310 : 129 : return nm->mkNode(Kind::FINITE_FIELD_MULT, nm->mkConst(coeff), n);
311 : 69 : };
312 : :
313 : : // 2. choose a subset of monomials w/ unique coefficients
314 : : // (preferring monomials with vars in bits)
315 : :
316 : : // that subset, as a (coeff -> var) map
317 : : // later, we'll iterate over monomials by coeff; this map will give the var
318 : : std::unordered_map<FiniteFieldValue, Node, FiniteFieldValueHashFunction>
319 : 138 : bitMonomials{};
320 : : // that subset, as a priority_queue over (-abs(signed_int(coeff)), coeff)
321 : : // later, we'll iterate over monomials in the coeff order given here
322 : 138 : std::priority_queue<std::pair<Integer, FiniteFieldValue>> q{};
323 : :
324 [ + + ]: 242 : for (const auto& [var, coeff] : monomials)
325 : : {
326 : : // iterate over monomials: (var, coeff) pairs
327 [ + - ]: 346 : Trace("ff::parse::debug")
328 : 173 : << "bitMonomial " << coeff << " " << var << std::endl;
329 : :
330 : 173 : auto it = bitMonomials.find(coeff);
331 [ + + ]: 173 : if (it == bitMonomials.end())
332 : : {
333 : : // new coefficient
334 [ + - ]: 103 : Trace("ff::parse::debug") << " fresh bit" << var << std::endl;
335 : 103 : bitMonomials.insert(it, {coeff, var});
336 : 103 : q.emplace(-coeff.toSignedInteger().abs(), coeff);
337 : : }
338 [ + + ][ + + ]: 70 : else if (bits.count(var) && !bits.count(it->second))
[ + + ]
339 : : {
340 : : // old coefficient, bit var, & the old var is not a bit; evict it.
341 [ + - ]: 6 : Trace("ff::parse::debug")
342 : 3 : << " " << var << " evicts " << it->second << std::endl;
343 : 3 : rest.push_back(mkMonomial(it->second, coeff));
344 : 3 : it->second = var;
345 : : }
346 : : else
347 : : {
348 : : // skip
349 [ + - ]: 134 : Trace("ff::parse::debug")
350 : 67 : << " skipped " << coeff << " " << var << std::endl;
351 [ + - ]: 134 : Trace("ff::parse::debug")
352 : 67 : << " isBit: " << std::boolalpha << !!bits.count(var) << std::endl;
353 : 67 : rest.push_back(mkMonomial(var, coeff));
354 : : }
355 : : }
356 : :
357 : : // 3. extact bitsums
358 : :
359 : 138 : std::vector<std::pair<FiniteFieldValue, std::vector<Node>>> bitSums{};
360 : 138 : FiniteFieldValue two(2, t.getType().getFfSize());
361 : : // choose a starting constant k; we'll search for a run: k*x, 2k*y, 4k*z, ...
362 : : // we choose k from the priority queue (i.e., k with least abs(k) goes first)
363 [ + + ]: 172 : while (!q.empty())
364 : : {
365 : 206 : FiniteFieldValue k = q.top().second;
366 : 103 : q.pop();
367 : :
368 : : // a list of variables x, y, z, ... in the discovered run
369 : 206 : std::vector<Node> bsBits{};
370 : :
371 : : // search for a run: k*x, 2k*y, 4k*z, ...
372 : 206 : FiniteFieldValue coeff = k;
373 [ + + ]: 206 : while (bitMonomials.count(coeff))
374 : : {
375 : 206 : auto var = bitMonomials.at(coeff);
376 : 103 : bsBits.push_back(var);
377 : 103 : bitMonomials.erase(coeff);
378 : 103 : coeff *= two;
379 : : }
380 : :
381 [ + + ]: 103 : if (bsBits.size() > 1)
382 : : {
383 : : // save as a bitsum if the length is greater than 1
384 : 16 : bitSums.emplace_back(k, std::move(bsBits));
385 : : }
386 [ + + ]: 87 : else if (bsBits.size() == 1)
387 : : {
388 : : // if one bit, add its summand to rest
389 : 59 : rest.push_back(mkMonomial(bsBits[0], coeff / two));
390 : : }
391 : : }
392 : :
393 [ - + ][ - + ]: 69 : Assert(bitMonomials.empty());
[ - - ]
394 [ - + ][ - + ]: 69 : Assert(q.empty());
[ - - ]
395 : :
396 : 69 : return {{std::move(bitSums), std::move(rest)}};
397 : : }
398 : :
399 : 459379 : std::optional<Node> disjunctiveBitConstraint(const Node& t)
400 : : {
401 [ + + ]: 146999 : if (t.getKind() == Kind::OR && t.getNumChildren() == 2
402 : 528192 : && t[0].getKind() == Kind::EQUAL && t[1].getKind() == Kind::EQUAL
403 : 606378 : && t[0][1].getType().isFiniteField() && t[1][0].getType().isFiniteField())
404 : : {
405 : : using theory::ff::parse::oneConstraint;
406 : : using theory::ff::parse::zeroConstraint;
407 : 6 : if ((oneConstraint(t[0]) && zeroConstraint(t[1]))
408 : 6 : || (oneConstraint(t[1]) && zeroConstraint(t[0])))
409 : : {
410 : 0 : return {theory::ff::parse::spectrum(t[0])->var};
411 : : }
412 : : }
413 : 459379 : return {};
414 : : }
415 : :
416 : : } // namespace parse
417 : : } // namespace ff
418 : : } // namespace theory
419 : : } // namespace cvc5::internal
|
