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