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 : : * a split groebner basis
11 : : */
12 : :
13 : : #ifdef CVC5_USE_COCOA
14 : :
15 : : #include "theory/ff/split_gb.h"
16 : :
17 : : // external includes
18 : : #include <CoCoA/BigIntOps.H>
19 : : #include <CoCoA/SparsePolyIter.H>
20 : : #include <CoCoA/SparsePolyOps-MinPoly.H>
21 : : #include <CoCoA/SparsePolyOps-RingElem.H>
22 : : #include <CoCoA/SparsePolyOps-ideal.H>
23 : : #include <CoCoA/SparsePolyRing.H>
24 : :
25 : : // std includes
26 : : #include <variant>
27 : :
28 : : // internal includes
29 : : #include "base/output.h"
30 : : #include "theory/ff/parse.h"
31 : : #include "util/resource_manager.h"
32 : :
33 : : namespace cvc5::internal {
34 : : namespace theory {
35 : : namespace ff {
36 : :
37 : : namespace {
38 : : /** Extend curR into a zero for this split Gb.
39 : : *
40 : : * @param origPolys Generators for an ideal.
41 : : * @param curBases A split basis for the same ideal.
42 : : * @param curR A partial zero for the ideal.
43 : : * @param bitProp Info about which vars are bitsums of which. See splitGb.
44 : : * @param env used for resource management
45 : : * @param stats FfStatistics to track
46 : : *
47 : : * @return A common (full) zero, a conflict polynomial, or false (indicating
48 : : * that no common zeros exist). The conflict polynomial is guaranteed to
49 : : * not be in the ideal generated by the first of the split bases.
50 : : */
51 : 983 : std::variant<Point, Poly, bool> splitZeroExtend(const Polys& origPolys,
52 : : const SplitGb&& curBases,
53 : : const PartialPoint&& curR,
54 : : const BitProp& bitProp,
55 : : const Env& env,
56 : : FfStatistics* stats)
57 : : {
58 [ - + ][ - + ]: 983 : Assert(origPolys.size());
[ - - ]
59 : 983 : CoCoA::ring polyRing = CoCoA::owner(origPolys[0]);
60 : 983 : SplitGb bases(curBases);
61 : 983 : PartialPoint r(curR);
62 : 983 : long nAssigned = std::count_if(
63 : 6044 : r.begin(), r.end(), [](const auto& v) { return v.has_value(); });
64 [ + + ]: 983 : if (std::any_of(bases.begin(), bases.end(), [](const Gb& i) {
65 : 1784 : return i.isWholeRing();
66 : : }))
67 : : {
68 [ + + ]: 2091 : for (const auto& p : origPolys)
69 : : {
70 : 1909 : auto value = cocoaEval(p, r);
71 [ + + ][ + + ]: 1909 : if (value.has_value() && !CoCoA::IsZero(*value) && !bases[0].contains(p))
[ - + ][ - + ]
72 : : {
73 : 0 : return p;
74 : : }
75 [ + - ]: 1909 : }
76 : 182 : return false;
77 : : }
78 : :
79 [ - + ]: 801 : if (env.getResourceManager()->outOfTime())
80 : : {
81 : 0 : throw FfTimeoutException("splitZeroExtend");
82 : : }
83 : :
84 [ + + ]: 801 : if (nAssigned == CoCoA::NumIndets(CoCoA::owner(origPolys[0])))
85 : : {
86 : 117 : Point out;
87 [ + + ]: 801 : for (const auto& v : r)
88 : : {
89 : 684 : out.push_back(*v);
90 : : }
91 : 117 : return out;
92 : 117 : }
93 : 684 : auto brancher = applyRule(bases[0], polyRing, r);
94 [ + - ]: 866 : for (auto next = brancher->next(); next.has_value(); next = brancher->next())
95 : : {
96 : 866 : long var = CoCoA::UnivariateIndetIndex(*next);
97 [ - + ][ - + ]: 866 : Assert(var >= 0);
[ - - ]
98 : 866 : Scalar val = -CoCoA::ConstantCoeff(*next);
99 [ - + ][ - + ]: 866 : Assert(!r[var].has_value());
[ - - ]
100 : 866 : PartialPoint newR = r;
101 : 866 : newR[var] = {val};
102 [ + - ]: 1732 : Trace("ff::split::mc::debug")
103 : 866 : << std::string(1 + nAssigned, ' ') << CoCoA::indet(polyRing, var)
104 : 866 : << " = " << val << std::endl;
105 : 866 : std::vector<Polys> newSplitGens{};
106 [ + + ]: 2598 : for (const auto& b : bases)
107 : : {
108 : 1732 : newSplitGens.push_back({});
109 : 3464 : std::copy(b.basis().begin(),
110 : 1732 : b.basis().end(),
111 : 1732 : std::back_inserter(newSplitGens.back()));
112 : 1732 : newSplitGens.back().push_back(*next);
113 : : }
114 : 866 : BitProp bitPropCopy = bitProp;
115 : 866 : SplitGb newBases = splitGb(newSplitGens, bitPropCopy, env, stats);
116 : : auto result = splitZeroExtend(origPolys,
117 : 866 : std::move(newBases),
118 : 866 : std::move(newR),
119 : : bitPropCopy,
120 : : env,
121 : 866 : stats);
122 [ + + ]: 866 : if (!std::holds_alternative<bool>(result))
123 : : {
124 : 684 : return result;
125 : : }
126 [ + + ][ + + ]: 4970 : }
[ + + ][ + + ]
[ + + ][ + + ]
[ - + ]
127 : 0 : return false;
128 : 983 : }
129 : : } // namespace
130 : :
131 : 838 : FfResult split(const std::vector<Node>& facts,
132 : : const FfSize& size,
133 : : const Env& env,
134 : : FfStatistics* stats)
135 : : {
136 : 838 : std::unordered_set<Node> bits{};
137 : 838 : CocoaEncoder enc(env.getNodeManager(), size);
138 [ + + ]: 12333 : for (const auto& fact : facts)
139 : : {
140 : 11495 : enc.addFact(fact);
141 : : }
142 : 838 : enc.endScan();
143 [ + + ]: 12333 : for (const auto& fact : facts)
144 : : {
145 : 11495 : enc.addFact(fact);
146 : : }
147 : :
148 : 838 : Polys nlGens = enc.polys();
149 : 838 : Polys lGens = enc.bitsumPolys();
150 [ + + ]: 12333 : for (const auto& p : enc.polys())
151 : : {
152 [ + + ]: 11495 : if (CoCoA::deg(p) <= 1)
153 : : {
154 : 4829 : lGens.push_back(p);
155 : : }
156 : : }
157 : :
158 : 838 : BitProp bitProp(facts, enc);
159 : :
160 : 3352 : std::vector<Polys> splitGens = {lGens, nlGens};
161 : 838 : SplitGb splitBasis = splitGb(splitGens, bitProp, env, stats);
162 [ + + ]: 838 : if (std::any_of(splitBasis.begin(), splitBasis.end(), [](const auto& b) {
163 : 865 : return b.isWholeRing();
164 : : }))
165 : : {
166 : : // return a trivial conflict
167 : 811 : return facts;
168 : : }
169 : :
170 : : std::optional<Point> root =
171 : 27 : splitFindZero(std::move(splitBasis), enc.polyRing(), bitProp, env, stats);
172 [ + - ]: 27 : if (root.has_value())
173 : : {
174 : 27 : FfModel model;
175 [ + + ]: 128 : for (const auto& [indetIdx, varNode] : enc.nodeIndets())
176 : : {
177 : 101 : FiniteFieldValue literal = enc.cocoaFfToFfVal(root.value()[indetIdx]);
178 [ + - ]: 202 : Trace("ff::model") << "Model: " << varNode << " = " << literal
179 : 101 : << std::endl;
180 : 101 : model.insert({varNode, literal});
181 : 128 : }
182 : 27 : return model;
183 : 27 : }
184 : :
185 : : // return a trivial conflict
186 : 0 : return facts;
187 : 838 : }
188 : :
189 : 1704 : SplitGb splitGb(const std::vector<Polys>& generatorSets,
190 : : BitProp& bitProp,
191 : : const Env& env,
192 : : FfStatistics* stats)
193 : : {
194 [ + + ]: 1704 : if (stats) ++stats->d_numGbRuns;
195 : 1704 : size_t k = generatorSets.size();
196 : 1704 : std::vector<Polys> newPolys(generatorSets);
197 : 3408 : SplitGb splitBasis(k);
198 : : do
199 : : {
200 : : // add newPolys to each basis
201 [ + + ]: 8199 : for (size_t i = 0; i < k; ++i)
202 : : {
203 [ + + ]: 5466 : if (newPolys[i].size())
204 : : {
205 : 4476 : Polys newGens{};
206 : :
207 : 4476 : const auto& basis = splitBasis[i].basis();
208 : 4476 : std::copy(basis.begin(), basis.end(), std::back_inserter(newGens));
209 : 8952 : std::copy(newPolys[i].begin(),
210 : 4476 : newPolys[i].end(),
211 : : std::back_inserter(newGens));
212 : : {
213 [ + + ]: 4476 : CodeTimer timer(stats ? &stats->d_timeGbRuns : nullptr);
214 : 4476 : splitBasis[i] = Gb(newGens, env.getResourceManager());
215 : 4476 : }
216 : 4476 : newPolys[i].clear();
217 : 4476 : }
218 : : }
219 : :
220 : : // compute polys that can be shared
221 : 2733 : Polys toPropagate = bitProp.getBitEqualities(splitBasis);
222 [ + + ]: 8199 : for (size_t i = 0; i < k; ++i)
223 : : {
224 : 5466 : const auto& basis = splitBasis[i].basis();
225 : 5466 : std::copy(basis.begin(), basis.end(), std::back_inserter(toPropagate));
226 : : }
227 : :
228 : : // share polys with ideals that accept them.
229 [ + + ]: 25994 : for (const auto& p : toPropagate)
230 : : {
231 [ + + ]: 69783 : for (size_t j = 0; j < k; ++j)
232 : : {
233 [ + + ][ + + ]: 46522 : if (admit(j, p) && !splitBasis[j].contains(p))
[ + + ]
234 : : {
235 : 2135 : newPolys[j].push_back(p);
236 : : }
237 : : }
238 : : }
239 [ + + ]: 2733 : } while (std::any_of(newPolys.begin(), newPolys.end(), [](const auto& s) {
240 : 4958 : return s.size();
241 : : }));
242 : 3408 : return splitBasis;
243 : 1704 : }
244 : :
245 : 46522 : bool admit(size_t i, const Poly& p)
246 : : {
247 [ - + ][ - + ]: 46522 : Assert(i < 2);
[ - - ]
248 [ + + ][ + + ]: 46522 : return CoCoA::deg(p) <= 1 && (i == 0 || CoCoA::NumTerms(p) <= 2);
[ + + ]
249 : : }
250 : :
251 : 117 : std::optional<Point> splitFindZero(SplitGb&& splitBasisIn,
252 : : CoCoA::ring polyRing,
253 : : BitProp& bitProp,
254 : : const Env& env,
255 : : FfStatistics* stats)
256 : : {
257 : 117 : SplitGb splitBasis = std::move(splitBasisIn);
258 : : while (true)
259 : : {
260 : 117 : Polys allGens{};
261 [ + + ]: 351 : for (const auto& b : splitBasis)
262 : : {
263 : 468 : std::copy(
264 : 234 : b.basis().begin(), b.basis().end(), std::back_inserter(allGens));
265 : : }
266 : 234 : PartialPoint nullPartialRoot(CoCoA::NumIndets(polyRing));
267 : : auto result = splitZeroExtend(allGens,
268 : 117 : SplitGb(splitBasis),
269 : 117 : std::move(nullPartialRoot),
270 : : bitProp,
271 : : env,
272 : 117 : stats);
273 [ - + ]: 117 : if (std::holds_alternative<Poly>(result))
274 : : {
275 : 0 : auto conflict = std::get<Poly>(result);
276 : 0 : std::vector<Polys> gens{};
277 [ - - ]: 0 : for (auto& b : splitBasis)
278 : : {
279 : 0 : gens.push_back({});
280 : 0 : std::copy(b.basis().begin(),
281 : 0 : b.basis().end(),
282 : 0 : std::back_inserter(gens.back()));
283 : 0 : gens.back().push_back(conflict);
284 : : }
285 : 0 : splitBasis = splitGb(gens, bitProp, env, stats);
286 : 0 : }
287 [ - + ]: 117 : else if (std::holds_alternative<bool>(result))
288 : : {
289 : 0 : return {};
290 : : }
291 : : else
292 : : {
293 : 117 : return {std::get<Point>(result)};
294 : : }
295 [ - + ][ - + ]: 351 : }
[ - + ]
296 : 117 : }
297 : :
298 : 684 : std::unique_ptr<AssignmentEnumerator> applyRule(const Gb& gb,
299 : : const CoCoA::ring& polyRing,
300 : : const PartialPoint& r)
301 : : {
302 [ - + ][ - + ]: 684 : Assert(static_cast<long>(r.size()) == CoCoA::NumIndets(polyRing));
[ - - ]
303 [ - + ][ - + ]: 1873 : Assert(std::any_of(
[ - - ]
304 : : r.begin(), r.end(), [](const auto& v) { return !v.has_value(); }));
305 : : // (1) are there any polynomials that are univariate in an unassigned
306 : : // variable?
307 : 684 : const auto& gens = gb.basis();
308 [ + + ]: 2477 : for (const auto& p : gens)
309 : : {
310 : 2301 : int varNumber = CoCoA::UnivariateIndetIndex(p);
311 [ + + ][ + + ]: 2301 : if (varNumber >= 0 && !r[varNumber].has_value())
[ + + ]
312 : : {
313 : 508 : return factorEnumerator(p);
314 : : }
315 : : }
316 : : // (2) if dimension 0, then compute such a polynomial
317 [ + + ]: 176 : if (gb.zeroDimensional())
318 : : {
319 : : // If zero-dimensional, we compute a minimal polynomial in some unset
320 : : // variable.
321 [ + - ]: 5 : for (size_t i = 0, n = r.size(); i < n; ++i)
322 : : {
323 [ + - ]: 5 : if (!r[i].has_value())
324 : : {
325 : 5 : Poly minPoly = gb.minimalPolynomial(CoCoA::indet(polyRing, i));
326 : 5 : return factorEnumerator(minPoly);
327 : 5 : }
328 : : }
329 : 0 : Unreachable() << "There should be some unset var";
330 : : }
331 : : else
332 : : {
333 : : // If positive dimension, we make a list of unset variables and
334 : : // round-robin guess.
335 : : //
336 : : // TODO(aozdemir): better model construction (cvc5-wishues/issues/138)
337 : 171 : Polys toGuess{};
338 [ + + ]: 1156 : for (size_t i = 0, n = r.size(); i < n; ++i)
339 : : {
340 [ + + ]: 985 : if (!r[i].has_value())
341 : : {
342 : 479 : toGuess.push_back(CoCoA::indet(polyRing, i));
343 : : }
344 : : }
345 : 342 : return std::make_unique<RoundRobinEnumerator>(toGuess,
346 : 342 : polyRing->myBaseRing());
347 : 171 : }
348 : : Unreachable();
349 : : return nullptr;
350 : : }
351 : :
352 : 90 : void checkZero(const SplitGb& origBases, const Point& zero)
353 : : {
354 [ + + ]: 270 : for (const auto& b : origBases)
355 : : {
356 [ + + ]: 929 : for (const auto& gen : b.basis())
357 : : {
358 : 749 : auto value = cocoaEval(gen, zero);
359 [ - + ]: 749 : if (!CoCoA::IsZero(value))
360 : : {
361 : 0 : std::stringstream o;
362 : 0 : o << "Bad zero!" << std::endl
363 : 0 : << "Generator " << gen << std::endl
364 : 0 : << "evaluated to " << value << std::endl
365 : 0 : << "under point: " << std::endl;
366 [ - - ]: 0 : for (size_t i = 0, n = zero.size(); i < n; ++i)
367 : : {
368 : 0 : o << " " << CoCoA::indet(CoCoA::owner(gen), i) << " -> " << zero[i]
369 : 0 : << std::endl;
370 : : }
371 : 0 : Assert(CoCoA::IsZero(value)) << o.str();
372 : 0 : }
373 : 749 : }
374 : : }
375 : 90 : }
376 : :
377 : 8266 : Gb::Gb() : d_ideal(), d_basis() {}
378 : 4857 : Gb::Gb(const std::vector<Poly>& generators, const ResourceManager* rm) : Gb()
379 : : {
380 [ + + ]: 4857 : if (generators.size())
381 : : {
382 : 4855 : d_ideal.emplace(CoCoA::ideal(generators));
383 : 4855 : d_basis = GBasisTimeout(d_ideal.value(), rm);
384 : : }
385 : 4857 : }
386 : :
387 : 46978 : bool Gb::contains(const Poly& p) const
388 : : {
389 [ + + ][ + + ]: 46978 : return d_ideal.has_value() && CoCoA::IsElem(p, d_ideal.value());
390 : : }
391 : 2851 : bool Gb::isWholeRing() const
392 : : {
393 [ + + ][ + + ]: 2851 : return d_ideal.has_value() && CoCoA::IsOne(d_ideal.value());
394 : : }
395 : 961 : Poly Gb::reduce(const Poly& p) const
396 : : {
397 [ + - ]: 961 : return d_ideal.has_value() ? CoCoA::NF(p, d_ideal.value()) : p;
398 : : }
399 : 383 : bool Gb::zeroDimensional() const
400 : : {
401 [ + + ][ + + ]: 383 : return d_ideal.has_value() && CoCoA::IsZeroDim(d_ideal.value());
402 : : }
403 : 5 : Poly Gb::minimalPolynomial(const Poly& var) const
404 : : {
405 [ - + ][ - + ]: 5 : Assert(zeroDimensional());
[ - - ]
406 [ - + ][ - + ]: 5 : Assert(CoCoA::UnivariateIndetIndex(var) != -1);
[ - - ]
407 : 5 : Poly minPoly = CoCoA::MinPolyQuot(var, *d_ideal, var);
408 : 5 : return minPoly;
409 : : }
410 : 15140 : const Polys& Gb::basis() const { return d_basis; }
411 : :
412 : 838 : BitProp::BitProp(const std::vector<Node>& facts, CocoaEncoder& encoder)
413 : 838 : : d_bits(), d_bitsums(encoder.bitsums()), d_enc(&encoder)
414 : : {
415 [ + + ]: 12333 : for (const auto& fact : facts)
416 : : {
417 : 11495 : auto bs = parse::bitConstraint(fact);
418 [ + + ]: 11495 : if (bs)
419 : : {
420 : 642 : d_bits.insert(*bs);
421 : : }
422 : 11495 : }
423 : 838 : }
424 : :
425 : 90 : BitProp::BitProp() : d_bits(), d_bitsums(), d_enc(nullptr) {}
426 : :
427 : 2733 : Polys BitProp::getBitEqualities(const SplitGb& splitBasis)
428 : : {
429 : 2733 : Polys output{};
430 : :
431 : 2733 : std::vector<Node> bitConstrainedBitsums{};
432 : :
433 : 2733 : std::vector<Node> nonConstantBitsums{};
434 [ + + ]: 3678 : for (const auto& bitsum : d_bitsums)
435 : : {
436 : : // does any basis know `bitsum = k`?
437 : 945 : bool isConst = false;
438 [ + + ]: 977 : for (const auto& b : splitBasis)
439 : : {
440 : 961 : Poly normal = b.reduce(d_enc->getTermEncoding(bitsum));
441 [ + + ]: 961 : if (CoCoA::IsConstant(normal))
442 : : {
443 : : // check that all inputs are bit-constrained
444 [ + + ]: 957 : if (std::all_of(bitsum.begin(), bitsum.end(), [&](const Node& bit) {
445 : 2802 : return isBit(bit, splitBasis);
446 : : }))
447 : : {
448 : : // this basis b knows that bitsum is a constant
449 : : Integer val =
450 : 1858 : d_enc->cocoaFfToFfVal(CoCoA::ConstantCoeff(normal)).getValue();
451 : :
452 [ - + ]: 929 : if (val >= Integer(2).pow(bitsum.getNumChildren()))
453 : : {
454 : 0 : output.clear();
455 : 0 : output.push_back(CoCoA::one(d_enc->polyRing()));
456 : 0 : return output;
457 : : }
458 : :
459 : : // propagate `bits(bitsum) = bits(k)`
460 [ + + ]: 3683 : for (size_t i = 0, n = bitsum.getNumChildren(); i < n; ++i)
461 : : {
462 : 2788 : auto bit = val.isBitSet(i) ? CoCoA::one(d_enc->polyRing())
463 [ + + ]: 2788 : : CoCoA::zero(d_enc->polyRing());
464 : 2754 : output.push_back(d_enc->getTermEncoding(bitsum[i]) - bit);
465 : 2754 : }
466 : 929 : isConst = true;
467 : 929 : break;
468 [ - + ]: 929 : }
469 : : }
470 [ + - ][ + ]: 961 : }
471 : : // no basis knows this bitsum is a constant :(
472 [ + + ]: 945 : if (!isConst)
473 : : {
474 : 16 : nonConstantBitsums.push_back(bitsum);
475 : : }
476 : : }
477 : :
478 : : // for all pairs of non-constant bitsums (a, b)
479 [ + + ]: 2749 : for (size_t i = 0, n = nonConstantBitsums.size(); i < n; ++i)
480 : : {
481 [ - + ]: 16 : for (size_t j = 0; j < i; ++j)
482 : : {
483 : 0 : Node a = nonConstantBitsums[i];
484 : 0 : Node b = nonConstantBitsums[j];
485 : 0 : Poly bsDiff = d_enc->getTermEncoding(a) - d_enc->getTermEncoding(b);
486 [ - - ]: 0 : if (std::any_of(
487 : 0 : splitBasis.begin(), splitBasis.end(), [&bsDiff](const auto& ii) {
488 : 0 : return ii.contains(bsDiff);
489 : : }))
490 : : {
491 : : // this basis knows a = b
492 [ - - ]: 0 : Trace("ffl::bitprop")
493 : 0 : << " (= " << a << "\n " << b << ")" << std::endl;
494 : 0 : size_t min = std::min(a.getNumChildren(), b.getNumChildren());
495 : 0 : size_t max = std::max(a.getNumChildren(), b.getNumChildren());
496 [ - - ]: 0 : if (max > d_enc->size().d_val.length())
497 : : {
498 [ - - ]: 0 : Trace("ffl::bitprop") << " bitsum overflow" << std::endl;
499 : 0 : continue;
500 : : }
501 : :
502 : : // check that all inputs to both a and b are bit-constrained
503 : 0 : bool allBits = true;
504 [ - - ]: 0 : for (const auto& sum : {a, b})
505 : : {
506 [ - - ]: 0 : for (const auto& c : sum)
507 : : {
508 [ - - ]: 0 : if (!isBit(c, splitBasis))
509 : : {
510 [ - - ]: 0 : Trace("ffl::bitprop") << " non-bit " << c << std::endl;
511 : 0 : allBits = false;
512 : : }
513 : 0 : }
514 [ - - ][ - - ]: 0 : }
515 : :
516 [ - - ]: 0 : if (!allBits) continue;
517 : :
518 : : // propagate `bits(a) = bits(b)`
519 [ - - ]: 0 : for (size_t k = 0; k < min; ++k)
520 : : {
521 : : Poly diff =
522 : 0 : d_enc->getTermEncoding(a[k]) - d_enc->getTermEncoding(b[k]);
523 : 0 : output.push_back(diff);
524 : 0 : }
525 : :
526 : 0 : if (a.getNumChildren() != min || b.getNumChildren() != min)
527 : : {
528 : : // bitsums have different lengths: propagate zeros for the longer part
529 [ - - ]: 0 : Node longer = b.getNumChildren() > min ? b : a;
530 [ - - ]: 0 : for (size_t k = min; k < max; ++k)
531 : : {
532 : 0 : Poly isZero = d_enc->getTermEncoding(longer[k]);
533 : 0 : output.push_back(isZero);
534 : 0 : }
535 : 0 : }
536 : : }
537 [ - - ][ - - ]: 0 : }
[ - - ]
538 : : }
539 : 2733 : return output;
540 : 2733 : }
541 : :
542 : 2802 : bool BitProp::isBit(const Node& possibleBit, const SplitGb& splitBasis)
543 : : {
544 [ + + ]: 2802 : if (d_bits.count(possibleBit))
545 : : {
546 : 1408 : return true;
547 : : }
548 : 1394 : Poly p = d_enc->getTermEncoding(possibleBit);
549 : 1394 : Poly bitConstraint = p * p - p;
550 [ + + ]: 1394 : if (std::any_of(splitBasis.begin(),
551 : : splitBasis.end(),
552 : 1422 : [&bitConstraint](const auto& ii) {
553 : 1422 : return ii.contains(bitConstraint);
554 : : }))
555 : : {
556 [ + - ]: 1366 : Trace("ffl::bitprop") << " bit through GB " << possibleBit << std::endl;
557 : 1366 : d_bits.insert(possibleBit);
558 : 1366 : return true;
559 : : }
560 : 28 : return false;
561 : 1394 : }
562 : :
563 : : } // namespace ff
564 : : } // namespace theory
565 : : } // namespace cvc5::internal
566 : :
567 : : #endif /* CVC5_USE_COCOA */
|
