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 : 9510349 : ConstraintRule::ConstraintRule(ConstraintP con, ArithProofType pt)
50 : 9510349 : : d_constraint(con), d_proofType(pt), d_antecedentEnd(AntecedentIdSentinel)
51 : : {
52 : 9510349 : d_farkasCoefficients = RationalVectorCPSentinel;
53 : 9510349 : }
54 : 3261871 : ConstraintRule::ConstraintRule(ConstraintP con,
55 : : ArithProofType pt,
56 : 3261871 : AntecedentId antecedentEnd)
57 : 3261871 : : d_constraint(con), d_proofType(pt), d_antecedentEnd(antecedentEnd)
58 : : {
59 : 3261871 : d_farkasCoefficients = RationalVectorCPSentinel;
60 : 3261871 : }
61 : :
62 : 3787921 : ConstraintRule::ConstraintRule(ConstraintP con,
63 : : ArithProofType pt,
64 : : AntecedentId antecedentEnd,
65 : 3787921 : RationalVectorCP coeffs)
66 : 3787921 : : d_constraint(con), d_proofType(pt), d_antecedentEnd(antecedentEnd)
67 : : {
68 [ + + ][ + - ]: 3787921 : Assert(con->isProofProducing() || coeffs == RationalVectorCPSentinel);
[ - + ][ - + ]
[ - - ]
69 : 3787921 : d_farkasCoefficients = coeffs;
70 : 3787921 : }
71 : :
72 : : /** Given a simplifiedKind this returns the corresponding ConstraintType. */
73 : : // ConstraintType constraintTypeOfLiteral(Kind k);
74 : 1190136 : ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp)
75 : : {
76 : 1190136 : Kind k = cmp.comparisonKind();
77 [ + + ][ + + ]: 1190136 : switch (k)
[ - ]
78 : : {
79 : 321163 : case Kind::LT:
80 : : case Kind::LEQ:
81 : : {
82 : 321163 : Polynomial l = cmp.getLeft();
83 [ + + ]: 321163 : if (l.leadingCoefficientIsPositive())
84 : : { // (< x c)
85 : 278436 : return UpperBound;
86 : : }
87 : : else
88 : : {
89 : 42727 : return LowerBound; // (< (-x) c)
90 : : }
91 : 321163 : }
92 : 323946 : case Kind::GT:
93 : : case Kind::GEQ:
94 : : {
95 : 323946 : Polynomial l = cmp.getLeft();
96 [ + + ]: 323946 : if (l.leadingCoefficientIsPositive())
97 : : {
98 : 280839 : return LowerBound; // (> x c)
99 : : }
100 : : else
101 : : {
102 : 43107 : return UpperBound; // (> (-x) c)
103 : : }
104 : 323946 : }
105 : 272759 : case Kind::EQUAL: return Equality;
106 : 272268 : case Kind::DISTINCT: return Disequality;
107 : 0 : default: Unhandled() << k;
108 : : }
109 : : }
110 : :
111 : 1501464 : Constraint::Constraint(ArithVar x,
112 : : ConstraintType t,
113 : : const DeltaRational& v,
114 : 1501464 : bool produceProofs)
115 : 1501464 : : d_variable(x),
116 : 1501464 : d_type(t),
117 : 1501464 : d_value(v),
118 : 1501464 : d_database(nullptr),
119 : 1501464 : d_literal(Node::null()),
120 : 1501464 : d_negation(NullConstraint),
121 : 1501464 : d_canBePropagated(false),
122 : 1501464 : d_assertionOrder(AssertionOrderSentinel),
123 : 1501464 : d_witness(TNode::null()),
124 : 1501464 : d_crid(ConstraintRuleIdSentinel),
125 : 1501464 : d_split(false),
126 : 1501464 : d_variablePosition(),
127 : 1501464 : d_produceProofs(produceProofs)
128 : : {
129 [ - + ][ - + ]: 1501464 : Assert(!initialized());
[ - - ]
130 : 1501464 : }
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 : 4399662 : ValueCollection::ValueCollection()
247 : 4399662 : : d_lowerBound(NullConstraint),
248 : 4399662 : d_upperBound(NullConstraint),
249 : 4399662 : d_equality(NullConstraint),
250 : 4399662 : d_disequality(NullConstraint)
251 : : {
252 : 4399662 : }
253 : :
254 : 33215362 : bool ValueCollection::hasLowerBound() const
255 : : {
256 : 33215362 : return d_lowerBound != NullConstraint;
257 : : }
258 : :
259 : 36590249 : bool ValueCollection::hasUpperBound() const
260 : : {
261 : 36590249 : return d_upperBound != NullConstraint;
262 : : }
263 : :
264 : 10115575 : bool ValueCollection::hasEquality() const
265 : : {
266 : 10115575 : return d_equality != NullConstraint;
267 : : }
268 : :
269 : 28533293 : bool ValueCollection::hasDisequality() const
270 : : {
271 : 28533293 : return d_disequality != NullConstraint;
272 : : }
273 : :
274 : 6125370 : ConstraintP ValueCollection::getLowerBound() const
275 : : {
276 [ - + ][ - + ]: 6125370 : Assert(hasLowerBound());
[ - - ]
277 : 6125370 : return d_lowerBound;
278 : : }
279 : :
280 : 6560790 : ConstraintP ValueCollection::getUpperBound() const
281 : : {
282 [ - + ][ - + ]: 6560790 : Assert(hasUpperBound());
[ - - ]
283 : 6560790 : return d_upperBound;
284 : : }
285 : :
286 : 844541 : ConstraintP ValueCollection::getEquality() const
287 : : {
288 [ - + ][ - + ]: 844541 : Assert(hasEquality());
[ - - ]
289 : 844541 : return d_equality;
290 : : }
291 : :
292 : 3846875 : ConstraintP ValueCollection::getDisequality() const
293 : : {
294 [ - + ][ - + ]: 3846875 : Assert(hasDisequality());
[ - - ]
295 : 3846875 : return d_disequality;
296 : : }
297 : :
298 : 1021085 : void ValueCollection::push_into(std::vector<ConstraintP>& vec) const
299 : : {
300 [ + - ]: 1021085 : Trace("arith::constraint") << "push_into " << *this << endl;
301 [ + + ]: 1021085 : if (hasEquality())
302 : : {
303 : 280393 : vec.push_back(d_equality);
304 : : }
305 [ + + ]: 1021085 : if (hasLowerBound())
306 : : {
307 : 468248 : vec.push_back(d_lowerBound);
308 : : }
309 [ + + ]: 1021085 : if (hasUpperBound())
310 : : {
311 : 468248 : vec.push_back(d_upperBound);
312 : : }
313 [ + + ]: 1021085 : if (hasDisequality())
314 : : {
315 : 280393 : vec.push_back(d_disequality);
316 : : }
317 : 1021085 : }
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 : 7313453 : bool ValueCollection::hasConstraintOfType(ConstraintType t) const
335 : : {
336 [ + + ][ + - ]: 7313453 : switch (t)
[ - ]
337 : : {
338 : 2424656 : case LowerBound: return hasLowerBound();
339 : 3943402 : case UpperBound: return hasUpperBound();
340 : 945395 : case Equality: return hasEquality();
341 : 0 : case Disequality: return hasDisequality();
342 : 0 : default: Unreachable();
343 : : }
344 : : }
345 : :
346 : 492237 : ArithVar ValueCollection::getVariable() const
347 : : {
348 [ - + ][ - + ]: 492237 : Assert(!empty());
[ - - ]
349 : 492237 : return nonNull()->getVariable();
350 : : }
351 : :
352 : 492237 : const DeltaRational& ValueCollection::getValue() const
353 : : {
354 [ - + ][ - + ]: 492237 : Assert(!empty());
[ - - ]
355 : 492237 : return nonNull()->getValue();
356 : : }
357 : :
358 : 1498190 : void ValueCollection::add(ConstraintP c)
359 : : {
360 [ - + ][ - + ]: 1498190 : Assert(c != NullConstraint);
[ - - ]
361 : :
362 [ + + ][ + - ]: 1498190 : Assert(empty() || getVariable() == c->getVariable());
[ - + ][ - + ]
[ - - ]
363 [ + + ][ + - ]: 1498190 : Assert(empty() || getValue() == c->getValue());
[ - + ][ - + ]
[ - - ]
364 : :
365 [ + + ][ + + ]: 1498190 : switch (c->getType())
[ - ]
366 : : {
367 : 468590 : case LowerBound:
368 [ - + ][ - + ]: 468590 : Assert(!hasLowerBound());
[ - - ]
369 : 468590 : d_lowerBound = c;
370 : 468590 : break;
371 : 280505 : case Equality:
372 [ - + ][ - + ]: 280505 : Assert(!hasEquality());
[ - - ]
373 : 280505 : d_equality = c;
374 : 280505 : break;
375 : 468590 : case UpperBound:
376 [ - + ][ - + ]: 468590 : Assert(!hasUpperBound());
[ - - ]
377 : 468590 : d_upperBound = c;
378 : 468590 : break;
379 : 280505 : case Disequality:
380 [ - + ][ - + ]: 280505 : Assert(!hasDisequality());
[ - - ]
381 : 280505 : d_disequality = c;
382 : 280505 : break;
383 : 0 : default: Unreachable();
384 : : }
385 : 1498190 : }
386 : :
387 : 5436604 : ConstraintP ValueCollection::getConstraintOfType(ConstraintType t) const
388 : : {
389 [ + + ][ + - ]: 5436604 : switch (t)
[ - ]
390 : : {
391 [ - + ][ - + ]: 1458334 : case LowerBound: Assert(hasLowerBound()); return d_lowerBound;
[ - - ]
392 [ - + ][ - + ]: 664890 : case Equality: Assert(hasEquality()); return d_equality;
[ - - ]
393 [ - + ][ - + ]: 3313380 : case UpperBound: Assert(hasUpperBound()); return d_upperBound;
[ - - ]
394 : 0 : case Disequality: Assert(hasDisequality()); return d_disequality;
395 : 0 : default: Unreachable();
396 : : }
397 : : }
398 : :
399 : 1497282 : void ValueCollection::remove(ConstraintType t)
400 : : {
401 [ + + ][ + + ]: 1497282 : switch (t)
[ - ]
402 : : {
403 : 468248 : case LowerBound:
404 [ - + ][ - + ]: 468248 : Assert(hasLowerBound());
[ - - ]
405 : 468248 : d_lowerBound = NullConstraint;
406 : 468248 : break;
407 : 280393 : case Equality:
408 [ - + ][ - + ]: 280393 : Assert(hasEquality());
[ - - ]
409 : 280393 : d_equality = NullConstraint;
410 : 280393 : break;
411 : 468248 : case UpperBound:
412 [ - + ][ - + ]: 468248 : Assert(hasUpperBound());
[ - - ]
413 : 468248 : d_upperBound = NullConstraint;
414 : 468248 : break;
415 : 280393 : case Disequality:
416 [ - + ][ - + ]: 280393 : Assert(hasDisequality());
[ - - ]
417 : 280393 : d_disequality = NullConstraint;
418 : 280393 : break;
419 : 0 : default: Unreachable();
420 : : }
421 : 1497282 : }
422 : :
423 : 5478136 : bool ValueCollection::empty() const
424 : : {
425 [ + + ][ + + ]: 8542697 : return !(hasLowerBound() || hasUpperBound() || hasEquality()
[ + + ]
426 [ + - ]: 8542697 : || hasDisequality());
427 : : }
428 : :
429 : 984474 : 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 [ + + ]: 984474 : if (hasLowerBound())
434 : : {
435 : 312320 : return d_lowerBound;
436 : : }
437 [ + + ]: 672154 : else if (hasUpperBound())
438 : : {
439 : 90054 : return d_upperBound;
440 : : }
441 [ + - ]: 582100 : else if (hasEquality())
442 : : {
443 : 582100 : 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 : 5327615 : 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 : 1498190 : void Constraint::initialize(ConstraintDatabase* db,
464 : : SortedConstraintMapIterator v,
465 : : ConstraintP negation)
466 : : {
467 [ - + ][ - + ]: 1498190 : Assert(!initialized());
[ - - ]
468 : 1498190 : d_database = db;
469 : 1498190 : d_variablePosition = v;
470 : 1498190 : d_negation = negation;
471 : 1498190 : }
472 : :
473 : 3001112 : Constraint::~Constraint()
474 : : {
475 : : // Call this instead of safeToGarbageCollect()
476 [ - + ][ - + ]: 1500556 : Assert(!contextDependentDataIsSet());
477 : :
478 [ + + ]: 1500556 : if (initialized())
479 : : {
480 : 1497282 : ValueCollection& vc = d_variablePosition->second;
481 [ + - ]: 1497282 : Trace("arith::constraint") << "removing" << vc << endl;
482 : :
483 : 1497282 : vc.remove(getType());
484 : :
485 [ + + ]: 1497282 : if (vc.empty())
486 : : {
487 [ + - ]: 1021085 : Trace("arith::constraint") << "erasing" << vc << endl;
488 : : SortedConstraintMap& perVariable =
489 : 1021085 : d_database->getVariableSCM(getVariable());
490 : 1021085 : perVariable.erase(d_variablePosition);
491 : : }
492 : :
493 [ + + ]: 1497282 : if (hasLiteral())
494 : : {
495 : 1192672 : d_database->d_nodetoConstraintMap.erase(getLiteral());
496 : : }
497 : : }
498 : 1500556 : }
499 : :
500 : 45677827 : const ConstraintRule& Constraint::getConstraintRule() const
501 : : {
502 [ - + ][ - + ]: 45677827 : Assert(hasProof());
[ - - ]
503 : 45677827 : return d_database->d_watches->d_constraintProofs[d_crid];
504 : : }
505 : :
506 : 5908766 : const ValueCollection& Constraint::getValueCollection() const
507 : : {
508 : 5908766 : return d_variablePosition->second;
509 : : }
510 : :
511 : 146831 : ConstraintP Constraint::getCeiling()
512 : : {
513 [ + - ]: 146831 : Trace("getCeiling") << "Constraint_::getCeiling on " << *this << endl;
514 [ - + ][ - + ]: 146831 : Assert(getValue().getInfinitesimalPart().sgn() > 0);
[ - - ]
515 : :
516 : 293662 : const DeltaRational ceiling(getValue().ceiling());
517 : 293662 : return d_database->getConstraint(getVariable(), getType(), ceiling);
518 : 146831 : }
519 : :
520 : 2499115 : ConstraintP Constraint::getFloor()
521 : : {
522 [ - + ][ - + ]: 2499115 : Assert(getValue().getInfinitesimalPart().sgn() < 0);
[ - - ]
523 : :
524 : 4998230 : const DeltaRational floor(Rational(getValue().floor()));
525 : 4998230 : return d_database->getConstraint(getVariable(), getType(), floor);
526 : 2499115 : }
527 : :
528 : 1835830 : void Constraint::setCanBePropagated()
529 : : {
530 [ - + ][ - + ]: 1835830 : Assert(!canBePropagated());
[ - - ]
531 : 1835830 : d_database->pushCanBePropagatedWatch(this);
532 : 1835830 : }
533 : :
534 : 10799775 : void Constraint::setAssertedToTheTheory(TNode witness, bool nowInConflict)
535 : : {
536 [ - + ][ - + ]: 10799775 : Assert(hasLiteral());
[ - - ]
537 [ - + ][ - + ]: 10799775 : Assert(!assertedToTheTheory());
[ - - ]
538 [ - + ][ - + ]: 10799775 : Assert(negationHasProof() == nowInConflict);
[ - - ]
539 : 10799775 : d_database->pushAssertionOrderWatch(this, witness);
540 : :
541 : 10799775 : if (TraceIsOn("constraint::conflictCommit") && nowInConflict)
542 : : {
543 [ - - ]: 0 : Trace("constraint::conflictCommit") << "inConflict@setAssertedToTheTheory";
544 [ - - ]: 0 : Trace("constraint::conflictCommit") << "\t" << this << std::endl;
545 [ - - ]: 0 : Trace("constraint::conflictCommit") << "\t" << getNegation() << std::endl;
546 [ - - ]: 0 : Trace("constraint::conflictCommit")
547 : 0 : << "\t" << getNegation()->externalExplainByAssertions() << std::endl;
548 : : }
549 : 10799775 : }
550 : :
551 : 0 : bool Constraint::satisfiedBy(const DeltaRational& dr) const
552 : : {
553 [ - - ][ - - ]: 0 : switch (getType())
[ - ]
554 : : {
555 : 0 : case LowerBound: return getValue() <= dr;
556 : 0 : case Equality: return getValue() == dr;
557 : 0 : case UpperBound: return getValue() >= dr;
558 : 0 : case Disequality: return getValue() != dr;
559 : : }
560 : 0 : Unreachable();
561 : : }
562 : :
563 : 18542838 : bool Constraint::isInternalAssumption() const
564 : : {
565 : 18542838 : return getProofType() == InternalAssumeAP;
566 : : }
567 : :
568 : 0 : TrustNode Constraint::externalExplainByAssertions() const
569 : : {
570 : 0 : NodeBuilder nb(d_database->nodeManager(), Kind::AND);
571 : 0 : auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel);
572 : 0 : Node exp = mkAndFromBuilder(d_database->nodeManager(), nb);
573 [ - - ]: 0 : if (d_database->isProofEnabled())
574 : : {
575 : 0 : std::vector<Node> assumptions;
576 [ - - ]: 0 : if (exp.getKind() == Kind::AND)
577 : : {
578 : 0 : assumptions.insert(assumptions.end(), exp.begin(), exp.end());
579 : : }
580 : : else
581 : : {
582 : 0 : assumptions.push_back(exp);
583 : : }
584 : 0 : auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
585 : 0 : return d_database->d_pfGen->mkTrustedPropagation(
586 : 0 : getLiteral(), d_database->nodeManager()->mkAnd(assumptions), pf);
587 : 0 : }
588 : 0 : return TrustNode::mkTrustPropExp(getLiteral(), exp);
589 : 0 : }
590 : :
591 : 19882535 : bool Constraint::isAssumption() const { return getProofType() == AssumeAP; }
592 : :
593 : 1323046 : bool Constraint::hasEqualityEngineProof() const
594 : : {
595 : 1323046 : return getProofType() == EqualityEngineAP;
596 : : }
597 : :
598 : 0 : bool Constraint::hasFarkasProof() const { return getProofType() == FarkasAP; }
599 : :
600 : 0 : bool Constraint::hasSimpleFarkasProof() const
601 : : {
602 [ - - ]: 0 : Trace("constraints::hsfp") << "hasSimpleFarkasProof " << this << std::endl;
603 [ - - ]: 0 : if (!hasFarkasProof())
604 : : {
605 [ - - ]: 0 : Trace("constraints::hsfp") << "There is no simple Farkas proof because "
606 : 0 : "there is no farkas proof."
607 : 0 : << std::endl;
608 : 0 : return false;
609 : : }
610 : :
611 : : // For each antecdent ...
612 : 0 : AntecedentId i = getConstraintRule().d_antecedentEnd;
613 [ - - ]: 0 : for (ConstraintCP a = d_database->getAntecedent(i); a != NullConstraint;
614 : 0 : a = d_database->getAntecedent(--i))
615 : : {
616 : : // ... that antecdent must be an assumption OR a tightened assumption ...
617 [ - - ]: 0 : if (a->isPossiblyTightenedAssumption())
618 : : {
619 : 0 : continue;
620 : : }
621 : :
622 : : // ... otherwise, we do not have a simple Farkas proof.
623 [ - - ]: 0 : if (TraceIsOn("constraints::hsfp"))
624 : : {
625 [ - - ]: 0 : Trace("constraints::hsfp") << "There is no simple Farkas proof b/c there "
626 : 0 : "is an antecdent w/ rule ";
627 [ - - ]: 0 : a->getConstraintRule().print(Trace("constraints::hsfp"), d_produceProofs);
628 [ - - ]: 0 : Trace("constraints::hsfp") << std::endl;
629 : : }
630 : :
631 : 0 : return false;
632 : : }
633 : 0 : return true;
634 : : }
635 : :
636 : 0 : bool Constraint::isPossiblyTightenedAssumption() const
637 : : {
638 : : // ... that antecdent must be an assumption ...
639 : :
640 [ - - ]: 0 : if (isAssumption()) return true;
641 [ - - ]: 0 : if (!hasIntTightenProof()) return false;
642 [ - - ]: 0 : if (getConstraintRule().d_antecedentEnd == AntecedentIdSentinel) return false;
643 : 0 : return d_database->getAntecedent(getConstraintRule().d_antecedentEnd)
644 : 0 : ->isAssumption();
645 : : }
646 : :
647 : 0 : bool Constraint::hasIntTightenProof() const
648 : : {
649 : 0 : return getProofType() == IntTightenAP;
650 : : }
651 : :
652 : 0 : bool Constraint::hasIntHoleProof() const { return getProofType() == IntHoleAP; }
653 : :
654 : 0 : bool Constraint::hasTrichotomyProof() const
655 : : {
656 : 0 : return getProofType() == TrichotomyAP;
657 : : }
658 : :
659 : 0 : void Constraint::printProofTree(std::ostream& out, size_t depth) const
660 : : {
661 [ - - ]: 0 : if (d_produceProofs)
662 : : {
663 : 0 : const ConstraintRule& rule = getConstraintRule();
664 : 0 : out << std::string(2 * depth, ' ') << "* " << getVariable() << " [";
665 : 0 : out << getProofLiteral();
666 [ - - ]: 0 : if (assertedToTheTheory())
667 : : {
668 : 0 : out << " | wit: " << getWitness();
669 : : }
670 : 0 : out << "]" << ' ' << getType() << ' ' << getValue() << " ("
671 : 0 : << getProofType() << ")";
672 [ - - ]: 0 : if (getProofType() == FarkasAP)
673 : : {
674 : 0 : out << " [";
675 : 0 : bool first = true;
676 [ - - ]: 0 : for (const auto& coeff : *rule.d_farkasCoefficients)
677 : : {
678 [ - - ]: 0 : if (!first)
679 : : {
680 : 0 : out << ", ";
681 : : }
682 : 0 : first = false;
683 : 0 : out << coeff;
684 : : }
685 : 0 : out << "]";
686 : : }
687 : 0 : out << endl;
688 : :
689 [ - - ]: 0 : for (AntecedentId i = rule.d_antecedentEnd; i != AntecedentIdSentinel; --i)
690 : : {
691 : 0 : ConstraintCP antecdent = d_database->getAntecedent(i);
692 [ - - ]: 0 : if (antecdent == NullConstraint)
693 : : {
694 : 0 : break;
695 : : }
696 : 0 : antecdent->printProofTree(out, depth + 1);
697 : : }
698 : 0 : return;
699 : : }
700 : 0 : out << "Cannot print proof. This is not a proof build." << endl;
701 : : }
702 : :
703 : 1193410 : bool Constraint::sanityChecking(Node n) const
704 : : {
705 : 1193410 : Comparison cmp = Comparison::parseNormalForm(n);
706 : 1193410 : Kind k = cmp.comparisonKind();
707 : 1193410 : Polynomial pleft = cmp.normalizedVariablePart();
708 [ + + ][ + + ]: 1193410 : Assert(k == Kind::EQUAL || k == Kind::DISTINCT
[ + + ][ + - ]
[ - + ][ - + ]
[ - - ]
709 : : || pleft.leadingCoefficientIsPositive());
710 : 1193410 : Assert(
711 : : k != Kind::EQUAL
712 : : || Monomial::isMember(n[0].getKind() == Kind::TO_REAL ? n[0][0] : n[0]));
713 : 1193410 : Assert(k != Kind::DISTINCT
714 : : || Monomial::isMember(n[0][0].getKind() == Kind::TO_REAL ? n[0][0][0]
715 : : : n[0][0]));
716 : :
717 : 1193410 : TNode left = pleft.getNode();
718 : 1193410 : DeltaRational right = cmp.normalizedDeltaRational();
719 : :
720 : 1193410 : const ArithVariables& avariables = d_database->getArithVariables();
721 : :
722 [ + - ]: 1193410 : Trace("Constraint::sanityChecking") << cmp.getNode() << endl;
723 [ + - ]: 1193410 : Trace("Constraint::sanityChecking") << k << endl;
724 [ + - ]: 1193410 : Trace("Constraint::sanityChecking") << pleft.getNode() << endl;
725 [ + - ]: 1193410 : Trace("Constraint::sanityChecking") << left << endl;
726 [ + - ]: 1193410 : Trace("Constraint::sanityChecking") << right << endl;
727 [ + - ]: 1193410 : Trace("Constraint::sanityChecking") << getValue() << endl;
728 [ + - ][ - + ]: 1193410 : Trace("Constraint::sanityChecking") << avariables.hasArithVar(left) << endl;
[ - - ]
729 [ + - ][ - + ]: 1193410 : Trace("Constraint::sanityChecking") << avariables.asArithVar(left) << endl;
[ - - ]
730 [ + - ]: 1193410 : Trace("Constraint::sanityChecking") << getVariable() << endl;
731 : :
732 [ + - ][ - - ]: 1193410 : if (avariables.hasArithVar(left)
733 [ + - ][ + - ]: 1193410 : && avariables.asArithVar(left) == getVariable() && getValue() == right)
[ + - ][ + - ]
[ + - ][ - - ]
734 : : {
735 [ + + ][ + - ]: 1193410 : switch (getType())
736 : : {
737 : 647892 : case LowerBound:
738 : : case UpperBound:
739 : : // Be overapproximate
740 [ + + ][ - + ]: 647892 : return k == Kind::GT || k == Kind::GEQ || k == Kind::LT
741 [ + - ][ - - ]: 1295784 : || k == Kind::LEQ;
742 : 272759 : case Equality: return k == Kind::EQUAL;
743 : 272759 : case Disequality: return k == Kind::DISTINCT;
744 : 0 : default: Unreachable();
745 : : }
746 : : }
747 : : else
748 : : {
749 : 0 : return false;
750 : : }
751 : 1193410 : }
752 : :
753 : 0 : ConstraintCP ConstraintDatabase::getAntecedent(AntecedentId p) const
754 : : {
755 : 0 : Assert(p < d_antecedents.size());
756 : 0 : return d_antecedents[p];
757 : : }
758 : :
759 : 0 : void ConstraintRule::print(std::ostream& out, bool produceProofs) const
760 : : {
761 [ - - ]: 0 : RationalVectorCP coeffs = produceProofs ? d_farkasCoefficients : nullptr;
762 : 0 : out << "{ConstraintRule, ";
763 : 0 : out << d_constraint << std::endl;
764 : 0 : out << "d_proofType= " << d_proofType << ", " << std::endl;
765 : 0 : out << "d_antecedentEnd= " << d_antecedentEnd << std::endl;
766 : :
767 [ - - ][ - - ]: 0 : if (d_constraint != NullConstraint && d_antecedentEnd != AntecedentIdSentinel)
768 : : {
769 : 0 : const ConstraintDatabase& database = d_constraint->getDatabase();
770 : :
771 : : size_t coeffIterator =
772 [ - - ]: 0 : (coeffs != RationalVectorCPSentinel) ? coeffs->size() - 1 : 0;
773 : 0 : AntecedentId p = d_antecedentEnd;
774 : : // must have at least one antecedent
775 : 0 : ConstraintCP antecedent = database.getAntecedent(p);
776 [ - - ]: 0 : while (antecedent != NullConstraint)
777 : : {
778 [ - - ]: 0 : if (coeffs != RationalVectorCPSentinel)
779 : : {
780 : 0 : out << coeffs->at(coeffIterator);
781 : : }
782 : : else
783 : : {
784 : 0 : out << "_";
785 : : }
786 : 0 : out << " * (" << *antecedent << ")" << std::endl;
787 : :
788 : 0 : Assert((coeffs == RationalVectorCPSentinel) || coeffIterator > 0);
789 : 0 : --p;
790 : 0 : coeffIterator =
791 [ - - ]: 0 : (coeffs != RationalVectorCPSentinel) ? coeffIterator - 1 : 0;
792 : 0 : antecedent = database.getAntecedent(p);
793 : : }
794 [ - - ]: 0 : if (coeffs != RationalVectorCPSentinel)
795 : : {
796 : 0 : out << coeffs->front();
797 : : }
798 : : else
799 : : {
800 : 0 : out << "_";
801 : : }
802 : 0 : out << " * (" << *(d_constraint->getNegation()) << ")";
803 : 0 : out << " [not d_constraint] " << endl;
804 : : }
805 : 0 : out << "}";
806 : 0 : }
807 : :
808 : 3787921 : bool Constraint::wellFormedFarkasProof(NodeManager* nm) const
809 : : {
810 [ - + ][ - + ]: 3787921 : Assert(hasProof());
[ - - ]
811 : :
812 : 3787921 : const ConstraintRule& cr = getConstraintRule();
813 [ - + ]: 3787921 : if (cr.d_constraint != this)
814 : : {
815 : 0 : return false;
816 : : }
817 [ - + ]: 3787921 : if (cr.d_proofType != FarkasAP)
818 : : {
819 : 0 : return false;
820 : : }
821 : :
822 : 3787921 : AntecedentId p = cr.d_antecedentEnd;
823 : :
824 : : // must have at least one antecedent
825 : 3787921 : ConstraintCP antecedent = d_database->d_antecedents[p];
826 [ - + ]: 3787921 : if (antecedent == NullConstraint)
827 : : {
828 : 0 : return false;
829 : : }
830 : :
831 [ + + ]: 3787921 : if (!d_produceProofs)
832 : : {
833 : 1180937 : return cr.d_farkasCoefficients == RationalVectorCPSentinel;
834 : : }
835 [ - + ][ - + ]: 2606984 : Assert(d_produceProofs);
[ - - ]
836 : :
837 [ - + ]: 2606984 : if (cr.d_farkasCoefficients == RationalVectorCPSentinel)
838 : : {
839 : 0 : return false;
840 : : }
841 [ - + ]: 2606984 : if (cr.d_farkasCoefficients->size() < 2)
842 : : {
843 : 0 : return false;
844 : : }
845 : :
846 : 2606984 : const ArithVariables& vars = d_database->getArithVariables();
847 : :
848 : 2606984 : DeltaRational rhs(0);
849 : 2606984 : Node lhs = Polynomial::mkZero(nm).getNode();
850 : :
851 : : RationalVector::const_iterator coeffIterator =
852 : 2606984 : cr.d_farkasCoefficients->end() - 1;
853 : 2606984 : RationalVector::const_iterator coeffBegin = cr.d_farkasCoefficients->begin();
854 : :
855 [ + + ]: 6123222 : while (antecedent != NullConstraint)
856 : : {
857 : 3516238 : Assert(lhs.isNull() || Polynomial::isMember(lhs));
858 : :
859 : 3516238 : const Rational& coeff = *coeffIterator;
860 : 3516238 : int coeffSgn = coeff.sgn();
861 : :
862 : 3516238 : rhs += antecedent->getValue() * coeff;
863 : :
864 : 3516238 : ArithVar antVar = antecedent->getVariable();
865 [ + - ][ + - ]: 3516238 : if (!lhs.isNull() && vars.hasNode(antVar))
[ + - ]
866 : : {
867 : 3516238 : Node antAsNode = vars.asNode(antVar);
868 [ + - ]: 3516238 : if (Polynomial::isMember(antAsNode))
869 : : {
870 : 3516238 : Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
871 : 3516238 : Polynomial antPoly = Polynomial::parsePolynomial(antAsNode);
872 : 3516238 : Polynomial sum = lhsPoly + (antPoly * coeff);
873 : 3516238 : lhs = sum.getNode();
874 : 3516238 : }
875 : : else
876 : : {
877 : 0 : lhs = Node::null();
878 : : }
879 : 3516238 : }
880 : : else
881 : : {
882 : 0 : lhs = Node::null();
883 : : }
884 [ + - ]: 7032476 : Trace("constraints::wffp")
885 : 3516238 : << "running sum: " << lhs << " <= " << rhs << endl;
886 : :
887 [ + + ][ + - ]: 3516238 : switch (antecedent->getType())
888 : : {
889 : 1335036 : case LowerBound:
890 : : // fc[l] < 0, therefore return false if coeffSgn >= 0
891 [ - + ]: 1335036 : if (coeffSgn >= 0)
892 : : {
893 : 0 : return false;
894 : : }
895 : 1335036 : break;
896 : 535869 : case UpperBound:
897 : : // fc[u] > 0, therefore return false if coeffSgn <= 0
898 [ - + ]: 535869 : if (coeffSgn <= 0)
899 : : {
900 : 0 : return false;
901 : : }
902 : 535869 : break;
903 : 1645333 : case Equality:
904 [ - + ]: 1645333 : if (coeffSgn == 0)
905 : : {
906 : 0 : return false;
907 : : }
908 : 1645333 : break;
909 : 0 : case Disequality:
910 : 0 : default: return false;
911 : : }
912 : :
913 [ - + ]: 3516238 : if (coeffIterator == coeffBegin)
914 : : {
915 : 0 : return false;
916 : : }
917 : 3516238 : --coeffIterator;
918 : 3516238 : --p;
919 : 3516238 : antecedent = d_database->d_antecedents[p];
920 : : }
921 [ - + ]: 2606984 : if (coeffIterator != coeffBegin)
922 : : {
923 : 0 : return false;
924 : : }
925 : :
926 : 2606984 : const Rational& firstCoeff = (*coeffBegin);
927 : 2606984 : int firstCoeffSgn = firstCoeff.sgn();
928 : 2606984 : rhs += (getNegation()->getValue()) * firstCoeff;
929 [ + - ][ + - ]: 2606984 : if (!lhs.isNull() && vars.hasNode(getVariable()))
[ + - ]
930 : : {
931 : 2606984 : Node firstAsNode = vars.asNode(getVariable());
932 [ + - ]: 2606984 : if (Polynomial::isMember(firstAsNode))
933 : : {
934 : 2606984 : Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
935 : 2606984 : Polynomial firstPoly = Polynomial::parsePolynomial(firstAsNode);
936 : 2606984 : Polynomial sum = lhsPoly + (firstPoly * firstCoeff);
937 : 2606984 : lhs = sum.getNode();
938 : 2606984 : }
939 : : else
940 : : {
941 : 0 : lhs = Node::null();
942 : : }
943 : 2606984 : }
944 : : else
945 : : {
946 : 0 : lhs = Node::null();
947 : : }
948 : :
949 [ + + ][ + - ]: 2606984 : switch (getNegation()->getType())
950 : : {
951 : 603076 : case LowerBound:
952 : : // fc[l] < 0, therefore return false if coeffSgn >= 0
953 [ - + ]: 603076 : if (firstCoeffSgn >= 0)
954 : : {
955 : 0 : return false;
956 : : }
957 : 603076 : break;
958 : 1050878 : case UpperBound:
959 : : // fc[u] > 0, therefore return false if coeffSgn <= 0
960 [ - + ]: 1050878 : if (firstCoeffSgn <= 0)
961 : : {
962 : 0 : return false;
963 : : }
964 : 1050878 : break;
965 : 953030 : case Equality:
966 [ - + ]: 953030 : if (firstCoeffSgn == 0)
967 : : {
968 : 0 : return false;
969 : : }
970 : 953030 : break;
971 : 0 : case Disequality:
972 : 0 : default: return false;
973 : : }
974 [ + - ]: 2606984 : Trace("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl;
975 : : // 0 = lhs <= rhs < 0
976 : 5213968 : return (lhs.isNull() || (Constant::isMember(lhs) && Constant(lhs).isZero()))
977 [ + - ][ + - ]: 5213968 : && rhs.sgn() < 0;
[ + - ]
978 : 2606984 : }
979 : :
980 : 155664 : ConstraintP Constraint::makeNegation(ArithVar v,
981 : : ConstraintType t,
982 : : const DeltaRational& r,
983 : : bool produceProofs)
984 : : {
985 [ + + ][ + - ]: 155664 : switch (t)
[ - ]
986 : : {
987 : 6518 : case LowerBound:
988 : : {
989 [ - + ][ - + ]: 6518 : Assert(r.infinitesimalSgn() >= 0);
[ - - ]
990 [ - + ]: 6518 : if (r.infinitesimalSgn() > 0)
991 : : {
992 : 0 : Assert(r.getInfinitesimalPart() == 1);
993 : : // make (not (v > r)), which is (v <= r)
994 : 0 : DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
995 : 0 : return new Constraint(v, UpperBound, dropInf, produceProofs);
996 : 0 : }
997 : : else
998 : : {
999 [ - + ][ - + ]: 6518 : Assert(r.infinitesimalSgn() == 0);
[ - - ]
1000 : : // make (not (v >= r)), which is (v < r)
1001 : 6518 : DeltaRational addInf(r.getNoninfinitesimalPart(), -1);
1002 : 6518 : return new Constraint(v, UpperBound, addInf, produceProofs);
1003 : 6518 : }
1004 : : }
1005 : 140909 : case UpperBound:
1006 : : {
1007 [ - + ][ - + ]: 140909 : Assert(r.infinitesimalSgn() <= 0);
[ - - ]
1008 [ - + ]: 140909 : if (r.infinitesimalSgn() < 0)
1009 : : {
1010 : 0 : Assert(r.getInfinitesimalPart() == -1);
1011 : : // make (not (v < r)), which is (v >= r)
1012 : 0 : DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
1013 : 0 : return new Constraint(v, LowerBound, dropInf, produceProofs);
1014 : 0 : }
1015 : : else
1016 : : {
1017 [ - + ][ - + ]: 140909 : Assert(r.infinitesimalSgn() == 0);
[ - - ]
1018 : : // make (not (v <= r)), which is (v > r)
1019 : 140909 : DeltaRational addInf(r.getNoninfinitesimalPart(), 1);
1020 : 140909 : return new Constraint(v, LowerBound, addInf, produceProofs);
1021 : 140909 : }
1022 : : }
1023 : 8237 : case Equality: return new Constraint(v, Disequality, r, produceProofs);
1024 : 0 : case Disequality: return new Constraint(v, Equality, r, produceProofs);
1025 : 0 : default: Unreachable(); return NullConstraint;
1026 : : }
1027 : : }
1028 : :
1029 : 51016 : ConstraintDatabase::ConstraintDatabase(Env& env,
1030 : : const ArithVariables& avars,
1031 : : ArithCongruenceManager& cm,
1032 : : RaiseConflict raiseConflict,
1033 : 51016 : EagerProofGenerator* pfGen)
1034 : : : EnvObj(env),
1035 : 51016 : d_varDatabases(),
1036 : 51016 : d_toPropagate(context()),
1037 : 51016 : d_antecedents(context(), false),
1038 : 51016 : d_watches(new Watches(context(), userContext())),
1039 : 51016 : d_avariables(avars),
1040 : 51016 : d_congruenceManager(cm),
1041 : 51016 : d_pfGen(pfGen),
1042 [ + + ]: 51016 : d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
1043 : : : nullptr),
1044 : 51016 : d_raiseConflict(raiseConflict),
1045 : 51016 : d_one(1),
1046 : 51016 : d_negOne(-1),
1047 : 102032 : d_statistics(statisticsRegistry())
1048 : : {
1049 : 51016 : }
1050 : :
1051 : 14061474 : SortedConstraintMap& ConstraintDatabase::getVariableSCM(ArithVar v) const
1052 : : {
1053 [ - + ][ - + ]: 14061474 : Assert(variableDatabaseIsSetup(v));
[ - - ]
1054 : 14061474 : return d_varDatabases[v]->d_constraints;
1055 : : }
1056 : :
1057 : 73824 : void ConstraintDatabase::pushSplitWatch(ConstraintP c)
1058 : : {
1059 [ - + ][ - + ]: 73824 : Assert(!c->d_split);
[ - - ]
1060 : 73824 : c->d_split = true;
1061 : 73824 : d_watches->d_splitWatches.push_back(c);
1062 : 73824 : }
1063 : :
1064 : 1835830 : void ConstraintDatabase::pushCanBePropagatedWatch(ConstraintP c)
1065 : : {
1066 [ - + ][ - + ]: 1835830 : Assert(!c->d_canBePropagated);
[ - - ]
1067 : 1835830 : c->d_canBePropagated = true;
1068 : 1835830 : d_watches->d_canBePropagatedWatches.push_back(c);
1069 : 1835830 : }
1070 : :
1071 : 10799775 : void ConstraintDatabase::pushAssertionOrderWatch(ConstraintP c, TNode witness)
1072 : : {
1073 [ - + ][ - + ]: 10799775 : Assert(!c->assertedToTheTheory());
[ - - ]
1074 : 10799775 : c->d_assertionOrder = d_watches->d_assertionOrderWatches.size();
1075 : 10799775 : c->d_witness = witness;
1076 : 10799775 : d_watches->d_assertionOrderWatches.push_back(c);
1077 : 10799775 : }
1078 : :
1079 : 16560141 : void ConstraintDatabase::pushConstraintRule(const ConstraintRule& crp)
1080 : : {
1081 : 16560141 : ConstraintP c = crp.d_constraint;
1082 [ - + ][ - + ]: 16560141 : Assert(c->d_crid == ConstraintRuleIdSentinel);
[ - - ]
1083 [ - + ][ - + ]: 16560141 : Assert(!c->hasProof());
[ - - ]
1084 : 16560141 : c->d_crid = d_watches->d_constraintProofs.size();
1085 : 16560141 : d_watches->d_constraintProofs.push_back(crp);
1086 : 16560141 : }
1087 : :
1088 : 3334367 : ConstraintP ConstraintDatabase::getConstraint(ArithVar v,
1089 : : ConstraintType t,
1090 : : const DeltaRational& r)
1091 : : {
1092 : : // This must always return a constraint.
1093 : :
1094 : 3334367 : SortedConstraintMap& scm = getVariableSCM(v);
1095 : 3334367 : pair<SortedConstraintMapIterator, bool> insertAttempt;
1096 : 3334367 : insertAttempt = scm.insert(make_pair(r, ValueCollection()));
1097 : :
1098 : 3334367 : SortedConstraintMapIterator pos = insertAttempt.first;
1099 : 3334367 : ValueCollection& vc = pos->second;
1100 [ + + ]: 3334367 : if (vc.hasConstraintOfType(t))
1101 : : {
1102 : 3178703 : return vc.getConstraintOfType(t);
1103 : : }
1104 : : else
1105 : : {
1106 : 155664 : ConstraintP c = new Constraint(v, t, r, options().smt.produceProofs);
1107 : : ConstraintP negC =
1108 : 155664 : Constraint::makeNegation(v, t, r, options().smt.produceProofs);
1109 : :
1110 : 155664 : SortedConstraintMapIterator negPos;
1111 [ + + ][ - + ]: 155664 : if (t == Equality || t == Disequality)
1112 : : {
1113 : 8237 : negPos = pos;
1114 : : }
1115 : : else
1116 : : {
1117 : 147427 : pair<SortedConstraintMapIterator, bool> negInsertAttempt;
1118 : : negInsertAttempt =
1119 : 147427 : scm.insert(make_pair(negC->getValue(), ValueCollection()));
1120 [ - + ][ - - ]: 147427 : Assert(negInsertAttempt.second
[ - + ][ - + ]
[ - - ]
1121 : : || !negInsertAttempt.first->second.hasConstraintOfType(
1122 : : negC->getType()));
1123 : 147427 : negPos = negInsertAttempt.first;
1124 : : }
1125 : :
1126 : 155664 : c->initialize(this, pos, negC);
1127 : 155664 : negC->initialize(this, negPos, c);
1128 : :
1129 : 155664 : vc.add(c);
1130 : 155664 : negPos->second.add(negC);
1131 : :
1132 : 155664 : return c;
1133 : : }
1134 : : }
1135 : :
1136 : 434292 : ConstraintP ConstraintDatabase::ensureConstraint(ValueCollection& vc,
1137 : : ConstraintType t)
1138 : : {
1139 [ + + ]: 434292 : if (vc.hasConstraintOfType(t))
1140 : : {
1141 : 418507 : return vc.getConstraintOfType(t);
1142 : : }
1143 : : else
1144 : : {
1145 : 15785 : return getConstraint(vc.getVariable(), t, vc.getValue());
1146 : : }
1147 : : }
1148 : :
1149 : 0 : bool ConstraintDatabase::emptyDatabase(
1150 : : const std::vector<PerVariableDatabase>& vec)
1151 : : {
1152 : 0 : std::vector<PerVariableDatabase>::const_iterator first = vec.begin();
1153 : 0 : std::vector<PerVariableDatabase>::const_iterator last = vec.end();
1154 : 0 : return std::find_if(first, last, PerVariableDatabase::IsEmpty) == last;
1155 : : }
1156 : :
1157 : 152004 : ConstraintDatabase::~ConstraintDatabase()
1158 : : {
1159 [ + - ]: 50668 : delete d_watches;
1160 : :
1161 : 50668 : std::vector<ConstraintP> constraintList;
1162 : :
1163 [ + + ]: 414937 : while (!d_varDatabases.empty())
1164 : : {
1165 : 364269 : PerVariableDatabase* back = d_varDatabases.back();
1166 : :
1167 : 364269 : SortedConstraintMap& scm = back->d_constraints;
1168 : 364269 : SortedConstraintMapIterator i = scm.begin(), i_end = scm.end();
1169 [ + + ]: 1385354 : for (; i != i_end; ++i)
1170 : : {
1171 : 1021085 : (i->second).push_into(constraintList);
1172 : : }
1173 [ + + ]: 1861551 : while (!constraintList.empty())
1174 : : {
1175 : 1497282 : ConstraintP c = constraintList.back();
1176 : 1497282 : constraintList.pop_back();
1177 [ + - ]: 1497282 : delete c;
1178 : : }
1179 [ - + ][ - + ]: 364269 : Assert(scm.empty());
1180 : 364269 : d_varDatabases.pop_back();
1181 [ + - ]: 364269 : delete back;
1182 : : }
1183 : :
1184 [ - + ][ - + ]: 50668 : Assert(d_nodetoConstraintMap.empty());
1185 : 50668 : }
1186 : :
1187 : 51016 : ConstraintDatabase::Statistics::Statistics(StatisticsRegistry& sr)
1188 : : : d_unatePropagateCalls(
1189 : 51016 : sr.registerInt("theory::arith::cd::unatePropagateCalls")),
1190 : : d_unatePropagateImplications(
1191 : 51016 : sr.registerInt("theory::arith::cd::unatePropagateImplications"))
1192 : : {
1193 : 51016 : }
1194 : :
1195 : 0 : void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c)
1196 : : {
1197 : 0 : Assert(c->safeToGarbageCollect());
1198 : 0 : ConstraintP neg = c->getNegation();
1199 : 0 : Assert(neg->safeToGarbageCollect());
1200 [ - - ]: 0 : delete c;
1201 [ - - ]: 0 : delete neg;
1202 : 0 : }
1203 : :
1204 : 368575 : void ConstraintDatabase::addVariable(ArithVar v)
1205 : : {
1206 [ + + ]: 368575 : if (d_reclaimable.isMember(v))
1207 : : {
1208 : 4078 : SortedConstraintMap& scm = getVariableSCM(v);
1209 : :
1210 : 4078 : std::vector<ConstraintP> constraintList;
1211 : :
1212 [ - + ]: 4078 : for (SortedConstraintMapIterator i = scm.begin(), end = scm.end(); i != end;
1213 : 0 : ++i)
1214 : : {
1215 : 0 : (i->second).push_into(constraintList);
1216 : : }
1217 [ - + ]: 4078 : while (!constraintList.empty())
1218 : : {
1219 : 0 : ConstraintP c = constraintList.back();
1220 : 0 : constraintList.pop_back();
1221 : 0 : Assert(c->safeToGarbageCollect());
1222 [ - - ]: 0 : delete c;
1223 : : }
1224 [ - + ][ - + ]: 4078 : Assert(scm.empty());
[ - - ]
1225 : :
1226 : 4078 : d_reclaimable.remove(v);
1227 : 4078 : }
1228 : : else
1229 : : {
1230 [ + - ]: 728994 : Trace("arith::constraint")
1231 : 364497 : << "about to fail" << v << " " << d_varDatabases.size() << endl;
1232 [ - + ][ - + ]: 364497 : Assert(v == d_varDatabases.size());
[ - - ]
1233 : 364497 : d_varDatabases.push_back(new PerVariableDatabase(v));
1234 : : }
1235 : 368575 : }
1236 : :
1237 : 4096 : void ConstraintDatabase::removeVariable(ArithVar v)
1238 : : {
1239 [ - + ][ - + ]: 4096 : Assert(!d_reclaimable.isMember(v));
[ - - ]
1240 : 4096 : d_reclaimable.add(v);
1241 : 4096 : }
1242 : :
1243 : 0 : bool Constraint::safeToGarbageCollect() const
1244 : : {
1245 : : // Do not call during destructor as getNegation() may be Null by this point
1246 : 0 : Assert(getNegation() != NullConstraint);
1247 : 0 : return !contextDependentDataIsSet()
1248 [ - - ][ - - ]: 0 : && !getNegation()->contextDependentDataIsSet();
1249 : : }
1250 : :
1251 : 1500556 : bool Constraint::contextDependentDataIsSet() const
1252 : : {
1253 [ + - ][ + - ]: 1500556 : return hasProof() || isSplit() || canBePropagated() || assertedToTheTheory();
[ + - ][ - + ]
1254 : : }
1255 : :
1256 : 36912 : TrustNode Constraint::split()
1257 : : {
1258 [ + + ][ + - ]: 36912 : Assert(isEquality() || isDisequality());
[ - + ][ - + ]
[ - - ]
1259 : :
1260 : 36912 : bool isEq = isEquality();
1261 : :
1262 [ + + ]: 36912 : ConstraintP eq = isEq ? this : d_negation;
1263 [ + + ]: 36912 : ConstraintP diseq = isEq ? d_negation : this;
1264 : :
1265 : 36912 : TNode eqNode = eq->getLiteral();
1266 [ - + ][ - + ]: 36912 : Assert(eqNode.getKind() == Kind::EQUAL);
[ - - ]
1267 : 36912 : TNode lhs = eqNode[0];
1268 : 36912 : TNode rhs = eqNode[1];
1269 : :
1270 : 36912 : NodeManager* nm = d_database->nodeManager();
1271 : 73824 : Node leqNode = NodeBuilder(nm, Kind::LEQ) << lhs << rhs;
1272 : 73824 : Node ltNode = NodeBuilder(nm, Kind::LT) << lhs << rhs;
1273 : 73824 : Node gtNode = NodeBuilder(nm, Kind::GT) << lhs << rhs;
1274 : 73824 : Node geqNode = NodeBuilder(nm, Kind::GEQ) << lhs << rhs;
1275 : :
1276 : 73824 : Node lemma = NodeBuilder(nm, Kind::OR) << leqNode << geqNode;
1277 : :
1278 : 36912 : TrustNode trustedLemma;
1279 [ + + ]: 36912 : if (d_database->isProofEnabled())
1280 : : {
1281 : 13415 : TypeNode type = lhs.getType();
1282 : : // Farkas proof that this works.
1283 : 13415 : auto nLeqPf = d_database->d_pnm->mkAssume(leqNode.negate());
1284 : 13415 : auto gtPf = ensurePredTransform(d_database->d_pnm, nLeqPf, gtNode);
1285 : 13415 : auto nGeqPf = d_database->d_pnm->mkAssume(geqNode.negate());
1286 : 13415 : auto ltPf = ensurePredTransform(d_database->d_pnm, nGeqPf, ltNode);
1287 : 53660 : std::vector<Pf> args{gtPf, ltPf};
1288 : 67075 : std::vector<Node> coeffs{nm->mkConstReal(-1), nm->mkConstReal(1)};
1289 : 13415 : std::vector<Node> coeffsUse = getMacroSumUbCoeff(nm, args, coeffs);
1290 : 13415 : auto sumPf = d_database->d_pnm->mkNode(
1291 : 13415 : ProofRule::MACRO_ARITH_SCALE_SUM_UB, args, coeffsUse);
1292 : : auto botPf =
1293 : 13415 : ensurePredTransform(d_database->d_pnm, sumPf, nm->mkConst(false));
1294 : 53660 : std::vector<Node> a = {leqNode.negate(), geqNode.negate()};
1295 : 26830 : auto notAndNotPf = d_database->d_pnm->mkScope(botPf, a);
1296 : : // No need to ensure that the expected node aggrees with `a` because we are
1297 : : // not providing an expected node.
1298 : : auto orNotNotPf =
1299 : 53660 : d_database->d_pnm->mkNode(ProofRule::NOT_AND, {notAndNotPf}, {});
1300 : 13415 : auto orPf = ensurePredTransform(d_database->d_pnm, orNotNotPf, lemma);
1301 : 13415 : trustedLemma = d_database->d_pfGen->mkTrustNode(lemma, orPf);
1302 : 13415 : }
1303 : : else
1304 : : {
1305 : 23497 : trustedLemma = TrustNode::mkTrustLemma(lemma);
1306 : : }
1307 : :
1308 : 36912 : eq->d_database->pushSplitWatch(eq);
1309 : 36912 : diseq->d_database->pushSplitWatch(diseq);
1310 : :
1311 : 73824 : return trustedLemma;
1312 : 36912 : }
1313 : :
1314 : 2386820 : bool ConstraintDatabase::hasLiteral(TNode literal) const
1315 : : {
1316 : 2386820 : return lookup(literal) != NullConstraint;
1317 : : }
1318 : :
1319 : 596705 : ConstraintP ConstraintDatabase::addLiteral(TNode literal)
1320 : : {
1321 [ - + ][ - + ]: 596705 : Assert(!hasLiteral(literal));
[ - - ]
1322 : 596705 : bool isNot = (literal.getKind() == Kind::NOT);
1323 [ - + ]: 596705 : Node atomNode = (isNot ? literal[0] : literal);
1324 : 596705 : Node negationNode = atomNode.notNode();
1325 : :
1326 [ - + ][ - + ]: 596705 : Assert(!hasLiteral(atomNode));
[ - - ]
1327 [ - + ][ - + ]: 596705 : Assert(!hasLiteral(negationNode));
[ - - ]
1328 : 596705 : Comparison posCmp = Comparison::parseNormalForm(atomNode);
1329 : :
1330 : 596705 : ConstraintType posType = Constraint::constraintTypeOfComparison(posCmp);
1331 : :
1332 : 596705 : Polynomial nvp = posCmp.normalizedVariablePart();
1333 : 596705 : ArithVar v = d_avariables.asArithVar(nvp.getNode());
1334 : :
1335 : 596705 : DeltaRational posDR = posCmp.normalizedDeltaRational();
1336 : :
1337 : : ConstraintP posC =
1338 : 596705 : new Constraint(v, posType, posDR, options().smt.produceProofs);
1339 : :
1340 [ + - ]: 1193410 : Trace("arith::constraint")
1341 : 596705 : << "addliteral( literal ->" << literal << ")" << endl;
1342 [ + - ]: 596705 : Trace("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl;
1343 : :
1344 : 596705 : SortedConstraintMap& scm = getVariableSCM(posC->getVariable());
1345 : 596705 : pair<SortedConstraintMapIterator, bool> insertAttempt;
1346 : 596705 : insertAttempt = scm.insert(make_pair(posC->getValue(), ValueCollection()));
1347 : :
1348 : 596705 : SortedConstraintMapIterator posI = insertAttempt.first;
1349 : : // If the attempt succeeds, i points to a new empty ValueCollection
1350 : : // If the attempt fails, i points to a pre-existing ValueCollection
1351 : :
1352 [ + + ]: 596705 : if (posI->second.hasConstraintOfType(posC->getType()))
1353 : : {
1354 : : // This is the situation where the ConstraintP exists, but
1355 : : // the literal has not been associated with it.
1356 : 3274 : ConstraintP hit = posI->second.getConstraintOfType(posC->getType());
1357 [ + - ]: 3274 : Trace("arith::constraint") << "hit " << hit << endl;
1358 [ + - ]: 3274 : Trace("arith::constraint") << "posC " << posC << endl;
1359 : :
1360 [ + - ]: 3274 : delete posC;
1361 : :
1362 : 3274 : hit->setLiteral(atomNode);
1363 : 3274 : hit->getNegation()->setLiteral(negationNode);
1364 [ - + ]: 3274 : return isNot ? hit->getNegation() : hit;
1365 : : }
1366 : : else
1367 : : {
1368 : 593431 : Comparison negCmp = Comparison::parseNormalForm(negationNode);
1369 : :
1370 : 593431 : ConstraintType negType = Constraint::constraintTypeOfComparison(negCmp);
1371 : 593431 : DeltaRational negDR = negCmp.normalizedDeltaRational();
1372 : :
1373 : : ConstraintP negC =
1374 : 593431 : new Constraint(v, negType, negDR, options().smt.produceProofs);
1375 : :
1376 : 593431 : SortedConstraintMapIterator negI;
1377 : :
1378 [ + + ]: 593431 : if (posC->isEquality())
1379 : : {
1380 : 272268 : negI = posI;
1381 : : }
1382 : : else
1383 : : {
1384 [ + + ][ + - ]: 321163 : Assert(posC->isLowerBound() || posC->isUpperBound());
[ - + ][ - + ]
[ - - ]
1385 : :
1386 : 321163 : pair<SortedConstraintMapIterator, bool> negInsertAttempt;
1387 : : negInsertAttempt =
1388 : 321163 : scm.insert(make_pair(negC->getValue(), ValueCollection()));
1389 : :
1390 [ + - ]: 321163 : Trace("nf::tmp") << "sdhjfgdhjkldfgljkhdfg" << endl;
1391 [ + - ]: 321163 : Trace("nf::tmp") << negC << endl;
1392 [ + - ]: 321163 : Trace("nf::tmp") << negC->getValue() << endl;
1393 : :
1394 : : // This should always succeed as the DeltaRational for the negation is
1395 : : // unique!
1396 [ - + ][ - + ]: 321163 : Assert(negInsertAttempt.second);
[ - - ]
1397 : :
1398 : 321163 : negI = negInsertAttempt.first;
1399 : : }
1400 : :
1401 : 593431 : (posI->second).add(posC);
1402 : 593431 : (negI->second).add(negC);
1403 : :
1404 : 593431 : posC->initialize(this, posI, negC);
1405 : 593431 : negC->initialize(this, negI, posC);
1406 : :
1407 : 593431 : posC->setLiteral(atomNode);
1408 : 593431 : negC->setLiteral(negationNode);
1409 : :
1410 [ - + ]: 593431 : return isNot ? negC : posC;
1411 : 593431 : }
1412 : 596705 : }
1413 : :
1414 : 19588080 : ConstraintP ConstraintDatabase::lookup(TNode literal) const
1415 : : {
1416 : : NodetoConstraintMap::const_iterator iter =
1417 : 19588080 : d_nodetoConstraintMap.find(literal);
1418 [ + + ]: 19588080 : if (iter == d_nodetoConstraintMap.end())
1419 : : {
1420 : 4187979 : return NullConstraint;
1421 : : }
1422 : : else
1423 : : {
1424 : 15400101 : return iter->second;
1425 : : }
1426 : : }
1427 : :
1428 : 9137585 : void Constraint::setAssumption(CVC5_UNUSED bool nowInConflict)
1429 : : {
1430 [ + - ]: 9137585 : Trace("constraints::pf") << "setAssumption(" << this << ")" << std::endl;
1431 [ - + ][ - + ]: 9137585 : Assert(!hasProof());
[ - - ]
1432 [ - + ][ - + ]: 9137585 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1433 [ - + ][ - + ]: 9137585 : Assert(hasLiteral());
[ - - ]
1434 [ - + ][ - + ]: 9137585 : Assert(assertedToTheTheory());
[ - - ]
1435 : :
1436 : 9137585 : d_database->pushConstraintRule(ConstraintRule(this, AssumeAP));
1437 : :
1438 [ - + ][ - + ]: 9137585 : Assert(inConflict() == nowInConflict);
[ - - ]
1439 : 9137585 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1440 : : {
1441 [ - - ]: 0 : Trace("constraint::conflictCommit")
1442 : 0 : << "inConflict@setAssumption " << this << std::endl;
1443 : : }
1444 : 9137585 : }
1445 : :
1446 : 6935679 : void Constraint::tryToPropagate()
1447 : : {
1448 [ - + ][ - + ]: 6935679 : Assert(hasProof());
[ - - ]
1449 [ - + ][ - + ]: 6935679 : Assert(!isAssumption());
[ - - ]
1450 [ - + ][ - + ]: 6935679 : Assert(!isInternalAssumption());
[ - - ]
1451 : :
1452 [ + - ][ + - ]: 8291850 : if (canBePropagated() && !assertedToTheTheory() && !isAssumption()
1453 [ + + ][ + - ]: 8291850 : && !isInternalAssumption())
[ + + ]
1454 : : {
1455 : 1356171 : propagate();
1456 : : }
1457 : 6935679 : }
1458 : :
1459 : 1389153 : void Constraint::propagate()
1460 : : {
1461 [ - + ][ - + ]: 1389153 : Assert(hasProof());
[ - - ]
1462 [ - + ][ - + ]: 1389153 : Assert(canBePropagated());
[ - - ]
1463 [ - + ][ - + ]: 1389153 : Assert(!assertedToTheTheory());
[ - - ]
1464 [ - + ][ - + ]: 1389153 : Assert(!isAssumption());
[ - - ]
1465 [ - + ][ - + ]: 1389153 : Assert(!isInternalAssumption());
[ - - ]
1466 : :
1467 : 1389153 : d_database->d_toPropagate.push(this);
1468 : 1389153 : }
1469 : :
1470 : : /*
1471 : : * Example:
1472 : : * x <= a and a < b
1473 : : * |= x <= b
1474 : : * ---
1475 : : * 1*(x <= a) + (-1)*(x > b) => (0 <= a-b)
1476 : : */
1477 : 3620125 : void Constraint::impliedByUnate(NodeManager* nm,
1478 : : ConstraintCP imp,
1479 : : CVC5_UNUSED bool nowInConflict)
1480 : : {
1481 [ + - ]: 7240250 : Trace("constraints::pf") << "impliedByUnate(" << this << ", " << *imp << ")"
1482 : 3620125 : << std::endl;
1483 [ - + ][ - + ]: 3620125 : Assert(!hasProof());
[ - - ]
1484 [ - + ][ - + ]: 3620125 : Assert(imp->hasProof());
[ - - ]
1485 [ - + ][ - + ]: 3620125 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1486 : :
1487 : 3620125 : d_database->d_antecedents.push_back(NullConstraint);
1488 : 3620125 : d_database->d_antecedents.push_back(imp);
1489 : :
1490 : 3620125 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1491 : :
1492 : : RationalVectorP coeffs;
1493 [ + + ]: 3620125 : if (d_produceProofs)
1494 : : {
1495 : 2490847 : std::pair<int, int> sgns = unateFarkasSigns(getNegation(), imp);
1496 : :
1497 : 2490847 : Rational first(sgns.first);
1498 : 2490847 : Rational second(sgns.second);
1499 : :
1500 : 2490847 : coeffs = new RationalVector();
1501 : 2490847 : coeffs->push_back(first);
1502 : 2490847 : coeffs->push_back(second);
1503 : 2490847 : }
1504 : : else
1505 : : {
1506 : 1129278 : coeffs = RationalVectorPSentinel;
1507 : : }
1508 : : // no need to delete coeffs the memory is owned by ConstraintRule
1509 : 3620125 : d_database->pushConstraintRule(
1510 : 3620125 : ConstraintRule(this, FarkasAP, antecedentEnd, coeffs));
1511 : :
1512 [ - + ][ - + ]: 3620125 : Assert(inConflict() == nowInConflict);
[ - - ]
1513 : 3620125 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1514 : : {
1515 [ - - ]: 0 : Trace("constraint::conflictCommit")
1516 : 0 : << "inConflict@impliedByUnate " << this << std::endl;
1517 : : }
1518 : :
1519 : 3620125 : if (TraceIsOn("constraints::wffp") && !wellFormedFarkasProof(nm))
1520 : : {
1521 [ - - ]: 0 : getConstraintRule().print(Trace("constraints::wffp"), d_produceProofs);
1522 : : }
1523 [ - + ][ - + ]: 3620125 : Assert(wellFormedFarkasProof(nm));
[ - - ]
1524 : 3620125 : }
1525 : :
1526 : 982702 : void Constraint::impliedByTrichotomy(ConstraintCP a,
1527 : : ConstraintCP b,
1528 : : CVC5_UNUSED bool nowInConflict)
1529 : : {
1530 [ + - ]: 1965404 : Trace("constraints::pf") << "impliedByTrichotomy(" << this << ", " << *a
1531 : 982702 : << ", ";
1532 [ + - ]: 982702 : Trace("constraints::pf") << *b << ")" << std::endl;
1533 [ - + ][ - + ]: 982702 : Assert(!hasProof());
[ - - ]
1534 [ - + ][ - + ]: 982702 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1535 [ - + ][ - + ]: 982702 : Assert(a->hasProof());
[ - - ]
1536 [ - + ][ - + ]: 982702 : Assert(b->hasProof());
[ - - ]
1537 : :
1538 : 982702 : d_database->d_antecedents.push_back(NullConstraint);
1539 : 982702 : d_database->d_antecedents.push_back(a);
1540 : 982702 : d_database->d_antecedents.push_back(b);
1541 : :
1542 : 982702 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1543 : 982702 : d_database->pushConstraintRule(
1544 : 982702 : ConstraintRule(this, TrichotomyAP, antecedentEnd));
1545 : :
1546 [ - + ][ - + ]: 982702 : Assert(inConflict() == nowInConflict);
[ - - ]
1547 : 982702 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1548 : : {
1549 [ - - ]: 0 : Trace("constraint::conflictCommit")
1550 : 0 : << "inConflict@impliedByTrichotomy " << this << std::endl;
1551 : : }
1552 : 982702 : }
1553 : :
1554 : 167796 : bool Constraint::allHaveProof(const ConstraintCPVec& b)
1555 : : {
1556 : 167796 : for (ConstraintCPVec::const_iterator i = b.begin(), i_end = b.end();
1557 [ + + ]: 2016934 : i != i_end;
1558 : 1849138 : ++i)
1559 : : {
1560 : 1849138 : ConstraintCP cp = *i;
1561 [ - + ]: 1849138 : if (!(cp->hasProof()))
1562 : : {
1563 : 0 : return false;
1564 : : }
1565 : : }
1566 : 167796 : return true;
1567 : : }
1568 : :
1569 : 2279169 : void Constraint::impliedByIntTighten(ConstraintCP a,
1570 : : CVC5_UNUSED bool nowInConflict)
1571 : : {
1572 [ + - ]: 4558338 : Trace("constraints::pf") << "impliedByIntTighten(" << this << ", " << *a
1573 : 2279169 : << ")" << std::endl;
1574 [ - + ][ - + ]: 2279169 : Assert(!hasProof());
[ - - ]
1575 [ - + ][ - + ]: 2279169 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1576 [ - + ][ - + ]: 2279169 : Assert(a->hasProof());
[ - - ]
1577 [ + - ]: 4558338 : Trace("pf::arith") << "impliedByIntTighten(" << this << ", " << a << ")"
1578 : 2279169 : << std::endl;
1579 : :
1580 : 2279169 : d_database->d_antecedents.push_back(NullConstraint);
1581 : 2279169 : d_database->d_antecedents.push_back(a);
1582 : 2279169 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1583 : 2279169 : d_database->pushConstraintRule(
1584 : 2279169 : ConstraintRule(this, IntTightenAP, antecedentEnd));
1585 : :
1586 [ - + ][ - + ]: 2279169 : Assert(inConflict() == nowInConflict);
[ - - ]
1587 [ + + ]: 2279169 : if (inConflict())
1588 : : {
1589 [ + - ]: 7188 : Trace("constraint::conflictCommit")
1590 : 3594 : << "inConflict impliedByIntTighten" << this << std::endl;
1591 : : }
1592 : 2279169 : }
1593 : :
1594 : 0 : void Constraint::impliedByIntHole(ConstraintCP a,
1595 : : CVC5_UNUSED bool nowInConflict)
1596 : : {
1597 [ - - ]: 0 : Trace("constraints::pf") << "impliedByIntHole(" << this << ", " << *a << ")"
1598 : 0 : << std::endl;
1599 : 0 : Assert(!hasProof());
1600 : 0 : Assert(negationHasProof() == nowInConflict);
1601 : 0 : Assert(a->hasProof());
1602 [ - - ]: 0 : Trace("pf::arith") << "impliedByIntHole(" << this << ", " << a << ")"
1603 : 0 : << std::endl;
1604 : :
1605 : 0 : d_database->d_antecedents.push_back(NullConstraint);
1606 : 0 : d_database->d_antecedents.push_back(a);
1607 : 0 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1608 : 0 : d_database->pushConstraintRule(
1609 : 0 : ConstraintRule(this, IntHoleAP, antecedentEnd));
1610 : :
1611 : 0 : Assert(inConflict() == nowInConflict);
1612 : 0 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1613 : : {
1614 [ - - ]: 0 : Trace("constraint::conflictCommit")
1615 : 0 : << "inConflict impliedByIntHole" << this << std::endl;
1616 : : }
1617 : 0 : }
1618 : :
1619 : 0 : void Constraint::impliedByIntHole(const ConstraintCPVec& b,
1620 : : CVC5_UNUSED bool nowInConflict)
1621 : : {
1622 [ - - ]: 0 : Trace("constraints::pf") << "impliedByIntHole(" << this;
1623 [ - - ]: 0 : if (TraceIsOn("constraints::pf"))
1624 : : {
1625 [ - - ]: 0 : for (const ConstraintCP& p : b)
1626 : : {
1627 [ - - ]: 0 : Trace("constraints::pf") << ", " << p;
1628 : : }
1629 : : }
1630 [ - - ]: 0 : Trace("constraints::pf") << ")" << std::endl;
1631 : :
1632 : 0 : Assert(!hasProof());
1633 : 0 : Assert(negationHasProof() == nowInConflict);
1634 : 0 : Assert(allHaveProof(b));
1635 : :
1636 : 0 : CDConstraintList& antecedents = d_database->d_antecedents;
1637 : 0 : antecedents.push_back(NullConstraint);
1638 : 0 : for (ConstraintCPVec::const_iterator i = b.begin(), i_end = b.end();
1639 [ - - ]: 0 : i != i_end;
1640 : 0 : ++i)
1641 : : {
1642 : 0 : antecedents.push_back(*i);
1643 : : }
1644 : 0 : AntecedentId antecedentEnd = antecedents.size() - 1;
1645 : :
1646 : 0 : d_database->pushConstraintRule(
1647 : 0 : ConstraintRule(this, IntHoleAP, antecedentEnd));
1648 : :
1649 : 0 : Assert(inConflict() == nowInConflict);
1650 : 0 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1651 : : {
1652 [ - - ]: 0 : Trace("constraint::conflictCommit")
1653 : 0 : << "inConflict@impliedByIntHole[vec] " << this << std::endl;
1654 : : }
1655 : 0 : }
1656 : :
1657 : : /*
1658 : : * If proofs are off, coeffs == RationalVectorSentinal.
1659 : : * If proofs are on,
1660 : : * coeffs != RationalVectorSentinal,
1661 : : * coeffs->size() = a.size() + 1,
1662 : : * for i in [0,a.size) : coeff[i] corresponds to a[i], and
1663 : : * coeff.back() corresponds to the current constraint.
1664 : : */
1665 : 167796 : void Constraint::impliedByFarkas(NodeManager* nm,
1666 : : const ConstraintCPVec& a,
1667 : : RationalVectorCP coeffs,
1668 : : CVC5_UNUSED bool nowInConflict)
1669 : : {
1670 [ + - ]: 167796 : Trace("constraints::pf") << "impliedByFarkas(" << this;
1671 [ - + ]: 167796 : if (TraceIsOn("constraints::pf"))
1672 : : {
1673 [ - - ]: 0 : for (const ConstraintCP& p : a)
1674 : : {
1675 [ - - ]: 0 : Trace("constraints::pf") << ", " << p;
1676 : : }
1677 : : }
1678 [ + - ]: 167796 : Trace("constraints::pf") << ", <coeffs>";
1679 [ + - ]: 167796 : Trace("constraints::pf") << ")" << std::endl;
1680 [ - + ][ - + ]: 167796 : Assert(!hasProof());
[ - - ]
1681 [ - + ][ - + ]: 167796 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1682 [ - + ][ - + ]: 167796 : Assert(allHaveProof(a));
[ - - ]
1683 : :
1684 [ - + ][ - + ]: 167796 : Assert(d_produceProofs == (coeffs != RationalVectorCPSentinel));
[ - - ]
1685 [ + + ][ + - ]: 167796 : Assert(!d_produceProofs || coeffs->size() == a.size() + 1);
[ - + ][ - + ]
[ - - ]
1686 : :
1687 [ - + ][ - + ]: 167796 : Assert(a.size() >= 1);
[ - - ]
1688 : :
1689 : 167796 : d_database->d_antecedents.push_back(NullConstraint);
1690 [ + + ]: 2016934 : for (ConstraintCPVec::const_iterator i = a.begin(), end = a.end(); i != end;
1691 : 1849138 : ++i)
1692 : : {
1693 : 1849138 : ConstraintCP c_i = *i;
1694 [ - + ][ - + ]: 1849138 : Assert(c_i->hasProof());
[ - - ]
1695 : 1849138 : d_database->d_antecedents.push_back(c_i);
1696 : : }
1697 : 167796 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1698 : :
1699 : : RationalVectorCP coeffsCopy;
1700 [ + + ]: 167796 : if (d_produceProofs)
1701 : : {
1702 [ - + ][ - + ]: 116137 : Assert(coeffs != RationalVectorCPSentinel);
[ - - ]
1703 : 116137 : coeffsCopy = new RationalVector(*coeffs);
1704 : : }
1705 : : else
1706 : : {
1707 : 51659 : coeffsCopy = RationalVectorCPSentinel;
1708 : : }
1709 : 167796 : d_database->pushConstraintRule(
1710 : 167796 : ConstraintRule(this, FarkasAP, antecedentEnd, coeffsCopy));
1711 : :
1712 [ - + ][ - + ]: 167796 : Assert(inConflict() == nowInConflict);
[ - - ]
1713 : 167796 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1714 : : {
1715 [ - - ]: 0 : Trace("constraint::conflictCommit")
1716 : 0 : << "inConflict@impliedByFarkas " << this << std::endl;
1717 : : }
1718 : 167796 : if (TraceIsOn("constraints::wffp") && !wellFormedFarkasProof(nm))
1719 : : {
1720 [ - - ]: 0 : getConstraintRule().print(Trace("constraints::wffp"), d_produceProofs);
1721 : : }
1722 [ - + ][ - + ]: 167796 : Assert(wellFormedFarkasProof(nm));
[ - - ]
1723 : 167796 : }
1724 : :
1725 : 0 : void Constraint::setInternalAssumption(CVC5_UNUSED bool nowInConflict)
1726 : : {
1727 [ - - ]: 0 : Trace("constraints::pf") << "setInternalAssumption(" << this;
1728 [ - - ]: 0 : Trace("constraints::pf") << ")" << std::endl;
1729 : 0 : Assert(!hasProof());
1730 : 0 : Assert(negationHasProof() == nowInConflict);
1731 : 0 : Assert(!assertedToTheTheory());
1732 : :
1733 : 0 : d_database->pushConstraintRule(ConstraintRule(this, InternalAssumeAP));
1734 : :
1735 : 0 : Assert(inConflict() == nowInConflict);
1736 : 0 : if (TraceIsOn("constraint::conflictCommit") && inConflict())
1737 : : {
1738 [ - - ]: 0 : Trace("constraint::conflictCommit")
1739 : 0 : << "inConflict@setInternalAssumption " << this << std::endl;
1740 : : }
1741 : 0 : }
1742 : :
1743 : 372764 : void Constraint::setEqualityEngineProof()
1744 : : {
1745 [ + - ]: 372764 : Trace("constraints::pf") << "setEqualityEngineProof(" << this;
1746 [ + - ]: 372764 : Trace("constraints::pf") << ")" << std::endl;
1747 [ - + ][ - + ]: 372764 : Assert(truthIsUnknown());
[ - - ]
1748 [ - + ][ - + ]: 372764 : Assert(hasLiteral());
[ - - ]
1749 : 372764 : d_database->pushConstraintRule(ConstraintRule(this, EqualityEngineAP));
1750 : 372764 : }
1751 : :
1752 : 7450463 : SortedConstraintMap& Constraint::constraintSet() const
1753 : : {
1754 [ - + ][ - + ]: 7450463 : Assert(d_database->variableDatabaseIsSetup(d_variable));
[ - - ]
1755 : 7450463 : return (d_database->d_varDatabases[d_variable])->d_constraints;
1756 : : }
1757 : :
1758 : 0 : bool Constraint::antecentListIsEmpty() const
1759 : : {
1760 : 0 : Assert(hasProof());
1761 : 0 : return d_database->d_antecedents[getEndAntecedent()] == NullConstraint;
1762 : : }
1763 : :
1764 : 0 : bool Constraint::antecedentListLengthIsOne() const
1765 : : {
1766 : 0 : Assert(hasProof());
1767 : 0 : return !antecentListIsEmpty()
1768 [ - - ][ - - ]: 0 : && d_database->d_antecedents[getEndAntecedent() - 1] == NullConstraint;
1769 : : }
1770 : :
1771 : 169273 : Node Constraint::externalImplication(NodeManager* nm,
1772 : : const ConstraintCPVec& b) const
1773 : : {
1774 [ - + ][ - + ]: 169273 : Assert(hasLiteral());
[ - - ]
1775 : 169273 : Node antecedent = externalExplainByAssertions(nm, b);
1776 : 169273 : Node implied = getLiteral();
1777 : 338546 : return antecedent.impNode(implied);
1778 : 169273 : }
1779 : :
1780 : 192865 : Node Constraint::externalExplainByAssertions(NodeManager* nm,
1781 : : const ConstraintCPVec& b)
1782 : : {
1783 : 192865 : return externalExplain(nm, b, AssertionOrderSentinel);
1784 : : }
1785 : :
1786 : 17135 : TrustNode Constraint::externalExplainForPropagation(TNode lit) const
1787 : : {
1788 [ - + ][ - + ]: 17135 : Assert(hasProof());
[ - - ]
1789 [ - + ][ - + ]: 17135 : Assert(!isAssumption());
[ - - ]
1790 [ - + ][ - + ]: 17135 : Assert(!isInternalAssumption());
[ - - ]
1791 : 17135 : NodeBuilder nb(d_database->nodeManager(), Kind::AND);
1792 : 17135 : auto pfFromAssumptions = externalExplain(nb, d_assertionOrder);
1793 : 17135 : Node n = mkAndFromBuilder(d_database->nodeManager(), nb);
1794 [ + + ]: 17135 : if (d_database->isProofEnabled())
1795 : : {
1796 : 7717 : std::vector<Node> assumptions;
1797 [ + + ]: 7717 : if (n.getKind() == Kind::AND)
1798 : : {
1799 : 3596 : assumptions.insert(assumptions.end(), n.begin(), n.end());
1800 : : }
1801 : : else
1802 : : {
1803 : 4121 : assumptions.push_back(n);
1804 : : }
1805 [ + + ]: 7717 : if (getProofLiteral() != lit)
1806 : : {
1807 : : pfFromAssumptions =
1808 : 4454 : ensurePredTransform(d_database->d_pnm, pfFromAssumptions, lit);
1809 : : }
1810 : 15434 : auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
1811 : 7717 : return d_database->d_pfGen->mkTrustedPropagation(
1812 : 7717 : lit, d_database->nodeManager()->mkAnd(assumptions), pf);
1813 : 7717 : }
1814 : : else
1815 : : {
1816 : 9418 : return TrustNode::mkTrustPropExp(lit, n);
1817 : : }
1818 : 17135 : }
1819 : :
1820 : 121023 : TrustNode Constraint::externalExplainConflict() const
1821 : : {
1822 [ + - ]: 121023 : Trace("pf::arith::explain") << this << std::endl;
1823 [ - + ][ - + ]: 121023 : Assert(inConflict());
[ - - ]
1824 : 121023 : NodeBuilder nb(d_database->nodeManager(), Kind::AND);
1825 : 121023 : auto pf1 = externalExplainByAssertions(nb);
1826 : 121023 : auto not2 = getNegation()->getProofLiteral().negate();
1827 : 121023 : auto pf2 = getNegation()->externalExplainByAssertions(nb);
1828 : 121023 : Node n = mkAndFromBuilder(d_database->nodeManager(), nb);
1829 [ + + ]: 121023 : if (d_database->isProofEnabled())
1830 : : {
1831 : 54910 : auto pfNot2 = ensurePredTransform(d_database->d_pnm, pf1, not2);
1832 : 54910 : std::vector<Node> lits;
1833 [ + - ]: 54910 : if (n.getKind() == Kind::AND)
1834 : : {
1835 : 54910 : lits.insert(lits.end(), n.begin(), n.end());
1836 : : }
1837 : : else
1838 : : {
1839 : 0 : lits.push_back(n);
1840 : : }
1841 [ - + ]: 54910 : if (TraceIsOn("arith::pf::externalExplainConflict"))
1842 : : {
1843 [ - - ]: 0 : Trace("arith::pf::externalExplainConflict") << "Lits:" << std::endl;
1844 [ - - ]: 0 : for (const auto& l : lits)
1845 : : {
1846 [ - - ]: 0 : Trace("arith::pf::externalExplainConflict") << " : " << l << std::endl;
1847 : : }
1848 : : }
1849 : : std::vector<Node> contraLits = {getProofLiteral(),
1850 : 219640 : getNegation()->getProofLiteral()};
1851 : : auto bot =
1852 : 54910 : not2.getKind() == Kind::NOT
1853 : 157329 : ? d_database->d_pnm->mkNode(ProofRule::CONTRA, {pf2, pfNot2}, {})
1854 : 281951 : : d_database->d_pnm->mkNode(ProofRule::CONTRA, {pfNot2, pf2}, {});
1855 [ - + ]: 54910 : if (TraceIsOn("arith::pf::tree"))
1856 : : {
1857 [ - - ]: 0 : Trace("arith::pf::tree") << *this << std::endl;
1858 [ - - ]: 0 : Trace("arith::pf::tree") << *getNegation() << std::endl;
1859 [ - - ]: 0 : Trace("arith::pf::tree") << "\n\nTree:\n";
1860 [ - - ]: 0 : printProofTree(Trace("arith::pf::tree"));
1861 [ - - ]: 0 : getNegation()->printProofTree(Trace("arith::pf::tree"));
1862 : : }
1863 : 109820 : auto confPf = d_database->d_pnm->mkScope(bot, lits);
1864 : 54910 : return d_database->d_pfGen->mkTrustNode(
1865 : 109820 : d_database->nodeManager()->mkAnd(lits), confPf, true);
1866 : 54910 : }
1867 : : else
1868 : : {
1869 : 66113 : return TrustNode::mkTrustConflict(n);
1870 : : }
1871 : 121023 : }
1872 : :
1873 : : struct ConstraintCPHash
1874 : : {
1875 : : /* Todo replace with an id */
1876 : 0 : size_t operator()(ConstraintCP c) const
1877 : : {
1878 : : Assert(sizeof(ConstraintCP) > 0);
1879 : 0 : return ((size_t)c) / sizeof(ConstraintCP);
1880 : : }
1881 : : };
1882 : :
1883 : 0 : void Constraint::assertionFringe(ConstraintCPVec& v)
1884 : : {
1885 : 0 : unordered_set<ConstraintCP, ConstraintCPHash> visited;
1886 : 0 : size_t writePos = 0;
1887 : :
1888 [ - - ]: 0 : if (!v.empty())
1889 : : {
1890 : 0 : const ConstraintDatabase* db = v.back()->d_database;
1891 : 0 : const CDConstraintList& antecedents = db->d_antecedents;
1892 [ - - ]: 0 : for (size_t i = 0; i < v.size(); ++i)
1893 : : {
1894 : 0 : ConstraintCP vi = v[i];
1895 [ - - ]: 0 : if (visited.find(vi) == visited.end())
1896 : : {
1897 : 0 : Assert(vi->hasProof());
1898 : 0 : visited.insert(vi);
1899 [ - - ]: 0 : if (vi->onFringe())
1900 : : {
1901 : 0 : v[writePos] = vi;
1902 : 0 : writePos++;
1903 : : }
1904 : : else
1905 : : {
1906 : 0 : Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof()
1907 : : || vi->hasIntHoleProof() || vi->hasIntTightenProof());
1908 : 0 : AntecedentId p = vi->getEndAntecedent();
1909 : :
1910 : 0 : ConstraintCP antecedent = antecedents[p];
1911 [ - - ]: 0 : while (antecedent != NullConstraint)
1912 : : {
1913 : 0 : v.push_back(antecedent);
1914 : 0 : --p;
1915 : 0 : antecedent = antecedents[p];
1916 : : }
1917 : : }
1918 : : }
1919 : : }
1920 : 0 : v.resize(writePos);
1921 : : }
1922 : 0 : }
1923 : :
1924 : 0 : void Constraint::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i)
1925 : : {
1926 : 0 : o.insert(o.end(), i.begin(), i.end());
1927 : 0 : assertionFringe(o);
1928 : 0 : }
1929 : :
1930 : 192865 : Node Constraint::externalExplain(NodeManager* nm,
1931 : : const ConstraintCPVec& v,
1932 : : AssertionOrder order)
1933 : : {
1934 : 192865 : NodeBuilder nb(nm, Kind::AND);
1935 : 192865 : ConstraintCPVec::const_iterator i, end;
1936 [ + + ]: 800985 : for (i = v.begin(), end = v.end(); i != end; ++i)
1937 : : {
1938 : 608120 : ConstraintCP v_i = *i;
1939 : 608120 : v_i->externalExplain(nb, order);
1940 : : }
1941 : 385730 : return mkAndFromBuilder(nm, nb);
1942 : 192865 : }
1943 : :
1944 : 8844700 : std::shared_ptr<ProofNode> Constraint::externalExplain(
1945 : : NodeBuilder& nb, AssertionOrder order) const
1946 : : {
1947 [ - + ]: 8844700 : if (TraceIsOn("pf::arith::explain"))
1948 : : {
1949 [ - - ]: 0 : this->printProofTree(Trace("arith::pf::tree"));
1950 [ - - ]: 0 : Trace("pf::arith::explain") << "Explaining: " << this << " with rule ";
1951 [ - - ]: 0 : getConstraintRule().print(Trace("pf::arith::explain"), d_produceProofs);
1952 [ - - ]: 0 : Trace("pf::arith::explain") << std::endl;
1953 : : }
1954 [ - + ][ - + ]: 8844700 : Assert(hasProof());
[ - - ]
1955 [ + + ][ + - ]: 8844700 : Assert(!isAssumption() || assertedToTheTheory());
[ - + ][ - + ]
[ - - ]
1956 [ - + ][ - + ]: 8844700 : Assert(!isInternalAssumption());
[ - - ]
1957 : 8844700 : std::shared_ptr<ProofNode> pf{};
1958 : :
1959 : 8844700 : ProofNodeManager* pnm = d_database->d_pnm;
1960 : :
1961 [ + + ]: 8844700 : if (assertedBefore(order))
1962 : : {
1963 [ + - ]: 7521654 : Trace("pf::arith::explain") << " already asserted" << std::endl;
1964 : 7521654 : nb << getWitness();
1965 [ + + ]: 7521654 : if (d_database->isProofEnabled())
1966 : : {
1967 : 3232906 : pf = pnm->mkAssume(getWitness());
1968 : : // If the witness and literal differ, prove the difference through a
1969 : : // rewrite.
1970 : 3232906 : pf = ensurePredTransform(pnm, pf, getProofLiteral());
1971 : : }
1972 : : }
1973 [ + + ]: 1323046 : else if (hasEqualityEngineProof())
1974 : : {
1975 : : // just assume, it will be explained again
1976 : 484 : Node lit = getLiteral();
1977 [ + + ]: 484 : if (d_database->isProofEnabled())
1978 : : {
1979 : 227 : std::shared_ptr<ProofNode> a = pnm->mkAssume(getLiteral());
1980 : 227 : Node plit = getProofLiteral();
1981 : 227 : pf = ensurePredTransform(pnm, a, plit);
1982 : 227 : }
1983 [ - + ][ - + ]: 484 : Assert(lit.getKind() != Kind::AND);
[ - - ]
1984 : 484 : nb << lit;
1985 : 484 : }
1986 : : else
1987 : : {
1988 [ + - ]: 1322562 : Trace("pf::arith::explain") << " recursion!" << std::endl;
1989 [ - + ][ - + ]: 1322562 : Assert(!isAssumption());
[ - - ]
1990 : 1322562 : AntecedentId p = getEndAntecedent();
1991 : 1322562 : ConstraintCP antecedent = d_database->d_antecedents[p];
1992 : 1322562 : std::vector<std::shared_ptr<ProofNode>> children;
1993 : :
1994 [ + + ]: 3739589 : while (antecedent != NullConstraint)
1995 : : {
1996 [ + - ]: 2417027 : Trace("pf::arith::explain") << "Explain " << antecedent << std::endl;
1997 : 2417027 : auto pn = antecedent->externalExplain(nb, order);
1998 [ + + ]: 2417027 : if (d_database->isProofEnabled())
1999 : : {
2000 : 989040 : children.push_back(pn);
2001 : : }
2002 : 2417027 : --p;
2003 : 2417027 : antecedent = d_database->d_antecedents[p];
2004 : 2417027 : }
2005 : :
2006 [ + + ]: 1322562 : if (d_database->isProofEnabled())
2007 : : {
2008 [ - + ][ + - ]: 638342 : switch (getProofType())
[ + - ]
2009 : : {
2010 : 0 : case ArithProofType::AssumeAP:
2011 : : case ArithProofType::EqualityEngineAP:
2012 : : {
2013 : 0 : Unreachable() << "These should be handled above";
2014 : : break;
2015 : : }
2016 : 59560 : case ArithProofType::FarkasAP:
2017 : : {
2018 : : // Per docs in constraint.h,
2019 : : // the 0th farkas coefficient is for the negation of the deduced
2020 : : // constraint the 1st corresponds to the last antecedent the nth
2021 : : // corresponds to the first antecedent Then, the farkas coefficients
2022 : : // and the antecedents are in the same order.
2023 : :
2024 : : // Enumerate child proofs (negation included) in d_farkasCoefficients
2025 : : // order
2026 : 59560 : Node plit = getNegation()->getProofLiteral();
2027 : 59560 : std::vector<std::shared_ptr<ProofNode>> farkasChildren;
2028 : 59560 : farkasChildren.push_back(pnm->mkAssume(plit));
2029 : 59560 : farkasChildren.insert(
2030 : 59560 : farkasChildren.end(), children.rbegin(), children.rend());
2031 : :
2032 : 59560 : NodeManager* nm = d_database->nodeManager();
2033 : :
2034 : : // Enumerate d_farkasCoefficients as nodes.
2035 : 59560 : std::vector<Node> farkasCoeffs;
2036 : 59560 : TypeNode type = plit[0].getType();
2037 [ + + ]: 489609 : for (Rational r : *getFarkasCoefficients())
2038 : : {
2039 : 430049 : farkasCoeffs.push_back(nm->mkConstRealOrInt(Rational(r)));
2040 : 430049 : }
2041 : : std::vector<Node> farkasCoeffsUse =
2042 : 59560 : getMacroSumUbCoeff(nm, farkasChildren, farkasCoeffs);
2043 : :
2044 : : // Apply the scaled-sum rule.
2045 : : std::shared_ptr<ProofNode> sumPf =
2046 : : pnm->mkNode(ProofRule::MACRO_ARITH_SCALE_SUM_UB,
2047 : : farkasChildren,
2048 : 59560 : farkasCoeffsUse);
2049 : :
2050 : : // Provable rewrite the result
2051 : 59560 : Node falsen = nm->mkConst(false);
2052 : 59560 : auto botPf = ensurePredTransform(pnm, sumPf, falsen);
2053 : :
2054 : : // Scope out the negated constraint, yielding a proof of the
2055 : : // constraint.
2056 : 178680 : std::vector<Node> assump{plit};
2057 : 119120 : auto maybeDoubleNotPf = pnm->mkScope(botPf, assump, false);
2058 : :
2059 : : // No need to ensure that the expected node aggrees with `assump`
2060 : : // because we are not providing an expected node.
2061 : : //
2062 : : // Prove that this is the literal (may need to clean a double-not)
2063 : 59560 : Node plit2 = getProofLiteral();
2064 : 59560 : pf = ensurePredTransform(pnm, maybeDoubleNotPf, plit2);
2065 : :
2066 : 59560 : break;
2067 : 59560 : }
2068 : 539013 : case ArithProofType::IntTightenAP:
2069 : : {
2070 [ + + ]: 539013 : if (isUpperBound())
2071 : : {
2072 : 1059102 : pf = pnm->mkNode(
2073 : 1588653 : ProofRule::INT_TIGHT_UB, children, {}, getProofLiteral());
2074 : : }
2075 [ + - ]: 9462 : else if (isLowerBound())
2076 : : {
2077 : 18924 : pf = pnm->mkNode(
2078 : 28386 : ProofRule::INT_TIGHT_LB, children, {}, getProofLiteral());
2079 : : }
2080 : : else
2081 : : {
2082 : 0 : Unreachable();
2083 : : }
2084 : 539013 : break;
2085 : : }
2086 : 0 : case ArithProofType::IntHoleAP:
2087 : : {
2088 : : // Use proofLit to ensure deterministic node ID assignments
2089 : 0 : Node proofLit = getProofLiteral();
2090 : 0 : pf = pnm->mkTrustedNode(
2091 : 0 : TrustId::THEORY_INFERENCE_ARITH, children, {proofLit}, proofLit);
2092 : 0 : break;
2093 : 0 : }
2094 : 39769 : case ArithProofType::TrichotomyAP:
2095 : : {
2096 : 79538 : pf = pnm->mkNode(
2097 : 119307 : ProofRule::ARITH_TRICHOTOMY, children, {}, getProofLiteral());
2098 : 39769 : break;
2099 : : }
2100 : 0 : case ArithProofType::InternalAssumeAP:
2101 : : case ArithProofType::NoAP:
2102 : : default:
2103 : : {
2104 : 0 : Unreachable() << getProofType()
2105 : 0 : << " should not be visible in explanation";
2106 : : break;
2107 : : }
2108 : : }
2109 : : }
2110 : 1322562 : }
2111 : 8844700 : return pf;
2112 : 0 : }
2113 : :
2114 : 1730 : Node Constraint::externalExplainByAssertions(NodeManager* nm,
2115 : : ConstraintCP a,
2116 : : ConstraintCP b)
2117 : : {
2118 : 1730 : NodeBuilder nb(nm, Kind::AND);
2119 : 1730 : a->externalExplainByAssertions(nb);
2120 : 1730 : b->externalExplainByAssertions(nb);
2121 : 3460 : return nb;
2122 : 1730 : }
2123 : :
2124 : 0 : Node Constraint::externalExplainByAssertions(NodeManager* nm,
2125 : : ConstraintCP a,
2126 : : ConstraintCP b,
2127 : : ConstraintCP c)
2128 : : {
2129 : 0 : NodeBuilder nb(nm, Kind::AND);
2130 : 0 : a->externalExplainByAssertions(nb);
2131 : 0 : b->externalExplainByAssertions(nb);
2132 : 0 : c->externalExplainByAssertions(nb);
2133 : 0 : return nb;
2134 : 0 : }
2135 : :
2136 : 827405 : ConstraintP Constraint::getStrictlyWeakerLowerBound(bool hasLiteral,
2137 : : bool asserted) const
2138 : : {
2139 [ - + ][ - + ]: 827405 : Assert(initialized());
[ - - ]
2140 [ + + ][ + - ]: 827405 : Assert(!asserted || hasLiteral);
[ - + ][ - + ]
[ - - ]
2141 : :
2142 : 827405 : SortedConstraintMapConstIterator i = d_variablePosition;
2143 : 827405 : const SortedConstraintMap& scm = constraintSet();
2144 : 827405 : SortedConstraintMapConstIterator i_begin = scm.begin();
2145 [ + + ]: 1716779 : while (i != i_begin)
2146 : : {
2147 : 1052544 : --i;
2148 : 1052544 : const ValueCollection& vc = i->second;
2149 [ + + ]: 1052544 : if (vc.hasLowerBound())
2150 : : {
2151 : 328317 : ConstraintP weaker = vc.getLowerBound();
2152 : :
2153 : : // asserted -> hasLiteral
2154 : : // hasLiteral -> weaker->hasLiteral()
2155 : : // asserted -> weaker->assertedToTheTheory()
2156 [ + + ]: 328317 : if ((!hasLiteral || (weaker->hasLiteral()))
2157 [ + - ][ + + ]: 656634 : && (!asserted || (weaker->assertedToTheTheory())))
[ + + ][ + + ]
2158 : : {
2159 : 163170 : return weaker;
2160 : : }
2161 : : }
2162 : : }
2163 : 664235 : return NullConstraint;
2164 : : }
2165 : :
2166 : 582879 : ConstraintP Constraint::getStrictlyWeakerUpperBound(bool hasLiteral,
2167 : : bool asserted) const
2168 : : {
2169 : 582879 : SortedConstraintMapConstIterator i = d_variablePosition;
2170 : 582879 : const SortedConstraintMap& scm = constraintSet();
2171 : 582879 : SortedConstraintMapConstIterator i_end = scm.end();
2172 : :
2173 : 582879 : ++i;
2174 [ + + ]: 1086645 : for (; i != i_end; ++i)
2175 : : {
2176 : 709810 : const ValueCollection& vc = i->second;
2177 [ + + ]: 709810 : if (vc.hasUpperBound())
2178 : : {
2179 : 260466 : ConstraintP weaker = vc.getUpperBound();
2180 [ + + ]: 260466 : if ((!hasLiteral || (weaker->hasLiteral()))
2181 [ + - ][ + + ]: 520932 : && (!asserted || (weaker->assertedToTheTheory())))
[ + + ][ + + ]
2182 : : {
2183 : 206044 : return weaker;
2184 : : }
2185 : : }
2186 : : }
2187 : :
2188 : 376835 : return NullConstraint;
2189 : : }
2190 : :
2191 : 8872163 : ConstraintP ConstraintDatabase::getBestImpliedBound(
2192 : : ArithVar v, ConstraintType t, const DeltaRational& r) const
2193 : : {
2194 [ - + ][ - + ]: 8872163 : Assert(variableDatabaseIsSetup(v));
[ - - ]
2195 [ + + ][ + - ]: 8872163 : Assert(t == UpperBound || t == LowerBound);
[ - + ][ - + ]
[ - - ]
2196 : :
2197 : 8872163 : SortedConstraintMap& scm = getVariableSCM(v);
2198 [ + + ]: 8872163 : if (t == UpperBound)
2199 : : {
2200 : 4228090 : SortedConstraintMapConstIterator i = scm.lower_bound(r);
2201 : 4228090 : SortedConstraintMapConstIterator i_end = scm.end();
2202 [ + + ][ + - ]: 4228090 : Assert(i == i_end || r <= i->first);
[ - + ][ - + ]
[ - - ]
2203 [ + + ]: 6389073 : for (; i != i_end; i++)
2204 : : {
2205 [ - + ][ - + ]: 3707768 : Assert(r <= i->first);
[ - - ]
2206 : 3707768 : const ValueCollection& vc = i->second;
2207 [ + + ]: 3707768 : if (vc.hasUpperBound())
2208 : : {
2209 : 1546785 : return vc.getUpperBound();
2210 : : }
2211 : : }
2212 : 2681305 : return NullConstraint;
2213 : : }
2214 : : else
2215 : : {
2216 [ - + ][ - + ]: 4644073 : Assert(t == LowerBound);
[ - - ]
2217 [ + + ]: 4644073 : if (scm.empty())
2218 : : {
2219 : 378163 : return NullConstraint;
2220 : : }
2221 : : else
2222 : : {
2223 : 4265910 : SortedConstraintMapConstIterator i = scm.lower_bound(r);
2224 : 4265910 : SortedConstraintMapConstIterator i_begin = scm.begin();
2225 : 4265910 : SortedConstraintMapConstIterator i_end = scm.end();
2226 [ + + ][ + - ]: 4265910 : Assert(i == i_end || r <= i->first);
[ - + ][ - + ]
[ - - ]
2227 : :
2228 : 4265910 : int fdj = 0;
2229 : :
2230 [ + + ]: 4265910 : if (i == i_end)
2231 : : {
2232 : 1703717 : --i;
2233 [ + - ]: 3407434 : Trace("getBestImpliedBound")
2234 : 1703717 : << fdj++ << " " << r << " " << i->first << endl;
2235 : : }
2236 [ + + ]: 2562193 : else if ((i->first) > r)
2237 : : {
2238 [ + + ]: 739357 : if (i == i_begin)
2239 : : {
2240 : 644222 : return NullConstraint;
2241 : : }
2242 : : else
2243 : : {
2244 : 95135 : --i;
2245 [ + - ]: 190270 : Trace("getBestImpliedBound")
2246 : 95135 : << fdj++ << " " << r << " " << i->first << endl;
2247 : : }
2248 : : }
2249 : :
2250 : : do
2251 : : {
2252 [ + - ]: 7938570 : Trace("getBestImpliedBound")
2253 : 3969285 : << fdj++ << " " << r << " " << i->first << endl;
2254 [ - + ][ - + ]: 3969285 : Assert(r >= i->first);
[ - - ]
2255 : 3969285 : const ValueCollection& vc = i->second;
2256 : :
2257 [ + + ]: 3969285 : if (vc.hasLowerBound())
2258 : : {
2259 : 1907499 : return vc.getLowerBound();
2260 : : }
2261 : :
2262 [ + + ]: 2061786 : if (i == i_begin)
2263 : : {
2264 : 1714189 : break;
2265 : : }
2266 : : else
2267 : : {
2268 : 347597 : --i;
2269 : : }
2270 : 347597 : } while (true);
2271 : 1714189 : return NullConstraint;
2272 : : }
2273 : : }
2274 : : }
2275 : :
2276 : 30384100 : bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const
2277 : : {
2278 : 30384100 : return v < d_varDatabases.size();
2279 : : }
2280 : :
2281 : 51016 : ConstraintDatabase::Watches::Watches(context::Context* satContext,
2282 : 51016 : context::Context* userContext)
2283 : 51016 : : d_constraintProofs(satContext),
2284 : 51016 : d_canBePropagatedWatches(satContext),
2285 : 51016 : d_assertionOrderWatches(satContext),
2286 : 51016 : d_splitWatches(userContext)
2287 : : {
2288 : 51016 : }
2289 : :
2290 : 1193410 : void Constraint::setLiteral(Node n)
2291 : : {
2292 [ + - ]: 1193410 : Trace("arith::constraint") << "Mapping " << *this << " to " << n << std::endl;
2293 [ - + ][ - + ]: 1193410 : Assert(Comparison::isNormalAtom(n));
[ - - ]
2294 [ - + ][ - + ]: 1193410 : Assert(!hasLiteral());
[ - - ]
2295 [ - + ][ - + ]: 1193410 : Assert(sanityChecking(n));
[ - - ]
2296 : 1193410 : d_literal = n;
2297 : 1193410 : NodetoConstraintMap& map = d_database->d_nodetoConstraintMap;
2298 [ - + ][ - + ]: 1193410 : Assert(map.find(n) == map.end());
[ - - ]
2299 : 1193410 : map.insert(make_pair(d_literal, this));
2300 : 1193410 : }
2301 : :
2302 : 4633248 : Node Constraint::getProofLiteral() const
2303 : : {
2304 [ - + ][ - + ]: 4633248 : Assert(d_database != nullptr);
[ - - ]
2305 [ - + ][ - + ]: 4633248 : Assert(d_database->d_avariables.hasNode(d_variable));
[ - - ]
2306 : 4633248 : Node varPart = d_database->d_avariables.asNode(d_variable);
2307 : : Kind cmp;
2308 : 4633248 : bool neg = false;
2309 [ + + ][ + + ]: 4633248 : switch (d_type)
[ - ]
2310 : : {
2311 : 1725103 : case ConstraintType::UpperBound:
2312 : : {
2313 [ + + ]: 1725103 : if (d_value.infinitesimalIsZero())
2314 : : {
2315 : 890247 : cmp = Kind::LEQ;
2316 : : }
2317 : : else
2318 : : {
2319 : 834856 : cmp = Kind::LT;
2320 : : }
2321 : 1725103 : break;
2322 : : }
2323 : 1103529 : case ConstraintType::LowerBound:
2324 : : {
2325 [ + + ]: 1103529 : if (d_value.infinitesimalIsZero())
2326 : : {
2327 : 966302 : cmp = Kind::GEQ;
2328 : : }
2329 : : else
2330 : : {
2331 : 137227 : cmp = Kind::GT;
2332 : : }
2333 : 1103529 : break;
2334 : : }
2335 : 1549174 : case ConstraintType::Equality:
2336 : : {
2337 : 1549174 : cmp = Kind::EQUAL;
2338 : 1549174 : break;
2339 : : }
2340 : 255442 : case ConstraintType::Disequality:
2341 : : {
2342 : 255442 : cmp = Kind::EQUAL;
2343 : 255442 : neg = true;
2344 : 255442 : break;
2345 : : }
2346 : 0 : default: Unreachable() << d_type;
2347 : : }
2348 : 4633248 : NodeManager* nm = d_database->nodeManager();
2349 : : Node constPart = nm->mkConstRealOrInt(
2350 : 13899744 : varPart.getType(), Rational(d_value.getNoninfinitesimalPart()));
2351 : 13899744 : Node posLit = nm->mkNode(cmp, varPart, constPart);
2352 [ + + ]: 9266496 : return neg ? posLit.negate() : posLit;
2353 : 4633248 : }
2354 : :
2355 : 75406 : void ConstraintDatabase::proveOr(std::vector<TrustNode>& out,
2356 : : ConstraintP a,
2357 : : ConstraintP b,
2358 : : bool negateSecond) const
2359 : : {
2360 : 75406 : Node la = a->getLiteral();
2361 : 75406 : Node lb = b->getLiteral();
2362 [ + + ]: 75406 : Node orN = (la < lb) ? la.orNode(lb) : lb.orNode(la);
2363 [ + + ]: 75406 : if (isProofEnabled())
2364 : : {
2365 [ - + ][ - + ]: 32643 : Assert(b->getNegation()->getType() != ConstraintType::Disequality);
[ - - ]
2366 : 32643 : auto nm = nodeManager();
2367 : 32643 : Node alit = a->getNegation()->getProofLiteral();
2368 : 32643 : TypeNode type = alit[0].getType();
2369 : 32643 : auto pf_neg_la = d_pnm->mkAssume(la.negate());
2370 : 32643 : pf_neg_la = ensurePredTransform(d_pnm, pf_neg_la, alit);
2371 : 32643 : Node blit = b->getNegation()->getProofLiteral();
2372 : 32643 : auto pf_neg_lb = d_pnm->mkAssume(lb.negate());
2373 : 32643 : pf_neg_lb = ensurePredTransform(d_pnm, pf_neg_lb, blit);
2374 [ + + ]: 32643 : int sndSign = negateSecond ? -1 : 1;
2375 : 130572 : std::vector<Pf> args{pf_neg_la, pf_neg_lb};
2376 : 0 : std::vector<Node> coeffs{nm->mkConstReal(Rational(-1 * sndSign)),
2377 : 163215 : nm->mkConstReal(Rational(sndSign))};
2378 : 32643 : std::vector<Node> coeffsUse = getMacroSumUbCoeff(nm, args, coeffs);
2379 : : auto sumubpf =
2380 : 32643 : d_pnm->mkNode(ProofRule::MACRO_ARITH_SCALE_SUM_UB, args, coeffsUse);
2381 : 32643 : auto bot_pf = ensurePredTransform(d_pnm, sumubpf, nm->mkConst(false));
2382 : 32643 : std::vector<Node> as;
2383 : 32643 : std::transform(orN.begin(), orN.end(), std::back_inserter(as), [](Node n) {
2384 : 65286 : return n.negate();
2385 : : });
2386 : : // No need to ensure that the expected node aggrees with `as` because we
2387 : : // are not providing an expected node.
2388 : : auto pf =
2389 : 130572 : d_pnm->mkNode(ProofRule::NOT_AND, {d_pnm->mkScope(bot_pf, as)}, {});
2390 : 32643 : pf = ensurePredTransform(d_pnm, pf, orN);
2391 : 32643 : out.push_back(d_pfGen->mkTrustNode(orN, pf));
2392 : 32643 : }
2393 : : else
2394 : : {
2395 : 42763 : out.push_back(TrustNode::mkTrustLemma(orN));
2396 : : }
2397 : 75406 : }
2398 : :
2399 : 70375 : void ConstraintDatabase::implies(std::vector<TrustNode>& out,
2400 : : ConstraintP a,
2401 : : ConstraintP b) const
2402 : : {
2403 : 70375 : Node la = a->getLiteral();
2404 : 70375 : Node lb = b->getLiteral();
2405 : :
2406 [ + + ]: 70375 : Node neg_la = (la.getKind() == Kind::NOT) ? la[0] : la.notNode();
2407 : :
2408 [ - + ][ - + ]: 70375 : Assert(lb != neg_la);
[ - - ]
2409 [ + + ][ + - ]: 70375 : Assert(b->getNegation()->getType() == ConstraintType::LowerBound
[ - + ][ - + ]
[ - - ]
2410 : : || b->getNegation()->getType() == ConstraintType::UpperBound);
2411 : 70375 : proveOr(out,
2412 : : a->getNegation(),
2413 : : b,
2414 : 70375 : b->getNegation()->getType() == ConstraintType::LowerBound);
2415 : 70375 : }
2416 : :
2417 : 5031 : void ConstraintDatabase::mutuallyExclusive(std::vector<TrustNode>& out,
2418 : : ConstraintP a,
2419 : : ConstraintP b) const
2420 : : {
2421 : 5031 : Node la = a->getLiteral();
2422 : 5031 : Node lb = b->getLiteral();
2423 : :
2424 : 5031 : Node neg_la = la.negate();
2425 : 5031 : Node neg_lb = lb.negate();
2426 : 5031 : proveOr(out, a->getNegation(), b->getNegation(), true);
2427 : 5031 : }
2428 : :
2429 : 116538 : void ConstraintDatabase::outputUnateInequalityLemmas(
2430 : : std::vector<TrustNode>& out, ArithVar v) const
2431 : : {
2432 : 116538 : SortedConstraintMap& scm = getVariableSCM(v);
2433 : 116538 : SortedConstraintMapConstIterator scm_iter = scm.begin();
2434 : 116538 : SortedConstraintMapConstIterator scm_end = scm.end();
2435 : 116538 : ConstraintP prev = NullConstraint;
2436 : : // get transitive unates
2437 : : // Only lower bounds or upperbounds should be done.
2438 [ + + ]: 373396 : for (; scm_iter != scm_end; ++scm_iter)
2439 : : {
2440 : 256858 : const ValueCollection& vc = scm_iter->second;
2441 [ + + ]: 256858 : if (vc.hasUpperBound())
2442 : : {
2443 : 120728 : ConstraintP ub = vc.getUpperBound();
2444 [ + + ]: 120728 : if (ub->hasLiteral())
2445 : : {
2446 [ + + ]: 120726 : if (prev != NullConstraint)
2447 : : {
2448 : 52630 : implies(out, prev, ub);
2449 : : }
2450 : 120726 : prev = ub;
2451 : : }
2452 : : }
2453 : : }
2454 : 116538 : }
2455 : :
2456 : 116538 : void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<TrustNode>& out,
2457 : : ArithVar v) const
2458 : : {
2459 : 116538 : vector<ConstraintP> equalities;
2460 : :
2461 : 116538 : SortedConstraintMap& scm = getVariableSCM(v);
2462 : 116538 : SortedConstraintMapConstIterator scm_iter = scm.begin();
2463 : 116538 : SortedConstraintMapConstIterator scm_end = scm.end();
2464 : :
2465 [ + + ]: 373396 : for (; scm_iter != scm_end; ++scm_iter)
2466 : : {
2467 : 256858 : const ValueCollection& vc = scm_iter->second;
2468 [ + + ]: 256858 : if (vc.hasEquality())
2469 : : {
2470 : 37953 : ConstraintP eq = vc.getEquality();
2471 [ + - ]: 37953 : if (eq->hasLiteral())
2472 : : {
2473 : 37953 : equalities.push_back(eq);
2474 : : }
2475 : : }
2476 : : }
2477 : :
2478 : 116538 : vector<ConstraintP>::const_iterator i, j, eq_end = equalities.end();
2479 [ + + ]: 154491 : for (i = equalities.begin(); i != eq_end; ++i)
2480 : : {
2481 : 37953 : ConstraintP at_i = *i;
2482 [ + + ]: 42984 : for (j = i + 1; j != eq_end; ++j)
2483 : : {
2484 : 5031 : ConstraintP at_j = *j;
2485 : :
2486 : 5031 : mutuallyExclusive(out, at_i, at_j);
2487 : : }
2488 : : }
2489 : :
2490 [ + + ]: 154491 : for (i = equalities.begin(); i != eq_end; ++i)
2491 : : {
2492 : 37953 : ConstraintP eq = *i;
2493 : 37953 : const ValueCollection& vc = eq->getValueCollection();
2494 [ + - ][ + - ]: 37953 : Assert(vc.hasEquality() && vc.getEquality()->hasLiteral());
[ - + ][ - + ]
[ - - ]
2495 : :
2496 [ + + ][ + - ]: 37953 : bool hasLB = vc.hasLowerBound() && vc.getLowerBound()->hasLiteral();
2497 [ + + ][ + + ]: 37953 : bool hasUB = vc.hasUpperBound() && vc.getUpperBound()->hasLiteral();
2498 : :
2499 [ + + ]: 37953 : ConstraintP lb = hasLB ? vc.getLowerBound()
2500 : 34183 : : eq->getStrictlyWeakerLowerBound(true, false);
2501 [ + + ]: 37953 : ConstraintP ub = hasUB ? vc.getUpperBound()
2502 : 37078 : : eq->getStrictlyWeakerUpperBound(true, false);
2503 : :
2504 [ + + ][ + + ]: 37953 : if (hasUB && hasLB && !eq->isSplit())
[ + - ][ + + ]
2505 : : {
2506 : 550 : out.push_back(eq->split());
2507 : : }
2508 [ + + ]: 37953 : if (lb != NullConstraint)
2509 : : {
2510 : 5902 : implies(out, eq, lb);
2511 : : }
2512 [ + + ]: 37953 : if (ub != NullConstraint)
2513 : : {
2514 : 11843 : implies(out, eq, ub);
2515 : : }
2516 : : }
2517 : 116538 : }
2518 : :
2519 : 28266 : void ConstraintDatabase::outputUnateEqualityLemmas(
2520 : : std::vector<TrustNode>& lemmas) const
2521 : : {
2522 [ + + ]: 144804 : for (ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v)
2523 : : {
2524 : 116538 : outputUnateEqualityLemmas(lemmas, v);
2525 : : }
2526 : 28266 : }
2527 : :
2528 : 28266 : void ConstraintDatabase::outputUnateInequalityLemmas(
2529 : : std::vector<TrustNode>& lemmas) const
2530 : : {
2531 [ + + ]: 144804 : for (ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v)
2532 : : {
2533 : 116538 : outputUnateInequalityLemmas(lemmas, v);
2534 : : }
2535 : 28266 : }
2536 : :
2537 : 7694054 : bool ConstraintDatabase::handleUnateProp(ConstraintP ant, ConstraintP cons)
2538 : : {
2539 [ + + ]: 7694054 : if (cons->negationHasProof())
2540 : : {
2541 [ + - ]: 4 : Trace("arith::unate") << "handleUnate: " << ant << " implies " << cons
2542 : 2 : << endl;
2543 : 2 : cons->impliedByUnate(nodeManager(), ant, true);
2544 : 2 : d_raiseConflict.raiseConflict(cons, InferenceId::ARITH_CONF_UNATE_PROP);
2545 : 2 : return true;
2546 : : }
2547 [ + + ]: 7694052 : else if (!cons->isTrue())
2548 : : {
2549 : 3610328 : ++d_statistics.d_unatePropagateImplications;
2550 [ + - ]: 7220656 : Trace("arith::unate") << "handleUnate: " << ant << " implies " << cons
2551 : 3610328 : << endl;
2552 : 3610328 : cons->impliedByUnate(nodeManager(), ant, false);
2553 : 3610328 : cons->tryToPropagate();
2554 : 3610328 : return false;
2555 : : }
2556 : : else
2557 : : {
2558 : 4083724 : return false;
2559 : : }
2560 : : }
2561 : :
2562 : 2236843 : void ConstraintDatabase::unatePropLowerBound(ConstraintP curr, ConstraintP prev)
2563 : : {
2564 [ + - ]: 4473686 : Trace("arith::unate") << "unatePropLowerBound " << curr << " " << prev
2565 : 2236843 : << endl;
2566 [ - + ][ - + ]: 2236843 : Assert(curr != prev);
[ - - ]
2567 [ - + ][ - + ]: 2236843 : Assert(curr != NullConstraint);
[ - - ]
2568 : 2236843 : bool hasPrev = !(prev == NullConstraint);
2569 [ + + ][ + - ]: 2236843 : Assert(!hasPrev || curr->getValue() > prev->getValue());
[ - + ][ - + ]
[ - - ]
2570 : :
2571 : 2236843 : ++d_statistics.d_unatePropagateCalls;
2572 : :
2573 : 2236843 : const SortedConstraintMap& scm = curr->constraintSet();
2574 : 2236843 : const SortedConstraintMapConstIterator scm_begin = scm.begin();
2575 : 2236843 : SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
2576 : :
2577 : : // Ignore the first ValueCollection
2578 : : // NOPE: (>= p c) then (= p c) NOPE
2579 : : // NOPE: (>= p c) then (not (= p c)) NOPE
2580 : :
2581 [ + + ]: 8051739 : while (scm_i != scm_begin)
2582 : : {
2583 : 6279478 : --scm_i; // move the iterator back
2584 : :
2585 : 6279478 : const ValueCollection& vc = scm_i->second;
2586 : :
2587 : : // If it has the previous element, do nothing and stop!
2588 [ + + ]: 1791612 : if (hasPrev && vc.hasConstraintOfType(prev->getType())
2589 [ + + ][ + + ]: 8071090 : && vc.getConstraintOfType(prev->getType()) == prev)
[ + + ]
2590 : : {
2591 : 464580 : break;
2592 : : }
2593 : :
2594 : : // Don't worry about implying the negation of upperbound.
2595 : : // These should all be handled by propagating the LowerBounds!
2596 [ + + ]: 5814898 : if (vc.hasLowerBound())
2597 : : {
2598 : 2213832 : ConstraintP lb = vc.getLowerBound();
2599 [ - + ]: 2213832 : if (handleUnateProp(curr, lb))
2600 : : {
2601 : 2 : return;
2602 : : }
2603 : : }
2604 [ + + ]: 5814898 : if (vc.hasDisequality())
2605 : : {
2606 : 527414 : ConstraintP dis = vc.getDisequality();
2607 [ + + ]: 527414 : if (handleUnateProp(curr, dis))
2608 : : {
2609 : 2 : return;
2610 : : }
2611 : : }
2612 : : }
2613 : : }
2614 : :
2615 : 2015575 : void ConstraintDatabase::unatePropUpperBound(ConstraintP curr, ConstraintP prev)
2616 : : {
2617 [ + - ]: 4031150 : Trace("arith::unate") << "unatePropUpperBound " << curr << " " << prev
2618 : 2015575 : << endl;
2619 [ - + ][ - + ]: 2015575 : Assert(curr != prev);
[ - - ]
2620 [ - + ][ - + ]: 2015575 : Assert(curr != NullConstraint);
[ - - ]
2621 : 2015575 : bool hasPrev = !(prev == NullConstraint);
2622 [ + + ][ + - ]: 2015575 : Assert(!hasPrev || curr->getValue() < prev->getValue());
[ - + ][ - + ]
[ - - ]
2623 : :
2624 : 2015575 : ++d_statistics.d_unatePropagateCalls;
2625 : :
2626 : 2015575 : const SortedConstraintMap& scm = curr->constraintSet();
2627 : 2015575 : const SortedConstraintMapConstIterator scm_end = scm.end();
2628 : 2015575 : SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
2629 : 2015575 : ++scm_i;
2630 [ + + ]: 7989039 : for (; scm_i != scm_end; ++scm_i)
2631 : : {
2632 : 6321791 : const ValueCollection& vc = scm_i->second;
2633 : :
2634 : : // If it has the previous element, do nothing and stop!
2635 [ + + ]: 1156477 : if (hasPrev && vc.hasConstraintOfType(prev->getType())
2636 [ + + ][ + + ]: 7478268 : && vc.getConstraintOfType(prev->getType()) == prev)
[ + + ]
2637 : : {
2638 : 348327 : break;
2639 : : }
2640 : : // Don't worry about implying the negation of upperbound.
2641 : : // These should all be handled by propagating the UpperBounds!
2642 [ + + ]: 5973464 : if (vc.hasUpperBound())
2643 : : {
2644 : 2348557 : ConstraintP ub = vc.getUpperBound();
2645 [ - + ]: 2348557 : if (handleUnateProp(curr, ub))
2646 : : {
2647 : 0 : return;
2648 : : }
2649 : : }
2650 [ + + ]: 5973464 : if (vc.hasDisequality())
2651 : : {
2652 : 387872 : ConstraintP dis = vc.getDisequality();
2653 [ - + ]: 387872 : if (handleUnateProp(curr, dis))
2654 : : {
2655 : 0 : return;
2656 : : }
2657 : : }
2658 : : }
2659 : : }
2660 : :
2661 : 1787761 : void ConstraintDatabase::unatePropEquality(ConstraintP curr,
2662 : : ConstraintP prevLB,
2663 : : ConstraintP prevUB)
2664 : : {
2665 [ + - ]: 3575522 : Trace("arith::unate") << "unatePropEquality " << curr << " " << prevLB << " "
2666 : 1787761 : << prevUB << endl;
2667 [ - + ][ - + ]: 1787761 : Assert(curr != prevLB);
[ - - ]
2668 [ - + ][ - + ]: 1787761 : Assert(curr != prevUB);
[ - - ]
2669 [ - + ][ - + ]: 1787761 : Assert(curr != NullConstraint);
[ - - ]
2670 : 1787761 : bool hasPrevLB = !(prevLB == NullConstraint);
2671 : 1787761 : bool hasPrevUB = !(prevUB == NullConstraint);
2672 [ + + ][ + - ]: 1787761 : Assert(!hasPrevLB || curr->getValue() >= prevLB->getValue());
[ - + ][ - + ]
[ - - ]
2673 [ + + ][ + - ]: 1787761 : Assert(!hasPrevUB || curr->getValue() <= prevUB->getValue());
[ - + ][ - + ]
[ - - ]
2674 : :
2675 : 1787761 : ++d_statistics.d_unatePropagateCalls;
2676 : :
2677 : 1787761 : const SortedConstraintMap& scm = curr->constraintSet();
2678 : 1787761 : SortedConstraintMapConstIterator scm_curr = curr->d_variablePosition;
2679 : : SortedConstraintMapConstIterator scm_last =
2680 [ + + ]: 1787761 : hasPrevUB ? prevUB->d_variablePosition : scm.end();
2681 : 1787761 : SortedConstraintMapConstIterator scm_i;
2682 [ + + ]: 1787761 : if (hasPrevLB)
2683 : : {
2684 : 219811 : scm_i = prevLB->d_variablePosition;
2685 [ + + ]: 219811 : if (scm_i != scm_curr)
2686 : : { // If this does not move this past scm_curr, move it one forward
2687 : 55887 : ++scm_i;
2688 : : }
2689 : : }
2690 : : else
2691 : : {
2692 : 1567950 : scm_i = scm.begin();
2693 : : }
2694 : :
2695 [ + + ]: 2872864 : for (; scm_i != scm_curr; ++scm_i)
2696 : : {
2697 : : // between the previous LB and the curr
2698 : 1085103 : const ValueCollection& vc = scm_i->second;
2699 : :
2700 : : // Don't worry about implying the negation of upperbound.
2701 : : // These should all be handled by propagating the LowerBounds!
2702 [ + + ]: 1085103 : if (vc.hasLowerBound())
2703 : : {
2704 : 332139 : ConstraintP lb = vc.getLowerBound();
2705 [ - + ]: 332139 : if (handleUnateProp(curr, lb))
2706 : : {
2707 : 0 : return;
2708 : : }
2709 : : }
2710 [ + + ]: 1085103 : if (vc.hasDisequality())
2711 : : {
2712 : 325185 : ConstraintP dis = vc.getDisequality();
2713 [ - + ]: 325185 : if (handleUnateProp(curr, dis))
2714 : : {
2715 : 0 : return;
2716 : : }
2717 : : }
2718 : : }
2719 [ - + ][ - + ]: 1787761 : Assert(scm_i == scm_curr);
[ - - ]
2720 [ + + ][ + + ]: 1787761 : if (!hasPrevUB || scm_i != scm_last)
[ + + ]
2721 : : {
2722 : 1738512 : ++scm_i;
2723 : : } // hasPrevUB implies scm_i != scm_last
2724 : :
2725 [ + + ]: 4420882 : for (; scm_i != scm_last; ++scm_i)
2726 : : {
2727 : : // between the curr and the previous UB imply the upperbounds and
2728 : : // disequalities.
2729 : 2633121 : const ValueCollection& vc = scm_i->second;
2730 : :
2731 : : // Don't worry about implying the negation of upperbound.
2732 : : // These should all be handled by propagating the UpperBounds!
2733 [ + + ]: 2633121 : if (vc.hasUpperBound())
2734 : : {
2735 : 901794 : ConstraintP ub = vc.getUpperBound();
2736 [ - + ]: 901794 : if (handleUnateProp(curr, ub))
2737 : : {
2738 : 0 : return;
2739 : : }
2740 : : }
2741 [ + + ]: 2633121 : if (vc.hasDisequality())
2742 : : {
2743 : 657261 : ConstraintP dis = vc.getDisequality();
2744 [ - + ]: 657261 : if (handleUnateProp(curr, dis))
2745 : : {
2746 : 0 : return;
2747 : : }
2748 : : }
2749 : : }
2750 : : }
2751 : :
2752 : 2490847 : std::pair<int, int> Constraint::unateFarkasSigns(ConstraintCP ca,
2753 : : ConstraintCP cb)
2754 : : {
2755 : 2490847 : ConstraintType a = ca->getType();
2756 : 2490847 : ConstraintType b = cb->getType();
2757 : :
2758 [ - + ][ - + ]: 2490847 : Assert(a != Disequality);
[ - - ]
2759 [ - + ][ - + ]: 2490847 : Assert(b != Disequality);
[ - - ]
2760 : :
2761 [ + + ][ + + ]: 2490847 : int a_sgn = (a == LowerBound) ? -1 : ((a == UpperBound) ? 1 : 0);
2762 [ + + ][ + + ]: 2490847 : int b_sgn = (b == LowerBound) ? -1 : ((b == UpperBound) ? 1 : 0);
2763 : :
2764 [ + + ][ + + ]: 2490847 : if (a_sgn == 0 && b_sgn == 0)
2765 : : {
2766 [ - + ][ - + ]: 555325 : Assert(a == Equality);
[ - - ]
2767 [ - + ][ - + ]: 555325 : Assert(b == Equality);
[ - - ]
2768 [ - + ][ - + ]: 555325 : Assert(ca->getValue() != cb->getValue());
[ - - ]
2769 [ + + ]: 555325 : if (ca->getValue() < cb->getValue())
2770 : : {
2771 : 174876 : a_sgn = 1;
2772 : 174876 : b_sgn = -1;
2773 : : }
2774 : : else
2775 : : {
2776 : 380449 : a_sgn = -1;
2777 : 380449 : b_sgn = 1;
2778 : : }
2779 : : }
2780 [ + + ]: 1935522 : else if (a_sgn == 0)
2781 : : {
2782 [ - + ][ - + ]: 372742 : Assert(b_sgn != 0);
[ - - ]
2783 [ - + ][ - + ]: 372742 : Assert(a == Equality);
[ - - ]
2784 : 372742 : a_sgn = -b_sgn;
2785 : : }
2786 [ + + ]: 1562780 : else if (b_sgn == 0)
2787 : : {
2788 [ - + ][ - + ]: 599589 : Assert(a_sgn != 0);
[ - - ]
2789 [ - + ][ - + ]: 599589 : Assert(b == Equality);
[ - - ]
2790 : 599589 : b_sgn = -a_sgn;
2791 : : }
2792 [ - + ][ - + ]: 2490847 : Assert(a_sgn != 0);
[ - - ]
2793 [ - + ][ - + ]: 2490847 : Assert(b_sgn != 0);
[ - - ]
2794 : :
2795 [ + - ]: 4981694 : Trace("arith::unateFarkasSigns")
2796 : 0 : << "Constraint::unateFarkasSigns(" << a << ", " << b << ") -> "
2797 : 2490847 : << "(" << a_sgn << ", " << b_sgn << ")" << endl;
2798 : 4981694 : return make_pair(a_sgn, b_sgn);
2799 : : }
2800 : :
2801 : : } // namespace arith::linear
2802 : : } // namespace theory
2803 : : } // namespace cvc5::internal
|
