Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Tim King, Alex Ozdemir, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * [[ Add one-line brief description here ]]
14 : : *
15 : : * [[ Add lengthier description here ]]
16 : : * \todo document this file
17 : : */
18 : : #include "theory/arith/linear/constraint.h"
19 : :
20 : : #include <algorithm>
21 : : #include <ostream>
22 : : #include <unordered_set>
23 : :
24 : : #include "base/output.h"
25 : : #include "options/smt_options.h"
26 : : #include "proof/eager_proof_generator.h"
27 : : #include "proof/proof_node_manager.h"
28 : : #include "smt/env.h"
29 : : #include "theory/arith/arith_proof_utilities.h"
30 : : #include "theory/arith/arith_utilities.h"
31 : : #include "theory/arith/linear/congruence_manager.h"
32 : : #include "theory/arith/linear/normal_form.h"
33 : : #include "theory/arith/linear/partial_model.h"
34 : : #include "theory/builtin/proof_checker.h"
35 : : #include "theory/rewriter.h"
36 : :
37 : : using namespace std;
38 : : using namespace cvc5::internal::kind;
39 : :
40 : : namespace cvc5::internal {
41 : : namespace theory {
42 : : namespace arith::linear {
43 : :
44 : 0 : ConstraintRule::ConstraintRule()
45 : : : d_constraint(NullConstraint),
46 : : d_proofType(NoAP),
47 : 0 : d_antecedentEnd(AntecedentIdSentinel)
48 : : {
49 : 0 : d_farkasCoefficients = RationalVectorCPSentinel;
50 : 0 : }
51 : :
52 : 10338000 : ConstraintRule::ConstraintRule(ConstraintP con, ArithProofType pt)
53 : 10338000 : : d_constraint(con), d_proofType(pt), d_antecedentEnd(AntecedentIdSentinel)
54 : : {
55 : 10338000 : d_farkasCoefficients = RationalVectorCPSentinel;
56 : 10338000 : }
57 : 3511010 : ConstraintRule::ConstraintRule(ConstraintP con,
58 : : ArithProofType pt,
59 : 3511010 : AntecedentId antecedentEnd)
60 : 3511010 : : d_constraint(con), d_proofType(pt), d_antecedentEnd(antecedentEnd)
61 : : {
62 : 3511010 : d_farkasCoefficients = RationalVectorCPSentinel;
63 : 3511010 : }
64 : :
65 : 3959530 : ConstraintRule::ConstraintRule(ConstraintP con,
66 : : ArithProofType pt,
67 : : AntecedentId antecedentEnd,
68 : 3959530 : RationalVectorCP coeffs)
69 : 3959530 : : d_constraint(con), d_proofType(pt), d_antecedentEnd(antecedentEnd)
70 : : {
71 [ + + ][ - + ]: 3959530 : Assert(con->isProofProducing() || coeffs == RationalVectorCPSentinel);
[ - + ][ - - ]
72 : 3959530 : d_farkasCoefficients = coeffs;
73 : 3959530 : }
74 : :
75 : : /** Given a simplifiedKind this returns the corresponding ConstraintType. */
76 : : //ConstraintType constraintTypeOfLiteral(Kind k);
77 : 1166590 : ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){
78 : 1166590 : Kind k = cmp.comparisonKind();
79 [ + + ][ + + ]: 1166590 : switch(k){
[ - ]
80 : 316713 : case Kind::LT:
81 : : case Kind::LEQ:
82 : : {
83 : 633426 : Polynomial l = cmp.getLeft();
84 [ + + ]: 316713 : if(l.leadingCoefficientIsPositive()){ // (< x c)
85 : 274571 : return UpperBound;
86 : : }else{
87 : 42142 : return LowerBound; // (< (-x) c)
88 : : }
89 : : }
90 : 319416 : case Kind::GT:
91 : : case Kind::GEQ:
92 : : {
93 : 638832 : Polynomial l = cmp.getLeft();
94 [ + + ]: 319416 : if(l.leadingCoefficientIsPositive()){
95 : 276911 : return LowerBound; // (> x c)
96 : : }else{
97 : 42505 : return UpperBound; // (> (-x) c)
98 : : }
99 : : }
100 : 265475 : case Kind::EQUAL: return Equality;
101 : 264983 : case Kind::DISTINCT: return Disequality;
102 : 0 : default: Unhandled() << k;
103 : : }
104 : : }
105 : :
106 : 1476240 : Constraint::Constraint(ArithVar x,
107 : : ConstraintType t,
108 : : const DeltaRational& v,
109 : 1476240 : bool produceProofs)
110 : : : d_variable(x),
111 : : d_type(t),
112 : : d_value(v),
113 : : d_database(NULL),
114 : : d_literal(Node::null()),
115 : : d_negation(NullConstraint),
116 : : d_canBePropagated(false),
117 : : d_assertionOrder(AssertionOrderSentinel),
118 : : d_witness(TNode::null()),
119 : : d_crid(ConstraintRuleIdSentinel),
120 : : d_split(false),
121 : : d_variablePosition(),
122 : 1476240 : d_produceProofs(produceProofs)
123 : : {
124 [ - + ][ - + ]: 1476240 : Assert(!initialized());
[ - - ]
125 : 1476240 : }
126 : :
127 : :
128 : 0 : std::ostream& operator<<(std::ostream& o, const ArithProofType apt){
129 [ - - ][ - - ]: 0 : switch(apt){
[ - - ][ - - ]
[ - ]
130 : 0 : case NoAP: o << "NoAP"; break;
131 : 0 : case AssumeAP: o << "AssumeAP"; break;
132 : 0 : case InternalAssumeAP: o << "InternalAssumeAP"; break;
133 : 0 : case FarkasAP: o << "FarkasAP"; break;
134 : 0 : case TrichotomyAP: o << "TrichotomyAP"; break;
135 : 0 : case EqualityEngineAP: o << "EqualityEngineAP"; break;
136 : 0 : case IntTightenAP: o << "IntTightenAP"; break;
137 : 0 : case IntHoleAP: o << "IntHoleAP"; break;
138 : 0 : default: break;
139 : : }
140 : 0 : return o;
141 : : }
142 : :
143 : 0 : std::ostream& operator<<(std::ostream& o, const ConstraintCP c){
144 [ - - ]: 0 : if(c == NullConstraint){
145 : 0 : return o << "NullConstraint";
146 : : }else{
147 : 0 : return o << *c;
148 : : }
149 : : }
150 : :
151 : 0 : std::ostream& operator<<(std::ostream& o, const ConstraintP c){
152 [ - - ]: 0 : if(c == NullConstraint){
153 : 0 : return o << "NullConstraint";
154 : : }else{
155 : 0 : return o << *c;
156 : : }
157 : : }
158 : :
159 : 0 : std::ostream& operator<<(std::ostream& o, const ConstraintType t){
160 [ - - ][ - - ]: 0 : switch(t){
[ - ]
161 : 0 : case LowerBound:
162 : 0 : return o << ">=";
163 : 0 : case UpperBound:
164 : 0 : return o << "<=";
165 : 0 : case Equality:
166 : 0 : return o << "=";
167 : 0 : case Disequality:
168 : 0 : return o << "!=";
169 : 0 : default:
170 : 0 : Unreachable();
171 : : }
172 : : }
173 : :
174 : 0 : std::ostream& operator<<(std::ostream& o, const Constraint& c){
175 : 0 : o << c.getVariable() << ' ' << c.getType() << ' ' << c.getValue();
176 [ - - ]: 0 : if(c.hasLiteral()){
177 : 0 : o << "(node " << c.getLiteral() << ')';
178 : : }
179 : 0 : return o;
180 : : }
181 : :
182 : 0 : std::ostream& operator<<(std::ostream& o, const ValueCollection& vc){
183 : 0 : o << "{";
184 : 0 : bool pending = false;
185 [ - - ]: 0 : if(vc.hasEquality()){
186 : 0 : o << "eq: " << vc.getEquality();
187 : 0 : pending = true;
188 : : }
189 [ - - ]: 0 : if(vc.hasLowerBound()){
190 [ - - ]: 0 : if(pending){
191 : 0 : o << ", ";
192 : : }
193 : 0 : o << "lb: " << vc.getLowerBound();
194 : 0 : pending = true;
195 : : }
196 [ - - ]: 0 : if(vc.hasUpperBound()){
197 [ - - ]: 0 : if(pending){
198 : 0 : o << ", ";
199 : : }
200 : 0 : o << "ub: " << vc.getUpperBound();
201 : 0 : pending = true;
202 : : }
203 [ - - ]: 0 : if(vc.hasDisequality()){
204 [ - - ]: 0 : if(pending){
205 : 0 : o << ", ";
206 : : }
207 : 0 : o << "de: " << vc.getDisequality();
208 : : }
209 : 0 : return o << "}";
210 : : }
211 : :
212 : 0 : std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){
213 : 0 : o << "[" << v.size() << "x";
214 : 0 : ConstraintCPVec::const_iterator i, end;
215 [ - - ]: 0 : for(i=v.begin(), end=v.end(); i != end; ++i){
216 : 0 : ConstraintCP c = *i;
217 : 0 : o << ", " << (*c);
218 : : }
219 : 0 : o << "]";
220 : 0 : return o;
221 : : }
222 : :
223 : 4629050 : ValueCollection::ValueCollection()
224 : : : d_lowerBound(NullConstraint),
225 : : d_upperBound(NullConstraint),
226 : : d_equality(NullConstraint),
227 : 4629050 : d_disequality(NullConstraint)
228 : 4629050 : {}
229 : :
230 : 34411200 : bool ValueCollection::hasLowerBound() const{
231 : 34411200 : return d_lowerBound != NullConstraint;
232 : : }
233 : :
234 : 37770600 : bool ValueCollection::hasUpperBound() const{
235 : 37770600 : return d_upperBound != NullConstraint;
236 : : }
237 : :
238 : 10573400 : bool ValueCollection::hasEquality() const{
239 : 10573400 : return d_equality != NullConstraint;
240 : : }
241 : :
242 : 30771200 : bool ValueCollection::hasDisequality() const {
243 : 30771200 : return d_disequality != NullConstraint;
244 : : }
245 : :
246 : 6467080 : ConstraintP ValueCollection::getLowerBound() const {
247 [ - + ][ - + ]: 6467080 : Assert(hasLowerBound());
[ - - ]
248 : 6467080 : return d_lowerBound;
249 : : }
250 : :
251 : 6847260 : ConstraintP ValueCollection::getUpperBound() const {
252 [ - + ][ - + ]: 6847260 : Assert(hasUpperBound());
[ - - ]
253 : 6847260 : return d_upperBound;
254 : : }
255 : :
256 : 996545 : ConstraintP ValueCollection::getEquality() const {
257 [ - + ][ - + ]: 996545 : Assert(hasEquality());
[ - - ]
258 : 996545 : return d_equality;
259 : : }
260 : :
261 : 4207830 : ConstraintP ValueCollection::getDisequality() const {
262 [ - + ][ - + ]: 4207830 : Assert(hasDisequality());
[ - - ]
263 : 4207830 : return d_disequality;
264 : : }
265 : :
266 : :
267 : 1004920 : void ValueCollection::push_into(std::vector<ConstraintP>& vec) const {
268 [ + - ]: 1004920 : Trace("arith::constraint") << "push_into " << *this << endl;
269 [ + + ]: 1004920 : if(hasEquality()){
270 : 274029 : vec.push_back(d_equality);
271 : : }
272 [ + + ]: 1004920 : if(hasLowerBound()){
273 : 462085 : vec.push_back(d_lowerBound);
274 : : }
275 [ + + ]: 1004920 : if(hasUpperBound()){
276 : 462085 : vec.push_back(d_upperBound);
277 : : }
278 [ + + ]: 1004920 : if(hasDisequality()){
279 : 274029 : vec.push_back(d_disequality);
280 : : }
281 : 1004920 : }
282 : :
283 : 0 : ValueCollection ValueCollection::mkFromConstraint(ConstraintP c){
284 : 0 : ValueCollection ret;
285 : 0 : Assert(ret.empty());
286 [ - - ][ - - ]: 0 : switch(c->getType()){
[ - ]
287 : 0 : case LowerBound:
288 : 0 : ret.d_lowerBound = c;
289 : 0 : break;
290 : 0 : case UpperBound:
291 : 0 : ret.d_upperBound = c;
292 : 0 : break;
293 : 0 : case Equality:
294 : 0 : ret.d_equality = c;
295 : 0 : break;
296 : 0 : case Disequality:
297 : 0 : ret.d_disequality = c;
298 : 0 : break;
299 : 0 : default:
300 : 0 : Unreachable();
301 : : }
302 : 0 : return ret;
303 : : }
304 : :
305 : 7771780 : bool ValueCollection::hasConstraintOfType(ConstraintType t) const{
306 [ + + ][ + - ]: 7771780 : switch(t){
[ - ]
307 : 2536120 : case LowerBound:
308 : 2536120 : return hasLowerBound();
309 : 4140890 : case UpperBound:
310 : 4140890 : return hasUpperBound();
311 : 1094770 : case Equality:
312 : 1094770 : return hasEquality();
313 : 0 : case Disequality:
314 : 0 : return hasDisequality();
315 : 0 : default:
316 : 0 : Unreachable();
317 : : }
318 : : }
319 : :
320 : 482594 : ArithVar ValueCollection::getVariable() const{
321 [ - + ][ - + ]: 482594 : Assert(!empty());
[ - - ]
322 : 482594 : return nonNull()->getVariable();
323 : : }
324 : :
325 : 482594 : const DeltaRational& ValueCollection::getValue() const{
326 [ - + ][ - + ]: 482594 : Assert(!empty());
[ - - ]
327 : 482594 : return nonNull()->getValue();
328 : : }
329 : :
330 : 1473040 : void ValueCollection::add(ConstraintP c){
331 [ - + ][ - + ]: 1473040 : Assert(c != NullConstraint);
[ - - ]
332 : :
333 [ + + ][ - + ]: 1473040 : Assert(empty() || getVariable() == c->getVariable());
[ - + ][ - - ]
334 [ + + ][ - + ]: 1473040 : Assert(empty() || getValue() == c->getValue());
[ - + ][ - - ]
335 : :
336 [ + + ][ + + ]: 1473040 : switch(c->getType()){
[ - ]
337 : 462400 : case LowerBound:
338 [ - + ][ - + ]: 462400 : Assert(!hasLowerBound());
[ - - ]
339 : 462400 : d_lowerBound = c;
340 : 462400 : break;
341 : 274120 : case Equality:
342 [ - + ][ - + ]: 274120 : Assert(!hasEquality());
[ - - ]
343 : 274120 : d_equality = c;
344 : 274120 : break;
345 : 462400 : case UpperBound:
346 [ - + ][ - + ]: 462400 : Assert(!hasUpperBound());
[ - - ]
347 : 462400 : d_upperBound = c;
348 : 462400 : break;
349 : 274120 : case Disequality:
350 [ - + ][ - + ]: 274120 : Assert(!hasDisequality());
[ - - ]
351 : 274120 : d_disequality = c;
352 : 274120 : break;
353 : 0 : default:
354 : 0 : Unreachable();
355 : : }
356 : 1473040 : }
357 : :
358 : 5828100 : ConstraintP ValueCollection::getConstraintOfType(ConstraintType t) const{
359 [ + + ][ + - ]: 5828100 : switch(t){
[ - ]
360 [ - + ][ - + ]: 1529930 : case LowerBound: Assert(hasLowerBound()); return d_lowerBound;
[ - - ]
361 [ - + ][ - + ]: 820654 : case Equality: Assert(hasEquality()); return d_equality;
[ - - ]
362 [ - + ][ - + ]: 3477520 : case UpperBound: Assert(hasUpperBound()); return d_upperBound;
[ - - ]
363 : 0 : case Disequality: Assert(hasDisequality()); return d_disequality;
364 : 0 : default: Unreachable();
365 : : }
366 : : }
367 : :
368 : 1472230 : void ValueCollection::remove(ConstraintType t){
369 [ + + ][ + + ]: 1472230 : switch(t){
[ - ]
370 : 462085 : case LowerBound:
371 [ - + ][ - + ]: 462085 : Assert(hasLowerBound());
[ - - ]
372 : 462085 : d_lowerBound = NullConstraint;
373 : 462085 : break;
374 : 274029 : case Equality:
375 [ - + ][ - + ]: 274029 : Assert(hasEquality());
[ - - ]
376 : 274029 : d_equality = NullConstraint;
377 : 274029 : break;
378 : 462085 : case UpperBound:
379 [ - + ][ - + ]: 462085 : Assert(hasUpperBound());
[ - - ]
380 : 462085 : d_upperBound = NullConstraint;
381 : 462085 : break;
382 : 274029 : case Disequality:
383 [ - + ][ - + ]: 274029 : Assert(hasDisequality());
[ - - ]
384 : 274029 : d_disequality = NullConstraint;
385 : 274029 : break;
386 : 0 : default:
387 : 0 : Unreachable();
388 : : }
389 : 1472230 : }
390 : :
391 : 5383500 : bool ValueCollection::empty() const{
392 : : return
393 [ + + ]: 9993100 : !(hasLowerBound() ||
394 [ + + ]: 4609600 : hasUpperBound() ||
395 [ + + ]: 4419060 : hasEquality() ||
396 [ + - ]: 8399450 : hasDisequality());
397 : : }
398 : :
399 : 965188 : ConstraintP ValueCollection::nonNull() const{
400 : : //This can be optimized by caching, but this is not necessary yet!
401 : : /* "Premature optimization is the root of all evil." */
402 [ + + ]: 965188 : if(hasLowerBound()){
403 : 311674 : return d_lowerBound;
404 [ + + ]: 653514 : }else if(hasUpperBound()){
405 : 88978 : return d_upperBound;
406 [ + - ]: 564536 : }else if(hasEquality()){
407 : 564536 : return d_equality;
408 [ - - ]: 0 : }else if(hasDisequality()){
409 : 0 : return d_disequality;
410 : : }else{
411 : 0 : return NullConstraint;
412 : : }
413 : : }
414 : :
415 : 5361290 : bool Constraint::initialized() const {
416 : 5361290 : return d_database != NULL;
417 : : }
418 : :
419 : 0 : const ConstraintDatabase& Constraint::getDatabase() const{
420 : 0 : Assert(initialized());
421 : 0 : return *d_database;
422 : : }
423 : :
424 : 1473040 : void Constraint::initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation){
425 [ - + ][ - + ]: 1473040 : Assert(!initialized());
[ - - ]
426 : 1473040 : d_database = db;
427 : 1473040 : d_variablePosition = v;
428 : 1473040 : d_negation = negation;
429 : 1473040 : }
430 : :
431 : 1475420 : Constraint::~Constraint() {
432 : : // Call this instead of safeToGarbageCollect()
433 [ - + ][ - + ]: 1475420 : Assert(!contextDependentDataIsSet());
434 : :
435 [ + + ]: 1475420 : if(initialized()){
436 : 1472230 : ValueCollection& vc = d_variablePosition->second;
437 [ + - ]: 1472230 : Trace("arith::constraint") << "removing" << vc << endl;
438 : :
439 : 1472230 : vc.remove(getType());
440 : :
441 [ + + ]: 1472230 : if(vc.empty()){
442 [ + - ]: 1004920 : Trace("arith::constraint") << "erasing" << vc << endl;
443 : 1004920 : SortedConstraintMap& perVariable = d_database->getVariableSCM(getVariable());
444 : 1004920 : perVariable.erase(d_variablePosition);
445 : : }
446 : :
447 [ + + ]: 1472230 : if(hasLiteral()){
448 : 1169120 : d_database->d_nodetoConstraintMap.erase(getLiteral());
449 : : }
450 : : }
451 : 1475420 : }
452 : :
453 : 48552600 : const ConstraintRule& Constraint::getConstraintRule() const {
454 [ - + ][ - + ]: 48552600 : Assert(hasProof());
[ - - ]
455 : 48552600 : return d_database->d_watches->d_constraintProofs[d_crid];
456 : : }
457 : :
458 : 6446950 : const ValueCollection& Constraint::getValueCollection() const{
459 : 6446950 : return d_variablePosition->second;
460 : : }
461 : :
462 : :
463 : 135672 : ConstraintP Constraint::getCeiling() {
464 [ + - ]: 135672 : Trace("getCeiling") << "Constraint_::getCeiling on " << *this << endl;
465 [ - + ][ - + ]: 135672 : Assert(getValue().getInfinitesimalPart().sgn() > 0);
[ - - ]
466 : :
467 : 407016 : const DeltaRational ceiling(getValue().ceiling());
468 : 271344 : return d_database->getConstraint(getVariable(), getType(), ceiling);
469 : : }
470 : :
471 : 2601710 : ConstraintP Constraint::getFloor() {
472 [ - + ][ - + ]: 2601710 : Assert(getValue().getInfinitesimalPart().sgn() < 0);
[ - - ]
473 : :
474 : 7805140 : const DeltaRational floor(Rational(getValue().floor()));
475 : 5203430 : return d_database->getConstraint(getVariable(), getType(), floor);
476 : : }
477 : :
478 : 1756180 : void Constraint::setCanBePropagated() {
479 [ - + ][ - + ]: 1756180 : Assert(!canBePropagated());
[ - - ]
480 : 1756180 : d_database->pushCanBePropagatedWatch(this);
481 : 1756180 : }
482 : :
483 : 11615400 : void Constraint::setAssertedToTheTheory(TNode witness, bool nowInConflict) {
484 [ - + ][ - + ]: 11615400 : Assert(hasLiteral());
[ - - ]
485 [ - + ][ - + ]: 11615400 : Assert(!assertedToTheTheory());
[ - - ]
486 [ - + ][ - + ]: 11615400 : Assert(negationHasProof() == nowInConflict);
[ - - ]
487 : 11615400 : d_database->pushAssertionOrderWatch(this, witness);
488 : :
489 : 11615400 : if(TraceIsOn("constraint::conflictCommit") && nowInConflict ){
490 [ - - ]: 0 : Trace("constraint::conflictCommit") << "inConflict@setAssertedToTheTheory";
491 [ - - ]: 0 : Trace("constraint::conflictCommit") << "\t" << this << std::endl;
492 [ - - ]: 0 : Trace("constraint::conflictCommit") << "\t" << getNegation() << std::endl;
493 : 0 : Trace("constraint::conflictCommit") << "\t" << getNegation()->externalExplainByAssertions() << std::endl;
494 : :
495 : : }
496 : 11615400 : }
497 : :
498 : 0 : bool Constraint::satisfiedBy(const DeltaRational& dr) const {
499 [ - - ][ - - ]: 0 : switch(getType()){
[ - ]
500 : 0 : case LowerBound:
501 : 0 : return getValue() <= dr;
502 : 0 : case Equality:
503 : 0 : return getValue() == dr;
504 : 0 : case UpperBound:
505 : 0 : return getValue() >= dr;
506 : 0 : case Disequality:
507 : 0 : return getValue() != dr;
508 : : }
509 : 0 : Unreachable();
510 : : }
511 : :
512 : 19729100 : bool Constraint::isInternalAssumption() const {
513 : 19729100 : return getProofType() == InternalAssumeAP;
514 : : }
515 : :
516 : 0 : TrustNode Constraint::externalExplainByAssertions() const
517 : : {
518 : 0 : NodeBuilder nb(d_database->nodeManager(), Kind::AND);
519 : 0 : auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel);
520 : 0 : Node exp = mkAndFromBuilder(d_database->nodeManager(), nb);
521 [ - - ]: 0 : if (d_database->isProofEnabled())
522 : : {
523 : 0 : std::vector<Node> assumptions;
524 [ - - ]: 0 : if (exp.getKind() == Kind::AND)
525 : : {
526 : 0 : assumptions.insert(assumptions.end(), exp.begin(), exp.end());
527 : : }
528 : : else
529 : : {
530 : 0 : assumptions.push_back(exp);
531 : : }
532 : 0 : auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
533 : 0 : return d_database->d_pfGen->mkTrustedPropagation(
534 : 0 : getLiteral(), d_database->nodeManager()->mkAnd(assumptions), pf);
535 : : }
536 : 0 : return TrustNode::mkTrustPropExp(getLiteral(), exp);
537 : : }
538 : :
539 : 21164500 : bool Constraint::isAssumption() const {
540 : 21164500 : return getProofType() == AssumeAP;
541 : : }
542 : :
543 : 1419650 : bool Constraint::hasEqualityEngineProof() const {
544 : 1419650 : return getProofType() == EqualityEngineAP;
545 : : }
546 : :
547 : 0 : bool Constraint::hasFarkasProof() const {
548 : 0 : return getProofType() == FarkasAP;
549 : : }
550 : :
551 : 0 : bool Constraint::hasSimpleFarkasProof() const
552 : : {
553 [ - - ]: 0 : Trace("constraints::hsfp") << "hasSimpleFarkasProof " << this << std::endl;
554 [ - - ]: 0 : if (!hasFarkasProof())
555 : : {
556 [ - - ]: 0 : Trace("constraints::hsfp") << "There is no simple Farkas proof because "
557 : 0 : "there is no farkas proof."
558 : 0 : << std::endl;
559 : 0 : return false;
560 : : }
561 : :
562 : : // For each antecdent ...
563 : 0 : AntecedentId i = getConstraintRule().d_antecedentEnd;
564 [ - - ]: 0 : for (ConstraintCP a = d_database->getAntecedent(i); a != NullConstraint;
565 : 0 : a = d_database->getAntecedent(--i))
566 : : {
567 : : // ... that antecdent must be an assumption OR a tightened assumption ...
568 [ - - ]: 0 : if (a->isPossiblyTightenedAssumption())
569 : : {
570 : 0 : continue;
571 : : }
572 : :
573 : : // ... otherwise, we do not have a simple Farkas proof.
574 [ - - ]: 0 : if (TraceIsOn("constraints::hsfp"))
575 : : {
576 [ - - ]: 0 : Trace("constraints::hsfp") << "There is no simple Farkas proof b/c there "
577 : 0 : "is an antecdent w/ rule ";
578 [ - - ]: 0 : a->getConstraintRule().print(Trace("constraints::hsfp"), d_produceProofs);
579 [ - - ]: 0 : Trace("constraints::hsfp") << std::endl;
580 : : }
581 : :
582 : 0 : return false;
583 : : }
584 : 0 : return true;
585 : : }
586 : :
587 : 0 : bool Constraint::isPossiblyTightenedAssumption() const
588 : : {
589 : : // ... that antecdent must be an assumption ...
590 : :
591 [ - - ]: 0 : if (isAssumption()) return true;
592 [ - - ]: 0 : if (!hasIntTightenProof()) return false;
593 [ - - ]: 0 : if (getConstraintRule().d_antecedentEnd == AntecedentIdSentinel) return false;
594 : 0 : return d_database->getAntecedent(getConstraintRule().d_antecedentEnd)
595 : 0 : ->isAssumption();
596 : : }
597 : :
598 : 0 : bool Constraint::hasIntTightenProof() const {
599 : 0 : return getProofType() == IntTightenAP;
600 : : }
601 : :
602 : 0 : bool Constraint::hasIntHoleProof() const {
603 : 0 : return getProofType() == IntHoleAP;
604 : : }
605 : :
606 : 0 : bool Constraint::hasTrichotomyProof() const {
607 : 0 : return getProofType() == TrichotomyAP;
608 : : }
609 : :
610 : 0 : void Constraint::printProofTree(std::ostream& out, size_t depth) const
611 : : {
612 [ - - ]: 0 : if (d_produceProofs)
613 : : {
614 : 0 : const ConstraintRule& rule = getConstraintRule();
615 : 0 : out << std::string(2 * depth, ' ') << "* " << getVariable() << " [";
616 : 0 : out << getProofLiteral();
617 [ - - ]: 0 : if (assertedToTheTheory())
618 : : {
619 : 0 : out << " | wit: " << getWitness();
620 : : }
621 : 0 : out << "]" << ' ' << getType() << ' ' << getValue() << " ("
622 : 0 : << getProofType() << ")";
623 [ - - ]: 0 : if (getProofType() == FarkasAP)
624 : : {
625 : 0 : out << " [";
626 : 0 : bool first = true;
627 [ - - ]: 0 : for (const auto& coeff : *rule.d_farkasCoefficients)
628 : : {
629 [ - - ]: 0 : if (!first)
630 : : {
631 : 0 : out << ", ";
632 : : }
633 : 0 : first = false;
634 : 0 : out << coeff;
635 : : }
636 : 0 : out << "]";
637 : : }
638 : 0 : out << endl;
639 : :
640 [ - - ]: 0 : for (AntecedentId i = rule.d_antecedentEnd; i != AntecedentIdSentinel; --i)
641 : : {
642 : 0 : ConstraintCP antecdent = d_database->getAntecedent(i);
643 [ - - ]: 0 : if (antecdent == NullConstraint)
644 : : {
645 : 0 : break;
646 : : }
647 : 0 : antecdent->printProofTree(out, depth + 1);
648 : : }
649 : 0 : return;
650 : : }
651 : 0 : out << "Cannot print proof. This is not a proof build." << endl;
652 : : }
653 : :
654 : 1169780 : bool Constraint::sanityChecking(Node n) const {
655 : 2339560 : Comparison cmp = Comparison::parseNormalForm(n);
656 : 1169780 : Kind k = cmp.comparisonKind();
657 : 2339560 : Polynomial pleft = cmp.normalizedVariablePart();
658 [ + + ][ + + ]: 1169780 : Assert(k == Kind::EQUAL || k == Kind::DISTINCT
[ - + ][ - + ]
[ - - ]
659 : : || pleft.leadingCoefficientIsPositive());
660 : 1169780 : Assert(
661 : : k != Kind::EQUAL
662 : : || Monomial::isMember(n[0].getKind() == Kind::TO_REAL ? n[0][0] : n[0]));
663 : 1169780 : Assert(k != Kind::DISTINCT
664 : : || Monomial::isMember(n[0][0].getKind() == Kind::TO_REAL ? n[0][0][0]
665 : : : n[0][0]));
666 : :
667 : 2339560 : TNode left = pleft.getNode();
668 : 2339560 : DeltaRational right = cmp.normalizedDeltaRational();
669 : :
670 : 1169780 : const ArithVariables& avariables = d_database->getArithVariables();
671 : :
672 [ + - ]: 1169780 : Trace("Constraint::sanityChecking") << cmp.getNode() << endl;
673 [ + - ]: 1169780 : Trace("Constraint::sanityChecking") << k << endl;
674 [ + - ]: 1169780 : Trace("Constraint::sanityChecking") << pleft.getNode() << endl;
675 [ + - ]: 1169780 : Trace("Constraint::sanityChecking") << left << endl;
676 [ + - ]: 1169780 : Trace("Constraint::sanityChecking") << right << endl;
677 [ + - ]: 1169780 : Trace("Constraint::sanityChecking") << getValue() << endl;
678 [ + - ][ - + ]: 1169780 : Trace("Constraint::sanityChecking") << avariables.hasArithVar(left) << endl;
[ - - ]
679 [ + - ][ - + ]: 1169780 : Trace("Constraint::sanityChecking") << avariables.asArithVar(left) << endl;
[ - - ]
680 [ + - ]: 1169780 : Trace("Constraint::sanityChecking") << getVariable() << endl;
681 : :
682 : :
683 [ + - ][ + - ]: 2339560 : if(avariables.hasArithVar(left) &&
[ - - ]
684 [ + - ][ + - ]: 2339560 : avariables.asArithVar(left) == getVariable() &&
[ + - ][ - - ]
685 [ + - ]: 1169780 : getValue() == right){
686 [ + + ][ + - ]: 1169780 : switch(getType()){
687 : 638832 : case LowerBound:
688 : : case UpperBound:
689 : : //Be overapproximate
690 [ + - ][ + + ]: 638832 : return k == Kind::GT || k == Kind::GEQ || k == Kind::LT || k == Kind::LEQ;
[ - + ][ - - ]
691 : 265475 : case Equality: return k == Kind::EQUAL;
692 : 265475 : case Disequality: return k == Kind::DISTINCT;
693 : 0 : default:
694 : 0 : Unreachable();
695 : : }
696 : : }else{
697 : 0 : return false;
698 : : }
699 : : }
700 : :
701 : 0 : ConstraintCP ConstraintDatabase::getAntecedent (AntecedentId p) const {
702 : 0 : Assert(p < d_antecedents.size());
703 : 0 : return d_antecedents[p];
704 : : }
705 : :
706 : 0 : void ConstraintRule::print(std::ostream& out, bool produceProofs) const
707 : : {
708 [ - - ]: 0 : RationalVectorCP coeffs = produceProofs ? d_farkasCoefficients : nullptr;
709 : 0 : out << "{ConstraintRule, ";
710 : 0 : out << d_constraint << std::endl;
711 : 0 : out << "d_proofType= " << d_proofType << ", " << std::endl;
712 : 0 : out << "d_antecedentEnd= "<< d_antecedentEnd << std::endl;
713 : :
714 [ - - ][ - - ]: 0 : if (d_constraint != NullConstraint && d_antecedentEnd != AntecedentIdSentinel)
715 : : {
716 : 0 : const ConstraintDatabase& database = d_constraint->getDatabase();
717 : :
718 [ - - ]: 0 : size_t coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffs->size()-1 : 0;
719 : 0 : AntecedentId p = d_antecedentEnd;
720 : : // must have at least one antecedent
721 : 0 : ConstraintCP antecedent = database.getAntecedent(p);
722 [ - - ]: 0 : while(antecedent != NullConstraint){
723 [ - - ]: 0 : if(coeffs != RationalVectorCPSentinel){
724 : 0 : out << coeffs->at(coeffIterator);
725 : : } else {
726 : 0 : out << "_";
727 : : }
728 : 0 : out << " * (" << *antecedent << ")" << std::endl;
729 : :
730 : 0 : Assert((coeffs == RationalVectorCPSentinel) || coeffIterator > 0);
731 : 0 : --p;
732 [ - - ]: 0 : coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffIterator-1 : 0;
733 : 0 : antecedent = database.getAntecedent(p);
734 : : }
735 [ - - ]: 0 : if(coeffs != RationalVectorCPSentinel){
736 : 0 : out << coeffs->front();
737 : : } else {
738 : 0 : out << "_";
739 : : }
740 : 0 : out << " * (" << *(d_constraint->getNegation()) << ")";
741 : 0 : out << " [not d_constraint] " << endl;
742 : : }
743 : 0 : out << "}";
744 : 0 : }
745 : :
746 : 3959530 : bool Constraint::wellFormedFarkasProof(NodeManager* nm) const
747 : : {
748 [ - + ][ - + ]: 3959530 : Assert(hasProof());
[ - - ]
749 : :
750 : 3959530 : const ConstraintRule& cr = getConstraintRule();
751 [ - + ]: 3959530 : if(cr.d_constraint != this){ return false; }
752 [ - + ]: 3959530 : if(cr.d_proofType != FarkasAP){ return false; }
753 : :
754 : 3959530 : AntecedentId p = cr.d_antecedentEnd;
755 : :
756 : : // must have at least one antecedent
757 : 3959530 : ConstraintCP antecedent = d_database->d_antecedents[p];
758 [ - + ]: 3959530 : if(antecedent == NullConstraint) { return false; }
759 : :
760 [ + + ]: 3959530 : if (!d_produceProofs)
761 : : {
762 : 1171930 : return cr.d_farkasCoefficients == RationalVectorCPSentinel;
763 : : }
764 [ - + ][ - + ]: 2787600 : Assert(d_produceProofs);
[ - - ]
765 : :
766 [ - + ]: 2787600 : if(cr.d_farkasCoefficients == RationalVectorCPSentinel){ return false; }
767 [ - + ]: 2787600 : if(cr.d_farkasCoefficients->size() < 2){ return false; }
768 : :
769 : 2787600 : const ArithVariables& vars = d_database->getArithVariables();
770 : :
771 : 5575200 : DeltaRational rhs(0);
772 : 5575200 : Node lhs = Polynomial::mkZero(nm).getNode();
773 : :
774 : 2787600 : RationalVector::const_iterator coeffIterator = cr.d_farkasCoefficients->end()-1;
775 : 2787600 : RationalVector::const_iterator coeffBegin = cr.d_farkasCoefficients->begin();
776 : :
777 [ + + ]: 6471120 : while(antecedent != NullConstraint){
778 : 3683520 : Assert(lhs.isNull() || Polynomial::isMember(lhs));
779 : :
780 : 3683520 : const Rational& coeff = *coeffIterator;
781 : 3683520 : int coeffSgn = coeff.sgn();
782 : :
783 : 3683520 : rhs += antecedent->getValue() * coeff;
784 : :
785 : 3683520 : ArithVar antVar = antecedent->getVariable();
786 [ + - ][ + - ]: 3683520 : if(!lhs.isNull() && vars.hasNode(antVar)){
[ + - ]
787 : 7367030 : Node antAsNode = vars.asNode(antVar);
788 [ + - ]: 3683520 : if(Polynomial::isMember(antAsNode)){
789 : 7367030 : Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
790 : 7367030 : Polynomial antPoly = Polynomial::parsePolynomial(antAsNode);
791 : 7367030 : Polynomial sum = lhsPoly + (antPoly * coeff);
792 : 3683520 : lhs = sum.getNode();
793 : : }else{
794 : 0 : lhs = Node::null();
795 : : }
796 : : } else {
797 : 0 : lhs = Node::null();
798 : : }
799 [ + - ]: 3683520 : Trace("constraints::wffp") << "running sum: " << lhs << " <= " << rhs << endl;
800 : :
801 [ + + ][ + - ]: 3683520 : switch( antecedent->getType() ){
802 : 1483540 : case LowerBound:
803 : : // fc[l] < 0, therefore return false if coeffSgn >= 0
804 [ - + ]: 1483540 : if(coeffSgn >= 0){ return false; }
805 : 1483540 : break;
806 : 551089 : case UpperBound:
807 : : // fc[u] > 0, therefore return false if coeffSgn <= 0
808 [ - + ]: 551089 : if(coeffSgn <= 0){ return false; }
809 : 551089 : break;
810 : 1648890 : case Equality:
811 [ - + ]: 1648890 : if(coeffSgn == 0) { return false; }
812 : 1648890 : break;
813 : 0 : case Disequality:
814 : : default:
815 : 0 : return false;
816 : : }
817 : :
818 [ - + ]: 3683520 : if(coeffIterator == coeffBegin){ return false; }
819 : 3683520 : --coeffIterator;
820 : 3683520 : --p;
821 : 3683520 : antecedent = d_database->d_antecedents[p];
822 : : }
823 [ - + ]: 2787600 : if(coeffIterator != coeffBegin){ return false; }
824 : :
825 : 2787600 : const Rational& firstCoeff = (*coeffBegin);
826 : 2787600 : int firstCoeffSgn = firstCoeff.sgn();
827 : 2787600 : rhs += (getNegation()->getValue()) * firstCoeff;
828 [ + - ][ + - ]: 2787600 : if(!lhs.isNull() && vars.hasNode(getVariable())){
[ + - ]
829 : 5575200 : Node firstAsNode = vars.asNode(getVariable());
830 [ + - ]: 2787600 : if(Polynomial::isMember(firstAsNode)){
831 : 5575200 : Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
832 : 5575200 : Polynomial firstPoly = Polynomial::parsePolynomial(firstAsNode);
833 : 5575200 : Polynomial sum = lhsPoly + (firstPoly * firstCoeff);
834 : 2787600 : lhs = sum.getNode();
835 : : }else{
836 : 0 : lhs = Node::null();
837 : : }
838 : : }else{
839 : 0 : lhs = Node::null();
840 : : }
841 : :
842 [ + + ][ + - ]: 2787600 : switch( getNegation()->getType() ){
843 : 592720 : case LowerBound:
844 : : // fc[l] < 0, therefore return false if coeffSgn >= 0
845 [ - + ]: 592720 : if(firstCoeffSgn >= 0){ return false; }
846 : 592720 : break;
847 : 1198830 : case UpperBound:
848 : : // fc[u] > 0, therefore return false if coeffSgn <= 0
849 [ - + ]: 1198830 : if(firstCoeffSgn <= 0){ return false; }
850 : 1198830 : break;
851 : 996046 : case Equality:
852 [ - + ]: 996046 : if(firstCoeffSgn == 0) { return false; }
853 : 996046 : break;
854 : 0 : case Disequality:
855 : : default:
856 : 0 : return false;
857 : : }
858 [ + - ]: 2787600 : Trace("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl;
859 : : // 0 = lhs <= rhs < 0
860 : 5575200 : return (lhs.isNull() || (Constant::isMember(lhs) && Constant(lhs).isZero()))
861 [ + - ][ + - ]: 5575200 : && rhs.sgn() < 0;
[ + - ]
862 : : }
863 : :
864 : 154824 : ConstraintP Constraint::makeNegation(ArithVar v,
865 : : ConstraintType t,
866 : : const DeltaRational& r,
867 : : bool produceProofs)
868 : : {
869 [ + + ][ + - ]: 154824 : switch(t){
[ - ]
870 : 6427 : case LowerBound:
871 : : {
872 [ - + ][ - + ]: 6427 : Assert(r.infinitesimalSgn() >= 0);
[ - - ]
873 [ - + ]: 6427 : if(r.infinitesimalSgn() > 0){
874 : 0 : Assert(r.getInfinitesimalPart() == 1);
875 : : // make (not (v > r)), which is (v <= r)
876 : 0 : DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
877 : 0 : return new Constraint(v, UpperBound, dropInf, produceProofs);
878 : : }else{
879 [ - + ][ - + ]: 6427 : Assert(r.infinitesimalSgn() == 0);
[ - - ]
880 : : // make (not (v >= r)), which is (v < r)
881 : 6427 : DeltaRational addInf(r.getNoninfinitesimalPart(), -1);
882 : 6427 : return new Constraint(v, UpperBound, addInf, produceProofs);
883 : : }
884 : : }
885 : 139260 : case UpperBound:
886 : : {
887 [ - + ][ - + ]: 139260 : Assert(r.infinitesimalSgn() <= 0);
[ - - ]
888 [ - + ]: 139260 : if(r.infinitesimalSgn() < 0){
889 : 0 : Assert(r.getInfinitesimalPart() == -1);
890 : : // make (not (v < r)), which is (v >= r)
891 : 0 : DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
892 : 0 : return new Constraint(v, LowerBound, dropInf, produceProofs);
893 : : }else{
894 [ - + ][ - + ]: 139260 : Assert(r.infinitesimalSgn() == 0);
[ - - ]
895 : : // make (not (v <= r)), which is (v > r)
896 : 139260 : DeltaRational addInf(r.getNoninfinitesimalPart(), 1);
897 : 139260 : return new Constraint(v, LowerBound, addInf, produceProofs);
898 : : }
899 : : }
900 : 9137 : case Equality: return new Constraint(v, Disequality, r, produceProofs);
901 : 0 : case Disequality: return new Constraint(v, Equality, r, produceProofs);
902 : 0 : default: Unreachable(); return NullConstraint;
903 : : }
904 : : }
905 : :
906 : 50287 : ConstraintDatabase::ConstraintDatabase(Env& env,
907 : : const ArithVariables& avars,
908 : : ArithCongruenceManager& cm,
909 : : RaiseConflict raiseConflict,
910 : 50287 : EagerProofGenerator* pfGen)
911 : : : EnvObj(env),
912 : : d_varDatabases(),
913 : : d_toPropagate(context()),
914 : : d_antecedents(context(), false),
915 : 50287 : d_watches(new Watches(context(), userContext())),
916 : : d_avariables(avars),
917 : : d_congruenceManager(cm),
918 : : d_pfGen(pfGen),
919 [ + + ]: 50287 : d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
920 : : : nullptr),
921 : : d_raiseConflict(raiseConflict),
922 : : d_one(1),
923 : : d_negOne(-1),
924 : 150861 : d_statistics(statisticsRegistry())
925 : : {
926 : 50287 : }
927 : :
928 : 14348900 : SortedConstraintMap& ConstraintDatabase::getVariableSCM(ArithVar v) const{
929 [ - + ][ - + ]: 14348900 : Assert(variableDatabaseIsSetup(v));
[ - - ]
930 : 14348900 : return d_varDatabases[v]->d_constraints;
931 : : }
932 : :
933 : 71094 : void ConstraintDatabase::pushSplitWatch(ConstraintP c){
934 [ - + ][ - + ]: 71094 : Assert(!c->d_split);
[ - - ]
935 : 71094 : c->d_split = true;
936 : 71094 : d_watches->d_splitWatches.push_back(c);
937 : 71094 : }
938 : :
939 : :
940 : 1756180 : void ConstraintDatabase::pushCanBePropagatedWatch(ConstraintP c){
941 [ - + ][ - + ]: 1756180 : Assert(!c->d_canBePropagated);
[ - - ]
942 : 1756180 : c->d_canBePropagated = true;
943 : 1756180 : d_watches->d_canBePropagatedWatches.push_back(c);
944 : 1756180 : }
945 : :
946 : 11615400 : void ConstraintDatabase::pushAssertionOrderWatch(ConstraintP c, TNode witness){
947 [ - + ][ - + ]: 11615400 : Assert(!c->assertedToTheTheory());
[ - - ]
948 : 11615400 : c->d_assertionOrder = d_watches->d_assertionOrderWatches.size();
949 : 11615400 : c->d_witness = witness;
950 : 11615400 : d_watches->d_assertionOrderWatches.push_back(c);
951 : 11615400 : }
952 : :
953 : :
954 : 17808600 : void ConstraintDatabase::pushConstraintRule(const ConstraintRule& crp){
955 : 17808600 : ConstraintP c = crp.d_constraint;
956 [ - + ][ - + ]: 17808600 : Assert(c->d_crid == ConstraintRuleIdSentinel);
[ - - ]
957 [ - + ][ - + ]: 17808600 : Assert(!c->hasProof());
[ - - ]
958 : 17808600 : c->d_crid = d_watches->d_constraintProofs.size();
959 : 17808600 : d_watches->d_constraintProofs.push_back(crp);
960 : 17808600 : }
961 : :
962 : 3581760 : ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){
963 : : //This must always return a constraint.
964 : :
965 : 3581760 : SortedConstraintMap& scm = getVariableSCM(v);
966 : 3581760 : pair<SortedConstraintMapIterator, bool> insertAttempt;
967 : 3581760 : insertAttempt = scm.insert(make_pair(r, ValueCollection()));
968 : :
969 : 3581760 : SortedConstraintMapIterator pos = insertAttempt.first;
970 : 3581760 : ValueCollection& vc = pos->second;
971 [ + + ]: 3581760 : if(vc.hasConstraintOfType(t)){
972 : 3426930 : return vc.getConstraintOfType(t);
973 : : }else{
974 : 154824 : ConstraintP c = new Constraint(v, t, r, options().smt.produceProofs);
975 : : ConstraintP negC =
976 : 154824 : Constraint::makeNegation(v, t, r, options().smt.produceProofs);
977 : :
978 : 154824 : SortedConstraintMapIterator negPos;
979 [ + + ][ - + ]: 154824 : if(t == Equality || t == Disequality){
980 : 9137 : negPos = pos;
981 : : }else{
982 : 145687 : pair<SortedConstraintMapIterator, bool> negInsertAttempt;
983 : 145687 : negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection()));
984 [ - + ][ - - ]: 145687 : Assert(negInsertAttempt.second
[ - + ][ - - ]
985 : : || !negInsertAttempt.first->second.hasConstraintOfType(
986 : : negC->getType()));
987 : 145687 : negPos = negInsertAttempt.first;
988 : : }
989 : :
990 : 154824 : c->initialize(this, pos, negC);
991 : 154824 : negC->initialize(this, negPos, c);
992 : :
993 : 154824 : vc.add(c);
994 : 154824 : negPos->second.add(negC);
995 : :
996 : 154824 : return c;
997 : : }
998 : : }
999 : :
1000 : 421789 : ConstraintP ConstraintDatabase::ensureConstraint(ValueCollection& vc, ConstraintType t){
1001 [ + + ]: 421789 : if(vc.hasConstraintOfType(t)){
1002 : 406718 : return vc.getConstraintOfType(t);
1003 : : }else{
1004 : 15071 : return getConstraint(vc.getVariable(), t, vc.getValue());
1005 : : }
1006 : : }
1007 : :
1008 : 0 : bool ConstraintDatabase::emptyDatabase(const std::vector<PerVariableDatabase>& vec){
1009 : 0 : std::vector<PerVariableDatabase>::const_iterator first = vec.begin();
1010 : 0 : std::vector<PerVariableDatabase>::const_iterator last = vec.end();
1011 : 0 : return std::find_if(first, last, PerVariableDatabase::IsEmpty) == last;
1012 : : }
1013 : :
1014 : 49942 : ConstraintDatabase::~ConstraintDatabase(){
1015 [ + - ]: 49942 : delete d_watches;
1016 : :
1017 : 49942 : std::vector<ConstraintP> constraintList;
1018 : :
1019 [ + + ]: 409056 : while(!d_varDatabases.empty()){
1020 : 359114 : PerVariableDatabase* back = d_varDatabases.back();
1021 : :
1022 : 359114 : SortedConstraintMap& scm = back->d_constraints;
1023 : 359114 : SortedConstraintMapIterator i = scm.begin(), i_end = scm.end();
1024 [ + + ]: 1364040 : for(; i != i_end; ++i){
1025 : 1004920 : (i->second).push_into(constraintList);
1026 : : }
1027 [ + + ]: 1831340 : while(!constraintList.empty()){
1028 : 1472230 : ConstraintP c = constraintList.back();
1029 : 1472230 : constraintList.pop_back();
1030 [ + - ]: 1472230 : delete c;
1031 : : }
1032 [ - + ][ - + ]: 359114 : Assert(scm.empty());
1033 : 359114 : d_varDatabases.pop_back();
1034 [ + - ]: 359114 : delete back;
1035 : : }
1036 : :
1037 [ - + ][ - + ]: 49942 : Assert(d_nodetoConstraintMap.empty());
1038 : 49942 : }
1039 : :
1040 : 50287 : ConstraintDatabase::Statistics::Statistics(StatisticsRegistry& sr)
1041 : : : d_unatePropagateCalls(
1042 : 50287 : sr.registerInt("theory::arith::cd::unatePropagateCalls")),
1043 : : d_unatePropagateImplications(
1044 : 50287 : sr.registerInt("theory::arith::cd::unatePropagateImplications"))
1045 : : {
1046 : 50287 : }
1047 : :
1048 : 0 : void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c){
1049 : 0 : Assert(c->safeToGarbageCollect());
1050 : 0 : ConstraintP neg = c->getNegation();
1051 : 0 : Assert(neg->safeToGarbageCollect());
1052 [ - - ]: 0 : delete c;
1053 [ - - ]: 0 : delete neg;
1054 : 0 : }
1055 : :
1056 : 363258 : void ConstraintDatabase::addVariable(ArithVar v){
1057 [ + + ]: 363258 : if(d_reclaimable.isMember(v)){
1058 : 3925 : SortedConstraintMap& scm = getVariableSCM(v);
1059 : :
1060 : 7850 : std::vector<ConstraintP> constraintList;
1061 : :
1062 [ - + ]: 3925 : for(SortedConstraintMapIterator i = scm.begin(), end = scm.end(); i != end; ++i){
1063 : 0 : (i->second).push_into(constraintList);
1064 : : }
1065 [ - + ]: 3925 : while(!constraintList.empty()){
1066 : 0 : ConstraintP c = constraintList.back();
1067 : 0 : constraintList.pop_back();
1068 : 0 : Assert(c->safeToGarbageCollect());
1069 [ - - ]: 0 : delete c;
1070 : : }
1071 [ - + ][ - + ]: 3925 : Assert(scm.empty());
[ - - ]
1072 : :
1073 : 3925 : d_reclaimable.remove(v);
1074 : : }else{
1075 [ + - ]: 359333 : Trace("arith::constraint") << "about to fail" << v << " " << d_varDatabases.size() << endl;
1076 [ - + ][ - + ]: 359333 : Assert(v == d_varDatabases.size());
[ - - ]
1077 : 359333 : d_varDatabases.push_back(new PerVariableDatabase(v));
1078 : : }
1079 : 363258 : }
1080 : :
1081 : 3943 : void ConstraintDatabase::removeVariable(ArithVar v){
1082 [ - + ][ - + ]: 3943 : Assert(!d_reclaimable.isMember(v));
[ - - ]
1083 : 3943 : d_reclaimable.add(v);
1084 : 3943 : }
1085 : :
1086 : 0 : bool Constraint::safeToGarbageCollect() const{
1087 : : // Do not call during destructor as getNegation() may be Null by this point
1088 : 0 : Assert(getNegation() != NullConstraint);
1089 [ - - ][ - - ]: 0 : return !contextDependentDataIsSet() && ! getNegation()->contextDependentDataIsSet();
1090 : : }
1091 : :
1092 : 1475420 : bool Constraint::contextDependentDataIsSet() const{
1093 [ + - ][ + - ]: 1475420 : return hasProof() || isSplit() || canBePropagated() || assertedToTheTheory();
[ + - ][ - + ]
1094 : : }
1095 : :
1096 : 35547 : TrustNode Constraint::split()
1097 : : {
1098 [ + + ][ - + ]: 35547 : Assert(isEquality() || isDisequality());
[ - + ][ - - ]
1099 : :
1100 : 35547 : bool isEq = isEquality();
1101 : :
1102 [ + + ]: 35547 : ConstraintP eq = isEq ? this : d_negation;
1103 [ + + ]: 35547 : ConstraintP diseq = isEq ? d_negation : this;
1104 : :
1105 : 71094 : TNode eqNode = eq->getLiteral();
1106 [ - + ][ - + ]: 35547 : Assert(eqNode.getKind() == Kind::EQUAL);
[ - - ]
1107 : 71094 : TNode lhs = eqNode[0];
1108 : 71094 : TNode rhs = eqNode[1];
1109 : :
1110 : 35547 : NodeManager* nm = d_database->nodeManager();
1111 : 106641 : Node leqNode = NodeBuilder(nm, Kind::LEQ) << lhs << rhs;
1112 : 106641 : Node ltNode = NodeBuilder(nm, Kind::LT) << lhs << rhs;
1113 : 106641 : Node gtNode = NodeBuilder(nm, Kind::GT) << lhs << rhs;
1114 : 106641 : Node geqNode = NodeBuilder(nm, Kind::GEQ) << lhs << rhs;
1115 : :
1116 : 106641 : Node lemma = NodeBuilder(nm, Kind::OR) << leqNode << geqNode;
1117 : :
1118 : 35547 : TrustNode trustedLemma;
1119 [ + + ]: 35547 : if (d_database->isProofEnabled())
1120 : : {
1121 : 24812 : TypeNode type = lhs.getType();
1122 : : // Farkas proof that this works.
1123 : 24812 : auto nLeqPf = d_database->d_pnm->mkAssume(leqNode.negate());
1124 : 24812 : auto gtPf = ensurePredTransform(d_database->d_pnm, nLeqPf, gtNode);
1125 : 24812 : auto nGeqPf = d_database->d_pnm->mkAssume(geqNode.negate());
1126 : 24812 : auto ltPf = ensurePredTransform(d_database->d_pnm, nGeqPf, ltNode);
1127 : 62030 : std::vector<Pf> args{gtPf, ltPf};
1128 : 74436 : std::vector<Node> coeffs{nm->mkConstReal(-1), nm->mkConstReal(1)};
1129 : 24812 : std::vector<Node> coeffsUse = getMacroSumUbCoeff(nm, args, coeffs);
1130 : 12406 : auto sumPf = d_database->d_pnm->mkNode(
1131 : 24812 : ProofRule::MACRO_ARITH_SCALE_SUM_UB, args, coeffsUse);
1132 : : auto botPf =
1133 : 24812 : ensurePredTransform(d_database->d_pnm, sumPf, nm->mkConst(false));
1134 : 62030 : std::vector<Node> a = {leqNode.negate(), geqNode.negate()};
1135 : 37218 : auto notAndNotPf = d_database->d_pnm->mkScope(botPf, a);
1136 : : // No need to ensure that the expected node aggrees with `a` because we are
1137 : : // not providing an expected node.
1138 : : auto orNotNotPf =
1139 : 62030 : d_database->d_pnm->mkNode(ProofRule::NOT_AND, {notAndNotPf}, {});
1140 : 12406 : auto orPf = ensurePredTransform(d_database->d_pnm, orNotNotPf, lemma);
1141 : 12406 : trustedLemma = d_database->d_pfGen->mkTrustNode(lemma, orPf);
1142 : : }
1143 : : else
1144 : : {
1145 : 23141 : trustedLemma = TrustNode::mkTrustLemma(lemma);
1146 : : }
1147 : :
1148 : 35547 : eq->d_database->pushSplitWatch(eq);
1149 : 35547 : diseq->d_database->pushSplitWatch(diseq);
1150 : :
1151 : 71094 : return trustedLemma;
1152 : : }
1153 : :
1154 : 2339560 : bool ConstraintDatabase::hasLiteral(TNode literal) const {
1155 : 2339560 : return lookup(literal) != NullConstraint;
1156 : : }
1157 : :
1158 : 584891 : ConstraintP ConstraintDatabase::addLiteral(TNode literal){
1159 [ - + ][ - + ]: 584891 : Assert(!hasLiteral(literal));
[ - - ]
1160 : 584891 : bool isNot = (literal.getKind() == Kind::NOT);
1161 [ - + ]: 1169780 : Node atomNode = (isNot ? literal[0] : literal);
1162 : 1169780 : Node negationNode = atomNode.notNode();
1163 : :
1164 [ - + ][ - + ]: 584891 : Assert(!hasLiteral(atomNode));
[ - - ]
1165 [ - + ][ - + ]: 584891 : Assert(!hasLiteral(negationNode));
[ - - ]
1166 : 1169780 : Comparison posCmp = Comparison::parseNormalForm(atomNode);
1167 : :
1168 : 584891 : ConstraintType posType = Constraint::constraintTypeOfComparison(posCmp);
1169 : :
1170 : 1169780 : Polynomial nvp = posCmp.normalizedVariablePart();
1171 : 584891 : ArithVar v = d_avariables.asArithVar(nvp.getNode());
1172 : :
1173 : 1169780 : DeltaRational posDR = posCmp.normalizedDeltaRational();
1174 : :
1175 : : ConstraintP posC =
1176 : 584891 : new Constraint(v, posType, posDR, options().smt.produceProofs);
1177 : :
1178 [ + - ]: 584891 : Trace("arith::constraint") << "addliteral( literal ->" << literal << ")" << endl;
1179 [ + - ]: 584891 : Trace("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl;
1180 : :
1181 : 584891 : SortedConstraintMap& scm = getVariableSCM(posC->getVariable());
1182 : 584891 : pair<SortedConstraintMapIterator, bool> insertAttempt;
1183 : 584891 : insertAttempt = scm.insert(make_pair(posC->getValue(), ValueCollection()));
1184 : :
1185 : 584891 : SortedConstraintMapIterator posI = insertAttempt.first;
1186 : : // If the attempt succeeds, i points to a new empty ValueCollection
1187 : : // If the attempt fails, i points to a pre-existing ValueCollection
1188 : :
1189 [ + + ]: 584891 : if(posI->second.hasConstraintOfType(posC->getType())){
1190 : : //This is the situation where the ConstraintP exists, but
1191 : : //the literal has not been associated with it.
1192 : 3195 : ConstraintP hit = posI->second.getConstraintOfType(posC->getType());
1193 [ + - ]: 3195 : Trace("arith::constraint") << "hit " << hit << endl;
1194 [ + - ]: 3195 : Trace("arith::constraint") << "posC " << posC << endl;
1195 : :
1196 [ + - ]: 3195 : delete posC;
1197 : :
1198 : 3195 : hit->setLiteral(atomNode);
1199 : 3195 : hit->getNegation()->setLiteral(negationNode);
1200 [ - + ]: 3195 : return isNot ? hit->getNegation(): hit;
1201 : : }else{
1202 : 1163390 : Comparison negCmp = Comparison::parseNormalForm(negationNode);
1203 : :
1204 : 581696 : ConstraintType negType = Constraint::constraintTypeOfComparison(negCmp);
1205 : 581696 : DeltaRational negDR = negCmp.normalizedDeltaRational();
1206 : :
1207 : : ConstraintP negC =
1208 : 581696 : new Constraint(v, negType, negDR, options().smt.produceProofs);
1209 : :
1210 : 581696 : SortedConstraintMapIterator negI;
1211 : :
1212 [ + + ]: 581696 : if(posC->isEquality()){
1213 : 264983 : negI = posI;
1214 : : }else{
1215 [ + + ][ - + ]: 316713 : Assert(posC->isLowerBound() || posC->isUpperBound());
[ - + ][ - - ]
1216 : :
1217 : 316713 : pair<SortedConstraintMapIterator, bool> negInsertAttempt;
1218 : 316713 : negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection()));
1219 : :
1220 [ + - ]: 316713 : Trace("nf::tmp") << "sdhjfgdhjkldfgljkhdfg" << endl;
1221 [ + - ]: 316713 : Trace("nf::tmp") << negC << endl;
1222 [ + - ]: 316713 : Trace("nf::tmp") << negC->getValue() << endl;
1223 : :
1224 : : //This should always succeed as the DeltaRational for the negation is unique!
1225 [ - + ][ - + ]: 316713 : Assert(negInsertAttempt.second);
[ - - ]
1226 : :
1227 : 316713 : negI = negInsertAttempt.first;
1228 : : }
1229 : :
1230 : 581696 : (posI->second).add(posC);
1231 : 581696 : (negI->second).add(negC);
1232 : :
1233 : 581696 : posC->initialize(this, posI, negC);
1234 : 581696 : negC->initialize(this, negI, posC);
1235 : :
1236 : 581696 : posC->setLiteral(atomNode);
1237 : 581696 : negC->setLiteral(negationNode);
1238 : :
1239 [ - + ]: 581696 : return isNot ? negC : posC;
1240 : : }
1241 : : }
1242 : :
1243 : :
1244 : 20223800 : ConstraintP ConstraintDatabase::lookup(TNode literal) const{
1245 : 20223800 : NodetoConstraintMap::const_iterator iter = d_nodetoConstraintMap.find(literal);
1246 [ + + ]: 20223800 : if(iter == d_nodetoConstraintMap.end()){
1247 : 4101070 : return NullConstraint;
1248 : : }else{
1249 : 16122700 : return iter->second;
1250 : : }
1251 : : }
1252 : :
1253 : 9964580 : void Constraint::setAssumption(bool nowInConflict){
1254 [ + - ]: 9964580 : Trace("constraints::pf") << "setAssumption(" << this << ")" << std::endl;
1255 [ - + ][ - + ]: 9964580 : Assert(!hasProof());
[ - - ]
1256 [ - + ][ - + ]: 9964580 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1257 [ - + ][ - + ]: 9964580 : Assert(hasLiteral());
[ - - ]
1258 [ - + ][ - + ]: 9964580 : Assert(assertedToTheTheory());
[ - - ]
1259 : :
1260 : 9964580 : d_database->pushConstraintRule(ConstraintRule(this, AssumeAP));
1261 : :
1262 [ - + ][ - + ]: 9964580 : Assert(inConflict() == nowInConflict);
[ - - ]
1263 : 9964580 : if(TraceIsOn("constraint::conflictCommit") && inConflict()){
1264 [ - - ]: 0 : Trace("constraint::conflictCommit") << "inConflict@setAssumption " << this << std::endl;
1265 : : }
1266 : 9964580 : }
1267 : :
1268 : 7360910 : void Constraint::tryToPropagate(){
1269 [ - + ][ - + ]: 7360910 : Assert(hasProof());
[ - - ]
1270 [ - + ][ - + ]: 7360910 : Assert(!isAssumption());
[ - - ]
1271 [ - + ][ - + ]: 7360910 : Assert(!isInternalAssumption());
[ - - ]
1272 : :
1273 [ + + ][ + - ]: 7360910 : if(canBePropagated() && !assertedToTheTheory() && !isAssumption() && !isInternalAssumption()){
[ + - ][ + - ]
[ + + ]
1274 : 1353640 : propagate();
1275 : : }
1276 : 7360910 : }
1277 : :
1278 : 1385550 : void Constraint::propagate(){
1279 [ - + ][ - + ]: 1385550 : Assert(hasProof());
[ - - ]
1280 [ - + ][ - + ]: 1385550 : Assert(canBePropagated());
[ - - ]
1281 [ - + ][ - + ]: 1385550 : Assert(!assertedToTheTheory());
[ - - ]
1282 [ - + ][ - + ]: 1385550 : Assert(!isAssumption());
[ - - ]
1283 [ - + ][ - + ]: 1385550 : Assert(!isInternalAssumption());
[ - - ]
1284 : :
1285 : 1385550 : d_database->d_toPropagate.push(this);
1286 : 1385550 : }
1287 : :
1288 : :
1289 : : /*
1290 : : * Example:
1291 : : * x <= a and a < b
1292 : : * |= x <= b
1293 : : * ---
1294 : : * 1*(x <= a) + (-1)*(x > b) => (0 <= a-b)
1295 : : */
1296 : 3792390 : void Constraint::impliedByUnate(NodeManager* nm,
1297 : : ConstraintCP imp,
1298 : : bool nowInConflict)
1299 : : {
1300 [ + - ]: 3792390 : Trace("constraints::pf") << "impliedByUnate(" << this << ", " << *imp << ")" << std::endl;
1301 [ - + ][ - + ]: 3792390 : Assert(!hasProof());
[ - - ]
1302 [ - + ][ - + ]: 3792390 : Assert(imp->hasProof());
[ - - ]
1303 [ - + ][ - + ]: 3792390 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1304 : :
1305 : 3792390 : d_database->d_antecedents.push_back(NullConstraint);
1306 : 3792390 : d_database->d_antecedents.push_back(imp);
1307 : :
1308 : 3792390 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1309 : :
1310 : : RationalVectorP coeffs;
1311 [ + + ]: 3792390 : if (d_produceProofs)
1312 : : {
1313 : 2674510 : std::pair<int, int> sgns = unateFarkasSigns(getNegation(), imp);
1314 : :
1315 : 5349030 : Rational first(sgns.first);
1316 : 5349030 : Rational second(sgns.second);
1317 : :
1318 : 2674510 : coeffs = new RationalVector();
1319 : 2674510 : coeffs->push_back(first);
1320 : 2674510 : coeffs->push_back(second);
1321 : : }
1322 : : else
1323 : : {
1324 : 1117870 : coeffs = RationalVectorPSentinel;
1325 : : }
1326 : : // no need to delete coeffs the memory is owned by ConstraintRule
1327 : 3792390 : d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffs));
1328 : :
1329 [ - + ][ - + ]: 3792390 : Assert(inConflict() == nowInConflict);
[ - - ]
1330 : 3792390 : if(TraceIsOn("constraint::conflictCommit") && inConflict()){
1331 [ - - ]: 0 : Trace("constraint::conflictCommit") << "inConflict@impliedByUnate " << this << std::endl;
1332 : : }
1333 : :
1334 : 3792390 : if (TraceIsOn("constraints::wffp") && !wellFormedFarkasProof(nm))
1335 : : {
1336 [ - - ]: 0 : getConstraintRule().print(Trace("constraints::wffp"), d_produceProofs);
1337 : : }
1338 [ - + ][ - + ]: 3792390 : Assert(wellFormedFarkasProof(nm));
[ - - ]
1339 : 3792390 : }
1340 : :
1341 : 1123490 : void Constraint::impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool nowInConflict){
1342 [ + - ]: 1123490 : Trace("constraints::pf") << "impliedByTrichotomy(" << this << ", " << *a << ", ";
1343 [ + - ]: 1123490 : Trace("constraints::pf") << *b << ")" << std::endl;
1344 [ - + ][ - + ]: 1123490 : Assert(!hasProof());
[ - - ]
1345 [ - + ][ - + ]: 1123490 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1346 [ - + ][ - + ]: 1123490 : Assert(a->hasProof());
[ - - ]
1347 [ - + ][ - + ]: 1123490 : Assert(b->hasProof());
[ - - ]
1348 : :
1349 : 1123490 : d_database->d_antecedents.push_back(NullConstraint);
1350 : 1123490 : d_database->d_antecedents.push_back(a);
1351 : 1123490 : d_database->d_antecedents.push_back(b);
1352 : :
1353 : 1123490 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1354 : 1123490 : d_database->pushConstraintRule(ConstraintRule(this, TrichotomyAP, antecedentEnd));
1355 : :
1356 [ - + ][ - + ]: 1123490 : Assert(inConflict() == nowInConflict);
[ - - ]
1357 : 1123490 : if(TraceIsOn("constraint::conflictCommit") && inConflict()){
1358 [ - - ]: 0 : Trace("constraint::conflictCommit") << "inConflict@impliedByTrichotomy " << this << std::endl;
1359 : : }
1360 : 1123490 : }
1361 : :
1362 : :
1363 : 167140 : bool Constraint::allHaveProof(const ConstraintCPVec& b){
1364 [ + + ]: 2189090 : for(ConstraintCPVec::const_iterator i=b.begin(), i_end=b.end(); i != i_end; ++i){
1365 : 2021950 : ConstraintCP cp = *i;
1366 [ - + ]: 2021950 : if(! (cp->hasProof())){ return false; }
1367 : : }
1368 : 167140 : return true;
1369 : : }
1370 : :
1371 : 2387520 : void Constraint::impliedByIntTighten(ConstraintCP a, bool nowInConflict){
1372 [ + - ]: 2387520 : Trace("constraints::pf") << "impliedByIntTighten(" << this << ", " << *a << ")" << std::endl;
1373 [ - + ][ - + ]: 2387520 : Assert(!hasProof());
[ - - ]
1374 [ - + ][ - + ]: 2387520 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1375 [ - + ][ - + ]: 2387520 : Assert(a->hasProof());
[ - - ]
1376 [ + - ]: 4775030 : Trace("pf::arith") << "impliedByIntTighten(" << this << ", " << a << ")"
1377 : 2387520 : << std::endl;
1378 : :
1379 : 2387520 : d_database->d_antecedents.push_back(NullConstraint);
1380 : 2387520 : d_database->d_antecedents.push_back(a);
1381 : 2387520 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1382 : 2387520 : d_database->pushConstraintRule(ConstraintRule(this, IntTightenAP, antecedentEnd));
1383 : :
1384 [ - + ][ - + ]: 2387520 : Assert(inConflict() == nowInConflict);
[ - - ]
1385 [ + + ]: 2387520 : if(inConflict()){
1386 [ + - ]: 3619 : Trace("constraint::conflictCommit") << "inConflict impliedByIntTighten" << this << std::endl;
1387 : : }
1388 : 2387520 : }
1389 : :
1390 : 0 : void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){
1391 [ - - ]: 0 : Trace("constraints::pf") << "impliedByIntHole(" << this << ", " << *a << ")" << std::endl;
1392 : 0 : Assert(!hasProof());
1393 : 0 : Assert(negationHasProof() == nowInConflict);
1394 : 0 : Assert(a->hasProof());
1395 [ - - ]: 0 : Trace("pf::arith") << "impliedByIntHole(" << this << ", " << a << ")"
1396 : 0 : << std::endl;
1397 : :
1398 : 0 : d_database->d_antecedents.push_back(NullConstraint);
1399 : 0 : d_database->d_antecedents.push_back(a);
1400 : 0 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1401 : 0 : d_database->pushConstraintRule(ConstraintRule(this, IntHoleAP, antecedentEnd));
1402 : :
1403 : 0 : Assert(inConflict() == nowInConflict);
1404 : 0 : if(TraceIsOn("constraint::conflictCommit") && inConflict()){
1405 [ - - ]: 0 : Trace("constraint::conflictCommit") << "inConflict impliedByIntHole" << this << std::endl;
1406 : : }
1407 : 0 : }
1408 : :
1409 : 0 : void Constraint::impliedByIntHole(const ConstraintCPVec& b, bool nowInConflict){
1410 [ - - ]: 0 : Trace("constraints::pf") << "impliedByIntHole(" << this;
1411 [ - - ]: 0 : if (TraceIsOn("constraints::pf")) {
1412 [ - - ]: 0 : for (const ConstraintCP& p : b)
1413 : : {
1414 [ - - ]: 0 : Trace("constraints::pf") << ", " << p;
1415 : : }
1416 : : }
1417 [ - - ]: 0 : Trace("constraints::pf") << ")" << std::endl;
1418 : :
1419 : 0 : Assert(!hasProof());
1420 : 0 : Assert(negationHasProof() == nowInConflict);
1421 : 0 : Assert(allHaveProof(b));
1422 : :
1423 : 0 : CDConstraintList& antecedents = d_database->d_antecedents;
1424 : 0 : antecedents.push_back(NullConstraint);
1425 [ - - ]: 0 : for(ConstraintCPVec::const_iterator i=b.begin(), i_end=b.end(); i != i_end; ++i){
1426 : 0 : antecedents.push_back(*i);
1427 : : }
1428 : 0 : AntecedentId antecedentEnd = antecedents.size() - 1;
1429 : :
1430 : 0 : d_database->pushConstraintRule(ConstraintRule(this, IntHoleAP, antecedentEnd));
1431 : :
1432 : 0 : Assert(inConflict() == nowInConflict);
1433 : 0 : if(TraceIsOn("constraint::conflictCommit") && inConflict()){
1434 [ - - ]: 0 : Trace("constraint::conflictCommit") << "inConflict@impliedByIntHole[vec] " << this << std::endl;
1435 : : }
1436 : 0 : }
1437 : :
1438 : : /*
1439 : : * If proofs are off, coeffs == RationalVectorSentinal.
1440 : : * If proofs are on,
1441 : : * coeffs != RationalVectorSentinal,
1442 : : * coeffs->size() = a.size() + 1,
1443 : : * for i in [0,a.size) : coeff[i] corresponds to a[i], and
1444 : : * coeff.back() corresponds to the current constraint.
1445 : : */
1446 : 167140 : void Constraint::impliedByFarkas(NodeManager* nm,
1447 : : const ConstraintCPVec& a,
1448 : : RationalVectorCP coeffs,
1449 : : bool nowInConflict)
1450 : : {
1451 [ + - ]: 167140 : Trace("constraints::pf") << "impliedByFarkas(" << this;
1452 [ - + ]: 167140 : if (TraceIsOn("constraints::pf")) {
1453 [ - - ]: 0 : for (const ConstraintCP& p : a)
1454 : : {
1455 [ - - ]: 0 : Trace("constraints::pf") << ", " << p;
1456 : : }
1457 : : }
1458 [ + - ]: 167140 : Trace("constraints::pf") << ", <coeffs>";
1459 [ + - ]: 167140 : Trace("constraints::pf") << ")" << std::endl;
1460 [ - + ][ - + ]: 167140 : Assert(!hasProof());
[ - - ]
1461 [ - + ][ - + ]: 167140 : Assert(negationHasProof() == nowInConflict);
[ - - ]
1462 [ - + ][ - + ]: 167140 : Assert(allHaveProof(a));
[ - - ]
1463 : :
1464 [ - + ][ - + ]: 167140 : Assert(d_produceProofs == (coeffs != RationalVectorCPSentinel));
[ - - ]
1465 [ + + ][ - + ]: 167140 : Assert(!d_produceProofs || coeffs->size() == a.size() + 1);
[ - + ][ - - ]
1466 : :
1467 [ - + ][ - + ]: 167140 : Assert(a.size() >= 1);
[ - - ]
1468 : :
1469 : 167140 : d_database->d_antecedents.push_back(NullConstraint);
1470 [ + + ]: 2189090 : for(ConstraintCPVec::const_iterator i = a.begin(), end = a.end(); i != end; ++i){
1471 : 2021950 : ConstraintCP c_i = *i;
1472 [ - + ][ - + ]: 2021950 : Assert(c_i->hasProof());
[ - - ]
1473 : 2021950 : d_database->d_antecedents.push_back(c_i);
1474 : : }
1475 : 167140 : AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
1476 : :
1477 : : RationalVectorCP coeffsCopy;
1478 [ + + ]: 167140 : if (d_produceProofs)
1479 : : {
1480 [ - + ][ - + ]: 113085 : Assert(coeffs != RationalVectorCPSentinel);
[ - - ]
1481 : 113085 : coeffsCopy = new RationalVector(*coeffs);
1482 : : }
1483 : : else
1484 : : {
1485 : 54055 : coeffsCopy = RationalVectorCPSentinel;
1486 : : }
1487 : 167140 : d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffsCopy));
1488 : :
1489 [ - + ][ - + ]: 167140 : Assert(inConflict() == nowInConflict);
[ - - ]
1490 : 167140 : if(TraceIsOn("constraint::conflictCommit") && inConflict()){
1491 [ - - ]: 0 : Trace("constraint::conflictCommit") << "inConflict@impliedByFarkas " << this << std::endl;
1492 : : }
1493 : 167140 : if (TraceIsOn("constraints::wffp") && !wellFormedFarkasProof(nm))
1494 : : {
1495 [ - - ]: 0 : getConstraintRule().print(Trace("constraints::wffp"), d_produceProofs);
1496 : : }
1497 [ - + ][ - + ]: 167140 : Assert(wellFormedFarkasProof(nm));
[ - - ]
1498 : 167140 : }
1499 : :
1500 : 0 : void Constraint::setInternalAssumption(bool nowInConflict){
1501 [ - - ]: 0 : Trace("constraints::pf") << "setInternalAssumption(" << this;
1502 [ - - ]: 0 : Trace("constraints::pf") << ")" << std::endl;
1503 : 0 : Assert(!hasProof());
1504 : 0 : Assert(negationHasProof() == nowInConflict);
1505 : 0 : Assert(!assertedToTheTheory());
1506 : :
1507 : 0 : d_database->pushConstraintRule(ConstraintRule(this, InternalAssumeAP));
1508 : :
1509 : 0 : Assert(inConflict() == nowInConflict);
1510 : 0 : if(TraceIsOn("constraint::conflictCommit") && inConflict()){
1511 [ - - ]: 0 : Trace("constraint::conflictCommit") << "inConflict@setInternalAssumption " << this << std::endl;
1512 : : }
1513 : 0 : }
1514 : :
1515 : :
1516 : 373448 : void Constraint::setEqualityEngineProof(){
1517 [ + - ]: 373448 : Trace("constraints::pf") << "setEqualityEngineProof(" << this;
1518 [ + - ]: 373448 : Trace("constraints::pf") << ")" << std::endl;
1519 [ - + ][ - + ]: 373448 : Assert(truthIsUnknown());
[ - - ]
1520 [ - + ][ - + ]: 373448 : Assert(hasLiteral());
[ - - ]
1521 : 373448 : d_database->pushConstraintRule(ConstraintRule(this, EqualityEngineAP));
1522 : 373448 : }
1523 : :
1524 : :
1525 : 8051770 : SortedConstraintMap& Constraint::constraintSet() const{
1526 [ - + ][ - + ]: 8051770 : Assert(d_database->variableDatabaseIsSetup(d_variable));
[ - - ]
1527 : 8051770 : return (d_database->d_varDatabases[d_variable])->d_constraints;
1528 : : }
1529 : :
1530 : 0 : bool Constraint::antecentListIsEmpty() const{
1531 : 0 : Assert(hasProof());
1532 : 0 : return d_database->d_antecedents[getEndAntecedent()] == NullConstraint;
1533 : : }
1534 : :
1535 : 0 : bool Constraint::antecedentListLengthIsOne() const {
1536 : 0 : Assert(hasProof());
1537 [ - - ]: 0 : return !antecentListIsEmpty() &&
1538 [ - - ]: 0 : d_database->d_antecedents[getEndAntecedent()-1] == NullConstraint;
1539 : : }
1540 : :
1541 : 173614 : Node Constraint::externalImplication(NodeManager* nm,
1542 : : const ConstraintCPVec& b) const
1543 : : {
1544 [ - + ][ - + ]: 173614 : Assert(hasLiteral());
[ - - ]
1545 : 347228 : Node antecedent = externalExplainByAssertions(nm, b);
1546 : 347228 : Node implied = getLiteral();
1547 : 347228 : return antecedent.impNode(implied);
1548 : : }
1549 : :
1550 : 194347 : Node Constraint::externalExplainByAssertions(NodeManager* nm,
1551 : : const ConstraintCPVec& b)
1552 : : {
1553 : 194347 : return externalExplain(nm, b, AssertionOrderSentinel);
1554 : : }
1555 : :
1556 : 16217 : TrustNode Constraint::externalExplainForPropagation(TNode lit) const
1557 : : {
1558 [ - + ][ - + ]: 16217 : Assert(hasProof());
[ - - ]
1559 [ - + ][ - + ]: 16217 : Assert(!isAssumption());
[ - - ]
1560 [ - + ][ - + ]: 16217 : Assert(!isInternalAssumption());
[ - - ]
1561 : 32434 : NodeBuilder nb(d_database->nodeManager(), Kind::AND);
1562 : 32434 : auto pfFromAssumptions = externalExplain(nb, d_assertionOrder);
1563 : 32434 : Node n = mkAndFromBuilder(d_database->nodeManager(), nb);
1564 [ + + ]: 16217 : if (d_database->isProofEnabled())
1565 : : {
1566 : 14136 : std::vector<Node> assumptions;
1567 [ + + ]: 7068 : if (n.getKind() == Kind::AND)
1568 : : {
1569 : 3362 : assumptions.insert(assumptions.end(), n.begin(), n.end());
1570 : : }
1571 : : else
1572 : : {
1573 : 3706 : assumptions.push_back(n);
1574 : : }
1575 [ + + ]: 7068 : if (getProofLiteral() != lit)
1576 : : {
1577 : : pfFromAssumptions =
1578 : 4079 : ensurePredTransform(d_database->d_pnm, pfFromAssumptions, lit);
1579 : : }
1580 : 14136 : auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
1581 : 7068 : return d_database->d_pfGen->mkTrustedPropagation(
1582 : 7068 : lit, d_database->nodeManager()->mkAnd(assumptions), pf);
1583 : : }
1584 : : else
1585 : : {
1586 : 9149 : return TrustNode::mkTrustPropExp(lit, n);
1587 : : }
1588 : : }
1589 : :
1590 : 116470 : TrustNode Constraint::externalExplainConflict() const
1591 : : {
1592 [ + - ]: 116470 : Trace("pf::arith::explain") << this << std::endl;
1593 [ - + ][ - + ]: 116470 : Assert(inConflict());
[ - - ]
1594 : 232940 : NodeBuilder nb(d_database->nodeManager(), Kind::AND);
1595 : 232940 : auto pf1 = externalExplainByAssertions(nb);
1596 : 232940 : auto not2 = getNegation()->getProofLiteral().negate();
1597 : 232940 : auto pf2 = getNegation()->externalExplainByAssertions(nb);
1598 : 232940 : Node n = mkAndFromBuilder(d_database->nodeManager(), nb);
1599 [ + + ]: 116470 : if (d_database->isProofEnabled())
1600 : : {
1601 : 100476 : auto pfNot2 = ensurePredTransform(d_database->d_pnm, pf1, not2);
1602 : 100476 : std::vector<Node> lits;
1603 [ + - ]: 50238 : if (n.getKind() == Kind::AND)
1604 : : {
1605 : 50238 : lits.insert(lits.end(), n.begin(), n.end());
1606 : : }
1607 : : else
1608 : : {
1609 : 0 : lits.push_back(n);
1610 : : }
1611 [ - + ]: 50238 : if (TraceIsOn("arith::pf::externalExplainConflict"))
1612 : : {
1613 [ - - ]: 0 : Trace("arith::pf::externalExplainConflict") << "Lits:" << std::endl;
1614 [ - - ]: 0 : for (const auto& l : lits)
1615 : : {
1616 [ - - ]: 0 : Trace("arith::pf::externalExplainConflict") << " : " << l << std::endl;
1617 : : }
1618 : : }
1619 : : std::vector<Node> contraLits = {getProofLiteral(),
1620 : 251190 : getNegation()->getProofLiteral()};
1621 : : auto bot =
1622 : 50238 : not2.getKind() == Kind::NOT
1623 : 95952 : ? d_database->d_pnm->mkNode(ProofRule::CONTRA, {pf2, pfNot2}, {})
1624 : 308214 : : d_database->d_pnm->mkNode(ProofRule::CONTRA, {pfNot2, pf2}, {});
1625 [ - + ]: 50238 : if (TraceIsOn("arith::pf::tree"))
1626 : : {
1627 [ - - ]: 0 : Trace("arith::pf::tree") << *this << std::endl;
1628 [ - - ]: 0 : Trace("arith::pf::tree") << *getNegation() << std::endl;
1629 [ - - ]: 0 : Trace("arith::pf::tree") << "\n\nTree:\n";
1630 [ - - ]: 0 : printProofTree(Trace("arith::pf::tree"));
1631 [ - - ]: 0 : getNegation()->printProofTree(Trace("arith::pf::tree"));
1632 : : }
1633 : 100476 : auto confPf = d_database->d_pnm->mkScope(bot, lits);
1634 : 50238 : return d_database->d_pfGen->mkTrustNode(
1635 : 100476 : d_database->nodeManager()->mkAnd(lits), confPf, true);
1636 : : }
1637 : : else
1638 : : {
1639 : 66232 : return TrustNode::mkTrustConflict(n);
1640 : : }
1641 : : }
1642 : :
1643 : : struct ConstraintCPHash {
1644 : : /* Todo replace with an id */
1645 : 0 : size_t operator()(ConstraintCP c) const{
1646 : : Assert(sizeof(ConstraintCP) > 0);
1647 : 0 : return ((size_t)c)/sizeof(ConstraintCP);
1648 : : }
1649 : : };
1650 : :
1651 : 0 : void Constraint::assertionFringe(ConstraintCPVec& v){
1652 : 0 : unordered_set<ConstraintCP, ConstraintCPHash> visited;
1653 : 0 : size_t writePos = 0;
1654 : :
1655 [ - - ]: 0 : if(!v.empty()){
1656 : 0 : const ConstraintDatabase* db = v.back()->d_database;
1657 : 0 : const CDConstraintList& antecedents = db->d_antecedents;
1658 [ - - ]: 0 : for(size_t i = 0; i < v.size(); ++i){
1659 : 0 : ConstraintCP vi = v[i];
1660 [ - - ]: 0 : if(visited.find(vi) == visited.end()){
1661 : 0 : Assert(vi->hasProof());
1662 : 0 : visited.insert(vi);
1663 [ - - ]: 0 : if(vi->onFringe()){
1664 : 0 : v[writePos] = vi;
1665 : 0 : writePos++;
1666 : : }else{
1667 : 0 : Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof()
1668 : : || vi->hasIntHoleProof() || vi->hasIntTightenProof());
1669 : 0 : AntecedentId p = vi->getEndAntecedent();
1670 : :
1671 : 0 : ConstraintCP antecedent = antecedents[p];
1672 [ - - ]: 0 : while(antecedent != NullConstraint){
1673 : 0 : v.push_back(antecedent);
1674 : 0 : --p;
1675 : 0 : antecedent = antecedents[p];
1676 : : }
1677 : : }
1678 : : }
1679 : : }
1680 : 0 : v.resize(writePos);
1681 : : }
1682 : 0 : }
1683 : :
1684 : 0 : void Constraint::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){
1685 : 0 : o.insert(o.end(), i.begin(), i.end());
1686 : 0 : assertionFringe(o);
1687 : 0 : }
1688 : :
1689 : 194347 : Node Constraint::externalExplain(NodeManager* nm,
1690 : : const ConstraintCPVec& v,
1691 : : AssertionOrder order)
1692 : : {
1693 : 388694 : NodeBuilder nb(nm, Kind::AND);
1694 : 194347 : ConstraintCPVec::const_iterator i, end;
1695 [ + + ]: 812588 : for(i = v.begin(), end = v.end(); i != end; ++i){
1696 : 618241 : ConstraintCP v_i = *i;
1697 : 618241 : v_i->externalExplain(nb, order);
1698 : : }
1699 : 388694 : return mkAndFromBuilder(nm, nb);
1700 : : }
1701 : :
1702 : 9612760 : std::shared_ptr<ProofNode> Constraint::externalExplain(
1703 : : NodeBuilder& nb, AssertionOrder order) const
1704 : : {
1705 [ - + ]: 9612760 : if (TraceIsOn("pf::arith::explain"))
1706 : : {
1707 [ - - ]: 0 : this->printProofTree(Trace("arith::pf::tree"));
1708 [ - - ]: 0 : Trace("pf::arith::explain") << "Explaining: " << this << " with rule ";
1709 [ - - ]: 0 : getConstraintRule().print(Trace("pf::arith::explain"), d_produceProofs);
1710 [ - - ]: 0 : Trace("pf::arith::explain") << std::endl;
1711 : : }
1712 [ - + ][ - + ]: 9612760 : Assert(hasProof());
[ - - ]
1713 [ + + ][ - + ]: 9612760 : Assert(!isAssumption() || assertedToTheTheory());
[ - + ][ - - ]
1714 [ - + ][ - + ]: 9612760 : Assert(!isInternalAssumption());
[ - - ]
1715 : 9612760 : std::shared_ptr<ProofNode> pf{};
1716 : :
1717 : 9612760 : ProofNodeManager* pnm = d_database->d_pnm;
1718 : :
1719 [ + + ]: 9612760 : if (assertedBefore(order))
1720 : : {
1721 [ + - ]: 8193110 : Trace("pf::arith::explain") << " already asserted" << std::endl;
1722 : 8193110 : nb << getWitness();
1723 [ + + ]: 8193110 : if (d_database->isProofEnabled())
1724 : : {
1725 : 3576480 : pf = pnm->mkAssume(getWitness());
1726 : : // If the witness and literal differ, prove the difference through a
1727 : : // rewrite.
1728 : 3576480 : pf = ensurePredTransform(pnm, pf, getProofLiteral());
1729 : : }
1730 : : }
1731 [ + + ]: 1419650 : else if (hasEqualityEngineProof())
1732 : : {
1733 : : // just assume, it will be explained again
1734 : 499 : Node lit = getLiteral();
1735 [ + + ]: 499 : if (d_database->isProofEnabled())
1736 : : {
1737 : 470 : std::shared_ptr<ProofNode> a = pnm->mkAssume(getLiteral());
1738 : 235 : Node plit = getProofLiteral();
1739 : 235 : pf = ensurePredTransform(pnm, a, plit);
1740 : : }
1741 [ - + ][ - + ]: 499 : Assert(lit.getKind() != Kind::AND);
[ - - ]
1742 : 499 : nb << lit;
1743 : : }
1744 : : else
1745 : : {
1746 [ + - ]: 1419160 : Trace("pf::arith::explain") << " recursion!" << std::endl;
1747 [ - + ][ - + ]: 1419160 : Assert(!isAssumption());
[ - - ]
1748 : 1419160 : AntecedentId p = getEndAntecedent();
1749 : 1419160 : ConstraintCP antecedent = d_database->d_antecedents[p];
1750 : 2838310 : std::vector<std::shared_ptr<ProofNode>> children;
1751 : :
1752 [ + + ]: 4053380 : while (antecedent != NullConstraint)
1753 : : {
1754 [ + - ]: 2634220 : Trace("pf::arith::explain") << "Explain " << antecedent << std::endl;
1755 : 2634220 : auto pn = antecedent->externalExplain(nb, order);
1756 [ + + ]: 2634220 : if (d_database->isProofEnabled())
1757 : : {
1758 : 1015730 : children.push_back(pn);
1759 : : }
1760 : 2634220 : --p;
1761 : 2634220 : antecedent = d_database->d_antecedents[p];
1762 : : }
1763 : :
1764 [ + + ]: 1419160 : if (d_database->isProofEnabled())
1765 : : {
1766 [ - + ][ + - ]: 689804 : switch (getProofType())
[ + - ]
1767 : : {
1768 : 0 : case ArithProofType::AssumeAP:
1769 : : case ArithProofType::EqualityEngineAP:
1770 : : {
1771 : 0 : Unreachable() << "These should be handled above";
1772 : : break;
1773 : : }
1774 : 54458 : case ArithProofType::FarkasAP:
1775 : : {
1776 : : // Per docs in constraint.h,
1777 : : // the 0th farkas coefficient is for the negation of the deduced
1778 : : // constraint the 1st corresponds to the last antecedent the nth
1779 : : // corresponds to the first antecedent Then, the farkas coefficients
1780 : : // and the antecedents are in the same order.
1781 : :
1782 : : // Enumerate child proofs (negation included) in d_farkasCoefficients
1783 : : // order
1784 : 108916 : Node plit = getNegation()->getProofLiteral();
1785 : 108916 : std::vector<std::shared_ptr<ProofNode>> farkasChildren;
1786 : 54458 : farkasChildren.push_back(pnm->mkAssume(plit));
1787 : : farkasChildren.insert(
1788 : 54458 : farkasChildren.end(), children.rbegin(), children.rend());
1789 : :
1790 : 54458 : NodeManager* nm = d_database->nodeManager();
1791 : :
1792 : : // Enumerate d_farkasCoefficients as nodes.
1793 : 108916 : std::vector<Node> farkasCoeffs;
1794 : 108916 : TypeNode type = plit[0].getType();
1795 [ + + ]: 452510 : for (Rational r : *getFarkasCoefficients())
1796 : : {
1797 : 398052 : farkasCoeffs.push_back(nm->mkConstRealOrInt(Rational(r)));
1798 : : }
1799 : : std::vector<Node> farkasCoeffsUse =
1800 : 108916 : getMacroSumUbCoeff(nm, farkasChildren, farkasCoeffs);
1801 : :
1802 : : // Apply the scaled-sum rule.
1803 : : std::shared_ptr<ProofNode> sumPf =
1804 : : pnm->mkNode(ProofRule::MACRO_ARITH_SCALE_SUM_UB,
1805 : : farkasChildren,
1806 : 108916 : farkasCoeffsUse);
1807 : :
1808 : : // Provable rewrite the result
1809 : 108916 : Node falsen = nm->mkConst(false);
1810 : 108916 : auto botPf = ensurePredTransform(pnm, sumPf, falsen);
1811 : :
1812 : : // Scope out the negated constraint, yielding a proof of the
1813 : : // constraint.
1814 : 217832 : std::vector<Node> assump{plit};
1815 : 163374 : auto maybeDoubleNotPf = pnm->mkScope(botPf, assump, false);
1816 : :
1817 : : // No need to ensure that the expected node aggrees with `assump`
1818 : : // because we are not providing an expected node.
1819 : : //
1820 : : // Prove that this is the literal (may need to clean a double-not)
1821 : 108916 : Node plit2 = getProofLiteral();
1822 : 54458 : pf = ensurePredTransform(pnm, maybeDoubleNotPf, plit2);
1823 : :
1824 : 54458 : break;
1825 : : }
1826 : 598554 : case ArithProofType::IntTightenAP:
1827 : : {
1828 [ + + ]: 598554 : if (isUpperBound())
1829 : : {
1830 : 1179410 : pf = pnm->mkNode(
1831 : 1769110 : ProofRule::INT_TIGHT_UB, children, {}, getProofLiteral());
1832 : : }
1833 [ + - ]: 8850 : else if (isLowerBound())
1834 : : {
1835 : 17700 : pf = pnm->mkNode(
1836 : 26550 : ProofRule::INT_TIGHT_LB, children, {}, getProofLiteral());
1837 : : }
1838 : : else
1839 : : {
1840 : 0 : Unreachable();
1841 : : }
1842 : 598554 : break;
1843 : : }
1844 : 0 : case ArithProofType::IntHoleAP:
1845 : : {
1846 : 0 : pf = pnm->mkTrustedNode(TrustId::THEORY_INFERENCE_ARITH,
1847 : : children,
1848 : : {getProofLiteral()},
1849 : 0 : getProofLiteral());
1850 : 0 : break;
1851 : : }
1852 : 36792 : case ArithProofType::TrichotomyAP:
1853 : : {
1854 : 73584 : pf = pnm->mkNode(
1855 : 110376 : ProofRule::ARITH_TRICHOTOMY, children, {}, getProofLiteral());
1856 : 36792 : break;
1857 : : }
1858 : 0 : case ArithProofType::InternalAssumeAP:
1859 : : case ArithProofType::NoAP:
1860 : : default:
1861 : : {
1862 : 0 : Unreachable() << getProofType()
1863 : 0 : << " should not be visible in explanation";
1864 : : break;
1865 : : }
1866 : : }
1867 : : }
1868 : : }
1869 : 9612760 : return pf;
1870 : : }
1871 : :
1872 : 1452 : Node Constraint::externalExplainByAssertions(NodeManager* nm,
1873 : : ConstraintCP a,
1874 : : ConstraintCP b)
1875 : : {
1876 : 2904 : NodeBuilder nb(nm, Kind::AND);
1877 : 1452 : a->externalExplainByAssertions(nb);
1878 : 1452 : b->externalExplainByAssertions(nb);
1879 : 2904 : return nb;
1880 : : }
1881 : :
1882 : 0 : Node Constraint::externalExplainByAssertions(NodeManager* nm,
1883 : : ConstraintCP a,
1884 : : ConstraintCP b,
1885 : : ConstraintCP c)
1886 : : {
1887 : 0 : NodeBuilder nb(nm, Kind::AND);
1888 : 0 : a->externalExplainByAssertions(nb);
1889 : 0 : b->externalExplainByAssertions(nb);
1890 : 0 : c->externalExplainByAssertions(nb);
1891 : 0 : return nb;
1892 : : }
1893 : :
1894 : 936590 : ConstraintP Constraint::getStrictlyWeakerLowerBound(bool hasLiteral, bool asserted) const {
1895 [ - + ][ - + ]: 936590 : Assert(initialized());
[ - - ]
1896 [ + + ][ - + ]: 936590 : Assert(!asserted || hasLiteral);
[ - + ][ - - ]
1897 : :
1898 : 936590 : SortedConstraintMapConstIterator i = d_variablePosition;
1899 : 936590 : const SortedConstraintMap& scm = constraintSet();
1900 : 936590 : SortedConstraintMapConstIterator i_begin = scm.begin();
1901 [ + + ]: 1921250 : while(i != i_begin){
1902 : 1150120 : --i;
1903 : 1150120 : const ValueCollection& vc = i->second;
1904 [ + + ]: 1150120 : if(vc.hasLowerBound()){
1905 : 316286 : ConstraintP weaker = vc.getLowerBound();
1906 : :
1907 : : // asserted -> hasLiteral
1908 : : // hasLiteral -> weaker->hasLiteral()
1909 : : // asserted -> weaker->assertedToTheTheory()
1910 [ + - ][ + + ]: 487521 : if((!hasLiteral || (weaker->hasLiteral())) &&
[ + + ]
1911 [ + + ][ + + ]: 171235 : (!asserted || ( weaker->assertedToTheTheory()))){
1912 : 165457 : return weaker;
1913 : : }
1914 : : }
1915 : : }
1916 : 771133 : return NullConstraint;
1917 : : }
1918 : :
1919 : 571961 : ConstraintP Constraint::getStrictlyWeakerUpperBound(bool hasLiteral, bool asserted) const {
1920 : 571961 : SortedConstraintMapConstIterator i = d_variablePosition;
1921 : 571961 : const SortedConstraintMap& scm = constraintSet();
1922 : 571961 : SortedConstraintMapConstIterator i_end = scm.end();
1923 : :
1924 : 571961 : ++i;
1925 [ + + ]: 1053990 : for(; i != i_end; ++i){
1926 : 671127 : const ValueCollection& vc = i->second;
1927 [ + + ]: 671127 : if(vc.hasUpperBound()){
1928 : 233237 : ConstraintP weaker = vc.getUpperBound();
1929 [ + - ][ + + ]: 433256 : if((!hasLiteral || (weaker->hasLiteral())) &&
[ + + ]
1930 [ + + ][ + + ]: 200019 : (!asserted || ( weaker->assertedToTheTheory()))){
1931 : 189098 : return weaker;
1932 : : }
1933 : : }
1934 : : }
1935 : :
1936 : 382863 : return NullConstraint;
1937 : : }
1938 : :
1939 : 8935440 : ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const {
1940 [ - + ][ - + ]: 8935440 : Assert(variableDatabaseIsSetup(v));
[ - - ]
1941 [ + + ][ - + ]: 8935440 : Assert(t == UpperBound || t == LowerBound);
[ - + ][ - - ]
1942 : :
1943 : 8935440 : SortedConstraintMap& scm = getVariableSCM(v);
1944 [ + + ]: 8935440 : if(t == UpperBound){
1945 : 4325340 : SortedConstraintMapConstIterator i = scm.lower_bound(r);
1946 : 4325340 : SortedConstraintMapConstIterator i_end = scm.end();
1947 [ + + ][ - + ]: 4325340 : Assert(i == i_end || r <= i->first);
[ - + ][ - - ]
1948 [ + + ]: 6480270 : for(; i != i_end; i++){
1949 [ - + ][ - + ]: 3775620 : Assert(r <= i->first);
[ - - ]
1950 : 3775620 : const ValueCollection& vc = i->second;
1951 [ + + ]: 3775620 : if(vc.hasUpperBound()){
1952 : 1620700 : return vc.getUpperBound();
1953 : : }
1954 : : }
1955 : 2704650 : return NullConstraint;
1956 : : }else{
1957 [ - + ][ - + ]: 4610090 : Assert(t == LowerBound);
[ - - ]
1958 [ + + ]: 4610090 : if(scm.empty()){
1959 : 357768 : return NullConstraint;
1960 : : }else{
1961 : 4252320 : SortedConstraintMapConstIterator i = scm.lower_bound(r);
1962 : 4252320 : SortedConstraintMapConstIterator i_begin = scm.begin();
1963 : 4252320 : SortedConstraintMapConstIterator i_end = scm.end();
1964 [ + + ][ - + ]: 4252320 : Assert(i == i_end || r <= i->first);
[ - + ][ - - ]
1965 : :
1966 : 4252320 : int fdj = 0;
1967 : :
1968 [ + + ]: 4252320 : if(i == i_end){
1969 : 1647380 : --i;
1970 [ + - ]: 1647380 : Trace("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl;
1971 [ + + ]: 2604940 : }else if( (i->first) > r){
1972 [ + + ]: 764343 : if(i == i_begin){
1973 : 679994 : return NullConstraint;
1974 : : }else{
1975 : 84349 : --i;
1976 [ + - ]: 84349 : Trace("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl;
1977 : : }
1978 : : }
1979 : :
1980 : : do{
1981 [ + - ]: 3892940 : Trace("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl;
1982 [ - + ][ - + ]: 3892940 : Assert(r >= i->first);
[ - - ]
1983 : 3892940 : const ValueCollection& vc = i->second;
1984 : :
1985 [ + + ]: 3892940 : if(vc.hasLowerBound()){
1986 : 1940320 : return vc.getLowerBound();
1987 : : }
1988 : :
1989 [ + + ]: 1952620 : if(i == i_begin){
1990 : 1632010 : break;
1991 : : }else{
1992 : 320612 : --i;
1993 : 320612 : }
1994 : : }while(true);
1995 : 1632010 : return NullConstraint;
1996 : : }
1997 : : }
1998 : : }
1999 : :
2000 : 31336100 : bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const {
2001 : 31336100 : return v < d_varDatabases.size();
2002 : : }
2003 : :
2004 : 50287 : ConstraintDatabase::Watches::Watches(context::Context* satContext,
2005 : 50287 : context::Context* userContext)
2006 : : : d_constraintProofs(satContext),
2007 : : d_canBePropagatedWatches(satContext),
2008 : : d_assertionOrderWatches(satContext),
2009 : 50287 : d_splitWatches(userContext)
2010 : 50287 : {}
2011 : :
2012 : :
2013 : 1169780 : void Constraint::setLiteral(Node n) {
2014 [ + - ]: 1169780 : Trace("arith::constraint") << "Mapping " << *this << " to " << n << std::endl;
2015 [ - + ][ - + ]: 1169780 : Assert(Comparison::isNormalAtom(n));
[ - - ]
2016 [ - + ][ - + ]: 1169780 : Assert(!hasLiteral());
[ - - ]
2017 [ - + ][ - + ]: 1169780 : Assert(sanityChecking(n));
[ - - ]
2018 : 1169780 : d_literal = n;
2019 : 1169780 : NodetoConstraintMap& map = d_database->d_nodetoConstraintMap;
2020 [ - + ][ - + ]: 1169780 : Assert(map.find(n) == map.end());
[ - - ]
2021 : 1169780 : map.insert(make_pair(d_literal, this));
2022 : 1169780 : }
2023 : :
2024 : 5128840 : Node Constraint::getProofLiteral() const
2025 : : {
2026 [ - + ][ - + ]: 5128840 : Assert(d_database != nullptr);
[ - - ]
2027 [ - + ][ - + ]: 5128840 : Assert(d_database->d_avariables.hasNode(d_variable));
[ - - ]
2028 : 10257700 : Node varPart = d_database->d_avariables.asNode(d_variable);
2029 : : Kind cmp;
2030 : 5128840 : bool neg = false;
2031 [ + + ][ + + ]: 5128840 : switch (d_type)
[ - ]
2032 : : {
2033 : 2006520 : case ConstraintType::UpperBound:
2034 : : {
2035 [ + + ]: 2006520 : if (d_value.infinitesimalIsZero())
2036 : : {
2037 : 1083670 : cmp = Kind::LEQ;
2038 : : }
2039 : : else
2040 : : {
2041 : 922854 : cmp = Kind::LT;
2042 : : }
2043 : 2006520 : break;
2044 : : }
2045 : 1287280 : case ConstraintType::LowerBound:
2046 : : {
2047 [ + + ]: 1287280 : if (d_value.infinitesimalIsZero())
2048 : : {
2049 : 1129460 : cmp = Kind::GEQ;
2050 : : }
2051 : : else
2052 : : {
2053 : 157821 : cmp = Kind::GT;
2054 : : }
2055 : 1287280 : break;
2056 : : }
2057 : 1587840 : case ConstraintType::Equality:
2058 : : {
2059 : 1587840 : cmp = Kind::EQUAL;
2060 : 1587840 : break;
2061 : : }
2062 : 247200 : case ConstraintType::Disequality:
2063 : : {
2064 : 247200 : cmp = Kind::EQUAL;
2065 : 247200 : neg = true;
2066 : 247200 : break;
2067 : : }
2068 : 0 : default: Unreachable() << d_type;
2069 : : }
2070 : 5128840 : NodeManager* nm = d_database->nodeManager();
2071 : : Node constPart = nm->mkConstRealOrInt(
2072 : 15386500 : varPart.getType(), Rational(d_value.getNoninfinitesimalPart()));
2073 : 15386500 : Node posLit = nm->mkNode(cmp, varPart, constPart);
2074 [ + + ]: 10257700 : return neg ? posLit.negate() : posLit;
2075 : : }
2076 : :
2077 : 74981 : void ConstraintDatabase::proveOr(std::vector<TrustNode>& out,
2078 : : ConstraintP a,
2079 : : ConstraintP b,
2080 : : bool negateSecond) const
2081 : : {
2082 : 149962 : Node la = a->getLiteral();
2083 : 149962 : Node lb = b->getLiteral();
2084 [ + + ]: 149962 : Node orN = (la < lb) ? la.orNode(lb) : lb.orNode(la);
2085 [ + + ]: 74981 : if (isProofEnabled())
2086 : : {
2087 [ - + ][ - + ]: 33764 : Assert(b->getNegation()->getType() != ConstraintType::Disequality);
[ - - ]
2088 : 33764 : auto nm = nodeManager();
2089 : 67528 : Node alit = a->getNegation()->getProofLiteral();
2090 : 67528 : TypeNode type = alit[0].getType();
2091 : 67528 : auto pf_neg_la = d_pnm->mkAssume(la.negate());
2092 : 33764 : pf_neg_la = ensurePredTransform(d_pnm, pf_neg_la, alit);
2093 : 67528 : Node blit = b->getNegation()->getProofLiteral();
2094 : 67528 : auto pf_neg_lb = d_pnm->mkAssume(lb.negate());
2095 : 33764 : pf_neg_lb = ensurePredTransform(d_pnm, pf_neg_lb, blit);
2096 [ + + ]: 33764 : int sndSign = negateSecond ? -1 : 1;
2097 : 168820 : std::vector<Pf> args{pf_neg_la, pf_neg_lb};
2098 : 33764 : std::vector<Node> coeffs{nm->mkConstReal(Rational(-1 * sndSign)),
2099 : 202584 : nm->mkConstReal(Rational(sndSign))};
2100 : 67528 : std::vector<Node> coeffsUse = getMacroSumUbCoeff(nm, args, coeffs);
2101 : : auto sumubpf =
2102 : 67528 : d_pnm->mkNode(ProofRule::MACRO_ARITH_SCALE_SUM_UB, args, coeffsUse);
2103 : 67528 : auto bot_pf = ensurePredTransform(d_pnm, sumubpf, nm->mkConst(false));
2104 : 67528 : std::vector<Node> as;
2105 : 67528 : std::transform(orN.begin(), orN.end(), std::back_inserter(as), [](Node n) {
2106 : 67528 : return n.negate();
2107 : 33764 : });
2108 : : // No need to ensure that the expected node aggrees with `as` because we
2109 : : // are not providing an expected node.
2110 : : auto pf =
2111 : 135056 : d_pnm->mkNode(ProofRule::NOT_AND, {d_pnm->mkScope(bot_pf, as)}, {});
2112 : 33764 : pf = ensurePredTransform(d_pnm, pf, orN);
2113 : 33764 : out.push_back(d_pfGen->mkTrustNode(orN, pf));
2114 : : }
2115 : : else
2116 : : {
2117 : 41217 : out.push_back(TrustNode::mkTrustLemma(orN));
2118 : : }
2119 : 74981 : }
2120 : :
2121 : 70229 : void ConstraintDatabase::implies(std::vector<TrustNode>& out,
2122 : : ConstraintP a,
2123 : : ConstraintP b) const
2124 : : {
2125 : 140458 : Node la = a->getLiteral();
2126 : 140458 : Node lb = b->getLiteral();
2127 : :
2128 [ + + ]: 140458 : Node neg_la = (la.getKind() == Kind::NOT) ? la[0] : la.notNode();
2129 : :
2130 [ - + ][ - + ]: 70229 : Assert(lb != neg_la);
[ - - ]
2131 [ + + ][ - + ]: 70229 : Assert(b->getNegation()->getType() == ConstraintType::LowerBound
[ - + ][ - - ]
2132 : : || b->getNegation()->getType() == ConstraintType::UpperBound);
2133 : 70229 : proveOr(out,
2134 : : a->getNegation(),
2135 : : b,
2136 : 70229 : b->getNegation()->getType() == ConstraintType::LowerBound);
2137 : 70229 : }
2138 : :
2139 : 4752 : void ConstraintDatabase::mutuallyExclusive(std::vector<TrustNode>& out,
2140 : : ConstraintP a,
2141 : : ConstraintP b) const
2142 : : {
2143 : 9504 : Node la = a->getLiteral();
2144 : 9504 : Node lb = b->getLiteral();
2145 : :
2146 : 9504 : Node neg_la = la.negate();
2147 : 9504 : Node neg_lb = lb.negate();
2148 : 4752 : proveOr(out, a->getNegation(), b->getNegation(), true);
2149 : 4752 : }
2150 : :
2151 : 119003 : void ConstraintDatabase::outputUnateInequalityLemmas(
2152 : : std::vector<TrustNode>& out, ArithVar v) const
2153 : : {
2154 : 119003 : SortedConstraintMap& scm = getVariableSCM(v);
2155 : 119003 : SortedConstraintMapConstIterator scm_iter = scm.begin();
2156 : 119003 : SortedConstraintMapConstIterator scm_end = scm.end();
2157 : 119003 : ConstraintP prev = NullConstraint;
2158 : : //get transitive unates
2159 : : //Only lower bounds or upperbounds should be done.
2160 [ + + ]: 380292 : for(; scm_iter != scm_end; ++scm_iter){
2161 : 261289 : const ValueCollection& vc = scm_iter->second;
2162 [ + + ]: 261289 : if(vc.hasUpperBound()){
2163 : 123543 : ConstraintP ub = vc.getUpperBound();
2164 [ + + ]: 123543 : if(ub->hasLiteral()){
2165 [ + + ]: 123541 : if(prev != NullConstraint){
2166 : 53089 : implies(out, prev, ub);
2167 : : }
2168 : 123541 : prev = ub;
2169 : : }
2170 : : }
2171 : : }
2172 : 119003 : }
2173 : :
2174 : 119003 : void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<TrustNode>& out,
2175 : : ArithVar v) const
2176 : : {
2177 : 238006 : vector<ConstraintP> equalities;
2178 : :
2179 : 119003 : SortedConstraintMap& scm = getVariableSCM(v);
2180 : 119003 : SortedConstraintMapConstIterator scm_iter = scm.begin();
2181 : 119003 : SortedConstraintMapConstIterator scm_end = scm.end();
2182 : :
2183 [ + + ]: 380292 : for(; scm_iter != scm_end; ++scm_iter){
2184 : 261289 : const ValueCollection& vc = scm_iter->second;
2185 [ + + ]: 261289 : if(vc.hasEquality()){
2186 : 37086 : ConstraintP eq = vc.getEquality();
2187 [ + - ]: 37086 : if(eq->hasLiteral()){
2188 : 37086 : equalities.push_back(eq);
2189 : : }
2190 : : }
2191 : : }
2192 : :
2193 : 119003 : vector<ConstraintP>::const_iterator i, j, eq_end = equalities.end();
2194 [ + + ]: 156089 : for(i = equalities.begin(); i != eq_end; ++i){
2195 : 37086 : ConstraintP at_i = *i;
2196 [ + + ]: 41838 : for(j= i + 1; j != eq_end; ++j){
2197 : 4752 : ConstraintP at_j = *j;
2198 : :
2199 : 4752 : mutuallyExclusive(out, at_i, at_j);
2200 : : }
2201 : : }
2202 : :
2203 [ + + ]: 156089 : for(i = equalities.begin(); i != eq_end; ++i){
2204 : 37086 : ConstraintP eq = *i;
2205 : 37086 : const ValueCollection& vc = eq->getValueCollection();
2206 [ + - ][ + - ]: 74172 : Assert(vc.hasEquality() && vc.getEquality()->hasLiteral());
[ - + ][ - - ]
2207 : :
2208 [ + + ][ + - ]: 37086 : bool hasLB = vc.hasLowerBound() && vc.getLowerBound()->hasLiteral();
2209 [ + + ][ + + ]: 37086 : bool hasUB = vc.hasUpperBound() && vc.getUpperBound()->hasLiteral();
2210 : :
2211 [ + + ]: 37086 : ConstraintP lb = hasLB ?
2212 : 37086 : vc.getLowerBound() : eq->getStrictlyWeakerLowerBound(true, false);
2213 [ + + ]: 37086 : ConstraintP ub = hasUB ?
2214 : 37086 : vc.getUpperBound() : eq->getStrictlyWeakerUpperBound(true, false);
2215 : :
2216 [ + + ][ + + ]: 37086 : if(hasUB && hasLB && !eq->isSplit()){
[ + - ][ + + ]
2217 : 550 : out.push_back(eq->split());
2218 : : }
2219 [ + + ]: 37086 : if(lb != NullConstraint){
2220 : 5742 : implies(out, eq, lb);
2221 : : }
2222 [ + + ]: 37086 : if(ub != NullConstraint){
2223 : 11398 : implies(out, eq, ub);
2224 : : }
2225 : : }
2226 : 119003 : }
2227 : :
2228 : 27832 : void ConstraintDatabase::outputUnateEqualityLemmas(
2229 : : std::vector<TrustNode>& lemmas) const
2230 : : {
2231 [ + + ]: 146835 : for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){
2232 : 119003 : outputUnateEqualityLemmas(lemmas, v);
2233 : : }
2234 : 27832 : }
2235 : :
2236 : 27832 : void ConstraintDatabase::outputUnateInequalityLemmas(
2237 : : std::vector<TrustNode>& lemmas) const
2238 : : {
2239 [ + + ]: 146835 : for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){
2240 : 119003 : outputUnateInequalityLemmas(lemmas, v);
2241 : : }
2242 : 27832 : }
2243 : :
2244 : 8245720 : bool ConstraintDatabase::handleUnateProp(ConstraintP ant, ConstraintP cons){
2245 [ + + ]: 8245720 : if(cons->negationHasProof()){
2246 [ + - ]: 2 : Trace("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
2247 : 2 : cons->impliedByUnate(nodeManager(), ant, true);
2248 : 2 : d_raiseConflict.raiseConflict(cons, InferenceId::ARITH_CONF_UNATE_PROP);
2249 : 2 : return true;
2250 [ + + ]: 8245720 : }else if(!cons->isTrue()){
2251 : 3783110 : ++d_statistics.d_unatePropagateImplications;
2252 [ + - ]: 3783110 : Trace("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
2253 : 3783110 : cons->impliedByUnate(nodeManager(), ant, false);
2254 : 3783110 : cons->tryToPropagate();
2255 : 3783110 : return false;
2256 : : } else {
2257 : 4462620 : return false;
2258 : : }
2259 : : }
2260 : :
2261 : 2507500 : void ConstraintDatabase::unatePropLowerBound(ConstraintP curr, ConstraintP prev){
2262 [ + - ]: 2507500 : Trace("arith::unate") << "unatePropLowerBound " << curr << " " << prev << endl;
2263 [ - + ][ - + ]: 2507500 : Assert(curr != prev);
[ - - ]
2264 [ - + ][ - + ]: 2507500 : Assert(curr != NullConstraint);
[ - - ]
2265 : 2507500 : bool hasPrev = ! (prev == NullConstraint);
2266 [ + + ][ - + ]: 2507500 : Assert(!hasPrev || curr->getValue() > prev->getValue());
[ - + ][ - - ]
2267 : :
2268 : 2507500 : ++d_statistics.d_unatePropagateCalls;
2269 : :
2270 : 2507500 : const SortedConstraintMap& scm = curr->constraintSet();
2271 : 2507500 : const SortedConstraintMapConstIterator scm_begin = scm.begin();
2272 : 2507500 : SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
2273 : :
2274 : : //Ignore the first ValueCollection
2275 : : // NOPE: (>= p c) then (= p c) NOPE
2276 : : // NOPE: (>= p c) then (not (= p c)) NOPE
2277 : :
2278 [ + + ]: 9003900 : while(scm_i != scm_begin){
2279 : 6984630 : --scm_i; // move the iterator back
2280 : :
2281 : 6984630 : const ValueCollection& vc = scm_i->second;
2282 : :
2283 : : //If it has the previous element, do nothing and stop!
2284 : 8906070 : if(hasPrev &&
2285 [ + + ]: 1921440 : vc.hasConstraintOfType(prev->getType())
2286 [ + + ][ + + ]: 8906070 : && vc.getConstraintOfType(prev->getType()) == prev){
[ + + ]
2287 : 488224 : break;
2288 : : }
2289 : :
2290 : : //Don't worry about implying the negation of upperbound.
2291 : : //These should all be handled by propagating the LowerBounds!
2292 [ + + ]: 6496400 : if(vc.hasLowerBound()){
2293 : 2474190 : ConstraintP lb = vc.getLowerBound();
2294 [ - + ]: 2474200 : if(handleUnateProp(curr, lb)){ return; }
2295 : : }
2296 [ + + ]: 6496400 : if(vc.hasDisequality()){
2297 : 545398 : ConstraintP dis = vc.getDisequality();
2298 [ + + ]: 545398 : if(handleUnateProp(curr, dis)){ return; }
2299 : : }
2300 : : }
2301 : : }
2302 : :
2303 : 2272440 : void ConstraintDatabase::unatePropUpperBound(ConstraintP curr, ConstraintP prev){
2304 [ + - ]: 2272440 : Trace("arith::unate") << "unatePropUpperBound " << curr << " " << prev << endl;
2305 [ - + ][ - + ]: 2272440 : Assert(curr != prev);
[ - - ]
2306 [ - + ][ - + ]: 2272440 : Assert(curr != NullConstraint);
[ - - ]
2307 : 2272440 : bool hasPrev = ! (prev == NullConstraint);
2308 [ + + ][ - + ]: 2272440 : Assert(!hasPrev || curr->getValue() < prev->getValue());
[ - + ][ - - ]
2309 : :
2310 : 2272440 : ++d_statistics.d_unatePropagateCalls;
2311 : :
2312 : 2272440 : const SortedConstraintMap& scm = curr->constraintSet();
2313 : 2272440 : const SortedConstraintMapConstIterator scm_end = scm.end();
2314 : 2272440 : SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
2315 : 2272440 : ++scm_i;
2316 [ + + ]: 8853730 : for(; scm_i != scm_end; ++scm_i){
2317 : 6964490 : const ValueCollection& vc = scm_i->second;
2318 : :
2319 : : //If it has the previous element, do nothing and stop!
2320 : 8226390 : if(hasPrev &&
2321 [ + + ][ + + ]: 7757000 : vc.hasConstraintOfType(prev->getType()) &&
[ + + ]
2322 [ + + ]: 792510 : vc.getConstraintOfType(prev->getType()) == prev){
2323 : 383203 : break;
2324 : : }
2325 : : //Don't worry about implying the negation of upperbound.
2326 : : //These should all be handled by propagating the UpperBounds!
2327 [ + + ]: 6581280 : if(vc.hasUpperBound()){
2328 : 2563470 : ConstraintP ub = vc.getUpperBound();
2329 [ - + ]: 2563470 : if(handleUnateProp(curr, ub)){ return; }
2330 : : }
2331 [ + + ]: 6581280 : if(vc.hasDisequality()){
2332 : 413917 : ConstraintP dis = vc.getDisequality();
2333 [ - + ]: 413917 : if(handleUnateProp(curr, dis)){ return; }
2334 : : }
2335 : : }
2336 : : }
2337 : :
2338 : 1763270 : void ConstraintDatabase::unatePropEquality(ConstraintP curr, ConstraintP prevLB, ConstraintP prevUB){
2339 [ + - ]: 1763270 : Trace("arith::unate") << "unatePropEquality " << curr << " " << prevLB << " " << prevUB << endl;
2340 [ - + ][ - + ]: 1763270 : Assert(curr != prevLB);
[ - - ]
2341 [ - + ][ - + ]: 1763270 : Assert(curr != prevUB);
[ - - ]
2342 [ - + ][ - + ]: 1763270 : Assert(curr != NullConstraint);
[ - - ]
2343 : 1763270 : bool hasPrevLB = ! (prevLB == NullConstraint);
2344 : 1763270 : bool hasPrevUB = ! (prevUB == NullConstraint);
2345 [ + + ][ - + ]: 1763270 : Assert(!hasPrevLB || curr->getValue() >= prevLB->getValue());
[ - + ][ - - ]
2346 [ + + ][ - + ]: 1763270 : Assert(!hasPrevUB || curr->getValue() <= prevUB->getValue());
[ - + ][ - - ]
2347 : :
2348 : 1763270 : ++d_statistics.d_unatePropagateCalls;
2349 : :
2350 : 1763270 : const SortedConstraintMap& scm = curr->constraintSet();
2351 : 1763270 : SortedConstraintMapConstIterator scm_curr = curr->d_variablePosition;
2352 [ + + ]: 1763270 : SortedConstraintMapConstIterator scm_last = hasPrevUB ? prevUB->d_variablePosition : scm.end();
2353 : 1763270 : SortedConstraintMapConstIterator scm_i;
2354 [ + + ]: 1763270 : if(hasPrevLB){
2355 : 220215 : scm_i = prevLB->d_variablePosition;
2356 [ + + ]: 220215 : if(scm_i != scm_curr){ // If this does not move this past scm_curr, move it one forward
2357 : 55502 : ++scm_i;
2358 : : }
2359 : : }else{
2360 : 1543060 : scm_i = scm.begin();
2361 : : }
2362 : :
2363 [ + + ]: 2947200 : for(; scm_i != scm_curr; ++scm_i){
2364 : : // between the previous LB and the curr
2365 : 1183930 : const ValueCollection& vc = scm_i->second;
2366 : :
2367 : : //Don't worry about implying the negation of upperbound.
2368 : : //These should all be handled by propagating the LowerBounds!
2369 [ + + ]: 1183930 : if(vc.hasLowerBound()){
2370 : 368227 : ConstraintP lb = vc.getLowerBound();
2371 [ - + ]: 368227 : if(handleUnateProp(curr, lb)){ return; }
2372 : : }
2373 [ + + ]: 1183930 : if(vc.hasDisequality()){
2374 : 325984 : ConstraintP dis = vc.getDisequality();
2375 [ - + ]: 325984 : if(handleUnateProp(curr, dis)){ return; }
2376 : : }
2377 : : }
2378 [ - + ][ - + ]: 1763270 : Assert(scm_i == scm_curr);
[ - - ]
2379 [ + + ][ + + ]: 1763270 : if(!hasPrevUB || scm_i != scm_last){
[ + + ]
2380 : 1715990 : ++scm_i;
2381 : : } // hasPrevUB implies scm_i != scm_last
2382 : :
2383 [ + + ]: 4409920 : for(; scm_i != scm_last; ++scm_i){
2384 : : // between the curr and the previous UB imply the upperbounds and disequalities.
2385 : 2646650 : const ValueCollection& vc = scm_i->second;
2386 : :
2387 : : //Don't worry about implying the negation of upperbound.
2388 : : //These should all be handled by propagating the UpperBounds!
2389 [ + + ]: 2646650 : if(vc.hasUpperBound()){
2390 : 902098 : ConstraintP ub = vc.getUpperBound();
2391 [ - + ]: 902098 : if(handleUnateProp(curr, ub)){ return; }
2392 : : }
2393 [ + + ]: 2646650 : if(vc.hasDisequality()){
2394 : 652435 : ConstraintP dis = vc.getDisequality();
2395 [ - + ]: 652435 : if(handleUnateProp(curr, dis)){ return; }
2396 : : }
2397 : : }
2398 : : }
2399 : :
2400 : 2674510 : std::pair<int, int> Constraint::unateFarkasSigns(ConstraintCP ca, ConstraintCP cb){
2401 : 2674510 : ConstraintType a = ca->getType();
2402 : 2674510 : ConstraintType b = cb->getType();
2403 : :
2404 [ - + ][ - + ]: 2674510 : Assert(a != Disequality);
[ - - ]
2405 [ - + ][ - + ]: 2674510 : Assert(b != Disequality);
[ - - ]
2406 : :
2407 [ + + ][ + + ]: 2674510 : int a_sgn = (a == LowerBound) ? -1 : ((a == UpperBound) ? 1 : 0);
2408 [ + + ][ + + ]: 2674510 : int b_sgn = (b == LowerBound) ? -1 : ((b == UpperBound) ? 1 : 0);
2409 : :
2410 [ + + ][ + + ]: 2674510 : if(a_sgn == 0 && b_sgn == 0){
2411 [ - + ][ - + ]: 550955 : Assert(a == Equality);
[ - - ]
2412 [ - + ][ - + ]: 550955 : Assert(b == Equality);
[ - - ]
2413 [ - + ][ - + ]: 550955 : Assert(ca->getValue() != cb->getValue());
[ - - ]
2414 [ + + ]: 550955 : if(ca->getValue() < cb->getValue()){
2415 : 175404 : a_sgn = 1;
2416 : 175404 : b_sgn = -1;
2417 : : }else{
2418 : 375551 : a_sgn = -1;
2419 : 375551 : b_sgn = 1;
2420 : : }
2421 [ + + ]: 2123560 : }else if(a_sgn == 0){
2422 [ - + ][ - + ]: 421777 : Assert(b_sgn != 0);
[ - - ]
2423 [ - + ][ - + ]: 421777 : Assert(a == Equality);
[ - - ]
2424 : 421777 : a_sgn = -b_sgn;
2425 [ + + ]: 1701780 : }else if(b_sgn == 0){
2426 [ - + ][ - + ]: 639119 : Assert(a_sgn != 0);
[ - - ]
2427 [ - + ][ - + ]: 639119 : Assert(b == Equality);
[ - - ]
2428 : 639119 : b_sgn = -a_sgn;
2429 : : }
2430 [ - + ][ - + ]: 2674510 : Assert(a_sgn != 0);
[ - - ]
2431 [ - + ][ - + ]: 2674510 : Assert(b_sgn != 0);
[ - - ]
2432 : :
2433 [ + - ]: 5349030 : Trace("arith::unateFarkasSigns") << "Constraint::unateFarkasSigns("<<a <<", " << b << ") -> "
2434 : 2674510 : << "("<<a_sgn<<", "<< b_sgn <<")"<< endl;
2435 : 5349030 : return make_pair(a_sgn, b_sgn);
2436 : : }
2437 : :
2438 : : } // namespace arith
2439 : : } // namespace theory
2440 : : } // namespace cvc5::internal
|
