1 /********************* */
2 /*! \file theory_arith.cpp
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): kshitij, ajreynol, mdeters, dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "expr/node.h"
19 #include "expr/kind.h"
20 #include "expr/metakind.h"
21 #include "expr/node_builder.h"
23 #include "theory/valuation.h"
24 #include "theory/rewriter.h"
26 #include "util/rational.h"
27 #include "util/integer.h"
28 #include "util/boolean_simplification.h"
29 #include "util/dense_map.h"
31 #include "smt/logic_exception.h"
33 #include "theory/arith/arith_utilities.h"
34 #include "theory/arith/delta_rational.h"
35 #include "theory/arith/partial_model.h"
36 #include "theory/arith/matrix.h"
38 #include "theory/arith/arith_rewriter.h"
39 #include "theory/arith/constraint.h"
40 #include "theory/arith/theory_arith.h"
41 #include "theory/arith/normal_form.h"
42 #include "theory/model.h"
44 #include "theory/arith/options.h"
49 using namespace CVC4::kind
;
55 const uint32_t RESET_START
= 2;
58 TheoryArith::TheoryArith(context::Context
* c
, context::UserContext
* u
, OutputChannel
& out
, Valuation valuation
, const LogicInfo
& logicInfo
, QuantifiersEngine
* qe
) :
59 Theory(THEORY_ARITH
, c
, u
, out
, valuation
, logicInfo
, qe
),
60 d_nlIncomplete( false),
61 d_qflraStatus(Result::SAT_UNKNOWN
),
63 d_hasDoneWorkSinceCut(false),
65 d_numberOfVariables(0),
67 d_setupLiteralCallback(this),
68 d_assertionsThatDoNotMatchTheirLiterals(c
),
69 d_nextIntegerCheckVar(0),
70 d_constantIntegerVariables(c
),
71 d_diseqQueue(c
, false),
72 d_currentPropagationList(),
74 d_partialModel(c
, d_deltaComputeCallback
),
76 d_linEq(d_partialModel
, d_tableau
, d_basicVarModelUpdateCallBack
),
79 d_tableauSizeHasBeenModified(false),
80 d_tableauResetDensity(1.6),
81 d_tableauResetPeriod(10),
83 d_raiseConflict(d_conflicts
),
84 d_tempVarMalloc(*this),
85 d_congruenceManager(c
, d_constraintDatabase
, d_setupLiteralCallback
, d_arithvarNodeMap
, d_raiseConflict
),
86 d_simplex(d_linEq
, d_raiseConflict
),
87 d_constraintDatabase(c
, u
, d_arithvarNodeMap
, d_congruenceManager
, d_raiseConflict
),
88 d_deltaComputeCallback(this),
89 d_basicVarModelUpdateCallBack(d_simplex
),
95 TheoryArith::~TheoryArith(){}
97 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
98 d_congruenceManager
.setMasterEqualityEngine(eq
);
101 Node
skolemFunction(const std::string
& name
, TypeNode dom
, TypeNode range
){
102 NodeManager
* currNM
= NodeManager::currentNM();
103 TypeNode functionType
= currNM
->mkFunctionType(dom
, range
);
104 return currNM
->mkSkolem(name
, functionType
);
107 Node
TheoryArith::getRealDivideBy0Func(){
108 Assert(!getLogicInfo().isLinear());
109 Assert(getLogicInfo().areRealsUsed());
111 if(d_realDivideBy0Func
.isNull()){
112 TypeNode realType
= NodeManager::currentNM()->realType();
113 d_realDivideBy0Func
= skolemFunction("/by0_$$", realType
, realType
);
115 return d_realDivideBy0Func
;
118 Node
TheoryArith::getIntDivideBy0Func(){
119 Assert(!getLogicInfo().isLinear());
120 Assert(getLogicInfo().areIntegersUsed());
122 if(d_intDivideBy0Func
.isNull()){
123 TypeNode intType
= NodeManager::currentNM()->integerType();
124 d_intDivideBy0Func
= skolemFunction("divby0_$$", intType
, intType
);
126 return d_intDivideBy0Func
;
129 Node
TheoryArith::getIntModulusBy0Func(){
130 Assert(!getLogicInfo().isLinear());
131 Assert(getLogicInfo().areIntegersUsed());
133 if(d_intModulusBy0Func
.isNull()){
134 TypeNode intType
= NodeManager::currentNM()->integerType();
135 d_intModulusBy0Func
= skolemFunction("modby0_$$", intType
, intType
);
137 return d_intModulusBy0Func
;
140 TheoryArith::ModelException::ModelException(TNode n
, const char* msg
) throw (){
142 ss
<< "Cannot construct a model for " << n
<< " as " << endl
<< msg
;
143 setMessage(ss
.str());
145 TheoryArith::ModelException::~ModelException() throw (){ }
148 TheoryArith::Statistics::Statistics():
149 d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
150 d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
151 d_statUserVariables("theory::arith::UserVariables", 0),
152 d_statSlackVariables("theory::arith::SlackVariables", 0),
153 d_statDisequalitySplits("theory::arith::DisequalitySplits", 0),
154 d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0),
155 d_simplifyTimer("theory::arith::simplifyTimer"),
156 d_staticLearningTimer("theory::arith::staticLearningTimer"),
157 d_presolveTime("theory::arith::presolveTime"),
158 d_newPropTime("theory::arith::newPropTimer"),
159 d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0),
160 d_initialTableauSize("theory::arith::initialTableauSize", 0),
161 d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
162 d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
163 d_restartTimer("theory::arith::restartTimer"),
164 d_boundComputationTime("theory::arith::bound::time"),
165 d_boundComputations("theory::arith::bound::boundComputations",0),
166 d_boundPropagations("theory::arith::bound::boundPropagations",0),
167 d_unknownChecks("theory::arith::status::unknowns", 0),
168 d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0),
169 d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow"),
170 d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0),
171 d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0),
172 d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0)
174 StatisticsRegistry::registerStat(&d_statAssertUpperConflicts
);
175 StatisticsRegistry::registerStat(&d_statAssertLowerConflicts
);
177 StatisticsRegistry::registerStat(&d_statUserVariables
);
178 StatisticsRegistry::registerStat(&d_statSlackVariables
);
179 StatisticsRegistry::registerStat(&d_statDisequalitySplits
);
180 StatisticsRegistry::registerStat(&d_statDisequalityConflicts
);
181 StatisticsRegistry::registerStat(&d_simplifyTimer
);
182 StatisticsRegistry::registerStat(&d_staticLearningTimer
);
184 StatisticsRegistry::registerStat(&d_presolveTime
);
185 StatisticsRegistry::registerStat(&d_newPropTime
);
187 StatisticsRegistry::registerStat(&d_externalBranchAndBounds
);
189 StatisticsRegistry::registerStat(&d_initialTableauSize
);
190 StatisticsRegistry::registerStat(&d_currSetToSmaller
);
191 StatisticsRegistry::registerStat(&d_smallerSetToCurr
);
192 StatisticsRegistry::registerStat(&d_restartTimer
);
194 StatisticsRegistry::registerStat(&d_boundComputationTime
);
195 StatisticsRegistry::registerStat(&d_boundComputations
);
196 StatisticsRegistry::registerStat(&d_boundPropagations
);
198 StatisticsRegistry::registerStat(&d_unknownChecks
);
199 StatisticsRegistry::registerStat(&d_maxUnknownsInARow
);
200 StatisticsRegistry::registerStat(&d_avgUnknownsInARow
);
201 StatisticsRegistry::registerStat(&d_revertsOnConflicts
);
202 StatisticsRegistry::registerStat(&d_commitsOnConflicts
);
203 StatisticsRegistry::registerStat(&d_nontrivialSatChecks
);
206 TheoryArith::Statistics::~Statistics(){
207 StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts
);
208 StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts
);
210 StatisticsRegistry::unregisterStat(&d_statUserVariables
);
211 StatisticsRegistry::unregisterStat(&d_statSlackVariables
);
212 StatisticsRegistry::unregisterStat(&d_statDisequalitySplits
);
213 StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts
);
214 StatisticsRegistry::unregisterStat(&d_simplifyTimer
);
215 StatisticsRegistry::unregisterStat(&d_staticLearningTimer
);
217 StatisticsRegistry::unregisterStat(&d_presolveTime
);
218 StatisticsRegistry::unregisterStat(&d_newPropTime
);
220 StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds
);
222 StatisticsRegistry::unregisterStat(&d_initialTableauSize
);
223 StatisticsRegistry::unregisterStat(&d_currSetToSmaller
);
224 StatisticsRegistry::unregisterStat(&d_smallerSetToCurr
);
225 StatisticsRegistry::unregisterStat(&d_restartTimer
);
227 StatisticsRegistry::unregisterStat(&d_boundComputationTime
);
228 StatisticsRegistry::unregisterStat(&d_boundComputations
);
229 StatisticsRegistry::unregisterStat(&d_boundPropagations
);
231 StatisticsRegistry::unregisterStat(&d_unknownChecks
);
232 StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow
);
233 StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow
);
234 StatisticsRegistry::unregisterStat(&d_revertsOnConflicts
);
235 StatisticsRegistry::unregisterStat(&d_commitsOnConflicts
);
236 StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks
);
239 void TheoryArith::revertOutOfConflict(){
240 d_partialModel
.revertAssignmentChanges();
242 d_currentPropagationList
.clear();
245 void TheoryArith::clearUpdates(){
246 d_updatedBounds
.purge();
249 void TheoryArith::zeroDifferenceDetected(ArithVar x
){
250 Assert(d_congruenceManager
.isWatchedVariable(x
));
251 Assert(d_partialModel
.upperBoundIsZero(x
));
252 Assert(d_partialModel
.lowerBoundIsZero(x
));
254 Constraint lb
= d_partialModel
.getLowerBoundConstraint(x
);
255 Constraint ub
= d_partialModel
.getUpperBoundConstraint(x
);
257 if(lb
->isEquality()){
258 d_congruenceManager
.watchedVariableIsZero(lb
);
259 }else if(ub
->isEquality()){
260 d_congruenceManager
.watchedVariableIsZero(ub
);
262 d_congruenceManager
.watchedVariableIsZero(lb
, ub
);
266 /* procedure AssertLower( x_i >= c_i ) */
267 bool TheoryArith::AssertLower(Constraint constraint
){
268 Assert(constraint
!= NullConstraint
);
269 Assert(constraint
->isLowerBound());
271 ArithVar x_i
= constraint
->getVariable();
272 const DeltaRational
& c_i
= constraint
->getValue();
274 Debug("arith") << "AssertLower(" << x_i
<< " " << c_i
<< ")"<< std::endl
;
276 Assert(!isInteger(x_i
) || c_i
.isIntegral());
278 //TODO Relax to less than?
279 if(d_partialModel
.lessThanLowerBound(x_i
, c_i
)){
283 int cmpToUB
= d_partialModel
.cmpToUpperBound(x_i
, c_i
);
284 if(cmpToUB
> 0){ // c_i < \lowerbound(x_i)
285 Constraint ubc
= d_partialModel
.getUpperBoundConstraint(x_i
);
286 Node conflict
= ConstraintValue::explainConflict(ubc
, constraint
);
287 Debug("arith") << "AssertLower conflict " << conflict
<< endl
;
288 ++(d_statistics
.d_statAssertLowerConflicts
);
289 d_raiseConflict(conflict
);
291 }else if(cmpToUB
== 0){
293 d_constantIntegerVariables
.push_back(x_i
);
294 Debug("dio::push") << x_i
<< endl
;
296 Constraint ub
= d_partialModel
.getUpperBoundConstraint(x_i
);
298 if(!d_congruenceManager
.isWatchedVariable(x_i
) || c_i
.sgn() != 0){
299 // if it is not a watched variable report it
300 // if it is is a watched variable and c_i == 0,
301 // let zeroDifferenceDetected(x_i) catch this
302 d_congruenceManager
.equalsConstant(constraint
, ub
);
305 const ValueCollection
& vc
= constraint
->getValueCollection();
306 if(vc
.hasDisequality()){
307 Assert(vc
.hasEquality());
308 const Constraint eq
= vc
.getEquality();
309 const Constraint diseq
= vc
.getDisequality();
311 //const Constraint ub = vc.getUpperBound();
312 Node conflict
= ConstraintValue::explainConflict(diseq
, ub
, constraint
);
314 ++(d_statistics
.d_statDisequalityConflicts
);
315 Debug("eq") << " assert lower conflict " << conflict
<< endl
;
316 d_raiseConflict(conflict
);
318 }else if(!eq
->isTrue()){
319 Debug("eq") << "lb == ub, propagate eq" << eq
<< endl
;
320 eq
->impliedBy(constraint
, d_partialModel
.getUpperBoundConstraint(x_i
));
321 // do not need to add to d_learnedBounds
326 const ValueCollection
& vc
= constraint
->getValueCollection();
328 if(vc
.hasDisequality()){
329 const Constraint diseq
= vc
.getDisequality();
331 const Constraint ub
= d_constraintDatabase
.ensureConstraint(const_cast<ValueCollection
&>(vc
), UpperBound
);
334 Node conflict
= ConstraintValue::explainConflict(diseq
, ub
, constraint
);
335 Debug("eq") << " assert upper conflict " << conflict
<< endl
;
336 d_raiseConflict(conflict
);
338 }else if(!ub
->negationHasProof()){
339 Constraint negUb
= ub
->getNegation();
340 negUb
->impliedBy(constraint
, diseq
);
341 d_learnedBounds
.push_back(negUb
);
347 d_currentPropagationList
.push_back(constraint
);
348 d_currentPropagationList
.push_back(d_partialModel
.getLowerBoundConstraint(x_i
));
350 d_partialModel
.setLowerBoundConstraint(constraint
);
352 if(d_congruenceManager
.isWatchedVariable(x_i
)){
355 d_congruenceManager
.watchedVariableCannotBeZero(constraint
);
356 }else if(sgn
== 0 && d_partialModel
.upperBoundIsZero(x_i
)){
357 zeroDifferenceDetected(x_i
);
361 d_updatedBounds
.softAdd(x_i
);
363 if(Debug
.isOn("model")) {
364 Debug("model") << "before" << endl
;
365 d_partialModel
.printModel(x_i
);
366 d_tableau
.debugPrintIsBasic(x_i
);
369 if(!d_tableau
.isBasic(x_i
)){
370 if(d_partialModel
.getAssignment(x_i
) < c_i
){
371 d_linEq
.update(x_i
, c_i
);
374 d_simplex
.updateBasic(x_i
);
377 if(Debug
.isOn("model")) {
378 Debug("model") << "after" << endl
;
379 d_partialModel
.printModel(x_i
);
380 d_tableau
.debugPrintIsBasic(x_i
);
386 /* procedure AssertUpper( x_i <= c_i) */
387 bool TheoryArith::AssertUpper(Constraint constraint
){
388 ArithVar x_i
= constraint
->getVariable();
389 const DeltaRational
& c_i
= constraint
->getValue();
391 Debug("arith") << "AssertUpper(" << x_i
<< " " << c_i
<< ")"<< std::endl
;
392 AssertArgument(constraint
!= NullConstraint
,
393 "AssertUpper() called on a NullConstraint.");
394 Assert(constraint
->isUpperBound());
396 //Too strong because of rounding with integers
397 //Assert(!constraint->hasLiteral() || original == constraint->getLiteral());
398 Assert(!isInteger(x_i
) || c_i
.isIntegral());
400 Debug("arith") << "AssertUpper(" << x_i
<< " " << c_i
<< ")"<< std::endl
;
402 if(d_partialModel
.greaterThanUpperBound(x_i
, c_i
) ){ // \upperbound(x_i) <= c_i
406 // cmpToLb = \lowerbound(x_i).cmp(c_i)
407 int cmpToLB
= d_partialModel
.cmpToLowerBound(x_i
, c_i
);
408 if( cmpToLB
< 0 ){ // \upperbound(x_i) < \lowerbound(x_i)
409 Constraint lbc
= d_partialModel
.getLowerBoundConstraint(x_i
);
410 Node conflict
= ConstraintValue::explainConflict(lbc
, constraint
);
411 Debug("arith") << "AssertUpper conflict " << conflict
<< endl
;
412 ++(d_statistics
.d_statAssertUpperConflicts
);
413 d_raiseConflict(conflict
);
415 }else if(cmpToLB
== 0){ // \lowerBound(x_i) == \upperbound(x_i)
417 d_constantIntegerVariables
.push_back(x_i
);
418 Debug("dio::push") << x_i
<< endl
;
420 Constraint lb
= d_partialModel
.getLowerBoundConstraint(x_i
);
421 if(!d_congruenceManager
.isWatchedVariable(x_i
) || c_i
.sgn() != 0){
422 // if it is not a watched variable report it
423 // if it is is a watched variable and c_i == 0,
424 // let zeroDifferenceDetected(x_i) catch this
425 d_congruenceManager
.equalsConstant(lb
, constraint
);
428 const ValueCollection
& vc
= constraint
->getValueCollection();
429 if(vc
.hasDisequality()){
430 Assert(vc
.hasEquality());
431 const Constraint diseq
= vc
.getDisequality();
432 const Constraint eq
= vc
.getEquality();
434 Node conflict
= ConstraintValue::explainConflict(diseq
, lb
, constraint
);
435 Debug("eq") << " assert upper conflict " << conflict
<< endl
;
436 d_raiseConflict(conflict
);
438 }else if(!eq
->isTrue()){
439 Debug("eq") << "lb == ub, propagate eq" << eq
<< endl
;
440 eq
->impliedBy(constraint
, d_partialModel
.getLowerBoundConstraint(x_i
));
441 //do not bother to add to d_learnedBounds
444 }else if(cmpToLB
> 0){
445 const ValueCollection
& vc
= constraint
->getValueCollection();
446 if(vc
.hasDisequality()){
447 const Constraint diseq
= vc
.getDisequality();
449 const Constraint lb
=
450 d_constraintDatabase
.ensureConstraint(const_cast<ValueCollection
&>(vc
), LowerBound
);
452 Node conflict
= ConstraintValue::explainConflict(diseq
, lb
, constraint
);
453 Debug("eq") << " assert upper conflict " << conflict
<< endl
;
454 d_raiseConflict(conflict
);
456 }else if(!lb
->negationHasProof()){
457 Constraint negLb
= lb
->getNegation();
458 negLb
->impliedBy(constraint
, diseq
);
459 //if(!negLb->canBePropagated()){
460 d_learnedBounds
.push_back(negLb
);
461 //}//otherwise let this be propagated/asserted later
467 d_currentPropagationList
.push_back(constraint
);
468 d_currentPropagationList
.push_back(d_partialModel
.getUpperBoundConstraint(x_i
));
469 //It is fine if this is NullConstraint
471 d_partialModel
.setUpperBoundConstraint(constraint
);
473 if(d_congruenceManager
.isWatchedVariable(x_i
)){
476 d_congruenceManager
.watchedVariableCannotBeZero(constraint
);
477 }else if(sgn
== 0 && d_partialModel
.lowerBoundIsZero(x_i
)){
478 zeroDifferenceDetected(x_i
);
482 d_updatedBounds
.softAdd(x_i
);
484 if(Debug
.isOn("model")) {
485 Debug("model") << "before" << endl
;
486 d_partialModel
.printModel(x_i
);
487 d_tableau
.debugPrintIsBasic(x_i
);
490 if(!d_tableau
.isBasic(x_i
)){
491 if(d_partialModel
.getAssignment(x_i
) > c_i
){
492 d_linEq
.update(x_i
, c_i
);
495 d_simplex
.updateBasic(x_i
);
498 if(Debug
.isOn("model")) {
499 Debug("model") << "after" << endl
;
500 d_partialModel
.printModel(x_i
);
501 d_tableau
.debugPrintIsBasic(x_i
);
508 /* procedure AssertEquality( x_i == c_i ) */
509 bool TheoryArith::AssertEquality(Constraint constraint
){
510 AssertArgument(constraint
!= NullConstraint
,
511 "AssertUpper() called on a NullConstraint.");
513 ArithVar x_i
= constraint
->getVariable();
514 const DeltaRational
& c_i
= constraint
->getValue();
516 Debug("arith") << "AssertEquality(" << x_i
<< " " << c_i
<< ")"<< std::endl
;
518 //Should be fine in integers
519 Assert(!isInteger(x_i
) || c_i
.isIntegral());
521 int cmpToLB
= d_partialModel
.cmpToLowerBound(x_i
, c_i
);
522 int cmpToUB
= d_partialModel
.cmpToUpperBound(x_i
, c_i
);
525 // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
526 if(cmpToUB
>= 0 && cmpToLB
<= 0){
531 Constraint ubc
= d_partialModel
.getUpperBoundConstraint(x_i
);
532 Node conflict
= ConstraintValue::explainConflict(ubc
, constraint
);
533 Debug("arith") << "AssertEquality conflicts with upper bound " << conflict
<< endl
;
534 d_raiseConflict(conflict
);
539 Constraint lbc
= d_partialModel
.getLowerBoundConstraint(x_i
);
540 Node conflict
= ConstraintValue::explainConflict(lbc
, constraint
);
541 Debug("arith") << "AssertEquality conflicts with lower bound" << conflict
<< endl
;
542 d_raiseConflict(conflict
);
546 Assert(cmpToUB
<= 0);
547 Assert(cmpToLB
>= 0);
548 Assert(cmpToUB
< 0 || cmpToLB
> 0);
552 d_constantIntegerVariables
.push_back(x_i
);
553 Debug("dio::push") << x_i
<< endl
;
556 // Don't bother to check whether x_i != c_i is in d_diseq
557 // The a and (not a) should never be on the fact queue
558 d_currentPropagationList
.push_back(constraint
);
559 d_currentPropagationList
.push_back(d_partialModel
.getLowerBoundConstraint(x_i
));
560 d_currentPropagationList
.push_back(d_partialModel
.getUpperBoundConstraint(x_i
));
562 d_partialModel
.setUpperBoundConstraint(constraint
);
563 d_partialModel
.setLowerBoundConstraint(constraint
);
565 if(d_congruenceManager
.isWatchedVariable(x_i
)){
568 zeroDifferenceDetected(x_i
);
570 d_congruenceManager
.watchedVariableCannotBeZero(constraint
);
571 d_congruenceManager
.equalsConstant(constraint
);
574 d_congruenceManager
.equalsConstant(constraint
);
577 d_updatedBounds
.softAdd(x_i
);
579 if(Debug
.isOn("model")) {
580 Debug("model") << "before" << endl
;
581 d_partialModel
.printModel(x_i
);
582 d_tableau
.debugPrintIsBasic(x_i
);
585 if(!d_tableau
.isBasic(x_i
)){
586 if(!(d_partialModel
.getAssignment(x_i
) == c_i
)){
587 d_linEq
.update(x_i
, c_i
);
590 d_simplex
.updateBasic(x_i
);
593 if(Debug
.isOn("model")) {
594 Debug("model") << "after" << endl
;
595 d_partialModel
.printModel(x_i
);
596 d_tableau
.debugPrintIsBasic(x_i
);
603 /* procedure AssertDisequality( x_i != c_i ) */
604 bool TheoryArith::AssertDisequality(Constraint constraint
){
606 AssertArgument(constraint
!= NullConstraint
,
607 "AssertUpper() called on a NullConstraint.");
608 ArithVar x_i
= constraint
->getVariable();
609 const DeltaRational
& c_i
= constraint
->getValue();
611 Debug("arith") << "AssertDisequality(" << x_i
<< " " << c_i
<< ")"<< std::endl
;
613 //Should be fine in integers
614 Assert(!isInteger(x_i
) || c_i
.isIntegral());
616 if(d_congruenceManager
.isWatchedVariable(x_i
)){
619 d_congruenceManager
.watchedVariableCannotBeZero(constraint
);
623 const ValueCollection
& vc
= constraint
->getValueCollection();
624 if(vc
.hasLowerBound() && vc
.hasUpperBound()){
625 const Constraint lb
= vc
.getLowerBound();
626 const Constraint ub
= vc
.getUpperBound();
627 if(lb
->isTrue() && ub
->isTrue()){
629 Debug("eq") << "explaining" << endl
;
630 ++(d_statistics
.d_statDisequalityConflicts
);
631 Node conflict
= ConstraintValue::explainConflict(constraint
, lb
, ub
);
632 d_raiseConflict(conflict
);
636 if(vc
.hasLowerBound() ){
637 const Constraint lb
= vc
.getLowerBound();
639 const Constraint ub
= d_constraintDatabase
.ensureConstraint(const_cast<ValueCollection
&>(vc
), UpperBound
);
640 Debug("eq") << "propagate UpperBound " << constraint
<< lb
<< ub
<< endl
;
641 const Constraint negUb
= ub
->getNegation();
642 if(!negUb
->isTrue()){
643 negUb
->impliedBy(constraint
, lb
);
644 d_learnedBounds
.push_back(negUb
);
648 if(vc
.hasUpperBound()){
649 const Constraint ub
= vc
.getUpperBound();
651 const Constraint lb
= d_constraintDatabase
.ensureConstraint(const_cast<ValueCollection
&>(vc
), LowerBound
);
653 Debug("eq") << "propagate LowerBound " << constraint
<< lb
<< ub
<< endl
;
654 const Constraint negLb
= lb
->getNegation();
655 if(!negLb
->isTrue()){
656 negLb
->impliedBy(constraint
, ub
);
657 d_learnedBounds
.push_back(negLb
);
662 bool split
= constraint
->isSplit();
664 if(!split
&& c_i
== d_partialModel
.getAssignment(x_i
)){
665 Debug("eq") << "lemma now! " << constraint
<< endl
;
666 d_out
->lemma(constraint
->split());
668 }else if(d_partialModel
.strictlyLessThanLowerBound(x_i
, c_i
)){
669 Debug("eq") << "can drop as less than lb" << constraint
<< endl
;
670 }else if(d_partialModel
.strictlyGreaterThanUpperBound(x_i
, c_i
)){
671 Debug("eq") << "can drop as less than ub" << constraint
<< endl
;
673 Debug("eq") << "push back" << constraint
<< endl
;
674 d_diseqQueue
.push(constraint
);
675 d_partialModel
.invalidateDelta();
677 Debug("eq") << "skipping already split " << constraint
<< endl
;
682 void TheoryArith::addSharedTerm(TNode n
){
683 Debug("arith::addSharedTerm") << "addSharedTerm: " << n
<< endl
;
685 d_partialModel
.invalidateDelta();
688 d_congruenceManager
.addSharedTerm(n
);
689 if(!n
.isConst() && !isSetup(n
)){
690 Polynomial poly
= Polynomial::parsePolynomial(n
);
691 Polynomial::iterator it
= poly
.begin();
692 Polynomial::iterator it_end
= poly
.end();
693 for (; it
!= it_end
; ++ it
) {
695 if (!m
.isConstant() && !isSetup(m
.getVarList().getNode())) {
696 setupVariableList(m
.getVarList());
702 Node
TheoryArith::ppRewrite(TNode atom
) {
703 Debug("arith::preprocess") << "arith::preprocess() : " << atom
<< endl
;
706 if (atom
.getKind() == kind::EQUAL
&& options::arithRewriteEq()) {
707 Node leq
= NodeBuilder
<2>(kind::LEQ
) << atom
[0] << atom
[1];
708 Node geq
= NodeBuilder
<2>(kind::GEQ
) << atom
[0] << atom
[1];
709 Node rewritten
= Rewriter::rewrite(leq
.andNode(geq
));
710 Debug("arith::preprocess") << "arith::preprocess() : returning "
711 << rewritten
<< endl
;
718 Theory::PPAssertStatus
TheoryArith::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) {
719 TimerStat::CodeTimer
codeTimer(d_statistics
.d_simplifyTimer
);
720 Debug("simplify") << "TheoryArith::solve(" << in
<< ")" << endl
;
724 Rational minConstant
= 0;
727 if (in
.getKind() == kind::EQUAL
) {
728 Comparison cmp
= Comparison::parseNormalForm(in
);
730 Polynomial left
= cmp
.getLeft();
731 Polynomial right
= cmp
.getRight();
733 Monomial m
= left
.getHead();
734 if (m
.getVarList().singleton()){
735 VarList vl
= m
.getVarList();
736 Node var
= vl
.getNode();
737 if (var
.getKind() == kind::VARIABLE
){
738 // if vl.isIntegral then m.getConstant().isOne()
739 if(!vl
.isIntegral() || m
.getConstant().isOne()){
745 // Solve for variable
746 if (!minVar
.isNull()) {
747 Polynomial right
= cmp
.getRight();
748 Node elim
= right
.getNode();
749 // ax + p = c -> (ax + p) -ax - c = -ax
750 // x = (p - ax - c) * -1/a
751 // Add the substitution if not recursive
752 Assert(elim
== Rewriter::rewrite(elim
));
755 static const unsigned MAX_SUB_SIZE
= 20;
756 if(false && right
.size() > MAX_SUB_SIZE
){
757 Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar
<< ":" << elim
<< endl
;
758 Debug("simplify") << right
.size() << endl
;
759 }else if(elim
.hasSubterm(minVar
)){
760 Debug("simplify") << "TheoryArith::solve(): can't substitute due to recursive pattern with sharing: " << minVar
<< ":" << elim
<< endl
;
761 }else if (!minVar
.getType().isInteger() || right
.isIntegral()) {
762 Assert(!elim
.hasSubterm(minVar
));
763 // cannot eliminate integers here unless we know the resulting
764 // substitution is integral
765 Debug("simplify") << "TheoryArith::solve(): substitution " << minVar
<< " |-> " << elim
<< endl
;
767 outSubstitutions
.addSubstitution(minVar
, elim
);
768 return PP_ASSERT_STATUS_SOLVED
;
770 Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar
<< ":" << minVar
.getType() << " |-> " << elim
<< ":" << elim
.getType() << endl
;
775 // If a relation, remember the bound
776 switch(in
.getKind()) {
782 d_learner
.addBound(in
);
790 return PP_ASSERT_STATUS_UNSOLVED
;
793 void TheoryArith::ppStaticLearn(TNode n
, NodeBuilder
<>& learned
) {
794 TimerStat::CodeTimer
codeTimer(d_statistics
.d_staticLearningTimer
);
796 d_learner
.staticLearning(n
, learned
);
801 ArithVar
TheoryArith::findShortestBasicRow(ArithVar variable
){
802 ArithVar bestBasic
= ARITHVAR_SENTINEL
;
803 uint64_t bestRowLength
= std::numeric_limits
<uint64_t>::max();
805 Tableau::ColIterator basicIter
= d_tableau
.colIterator(variable
);
806 for(; !basicIter
.atEnd(); ++basicIter
){
807 const Tableau::Entry
& entry
= *basicIter
;
808 Assert(entry
.getColVar() == variable
);
809 RowIndex ridx
= entry
.getRowIndex();
810 ArithVar basic
= d_tableau
.rowIndexToBasic(ridx
);
811 uint32_t rowLength
= d_tableau
.getRowLength(ridx
);
812 if((rowLength
< bestRowLength
) ||
813 (rowLength
== bestRowLength
&& basic
< bestBasic
)){
815 bestRowLength
= rowLength
;
818 Assert(bestBasic
== ARITHVAR_SENTINEL
|| bestRowLength
< std::numeric_limits
<uint32_t>::max());
822 void TheoryArith::setupVariable(const Variable
& x
){
823 Node n
= x
.getNode();
827 ++(d_statistics
.d_statUserVariables
);
828 requestArithVar(n
,false);
829 //ArithVar varN = requestArithVar(n,false);
830 //setupInitialValue(varN);
841 void TheoryArith::setupVariableList(const VarList
& vl
){
844 TNode vlNode
= vl
.getNode();
845 Assert(!isSetup(vlNode
));
846 Assert(!d_arithvarNodeMap
.hasArithVar(vlNode
));
848 for(VarList::iterator i
= vl
.begin(), end
= vl
.end(); i
!= end
; ++i
){
851 if(!isSetup(var
.getNode())){
857 // vl is the product of at least 2 variables
858 // vl : (* v1 v2 ...)
859 if(getLogicInfo().isLinear()){
860 throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
863 d_out
->setIncomplete();
864 d_nlIncomplete
= true;
866 ++(d_statistics
.d_statUserVariables
);
867 requestArithVar(vlNode
, false);
868 //ArithVar av = requestArithVar(vlNode, false);
869 //setupInitialValue(av);
875 * Only call markSetup if the VarList is not a singleton.
876 * See the comment in setupPolynomail for more.
880 void TheoryArith::cautiousSetupPolynomial(const Polynomial
& p
){
881 if(p
.containsConstant()){
883 Polynomial noConstant
= p
.getTail();
884 if(!isSetup(noConstant
.getNode())){
885 setupPolynomial(noConstant
);
888 }else if(!isSetup(p
.getNode())){
893 void TheoryArith::setupDivLike(const Variable
& v
){
894 Assert(v
.isDivLike());
896 if(getLogicInfo().isLinear()){
897 throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
900 Node vnode
= v
.getNode();
901 Assert(isSetup(vnode
)); // Otherwise there is some invariant breaking recursion
902 Polynomial m
= Polynomial::parsePolynomial(vnode
[0]);
903 Polynomial n
= Polynomial::parsePolynomial(vnode
[1]);
905 cautiousSetupPolynomial(m
);
906 cautiousSetupPolynomial(n
);
909 switch(vnode
.getKind()){
913 lem
= definingIteForDivLike(vnode
);
916 lem
= axiomIteForTotalDivision(vnode
);
918 case INTS_DIVISION_TOTAL
:
919 case INTS_MODULUS_TOTAL
:
920 lem
= axiomIteForTotalIntDivision(vnode
);
923 /* intentionally blank */
928 Debug("arith::div") << lem
<< endl
;
933 Node
TheoryArith::definingIteForDivLike(Node divLike
){
934 Kind k
= divLike
.getKind();
935 Assert(k
== DIVISION
|| k
== INTS_DIVISION
|| k
== INTS_MODULUS
);
936 // (for all ((n Real) (d Real))
940 // (APPLY [div_0_skolem_function] n)
941 // (DIVISION_TOTAL x y))))
943 Polynomial n
= Polynomial::parsePolynomial(divLike
[0]);
944 Polynomial d
= Polynomial::parsePolynomial(divLike
[1]);
946 NodeManager
* currNM
= NodeManager::currentNM();
947 Node dEq0
= currNM
->mkNode(EQUAL
, d
.getNode(), mkRationalNode(0));
949 Kind kTotal
= (k
== DIVISION
) ? DIVISION_TOTAL
:
950 (k
== INTS_DIVISION
) ? INTS_DIVISION_TOTAL
: INTS_MODULUS_TOTAL
;
952 Node by0Func
= (k
== DIVISION
) ? getRealDivideBy0Func():
953 (k
== INTS_DIVISION
) ? getIntDivideBy0Func() : getIntModulusBy0Func();
956 Debug("arith::div") << divLike
<< endl
;
957 Debug("arith::div") << by0Func
<< endl
;
959 Node divTotal
= currNM
->mkNode(kTotal
, n
.getNode(), d
.getNode());
960 Node divZero
= currNM
->mkNode(APPLY_UF
, by0Func
, n
.getNode());
962 Node defining
= divLike
.eqNode(dEq0
.iteNode( divZero
, divTotal
));
967 Node
TheoryArith::axiomIteForTotalDivision(Node div_tot
){
968 Assert(div_tot
.getKind() == DIVISION_TOTAL
);
970 // Inverse of multiplication axiom:
971 // (for all ((n Real) (d Real))
973 // (= (DIVISION_TOTAL n d) 0)
974 // (= (* d (DIVISION_TOTAL n d)) n)))
977 Polynomial n
= Polynomial::parsePolynomial(div_tot
[0]);
978 Polynomial d
= Polynomial::parsePolynomial(div_tot
[1]);
979 Polynomial div_tot_p
= Polynomial::parsePolynomial(div_tot
);
981 Comparison invEq
= Comparison::mkComparison(EQUAL
, n
, d
* div_tot_p
);
982 Comparison zeroEq
= Comparison::mkComparison(EQUAL
, div_tot_p
, Polynomial::mkZero());
983 Node dEq0
= (d
.getNode()).eqNode(mkRationalNode(0));
984 Node ite
= dEq0
.iteNode(zeroEq
.getNode(), invEq
.getNode());
989 Node
TheoryArith::axiomIteForTotalIntDivision(Node int_div_like
){
990 Kind k
= int_div_like
.getKind();
991 Assert(k
== INTS_DIVISION_TOTAL
|| k
== INTS_MODULUS_TOTAL
);
993 // (for all ((m Int) (n Int))
994 // (=> (distinct n 0)
995 // (let ((q (div m n)) (r (mod m n)))
996 // (and (= m (+ (* n q) r))
997 // (<= 0 r (- (abs n) 1))))))
999 // Updated for div 0 functions
1000 // (for all ((m Int) (n Int))
1001 // (let ((q (div m n)) (r (mod m n)))
1003 // (and (= q (div_0_func m)) (= r (mod_0_func m)))
1004 // (and (= m (+ (* n q) r))
1005 // (<= 0 r (- (abs n) 1)))))))
1007 Polynomial n
= Polynomial::parsePolynomial(int_div_like
[0]);
1008 Polynomial d
= Polynomial::parsePolynomial(int_div_like
[1]);
1010 NodeManager
* currNM
= NodeManager::currentNM();
1011 Node zero
= mkRationalNode(0);
1013 Node q
= (k
== INTS_DIVISION_TOTAL
) ? int_div_like
: currNM
->mkNode(INTS_DIVISION_TOTAL
, n
.getNode(), d
.getNode());
1014 Node r
= (k
== INTS_MODULUS_TOTAL
) ? int_div_like
: currNM
->mkNode(INTS_MODULUS_TOTAL
, n
.getNode(), d
.getNode());
1016 Node dEq0
= (d
.getNode()).eqNode(zero
);
1017 Node qEq0
= q
.eqNode(zero
);
1018 Node rEq0
= r
.eqNode(zero
);
1020 Polynomial rp
= Polynomial::parsePolynomial(r
);
1021 Polynomial qp
= Polynomial::parsePolynomial(q
);
1023 Node abs_d
= (n
.isConstant()) ?
1024 d
.getHead().getConstant().abs().getNode() : mkIntSkolem("abs_$$");
1026 Node eq
= Comparison::mkComparison(EQUAL
, n
, d
* qp
+ rp
).getNode();
1027 Node leq0
= currNM
->mkNode(LEQ
, zero
, r
);
1028 Node leq1
= currNM
->mkNode(LT
, r
, abs_d
);
1030 Node andE
= currNM
->mkNode(AND
, eq
, leq0
, leq1
);
1031 Node defDivMode
= dEq0
.iteNode(qEq0
.andNode(rEq0
), andE
);
1032 Node lem
= abs_d
.getMetaKind () == metakind::VARIABLE
?
1033 defDivMode
.andNode(d
.makeAbsCondition(Variable(abs_d
))) : defDivMode
;
1039 void TheoryArith::setupPolynomial(const Polynomial
& poly
) {
1040 Assert(!poly
.containsConstant());
1041 TNode polyNode
= poly
.getNode();
1042 Assert(!isSetup(polyNode
));
1043 Assert(!d_arithvarNodeMap
.hasArithVar(polyNode
));
1045 for(Polynomial::iterator i
= poly
.begin(), end
= poly
.end(); i
!= end
; ++i
){
1047 const VarList
& vl
= mono
.getVarList();
1048 if(!isSetup(vl
.getNode())){
1049 setupVariableList(vl
);
1053 if(polyNode
.getKind() == PLUS
){
1054 d_tableauSizeHasBeenModified
= true;
1056 vector
<ArithVar
> variables
;
1057 vector
<Rational
> coefficients
;
1058 asVectors(poly
, coefficients
, variables
);
1060 ArithVar varSlack
= requestArithVar(polyNode
, true);
1061 d_tableau
.addRow(varSlack
, coefficients
, variables
);
1062 setupBasicValue(varSlack
);
1064 //Add differences to the difference manager
1065 Polynomial::iterator i
= poly
.begin(), end
= poly
.end();
1067 Monomial first
= *i
;
1070 Monomial second
= *i
;
1073 if(first
.getConstant().isOne() && second
.getConstant().getValue() == -1){
1074 VarList vl0
= first
.getVarList();
1075 VarList vl1
= second
.getVarList();
1076 if(vl0
.singleton() && vl1
.singleton()){
1077 d_congruenceManager
.addWatchedPair(varSlack
, vl0
.getNode(), vl1
.getNode());
1084 ++(d_statistics
.d_statSlackVariables
);
1085 markSetup(polyNode
);
1089 * It is worth documenting that polyNode should only be marked as
1090 * being setup by this function if it has kind PLUS.
1091 * Other kinds will be marked as being setup by lower levels of setup
1092 * specifically setupVariableList.
1096 void TheoryArith::setupAtom(TNode atom
) {
1097 Assert(isRelationOperator(atom
.getKind()));
1098 Assert(Comparison::isNormalAtom(atom
));
1099 Assert(!isSetup(atom
));
1100 Assert(!d_constraintDatabase
.hasLiteral(atom
));
1102 Comparison cmp
= Comparison::parseNormalForm(atom
);
1103 Polynomial nvp
= cmp
.normalizedVariablePart();
1104 Assert(!nvp
.isZero());
1106 if(!isSetup(nvp
.getNode())){
1107 setupPolynomial(nvp
);
1110 d_constraintDatabase
.addLiteral(atom
);
1115 void TheoryArith::preRegisterTerm(TNode n
) {
1116 Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n
<<")"<< endl
;
1118 if(isRelationOperator(n
.getKind())){
1122 Constraint c
= d_constraintDatabase
.lookup(n
);
1123 Assert(c
!= NullConstraint
);
1125 Debug("arith::preregister") << "setup constraint" << c
<< endl
;
1126 Assert(!c
->canBePropagated());
1127 c
->setPreregistered();
1130 Debug("arith::preregister") << "end arith::preRegisterTerm("<< n
<<")" << endl
;
1133 void TheoryArith::releaseArithVar(ArithVar v
){
1134 Assert(d_arithvarNodeMap
.hasNode(v
));
1136 d_constraintDatabase
.removeVariable(v
);
1137 d_arithvarNodeMap
.remove(v
);
1139 d_pool
.push_back(v
);
1142 ArithVar
TheoryArith::requestArithVar(TNode x
, bool slack
){
1143 //TODO : The VarList trick is good enough?
1144 Assert(isLeaf(x
) || VarList::isMember(x
) || x
.getKind() == PLUS
);
1145 if(getLogicInfo().isLinear() && Variable::isDivMember(x
)){
1146 throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
1148 Assert(!d_arithvarNodeMap
.hasArithVar(x
));
1149 Assert(x
.getType().isReal());// real or integer
1151 // ArithVar varX = d_variables.size();
1152 // d_variables.push_back(Node(x));
1154 bool reclaim
= !d_pool
.empty();
1158 varX
= d_pool
.back();
1161 d_partialModel
.setAssignment(varX
, d_DELTA_ZERO
, d_DELTA_ZERO
);
1163 varX
= d_numberOfVariables
;
1164 ++d_numberOfVariables
;
1166 d_slackVars
.push_back(true);
1167 d_variableTypes
.push_back(ATReal
);
1169 d_simplex
.increaseMax();
1171 d_tableau
.increaseSize();
1172 d_tableauSizeHasBeenModified
= true;
1174 d_partialModel
.initialize(varX
, d_DELTA_ZERO
);
1179 //The type computation is not quite accurate for Rationals that are integral.
1180 //We'll use the isIntegral check from the polynomial package instead.
1181 Polynomial p
= Polynomial::parsePolynomial(x
);
1182 type
= p
.isIntegral() ? ATInteger
: ATReal
;
1184 type
= nodeToArithType(x
);
1186 d_variableTypes
[varX
] = type
;
1187 d_slackVars
[varX
] = slack
;
1189 d_constraintDatabase
.addVariable(varX
);
1191 d_arithvarNodeMap
.setArithVar(x
,varX
);
1193 // Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl;
1196 // //The type computation is not quite accurate for Rationals that are integral.
1197 // //We'll use the isIntegral check from the polynomial package instead.
1198 // Polynomial p = Polynomial::parsePolynomial(x);
1199 // d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal);
1201 // d_variableTypes.push_back(nodeToArithType(x));
1204 // d_slackVars.push_back(slack);
1206 // d_simplex.increaseMax();
1208 // d_tableau.increaseSize();
1209 // d_tableauSizeHasBeenModified = true;
1211 // d_constraintDatabase.addVariable(varX);
1213 Debug("arith::arithvar") << x
<< " |-> " << varX
<< endl
;
1215 Assert(!d_partialModel
.hasUpperBound(varX
));
1216 Assert(!d_partialModel
.hasLowerBound(varX
));
1221 void TheoryArith::asVectors(const Polynomial
& p
, std::vector
<Rational
>& coeffs
, std::vector
<ArithVar
>& variables
) {
1222 for(Polynomial::iterator i
= p
.begin(), end
= p
.end(); i
!= end
; ++i
){
1223 const Monomial
& mono
= *i
;
1224 const Constant
& constant
= mono
.getConstant();
1225 const VarList
& variable
= mono
.getVarList();
1227 Node n
= variable
.getNode();
1229 Debug("rewriter") << "should be var: " << n
<< endl
;
1231 // TODO: This VarList::isMember(n) can be stronger
1232 Assert(isLeaf(n
) || VarList::isMember(n
));
1233 Assert(theoryOf(n
) != THEORY_ARITH
|| d_arithvarNodeMap
.hasArithVar(n
));
1235 Assert(d_arithvarNodeMap
.hasArithVar(n
));
1236 ArithVar av
= d_arithvarNodeMap
.asArithVar(n
);
1238 coeffs
.push_back(constant
.getValue());
1239 variables
.push_back(av
);
1244 * For basic variables the row must have been added to the tableau.
1246 void TheoryArith::setupBasicValue(ArithVar x
){
1247 Assert(d_tableau
.isBasic(x
));
1249 // if(!d_tableau.isBasic(x)){
1250 // d_partialModel.setAssignment(x, d_DELTA_ZERO, d_DELTA_ZERO);
1252 //If the variable is basic, assertions may have already happened and updates
1253 //may have occured before setting this variable up.
1255 //This can go away if the tableau creation is done at preregister
1256 //time instead of register
1257 DeltaRational safeAssignment
= d_linEq
.computeRowValue(x
, true);
1258 DeltaRational assignment
= d_linEq
.computeRowValue(x
, false);
1259 //d_partialModel.initialize(x,safeAssignment);
1260 //d_partialModel.setAssignment(x,assignment);
1261 d_partialModel
.setAssignment(x
,safeAssignment
,assignment
);
1264 Debug("arith") << "setupVariable("<<x
<<")"<<std::endl
;
1267 ArithVar
TheoryArith::determineArithVar(const Polynomial
& p
) const{
1268 Assert(!p
.containsConstant());
1269 Assert(p
.getHead().constantIsPositive());
1270 TNode n
= p
.getNode();
1271 Debug("determineArithVar") << "determineArithVar(" << n
<< ")" << endl
;
1272 return d_arithvarNodeMap
.asArithVar(n
);
1275 ArithVar
TheoryArith::determineArithVar(TNode assertion
) const{
1276 Debug("determineArithVar") << "determineArithVar " << assertion
<< endl
;
1277 Comparison cmp
= Comparison::parseNormalForm(assertion
);
1278 Polynomial variablePart
= cmp
.normalizedVariablePart();
1279 return determineArithVar(variablePart
);
1283 bool TheoryArith::canSafelyAvoidEqualitySetup(TNode equality
){
1284 Assert(equality
.getKind() == EQUAL
);
1285 return d_arithvarNodeMap
.hasArithVar(equality
[0]);
1288 Comparison
TheoryArith::mkIntegerEqualityFromAssignment(ArithVar v
){
1289 const DeltaRational
& beta
= d_partialModel
.getAssignment(v
);
1291 Assert(beta
.isIntegral());
1292 Polynomial
betaAsPolynomial( Constant::mkConstant(beta
.floor()) );
1294 TNode var
= d_arithvarNodeMap
.asNode(v
);
1295 Polynomial varAsPolynomial
= Polynomial::parsePolynomial(var
);
1296 return Comparison::mkComparison(EQUAL
, varAsPolynomial
, betaAsPolynomial
);
1299 Node
TheoryArith::dioCutting(){
1300 context::Context::ScopedPush
speculativePush(getSatContext());
1301 //DO NOT TOUCH THE OUTPUTSTREAM
1303 for(var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
1306 const DeltaRational
& dr
= d_partialModel
.getAssignment(v
);
1307 if(d_partialModel
.equalsUpperBound(v
, dr
) || d_partialModel
.equalsLowerBound(v
, dr
)){
1308 if(!d_partialModel
.boundsAreEqual(v
)){
1309 // If the bounds are equal this is already in the dioSolver
1310 //Add v = dr as a speculation.
1311 Comparison eq
= mkIntegerEqualityFromAssignment(v
);
1312 Debug("dio::push") <<v
<< " " << eq
.getNode() << endl
;
1313 Assert(!eq
.isBoolean());
1314 d_diosolver
.pushInputConstraint(eq
, eq
.getNode());
1315 // It does not matter what the explanation of eq is.
1316 // It cannot be used in a conflict
1322 SumPair plane
= d_diosolver
.processEquationsForCut();
1324 return Node::null();
1326 Polynomial p
= plane
.getPolynomial();
1327 Polynomial
c(plane
.getConstant() * Constant::mkConstant(-1));
1328 Integer gcd
= p
.gcd();
1329 Assert(p
.isIntegral());
1330 Assert(c
.isIntegral());
1332 Assert(!gcd
.divides(c
.asConstant().getNumerator()));
1333 Comparison leq
= Comparison::mkComparison(LEQ
, p
, c
);
1334 Comparison geq
= Comparison::mkComparison(GEQ
, p
, c
);
1335 Node lemma
= NodeManager::currentNM()->mkNode(OR
, leq
.getNode(), geq
.getNode());
1336 Node rewrittenLemma
= Rewriter::rewrite(lemma
);
1337 Debug("arith::dio") << "dioCutting found the plane: " << plane
.getNode() << endl
;
1338 Debug("arith::dio") << "resulting in the cut: " << lemma
<< endl
;
1339 Debug("arith::dio") << "rewritten " << rewrittenLemma
<< endl
;
1340 return rewrittenLemma
;
1344 Node
TheoryArith::callDioSolver(){
1345 while(!d_constantIntegerVariables
.empty()){
1346 ArithVar v
= d_constantIntegerVariables
.front();
1347 d_constantIntegerVariables
.pop();
1349 Debug("arith::dio") << v
<< endl
;
1351 Assert(isInteger(v
));
1352 Assert(d_partialModel
.boundsAreEqual(v
));
1355 Constraint lb
= d_partialModel
.getLowerBoundConstraint(v
);
1356 Constraint ub
= d_partialModel
.getUpperBoundConstraint(v
);
1358 Node orig
= Node::null();
1359 if(lb
->isEquality()){
1360 orig
= lb
->explainForConflict();
1361 }else if(ub
->isEquality()){
1362 orig
= ub
->explainForConflict();
1364 orig
= ConstraintValue::explainConflict(ub
, lb
);
1367 Assert(d_partialModel
.assignmentIsConsistent(v
));
1369 Comparison eq
= mkIntegerEqualityFromAssignment(v
);
1372 //This can only be a conflict
1373 Assert(!eq
.getNode().getConst
<bool>());
1375 //This should be handled by the normal form earlier in the case of equality
1376 Assert(orig
.getKind() != EQUAL
);
1379 Debug("dio::push") << v
<< " " << eq
.getNode() << " with reason " << orig
<< endl
;
1380 d_diosolver
.pushInputConstraint(eq
, orig
);
1384 return d_diosolver
.processEquationsForConflict();
1387 Constraint
TheoryArith::constraintFromFactQueue(){
1389 TNode assertion
= get();
1391 Kind simpleKind
= Comparison::comparisonKind(assertion
);
1392 Constraint constraint
= d_constraintDatabase
.lookup(assertion
);
1393 if(constraint
== NullConstraint
){
1394 Assert(simpleKind
== EQUAL
|| simpleKind
== DISTINCT
);
1395 bool isDistinct
= simpleKind
== DISTINCT
;
1396 Node eq
= (simpleKind
== DISTINCT
) ? assertion
[0] : assertion
;
1397 Assert(!isSetup(eq
));
1398 Node reEq
= Rewriter::rewrite(eq
);
1399 if(reEq
.getKind() == CONST_BOOLEAN
){
1400 if(reEq
.getConst
<bool>() == isDistinct
){
1401 // if is (not true), or false
1402 Assert((reEq
.getConst
<bool>() && isDistinct
) ||
1403 (!reEq
.getConst
<bool>() && !isDistinct
));
1404 d_raiseConflict(assertion
);
1406 return NullConstraint
;
1408 Assert(reEq
.getKind() != CONST_BOOLEAN
);
1412 Node reAssertion
= isDistinct
? reEq
.notNode() : reEq
;
1413 constraint
= d_constraintDatabase
.lookup(reAssertion
);
1415 if(assertion
!= reAssertion
){
1416 Debug("arith::nf") << "getting non-nf assertion " << assertion
<< " |-> " << reAssertion
<< endl
;
1417 Assert(constraint
!= NullConstraint
);
1418 d_assertionsThatDoNotMatchTheirLiterals
.insert(assertion
, constraint
);
1422 // Kind simpleKind = Comparison::comparisonKind(assertion);
1423 // Assert(simpleKind != UNDEFINED_KIND);
1424 // Assert(constraint != NullConstraint ||
1425 // simpleKind == EQUAL ||
1426 // simpleKind == DISTINCT );
1427 // if(simpleKind == EQUAL || simpleKind == DISTINCT){
1428 // Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
1430 // if(!isSetup(eq)){
1431 // //The previous code was equivalent to:
1433 // constraint = d_constraintDatabase.lookup(assertion);
1436 Assert(constraint
!= NullConstraint
);
1438 if(constraint
->negationHasProof()){
1439 Constraint negation
= constraint
->getNegation();
1440 if(negation
->isSelfExplaining()){
1441 if(Debug
.isOn("whytheoryenginewhy")){
1445 Debug("arith::eq") << constraint
<< endl
;
1446 Debug("arith::eq") << negation
<< endl
;
1448 NodeBuilder
<> nb(kind::AND
);
1450 negation
->explainForConflict(nb
);
1452 Debug("arith::eq") << "conflict" << conflict
<< endl
;
1453 d_raiseConflict(conflict
);
1454 return NullConstraint
;
1456 Assert(!constraint
->negationHasProof());
1458 if(constraint
->assertedToTheTheory()){
1460 return NullConstraint
;
1462 Debug("arith::constraint") << "arith constraint " << constraint
<< std::endl
;
1463 constraint
->setAssertedToTheTheory(assertion
);
1465 if(!constraint
->hasProof()){
1466 Debug("arith::constraint") << "marking as constraint as self explaining " << endl
;
1467 constraint
->selfExplaining();
1469 Debug("arith::constraint") << "already has proof: " << constraint
->explainForConflict() << endl
;
1476 bool TheoryArith::assertionCases(Constraint constraint
){
1477 Assert(constraint
->hasProof());
1478 Assert(!constraint
->negationHasProof());
1480 ArithVar x_i
= constraint
->getVariable();
1482 switch(constraint
->getType()){
1484 if(isInteger(x_i
) && constraint
->isStrictUpperBound()){
1485 Constraint floorConstraint
= constraint
->getFloor();
1486 if(!floorConstraint
->isTrue()){
1487 if(floorConstraint
->negationHasProof()){
1488 Node conf
= ConstraintValue::explainConflict(constraint
, floorConstraint
->getNegation());
1489 d_raiseConflict(conf
);
1492 floorConstraint
->impliedBy(constraint
);
1493 // Do not need to add to d_learnedBounds
1496 return AssertUpper(floorConstraint
);
1498 return AssertUpper(constraint
);
1501 if(isInteger(x_i
) && constraint
->isStrictLowerBound()){
1502 Constraint ceilingConstraint
= constraint
->getCeiling();
1503 if(!ceilingConstraint
->isTrue()){
1504 if(ceilingConstraint
->negationHasProof()){
1505 Node conf
= ConstraintValue::explainConflict(constraint
, ceilingConstraint
->getNegation());
1506 d_raiseConflict(conf
);
1509 ceilingConstraint
->impliedBy(constraint
);
1510 // Do not need to add to learnedBounds
1512 return AssertLower(ceilingConstraint
);
1514 return AssertLower(constraint
);
1517 return AssertEquality(constraint
);
1519 return AssertDisequality(constraint
);
1527 * Looks for the next integer variable without an integer assignment in a round robin fashion.
1528 * Changes the value of d_nextIntegerCheckVar.
1530 * If this returns false, d_nextIntegerCheckVar does not have an integer assignment.
1531 * If this returns true, all integer variables have an integer assignment.
1533 bool TheoryArith::hasIntegerModel(){
1534 //if(d_variables.size() > 0){
1535 if(getNumberOfVariables()){
1536 const ArithVar rrEnd
= d_nextIntegerCheckVar
;
1538 //Do not include slack variables
1539 if(isInteger(d_nextIntegerCheckVar
) && !isSlackVariable(d_nextIntegerCheckVar
)) { // integer
1540 const DeltaRational
& d
= d_partialModel
.getAssignment(d_nextIntegerCheckVar
);
1541 if(!d
.isIntegral()){
1545 } while((d_nextIntegerCheckVar
= (1 + d_nextIntegerCheckVar
== getNumberOfVariables() ? 0 : 1 + d_nextIntegerCheckVar
)) != rrEnd
);
1550 /** Outputs conflicts to the output channel. */
1551 void TheoryArith::outputConflicts(){
1552 Assert(!d_conflicts
.empty());
1553 for(size_t i
= 0, i_end
= d_conflicts
.size(); i
< i_end
; ++i
){
1554 Node conflict
= d_conflicts
[i
];
1555 Debug("arith::conflict") << "d_conflicts[" << i
<< "] " << conflict
<< endl
;
1556 d_out
->conflict(conflict
);
1560 void TheoryArith::check(Effort effortLevel
){
1561 Assert(d_currentPropagationList
.empty());
1562 Debug("effortlevel") << "TheoryArith::check " << effortLevel
<< std::endl
;
1563 Debug("arith") << "TheoryArith::check begun " << effortLevel
<< std::endl
;
1565 if(Debug
.isOn("arith::consistency")){
1566 Assert(unenqueuedVariablesAreConsistent());
1569 bool newFacts
= !done();
1570 //If previous == SAT, then reverts on conflicts are safe
1571 //Otherwise, they are not and must be committed.
1572 Result::Sat previous
= d_qflraStatus
;
1574 d_qflraStatus
= Result::SAT_UNKNOWN
;
1575 d_hasDoneWorkSinceCut
= true;
1579 Constraint curr
= constraintFromFactQueue();
1580 if(curr
!= NullConstraint
){
1581 bool res CVC4_UNUSED
= assertionCases(curr
);
1582 Assert(!res
|| inConflict());
1584 if(inConflict()){ break; }
1587 while(!d_learnedBounds
.empty()){
1588 // we may attempt some constraints twice. this is okay!
1589 Constraint curr
= d_learnedBounds
.front();
1590 d_learnedBounds
.pop();
1591 Debug("arith::learned") << curr
<< endl
;
1593 bool res CVC4_UNUSED
= assertionCases(curr
);
1594 Assert(!res
|| inConflict());
1596 if(inConflict()){ break; }
1601 d_qflraStatus
= Result::UNSAT
;
1602 if(previous
== Result::SAT
){
1603 ++d_statistics
.d_revertsOnConflicts
;
1604 Debug("arith::bt") << "clearing here " << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1605 revertOutOfConflict();
1606 d_simplex
.clearQueue();
1608 ++d_statistics
.d_commitsOnConflicts
;
1609 Debug("arith::bt") << "committing here " << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1610 d_partialModel
.commitAssignmentChanges();
1611 revertOutOfConflict();
1618 if(Debug
.isOn("arith::print_assertions")) {
1619 debugPrintAssertions();
1622 bool emmittedConflictOrSplit
= false;
1623 Assert(d_conflicts
.empty());
1625 d_qflraStatus
= d_simplex
.findModel(fullEffort(effortLevel
));
1627 switch(d_qflraStatus
){
1630 ++d_statistics
.d_nontrivialSatChecks
;
1633 Debug("arith::bt") << "committing sap inConflit" << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1634 d_partialModel
.commitAssignmentChanges();
1635 d_unknownsInARow
= 0;
1636 if(Debug
.isOn("arith::consistency")){
1637 Assert(entireStateIsConsistent("sat comit"));
1640 case Result::SAT_UNKNOWN
:
1642 ++(d_statistics
.d_unknownChecks
);
1643 Assert(!fullEffort(effortLevel
));
1644 Debug("arith::bt") << "committing unknown" << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1645 d_partialModel
.commitAssignmentChanges();
1646 d_statistics
.d_maxUnknownsInARow
.maxAssign(d_unknownsInARow
);
1649 d_unknownsInARow
= 0;
1650 if(previous
== Result::SAT
){
1651 ++d_statistics
.d_revertsOnConflicts
;
1652 Debug("arith::bt") << "clearing on conflict" << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1653 revertOutOfConflict();
1654 d_simplex
.clearQueue();
1656 ++d_statistics
.d_commitsOnConflicts
;
1658 Debug("arith::bt") << "committing on conflict" << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1659 d_partialModel
.commitAssignmentChanges();
1660 revertOutOfConflict();
1662 if(Debug
.isOn("arith::consistency::comitonconflict")){
1663 entireStateIsConsistent("commit on conflict");
1667 emmittedConflictOrSplit
= true;
1672 d_statistics
.d_avgUnknownsInARow
.addEntry(d_unknownsInARow
);
1674 // This should be fine if sat or unknown
1675 if(!emmittedConflictOrSplit
&&
1676 (options::arithPropagationMode() == UNATE_PROP
||
1677 options::arithPropagationMode() == BOTH_PROP
)){
1678 TimerStat::CodeTimer
codeTimer(d_statistics
.d_newPropTime
);
1679 Assert(d_qflraStatus
!= Result::UNSAT
);
1681 while(!d_currentPropagationList
.empty() && !inConflict()){
1682 Constraint curr
= d_currentPropagationList
.front();
1683 d_currentPropagationList
.pop_front();
1685 ConstraintType t
= curr
->getType();
1686 Assert(t
!= Disequality
, "Disequalities are not allowed in d_currentPropagation");
1692 Constraint prev
= d_currentPropagationList
.front();
1693 d_currentPropagationList
.pop_front();
1694 d_constraintDatabase
.unatePropLowerBound(curr
, prev
);
1699 Constraint prev
= d_currentPropagationList
.front();
1700 d_currentPropagationList
.pop_front();
1701 d_constraintDatabase
.unatePropUpperBound(curr
, prev
);
1706 Constraint prevLB
= d_currentPropagationList
.front();
1707 d_currentPropagationList
.pop_front();
1708 Constraint prevUB
= d_currentPropagationList
.front();
1709 d_currentPropagationList
.pop_front();
1710 d_constraintDatabase
.unatePropEquality(curr
, prevLB
, prevUB
);
1714 Unhandled(curr
->getType());
1719 Debug("arith::unate") << "unate conflict" << endl
;
1720 revertOutOfConflict();
1721 d_qflraStatus
= Result::UNSAT
;
1723 emmittedConflictOrSplit
= true;
1724 Debug("arith::bt") << "committing on unate conflict" << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1728 TimerStat::CodeTimer
codeTimer(d_statistics
.d_newPropTime
);
1729 d_currentPropagationList
.clear();
1731 Assert( d_currentPropagationList
.empty());
1734 if(!emmittedConflictOrSplit
&& fullEffort(effortLevel
)){
1735 emmittedConflictOrSplit
= splitDisequalities();
1738 if(!emmittedConflictOrSplit
&& fullEffort(effortLevel
) && !hasIntegerModel()){
1739 Node possibleConflict
= Node::null();
1740 if(!emmittedConflictOrSplit
&& options::arithDioSolver()){
1741 possibleConflict
= callDioSolver();
1742 if(possibleConflict
!= Node::null()){
1743 revertOutOfConflict();
1744 Debug("arith::conflict") << "dio conflict " << possibleConflict
<< endl
;
1745 d_out
->conflict(possibleConflict
);
1746 emmittedConflictOrSplit
= true;
1750 if(!emmittedConflictOrSplit
&& d_hasDoneWorkSinceCut
&& options::arithDioSolver()){
1751 Node possibleLemma
= dioCutting();
1752 if(!possibleLemma
.isNull()){
1753 Debug("arith") << "dio cut " << possibleLemma
<< endl
;
1754 emmittedConflictOrSplit
= true;
1755 d_hasDoneWorkSinceCut
= false;
1756 d_out
->lemma(possibleLemma
);
1760 if(!emmittedConflictOrSplit
) {
1761 Node possibleLemma
= roundRobinBranch();
1762 if(!possibleLemma
.isNull()){
1763 ++(d_statistics
.d_externalBranchAndBounds
);
1764 emmittedConflictOrSplit
= true;
1765 d_out
->lemma(possibleLemma
);
1768 }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
1769 if(fullEffort(effortLevel
) && d_nlIncomplete
){
1770 // TODO this is total paranoia
1771 d_out
->setIncomplete();
1774 if(Debug
.isOn("paranoid:check_tableau")){ d_linEq
.debugCheckTableau(); }
1775 if(Debug
.isOn("arith::print_model")) { debugPrintModel(); }
1776 Debug("arith") << "TheoryArith::check end" << std::endl
;
1779 /** Returns true if the roundRobinBranching() issues a lemma. */
1780 Node
TheoryArith::roundRobinBranch(){
1781 if(hasIntegerModel()){
1782 return Node::null();
1784 ArithVar v
= d_nextIntegerCheckVar
;
1786 Assert(isInteger(v
));
1787 Assert(!isSlackVariable(v
));
1789 const DeltaRational
& d
= d_partialModel
.getAssignment(v
);
1790 const Rational
& r
= d
.getNoninfinitesimalPart();
1791 const Rational
& i
= d
.getInfinitesimalPart();
1792 Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap
.asNode(v
) << "]] is " << r
<< "[" << i
<< "]" << endl
;
1794 Assert(! (r
.getDenominator() == 1 && i
.getNumerator() == 0));
1795 Assert(!d
.isIntegral());
1797 TNode var
= d_arithvarNodeMap
.asNode(v
);
1798 Integer floor_d
= d
.floor();
1799 Integer ceil_d
= d
.ceiling();
1801 Node leq
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ
, var
, mkRationalNode(floor_d
)));
1802 Node geq
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ
, var
, mkRationalNode(ceil_d
)));
1805 Node lem
= NodeManager::currentNM()->mkNode(kind::OR
, leq
, geq
);
1806 Trace("integers") << "integers: branch & bound: " << lem
<< endl
;
1807 if(d_valuation
.isSatLiteral(lem
[0])) {
1808 Debug("integers") << " " << lem
[0] << " == " << d_valuation
.getSatValue(lem
[0]) << endl
;
1810 Debug("integers") << " " << lem
[0] << " is not assigned a SAT literal" << endl
;
1812 if(d_valuation
.isSatLiteral(lem
[1])) {
1813 Debug("integers") << " " << lem
[1] << " == " << d_valuation
.getSatValue(lem
[1]) << endl
;
1815 Debug("integers") << " " << lem
[1] << " is not assigned a SAT literal" << endl
;
1821 bool TheoryArith::splitDisequalities(){
1822 bool splitSomething
= false;
1824 vector
<Constraint
> save
;
1826 while(!d_diseqQueue
.empty()){
1827 Constraint front
= d_diseqQueue
.front();
1830 if(front
->isSplit()){
1831 Debug("eq") << "split already" << endl
;
1833 Debug("eq") << "not split already" << endl
;
1835 ArithVar lhsVar
= front
->getVariable();
1837 const DeltaRational
& lhsValue
= d_partialModel
.getAssignment(lhsVar
);
1838 const DeltaRational
& rhsValue
= front
->getValue();
1839 if(lhsValue
== rhsValue
){
1840 Debug("arith::lemma") << "Splitting on " << front
<< endl
;
1841 Debug("arith::lemma") << "LHS value = " << lhsValue
<< endl
;
1842 Debug("arith::lemma") << "RHS value = " << rhsValue
<< endl
;
1843 Node lemma
= front
->split();
1844 ++(d_statistics
.d_statDisequalitySplits
);
1845 Node relem
= Rewriter::rewrite(lemma
);
1847 Debug("arith::lemma") << "Now " << relem
<< endl
;
1848 d_out
->lemma(lemma
);
1849 splitSomething
= true;
1850 }else if(d_partialModel
.strictlyLessThanLowerBound(lhsVar
, rhsValue
)){
1851 Debug("eq") << "can drop as less than lb" << front
<< endl
;
1852 }else if(d_partialModel
.strictlyGreaterThanUpperBound(lhsVar
, rhsValue
)){
1853 Debug("eq") << "can drop as greater than ub" << front
<< endl
;
1855 Debug("eq") << "save" << front
<< ": " <<lhsValue
<< " != " << rhsValue
<< endl
;
1856 save
.push_back(front
);
1860 vector
<Constraint
>::const_iterator i
=save
.begin(), i_end
= save
.end();
1861 for(; i
!= i_end
; ++i
){
1862 d_diseqQueue
.push(*i
);
1864 return splitSomething
;
1868 * Should be guarded by at least Debug.isOn("arith::print_assertions").
1869 * Prints to Debug("arith::print_assertions")
1871 void TheoryArith::debugPrintAssertions() {
1872 Debug("arith::print_assertions") << "Assertions:" << endl
;
1873 for (var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
1875 if (d_partialModel
.hasLowerBound(i
)) {
1876 Constraint lConstr
= d_partialModel
.getLowerBoundConstraint(i
);
1877 Debug("arith::print_assertions") << lConstr
<< endl
;
1880 if (d_partialModel
.hasUpperBound(i
)) {
1881 Constraint uConstr
= d_partialModel
.getUpperBoundConstraint(i
);
1882 Debug("arith::print_assertions") << uConstr
<< endl
;
1885 context::CDQueue
<Constraint
>::const_iterator it
= d_diseqQueue
.begin();
1886 context::CDQueue
<Constraint
>::const_iterator it_end
= d_diseqQueue
.end();
1887 for(; it
!= it_end
; ++ it
) {
1888 Debug("arith::print_assertions") << *it
<< endl
;
1892 void TheoryArith::debugPrintModel(){
1893 Debug("arith::print_model") << "Model:" << endl
;
1894 for (var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
1896 if(d_arithvarNodeMap
.hasNode(i
)){
1897 Debug("arith::print_model") << d_arithvarNodeMap
.asNode(i
) << " : " <<
1898 d_partialModel
.getAssignment(i
);
1899 if(d_tableau
.isBasic(i
))
1900 Debug("arith::print_model") << " (basic)";
1901 Debug("arith::print_model") << endl
;
1908 Node
TheoryArith::explain(TNode n
) {
1910 Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n
<< endl
;
1912 Constraint c
= d_constraintDatabase
.lookup(n
);
1913 if(c
!= NullConstraint
){
1914 Assert(!c
->isSelfExplaining());
1915 Node exp
= c
->explainForPropagation();
1916 Debug("arith::explain") << "constraint explanation" << n
<< ":" << exp
<< endl
;
1918 }else if(d_assertionsThatDoNotMatchTheirLiterals
.find(n
) != d_assertionsThatDoNotMatchTheirLiterals
.end()){
1919 c
= d_assertionsThatDoNotMatchTheirLiterals
[n
];
1920 if(!c
->isSelfExplaining()){
1921 Node exp
= c
->explainForPropagation();
1922 Debug("arith::explain") << "assertions explanation" << n
<< ":" << exp
<< endl
;
1925 Debug("arith::explain") << "this is a strange mismatch" << n
<< endl
;
1926 Assert(d_congruenceManager
.canExplain(n
));
1927 Debug("arith::explain") << "this is a strange mismatch" << n
<< endl
;
1928 return d_congruenceManager
.explain(n
);
1931 Assert(d_congruenceManager
.canExplain(n
));
1932 Debug("arith::explain") << "dm explanation" << n
<< endl
;
1933 return d_congruenceManager
.explain(n
);
1938 void TheoryArith::propagate(Effort e
) {
1939 // This uses model values for safety. Disable for now.
1940 if(d_qflraStatus
== Result::SAT
&&
1941 (options::arithPropagationMode() == BOUND_INFERENCE_PROP
||
1942 options::arithPropagationMode() == BOTH_PROP
)
1943 && hasAnyUpdates()){
1944 propagateCandidates();
1949 while(d_constraintDatabase
.hasMorePropagations()){
1950 Constraint c
= d_constraintDatabase
.nextPropagation();
1951 Debug("arith::prop") << "next prop" << getSatContext()->getLevel() << ": " << c
<< endl
;
1953 if(c
->negationHasProof()){
1954 Debug("arith::prop") << "negation has proof " << c
->getNegation() << endl
1955 << c
->getNegation()->explainForConflict() << endl
;
1957 Assert(!c
->negationHasProof(), "A constraint has been propagated on the constraint propagation queue, but the negation has been set to true. Contact Tim now!");
1959 if(!c
->assertedToTheTheory()){
1960 Node literal
= c
->getLiteral();
1961 Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal
<< endl
;
1963 d_out
->propagate(literal
);
1965 Debug("arith::prop") << "already asserted to the theory " << c
->getLiteral() << endl
;
1969 while(d_congruenceManager
.hasMorePropagations()){
1970 TNode toProp
= d_congruenceManager
.getNextPropagation();
1972 //Currently if the flag is set this came from an equality detected by the
1973 //equality engine in the the difference manager.
1974 Node normalized
= Rewriter::rewrite(toProp
);
1976 Constraint constraint
= d_constraintDatabase
.lookup(normalized
);
1977 if(constraint
== NullConstraint
){
1978 Debug("arith::prop") << "propagating on non-constraint? " << toProp
<< endl
;
1979 d_out
->propagate(toProp
);
1980 }else if(constraint
->negationHasProof()){
1981 Node exp
= d_congruenceManager
.explain(toProp
);
1982 Node notNormalized
= normalized
.getKind() == NOT
?
1983 normalized
[0] : normalized
.notNode();
1984 Node lp
= flattenAnd(exp
.andNode(notNormalized
));
1985 Debug("arith::prop") << "propagate conflict" << lp
<< endl
;
1986 d_out
->conflict(lp
);
1989 Debug("arith::prop") << "propagating still?" << toProp
<< endl
;
1991 d_out
->propagate(toProp
);
1996 DeltaRational
TheoryArith::getDeltaValue(TNode n
) const throw (DeltaRationalException
, ModelException
) {
1997 AlwaysAssert(d_qflraStatus
!= Result::SAT_UNKNOWN
);
1998 Debug("arith::value") << n
<< std::endl
;
2000 switch(n
.getKind()) {
2002 case kind::CONST_RATIONAL
:
2003 return n
.getConst
<Rational
>();
2005 case kind::PLUS
: { // 2+ args
2006 DeltaRational
value(0);
2007 for(TNode::iterator i
= n
.begin(), iend
= n
.end(); i
!= iend
; ++i
) {
2008 value
= value
+ getDeltaValue(*i
);
2013 case kind::MULT
: { // 2+ args
2014 DeltaRational
value(1);
2015 unsigned variableParts
= 0;
2016 for(TNode::iterator i
= n
.begin(), iend
= n
.end(); i
!= iend
; ++i
) {
2018 value
= value
* getDeltaValue(curr
);
2019 if(!curr
.isConst()){
2023 // TODO: This is a bit of a weak check
2025 ArithVar var
= d_arithvarNodeMap
.asArithVar(n
);
2026 const DeltaRational
& assign
= d_partialModel
.getAssignment(var
);
2027 if(assign
!= value
){
2028 throw ModelException(n
, "Model disagrees on non-linear term.");
2033 case kind::MINUS
:{ // 2 args
2034 return getDeltaValue(n
[0]) - getDeltaValue(n
[1]);
2037 case kind::UMINUS
:{ // 1 arg
2038 return (- getDeltaValue(n
[0]));
2041 case kind::DIVISION
:{ // 2 args
2042 DeltaRational res
= getDeltaValue(n
[0]) / getDeltaValue(n
[1]);
2044 ArithVar var
= d_arithvarNodeMap
.asArithVar(n
);
2045 if(d_partialModel
.getAssignment(var
) != res
){
2046 throw ModelException(n
, "Model disagrees on non-linear term.");
2051 case kind::DIVISION_TOTAL
:
2052 case kind::INTS_DIVISION_TOTAL
:
2053 case kind::INTS_MODULUS_TOTAL
: { // 2 args
2054 DeltaRational denom
= getDeltaValue(n
[1]);
2056 return DeltaRational(0,0);
2058 DeltaRational numer
= getDeltaValue(n
[0]);
2060 if(n
.getKind() == kind::DIVISION_TOTAL
){
2061 res
= numer
/ denom
;
2062 }else if(n
.getKind() == kind::INTS_DIVISION_TOTAL
){
2063 res
= Rational(numer
.euclidianDivideQuotient(denom
));
2065 Assert(n
.getKind() == kind::INTS_MODULUS_TOTAL
);
2066 res
= Rational(numer
.euclidianDivideRemainder(denom
));
2069 ArithVar var
= d_arithvarNodeMap
.asArithVar(n
);
2070 if(d_partialModel
.getAssignment(var
) != res
){
2071 throw ModelException(n
, "Model disagrees on non-linear term.");
2080 ArithVar var
= d_arithvarNodeMap
.asArithVar(n
);
2081 return d_partialModel
.getAssignment(var
);
2083 throw ModelException(n
, "Expected a setup node.");
2088 Rational
TheoryArith::deltaValueForTotalOrder() const{
2090 std::set
<DeltaRational
> relevantDeltaValues
;
2091 context::CDQueue
<Constraint
>::const_iterator qiter
= d_diseqQueue
.begin();
2092 context::CDQueue
<Constraint
>::const_iterator qiter_end
= d_diseqQueue
.end();
2094 for(; qiter
!= qiter_end
; ++qiter
){
2095 Constraint curr
= *qiter
;
2097 const DeltaRational
& rhsValue
= curr
->getValue();
2098 relevantDeltaValues
.insert(rhsValue
);
2101 for(shared_terms_iterator shared_iter
= shared_terms_begin(),
2102 shared_end
= shared_terms_end(); shared_iter
!= shared_end
; ++shared_iter
){
2103 Node sharedCurr
= *shared_iter
;
2105 // ModelException is fatal as this point. Don't catch!
2106 // DeltaRationalException is fatal as this point. Don't catch!
2107 DeltaRational val
= getDeltaValue(sharedCurr
);
2108 relevantDeltaValues
.insert(val
);
2111 for(var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
2113 const DeltaRational
& value
= d_partialModel
.getAssignment(v
);
2114 relevantDeltaValues
.insert(value
);
2115 if( d_partialModel
.hasLowerBound(v
)){
2116 const DeltaRational
& lb
= d_partialModel
.getLowerBound(v
);
2117 relevantDeltaValues
.insert(lb
);
2119 if( d_partialModel
.hasUpperBound(v
)){
2120 const DeltaRational
& ub
= d_partialModel
.getUpperBound(v
);
2121 relevantDeltaValues
.insert(ub
);
2125 if(relevantDeltaValues
.size() >= 2){
2126 std::set
<DeltaRational
>::const_iterator iter
= relevantDeltaValues
.begin();
2127 std::set
<DeltaRational
>::const_iterator iter_end
= relevantDeltaValues
.end();
2128 DeltaRational prev
= *iter
;
2130 for(; iter
!= iter_end
; ++iter
){
2131 const DeltaRational
& curr
= *iter
;
2133 Assert(prev
< curr
);
2135 DeltaRational::seperatingDelta(min
, prev
, curr
);
2140 Assert(min
.sgn() > 0);
2141 Rational belowMin
= min
/Rational(2);
2145 void TheoryArith::collectModelInfo( TheoryModel
* m
, bool fullModel
){
2146 AlwaysAssert(d_qflraStatus
== Result::SAT
);
2147 //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
2149 if(Debug
.isOn("arith::collectModelInfo")){
2153 Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl
;
2156 // Delta lasts at least the duration of the function call
2157 const Rational
& delta
= d_partialModel
.getDelta();
2158 std::hash_set
<TNode
, TNodeHashFunction
> shared
= currentlySharedTerms();
2161 // This is not very good for user push/pop....
2162 // Revisit when implementing push/pop
2163 for(var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
2165 if(!isSlackVariable(v
)){
2166 Node term
= d_arithvarNodeMap
.asNode(v
);
2168 if(theoryOf(term
) == THEORY_ARITH
|| shared
.find(term
) != shared
.end()){
2169 const DeltaRational
& mod
= d_partialModel
.getAssignment(v
);
2170 Rational qmodel
= mod
.substituteDelta(delta
);
2172 Node qNode
= mkRationalNode(qmodel
);
2173 Debug("arith::collectModelInfo") << "m->assertEquality(" << term
<< ", " << qmodel
<< ", true)" << endl
;
2175 m
->assertEquality(term
, qNode
, true);
2177 Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term
<< ", true)" << endl
;
2183 // Iterate over equivalence classes in LinearEqualityModule
2184 // const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine();
2185 // m->assertEqualityEngine(&ee);
2187 Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl
;
2190 bool TheoryArith::safeToReset() const {
2191 Assert(!d_tableauSizeHasBeenModified
);
2193 ArithPriorityQueue::const_iterator conf_iter
= d_simplex
.queueBegin();
2194 ArithPriorityQueue::const_iterator conf_end
= d_simplex
.queueEnd();
2195 for(; conf_iter
!= conf_end
; ++conf_iter
){
2196 ArithVar basic
= *conf_iter
;
2197 if(!d_smallTableauCopy
.isBasic(basic
)){
2205 void TheoryArith::notifyRestart(){
2206 TimerStat::CodeTimer
codeTimer(d_statistics
.d_restartTimer
);
2208 if(Debug
.isOn("paranoid:check_tableau")){ d_linEq
.debugCheckTableau(); }
2210 ++d_restartsCounter
;
2212 uint32_t currSize
= d_tableau
.size();
2213 uint32_t copySize
= d_smallTableauCopy
.size();
2215 Debug("arith::reset") << "resetting" << d_restartsCounter
<< endl
;
2216 Debug("arith::reset") << "curr " << currSize
<< " copy " << copySize
<< endl
;
2217 Debug("arith::reset") << "tableauSizeHasBeenModified " << d_tableauSizeHasBeenModified
<< endl
;
2219 if(d_tableauSizeHasBeenModified
){
2220 Debug("arith::reset") << "row has been added must copy " << d_restartsCounter
<< endl
;
2221 d_smallTableauCopy
= d_tableau
;
2222 d_tableauSizeHasBeenModified
= false;
2223 }else if( d_restartsCounter
>= RESET_START
){
2224 if(copySize
>= currSize
* 1.1 ){
2225 Debug("arith::reset") << "size has shrunk " << d_restartsCounter
<< endl
;
2226 ++d_statistics
.d_smallerSetToCurr
;
2227 d_smallTableauCopy
= d_tableau
;
2228 }else if(d_tableauResetDensity
* copySize
<= currSize
){
2229 d_simplex
.reduceQueue();
2231 Debug("arith::reset") << "resetting " << d_restartsCounter
<< endl
;
2232 ++d_statistics
.d_currSetToSmaller
;
2233 d_tableau
= d_smallTableauCopy
;
2235 Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter
<< endl
;
2239 Assert(unenqueuedVariablesAreConsistent());
2242 bool TheoryArith::entireStateIsConsistent(const string
& s
){
2244 for(var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
2246 //ArithVar var = d_arithvarNodeMap.asArithVar(*i);
2247 if(!d_partialModel
.assignmentIsConsistent(var
)){
2248 d_partialModel
.printModel(var
);
2249 Warning() << s
<< ":" << "Assignment is not consistent for " << var
<< d_arithvarNodeMap
.asNode(var
);
2250 if(d_tableau
.isBasic(var
)){
2251 Warning() << " (basic)";
2260 bool TheoryArith::unenqueuedVariablesAreConsistent(){
2262 for(var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
2264 if(!d_partialModel
.assignmentIsConsistent(var
)){
2265 if(!d_simplex
.debugIsInCollectionQueue(var
)){
2267 d_partialModel
.printModel(var
);
2268 Warning() << "Unenqueued var is not consistent for " << var
<< d_arithvarNodeMap
.asNode(var
);
2269 if(d_tableau
.isBasic(var
)){
2270 Warning() << " (basic)";
2274 } else if(Debug
.isOn("arith::consistency::initial")){
2275 d_partialModel
.printModel(var
);
2276 Warning() << "Initial var is not consistent for " << var
<< d_arithvarNodeMap
.asNode(var
);
2277 if(d_tableau
.isBasic(var
)){
2278 Warning() << " (basic)";
2287 void TheoryArith::presolve(){
2288 TimerStat::CodeTimer
codeTimer(d_statistics
.d_presolveTime
);
2290 d_statistics
.d_initialTableauSize
.setData(d_tableau
.size());
2292 if(Debug
.isOn("paranoid:check_tableau")){ d_linEq
.debugCheckTableau(); }
2294 static CVC4_THREADLOCAL(unsigned) callCount
= 0;
2295 if(Debug
.isOn("arith::presolve")) {
2296 Debug("arith::presolve") << "TheoryArith::presolve #" << callCount
<< endl
;
2297 callCount
= callCount
+ 1;
2300 vector
<Node
> lemmas
;
2301 switch(options::arithUnateLemmaMode()){
2302 case NO_PRESOLVE_LEMMAS
:
2304 case INEQUALITY_PRESOLVE_LEMMAS
:
2305 d_constraintDatabase
.outputUnateInequalityLemmas(lemmas
);
2307 case EQUALITY_PRESOLVE_LEMMAS
:
2308 d_constraintDatabase
.outputUnateEqualityLemmas(lemmas
);
2310 case ALL_PRESOLVE_LEMMAS
:
2311 d_constraintDatabase
.outputUnateInequalityLemmas(lemmas
);
2312 d_constraintDatabase
.outputUnateEqualityLemmas(lemmas
);
2315 Unhandled(options::arithUnateLemmaMode());
2318 vector
<Node
>::const_iterator i
= lemmas
.begin(), i_end
= lemmas
.end();
2319 for(; i
!= i_end
; ++i
){
2321 Debug("arith::oldprop") << " lemma lemma duck " <<lem
<< endl
;
2325 // if(options::arithUnateLemmaMode() == Options::ALL_UNATE){
2326 // vector<Node> lemmas;
2327 // d_constraintDatabase.outputAllUnateLemmas(lemmas);
2328 // vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
2329 // for(; i != i_end; ++i){
2331 // Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
2332 // d_out->lemma(lem);
2337 EqualityStatus
TheoryArith::getEqualityStatus(TNode a
, TNode b
) {
2338 if(d_qflraStatus
== Result::SAT_UNKNOWN
){
2339 return EQUALITY_UNKNOWN
;
2342 if (getDeltaValue(a
) == getDeltaValue(b
)) {
2343 return EQUALITY_TRUE_IN_MODEL
;
2345 return EQUALITY_FALSE_IN_MODEL
;
2347 } catch (DeltaRationalException
& dr
) {
2348 return EQUALITY_UNKNOWN
;
2349 } catch (ModelException
& me
) {
2350 return EQUALITY_UNKNOWN
;
2355 bool TheoryArith::propagateCandidateBound(ArithVar basic
, bool upperBound
){
2356 ++d_statistics
.d_boundComputations
;
2358 DeltaRational bound
= upperBound
?
2359 d_linEq
.computeUpperBound(basic
):
2360 d_linEq
.computeLowerBound(basic
);
2362 if((upperBound
&& d_partialModel
.strictlyLessThanUpperBound(basic
, bound
)) ||
2363 (!upperBound
&& d_partialModel
.strictlyGreaterThanLowerBound(basic
, bound
))){
2365 // TODO: "Policy point"
2366 //We are only going to recreate the functionality for now.
2367 //In the future this can be improved to generate a temporary constraint
2369 //Experiment with doing this everytime or only when the new constraint
2370 //implies an unknown fact.
2372 ConstraintType t
= upperBound
? UpperBound
: LowerBound
;
2373 Constraint bestImplied
= d_constraintDatabase
.getBestImpliedBound(basic
, t
, bound
);
2375 // Node bestImplied = upperBound ?
2376 // d_apm.getBestImpliedUpperBound(basic, bound):
2377 // d_apm.getBestImpliedLowerBound(basic, bound);
2379 if(bestImplied
!= NullConstraint
){
2380 //This should be stronger
2381 Assert(!upperBound
|| bound
<= bestImplied
->getValue());
2382 Assert(!upperBound
|| d_partialModel
.lessThanUpperBound(basic
, bestImplied
->getValue()));
2384 Assert( upperBound
|| bound
>= bestImplied
->getValue());
2385 Assert( upperBound
|| d_partialModel
.greaterThanLowerBound(basic
, bestImplied
->getValue()));
2388 // Constraint c = d_constraintDatabase.lookup(bestImplied);
2389 // Assert(c != NullConstraint);
2391 bool assertedToTheTheory
= bestImplied
->assertedToTheTheory();
2392 bool canBePropagated
= bestImplied
->canBePropagated();
2393 bool hasProof
= bestImplied
->hasProof();
2395 Debug("arith::prop") << "arith::prop" << basic
2396 << " " << assertedToTheTheory
2397 << " " << canBePropagated
2401 if(bestImplied
->negationHasProof()){
2402 Warning() << "the negation of " << bestImplied
<< " : " << endl
2403 << "has proof " << bestImplied
->getNegation() << endl
2404 << bestImplied
->getNegation()->explainForConflict() << endl
;
2407 if(!assertedToTheTheory
&& canBePropagated
&& !hasProof
){
2409 Assert(bestImplied
!= d_partialModel
.getUpperBoundConstraint(basic
));
2410 d_linEq
.propagateNonbasicsUpperBound(basic
, bestImplied
);
2412 Assert(bestImplied
!= d_partialModel
.getLowerBoundConstraint(basic
));
2413 d_linEq
.propagateNonbasicsLowerBound(basic
, bestImplied
);
2415 // I think this can be skipped if canBePropagated is true
2416 //d_learnedBounds.push(bestImplied);
2424 void TheoryArith::propagateCandidate(ArithVar basic
){
2425 bool success
= false;
2426 if(d_partialModel
.strictlyAboveLowerBound(basic
) && d_linEq
.hasLowerBounds(basic
)){
2427 success
|= propagateCandidateLowerBound(basic
);
2429 if(d_partialModel
.strictlyBelowUpperBound(basic
) && d_linEq
.hasUpperBounds(basic
)){
2430 success
|= propagateCandidateUpperBound(basic
);
2433 ++d_statistics
.d_boundPropagations
;
2437 void TheoryArith::propagateCandidates(){
2438 TimerStat::CodeTimer
codeTimer(d_statistics
.d_boundComputationTime
);
2440 Assert(d_candidateBasics
.empty());
2442 if(d_updatedBounds
.empty()){ return; }
2444 DenseSet::const_iterator i
= d_updatedBounds
.begin();
2445 DenseSet::const_iterator end
= d_updatedBounds
.end();
2446 for(; i
!= end
; ++i
){
2448 if(d_tableau
.isBasic(var
) &&
2449 d_tableau
.getRowLength(d_tableau
.basicToRowIndex(var
)) <= options::arithPropagateMaxLength()){
2450 d_candidateBasics
.softAdd(var
);
2452 Tableau::ColIterator basicIter
= d_tableau
.colIterator(var
);
2453 for(; !basicIter
.atEnd(); ++basicIter
){
2454 const Tableau::Entry
& entry
= *basicIter
;
2455 RowIndex ridx
= entry
.getRowIndex();
2456 ArithVar rowVar
= d_tableau
.rowIndexToBasic(ridx
);
2457 Assert(entry
.getColVar() == var
);
2458 Assert(d_tableau
.isBasic(rowVar
));
2459 if(d_tableau
.getRowLength(ridx
) <= options::arithPropagateMaxLength()){
2460 d_candidateBasics
.softAdd(rowVar
);
2465 d_updatedBounds
.purge();
2467 while(!d_candidateBasics
.empty()){
2468 ArithVar candidate
= d_candidateBasics
.back();
2469 d_candidateBasics
.pop_back();
2470 Assert(d_tableau
.isBasic(candidate
));
2471 propagateCandidate(candidate
);
2475 }/* CVC4::theory::arith namespace */
2476 }/* CVC4::theory namespace */
2477 }/* CVC4 namespace */