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 : : * [[ Add one-line brief description here ]]
11 : : *
12 : : * [[ Add lengthier description here ]]
13 : : * \todo document this file
14 : : */
15 : : #include "theory/arith/linear/constraint.h"
16 : :
17 : : #include <algorithm>
18 : : #include <ostream>
19 : : #include <unordered_set>
20 : :
21 : : #include "base/output.h"
22 : : #include "options/smt_options.h"
23 : : #include "proof/eager_proof_generator.h"
24 : : #include "proof/proof_node_manager.h"
25 : : #include "smt/env.h"
26 : : #include "theory/arith/arith_proof_utilities.h"
27 : : #include "theory/arith/arith_utilities.h"
28 : : #include "theory/arith/linear/congruence_manager.h"
29 : : #include "theory/arith/linear/normal_form.h"
30 : : #include "theory/arith/linear/partial_model.h"
31 : : #include "theory/builtin/proof_checker.h"
32 : : #include "theory/rewriter.h"
33 : :
34 : : using namespace std;
35 : : using namespace cvc5::internal::kind;
36 : :
37 : : namespace cvc5::internal {
38 : : namespace theory {
39 : : namespace arith::linear {
40 : :
41 : 0 : ConstraintRule::ConstraintRule()
42 : 0 : : d_constraint(NullConstraint),
43 : 0 : d_proofType(NoAP),
44 : 0 : d_antecedentEnd(AntecedentIdSentinel)
45 : : {
46 : 0 : d_farkasCoefficients = RationalVectorCPSentinel;
47 : 0 : }
48 : :
49 : 8331799 : ConstraintRule::ConstraintRule(ConstraintP con, ArithProofType pt)
50 : 8331799 : : d_constraint(con), d_proofType(pt), d_antecedentEnd(AntecedentIdSentinel)
51 : : {
52 : 8331799 : d_farkasCoefficients = RationalVectorCPSentinel;
53 : 8331799 : }
54 : 2580025 : ConstraintRule::ConstraintRule(ConstraintP con,
55 : : ArithProofType pt,
56 : 2580025 : AntecedentId antecedentEnd)
57 : 2580025 : : d_constraint(con), d_proofType(pt), d_antecedentEnd(antecedentEnd)
58 : : {
59 : 2580025 : d_farkasCoefficients = RationalVectorCPSentinel;
60 : 2580025 : }
61 : :
62 : 2346172 : ConstraintRule::ConstraintRule(ConstraintP con,
63 : : ArithProofType pt,
64 : : AntecedentId antecedentEnd,
65 : 2346172 : RationalVectorCP coeffs)
66 : 2346172 : : d_constraint(con), d_proofType(pt), d_antecedentEnd(antecedentEnd)
67 : : {
68 [ + + ][ + - ]: 2346172 : Assert(con->isProofProducing() || coeffs == RationalVectorCPSentinel);
[ - + ][ - + ]
[ - - ]
69 : 2346172 : d_farkasCoefficients = coeffs;
70 : 2346172 : }
71 : :
72 : : /** Given a simplifiedKind this returns the corresponding ConstraintType. */
73 : : // ConstraintType constraintTypeOfLiteral(Kind k);
74 : 1187902 : ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp)
75 : : {
76 : 1187902 : Kind k = cmp.comparisonKind();
77 [ + + ][ + + ]: 1187902 : switch (k)
[ - ]
78 : : {
79 : 315064 : case Kind::LT:
80 : : case Kind::LEQ:
81 : : {
82 : 315064 : Polynomial l = cmp.getLeft();
83 [ + + ]: 315064 : if (l.leadingCoefficientIsPositive())
84 : : { // (< x c)
85 : 272769 : return UpperBound;
86 : : }
87 : : else
88 : : {
89 : 42295 : return LowerBound; // (< (-x) c)
90 : : }
91 : 315064 : }
92 : 317295 : case Kind::GT:
93 : : case Kind::GEQ:
94 : : {
95 : 317295 : Polynomial l = cmp.getLeft();
96 [ + + ]: 317295 : if (l.leadingCoefficientIsPositive())
97 : : {
98 : 274687 : return LowerBound; // (> x c)
99 : : }
100 : : else
101 : : {
102 : 42608 : return UpperBound; // (> (-x) c)
103 : : }
104 : 317295 : }
105 : 281529 : case Kind::EQUAL: return Equality;
106 : 274014 : case Kind::DISTINCT: return Disequality;
107 : 0 : default: Unhandled() << k;
108 : : }
109 : : }
110 : :
111 : 1489098 : Constraint::Constraint(ArithVar x,
112 : : ConstraintType t,
113 : : const DeltaRational& v,
114 : 1489098 : bool produceProofs)
115 : 1489098 : : d_variable(x),
116 : 1489098 : d_type(t),
117 : 1489098 : d_value(v),
118 : 1489098 : d_database(nullptr),
119 : 1489098 : d_literal(Node::null()),
120 : 1489098 : d_negation(NullConstraint),
121 : 1489098 : d_canBePropagated(false),
122 : 1489098 : d_assertionOrder(AssertionOrderSentinel),
123 : 1489098 : d_witness(TNode::null()),
124 : 1489098 : d_crid(ConstraintRuleIdSentinel),
125 : 1489098 : d_split(false),
126 : 1489098 : d_variablePosition(),
127 : 1489098 : d_produceProofs(produceProofs)
128 : : {
129 [ - + ][ - + ]: 1489098 : Assert(!initialized());
[ - - ]
130 : 1489098 : }
131 : :
132 : 0 : std::ostream& operator<<(std::ostream& o, const ArithProofType apt)
133 : : {
134 [ - - ][ - - ]: 0 : switch (apt)
[ - - ][ - - ]
[ - ]
135 : : {
136 : 0 : case NoAP: o << "NoAP"; break;
137 : 0 : case AssumeAP: o << "AssumeAP"; break;
138 : 0 : case InternalAssumeAP: o << "InternalAssumeAP"; break;
139 : 0 : case FarkasAP: o << "FarkasAP"; break;
140 : 0 : case TrichotomyAP: o << "TrichotomyAP"; break;
141 : 0 : case EqualityEngineAP: o << "EqualityEngineAP"; break;
142 : 0 : case IntTightenAP: o << "IntTightenAP"; break;
143 : 0 : case IntHoleAP: o << "IntHoleAP"; break;
144 : 0 : default: break;
145 : : }
146 : 0 : return o;
147 : : }
148 : :
149 : 0 : std::ostream& operator<<(std::ostream& o, const ConstraintCP c)
150 : : {
151 [ - - ]: 0 : if (c == NullConstraint)
152 : : {
153 : 0 : return o << "NullConstraint";
154 : : }
155 : : else
156 : : {
157 : 0 : return o << *c;
158 : : }
159 : : }
160 : :
161 : 0 : std::ostream& operator<<(std::ostream& o, const ConstraintP c)
162 : : {
163 [ - - ]: 0 : if (c == NullConstraint)
164 : : {
165 : 0 : return o << "NullConstraint";
166 : : }
167 : : else
168 : : {
169 : 0 : return o << *c;
170 : : }
171 : : }
172 : :
173 : 0 : std::ostream& operator<<(std::ostream& o, const ConstraintType t)
174 : : {
175 [ - - ][ - - ]: 0 : switch (t)
[ - ]
176 : : {
177 : 0 : case LowerBound: return o << ">=";
178 : 0 : case UpperBound: return o << "<=";
179 : 0 : case Equality: return o << "=";
180 : 0 : case Disequality: return o << "!=";
181 : 0 : default: Unreachable();
182 : : }
183 : : }
184 : :
185 : 0 : std::ostream& operator<<(std::ostream& o, const Constraint& c)
186 : : {
187 : 0 : o << c.getVariable() << ' ' << c.getType() << ' ' << c.getValue();
188 [ - - ]: 0 : if (c.hasLiteral())
189 : : {
190 : 0 : o << "(node " << c.getLiteral() << ')';
191 : : }
192 : 0 : return o;
193 : : }
194 : :
195 : 0 : std::ostream& operator<<(std::ostream& o, const ValueCollection& vc)
196 : : {
197 : 0 : o << "{";
198 : 0 : bool pending = false;
199 [ - - ]: 0 : if (vc.hasEquality())
200 : : {
201 : 0 : o << "eq: " << vc.getEquality();
202 : 0 : pending = true;
203 : : }
204 [ - - ]: 0 : if (vc.hasLowerBound())
205 : : {
206 [ - - ]: 0 : if (pending)
207 : : {
208 : 0 : o << ", ";
209 : : }
210 : 0 : o << "lb: " << vc.getLowerBound();
211 : 0 : pending = true;
212 : : }
213 [ - - ]: 0 : if (vc.hasUpperBound())
214 : : {
215 [ - - ]: 0 : if (pending)
216 : : {
217 : 0 : o << ", ";
218 : : }
219 : 0 : o << "ub: " << vc.getUpperBound();
220 : 0 : pending = true;
221 : : }
222 [ - - ]: 0 : if (vc.hasDisequality())
223 : : {
224 [ - - ]: 0 : if (pending)
225 : : {
226 : 0 : o << ", ";
227 : : }
228 : 0 : o << "de: " << vc.getDisequality();
229 : : }
230 : 0 : return o << "}";
231 : : }
232 : :
233 : 0 : std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v)
234 : : {
235 : 0 : o << "[" << v.size() << "x";
236 : 0 : ConstraintCPVec::const_iterator i, end;
237 [ - - ]: 0 : for (i = v.begin(), end = v.end(); i != end; ++i)
238 : : {
239 : 0 : ConstraintCP c = *i;
240 : 0 : o << ", " << (*c);
241 : : }
242 : 0 : o << "]";
243 : 0 : return o;
244 : : }
245 : :
246 : 3625022 : ValueCollection::ValueCollection()
247 : 3625022 : : d_lowerBound(NullConstraint),
248 : 3625022 : d_upperBound(NullConstraint),
249 : 3625022 : d_equality(NullConstraint),
250 : 3625022 : d_disequality(NullConstraint)
251 : : {
252 : 3625022 : }
253 : :
254 : 29049591 : bool ValueCollection::hasLowerBound() const
255 : : {
256 : 29049591 : return d_lowerBound != NullConstraint;
257 : : }
258 : :
259 : 29744682 : bool ValueCollection::hasUpperBound() const
260 : : {
261 : 29744682 : return d_upperBound != NullConstraint;
262 : : }
263 : :
264 : 9702273 : bool ValueCollection::hasEquality() const
265 : : {
266 : 9702273 : return d_equality != NullConstraint;
267 : : }
268 : :
269 : 23077154 : bool ValueCollection::hasDisequality() const
270 : : {
271 : 23077154 : return d_disequality != NullConstraint;
272 : : }
273 : :
274 : 5053273 : ConstraintP ValueCollection::getLowerBound() const
275 : : {
276 [ - + ][ - + ]: 5053273 : Assert(hasLowerBound());
[ - - ]
277 : 5053273 : return d_lowerBound;
278 : : }
279 : :
280 : 5190616 : ConstraintP ValueCollection::getUpperBound() const
281 : : {
282 [ - + ][ - + ]: 5190616 : Assert(hasUpperBound());
[ - - ]
283 : 5190616 : return d_upperBound;
284 : : }
285 : :
286 : 722446 : ConstraintP ValueCollection::getEquality() const
287 : : {
288 [ - + ][ - + ]: 722446 : Assert(hasEquality());
[ - - ]
289 : 722446 : return d_equality;
290 : : }
291 : :
292 : 2910537 : ConstraintP ValueCollection::getDisequality() const
293 : : {
294 [ - + ][ - + ]: 2910537 : Assert(hasDisequality());
[ - - ]
295 : 2910537 : return d_disequality;
296 : : }
297 : :
298 : 994956 : void ValueCollection::push_into(std::vector<ConstraintP>& vec) const
299 : : {
300 [ + - ]: 994956 : Trace("arith::constraint") << "push_into " << *this << endl;
301 [ + + ]: 994956 : if (hasEquality())
302 : : {
303 : 282621 : vec.push_back(d_equality);
304 : : }
305 [ + + ]: 994956 : if (hasLowerBound())
306 : : {
307 : 455593 : vec.push_back(d_lowerBound);
308 : : }
309 [ + + ]: 994956 : if (hasUpperBound())
310 : : {
311 : 455593 : vec.push_back(d_upperBound);
312 : : }
313 [ + + ]: 994956 : if (hasDisequality())
314 : : {
315 : 282621 : vec.push_back(d_disequality);
316 : : }
317 : 994956 : }
318 : :
319 : 0 : ValueCollection ValueCollection::mkFromConstraint(ConstraintP c)
320 : : {
321 : 0 : ValueCollection ret;
322 : 0 : Assert(ret.empty());
323 [ - - ][ - - ]: 0 : switch (c->getType())
[ - ]
324 : : {
325 : 0 : case LowerBound: ret.d_lowerBound = c; break;
326 : 0 : case UpperBound: ret.d_upperBound = c; break;
327 : 0 : case Equality: ret.d_equality = c; break;
328 : 0 : case Disequality: ret.d_disequality = c; break;
329 : 0 : default: Unreachable();
330 : : }
331 : 0 : return ret;
332 : : }
333 : :
334 : 6093191 : bool ValueCollection::hasConstraintOfType(ConstraintType t) const
335 : : {
336 [ + + ][ + - ]: 6093191 : switch (t)
[ - ]
337 : : {
338 : 2236107 : case LowerBound: return hasLowerBound();
339 : 2991459 : case UpperBound: return hasUpperBound();
340 : 865625 : case Equality: return hasEquality();
341 : 0 : case Disequality: return hasDisequality();
342 : 0 : default: Unreachable();
343 : : }
344 : : }
345 : :
346 : 502797 : ArithVar ValueCollection::getVariable() const
347 : : {
348 [ - + ][ - + ]: 502797 : Assert(!empty());
[ - - ]
349 : 502797 : return nonNull()->getVariable();
350 : : }
351 : :
352 : 502797 : const DeltaRational& ValueCollection::getValue() const
353 : : {
354 [ - + ][ - + ]: 502797 : Assert(!empty());
[ - - ]
355 : 502797 : return nonNull()->getValue();
356 : : }
357 : :
358 : 1478900 : void ValueCollection::add(ConstraintP c)
359 : : {
360 [ - + ][ - + ]: 1478900 : Assert(c != NullConstraint);
[ - - ]
361 : :
362 [ + + ][ + - ]: 1478900 : Assert(empty() || getVariable() == c->getVariable());
[ - + ][ - + ]
[ - - ]
363 [ + + ][ + - ]: 1478900 : Assert(empty() || getValue() == c->getValue());
[ - + ][ - + ]
[ - - ]
364 : :
365 [ + + ][ + + ]: 1478900 : switch (c->getType())
[ - ]
366 : : {
367 : 456829 : case LowerBound:
368 [ - + ][ - + ]: 456829 : Assert(!hasLowerBound());
[ - - ]
369 : 456829 : d_lowerBound = c;
370 : 456829 : break;
371 : 282621 : case Equality:
372 [ - + ][ - + ]: 282621 : Assert(!hasEquality());
[ - - ]
373 : 282621 : d_equality = c;
374 : 282621 : break;
375 : 456829 : case UpperBound:
376 [ - + ][ - + ]: 456829 : Assert(!hasUpperBound());
[ - - ]
377 : 456829 : d_upperBound = c;
378 : 456829 : break;
379 : 282621 : case Disequality:
380 [ - + ][ - + ]: 282621 : Assert(!hasDisequality());
[ - - ]
381 : 282621 : d_disequality = c;
382 : 282621 : break;
383 : 0 : default: Unreachable();
384 : : }
385 : 1478900 : }
386 : :
387 : 4421047 : ConstraintP ValueCollection::getConstraintOfType(ConstraintType t) const
388 : : {
389 [ + + ][ + - ]: 4421047 : switch (t)
[ - ]
390 : : {
391 [ - + ][ - + ]: 1360804 : case LowerBound: Assert(hasLowerBound()); return d_lowerBound;
[ - - ]
392 [ - + ][ - + ]: 583004 : case Equality: Assert(hasEquality()); return d_equality;
[ - - ]
393 [ - + ][ - + ]: 2477239 : case UpperBound: Assert(hasUpperBound()); return d_upperBound;
[ - - ]
394 : 0 : case Disequality: Assert(hasDisequality()); return d_disequality;
395 : 0 : default: Unreachable();
396 : : }
397 : : }
398 : :
399 : 1478900 : void ValueCollection::remove(ConstraintType t)
400 : : {
401 [ + + ][ + + ]: 1478900 : switch (t)
[ - ]
402 : : {
403 : 456829 : case LowerBound:
404 [ - + ][ - + ]: 456829 : Assert(hasLowerBound());
[ - - ]
405 : 456829 : d_lowerBound = NullConstraint;
406 : 456829 : break;
407 : 282621 : case Equality:
408 [ - + ][ - + ]: 282621 : Assert(hasEquality());
[ - - ]
409 : 282621 : d_equality = NullConstraint;
410 : 282621 : break;
411 : 456829 : case UpperBound:
412 [ - + ][ - + ]: 456829 : Assert(hasUpperBound());
[ - - ]
413 : 456829 : d_upperBound = NullConstraint;
414 : 456829 : break;
415 : 282621 : case Disequality:
416 [ - + ][ - + ]: 282621 : Assert(hasDisequality());
[ - - ]
417 : 282621 : d_disequality = NullConstraint;
418 : 282621 : break;
419 : 0 : default: Unreachable();
420 : : }
421 : 1478900 : }
422 : :
423 : 5442294 : bool ValueCollection::empty() const
424 : : {
425 [ + + ][ + + ]: 8431998 : return !(hasLowerBound() || hasUpperBound() || hasEquality()
[ + + ]
426 [ + - ]: 8431998 : || hasDisequality());
427 : : }
428 : :
429 : 1005594 : ConstraintP ValueCollection::nonNull() const
430 : : {
431 : : // This can be optimized by caching, but this is not necessary yet!
432 : : /* "Premature optimization is the root of all evil." */
433 [ + + ]: 1005594 : if (hasLowerBound())
434 : : {
435 : 321498 : return d_lowerBound;
436 : : }
437 [ + + ]: 684096 : else if (hasUpperBound())
438 : : {
439 : 91240 : return d_upperBound;
440 : : }
441 [ + - ]: 592856 : else if (hasEquality())
442 : : {
443 : 592856 : return d_equality;
444 : : }
445 [ - - ]: 0 : else if (hasDisequality())
446 : : {
447 : 0 : return d_disequality;
448 : : }
449 : : else
450 : : {
451 : 0 : return NullConstraint;
452 : : }
453 : : }
454 : :
455 : 5303634 : bool Constraint::initialized() const { return d_database != nullptr; }
456 : :
457 : 0 : const ConstraintDatabase& Constraint::getDatabase() const
458 : : {
459 : 0 : Assert(initialized());
460 : 0 : return *d_database;
461 : : }
462 : :
463 : 1478900 : void Constraint::initialize(ConstraintDatabase* db,
464 : : SortedConstraintMapIterator v,
465 : : ConstraintP negation)
466 : : {
467 [ - + ][ - + ]: 1478900 : Assert(!initialized());
[ - - ]
468 : 1478900 : d_database = db;
469 : 1478900 : d_variablePosition = v;
470 : 1478900 : d_negation = negation;
471 : 1478900 : }
472 : :
473 : 2978196 : Constraint::~Constraint()
474 : : {
475 : : // Call this instead of safeToGarbageCollect()
476 [ - + ][ - + ]: 1489098 : Assert(!contextDependentDataIsSet());
477 : :
478 [ + + ]: 1489098 : if (initialized())
479 : : {
480 : 1478900 : ValueCollection& vc = d_variablePosition->second;
481 [ + - ]: 1478900 : Trace("arith::constraint") << "removing" << vc << endl;
482 : :
483 : 1478900 : vc.remove(getType());
484 : :
485 [ + + ]: 1478900 : if (vc.empty())
486 : : {
487 [ + - ]: 996568 : Trace("arith::constraint") << "erasing" << vc << endl;
488 : : SortedConstraintMap& perVariable =
489 : 996568 : d_database->getVariableSCM(getVariable());
490 : 996568 : perVariable.erase(d_variablePosition);
491 : : }
492 : :
493 [ + + ]: 1478900 : if (hasLiteral())
494 : : {
495 : 1182104 : d_database->d_nodetoConstraintMap.erase(getLiteral());
496 : : }
497 : : std::unordered_map<ConstraintP, std::vector<Node>>::iterator ita =
498 : 1478900 : d_database->d_altLiterals.find(this);
499 [ + + ]: 1478900 : if (ita != d_database->d_altLiterals.end())
500 : : {
501 [ + + ]: 26594 : for (const Node& l : ita->second)
502 : : {
503 : 14200 : d_database->d_nodetoConstraintMap.erase(l);
504 : : }
505 : 12394 : d_database->d_altLiterals.erase(ita);
506 : : }
507 : : }
508 : 1489098 : }
509 : :
510 : 35057327 : const ConstraintRule& Constraint::getConstraintRule() const
511 : : {
512 [ - + ][ - + ]: 35057327 : Assert(hasProof());
[ - - ]
513 : 35057327 : return d_database->d_watches->d_constraintProofs[d_crid];
514 : : }
515 : :
516 : 5041217 : const ValueCollection& Constraint::getValueCollection() const
517 : : {
518 : 5041217 : return d_variablePosition->second;
519 : : }
520 : :
521 : 150198 : ConstraintP Constraint::getCeiling()
522 : : {
523 [ + - ]: 150198 : Trace("getCeiling") << "Constraint_::getCeiling on " << *this << endl;
524 [ - + ][ - + ]: 150198 : Assert(getValue().getInfinitesimalPart().sgn() > 0);
[ - - ]
525 : :
526 : 300396 : const DeltaRational ceiling(getValue().ceiling());
527 : 300396 : return d_database->getConstraint(getVariable(), getType(), ceiling);
528 : 150198 : }
529 : :
530 : 1814046 : ConstraintP Constraint::getFloor()
531 : : {
532 [ - + ][ - + ]: 1814046 : Assert(getValue().getInfinitesimalPart().sgn() < 0);
[ - - ]
533 : :
534 : 3628092 : const DeltaRational floor(Rational(getValue().floor()));
535 : 3628092 : return d_database->getConstraint(getVariable(), getType(), floor);
536 : 1814046 : }
537 : :
538 : 2371132 : void Constraint::setCanBePropagated()
539 : : {
540 [ - + ][ - + ]: 2371132 : Assert(!canBePropagated());
[ - - ]
541 : 2371132 : d_database->pushCanBePropagatedWatch(this);
542 : 2371132 : }
543 : :
544 : 9051809 : void Constraint::setAssertedToTheTheory(TNode witness, bool nowInConflict)
545 : : {
546 [ - + ][ - + ]: 9051809 : Assert(hasLiteral());
[ - - ]
547 [ - + ][ - + ]: 9051809 : Assert(!assertedToTheTheory());
[ - - ]
548 [ - + ][ - + ]: 9051809 : Assert(negationHasProof() == nowInConflict);
[ - - ]
549 : 9051809 : d_database->pushAssertionOrderWatch(this, witness);
550 : :
551 : 9051809 : if (TraceIsOn("constraint::conflictCommit") && nowInConflict)
552 : : {
553 [ - - ]: 0 : Trace("constraint::conflictCommit") << "inConflict@setAssertedToTheTheory";
554 [ - - ]: 0 : Trace("constraint::conflictCommit") << "\t" << this << std::endl;
555 [ - - ]: 0 : Trace("constraint::conflictCommit") << "\t" << getNegation() << std::endl;
556 [ - - ]: 0 : Trace("constraint::conflictCommit")
557 : 0 : << "\t" << getNegation()->externalExplainByAssertions() << std::endl;
558 : : }
559 : 9051809 : }
560 : :
561 : 0 : bool Constraint::satisfiedBy(const DeltaRational& dr) const
562 : : {
563 [ - - ][ - - ]: 0 : switch (getType())
[ - ]
564 : : {
565 : 0 : case LowerBound: return getValue() <= dr;
566 : 0 : case Equality: return getValue() == dr;
567 : 0 : case UpperBound: return getValue() >= dr;
568 : 0 : case Disequality: return getValue() != dr;
569 : : }
570 : 0 : Unreachable();
571 : : }
572 : :
573 : 14486689 : bool Constraint::isInternalAssumption() const
574 : : {
575 : 14486689 : return getProofType() == InternalAssumeAP;
576 : : }
577 : :
578 : 0 : TrustNode Constraint::externalExplainByAssertions() const
579 : : {
580 : 0 : NodeBuilder nb(d_database->nodeManager(), Kind::AND);
581 : 0 : auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel);
582 : 0 : Node exp = mkAndFromBuilder(d_database->nodeManager(), nb);
583 [ - - ]: 0 : if (d_database->isProofEnabled())
584 : : {
585 : 0 : std::vector<Node> assumptions;
586 [ - - ]: 0 : if (exp.getKind() == Kind::AND)
587 : : {
588 : 0 : assumptions.insert(assumptions.end(), exp.begin(), exp.end());
589 : : }
590 : : else
591 : : {
592 : 0 : assumptions.push_back(exp);
593 : : }
594 : 0 : auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
595 : 0 : return d_database->d_pfGen->mkTrustedPropagation(
596 : 0 : getLiteral(), d_database->nodeManager()->mkAnd(assumptions), pf);
597 : 0 : }
598 : 0 : return TrustNode::mkTrustPropExp(getLiteral(), exp);
599 : 0 : }
600 : :
601 : 15513966 : bool Constraint::isAssumption() const { return getProofType() == AssumeAP; }
602 : :
603 : 1019437 : bool Constraint::hasEqualityEngineProof() const
604 : : {
605 : 1019437 : return getProofType() == EqualityEngineAP;
606 : : }
607 : :
608 : 7732 : bool Constraint::hasFarkasProof() const { return getProofType() == FarkasAP; }
609 : :
610 : 0 : bool Constraint::hasSimpleFarkasProof() const
611 : : {
612 [ - - ]: 0 : Trace("constraints::hsfp") << "hasSimpleFarkasProof " << this << std::endl;
613 [ - - ]: 0 : if (!hasFarkasProof())
614 : : {
615 [ - - ]: 0 : Trace("constraints::hsfp") << "There is no simple Farkas proof because "
616 : 0 : "there is no farkas proof."
617 : 0 : << std::endl;
618 : 0 : return false;
619 : : }
620 : :
621 : : // For each antecdent ...
622 : 0 : AntecedentId i = getConstraintRule().d_antecedentEnd;
623 [ - - ]: 0 : for (ConstraintCP a = d_database->getAntecedent(i); a != NullConstraint;
624 : 0 : a = d_database->getAntecedent(--i))
625 : : {
626 : : // ... that antecdent must be an assumption OR a tightened assumption ...
627 [ - - ]: 0 : if (a->isPossiblyTightenedAssumption())
628 : : {
629 : 0 : continue;
630 : : }
631 : :
632 : : // ... otherwise, we do not have a simple Farkas proof.
633 [ - - ]: 0 : if (TraceIsOn("constraints::hsfp"))
634 : : {
635 [ - - ]: 0 : Trace("constraints::hsfp") << "There is no simple Farkas proof b/c there "
636 : 0 : "is an antecdent w/ rule ";
637 [ - - ]: 0 : a->getConstraintRule().print(Trace("constraints::hsfp"), d_produceProofs);
638 [ - - ]: 0 : Trace("constraints::hsfp") << std::endl;
639 : : }
640 : :
641 : 0 : return false;
642 : : }
643 : 0 : return true;
644 : : }
645 : :
646 : 0 : bool Constraint::isPossiblyTightenedAssumption() const
647 : : {
648 : : // ... that antecdent must be an assumption ...
649 : :
650 [ - - ]: 0 : if (isAssumption()) return true;
651 [ - - ]: 0 : if (!hasIntTightenProof()) return false;
652 [ - - ]: 0 : if (getConstraintRule().d_antecedentEnd == AntecedentIdSentinel) return false;
653 : 0 : return d_database->getAntecedent(getConstraintRule().d_antecedentEnd)
654 : 0 : ->isAssumption();
655 : : }
656 : :
657 : 4752 : bool Constraint::hasIntTightenProof() const
658 : : {
659 : 4752 : return getProofType() == IntTightenAP;
660 : : }
661 : :
662 : 6508 : bool Constraint::hasIntHoleProof() const { return getProofType() == IntHoleAP; }
663 : :
664 : 7732 : bool Constraint::hasTrichotomyProof() const
665 : : {
666 : 7732 : return getProofType() == TrichotomyAP;
667 : : }
668 : :
669 : 0 : void Constraint::printProofTree(std::ostream& out, size_t depth) const
670 : : {
671 [ - - ]: 0 : if (d_produceProofs)
672 : : {
673 : 0 : const ConstraintRule& rule = getConstraintRule();
674 : 0 : out << std::string(2 * depth, ' ') << "* " << getVariable() << " [";
675 : 0 : out << getProofLiteral();
676 [ - - ]: 0 : if (assertedToTheTheory())
677 : : {
678 : 0 : out << " | wit: " << getWitness();
679 : : }
680 : 0 : out << "]" << ' ' << getType() << ' ' << getValue() << " ("
681 : 0 : << getProofType() << ")";
682 [ - - ]: 0 : if (getProofType() == FarkasAP)
683 : : {
684 : 0 : out << " [";
685 : 0 : bool first = true;
686 [ - - ]: 0 : for (const auto& coeff : *rule.d_farkasCoefficients)
687 : : {
688 [ - - ]: 0 : if (!first)
689 : : {
690 : 0 : out << ", ";
691 : : }
692 : 0 : first = false;
693 : 0 : out << coeff;
694 : : }
695 : 0 : out << "]";
696 : : }
697 : 0 : out << endl;
698 : :
699 [ - - ]: 0 : for (AntecedentId i = rule.d_antecedentEnd; i != AntecedentIdSentinel; --i)
700 : : {
701 : 0 : ConstraintCP antecdent = d_database->getAntecedent(i);
702 [ - - ]: 0 : if (antecdent == NullConstraint)
703 : : {
704 : 0 : break;
705 : : }
706 : 0 : antecdent->printProofTree(out, depth + 1);
707 : : }
708 : 0 : return;
709 : : }
710 : 0 : out << "Cannot print proof. This is not a proof build." << endl;
711 : : }
712 : :
713 : 1196304 : bool Constraint::sanityChecking(Node n) const
714 : : {
715 : 1196304 : Comparison cmp = Comparison::parseNormalForm(n);
716 : 1196304 : Kind k = cmp.comparisonKind();
717 : 1196304 : Polynomial pleft = cmp.normalizedVariablePart();
718 [ + + ][ + + ]: 1196304 : Assert(k == Kind::EQUAL || k == Kind::DISTINCT
[ + + ][ + - ]
[ - + ][ - + ]
[ - - ]
719 : : || pleft.leadingCoefficientIsPositive());
720 : 1196304 : Assert(
721 : : k != Kind::EQUAL
722 : : || Monomial::isMember(n[0].getKind() == Kind::TO_REAL ? n[0][0] : n[0]));
723 : 1196304 : Assert(k != Kind::DISTINCT
724 : : || Monomial::isMember(n[0][0].getKind() == Kind::TO_REAL ? n[0][0][0]
725 : : : n[0][0]));
726 : :
727 : 1196304 : TNode left = pleft.getNode();
728 : 1196304 : DeltaRational right = cmp.normalizedDeltaRational();
729 : :
730 : 1196304 : const ArithVariables& avariables = d_database->getArithVariables();
731 : :
732 [ + - ]: 1196304 : Trace("Constraint::sanityChecking") << cmp.getNode() << endl;
733 [ + - ]: 1196304 : Trace("Constraint::sanityChecking") << k << endl;
734 [ + - ]: 1196304 : Trace("Constraint::sanityChecking") << pleft.getNode() << endl;
735 [ + - ]: 1196304 : Trace("Constraint::sanityChecking") << left << endl;
736 [ + - ]: 1196304 : Trace("Constraint::sanityChecking") << right << endl;
737 [ + - ]: 1196304 : Trace("Constraint::sanityChecking") << getValue() << endl;
738 [ + - ][ - + ]: 1196304 : Trace("Constraint::sanityChecking") << avariables.hasArithVar(left) << endl;
[ - - ]
739 [ + - ][ - + ]: 1196304 : Trace("Constraint::sanityChecking") << avariables.asArithVar(left) << endl;
[ - - ]
740 [ + - ]: 1196304 : Trace("Constraint::sanityChecking") << getVariable() << endl;
741 : :
742 [ + - ][ - - ]: 1196304 : if (avariables.hasArithVar(left)
743 [ + - ][ + - ]: 1196304 : && avariables.asArithVar(left) == getVariable() && getValue() == right)
[ + - ][ + - ]
[ + - ][ - - ]
744 : : {
745 [ + + ][ + - ]: 1196304 : switch (getType())
746 : : {
747 : 633246 : case LowerBound:
748 : : case UpperBound:
749 : : // Be overapproximate
750 [ + + ][ - + ]: 633246 : return k == Kind::GT || k == Kind::GEQ || k == Kind::LT
751 [ + - ][ - - ]: 1266492 : || k == Kind::LEQ;
752 : 281529 : case Equality: return k == Kind::EQUAL;
753 : 281529 : case Disequality: return k == Kind::DISTINCT;
754 : 0 : default: Unreachable();
755 : : }
756 : : }
757 : : else
758 : : {
759 : 0 : return false;
760 : : }
761 : 1196304 : }
762 : :
763 : 0 : ConstraintCP ConstraintDatabase::getAntecedent(AntecedentId p) const
764 : : {
765 : 0 : Assert(p < d_antecedents.size());
766 : 0 : return d_antecedents[p];
767 : : }
768 : :
769 : 0 : void ConstraintRule::print(std::ostream& out, bool produceProofs) const
770 : : {
771 [ - - ]: 0 : RationalVectorCP coeffs = produceProofs ? d_farkasCoefficients : nullptr;
772 : 0 : out << "{ConstraintRule, ";
773 : 0 : out << d_constraint << std::endl;
774 : 0 : out << "d_proofType= " << d_proofType << ", " << std::endl;
775 : 0 : out << "d_antecedentEnd= " << d_antecedentEnd << std::endl;
776 : :
777 [ - - ][ - - ]: 0 : if (d_constraint != NullConstraint && d_antecedentEnd != AntecedentIdSentinel)
778 : : {
779 : 0 : const ConstraintDatabase& database = d_constraint->getDatabase();
780 : :
781 : : size_t coeffIterator =
782 [ - - ]: 0 : (coeffs != RationalVectorCPSentinel) ? coeffs->size() - 1 : 0;
783 : 0 : AntecedentId p = d_antecedentEnd;
784 : : // must have at least one antecedent
785 : 0 : ConstraintCP antecedent = database.getAntecedent(p);
786 [ - - ]: 0 : while (antecedent != NullConstraint)
787 : : {
788 [ - - ]: 0 : if (coeffs != RationalVectorCPSentinel)
789 : : {
790 : 0 : out << coeffs->at(coeffIterator);
791 : : }
792 : : else
793 : : {
794 : 0 : out << "_";
795 : : }
796 : 0 : out << " * (" << *antecedent << ")" << std::endl;
797 : :
798 : 0 : Assert((coeffs == RationalVectorCPSentinel) || coeffIterator > 0);
799 : 0 : --p;
800 : 0 : coeffIterator =
801 [ - - ]: 0 : (coeffs != RationalVectorCPSentinel) ? coeffIterator - 1 : 0;
802 : 0 : antecedent = database.getAntecedent(p);
803 : : }
804 [ - - ]: 0 : if (coeffs != RationalVectorCPSentinel)
805 : : {
806 : 0 : out << coeffs->front();
807 : : }
808 : : else
809 : : {
810 : 0 : out << "_";
811 : : }
812 : 0 : out << " * (" << *(d_constraint->getNegation()) << ")";
813 : 0 : out << " [not d_constraint] " << endl;
814 : : }
815 : 0 : out << "}";
816 : 0 : }
817 : :
818 : 2346172 : bool Constraint::wellFormedFarkasProof(NodeManager* nm) const
819 : : {
820 [ - + ][ - + ]: 2346172 : Assert(hasProof());
[ - - ]
821 : :
822 : 2346172 : const ConstraintRule& cr = getConstraintRule();
823 [ - + ]: 2346172 : if (cr.d_constraint != this)
824 : : {
825 : 0 : return false;
826 : : }
827 [ - + ]: 2346172 : if (cr.d_proofType != FarkasAP)
828 : : {
829 : 0 : return false;
830 : : }
831 : :
832 : 2346172 : AntecedentId p = cr.d_antecedentEnd;
833 : :
834 : : // must have at least one antecedent
835 : 2346172 : ConstraintCP antecedent = d_database->d_antecedents[p];
836 [ - + ]: 2346172 : if (antecedent == NullConstraint)
837 : : {
838 : 0 : return false;
839 : : }
840 : :
841 [ + + ]: 2346172 : if (!d_produceProofs)
842 : : {
843 : 939757 : return cr.d_farkasCoefficients == RationalVectorCPSentinel;
844 : : }
845 [ - + ][ - + ]: 1406415 : Assert(d_produceProofs);
[ - - ]
846 : :
847 [ - + ]: 1406415 : if (cr.d_farkasCoefficients == RationalVectorCPSentinel)
848 : : {
849 : 0 : return false;
850 : : }
851 [ - + ]: 1406415 : if (cr.d_farkasCoefficients->size() < 2)
852 : : {
853 : 0 : return false;
854 : : }
855 : :
856 : 1406415 : const ArithVariables& vars = d_database->getArithVariables();
857 : :
858 : 1406415 : DeltaRational rhs(0);
859 : 1406415 : Node lhs = Polynomial::mkZero(nm).getNode();
860 : :
861 : : RationalVector::const_iterator coeffIterator =
862 : 1406415 : cr.d_farkasCoefficients->end() - 1;
863 : 1406415 : RationalVector::const_iterator coeffBegin = cr.d_farkasCoefficients->begin();
864 : :
865 [ + + ]: 3655673 : while (antecedent != NullConstraint)
866 : : {
867 : 2249258 : Assert(lhs.isNull() || Polynomial::isMember(lhs));
868 : :
869 : 2249258 : const Rational& coeff = *coeffIterator;
870 : 2249258 : int coeffSgn = coeff.sgn();
871 : :
872 : 2249258 : rhs += antecedent->getValue() * coeff;
873 : :
874 : 2249258 : ArithVar antVar = antecedent->getVariable();
875 [ + - ][ + - ]: 2249258 : if (!lhs.isNull() && vars.hasNode(antVar))
[ + - ]
876 : : {
877 : 2249258 : Node antAsNode = vars.asNode(antVar);
878 [ + - ]: 2249258 : if (Polynomial::isMember(antAsNode))
879 : : {
880 : 2249258 : Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
881 : 2249258 : Polynomial antPoly = Polynomial::parsePolynomial(antAsNode);
882 : 2249258 : Polynomial sum = lhsPoly + (antPoly * coeff);
883 : 2249258 : lhs = sum.getNode();
884 : 2249258 : }
885 : : else
886 : : {
887 : 0 : lhs = Node::null();
888 : : }
889 : 2249258 : }
890 : : else
891 : : {
892 : 0 : lhs = Node::null();
893 : : }
894 [ + - ]: 4498516 : Trace("constraints::wffp")
895 : 2249258 : << "running sum: " << lhs << " <= " << rhs << endl;
896 : :
897 [ + + ][ + - ]: 2249258 : switch (antecedent->getType())
898 : : {
899 : 981012 : case LowerBound:
900 : : // fc[l] < 0, therefore return false if coeffSgn >= 0
901 [ - + ]: 981012 : if (coeffSgn >= 0)
902 : : {
903 : 0 : return false;
904 : : }
905 : 981012 : break;
906 : 386713 : case UpperBound:
907 : : // fc[u] > 0, therefore return false if coeffSgn <= 0
908 [ - + ]: 386713 : if (coeffSgn <= 0)
909 : : {
910 : 0 : return false;
911 : : }
912 : 386713 : break;
913 : 881533 : case Equality:
914 [ - + ]: 881533 : if (coeffSgn == 0)
915 : : {
916 : 0 : return false;
917 : : }
918 : 881533 : break;
919 : 0 : case Disequality:
920 : 0 : default: return false;
921 : : }
922 : :
923 [ - + ]: 2249258 : if (coeffIterator == coeffBegin)
924 : : {
925 : 0 : return false;
926 : : }
927 : 2249258 : --coeffIterator;
928 : 2249258 : --p;
929 : 2249258 : antecedent = d_database->d_antecedents[p];
930 : : }
931 [ - + ]: 1406415 : if (coeffIterator != coeffBegin)
932 : : {
933 : 0 : return false;
934 : : }
935 : :
936 : 1406415 : const Rational& firstCoeff = (*coeffBegin);
937 : 1406415 : int firstCoeffSgn = firstCoeff.sgn();
938 : 1406415 : rhs += (getNegation()->getValue()) * firstCoeff;
939 [ + - ][ + - ]: 1406415 : if (!lhs.isNull() && vars.hasNode(getVariable()))
[ + - ]
940 : : {
941 : 1406415 : Node firstAsNode = vars.asNode(getVariable());
942 [ + - ]: 1406415 : if (Polynomial::isMember(firstAsNode))
943 : : {
944 : 1406415 : Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
945 : 1406415 : Polynomial firstPoly = Polynomial::parsePolynomial(firstAsNode);
946 : 1406415 : Polynomial sum = lhsPoly + (firstPoly * firstCoeff);
947 : 1406415 : lhs = sum.getNode();
948 : 1406415 : }
949 : : else
950 : : {
951 : 0 : lhs = Node::null();
952 : : }
953 : 1406415 : }
954 : : else
955 : : {
956 : 0 : lhs = Node::null();
957 : : }
958 : :
959 [ + + ][ + - ]: 1406415 : switch (getNegation()->getType())
960 : : {
961 : 299982 : case LowerBound:
962 : : // fc[l] < 0, therefore return false if coeffSgn >= 0
963 [ - + ]: 299982 : if (firstCoeffSgn >= 0)
964 : : {
965 : 0 : return false;
966 : : }
967 : 299982 : break;
968 : 676325 : case UpperBound:
969 : : // fc[u] > 0, therefore return false if coeffSgn <= 0
970 [ - + ]: 676325 : if (firstCoeffSgn <= 0)
971 : : {
972 : 0 : return false;
973 : : }
974 : 676325 : break;
975 : 430108 : case Equality:
976 [ - + ]: 430108 : if (firstCoeffSgn == 0)
977 : : {
978 : 0 : return false;
979 : : }
980 : 430108 : break;
981 : 0 : case Disequality:
982 : 0 : default: return false;
983 : : }
984 [ + - ]: 1406415 : Trace("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl;
985 : : // 0 = lhs <= rhs < 0
986 : 2812830 : return (lhs.isNull() || (Constant::isMember(lhs) && Constant(lhs).isZero()))
987 [ + - ][ + - ]: 2812830 : && rhs.sgn() < 0;
[ + - ]
988 : 1406415 : }
989 : :
990 : 151496 : ConstraintP Constraint::makeNegation(ArithVar v,
991 : : ConstraintType t,
992 : : const DeltaRational& r,
993 : : bool produceProofs)
994 : : {
995 [ + + ][ + - ]: 151496 : switch (t)
[ - ]
996 : : {
997 : 7107 : case LowerBound:
998 : : {
999 [ - + ][ - + ]: 7107 : Assert(r.infinitesimalSgn() >= 0);
[ - - ]
1000 [ - + ]: 7107 : if (r.infinitesimalSgn() > 0)
1001 : : {
1002 : 0 : Assert(r.getInfinitesimalPart() == 1);
1003 : : // make (not (v > r)), which is (v <= r)
1004 : 0 : DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
1005 : 0 : return new Constraint(v, UpperBound, dropInf, produceProofs);
1006 : 0 : }
1007 : : else
1008 : : {
1009 [ - + ][ - + ]: 7107 : Assert(r.infinitesimalSgn() == 0);
[ - - ]
1010 : : // make (not (v >= r)), which is (v < r)
1011 : 7107 : DeltaRational addInf(r.getNoninfinitesimalPart(), -1);
1012 : 7107 : return new Constraint(v, UpperBound, addInf, produceProofs);
1013 : 7107 : }
1014 : : }
1015 : 135782 : case UpperBound:
1016 : : {
1017 [ - + ][ - + ]: 135782 : Assert(r.infinitesimalSgn() <= 0);
[ - - ]
1018 [ + + ]: 135782 : if (r.infinitesimalSgn() < 0)
1019 : : {
1020 [ - + ][ - + ]: 820 : Assert(r.getInfinitesimalPart() == -1);
[ - - ]
1021 : : // make (not (v < r)), which is (v >= r)
1022 : 820 : DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
1023 : 820 : return new Constraint(v, LowerBound, dropInf, produceProofs);
1024 : 820 : }
1025 : : else
1026 : : {
1027 [ - + ][ - + ]: 134962 : Assert(r.infinitesimalSgn() == 0);
[ - - ]
1028 : : // make (not (v <= r)), which is (v > r)
1029 : 134962 : DeltaRational addInf(r.getNoninfinitesimalPart(), 1);
1030 : 134962 : return new Constraint(v, LowerBound, addInf, produceProofs);
1031 : 134962 : }
1032 : : }
1033 : 8607 : case Equality: return new Constraint(v, Disequality, r, produceProofs);
1034 : 0 : case Disequality: return new Constraint(v, Equality, r, produceProofs);
1035 : 0 : default: Unreachable(); return NullConstraint;
1036 : : }
1037 : : }
1038 : :
1039 : 28777 : ConstraintDatabase::ConstraintDatabase(Env& env,
1040 : : const ArithVariables& avars,
1041 : : ArithCongruenceManager& cm,
1042 : : RaiseConflict raiseConflict,
1043 : 28777 : EagerProofGenerator* pfGen)
1044 : : : EnvObj(env),
1045 : 28777 : d_varDatabases(),
1046 : 28777 : d_toPropagate(context()),
1047 : 28777 : d_antecedents(context(), false),
1048 : 28777 : d_watches(new Watches(context(), userContext())),
1049 : 28777 : d_avariables(avars),
1050 : 28777 : d_congruenceManager(cm),
1051 : 28777 : d_pfGen(pfGen),
1052 [ + + ]: 28777 : d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
1053 : : : nullptr),
1054 : 28777 : d_raiseConflict(raiseConflict),
1055 : 28777 : d_one(1),
1056 : 28777 : d_negOne(-1),
1057 : 57554 : d_statistics(statisticsRegistry())
1058 : : {
1059 : 28777 : }
1060 : :
1061 : 11472829 : SortedConstraintMap& ConstraintDatabase::getVariableSCM(ArithVar v) const
1062 : : {
1063 [ - + ][ - + ]: 11472829 : Assert(variableDatabaseIsSetup(v));
[ - - ]
1064 : 11472829 : return d_varDatabases[v]->d_constraints;
1065 : : }
1066 : :
1067 : 75618 : void ConstraintDatabase::pushSplitWatch(ConstraintP c)
1068 : : {
1069 [ - + ][ - + ]: 75618 : Assert(!c->d_split);
[ - - ]
1070 : 75618 : c->d_split = true;
1071 : 75618 : d_watches->d_splitWatches.push_back(c);
1072 : 75618 : }
1073 : :
1074 : 2371132 : void ConstraintDatabase::pushCanBePropagatedWatch(ConstraintP c)
1075 : : {
1076 [ - + ][ - + ]: 2371132 : Assert(!c->d_canBePropagated);
[ - - ]
1077 : 2371132 : c->d_canBePropagated = true;
1078 : 2371132 : d_watches->d_canBePropagatedWatches.push_back(c);
1079 : 2371132 : }
1080 : :
1081 : 9051809 : void ConstraintDatabase::pushAssertionOrderWatch(ConstraintP c, TNode witness)
1082 : : {
1083 [ - + ][ - + ]: 9051809 : Assert(!c->assertedToTheTheory());
[ - - ]
1084 : 9051809 : c->d_assertionOrder = d_watches->d_assertionOrderWatches.size();
1085 : 9051809 : c->d_witness = witness;
1086 : 9051809 : d_watches->d_assertionOrderWatches.push_back(c);
1087 : 9051809 : }
1088 : :
1089 : 13257996 : void ConstraintDatabase::pushConstraintRule(const ConstraintRule& crp)
1090 : : {
1091 : 13257996 : ConstraintP c = crp.d_constraint;
1092 [ - + ][ - + ]: 13257996 : Assert(c->d_crid == ConstraintRuleIdSentinel);
[ - - ]
1093 [ - + ][ - + ]: 13257996 : Assert(!c->hasProof());
[ - - ]
1094 : 13257996 : c->d_crid = d_watches->d_constraintProofs.size();
1095 : 13257996 : d_watches->d_constraintProofs.push_back(crp);
1096 : 13257996 : }
1097 : :
1098 : 2570041 : ConstraintP ConstraintDatabase::getConstraint(ArithVar v,
1099 : : ConstraintType t,
1100 : : const DeltaRational& r)
1101 : : {
1102 : : // This must always return a constraint.
1103 : :
1104 : 2570041 : SortedConstraintMap& scm = getVariableSCM(v);
1105 : 2570041 : pair<SortedConstraintMapIterator, bool> insertAttempt;
1106 : 2570041 : insertAttempt = scm.insert(make_pair(r, ValueCollection()));
1107 : :
1108 : 2570041 : SortedConstraintMapIterator pos = insertAttempt.first;
1109 : 2570041 : ValueCollection& vc = pos->second;
1110 [ + + ]: 2570041 : if (vc.hasConstraintOfType(t))
1111 : : {
1112 : 2418545 : return vc.getConstraintOfType(t);
1113 : : }
1114 : : else
1115 : : {
1116 : 151496 : ConstraintP c = new Constraint(v, t, r, options().smt.produceProofs);
1117 : : ConstraintP negC =
1118 : 151496 : Constraint::makeNegation(v, t, r, options().smt.produceProofs);
1119 : :
1120 : 151496 : SortedConstraintMapIterator negPos;
1121 [ + + ][ - + ]: 151496 : if (t == Equality || t == Disequality)
1122 : : {
1123 : 8607 : negPos = pos;
1124 : : }
1125 : : else
1126 : : {
1127 : 142889 : pair<SortedConstraintMapIterator, bool> negInsertAttempt;
1128 : : negInsertAttempt =
1129 : 142889 : scm.insert(make_pair(negC->getValue(), ValueCollection()));
1130 [ + + ][ + - ]: 142889 : Assert(negInsertAttempt.second
[ - + ][ - + ]
[ - - ]
1131 : : || !negInsertAttempt.first->second.hasConstraintOfType(
1132 : : negC->getType()));
1133 : 142889 : negPos = negInsertAttempt.first;
1134 : : }
1135 : :
1136 : 151496 : c->initialize(this, pos, negC);
1137 : 151496 : negC->initialize(this, negPos, c);
1138 : :
1139 : 151496 : vc.add(c);
1140 : 151496 : negPos->second.add(negC);
1141 : :
1142 : 151496 : return c;
1143 : : }
1144 : : }
1145 : :
1146 : 368404 : ConstraintP ConstraintDatabase::ensureConstraint(ValueCollection& vc,
1147 : : ConstraintType t)
1148 : : {
1149 [ + + ]: 368404 : if (vc.hasConstraintOfType(t))
1150 : : {
1151 : 347939 : return vc.getConstraintOfType(t);
1152 : : }
1153 : : else
1154 : : {
1155 : 20465 : return getConstraint(vc.getVariable(), t, vc.getValue());
1156 : : }
1157 : : }
1158 : :
1159 : 0 : bool ConstraintDatabase::emptyDatabase(
1160 : : const std::vector<PerVariableDatabase>& vec)
1161 : : {
1162 : 0 : std::vector<PerVariableDatabase>::const_iterator first = vec.begin();
1163 : 0 : std::vector<PerVariableDatabase>::const_iterator last = vec.end();
1164 : 0 : return std::find_if(first, last, PerVariableDatabase::IsEmpty) == last;
1165 : : }
1166 : :
1167 : 86292 : ConstraintDatabase::~ConstraintDatabase()
1168 : : {
1169 [ + - ]: 28764 : delete d_watches;
1170 : :
1171 : 28764 : std::vector<ConstraintP> constraintList;
1172 : :
1173 [ + + ]: 380887 : while (!d_varDatabases.empty())
1174 : : {
1175 : 352123 : PerVariableDatabase* back = d_varDatabases.back();
1176 : :
1177 : 352123 : SortedConstraintMap& scm = back->d_constraints;
1178 : 352123 : SortedConstraintMapIterator i = scm.begin(), i_end = scm.end();
1179 [ + + ]: 1346815 : for (; i != i_end; ++i)
1180 : : {
1181 : 994692 : (i->second).push_into(constraintList);
1182 : : }
1183 [ + + ]: 1828287 : while (!constraintList.empty())
1184 : : {
1185 : 1476164 : ConstraintP c = constraintList.back();
1186 : 1476164 : constraintList.pop_back();
1187 [ + - ]: 1476164 : delete c;
1188 : : }
1189 [ - + ][ - + ]: 352123 : Assert(scm.empty());
1190 : 352123 : d_varDatabases.pop_back();
1191 [ + - ]: 352123 : delete back;
1192 : : }
1193 : :
1194 [ - + ][ - + ]: 28764 : Assert(d_nodetoConstraintMap.empty());
1195 : 28764 : }
1196 : :
1197 : 28777 : ConstraintDatabase::Statistics::Statistics(StatisticsRegistry& sr)
1198 : : : d_unatePropagateCalls(
1199 : 28777 : sr.registerInt("theory::arith::cd::unatePropagateCalls")),
1200 : : d_unatePropagateImplications(
1201 : 28777 : sr.registerInt("theory::arith::cd::unatePropagateImplications"))
1202 : : {
1203 : 28777 : }
1204 : :
1205 : 1236 : void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c)
1206 : : {
1207 [ - + ][ - + ]: 1236 : Assert(c->safeToGarbageCollect());
[ - - ]
1208 : 1236 : ConstraintP neg = c->getNegation();
1209 [ - + ][ - + ]: 1236 : Assert(neg->safeToGarbageCollect());
[ - - ]
1210 [ + - ]: 1236 : delete c;
1211 [ + - ]: 1236 : delete neg;
1212 : 1236 : }
1213 : :
1214 : 356187 : void ConstraintDatabase::addVariable(ArithVar v)
1215 : : {
1216 [ + + ]: 356187 : if (d_reclaimable.isMember(v))
1217 : : {
1218 : 4064 : SortedConstraintMap& scm = getVariableSCM(v);
1219 : :
1220 : 4064 : std::vector<ConstraintP> constraintList;
1221 : :
1222 [ + + ]: 4328 : for (SortedConstraintMapIterator i = scm.begin(), end = scm.end(); i != end;
1223 : 264 : ++i)
1224 : : {
1225 : 264 : (i->second).push_into(constraintList);
1226 : : }
1227 [ + + ]: 4328 : while (!constraintList.empty())
1228 : : {
1229 : 264 : ConstraintP c = constraintList.back();
1230 : 264 : constraintList.pop_back();
1231 [ - + ][ - + ]: 264 : Assert(c->safeToGarbageCollect());
[ - - ]
1232 [ + - ]: 264 : delete c;
1233 : : }
1234 [ - + ][ - + ]: 4064 : Assert(scm.empty());
[ - - ]
1235 : :
1236 : 4064 : d_reclaimable.remove(v);
1237 : 4064 : }
1238 : : else
1239 : : {
1240 [ + - ]: 704246 : Trace("arith::constraint")
1241 : 352123 : << "about to fail" << v << " " << d_varDatabases.size() << endl;
1242 [ - + ][ - + ]: 352123 : Assert(v == d_varDatabases.size());
[ - - ]
1243 : 352123 : d_varDatabases.push_back(new PerVariableDatabase(v));
1244 : : }
1245 : 356187 : }
1246 : :
1247 : 4138 : void ConstraintDatabase::removeVariable(ArithVar v)
1248 : : {
1249 [ - + ][ - + ]: 4138 : Assert(!d_reclaimable.isMember(v));
[ - - ]
1250 : 4138 : d_reclaimable.add(v);
1251 : 4138 : }
1252 : :
1253 : 2736 : bool Constraint::safeToGarbageCollect() const
1254 : : {
1255 : : // Do not call during destructor as getNegation() may be Null by this point
1256 [ - + ][ - + ]: 2736 : Assert(getNegation() != NullConstraint);
[ - - ]
1257 : 2736 : return !contextDependentDataIsSet()
1258 [ + - ][ + - ]: 2736 : && !getNegation()->contextDependentDataIsSet();
1259 : : }
1260 : :
1261 : 1494570 : bool Constraint::contextDependentDataIsSet() const
1262 : : {
1263 [ + - ][ + - ]: 1494570 : return hasProof() || isSplit() || canBePropagated() || assertedToTheTheory();
[ + - ][ - + ]
1264 : : }
1265 : :
1266 : 37809 : TrustNode Constraint::split()
1267 : : {
1268 [ + + ][ + - ]: 37809 : Assert(isEquality() || isDisequality());
[ - + ][ - + ]
[ - - ]
1269 : :
1270 : 37809 : bool isEq = isEquality();
1271 : :
1272 [ + + ]: 37809 : ConstraintP eq = isEq ? this : d_negation;
1273 [ + + ]: 37809 : ConstraintP diseq = isEq ? d_negation : this;
1274 : :
1275 : 37809 : TNode eqNode = eq->getLiteral();
1276 [ - + ][ - + ]: 37809 : Assert(eqNode.getKind() == Kind::EQUAL);
[ - - ]
1277 : 37809 : TNode lhs = eqNode[0];
1278 : 37809 : TNode rhs = eqNode[1];
1279 : :
1280 : 37809 : NodeManager* nm = d_database->nodeManager();
1281 : 75618 : Node leqNode = NodeBuilder(nm, Kind::LEQ) << lhs << rhs;
1282 : 75618 : Node ltNode = NodeBuilder(nm, Kind::LT) << lhs << rhs;
1283 : 75618 : Node gtNode = NodeBuilder(nm, Kind::GT) << lhs << rhs;
1284 : 75618 : Node geqNode = NodeBuilder(nm, Kind::GEQ) << lhs << rhs;
1285 : :
1286 : 75618 : Node lemma = NodeBuilder(nm, Kind::OR) << leqNode << geqNode;
1287 : :
1288 : 37809 : TrustNode trustedLemma;
1289 [ + + ]: 37809 : if (d_database->isProofEnabled())
1290 : : {
1291 : 15455 : TypeNode type = lhs.getType();
1292 : : // Farkas proof that this works.
1293 : 15455 : auto nLeqPf = d_database->d_pnm->mkAssume(leqNode.negate());
1294 : 15455 : auto gtPf = ensurePredTransform(d_database->d_pnm, nLeqPf, gtNode);
1295 : 15455 : auto nGeqPf = d_database->d_pnm->mkAssume(geqNode.negate());
1296 : 15455 : auto ltPf = ensurePredTransform(d_database->d_pnm, nGeqPf, ltNode);
1297 : 61820 : std::vector<Pf> args{gtPf, ltPf};
1298 : 77275 : std::vector<Node> coeffs{nm->mkConstReal(-1), nm->mkConstReal(1)};
1299 : 15455 : std::vector<Node> coeffsUse = getMacroSumUbCoeff(nm, args, coeffs);
1300 : 15455 : auto sumPf = d_database->d_pnm->mkNode(
1301 : 15455 : ProofRule::MACRO_ARITH_SCALE_SUM_UB, args, coeffsUse);
1302 : : auto botPf =
1303 : 15455 : ensurePredTransform(d_database->d_pnm, sumPf, nm->mkConst(false));
1304 : 61820 : std::vector<Node> a = {leqNode.negate(), geqNode.negate()};
1305 : 30910 : auto notAndNotPf = d_database->d_pnm->mkScope(botPf, a);
1306 : : // No need to ensure that the expected node aggrees with `a` because we are
1307 : : // not providing an expected node.
1308 : : auto orNotNotPf =
1309 : 61820 : d_database->d_pnm->mkNode(ProofRule::NOT_AND, {notAndNotPf}, {});
1310 : 15455 : auto orPf = ensurePredTransform(d_database->d_pnm, orNotNotPf, lemma);
1311 : 15455 : trustedLemma = d_database->d_pfGen->mkTrustNode(lemma, orPf);
1312 : 15455 : }
1313 : : else
1314 : : {
1315 : 22354 : trustedLemma = TrustNode::mkTrustLemma(lemma);
1316 : : }
1317 : :
1318 : 37809 : eq->d_database->pushSplitWatch(eq);
1319 : 37809 : diseq->d_database->pushSplitWatch(diseq);
1320 : :
1321 : 75618 : return trustedLemma;
1322 : 37809 : }
1323 : :
1324 : 2392608 : bool ConstraintDatabase::hasLiteral(TNode literal) const
1325 : : {
1326 : 2392608 : return lookup(literal) != NullConstraint;
1327 : : }
1328 : :
1329 : 598152 : ConstraintP ConstraintDatabase::addLiteral(TNode literal, TNode nliteral)
1330 : : {
1331 [ - + ][ - + ]: 598152 : Assert(!hasLiteral(literal));
[ - - ]
1332 : 598152 : bool isNot = (literal.getKind() == Kind::NOT);
1333 [ - + ]: 598152 : Node atomNode = (isNot ? literal[0] : literal);
1334 : 598152 : Node negationNode = atomNode.notNode();
1335 : : // The normal form of the atom, which determines the constraint this literal
1336 : : // maps to. Note this may be distinct from atomNode.
1337 [ - + ]: 598152 : Node nAtomNode = (nliteral.getKind() == Kind::NOT ? nliteral[0] : nliteral);
1338 [ - + ][ - + ]: 598152 : Assert((nliteral.getKind() == Kind::NOT) == isNot);
[ - - ]
1339 : :
1340 [ - + ][ - + ]: 598152 : Assert(!hasLiteral(atomNode));
[ - - ]
1341 [ - + ][ - + ]: 598152 : Assert(!hasLiteral(negationNode));
[ - - ]
1342 : 598152 : Comparison posCmp = Comparison::parseNormalForm(nAtomNode);
1343 : :
1344 : 598152 : ConstraintType posType = Constraint::constraintTypeOfComparison(posCmp);
1345 : :
1346 : 598152 : Polynomial nvp = posCmp.normalizedVariablePart();
1347 : 598152 : ArithVar v = d_avariables.asArithVar(nvp.getNode());
1348 : :
1349 : 598152 : DeltaRational posDR = posCmp.normalizedDeltaRational();
1350 : :
1351 : : ConstraintP posC =
1352 : 598152 : new Constraint(v, posType, posDR, options().smt.produceProofs);
1353 : :
1354 [ + - ]: 1196304 : Trace("arith::constraint")
1355 : 598152 : << "addliteral( literal ->" << literal << ")" << endl;
1356 [ + - ]: 598152 : Trace("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl;
1357 : :
1358 : 598152 : SortedConstraintMap& scm = getVariableSCM(posC->getVariable());
1359 : 598152 : pair<SortedConstraintMapIterator, bool> insertAttempt;
1360 : 598152 : insertAttempt = scm.insert(make_pair(posC->getValue(), ValueCollection()));
1361 : :
1362 : 598152 : SortedConstraintMapIterator posI = insertAttempt.first;
1363 : : // If the attempt succeeds, i points to a new empty ValueCollection
1364 : : // If the attempt fails, i points to a pre-existing ValueCollection
1365 : :
1366 [ + + ]: 598152 : if (posI->second.hasConstraintOfType(posC->getType()))
1367 : : {
1368 : : // This is the situation where the ConstraintP exists, but
1369 : : // the literal has not been associated with it.
1370 : 10198 : ConstraintP hit = posI->second.getConstraintOfType(posC->getType());
1371 [ + - ]: 10198 : Trace("arith::constraint") << "hit " << hit << endl;
1372 [ + - ]: 10198 : Trace("arith::constraint") << "posC " << posC << endl;
1373 : :
1374 [ + - ]: 10198 : delete posC;
1375 : :
1376 : 10198 : hit->setLiteral(atomNode, nAtomNode);
1377 : 10198 : hit->getNegation()->setLiteral(negationNode, nAtomNode.notNode());
1378 [ - + ]: 10198 : return isNot ? hit->getNegation() : hit;
1379 : : }
1380 : : else
1381 : : {
1382 : 1175908 : Comparison negCmp = Comparison::parseNormalForm(nAtomNode.notNode());
1383 : :
1384 : 587954 : ConstraintType negType = Constraint::constraintTypeOfComparison(negCmp);
1385 : 587954 : DeltaRational negDR = negCmp.normalizedDeltaRational();
1386 : :
1387 : : ConstraintP negC =
1388 : 587954 : new Constraint(v, negType, negDR, options().smt.produceProofs);
1389 : :
1390 : 587954 : SortedConstraintMapIterator negI;
1391 : :
1392 [ + + ]: 587954 : if (posC->isEquality())
1393 : : {
1394 : 274014 : negI = posI;
1395 : : }
1396 : : else
1397 : : {
1398 [ + + ][ + - ]: 313940 : Assert(posC->isLowerBound() || posC->isUpperBound());
[ - + ][ - + ]
[ - - ]
1399 : :
1400 : 313940 : pair<SortedConstraintMapIterator, bool> negInsertAttempt;
1401 : : negInsertAttempt =
1402 : 313940 : scm.insert(make_pair(negC->getValue(), ValueCollection()));
1403 : :
1404 [ + - ]: 313940 : Trace("nf::tmp") << "sdhjfgdhjkldfgljkhdfg" << endl;
1405 [ + - ]: 313940 : Trace("nf::tmp") << negC << endl;
1406 [ + - ]: 313940 : Trace("nf::tmp") << negC->getValue() << endl;
1407 : :
1408 : : // This should always succeed as the DeltaRational for the negation is
1409 : : // unique!
1410 [ - + ][ - + ]: 313940 : Assert(negInsertAttempt.second);
[ - - ]
1411 : :
1412 : 313940 : negI = negInsertAttempt.first;
1413 : : }
1414 : :
1415 : 587954 : (posI->second).add(posC);
1416 : 587954 : (negI->second).add(negC);
1417 : :
1418 : 587954 : posC->initialize(this, posI, negC);
1419 : 587954 : negC->initialize(this, negI, posC);
1420 : :
1421 : 587954 : posC->setLiteral(atomNode, nAtomNode);
1422 : 587954 : negC->setLiteral(negationNode, nAtomNode.notNode());
1423 : :
1424 [ - + ]: 587954 : return isNot ? negC : posC;
1425 : 587954 : }
1426 : 598152 : }
1427 : :
1428 : 16904187 : ConstraintP ConstraintDatabase::lookup(TNode literal) const
1429 : : {
1430 : : NodetoConstraintMap::const_iterator iter =
1431 : 16904187 : d_nodetoConstraintMap.find(literal);
1432 [ + + ]: 16904187 : if (iter == d_nodetoConstraintMap.end())
1433 : : {
1434 : 3622537 : return NullConstraint;
1435 : : }
1436 : : else
1437 : : {
1438 : 13281650 : return iter->second;
1439 : : }
1440 : : }
1441 : :
1442 : 7972639 : void Constraint::setAssumption(CVC5_UNUSED bool nowInConflict)
1443 : : {
1444 [ + - ]: 7972639 : Trace("constraints::pf") << "setAssumption(" << this << ")" << std::endl;
1445 [ - + ][ - + ]: 7972639 : Assert(!hasProof());
[ - - ]
1446 [ - + ][ - + ]: 7972639 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1447 [ - + ][ - + ]: 7972639 : Assert(hasLiteral());
[ - - ]
1448 [ - + ][ - + ]: 7972639 : Assert(assertedToTheTheory());
[ - - ]
1449 : :
1450 : 7972639 : d_database->pushConstraintRule(ConstraintRule(this, AssumeAP));
1451 : :
1452 [ - + ][ - + ]: 7972639 : Assert(inConflict() == nowInConflict);
[ - - ]
1453 : 7972639 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1454 : : {
1455 [ - - ]: 0 : Trace("constraint::conflictCommit")
1456 : 0 : << "inConflict@setAssumption " << this << std::endl;
1457 : : }
1458 : 7972639 : }
1459 : :
1460 : 4806210 : void Constraint::tryToPropagate()
1461 : : {
1462 [ - + ][ - + ]: 4806210 : Assert(hasProof());
[ - - ]
1463 [ - + ][ - + ]: 4806210 : Assert(!isAssumption());
[ - - ]
1464 [ - + ][ - + ]: 4806210 : Assert(!isInternalAssumption());
[ - - ]
1465 : :
1466 [ + - ][ + - ]: 5686877 : if (canBePropagated() && !assertedToTheTheory() && !isAssumption()
1467 [ + + ][ + - ]: 5686877 : && !isInternalAssumption())
[ + + ]
1468 : : {
1469 : 880667 : propagate();
1470 : : }
1471 : 4806210 : }
1472 : :
1473 : 905643 : void Constraint::propagate()
1474 : : {
1475 [ - + ][ - + ]: 905643 : Assert(hasProof());
[ - - ]
1476 [ - + ][ - + ]: 905643 : Assert(canBePropagated());
[ - - ]
1477 [ - + ][ - + ]: 905643 : Assert(!assertedToTheTheory());
[ - - ]
1478 [ - + ][ - + ]: 905643 : Assert(!isAssumption());
[ - - ]
1479 [ - + ][ - + ]: 905643 : Assert(!isInternalAssumption());
[ - - ]
1480 : :
1481 : 905643 : d_database->d_toPropagate.push(this);
1482 : 905643 : }
1483 : :
1484 : : /*
1485 : : * Example:
1486 : : * x <= a and a < b
1487 : : * |= x <= b
1488 : : * ---
1489 : : * 1*(x <= a) + (-1)*(x > b) => (0 <= a-b)
1490 : : */
1491 : 2183582 : void Constraint::impliedByUnate(NodeManager* nm,
1492 : : ConstraintCP imp,
1493 : : CVC5_UNUSED bool nowInConflict)
1494 : : {
1495 [ + - ]: 4367164 : Trace("constraints::pf") << "impliedByUnate(" << this << ", " << *imp << ")"
1496 : 2183582 : << std::endl;
1497 [ - + ][ - + ]: 2183582 : Assert(!hasProof());
[ - - ]
1498 [ - + ][ - + ]: 2183582 : Assert(imp->hasProof());
[ - - ]
1499 [ - + ][ - + ]: 2183582 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1500 : :
1501 : 2183582 : d_database->d_antecedents.push_back(NullConstraint);
1502 : 2183582 : d_database->d_antecedents.push_back(imp);
1503 : :
1504 : 2183582 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1505 : :
1506 : : RationalVectorP coeffs;
1507 [ + + ]: 2183582 : if (d_produceProofs)
1508 : : {
1509 : 1300433 : std::pair<int, int> sgns = unateFarkasSigns(getNegation(), imp);
1510 : :
1511 : 1300433 : Rational first(sgns.first);
1512 : 1300433 : Rational second(sgns.second);
1513 : :
1514 : 1300433 : coeffs = new RationalVector();
1515 : 1300433 : coeffs->push_back(first);
1516 : 1300433 : coeffs->push_back(second);
1517 : 1300433 : }
1518 : : else
1519 : : {
1520 : 883149 : coeffs = RationalVectorPSentinel;
1521 : : }
1522 : : // no need to delete coeffs the memory is owned by ConstraintRule
1523 : 2183582 : d_database->pushConstraintRule(
1524 : 2183582 : ConstraintRule(this, FarkasAP, antecedentEnd, coeffs));
1525 : :
1526 [ - + ][ - + ]: 2183582 : Assert(inConflict() == nowInConflict);
[ - - ]
1527 : 2183582 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1528 : : {
1529 [ - - ]: 0 : Trace("constraint::conflictCommit")
1530 : 0 : << "inConflict@impliedByUnate " << this << std::endl;
1531 : : }
1532 : :
1533 : 2183582 : if (TraceIsOn("constraints::wffp") && !wellFormedFarkasProof(nm))
1534 : : {
1535 [ - - ]: 0 : getConstraintRule().print(Trace("constraints::wffp"), d_produceProofs);
1536 : : }
1537 [ - + ][ - + ]: 2183582 : Assert(wellFormedFarkasProof(nm));
[ - - ]
1538 : 2183582 : }
1539 : :
1540 : 822023 : void Constraint::impliedByTrichotomy(ConstraintCP a,
1541 : : ConstraintCP b,
1542 : : CVC5_UNUSED bool nowInConflict)
1543 : : {
1544 [ + - ]: 1644046 : Trace("constraints::pf") << "impliedByTrichotomy(" << this << ", " << *a
1545 : 822023 : << ", ";
1546 [ + - ]: 822023 : Trace("constraints::pf") << *b << ")" << std::endl;
1547 [ - + ][ - + ]: 822023 : Assert(!hasProof());
[ - - ]
1548 [ - + ][ - + ]: 822023 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1549 [ - + ][ - + ]: 822023 : Assert(a->hasProof());
[ - - ]
1550 [ - + ][ - + ]: 822023 : Assert(b->hasProof());
[ - - ]
1551 : :
1552 : 822023 : d_database->d_antecedents.push_back(NullConstraint);
1553 : 822023 : d_database->d_antecedents.push_back(a);
1554 : 822023 : d_database->d_antecedents.push_back(b);
1555 : :
1556 : 822023 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1557 : 822023 : d_database->pushConstraintRule(
1558 : 822023 : ConstraintRule(this, TrichotomyAP, antecedentEnd));
1559 : :
1560 [ - + ][ - + ]: 822023 : Assert(inConflict() == nowInConflict);
[ - - ]
1561 : 822023 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1562 : : {
1563 [ - - ]: 0 : Trace("constraint::conflictCommit")
1564 : 0 : << "inConflict@impliedByTrichotomy " << this << std::endl;
1565 : : }
1566 : 822023 : }
1567 : :
1568 : 163442 : bool Constraint::allHaveProof(const ConstraintCPVec& b)
1569 : : {
1570 : 163442 : for (ConstraintCPVec::const_iterator i = b.begin(), i_end = b.end();
1571 [ + + ]: 1978621 : i != i_end;
1572 : 1815179 : ++i)
1573 : : {
1574 : 1815179 : ConstraintCP cp = *i;
1575 [ - + ]: 1815179 : if (!(cp->hasProof()))
1576 : : {
1577 : 0 : return false;
1578 : : }
1579 : : }
1580 : 163442 : return true;
1581 : : }
1582 : :
1583 : 1757150 : void Constraint::impliedByIntTighten(ConstraintCP a,
1584 : : CVC5_UNUSED bool nowInConflict)
1585 : : {
1586 [ + - ]: 3514300 : Trace("constraints::pf") << "impliedByIntTighten(" << this << ", " << *a
1587 : 1757150 : << ")" << std::endl;
1588 [ - + ][ - + ]: 1757150 : Assert(!hasProof());
[ - - ]
1589 [ - + ][ - + ]: 1757150 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1590 [ - + ][ - + ]: 1757150 : Assert(a->hasProof());
[ - - ]
1591 [ + - ]: 3514300 : Trace("pf::arith") << "impliedByIntTighten(" << this << ", " << a << ")"
1592 : 1757150 : << std::endl;
1593 : :
1594 : 1757150 : d_database->d_antecedents.push_back(NullConstraint);
1595 : 1757150 : d_database->d_antecedents.push_back(a);
1596 : 1757150 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1597 : 1757150 : d_database->pushConstraintRule(
1598 : 1757150 : ConstraintRule(this, IntTightenAP, antecedentEnd));
1599 : :
1600 [ - + ][ - + ]: 1757150 : Assert(inConflict() == nowInConflict);
[ - - ]
1601 [ + + ]: 1757150 : if (inConflict())
1602 : : {
1603 [ + - ]: 3284 : Trace("constraint::conflictCommit")
1604 : 1642 : << "inConflict impliedByIntTighten" << this << std::endl;
1605 : : }
1606 : 1757150 : }
1607 : :
1608 : 0 : void Constraint::impliedByIntHole(ConstraintCP a,
1609 : : CVC5_UNUSED bool nowInConflict)
1610 : : {
1611 [ - - ]: 0 : Trace("constraints::pf") << "impliedByIntHole(" << this << ", " << *a << ")"
1612 : 0 : << std::endl;
1613 : 0 : Assert(!hasProof());
1614 : 0 : Assert(negationHasProof() == nowInConflict);
1615 : 0 : Assert(a->hasProof());
1616 [ - - ]: 0 : Trace("pf::arith") << "impliedByIntHole(" << this << ", " << a << ")"
1617 : 0 : << std::endl;
1618 : :
1619 : 0 : d_database->d_antecedents.push_back(NullConstraint);
1620 : 0 : d_database->d_antecedents.push_back(a);
1621 : 0 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1622 : 0 : d_database->pushConstraintRule(
1623 : 0 : ConstraintRule(this, IntHoleAP, antecedentEnd));
1624 : :
1625 : 0 : Assert(inConflict() == nowInConflict);
1626 : 0 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1627 : : {
1628 [ - - ]: 0 : Trace("constraint::conflictCommit")
1629 : 0 : << "inConflict impliedByIntHole" << this << std::endl;
1630 : : }
1631 : 0 : }
1632 : :
1633 : 852 : void Constraint::impliedByIntHole(const ConstraintCPVec& b,
1634 : : CVC5_UNUSED bool nowInConflict)
1635 : : {
1636 [ + - ]: 852 : Trace("constraints::pf") << "impliedByIntHole(" << this;
1637 [ - + ]: 852 : if (TraceIsOn("constraints::pf"))
1638 : : {
1639 [ - - ]: 0 : for (const ConstraintCP& p : b)
1640 : : {
1641 [ - - ]: 0 : Trace("constraints::pf") << ", " << p;
1642 : : }
1643 : : }
1644 [ + - ]: 852 : Trace("constraints::pf") << ")" << std::endl;
1645 : :
1646 [ - + ][ - + ]: 852 : Assert(!hasProof());
[ - - ]
1647 [ - + ][ - + ]: 852 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1648 [ - + ][ - + ]: 852 : Assert(allHaveProof(b));
[ - - ]
1649 : :
1650 : 852 : CDConstraintList& antecedents = d_database->d_antecedents;
1651 : 852 : antecedents.push_back(NullConstraint);
1652 : 852 : for (ConstraintCPVec::const_iterator i = b.begin(), i_end = b.end();
1653 [ + + ]: 7956 : i != i_end;
1654 : 7104 : ++i)
1655 : : {
1656 : 7104 : antecedents.push_back(*i);
1657 : : }
1658 : 852 : AntecedentId antecedentEnd = antecedents.size() - 1;
1659 : :
1660 : 852 : d_database->pushConstraintRule(
1661 : 852 : ConstraintRule(this, IntHoleAP, antecedentEnd));
1662 : :
1663 [ - + ][ - + ]: 852 : Assert(inConflict() == nowInConflict);
[ - - ]
1664 : 852 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1665 : : {
1666 [ - - ]: 0 : Trace("constraint::conflictCommit")
1667 : 0 : << "inConflict@impliedByIntHole[vec] " << this << std::endl;
1668 : : }
1669 : 852 : }
1670 : :
1671 : : /*
1672 : : * If proofs are off, coeffs == RationalVectorSentinal.
1673 : : * If proofs are on,
1674 : : * coeffs != RationalVectorSentinal,
1675 : : * coeffs->size() = a.size() + 1,
1676 : : * for i in [0,a.size) : coeff[i] corresponds to a[i], and
1677 : : * coeff.back() corresponds to the current constraint.
1678 : : */
1679 : 162590 : void Constraint::impliedByFarkas(NodeManager* nm,
1680 : : const ConstraintCPVec& a,
1681 : : RationalVectorCP coeffs,
1682 : : CVC5_UNUSED bool nowInConflict)
1683 : : {
1684 [ + - ]: 162590 : Trace("constraints::pf") << "impliedByFarkas(" << this;
1685 [ - + ]: 162590 : if (TraceIsOn("constraints::pf"))
1686 : : {
1687 [ - - ]: 0 : for (const ConstraintCP& p : a)
1688 : : {
1689 [ - - ]: 0 : Trace("constraints::pf") << ", " << p;
1690 : : }
1691 : : }
1692 [ + - ]: 162590 : Trace("constraints::pf") << ", <coeffs>";
1693 [ + - ]: 162590 : Trace("constraints::pf") << ")" << std::endl;
1694 [ - + ][ - + ]: 162590 : Assert(!hasProof());
[ - - ]
1695 [ - + ][ - + ]: 162590 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1696 [ - + ][ - + ]: 162590 : Assert(allHaveProof(a));
[ - - ]
1697 : :
1698 [ - + ][ - + ]: 162590 : Assert(d_produceProofs == (coeffs != RationalVectorCPSentinel));
[ - - ]
1699 [ + + ][ + - ]: 162590 : Assert(!d_produceProofs || coeffs->size() == a.size() + 1);
[ - + ][ - + ]
[ - - ]
1700 : :
1701 [ - + ][ - + ]: 162590 : Assert(a.size() >= 1);
[ - - ]
1702 : :
1703 : 162590 : d_database->d_antecedents.push_back(NullConstraint);
1704 [ + + ]: 1970665 : for (ConstraintCPVec::const_iterator i = a.begin(), end = a.end(); i != end;
1705 : 1808075 : ++i)
1706 : : {
1707 : 1808075 : ConstraintCP c_i = *i;
1708 [ - + ][ - + ]: 1808075 : Assert(c_i->hasProof());
[ - - ]
1709 : 1808075 : d_database->d_antecedents.push_back(c_i);
1710 : : }
1711 : 162590 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1712 : :
1713 : : RationalVectorCP coeffsCopy;
1714 [ + + ]: 162590 : if (d_produceProofs)
1715 : : {
1716 [ - + ][ - + ]: 105982 : Assert(coeffs != RationalVectorCPSentinel);
[ - - ]
1717 : 105982 : coeffsCopy = new RationalVector(*coeffs);
1718 : : }
1719 : : else
1720 : : {
1721 : 56608 : coeffsCopy = RationalVectorCPSentinel;
1722 : : }
1723 : 162590 : d_database->pushConstraintRule(
1724 : 162590 : ConstraintRule(this, FarkasAP, antecedentEnd, coeffsCopy));
1725 : :
1726 [ - + ][ - + ]: 162590 : Assert(inConflict() == nowInConflict);
[ - - ]
1727 : 162590 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1728 : : {
1729 [ - - ]: 0 : Trace("constraint::conflictCommit")
1730 : 0 : << "inConflict@impliedByFarkas " << this << std::endl;
1731 : : }
1732 : 162590 : if (TraceIsOn("constraints::wffp") && !wellFormedFarkasProof(nm))
1733 : : {
1734 [ - - ]: 0 : getConstraintRule().print(Trace("constraints::wffp"), d_produceProofs);
1735 : : }
1736 [ - + ][ - + ]: 162590 : Assert(wellFormedFarkasProof(nm));
[ - - ]
1737 : 162590 : }
1738 : :
1739 : 1268 : void Constraint::setInternalAssumption(CVC5_UNUSED bool nowInConflict)
1740 : : {
1741 [ + - ]: 1268 : Trace("constraints::pf") << "setInternalAssumption(" << this;
1742 [ + - ]: 1268 : Trace("constraints::pf") << ")" << std::endl;
1743 [ - + ][ - + ]: 1268 : Assert(!hasProof());
[ - - ]
1744 [ - + ][ - + ]: 1268 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1745 [ - + ][ - + ]: 1268 : Assert(!assertedToTheTheory());
[ - - ]
1746 : :
1747 : 1268 : d_database->pushConstraintRule(ConstraintRule(this, InternalAssumeAP));
1748 : :
1749 [ - + ][ - + ]: 1268 : Assert(inConflict() == nowInConflict);
[ - - ]
1750 : 1268 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1751 : : {
1752 [ - - ]: 0 : Trace("constraint::conflictCommit")
1753 : 0 : << "inConflict@setInternalAssumption " << this << std::endl;
1754 : : }
1755 : 1268 : }
1756 : :
1757 : 357892 : void Constraint::setEqualityEngineProof()
1758 : : {
1759 [ + - ]: 357892 : Trace("constraints::pf") << "setEqualityEngineProof(" << this;
1760 [ + - ]: 357892 : Trace("constraints::pf") << ")" << std::endl;
1761 [ - + ][ - + ]: 357892 : Assert(truthIsUnknown());
[ - - ]
1762 [ - + ][ - + ]: 357892 : Assert(hasLiteral());
[ - - ]
1763 : 357892 : d_database->pushConstraintRule(ConstraintRule(this, EqualityEngineAP));
1764 : 357892 : }
1765 : :
1766 : 6480349 : SortedConstraintMap& Constraint::constraintSet() const
1767 : : {
1768 [ - + ][ - + ]: 6480349 : Assert(d_database->variableDatabaseIsSetup(d_variable));
[ - - ]
1769 : 6480349 : return (d_database->d_varDatabases[d_variable])->d_constraints;
1770 : : }
1771 : :
1772 : 0 : bool Constraint::antecentListIsEmpty() const
1773 : : {
1774 : 0 : Assert(hasProof());
1775 : 0 : return d_database->d_antecedents[getEndAntecedent()] == NullConstraint;
1776 : : }
1777 : :
1778 : 0 : bool Constraint::antecedentListLengthIsOne() const
1779 : : {
1780 : 0 : Assert(hasProof());
1781 : 0 : return !antecentListIsEmpty()
1782 [ - - ][ - - ]: 0 : && d_database->d_antecedents[getEndAntecedent() - 1] == NullConstraint;
1783 : : }
1784 : :
1785 : 151336 : Node Constraint::externalImplication(NodeManager* nm,
1786 : : const ConstraintCPVec& b) const
1787 : : {
1788 [ - + ][ - + ]: 151336 : Assert(hasLiteral());
[ - - ]
1789 : 151336 : Node antecedent = externalExplainByAssertions(nm, b);
1790 : 151336 : Node implied = getLiteral();
1791 : 302672 : return antecedent.impNode(implied);
1792 : 151336 : }
1793 : :
1794 : 174187 : Node Constraint::externalExplainByAssertions(NodeManager* nm,
1795 : : const ConstraintCPVec& b)
1796 : : {
1797 : 174187 : return externalExplain(nm, b, AssertionOrderSentinel);
1798 : : }
1799 : :
1800 : 37725 : TrustNode Constraint::externalExplainForPropagation(TNode lit) const
1801 : : {
1802 [ - + ][ - + ]: 37725 : Assert(hasProof());
[ - - ]
1803 [ - + ][ - + ]: 37725 : Assert(!isAssumption());
[ - - ]
1804 [ - + ][ - + ]: 37725 : Assert(!isInternalAssumption());
[ - - ]
1805 : 37725 : NodeBuilder nb(d_database->nodeManager(), Kind::AND);
1806 : 37725 : auto pfFromAssumptions = externalExplain(nb, d_assertionOrder);
1807 : 37725 : Node n = mkAndFromBuilder(d_database->nodeManager(), nb);
1808 [ + + ]: 37725 : if (d_database->isProofEnabled())
1809 : : {
1810 : 17430 : std::vector<Node> assumptions;
1811 [ + + ]: 17430 : if (n.getKind() == Kind::AND)
1812 : : {
1813 : 5882 : assumptions.insert(assumptions.end(), n.begin(), n.end());
1814 : : }
1815 : : else
1816 : : {
1817 : 11548 : assumptions.push_back(n);
1818 : : }
1819 [ + + ]: 17430 : if (getProofLiteral() != lit)
1820 : : {
1821 : : pfFromAssumptions =
1822 : 10509 : ensurePredTransform(d_database->d_pnm, pfFromAssumptions, lit);
1823 : : }
1824 : 34860 : auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
1825 : 17430 : return d_database->d_pfGen->mkTrustedPropagation(
1826 : 17430 : lit, d_database->nodeManager()->mkAnd(assumptions), pf);
1827 : 17430 : }
1828 : : else
1829 : : {
1830 : 20295 : return TrustNode::mkTrustPropExp(lit, n);
1831 : : }
1832 : 37725 : }
1833 : :
1834 : 121507 : TrustNode Constraint::externalExplainConflict() const
1835 : : {
1836 [ + - ]: 121507 : Trace("pf::arith::explain") << this << std::endl;
1837 [ - + ][ - + ]: 121507 : Assert(inConflict());
[ - - ]
1838 : 121507 : NodeBuilder nb(d_database->nodeManager(), Kind::AND);
1839 : 121507 : auto pf1 = externalExplainByAssertions(nb);
1840 : 121507 : auto not2 = getNegation()->getProofLiteral().negate();
1841 : 121507 : auto pf2 = getNegation()->externalExplainByAssertions(nb);
1842 : 121507 : Node n = mkAndFromBuilder(d_database->nodeManager(), nb);
1843 [ + + ]: 121507 : if (d_database->isProofEnabled())
1844 : : {
1845 : 48786 : auto pfNot2 = ensurePredTransform(d_database->d_pnm, pf1, not2);
1846 : 48786 : std::vector<Node> lits;
1847 [ + - ]: 48786 : if (n.getKind() == Kind::AND)
1848 : : {
1849 : 48786 : lits.insert(lits.end(), n.begin(), n.end());
1850 : : }
1851 : : else
1852 : : {
1853 : 0 : lits.push_back(n);
1854 : : }
1855 [ - + ]: 48786 : if (TraceIsOn("arith::pf::externalExplainConflict"))
1856 : : {
1857 [ - - ]: 0 : Trace("arith::pf::externalExplainConflict") << "Lits:" << std::endl;
1858 [ - - ]: 0 : for (const auto& l : lits)
1859 : : {
1860 [ - - ]: 0 : Trace("arith::pf::externalExplainConflict") << " : " << l << std::endl;
1861 : : }
1862 : : }
1863 : : std::vector<Node> contraLits = {getProofLiteral(),
1864 : 195144 : getNegation()->getProofLiteral()};
1865 : : auto bot =
1866 : 48786 : not2.getKind() == Kind::NOT
1867 : 139422 : ? d_database->d_pnm->mkNode(ProofRule::CONTRA, {pf2, pfNot2}, {})
1868 : 250866 : : d_database->d_pnm->mkNode(ProofRule::CONTRA, {pfNot2, pf2}, {});
1869 [ - + ]: 48786 : if (TraceIsOn("arith::pf::tree"))
1870 : : {
1871 [ - - ]: 0 : Trace("arith::pf::tree") << *this << std::endl;
1872 [ - - ]: 0 : Trace("arith::pf::tree") << *getNegation() << std::endl;
1873 [ - - ]: 0 : Trace("arith::pf::tree") << "\n\nTree:\n";
1874 [ - - ]: 0 : printProofTree(Trace("arith::pf::tree"));
1875 [ - - ]: 0 : getNegation()->printProofTree(Trace("arith::pf::tree"));
1876 : : }
1877 : 97572 : auto confPf = d_database->d_pnm->mkScope(bot, lits);
1878 : 48786 : return d_database->d_pfGen->mkTrustNode(
1879 : 97572 : d_database->nodeManager()->mkAnd(lits), confPf, true);
1880 : 48786 : }
1881 : : else
1882 : : {
1883 : 72721 : return TrustNode::mkTrustConflict(n);
1884 : : }
1885 : 121507 : }
1886 : :
1887 : : struct ConstraintCPHash
1888 : : {
1889 : : /* Todo replace with an id */
1890 : 90572 : size_t operator()(ConstraintCP c) const
1891 : : {
1892 : : Assert(sizeof(ConstraintCP) > 0);
1893 : 90572 : return ((size_t)c) / sizeof(ConstraintCP);
1894 : : }
1895 : : };
1896 : :
1897 : 3040 : void Constraint::assertionFringe(ConstraintCPVec& v)
1898 : : {
1899 : 3040 : unordered_set<ConstraintCP, ConstraintCPHash> visited;
1900 : 3040 : size_t writePos = 0;
1901 : :
1902 [ + - ]: 3040 : if (!v.empty())
1903 : : {
1904 : 3040 : const ConstraintDatabase* db = v.back()->d_database;
1905 : 3040 : const CDConstraintList& antecedents = db->d_antecedents;
1906 [ + + ]: 52732 : for (size_t i = 0; i < v.size(); ++i)
1907 : : {
1908 : 49692 : ConstraintCP vi = v[i];
1909 [ + + ]: 49692 : if (visited.find(vi) == visited.end())
1910 : : {
1911 [ - + ][ - + ]: 40880 : Assert(vi->hasProof());
[ - - ]
1912 : 40880 : visited.insert(vi);
1913 [ + + ]: 40880 : if (vi->onFringe())
1914 : : {
1915 : 33148 : v[writePos] = vi;
1916 : 33148 : writePos++;
1917 : : }
1918 : : else
1919 : : {
1920 [ + - ][ + + ]: 7732 : Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof()
[ + + ][ + + ]
[ + + ][ + - ]
[ - + ][ - + ]
[ - - ]
1921 : : || vi->hasIntHoleProof() || vi->hasIntTightenProof());
1922 : 7732 : AntecedentId p = vi->getEndAntecedent();
1923 : :
1924 : 7732 : ConstraintCP antecedent = antecedents[p];
1925 [ + + ]: 32304 : while (antecedent != NullConstraint)
1926 : : {
1927 : 24572 : v.push_back(antecedent);
1928 : 24572 : --p;
1929 : 24572 : antecedent = antecedents[p];
1930 : : }
1931 : : }
1932 : : }
1933 : : }
1934 : 3040 : v.resize(writePos);
1935 : : }
1936 : 3040 : }
1937 : :
1938 : 0 : void Constraint::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i)
1939 : : {
1940 : 0 : o.insert(o.end(), i.begin(), i.end());
1941 : 0 : assertionFringe(o);
1942 : 0 : }
1943 : :
1944 : 174187 : Node Constraint::externalExplain(NodeManager* nm,
1945 : : const ConstraintCPVec& v,
1946 : : AssertionOrder order)
1947 : : {
1948 : 174187 : NodeBuilder nb(nm, Kind::AND);
1949 : 174187 : ConstraintCPVec::const_iterator i, end;
1950 [ + + ]: 736422 : for (i = v.begin(), end = v.end(); i != end; ++i)
1951 : : {
1952 : 562235 : ConstraintCP v_i = *i;
1953 : 562235 : v_i->externalExplain(nb, order);
1954 : : }
1955 : 348374 : return mkAndFromBuilder(nm, nb);
1956 : 174187 : }
1957 : :
1958 : 7834644 : std::shared_ptr<ProofNode> Constraint::externalExplain(
1959 : : NodeBuilder& nb, AssertionOrder order) const
1960 : : {
1961 [ - + ]: 7834644 : if (TraceIsOn("pf::arith::explain"))
1962 : : {
1963 [ - - ]: 0 : this->printProofTree(Trace("arith::pf::tree"));
1964 [ - - ]: 0 : Trace("pf::arith::explain") << "Explaining: " << this << " with rule ";
1965 [ - - ]: 0 : getConstraintRule().print(Trace("pf::arith::explain"), d_produceProofs);
1966 [ - - ]: 0 : Trace("pf::arith::explain") << std::endl;
1967 : : }
1968 [ - + ][ - + ]: 7834644 : Assert(hasProof());
[ - - ]
1969 [ + + ][ + - ]: 7834644 : Assert(!isAssumption() || assertedToTheTheory());
[ - + ][ - + ]
[ - - ]
1970 [ - + ][ - + ]: 7834644 : Assert(!isInternalAssumption());
[ - - ]
1971 : 7834644 : std::shared_ptr<ProofNode> pf{};
1972 : :
1973 : 7834644 : ProofNodeManager* pnm = d_database->d_pnm;
1974 : :
1975 [ + + ]: 7834644 : if (assertedBefore(order))
1976 : : {
1977 [ + - ]: 6822939 : Trace("pf::arith::explain") << " already asserted" << std::endl;
1978 : 6822939 : nb << getWitness();
1979 [ + + ]: 6822939 : if (d_database->isProofEnabled())
1980 : : {
1981 : 2942651 : pf = pnm->mkAssume(getWitness());
1982 : : // If the witness and literal differ, prove the difference through a
1983 : : // rewrite.
1984 : 2942651 : pf = ensurePredTransform(pnm, pf, getProofLiteral());
1985 : : }
1986 : : }
1987 [ + + ]: 1011705 : else if (hasEqualityEngineProof())
1988 : : {
1989 : : // just assume, it will be explained again
1990 : 353 : Node lit = getLiteral();
1991 [ + + ]: 353 : if (d_database->isProofEnabled())
1992 : : {
1993 : 156 : std::shared_ptr<ProofNode> a = pnm->mkAssume(getLiteral());
1994 : 156 : Node plit = getProofLiteral();
1995 : 156 : pf = ensurePredTransform(pnm, a, plit);
1996 : 156 : }
1997 [ - + ][ - + ]: 353 : Assert(lit.getKind() != Kind::AND);
[ - - ]
1998 : 353 : nb << lit;
1999 : 353 : }
2000 : : else
2001 : : {
2002 [ + - ]: 1011352 : Trace("pf::arith::explain") << " recursion!" << std::endl;
2003 [ - + ][ - + ]: 1011352 : Assert(!isAssumption());
[ - - ]
2004 : 1011352 : AntecedentId p = getEndAntecedent();
2005 : 1011352 : ConstraintCP antecedent = d_database->d_antecedents[p];
2006 : 1011352 : std::vector<std::shared_ptr<ProofNode>> children;
2007 : :
2008 [ + + ]: 3150970 : while (antecedent != NullConstraint)
2009 : : {
2010 [ + - ]: 2139618 : Trace("pf::arith::explain") << "Explain " << antecedent << std::endl;
2011 : 2139618 : auto pn = antecedent->externalExplain(nb, order);
2012 [ + + ]: 2139618 : if (d_database->isProofEnabled())
2013 : : {
2014 : 793047 : children.push_back(pn);
2015 : : }
2016 : 2139618 : --p;
2017 : 2139618 : antecedent = d_database->d_antecedents[p];
2018 : 2139618 : }
2019 : :
2020 [ + + ]: 1011352 : if (d_database->isProofEnabled())
2021 : : {
2022 [ - + ][ + - ]: 461003 : switch (getProofType())
[ + - ]
2023 : : {
2024 : 0 : case ArithProofType::AssumeAP:
2025 : : case ArithProofType::EqualityEngineAP:
2026 : : {
2027 : 0 : Unreachable() << "These should be handled above";
2028 : : break;
2029 : : }
2030 : 62745 : case ArithProofType::FarkasAP:
2031 : : {
2032 : : // Per docs in constraint.h,
2033 : : // the 0th farkas coefficient is for the negation of the deduced
2034 : : // constraint the 1st corresponds to the last antecedent the nth
2035 : : // corresponds to the first antecedent Then, the farkas coefficients
2036 : : // and the antecedents are in the same order.
2037 : :
2038 : : // Enumerate child proofs (negation included) in d_farkasCoefficients
2039 : : // order
2040 : 62745 : Node plit = getNegation()->getProofLiteral();
2041 : 62745 : std::vector<std::shared_ptr<ProofNode>> farkasChildren;
2042 : 62745 : farkasChildren.push_back(pnm->mkAssume(plit));
2043 : 62745 : farkasChildren.insert(
2044 : 62745 : farkasChildren.end(), children.rbegin(), children.rend());
2045 : :
2046 : 62745 : NodeManager* nm = d_database->nodeManager();
2047 : :
2048 : : // Enumerate d_farkasCoefficients as nodes.
2049 : 62745 : std::vector<Node> farkasCoeffs;
2050 : 62745 : TypeNode type = plit[0].getType();
2051 [ + + ]: 484454 : for (Rational r : *getFarkasCoefficients())
2052 : : {
2053 : 421709 : farkasCoeffs.push_back(nm->mkConstRealOrInt(Rational(r)));
2054 : 421709 : }
2055 : : std::vector<Node> farkasCoeffsUse =
2056 : 62745 : getMacroSumUbCoeff(nm, farkasChildren, farkasCoeffs);
2057 : :
2058 : : // Apply the scaled-sum rule.
2059 : : std::shared_ptr<ProofNode> sumPf =
2060 : : pnm->mkNode(ProofRule::MACRO_ARITH_SCALE_SUM_UB,
2061 : : farkasChildren,
2062 : 62745 : farkasCoeffsUse);
2063 : :
2064 : : // Provable rewrite the result
2065 : 62745 : Node falsen = nm->mkConst(false);
2066 : 62745 : auto botPf = ensurePredTransform(pnm, sumPf, falsen);
2067 : :
2068 : : // Scope out the negated constraint, yielding a proof of the
2069 : : // constraint.
2070 : 188235 : std::vector<Node> assump{plit};
2071 : 125490 : auto maybeDoubleNotPf = pnm->mkScope(botPf, assump, false);
2072 : :
2073 : : // No need to ensure that the expected node aggrees with `assump`
2074 : : // because we are not providing an expected node.
2075 : : //
2076 : : // Prove that this is the literal (may need to clean a double-not)
2077 : 62745 : Node plit2 = getProofLiteral();
2078 : 62745 : pf = ensurePredTransform(pnm, maybeDoubleNotPf, plit2);
2079 : :
2080 : 62745 : break;
2081 : 62745 : }
2082 : 362433 : case ArithProofType::IntTightenAP:
2083 : : {
2084 [ + + ]: 362433 : if (isUpperBound())
2085 : : {
2086 : 691924 : pf = pnm->mkNode(
2087 : 1037886 : ProofRule::INT_TIGHT_UB, children, {}, getProofLiteral());
2088 : : }
2089 [ + - ]: 16471 : else if (isLowerBound())
2090 : : {
2091 : 32942 : pf = pnm->mkNode(
2092 : 49413 : ProofRule::INT_TIGHT_LB, children, {}, getProofLiteral());
2093 : : }
2094 : : else
2095 : : {
2096 : 0 : Unreachable();
2097 : : }
2098 : 362433 : break;
2099 : : }
2100 : 0 : case ArithProofType::IntHoleAP:
2101 : : {
2102 : : // Use proofLit to ensure deterministic node ID assignments
2103 : 0 : Node proofLit = getProofLiteral();
2104 : 0 : pf = pnm->mkTrustedNode(
2105 : 0 : TrustId::THEORY_INFERENCE_ARITH, children, {proofLit}, proofLit);
2106 : 0 : break;
2107 : 0 : }
2108 : 35825 : case ArithProofType::TrichotomyAP:
2109 : : {
2110 : 71650 : pf = pnm->mkNode(
2111 : 107475 : ProofRule::ARITH_TRICHOTOMY, children, {}, getProofLiteral());
2112 : 35825 : break;
2113 : : }
2114 : 0 : case ArithProofType::InternalAssumeAP:
2115 : : case ArithProofType::NoAP:
2116 : : default:
2117 : : {
2118 : 0 : Unreachable() << getProofType()
2119 : 0 : << " should not be visible in explanation";
2120 : : break;
2121 : : }
2122 : : }
2123 : : }
2124 : 1011352 : }
2125 : 7834644 : return pf;
2126 : 0 : }
2127 : :
2128 : 1704 : Node Constraint::externalExplainByAssertions(NodeManager* nm,
2129 : : ConstraintCP a,
2130 : : ConstraintCP b)
2131 : : {
2132 : 1704 : NodeBuilder nb(nm, Kind::AND);
2133 : 1704 : a->externalExplainByAssertions(nb);
2134 : 1704 : b->externalExplainByAssertions(nb);
2135 : 3408 : return nb;
2136 : 1704 : }
2137 : :
2138 : 0 : Node Constraint::externalExplainByAssertions(NodeManager* nm,
2139 : : ConstraintCP a,
2140 : : ConstraintCP b,
2141 : : ConstraintCP c)
2142 : : {
2143 : 0 : NodeBuilder nb(nm, Kind::AND);
2144 : 0 : a->externalExplainByAssertions(nb);
2145 : 0 : b->externalExplainByAssertions(nb);
2146 : 0 : c->externalExplainByAssertions(nb);
2147 : 0 : return nb;
2148 : 0 : }
2149 : :
2150 : 846538 : ConstraintP Constraint::getStrictlyWeakerLowerBound(bool hasLiteral,
2151 : : bool asserted) const
2152 : : {
2153 [ - + ][ - + ]: 846538 : Assert(initialized());
[ - - ]
2154 [ + + ][ + - ]: 846538 : Assert(!asserted || hasLiteral);
[ - + ][ - + ]
[ - - ]
2155 : :
2156 : 846538 : SortedConstraintMapConstIterator i = d_variablePosition;
2157 : 846538 : const SortedConstraintMap& scm = constraintSet();
2158 : 846538 : SortedConstraintMapConstIterator i_begin = scm.begin();
2159 [ + + ]: 1724355 : while (i != i_begin)
2160 : : {
2161 : 1028150 : --i;
2162 : 1028150 : const ValueCollection& vc = i->second;
2163 [ + + ]: 1028150 : if (vc.hasLowerBound())
2164 : : {
2165 : 304654 : ConstraintP weaker = vc.getLowerBound();
2166 : :
2167 : : // asserted -> hasLiteral
2168 : : // hasLiteral -> weaker->hasLiteral()
2169 : : // asserted -> weaker->assertedToTheTheory()
2170 [ + + ]: 304654 : if ((!hasLiteral || (weaker->hasLiteral()))
2171 [ + - ][ + + ]: 609308 : && (!asserted || (weaker->assertedToTheTheory())))
[ + + ][ + + ]
2172 : : {
2173 : 150333 : return weaker;
2174 : : }
2175 : : }
2176 : : }
2177 : 696205 : return NullConstraint;
2178 : : }
2179 : :
2180 : 601278 : ConstraintP Constraint::getStrictlyWeakerUpperBound(bool hasLiteral,
2181 : : bool asserted) const
2182 : : {
2183 : 601278 : SortedConstraintMapConstIterator i = d_variablePosition;
2184 : 601278 : const SortedConstraintMap& scm = constraintSet();
2185 : 601278 : SortedConstraintMapConstIterator i_end = scm.end();
2186 : :
2187 : 601278 : ++i;
2188 [ + + ]: 1100936 : for (; i != i_end; ++i)
2189 : : {
2190 : 711534 : const ValueCollection& vc = i->second;
2191 [ + + ]: 711534 : if (vc.hasUpperBound())
2192 : : {
2193 : 284349 : ConstraintP weaker = vc.getUpperBound();
2194 [ + + ]: 284349 : if ((!hasLiteral || (weaker->hasLiteral()))
2195 [ + - ][ + + ]: 568698 : && (!asserted || (weaker->assertedToTheTheory())))
[ + + ][ + + ]
2196 : : {
2197 : 211876 : return weaker;
2198 : : }
2199 : : }
2200 : : }
2201 : :
2202 : 389402 : return NullConstraint;
2203 : : }
2204 : :
2205 : 7068980 : ConstraintP ConstraintDatabase::getBestImpliedBound(
2206 : : ArithVar v, ConstraintType t, const DeltaRational& r) const
2207 : : {
2208 [ - + ][ - + ]: 7068980 : Assert(variableDatabaseIsSetup(v));
[ - - ]
2209 [ + + ][ + - ]: 7068980 : Assert(t == UpperBound || t == LowerBound);
[ - + ][ - + ]
[ - - ]
2210 : :
2211 : 7068980 : SortedConstraintMap& scm = getVariableSCM(v);
2212 [ + + ]: 7068980 : if (t == UpperBound)
2213 : : {
2214 : 3296326 : SortedConstraintMapConstIterator i = scm.lower_bound(r);
2215 : 3296326 : SortedConstraintMapConstIterator i_end = scm.end();
2216 [ + + ][ + - ]: 3296326 : Assert(i == i_end || r <= i->first);
[ - + ][ - + ]
[ - - ]
2217 [ + + ]: 4959576 : for (; i != i_end; i++)
2218 : : {
2219 [ - + ][ - + ]: 2867603 : Assert(r <= i->first);
[ - - ]
2220 : 2867603 : const ValueCollection& vc = i->second;
2221 [ + + ]: 2867603 : if (vc.hasUpperBound())
2222 : : {
2223 : 1204353 : return vc.getUpperBound();
2224 : : }
2225 : : }
2226 : 2091973 : return NullConstraint;
2227 : : }
2228 : : else
2229 : : {
2230 [ - + ][ - + ]: 3772654 : Assert(t == LowerBound);
[ - - ]
2231 [ + + ]: 3772654 : if (scm.empty())
2232 : : {
2233 : 303700 : return NullConstraint;
2234 : : }
2235 : : else
2236 : : {
2237 : 3468954 : SortedConstraintMapConstIterator i = scm.lower_bound(r);
2238 : 3468954 : SortedConstraintMapConstIterator i_begin = scm.begin();
2239 : 3468954 : SortedConstraintMapConstIterator i_end = scm.end();
2240 [ + + ][ + - ]: 3468954 : Assert(i == i_end || r <= i->first);
[ - + ][ - + ]
[ - - ]
2241 : :
2242 : 3468954 : int fdj = 0;
2243 : :
2244 [ + + ]: 3468954 : if (i == i_end)
2245 : : {
2246 : 1428751 : --i;
2247 [ + - ]: 2857502 : Trace("getBestImpliedBound")
2248 : 1428751 : << fdj++ << " " << r << " " << i->first << endl;
2249 : : }
2250 [ + + ]: 2040203 : else if ((i->first) > r)
2251 : : {
2252 [ + + ]: 624916 : if (i == i_begin)
2253 : : {
2254 : 549348 : return NullConstraint;
2255 : : }
2256 : : else
2257 : : {
2258 : 75568 : --i;
2259 [ + - ]: 151136 : Trace("getBestImpliedBound")
2260 : 75568 : << fdj++ << " " << r << " " << i->first << endl;
2261 : : }
2262 : : }
2263 : :
2264 : : do
2265 : : {
2266 [ + - ]: 6353338 : Trace("getBestImpliedBound")
2267 : 3176669 : << fdj++ << " " << r << " " << i->first << endl;
2268 [ - + ][ - + ]: 3176669 : Assert(r >= i->first);
[ - - ]
2269 : 3176669 : const ValueCollection& vc = i->second;
2270 : :
2271 [ + + ]: 3176669 : if (vc.hasLowerBound())
2272 : : {
2273 : 1569174 : return vc.getLowerBound();
2274 : : }
2275 : :
2276 [ + + ]: 1607495 : if (i == i_begin)
2277 : : {
2278 : 1350432 : break;
2279 : : }
2280 : : else
2281 : : {
2282 : 257063 : --i;
2283 : : }
2284 : 257063 : } while (true);
2285 : 1350432 : return NullConstraint;
2286 : : }
2287 : : }
2288 : : }
2289 : :
2290 : 25023954 : bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const
2291 : : {
2292 : 25023954 : return v < d_varDatabases.size();
2293 : : }
2294 : :
2295 : 28777 : ConstraintDatabase::Watches::Watches(context::Context* satContext,
2296 : 28777 : context::Context* userContext)
2297 : 28777 : : d_constraintProofs(satContext),
2298 : 28777 : d_canBePropagatedWatches(satContext),
2299 : 28777 : d_assertionOrderWatches(satContext),
2300 : 28777 : d_splitWatches(userContext)
2301 : : {
2302 : 28777 : }
2303 : :
2304 : 1196304 : void Constraint::setLiteral(Node n, CVC5_UNUSED Node nn)
2305 : : {
2306 [ + - ]: 1196304 : Trace("arith::constraint") << "Mapping " << *this << " to " << n << std::endl;
2307 : : // Note that we check the normal form nn of the literal here, not the
2308 : : // literal n itself. The literal may be an equality that is not in normal
2309 : : // form, e.g. (= (+ x 1) 2), (= 1 x) or (= (to_real x) 0.0), since the
2310 : : // rewriter does not normalize equalities, see rewriter::normalizeEquality.
2311 [ - + ][ - + ]: 1196304 : Assert(Comparison::isNormalAtom(nn));
[ - - ]
2312 [ - + ][ - + ]: 1196304 : Assert(sanityChecking(nn));
[ - - ]
2313 : 1196304 : NodetoConstraintMap& map = d_database->d_nodetoConstraintMap;
2314 [ - + ][ - + ]: 1196304 : Assert(map.find(n) == map.end());
[ - - ]
2315 : 1196304 : map.insert(make_pair(n, this));
2316 [ + + ]: 1196304 : if (hasLiteral())
2317 : : {
2318 : : // Multiple atoms may normalize to the same constraint. This is possible
2319 : : // for equalities, whose rewritten form retains the type of the original
2320 : : // equality, e.g. both (= x 0) and (= (to_real x) 0.0) may occur for an
2321 : : // integer variable x. We keep the first such atom as the literal of this
2322 : : // constraint and remember the others so that the node-to-constraint map
2323 : : // can be cleaned up when this constraint is deleted. Note the constraint
2324 : : // may still be asserted or explained using any of these atoms, which is
2325 : : // handled by tracking the witness of the assertion.
2326 : 14200 : d_database->d_altLiterals[this].push_back(n);
2327 : 14200 : return;
2328 : : }
2329 : 1182104 : d_literal = n;
2330 : : }
2331 : :
2332 : 4125577 : Node Constraint::getProofLiteral() const
2333 : : {
2334 [ - + ][ - + ]: 4125577 : Assert(d_database != nullptr);
[ - - ]
2335 [ - + ][ - + ]: 4125577 : Assert(d_database->d_avariables.hasNode(d_variable));
[ - - ]
2336 : 4125577 : Node varPart = d_database->d_avariables.asNode(d_variable);
2337 : : Kind cmp;
2338 : 4125577 : bool neg = false;
2339 [ + + ][ + + ]: 4125577 : switch (d_type)
[ - ]
2340 : : {
2341 : 1444060 : case ConstraintType::UpperBound:
2342 : : {
2343 [ + + ]: 1444060 : if (d_value.infinitesimalIsZero())
2344 : : {
2345 : 782717 : cmp = Kind::LEQ;
2346 : : }
2347 : : else
2348 : : {
2349 : 661343 : cmp = Kind::LT;
2350 : : }
2351 : 1444060 : break;
2352 : : }
2353 : 1064980 : case ConstraintType::LowerBound:
2354 : : {
2355 [ + + ]: 1064980 : if (d_value.infinitesimalIsZero())
2356 : : {
2357 : 902482 : cmp = Kind::GEQ;
2358 : : }
2359 : : else
2360 : : {
2361 : 162498 : cmp = Kind::GT;
2362 : : }
2363 : 1064980 : break;
2364 : : }
2365 : 1390831 : case ConstraintType::Equality:
2366 : : {
2367 : 1390831 : cmp = Kind::EQUAL;
2368 : 1390831 : break;
2369 : : }
2370 : 225706 : case ConstraintType::Disequality:
2371 : : {
2372 : 225706 : cmp = Kind::EQUAL;
2373 : 225706 : neg = true;
2374 : 225706 : break;
2375 : : }
2376 : 0 : default: Unreachable() << d_type;
2377 : : }
2378 : 4125577 : NodeManager* nm = d_database->nodeManager();
2379 : : Node constPart = nm->mkConstRealOrInt(
2380 : 12376731 : varPart.getType(), Rational(d_value.getNoninfinitesimalPart()));
2381 : 12376731 : Node posLit = nm->mkNode(cmp, varPart, constPart);
2382 [ + + ]: 8251154 : return neg ? posLit.negate() : posLit;
2383 : 4125577 : }
2384 : :
2385 : 75796 : void ConstraintDatabase::proveOr(std::vector<TrustNode>& out,
2386 : : ConstraintP a,
2387 : : ConstraintP b,
2388 : : bool negateSecond) const
2389 : : {
2390 : 75796 : Node la = a->getLiteral();
2391 : 75796 : Node lb = b->getLiteral();
2392 [ + + ]: 75796 : Node orN = (la < lb) ? la.orNode(lb) : lb.orNode(la);
2393 [ + + ]: 75796 : if (isProofEnabled())
2394 : : {
2395 [ - + ][ - + ]: 33266 : Assert(b->getNegation()->getType() != ConstraintType::Disequality);
[ - - ]
2396 : 33266 : auto nm = nodeManager();
2397 : 33266 : Node alit = a->getNegation()->getProofLiteral();
2398 : 33266 : TypeNode type = alit[0].getType();
2399 : 33266 : auto pf_neg_la = d_pnm->mkAssume(la.negate());
2400 : 33266 : pf_neg_la = ensurePredTransform(d_pnm, pf_neg_la, alit);
2401 : 33266 : Node blit = b->getNegation()->getProofLiteral();
2402 : 33266 : auto pf_neg_lb = d_pnm->mkAssume(lb.negate());
2403 : 33266 : pf_neg_lb = ensurePredTransform(d_pnm, pf_neg_lb, blit);
2404 [ + + ]: 33266 : int sndSign = negateSecond ? -1 : 1;
2405 : 133064 : std::vector<Pf> args{pf_neg_la, pf_neg_lb};
2406 : 0 : std::vector<Node> coeffs{nm->mkConstReal(Rational(-1 * sndSign)),
2407 : 166330 : nm->mkConstReal(Rational(sndSign))};
2408 : 33266 : std::vector<Node> coeffsUse = getMacroSumUbCoeff(nm, args, coeffs);
2409 : : auto sumubpf =
2410 : 33266 : d_pnm->mkNode(ProofRule::MACRO_ARITH_SCALE_SUM_UB, args, coeffsUse);
2411 : 33266 : auto bot_pf = ensurePredTransform(d_pnm, sumubpf, nm->mkConst(false));
2412 : 33266 : std::vector<Node> as;
2413 : 33266 : std::transform(orN.begin(), orN.end(), std::back_inserter(as), [](Node n) {
2414 : 66532 : return n.negate();
2415 : : });
2416 : : // No need to ensure that the expected node aggrees with `as` because we
2417 : : // are not providing an expected node.
2418 : : auto pf =
2419 : 133064 : d_pnm->mkNode(ProofRule::NOT_AND, {d_pnm->mkScope(bot_pf, as)}, {});
2420 : 33266 : pf = ensurePredTransform(d_pnm, pf, orN);
2421 : 33266 : out.push_back(d_pfGen->mkTrustNode(orN, pf));
2422 : 33266 : }
2423 : : else
2424 : : {
2425 : 42530 : out.push_back(TrustNode::mkTrustLemma(orN));
2426 : : }
2427 : 75796 : }
2428 : :
2429 : 71255 : void ConstraintDatabase::implies(std::vector<TrustNode>& out,
2430 : : ConstraintP a,
2431 : : ConstraintP b) const
2432 : : {
2433 : 71255 : Node la = a->getLiteral();
2434 : 71255 : Node lb = b->getLiteral();
2435 : :
2436 [ + + ]: 71255 : Node neg_la = (la.getKind() == Kind::NOT) ? la[0] : la.notNode();
2437 : :
2438 [ - + ][ - + ]: 71255 : Assert(lb != neg_la);
[ - - ]
2439 [ + + ][ + - ]: 71255 : Assert(b->getNegation()->getType() == ConstraintType::LowerBound
[ - + ][ - + ]
[ - - ]
2440 : : || b->getNegation()->getType() == ConstraintType::UpperBound);
2441 : 71255 : proveOr(out,
2442 : : a->getNegation(),
2443 : : b,
2444 : 71255 : b->getNegation()->getType() == ConstraintType::LowerBound);
2445 : 71255 : }
2446 : :
2447 : 4541 : void ConstraintDatabase::mutuallyExclusive(std::vector<TrustNode>& out,
2448 : : ConstraintP a,
2449 : : ConstraintP b) const
2450 : : {
2451 : 4541 : Node la = a->getLiteral();
2452 : 4541 : Node lb = b->getLiteral();
2453 : :
2454 : 4541 : Node neg_la = la.negate();
2455 : 4541 : Node neg_lb = lb.negate();
2456 : 4541 : proveOr(out, a->getNegation(), b->getNegation(), true);
2457 : 4541 : }
2458 : :
2459 : 117512 : void ConstraintDatabase::outputUnateInequalityLemmas(
2460 : : std::vector<TrustNode>& out, ArithVar v) const
2461 : : {
2462 : 117512 : SortedConstraintMap& scm = getVariableSCM(v);
2463 : 117512 : SortedConstraintMapConstIterator scm_iter = scm.begin();
2464 : 117512 : SortedConstraintMapConstIterator scm_end = scm.end();
2465 : 117512 : ConstraintP prev = NullConstraint;
2466 : : // get transitive unates
2467 : : // Only lower bounds or upperbounds should be done.
2468 [ + + ]: 375269 : for (; scm_iter != scm_end; ++scm_iter)
2469 : : {
2470 : 257757 : const ValueCollection& vc = scm_iter->second;
2471 [ + + ]: 257757 : if (vc.hasUpperBound())
2472 : : {
2473 : 121385 : ConstraintP ub = vc.getUpperBound();
2474 [ + + ]: 121385 : if (ub->hasLiteral())
2475 : : {
2476 [ + + ]: 121381 : if (prev != NullConstraint)
2477 : : {
2478 : 52988 : implies(out, prev, ub);
2479 : : }
2480 : 121381 : prev = ub;
2481 : : }
2482 : : }
2483 : : }
2484 : 117512 : }
2485 : :
2486 : 117512 : void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<TrustNode>& out,
2487 : : ArithVar v) const
2488 : : {
2489 : 117512 : vector<ConstraintP> equalities;
2490 : :
2491 : 117512 : SortedConstraintMap& scm = getVariableSCM(v);
2492 : 117512 : SortedConstraintMapConstIterator scm_iter = scm.begin();
2493 : 117512 : SortedConstraintMapConstIterator scm_end = scm.end();
2494 : :
2495 [ + + ]: 375269 : for (; scm_iter != scm_end; ++scm_iter)
2496 : : {
2497 : 257757 : const ValueCollection& vc = scm_iter->second;
2498 [ + + ]: 257757 : if (vc.hasEquality())
2499 : : {
2500 : 37669 : ConstraintP eq = vc.getEquality();
2501 [ + - ]: 37669 : if (eq->hasLiteral())
2502 : : {
2503 : 37669 : equalities.push_back(eq);
2504 : : }
2505 : : }
2506 : : }
2507 : :
2508 : 117512 : vector<ConstraintP>::const_iterator i, j, eq_end = equalities.end();
2509 [ + + ]: 155181 : for (i = equalities.begin(); i != eq_end; ++i)
2510 : : {
2511 : 37669 : ConstraintP at_i = *i;
2512 [ + + ]: 42210 : for (j = i + 1; j != eq_end; ++j)
2513 : : {
2514 : 4541 : ConstraintP at_j = *j;
2515 : :
2516 : 4541 : mutuallyExclusive(out, at_i, at_j);
2517 : : }
2518 : : }
2519 : :
2520 [ + + ]: 155181 : for (i = equalities.begin(); i != eq_end; ++i)
2521 : : {
2522 : 37669 : ConstraintP eq = *i;
2523 : 37669 : const ValueCollection& vc = eq->getValueCollection();
2524 [ + - ][ + - ]: 37669 : Assert(vc.hasEquality() && vc.getEquality()->hasLiteral());
[ - + ][ - + ]
[ - - ]
2525 : :
2526 [ + + ][ + - ]: 37669 : bool hasLB = vc.hasLowerBound() && vc.getLowerBound()->hasLiteral();
2527 [ + + ][ + + ]: 37669 : bool hasUB = vc.hasUpperBound() && vc.getUpperBound()->hasLiteral();
2528 : :
2529 [ + + ]: 37669 : ConstraintP lb = hasLB ? vc.getLowerBound()
2530 : 33789 : : eq->getStrictlyWeakerLowerBound(true, false);
2531 [ + + ]: 37669 : ConstraintP ub = hasUB ? vc.getUpperBound()
2532 : 36775 : : eq->getStrictlyWeakerUpperBound(true, false);
2533 : :
2534 [ + + ][ + + ]: 37669 : if (hasUB && hasLB && !eq->isSplit())
[ + - ][ + + ]
2535 : : {
2536 : 550 : out.push_back(eq->split());
2537 : : }
2538 [ + + ]: 37669 : if (lb != NullConstraint)
2539 : : {
2540 : 6145 : implies(out, eq, lb);
2541 : : }
2542 [ + + ]: 37669 : if (ub != NullConstraint)
2543 : : {
2544 : 12122 : implies(out, eq, ub);
2545 : : }
2546 : : }
2547 : 117512 : }
2548 : :
2549 : 24662 : void ConstraintDatabase::outputUnateEqualityLemmas(
2550 : : std::vector<TrustNode>& lemmas) const
2551 : : {
2552 [ + + ]: 142174 : for (ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v)
2553 : : {
2554 : 117512 : outputUnateEqualityLemmas(lemmas, v);
2555 : : }
2556 : 24662 : }
2557 : :
2558 : 24662 : void ConstraintDatabase::outputUnateInequalityLemmas(
2559 : : std::vector<TrustNode>& lemmas) const
2560 : : {
2561 [ + + ]: 142174 : for (ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v)
2562 : : {
2563 : 117512 : outputUnateInequalityLemmas(lemmas, v);
2564 : : }
2565 : 24662 : }
2566 : :
2567 : 5582416 : bool ConstraintDatabase::handleUnateProp(ConstraintP ant, ConstraintP cons)
2568 : : {
2569 [ - + ]: 5582416 : if (cons->negationHasProof())
2570 : : {
2571 [ - - ]: 0 : Trace("arith::unate") << "handleUnate: " << ant << " implies " << cons
2572 : 0 : << endl;
2573 : 0 : cons->impliedByUnate(nodeManager(), ant, true);
2574 : 0 : d_raiseConflict.raiseConflict(cons, InferenceId::ARITH_CONF_UNATE_PROP);
2575 : 0 : return true;
2576 : : }
2577 [ + + ]: 5582416 : else if (!cons->isTrue())
2578 : : {
2579 : 2172489 : ++d_statistics.d_unatePropagateImplications;
2580 [ + - ]: 4344978 : Trace("arith::unate") << "handleUnate: " << ant << " implies " << cons
2581 : 2172489 : << endl;
2582 : 2172489 : cons->impliedByUnate(nodeManager(), ant, false);
2583 : 2172489 : cons->tryToPropagate();
2584 : 2172489 : return false;
2585 : : }
2586 : : else
2587 : : {
2588 : 3409927 : return false;
2589 : : }
2590 : : }
2591 : :
2592 : 1992304 : void ConstraintDatabase::unatePropLowerBound(ConstraintP curr, ConstraintP prev)
2593 : : {
2594 [ + - ]: 3984608 : Trace("arith::unate") << "unatePropLowerBound " << curr << " " << prev
2595 : 1992304 : << endl;
2596 [ - + ][ - + ]: 1992304 : Assert(curr != prev);
[ - - ]
2597 [ - + ][ - + ]: 1992304 : Assert(curr != NullConstraint);
[ - - ]
2598 : 1992304 : bool hasPrev = !(prev == NullConstraint);
2599 [ + + ][ + - ]: 1992304 : Assert(!hasPrev || curr->getValue() > prev->getValue());
[ - + ][ - + ]
[ - - ]
2600 : :
2601 : 1992304 : ++d_statistics.d_unatePropagateCalls;
2602 : :
2603 : 1992304 : const SortedConstraintMap& scm = curr->constraintSet();
2604 : 1992304 : const SortedConstraintMapConstIterator scm_begin = scm.begin();
2605 : 1992304 : SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
2606 : :
2607 : : // Ignore the first ValueCollection
2608 : : // NOPE: (>= p c) then (= p c) NOPE
2609 : : // NOPE: (>= p c) then (not (= p c)) NOPE
2610 : :
2611 [ + + ]: 6787330 : while (scm_i != scm_begin)
2612 : : {
2613 : 5238061 : --scm_i; // move the iterator back
2614 : :
2615 : 5238061 : const ValueCollection& vc = scm_i->second;
2616 : :
2617 : : // If it has the previous element, do nothing and stop!
2618 [ + + ]: 1676084 : if (hasPrev && vc.hasConstraintOfType(prev->getType())
2619 [ + + ][ + + ]: 6914145 : && vc.getConstraintOfType(prev->getType()) == prev)
[ + + ]
2620 : : {
2621 : 443035 : break;
2622 : : }
2623 : :
2624 : : // Don't worry about implying the negation of upperbound.
2625 : : // These should all be handled by propagating the LowerBounds!
2626 [ + + ]: 4795026 : if (vc.hasLowerBound())
2627 : : {
2628 : 1810519 : ConstraintP lb = vc.getLowerBound();
2629 [ - + ]: 1810519 : if (handleUnateProp(curr, lb))
2630 : : {
2631 : 0 : return;
2632 : : }
2633 : : }
2634 [ + + ]: 4795026 : if (vc.hasDisequality())
2635 : : {
2636 : 476959 : ConstraintP dis = vc.getDisequality();
2637 [ - + ]: 476959 : if (handleUnateProp(curr, dis))
2638 : : {
2639 : 0 : return;
2640 : : }
2641 : : }
2642 : : }
2643 : : }
2644 : :
2645 : 1563881 : void ConstraintDatabase::unatePropUpperBound(ConstraintP curr, ConstraintP prev)
2646 : : {
2647 [ + - ]: 3127762 : Trace("arith::unate") << "unatePropUpperBound " << curr << " " << prev
2648 : 1563881 : << endl;
2649 [ - + ][ - + ]: 1563881 : Assert(curr != prev);
[ - - ]
2650 [ - + ][ - + ]: 1563881 : Assert(curr != NullConstraint);
[ - - ]
2651 : 1563881 : bool hasPrev = !(prev == NullConstraint);
2652 [ + + ][ + - ]: 1563881 : Assert(!hasPrev || curr->getValue() < prev->getValue());
[ - + ][ - + ]
[ - - ]
2653 : :
2654 : 1563881 : ++d_statistics.d_unatePropagateCalls;
2655 : :
2656 : 1563881 : const SortedConstraintMap& scm = curr->constraintSet();
2657 : 1563881 : const SortedConstraintMapConstIterator scm_end = scm.end();
2658 : 1563881 : SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
2659 : 1563881 : ++scm_i;
2660 [ + + ]: 6072140 : for (; scm_i != scm_end; ++scm_i)
2661 : : {
2662 : 4776074 : const ValueCollection& vc = scm_i->second;
2663 : :
2664 : : // If it has the previous element, do nothing and stop!
2665 [ + + ]: 879974 : if (hasPrev && vc.hasConstraintOfType(prev->getType())
2666 [ + + ][ + + ]: 5656048 : && vc.getConstraintOfType(prev->getType()) == prev)
[ + + ]
2667 : : {
2668 : 267815 : break;
2669 : : }
2670 : : // Don't worry about implying the negation of upperbound.
2671 : : // These should all be handled by propagating the UpperBounds!
2672 [ + + ]: 4508259 : if (vc.hasUpperBound())
2673 : : {
2674 : 1776967 : ConstraintP ub = vc.getUpperBound();
2675 [ - + ]: 1776967 : if (handleUnateProp(curr, ub))
2676 : : {
2677 : 0 : return;
2678 : : }
2679 : : }
2680 [ + + ]: 4508259 : if (vc.hasDisequality())
2681 : : {
2682 : 299779 : ConstraintP dis = vc.getDisequality();
2683 [ - + ]: 299779 : if (handleUnateProp(curr, dis))
2684 : : {
2685 : 0 : return;
2686 : : }
2687 : : }
2688 : : }
2689 : : }
2690 : :
2691 : 1476348 : void ConstraintDatabase::unatePropEquality(ConstraintP curr,
2692 : : ConstraintP prevLB,
2693 : : ConstraintP prevUB)
2694 : : {
2695 [ + - ]: 2952696 : Trace("arith::unate") << "unatePropEquality " << curr << " " << prevLB << " "
2696 : 1476348 : << prevUB << endl;
2697 [ - + ][ - + ]: 1476348 : Assert(curr != prevLB);
[ - - ]
2698 [ - + ][ - + ]: 1476348 : Assert(curr != prevUB);
[ - - ]
2699 [ - + ][ - + ]: 1476348 : Assert(curr != NullConstraint);
[ - - ]
2700 : 1476348 : bool hasPrevLB = !(prevLB == NullConstraint);
2701 : 1476348 : bool hasPrevUB = !(prevUB == NullConstraint);
2702 [ + + ][ + - ]: 1476348 : Assert(!hasPrevLB || curr->getValue() >= prevLB->getValue());
[ - + ][ - + ]
[ - - ]
2703 [ + + ][ + - ]: 1476348 : Assert(!hasPrevUB || curr->getValue() <= prevUB->getValue());
[ - + ][ - + ]
[ - - ]
2704 : :
2705 : 1476348 : ++d_statistics.d_unatePropagateCalls;
2706 : :
2707 : 1476348 : const SortedConstraintMap& scm = curr->constraintSet();
2708 : 1476348 : SortedConstraintMapConstIterator scm_curr = curr->d_variablePosition;
2709 : : SortedConstraintMapConstIterator scm_last =
2710 [ + + ]: 1476348 : hasPrevUB ? prevUB->d_variablePosition : scm.end();
2711 : 1476348 : SortedConstraintMapConstIterator scm_i;
2712 [ + + ]: 1476348 : if (hasPrevLB)
2713 : : {
2714 : 188603 : scm_i = prevLB->d_variablePosition;
2715 [ + + ]: 188603 : if (scm_i != scm_curr)
2716 : : { // If this does not move this past scm_curr, move it one forward
2717 : 31819 : ++scm_i;
2718 : : }
2719 : : }
2720 : : else
2721 : : {
2722 : 1287745 : scm_i = scm.begin();
2723 : : }
2724 : :
2725 [ + + ]: 2202485 : for (; scm_i != scm_curr; ++scm_i)
2726 : : {
2727 : : // between the previous LB and the curr
2728 : 726137 : const ValueCollection& vc = scm_i->second;
2729 : :
2730 : : // Don't worry about implying the negation of upperbound.
2731 : : // These should all be handled by propagating the LowerBounds!
2732 [ + + ]: 726137 : if (vc.hasLowerBound())
2733 : : {
2734 : 202773 : ConstraintP lb = vc.getLowerBound();
2735 [ - + ]: 202773 : if (handleUnateProp(curr, lb))
2736 : : {
2737 : 0 : return;
2738 : : }
2739 : : }
2740 [ + + ]: 726137 : if (vc.hasDisequality())
2741 : : {
2742 : 188095 : ConstraintP dis = vc.getDisequality();
2743 [ - + ]: 188095 : if (handleUnateProp(curr, dis))
2744 : : {
2745 : 0 : return;
2746 : : }
2747 : : }
2748 : : }
2749 [ - + ][ - + ]: 1476348 : Assert(scm_i == scm_curr);
[ - - ]
2750 [ + + ][ + + ]: 1476348 : if (!hasPrevUB || scm_i != scm_last)
[ + + ]
2751 : : {
2752 : 1437317 : ++scm_i;
2753 : : } // hasPrevUB implies scm_i != scm_last
2754 : :
2755 [ + + ]: 3177420 : for (; scm_i != scm_last; ++scm_i)
2756 : : {
2757 : : // between the curr and the previous UB imply the upperbounds and
2758 : : // disequalities.
2759 : 1701072 : const ValueCollection& vc = scm_i->second;
2760 : :
2761 : : // Don't worry about implying the negation of upperbound.
2762 : : // These should all be handled by propagating the UpperBounds!
2763 [ + + ]: 1701072 : if (vc.hasUpperBound())
2764 : : {
2765 : 605895 : ConstraintP ub = vc.getUpperBound();
2766 [ - + ]: 605895 : if (handleUnateProp(curr, ub))
2767 : : {
2768 : 0 : return;
2769 : : }
2770 : : }
2771 [ + + ]: 1701072 : if (vc.hasDisequality())
2772 : : {
2773 : 221429 : ConstraintP dis = vc.getDisequality();
2774 [ - + ]: 221429 : if (handleUnateProp(curr, dis))
2775 : : {
2776 : 0 : return;
2777 : : }
2778 : : }
2779 : : }
2780 : : }
2781 : :
2782 : 1300433 : std::pair<int, int> Constraint::unateFarkasSigns(ConstraintCP ca,
2783 : : ConstraintCP cb)
2784 : : {
2785 : 1300433 : ConstraintType a = ca->getType();
2786 : 1300433 : ConstraintType b = cb->getType();
2787 : :
2788 [ - + ][ - + ]: 1300433 : Assert(a != Disequality);
[ - - ]
2789 [ - + ][ - + ]: 1300433 : Assert(b != Disequality);
[ - - ]
2790 : :
2791 [ + + ][ + + ]: 1300433 : int a_sgn = (a == LowerBound) ? -1 : ((a == UpperBound) ? 1 : 0);
2792 [ + + ][ + + ]: 1300433 : int b_sgn = (b == LowerBound) ? -1 : ((b == UpperBound) ? 1 : 0);
2793 : :
2794 [ + + ][ + + ]: 1300433 : if (a_sgn == 0 && b_sgn == 0)
2795 : : {
2796 [ - + ][ - + ]: 136395 : Assert(a == Equality);
[ - - ]
2797 [ - + ][ - + ]: 136395 : Assert(b == Equality);
[ - - ]
2798 [ - + ][ - + ]: 136395 : Assert(ca->getValue() != cb->getValue());
[ - - ]
2799 [ + + ]: 136395 : if (ca->getValue() < cb->getValue())
2800 : : {
2801 : 51095 : a_sgn = 1;
2802 : 51095 : b_sgn = -1;
2803 : : }
2804 : : else
2805 : : {
2806 : 85300 : a_sgn = -1;
2807 : 85300 : b_sgn = 1;
2808 : : }
2809 : : }
2810 [ + + ]: 1164038 : else if (a_sgn == 0)
2811 : : {
2812 [ - + ][ - + ]: 272950 : Assert(b_sgn != 0);
[ - - ]
2813 [ - + ][ - + ]: 272950 : Assert(a == Equality);
[ - - ]
2814 : 272950 : a_sgn = -b_sgn;
2815 : : }
2816 [ + + ]: 891088 : else if (b_sgn == 0)
2817 : : {
2818 [ - + ][ - + ]: 276347 : Assert(a_sgn != 0);
[ - - ]
2819 [ - + ][ - + ]: 276347 : Assert(b == Equality);
[ - - ]
2820 : 276347 : b_sgn = -a_sgn;
2821 : : }
2822 [ - + ][ - + ]: 1300433 : Assert(a_sgn != 0);
[ - - ]
2823 [ - + ][ - + ]: 1300433 : Assert(b_sgn != 0);
[ - - ]
2824 : :
2825 [ + - ]: 2600866 : Trace("arith::unateFarkasSigns")
2826 : 0 : << "Constraint::unateFarkasSigns(" << a << ", " << b << ") -> "
2827 : 1300433 : << "(" << a_sgn << ", " << b_sgn << ")" << endl;
2828 : 2600866 : return make_pair(a_sgn, b_sgn);
2829 : : }
2830 : :
2831 : : } // namespace arith::linear
2832 : : } // namespace theory
2833 : : } // namespace cvc5::internal
|
