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 "theory/arith/theory_arith_private.h"
20 #include "expr/node.h"
21 #include "expr/kind.h"
22 #include "expr/metakind.h"
23 #include "expr/node_builder.h"
25 #include "context/context.h"
26 #include "context/cdlist.h"
27 #include "context/cdhashset.h"
28 #include "context/cdinsert_hashmap.h"
29 #include "context/cdqueue.h"
31 #include "theory/valuation.h"
32 #include "theory/rewriter.h"
34 #include "util/rational.h"
35 #include "util/integer.h"
36 #include "util/boolean_simplification.h"
37 #include "util/dense_map.h"
38 #include "util/statistics_registry.h"
39 #include "util/result.h"
41 #include "smt/logic_exception.h"
43 #include "theory/arith/arithvar.h"
44 #include "theory/arith/delta_rational.h"
45 #include "theory/arith/matrix.h"
46 #include "theory/arith/arith_rewriter.h"
47 #include "theory/arith/partial_model.h"
48 #include "theory/arith/linear_equality.h"
49 #include "theory/arith/simplex.h"
50 #include "theory/arith/arith_static_learner.h"
51 #include "theory/arith/dio_solver.h"
52 #include "theory/arith/congruence_manager.h"
54 #include "theory/arith/approx_simplex.h"
55 #include "theory/arith/constraint.h"
57 #include "theory/arith/arith_utilities.h"
58 #include "theory/arith/delta_rational.h"
59 #include "theory/arith/partial_model.h"
60 #include "theory/arith/matrix.h"
62 #include "theory/arith/arith_rewriter.h"
63 #include "theory/arith/constraint.h"
64 #include "theory/arith/theory_arith.h"
65 #include "theory/arith/normal_form.h"
66 #include "theory/model.h"
68 #include "theory/arith/options.h"
70 #include "theory/quantifiers/bounded_integers.h"
79 using namespace CVC4::kind
;
85 TheoryArithPrivate::TheoryArithPrivate(TheoryArith
& containing
, context::Context
* c
, context::UserContext
* u
, OutputChannel
& out
, Valuation valuation
, const LogicInfo
& logicInfo
, QuantifiersEngine
* qe
) :
86 d_containing(containing
),
87 d_nlIncomplete( false),
89 d_constraintDatabase(c
, u
, d_partialModel
, d_congruenceManager
, RaiseConflict(*this)),
90 d_qflraStatus(Result::SAT_UNKNOWN
),
92 d_hasDoneWorkSinceCut(false),
95 d_assertionsThatDoNotMatchTheirLiterals(c
),
96 d_nextIntegerCheckVar(0),
97 d_constantIntegerVariables(c
),
98 d_diseqQueue(c
, false),
99 d_currentPropagationList(),
101 d_partialModel(c
, DeltaComputeCallback(*this)),
102 d_errorSet(d_partialModel
, TableauSizes(&d_tableau
), BoundCountingLookup(*this)),
104 d_linEq(d_partialModel
, d_tableau
, d_rowTracking
, BasicVarModelUpdateCallBack(*this)),
106 d_restartsCounter(0),
107 d_tableauSizeHasBeenModified(false),
108 d_tableauResetDensity(1.6),
109 d_tableauResetPeriod(10),
111 d_congruenceManager(c
, d_constraintDatabase
, SetupLiteralCallBack(*this), d_partialModel
, RaiseConflict(*this)),
112 d_dualSimplex(d_linEq
, d_errorSet
, RaiseConflict(*this), TempVarMalloc(*this)),
113 d_fcSimplex(d_linEq
, d_errorSet
, RaiseConflict(*this), TempVarMalloc(*this)),
114 d_soiSimplex(d_linEq
, d_errorSet
, RaiseConflict(*this), TempVarMalloc(*this)),
115 d_attemptSolSimplex(d_linEq
, d_errorSet
, RaiseConflict(*this), TempVarMalloc(*this)),
117 d_fullCheckCounter(0),
120 d_likelyIntegerInfeasible(c
, false),
121 d_guessedCoeffSet(c
, false),
128 TheoryArithPrivate::~TheoryArithPrivate(){ }
131 void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
132 d_congruenceManager
.setMasterEqualityEngine(eq
);
135 Node
TheoryArithPrivate::getRealDivideBy0Func(){
136 Assert(!getLogicInfo().isLinear());
137 Assert(getLogicInfo().areRealsUsed());
139 if(d_realDivideBy0Func
.isNull()){
140 TypeNode realType
= NodeManager::currentNM()->realType();
141 d_realDivideBy0Func
= skolemFunction("/by0_$$", realType
, realType
);
143 return d_realDivideBy0Func
;
146 Node
TheoryArithPrivate::getIntDivideBy0Func(){
147 Assert(!getLogicInfo().isLinear());
148 Assert(getLogicInfo().areIntegersUsed());
150 if(d_intDivideBy0Func
.isNull()){
151 TypeNode intType
= NodeManager::currentNM()->integerType();
152 d_intDivideBy0Func
= skolemFunction("divby0_$$", intType
, intType
);
154 return d_intDivideBy0Func
;
157 Node
TheoryArithPrivate::getIntModulusBy0Func(){
158 Assert(!getLogicInfo().isLinear());
159 Assert(getLogicInfo().areIntegersUsed());
161 if(d_intModulusBy0Func
.isNull()){
162 TypeNode intType
= NodeManager::currentNM()->integerType();
163 d_intModulusBy0Func
= skolemFunction("modby0_$$", intType
, intType
);
165 return d_intModulusBy0Func
;
168 TheoryArithPrivate::ModelException::ModelException(TNode n
, const char* msg
) throw (){
170 ss
<< "Cannot construct a model for " << n
<< " as " << endl
<< msg
;
171 setMessage(ss
.str());
173 TheoryArithPrivate::ModelException::~ModelException() throw (){ }
176 TheoryArithPrivate::Statistics::Statistics():
177 d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
178 d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
179 d_statUserVariables("theory::arith::UserVariables", 0),
180 d_statSlackVariables("theory::arith::SlackVariables", 0),
181 d_statDisequalitySplits("theory::arith::DisequalitySplits", 0),
182 d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0),
183 d_simplifyTimer("theory::arith::simplifyTimer"),
184 d_staticLearningTimer("theory::arith::staticLearningTimer"),
185 d_presolveTime("theory::arith::presolveTime"),
186 d_newPropTime("theory::arith::newPropTimer"),
187 d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0),
188 d_initialTableauSize("theory::arith::initialTableauSize", 0),
189 d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
190 d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
191 d_restartTimer("theory::arith::restartTimer"),
192 d_boundComputationTime("theory::arith::bound::time"),
193 d_boundComputations("theory::arith::bound::boundComputations",0),
194 d_boundPropagations("theory::arith::bound::boundPropagations",0),
195 d_unknownChecks("theory::arith::status::unknowns", 0),
196 d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0),
197 d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow"),
198 d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0),
199 d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0),
200 d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0),
201 d_satPivots("pivots::sat"),
202 d_unsatPivots("pivots::unsat"),
203 d_unknownPivots("pivots::unkown")
205 StatisticsRegistry::registerStat(&d_statAssertUpperConflicts
);
206 StatisticsRegistry::registerStat(&d_statAssertLowerConflicts
);
208 StatisticsRegistry::registerStat(&d_statUserVariables
);
209 StatisticsRegistry::registerStat(&d_statSlackVariables
);
210 StatisticsRegistry::registerStat(&d_statDisequalitySplits
);
211 StatisticsRegistry::registerStat(&d_statDisequalityConflicts
);
212 StatisticsRegistry::registerStat(&d_simplifyTimer
);
213 StatisticsRegistry::registerStat(&d_staticLearningTimer
);
215 StatisticsRegistry::registerStat(&d_presolveTime
);
216 StatisticsRegistry::registerStat(&d_newPropTime
);
218 StatisticsRegistry::registerStat(&d_externalBranchAndBounds
);
220 StatisticsRegistry::registerStat(&d_initialTableauSize
);
221 StatisticsRegistry::registerStat(&d_currSetToSmaller
);
222 StatisticsRegistry::registerStat(&d_smallerSetToCurr
);
223 StatisticsRegistry::registerStat(&d_restartTimer
);
225 StatisticsRegistry::registerStat(&d_boundComputationTime
);
226 StatisticsRegistry::registerStat(&d_boundComputations
);
227 StatisticsRegistry::registerStat(&d_boundPropagations
);
229 StatisticsRegistry::registerStat(&d_unknownChecks
);
230 StatisticsRegistry::registerStat(&d_maxUnknownsInARow
);
231 StatisticsRegistry::registerStat(&d_avgUnknownsInARow
);
232 StatisticsRegistry::registerStat(&d_revertsOnConflicts
);
233 StatisticsRegistry::registerStat(&d_commitsOnConflicts
);
234 StatisticsRegistry::registerStat(&d_nontrivialSatChecks
);
237 StatisticsRegistry::registerStat(&d_satPivots
);
238 StatisticsRegistry::registerStat(&d_unsatPivots
);
239 StatisticsRegistry::registerStat(&d_unknownPivots
);
242 TheoryArithPrivate::Statistics::~Statistics(){
243 StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts
);
244 StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts
);
246 StatisticsRegistry::unregisterStat(&d_statUserVariables
);
247 StatisticsRegistry::unregisterStat(&d_statSlackVariables
);
248 StatisticsRegistry::unregisterStat(&d_statDisequalitySplits
);
249 StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts
);
250 StatisticsRegistry::unregisterStat(&d_simplifyTimer
);
251 StatisticsRegistry::unregisterStat(&d_staticLearningTimer
);
253 StatisticsRegistry::unregisterStat(&d_presolveTime
);
254 StatisticsRegistry::unregisterStat(&d_newPropTime
);
256 StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds
);
258 StatisticsRegistry::unregisterStat(&d_initialTableauSize
);
259 StatisticsRegistry::unregisterStat(&d_currSetToSmaller
);
260 StatisticsRegistry::unregisterStat(&d_smallerSetToCurr
);
261 StatisticsRegistry::unregisterStat(&d_restartTimer
);
263 StatisticsRegistry::unregisterStat(&d_boundComputationTime
);
264 StatisticsRegistry::unregisterStat(&d_boundComputations
);
265 StatisticsRegistry::unregisterStat(&d_boundPropagations
);
267 StatisticsRegistry::unregisterStat(&d_unknownChecks
);
268 StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow
);
269 StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow
);
270 StatisticsRegistry::unregisterStat(&d_revertsOnConflicts
);
271 StatisticsRegistry::unregisterStat(&d_commitsOnConflicts
);
272 StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks
);
274 StatisticsRegistry::unregisterStat(&d_satPivots
);
275 StatisticsRegistry::unregisterStat(&d_unsatPivots
);
276 StatisticsRegistry::unregisterStat(&d_unknownPivots
);
279 void TheoryArithPrivate::revertOutOfConflict(){
280 d_partialModel
.revertAssignmentChanges();
282 d_currentPropagationList
.clear();
285 void TheoryArithPrivate::clearUpdates(){
286 d_updatedBounds
.purge();
289 void TheoryArithPrivate::zeroDifferenceDetected(ArithVar x
){
290 Assert(d_congruenceManager
.isWatchedVariable(x
));
291 Assert(d_partialModel
.upperBoundIsZero(x
));
292 Assert(d_partialModel
.lowerBoundIsZero(x
));
294 Constraint lb
= d_partialModel
.getLowerBoundConstraint(x
);
295 Constraint ub
= d_partialModel
.getUpperBoundConstraint(x
);
297 if(lb
->isEquality()){
298 d_congruenceManager
.watchedVariableIsZero(lb
);
299 }else if(ub
->isEquality()){
300 d_congruenceManager
.watchedVariableIsZero(ub
);
302 d_congruenceManager
.watchedVariableIsZero(lb
, ub
);
306 /* procedure AssertLower( x_i >= c_i ) */
307 bool TheoryArithPrivate::AssertLower(Constraint constraint
){
308 Assert(constraint
!= NullConstraint
);
309 Assert(constraint
->isLowerBound());
311 ArithVar x_i
= constraint
->getVariable();
312 const DeltaRational
& c_i
= constraint
->getValue();
314 Debug("arith") << "AssertLower(" << x_i
<< " " << c_i
<< ")"<< std::endl
;
316 Assert(!isInteger(x_i
) || c_i
.isIntegral());
318 //TODO Relax to less than?
319 if(d_partialModel
.lessThanLowerBound(x_i
, c_i
)){
323 int cmpToUB
= d_partialModel
.cmpToUpperBound(x_i
, c_i
);
324 if(cmpToUB
> 0){ // c_i < \lowerbound(x_i)
325 Constraint ubc
= d_partialModel
.getUpperBoundConstraint(x_i
);
326 Node conflict
= ConstraintValue::explainConflict(ubc
, constraint
);
327 Debug("arith") << "AssertLower conflict " << conflict
<< endl
;
328 ++(d_statistics
.d_statAssertLowerConflicts
);
329 raiseConflict(conflict
);
331 }else if(cmpToUB
== 0){
333 d_constantIntegerVariables
.push_back(x_i
);
334 Debug("dio::push") << x_i
<< endl
;
336 Constraint ub
= d_partialModel
.getUpperBoundConstraint(x_i
);
338 if(!d_congruenceManager
.isWatchedVariable(x_i
) || c_i
.sgn() != 0){
339 // if it is not a watched variable report it
340 // if it is is a watched variable and c_i == 0,
341 // let zeroDifferenceDetected(x_i) catch this
342 d_congruenceManager
.equalsConstant(constraint
, ub
);
345 const ValueCollection
& vc
= constraint
->getValueCollection();
346 if(vc
.hasDisequality()){
347 Assert(vc
.hasEquality());
348 const Constraint eq
= vc
.getEquality();
349 const Constraint diseq
= vc
.getDisequality();
351 //const Constraint ub = vc.getUpperBound();
352 Node conflict
= ConstraintValue::explainConflict(diseq
, ub
, constraint
);
354 ++(d_statistics
.d_statDisequalityConflicts
);
355 Debug("eq") << " assert lower conflict " << conflict
<< endl
;
356 raiseConflict(conflict
);
358 }else if(!eq
->isTrue()){
359 Debug("eq") << "lb == ub, propagate eq" << eq
<< endl
;
360 eq
->impliedBy(constraint
, d_partialModel
.getUpperBoundConstraint(x_i
));
361 // do not need to add to d_learnedBounds
366 const ValueCollection
& vc
= constraint
->getValueCollection();
368 if(vc
.hasDisequality()){
369 const Constraint diseq
= vc
.getDisequality();
371 const Constraint ub
= d_constraintDatabase
.ensureConstraint(const_cast<ValueCollection
&>(vc
), UpperBound
);
374 Node conflict
= ConstraintValue::explainConflict(diseq
, ub
, constraint
);
375 Debug("eq") << " assert upper conflict " << conflict
<< endl
;
376 raiseConflict(conflict
);
378 }else if(!ub
->negationHasProof()){
379 Constraint negUb
= ub
->getNegation();
380 negUb
->impliedBy(constraint
, diseq
);
381 d_learnedBounds
.push_back(negUb
);
387 d_currentPropagationList
.push_back(constraint
);
388 d_currentPropagationList
.push_back(d_partialModel
.getLowerBoundConstraint(x_i
));
390 d_partialModel
.setLowerBoundConstraint(constraint
);
392 if(d_congruenceManager
.isWatchedVariable(x_i
)){
395 d_congruenceManager
.watchedVariableCannotBeZero(constraint
);
396 }else if(sgn
== 0 && d_partialModel
.upperBoundIsZero(x_i
)){
397 zeroDifferenceDetected(x_i
);
401 d_updatedBounds
.softAdd(x_i
);
403 if(Debug
.isOn("model")) {
404 Debug("model") << "before" << endl
;
405 d_partialModel
.printModel(x_i
);
406 d_tableau
.debugPrintIsBasic(x_i
);
409 if(!d_tableau
.isBasic(x_i
)){
410 if(d_partialModel
.getAssignment(x_i
) < c_i
){
411 d_linEq
.update(x_i
, c_i
);
414 d_errorSet
.signalVariable(x_i
);
417 if(Debug
.isOn("model")) {
418 Debug("model") << "after" << endl
;
419 d_partialModel
.printModel(x_i
);
420 d_tableau
.debugPrintIsBasic(x_i
);
426 /* procedure AssertUpper( x_i <= c_i) */
427 bool TheoryArithPrivate::AssertUpper(Constraint constraint
){
428 ArithVar x_i
= constraint
->getVariable();
429 const DeltaRational
& c_i
= constraint
->getValue();
431 Debug("arith") << "AssertUpper(" << x_i
<< " " << c_i
<< ")"<< std::endl
;
432 AssertArgument(constraint
!= NullConstraint
,
433 "AssertUpper() called on a NullConstraint.");
434 Assert(constraint
->isUpperBound());
436 //Too strong because of rounding with integers
437 //Assert(!constraint->hasLiteral() || original == constraint->getLiteral());
438 Assert(!isInteger(x_i
) || c_i
.isIntegral());
440 Debug("arith") << "AssertUpper(" << x_i
<< " " << c_i
<< ")"<< std::endl
;
442 if(d_partialModel
.greaterThanUpperBound(x_i
, c_i
) ){ // \upperbound(x_i) <= c_i
446 // cmpToLb = \lowerbound(x_i).cmp(c_i)
447 int cmpToLB
= d_partialModel
.cmpToLowerBound(x_i
, c_i
);
448 if( cmpToLB
< 0 ){ // \upperbound(x_i) < \lowerbound(x_i)
449 Constraint lbc
= d_partialModel
.getLowerBoundConstraint(x_i
);
450 Node conflict
= ConstraintValue::explainConflict(lbc
, constraint
);
451 Debug("arith") << "AssertUpper conflict " << conflict
<< endl
;
452 ++(d_statistics
.d_statAssertUpperConflicts
);
453 raiseConflict(conflict
);
455 }else if(cmpToLB
== 0){ // \lowerBound(x_i) == \upperbound(x_i)
457 d_constantIntegerVariables
.push_back(x_i
);
458 Debug("dio::push") << x_i
<< endl
;
460 Constraint lb
= d_partialModel
.getLowerBoundConstraint(x_i
);
461 if(!d_congruenceManager
.isWatchedVariable(x_i
) || c_i
.sgn() != 0){
462 // if it is not a watched variable report it
463 // if it is is a watched variable and c_i == 0,
464 // let zeroDifferenceDetected(x_i) catch this
465 d_congruenceManager
.equalsConstant(lb
, constraint
);
468 const ValueCollection
& vc
= constraint
->getValueCollection();
469 if(vc
.hasDisequality()){
470 Assert(vc
.hasEquality());
471 const Constraint diseq
= vc
.getDisequality();
472 const Constraint eq
= vc
.getEquality();
474 Node conflict
= ConstraintValue::explainConflict(diseq
, lb
, constraint
);
475 Debug("eq") << " assert upper conflict " << conflict
<< endl
;
476 raiseConflict(conflict
);
478 }else if(!eq
->isTrue()){
479 Debug("eq") << "lb == ub, propagate eq" << eq
<< endl
;
480 eq
->impliedBy(constraint
, d_partialModel
.getLowerBoundConstraint(x_i
));
481 //do not bother to add to d_learnedBounds
484 }else if(cmpToLB
> 0){
485 const ValueCollection
& vc
= constraint
->getValueCollection();
486 if(vc
.hasDisequality()){
487 const Constraint diseq
= vc
.getDisequality();
489 const Constraint lb
=
490 d_constraintDatabase
.ensureConstraint(const_cast<ValueCollection
&>(vc
), LowerBound
);
492 Node conflict
= ConstraintValue::explainConflict(diseq
, lb
, constraint
);
493 Debug("eq") << " assert upper conflict " << conflict
<< endl
;
494 raiseConflict(conflict
);
496 }else if(!lb
->negationHasProof()){
497 Constraint negLb
= lb
->getNegation();
498 negLb
->impliedBy(constraint
, diseq
);
499 d_learnedBounds
.push_back(negLb
);
505 d_currentPropagationList
.push_back(constraint
);
506 d_currentPropagationList
.push_back(d_partialModel
.getUpperBoundConstraint(x_i
));
507 //It is fine if this is NullConstraint
509 d_partialModel
.setUpperBoundConstraint(constraint
);
511 if(d_congruenceManager
.isWatchedVariable(x_i
)){
514 d_congruenceManager
.watchedVariableCannotBeZero(constraint
);
515 }else if(sgn
== 0 && d_partialModel
.lowerBoundIsZero(x_i
)){
516 zeroDifferenceDetected(x_i
);
520 d_updatedBounds
.softAdd(x_i
);
522 if(Debug
.isOn("model")) {
523 Debug("model") << "before" << endl
;
524 d_partialModel
.printModel(x_i
);
525 d_tableau
.debugPrintIsBasic(x_i
);
528 if(!d_tableau
.isBasic(x_i
)){
529 if(d_partialModel
.getAssignment(x_i
) > c_i
){
530 d_linEq
.update(x_i
, c_i
);
533 d_errorSet
.signalVariable(x_i
);
536 if(Debug
.isOn("model")) {
537 Debug("model") << "after" << endl
;
538 d_partialModel
.printModel(x_i
);
539 d_tableau
.debugPrintIsBasic(x_i
);
546 /* procedure AssertEquality( x_i == c_i ) */
547 bool TheoryArithPrivate::AssertEquality(Constraint constraint
){
548 AssertArgument(constraint
!= NullConstraint
,
549 "AssertUpper() called on a NullConstraint.");
551 ArithVar x_i
= constraint
->getVariable();
552 const DeltaRational
& c_i
= constraint
->getValue();
554 Debug("arith") << "AssertEquality(" << x_i
<< " " << c_i
<< ")"<< std::endl
;
556 //Should be fine in integers
557 Assert(!isInteger(x_i
) || c_i
.isIntegral());
559 int cmpToLB
= d_partialModel
.cmpToLowerBound(x_i
, c_i
);
560 int cmpToUB
= d_partialModel
.cmpToUpperBound(x_i
, c_i
);
563 // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
564 if(cmpToUB
>= 0 && cmpToLB
<= 0){
569 Constraint ubc
= d_partialModel
.getUpperBoundConstraint(x_i
);
570 Node conflict
= ConstraintValue::explainConflict(ubc
, constraint
);
571 Debug("arith") << "AssertEquality conflicts with upper bound " << conflict
<< endl
;
572 raiseConflict(conflict
);
577 Constraint lbc
= d_partialModel
.getLowerBoundConstraint(x_i
);
578 Node conflict
= ConstraintValue::explainConflict(lbc
, constraint
);
579 Debug("arith") << "AssertEquality conflicts with lower bound" << conflict
<< endl
;
580 raiseConflict(conflict
);
584 Assert(cmpToUB
<= 0);
585 Assert(cmpToLB
>= 0);
586 Assert(cmpToUB
< 0 || cmpToLB
> 0);
590 d_constantIntegerVariables
.push_back(x_i
);
591 Debug("dio::push") << x_i
<< endl
;
594 // Don't bother to check whether x_i != c_i is in d_diseq
595 // The a and (not a) should never be on the fact queue
596 d_currentPropagationList
.push_back(constraint
);
597 d_currentPropagationList
.push_back(d_partialModel
.getLowerBoundConstraint(x_i
));
598 d_currentPropagationList
.push_back(d_partialModel
.getUpperBoundConstraint(x_i
));
600 d_partialModel
.setUpperBoundConstraint(constraint
);
601 d_partialModel
.setLowerBoundConstraint(constraint
);
603 if(d_congruenceManager
.isWatchedVariable(x_i
)){
606 zeroDifferenceDetected(x_i
);
608 d_congruenceManager
.watchedVariableCannotBeZero(constraint
);
609 d_congruenceManager
.equalsConstant(constraint
);
612 d_congruenceManager
.equalsConstant(constraint
);
615 d_updatedBounds
.softAdd(x_i
);
617 if(Debug
.isOn("model")) {
618 Debug("model") << "before" << endl
;
619 d_partialModel
.printModel(x_i
);
620 d_tableau
.debugPrintIsBasic(x_i
);
623 if(!d_tableau
.isBasic(x_i
)){
624 if(!(d_partialModel
.getAssignment(x_i
) == c_i
)){
625 d_linEq
.update(x_i
, c_i
);
628 d_errorSet
.signalVariable(x_i
);
631 if(Debug
.isOn("model")) {
632 Debug("model") << "after" << endl
;
633 d_partialModel
.printModel(x_i
);
634 d_tableau
.debugPrintIsBasic(x_i
);
641 /* procedure AssertDisequality( x_i != c_i ) */
642 bool TheoryArithPrivate::AssertDisequality(Constraint constraint
){
644 AssertArgument(constraint
!= NullConstraint
,
645 "AssertUpper() called on a NullConstraint.");
646 ArithVar x_i
= constraint
->getVariable();
647 const DeltaRational
& c_i
= constraint
->getValue();
649 Debug("arith") << "AssertDisequality(" << x_i
<< " " << c_i
<< ")"<< std::endl
;
651 //Should be fine in integers
652 Assert(!isInteger(x_i
) || c_i
.isIntegral());
654 if(d_congruenceManager
.isWatchedVariable(x_i
)){
657 d_congruenceManager
.watchedVariableCannotBeZero(constraint
);
661 const ValueCollection
& vc
= constraint
->getValueCollection();
662 if(vc
.hasLowerBound() && vc
.hasUpperBound()){
663 const Constraint lb
= vc
.getLowerBound();
664 const Constraint ub
= vc
.getUpperBound();
665 if(lb
->isTrue() && ub
->isTrue()){
667 Debug("eq") << "explaining" << endl
;
668 ++(d_statistics
.d_statDisequalityConflicts
);
669 Node conflict
= ConstraintValue::explainConflict(constraint
, lb
, ub
);
670 raiseConflict(conflict
);
674 if(vc
.hasLowerBound() ){
675 const Constraint lb
= vc
.getLowerBound();
677 const Constraint ub
= d_constraintDatabase
.ensureConstraint(const_cast<ValueCollection
&>(vc
), UpperBound
);
678 Debug("eq") << "propagate UpperBound " << constraint
<< lb
<< ub
<< endl
;
679 const Constraint negUb
= ub
->getNegation();
680 if(!negUb
->isTrue()){
681 negUb
->impliedBy(constraint
, lb
);
682 d_learnedBounds
.push_back(negUb
);
686 if(vc
.hasUpperBound()){
687 const Constraint ub
= vc
.getUpperBound();
689 const Constraint lb
= d_constraintDatabase
.ensureConstraint(const_cast<ValueCollection
&>(vc
), LowerBound
);
691 Debug("eq") << "propagate LowerBound " << constraint
<< lb
<< ub
<< endl
;
692 const Constraint negLb
= lb
->getNegation();
693 if(!negLb
->isTrue()){
694 negLb
->impliedBy(constraint
, ub
);
695 d_learnedBounds
.push_back(negLb
);
700 bool split
= constraint
->isSplit();
702 if(!split
&& c_i
== d_partialModel
.getAssignment(x_i
)){
703 Debug("eq") << "lemma now! " << constraint
<< endl
;
704 outputLemma(constraint
->split());
706 }else if(d_partialModel
.strictlyLessThanLowerBound(x_i
, c_i
)){
707 Debug("eq") << "can drop as less than lb" << constraint
<< endl
;
708 }else if(d_partialModel
.strictlyGreaterThanUpperBound(x_i
, c_i
)){
709 Debug("eq") << "can drop as less than ub" << constraint
<< endl
;
711 Debug("eq") << "push back" << constraint
<< endl
;
712 d_diseqQueue
.push(constraint
);
713 d_partialModel
.invalidateDelta();
715 Debug("eq") << "skipping already split " << constraint
<< endl
;
720 void TheoryArithPrivate::addSharedTerm(TNode n
){
721 Debug("arith::addSharedTerm") << "addSharedTerm: " << n
<< endl
;
723 d_partialModel
.invalidateDelta();
726 d_congruenceManager
.addSharedTerm(n
);
727 if(!n
.isConst() && !isSetup(n
)){
728 Polynomial poly
= Polynomial::parsePolynomial(n
);
729 Polynomial::iterator it
= poly
.begin();
730 Polynomial::iterator it_end
= poly
.end();
731 for (; it
!= it_end
; ++ it
) {
733 if (!m
.isConstant() && !isSetup(m
.getVarList().getNode())) {
734 setupVariableList(m
.getVarList());
741 struct ToIntegerTag
{ };
742 struct LinearIntDivTag
{ };
743 }/* CVC4::theory::arith::attr namespace */
746 * This attribute maps the child of a to_int / is_int to the
747 * corresponding integer skolem.
749 typedef expr::Attribute
<attr::ToIntegerTag
, Node
> ToIntegerAttr
;
752 * This attribute maps division-by-constant-k terms to a variable
753 * used to eliminate them.
755 typedef expr::Attribute
<attr::LinearIntDivTag
, Node
> LinearIntDivAttr
;
757 Node
TheoryArithPrivate::ppRewriteTerms(TNode n
) {
758 if(Theory::theoryOf(n
) != THEORY_ARITH
) {
762 NodeManager
* nm
= NodeManager::currentNM();
764 switch(Kind k
= n
.getKind()) {
766 case kind::TO_INTEGER
:
767 case kind::IS_INTEGER
: {
769 if(!n
[0].getAttribute(ToIntegerAttr(), intVar
)) {
770 intVar
= nm
->mkSkolem("toInt", nm
->integerType(), "a conversion of a Real term to its Integer part");
771 n
[0].setAttribute(ToIntegerAttr(), intVar
);
772 d_containing
.d_out
->lemma(nm
->mkNode(kind::AND
, nm
->mkNode(kind::LT
, nm
->mkNode(kind::MINUS
, n
[0], nm
->mkConst(Rational(1))), intVar
), nm
->mkNode(kind::LEQ
, intVar
, n
[0])));
774 if(n
.getKind() == kind::TO_INTEGER
) {
778 Node node
= nm
->mkNode(kind::EQUAL
, node
[0], intVar
);
784 case kind::INTS_DIVISION
:
785 case kind::INTS_DIVISION_TOTAL
: {
786 if(!options::rewriteDivk()) {
789 Node num
= Rewriter::rewrite(n
[0]);
790 Node den
= Rewriter::rewrite(n
[1]);
792 const Rational
& rat
= den
.getConst
<Rational
>();
793 Assert(!num
.isConst());
796 Node rw
= nm
->mkNode(k
, num
, den
);
797 if(!rw
.getAttribute(LinearIntDivAttr(), intVar
)) {
798 intVar
= nm
->mkSkolem("linearIntDiv", nm
->integerType(), "the result of an intdiv-by-k term");
799 rw
.setAttribute(LinearIntDivAttr(), intVar
);
801 d_containing
.d_out
->lemma(nm
->mkNode(kind::AND
, nm
->mkNode(kind::LEQ
, nm
->mkNode(kind::MULT
, den
, intVar
), num
), nm
->mkNode(kind::LT
, num
, nm
->mkNode(kind::MULT
, den
, nm
->mkNode(kind::PLUS
, intVar
, nm
->mkConst(Rational(1)))))));
803 d_containing
.d_out
->lemma(nm
->mkNode(kind::AND
, nm
->mkNode(kind::LEQ
, nm
->mkNode(kind::MULT
, den
, intVar
), num
), nm
->mkNode(kind::LT
, num
, nm
->mkNode(kind::MULT
, den
, nm
->mkNode(kind::PLUS
, intVar
, nm
->mkConst(Rational(-1)))))));
812 case kind::INTS_MODULUS
:
813 case kind::INTS_MODULUS_TOTAL
: {
814 if(!options::rewriteDivk()) {
817 Node num
= Rewriter::rewrite(n
[0]);
818 Node den
= Rewriter::rewrite(n
[1]);
820 const Rational
& rat
= den
.getConst
<Rational
>();
821 Assert(!num
.isConst());
824 Node rw
= nm
->mkNode(k
, num
, den
);
825 if(!rw
.getAttribute(LinearIntDivAttr(), intVar
)) {
826 intVar
= nm
->mkSkolem("linearIntDiv", nm
->integerType(), "the result of an intdiv-by-k term");
827 rw
.setAttribute(LinearIntDivAttr(), intVar
);
829 d_containing
.d_out
->lemma(nm
->mkNode(kind::AND
, nm
->mkNode(kind::LEQ
, nm
->mkNode(kind::MULT
, den
, intVar
), num
), nm
->mkNode(kind::LT
, num
, nm
->mkNode(kind::MULT
, den
, nm
->mkNode(kind::PLUS
, intVar
, nm
->mkConst(Rational(1)))))));
831 d_containing
.d_out
->lemma(nm
->mkNode(kind::AND
, nm
->mkNode(kind::LEQ
, nm
->mkNode(kind::MULT
, den
, intVar
), num
), nm
->mkNode(kind::LT
, num
, nm
->mkNode(kind::MULT
, den
, nm
->mkNode(kind::PLUS
, intVar
, nm
->mkConst(Rational(-1)))))));
834 Node node
= nm
->mkNode(kind::MINUS
, num
, nm
->mkNode(kind::MULT
, den
, intVar
));
845 for(TNode::const_iterator i
= n
.begin(); i
!= n
.end(); ++i
) {
846 Node rewritten
= ppRewriteTerms(*i
);
847 if(rewritten
!= *i
) {
848 NodeBuilder
<> b(n
.getKind());
849 b
.append(n
.begin(), i
);
851 for(++i
; i
!= n
.end(); ++i
) {
852 b
<< ppRewriteTerms(*i
);
862 Node
TheoryArithPrivate::ppRewrite(TNode atom
) {
863 Debug("arith::preprocess") << "arith::preprocess() : " << atom
<< endl
;
865 if (atom
.getKind() == kind::EQUAL
&& options::arithRewriteEq()) {
866 Node leq
= NodeBuilder
<2>(kind::LEQ
) << atom
[0] << atom
[1];
867 Node geq
= NodeBuilder
<2>(kind::GEQ
) << atom
[0] << atom
[1];
868 leq
= ppRewriteTerms(leq
);
869 geq
= ppRewriteTerms(geq
);
870 Node rewritten
= Rewriter::rewrite(leq
.andNode(geq
));
871 Debug("arith::preprocess") << "arith::preprocess() : returning "
872 << rewritten
<< endl
;
875 return ppRewriteTerms(atom
);
879 Theory::PPAssertStatus
TheoryArithPrivate::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) {
880 TimerStat::CodeTimer
codeTimer(d_statistics
.d_simplifyTimer
);
881 Debug("simplify") << "TheoryArithPrivate::solve(" << in
<< ")" << endl
;
885 Rational minConstant
= 0;
888 if (in
.getKind() == kind::EQUAL
) {
889 Comparison cmp
= Comparison::parseNormalForm(in
);
891 Polynomial left
= cmp
.getLeft();
892 Polynomial right
= cmp
.getRight();
894 Monomial m
= left
.getHead();
895 if (m
.getVarList().singleton()){
896 VarList vl
= m
.getVarList();
897 Node var
= vl
.getNode();
898 if (var
.getKind() == kind::VARIABLE
){
899 // if vl.isIntegral then m.getConstant().isOne()
900 if(!vl
.isIntegral() || m
.getConstant().isOne()){
906 // Solve for variable
907 if (!minVar
.isNull()) {
908 Polynomial right
= cmp
.getRight();
909 Node elim
= right
.getNode();
910 // ax + p = c -> (ax + p) -ax - c = -ax
911 // x = (p - ax - c) * -1/a
912 // Add the substitution if not recursive
913 Assert(elim
== Rewriter::rewrite(elim
));
916 static const unsigned MAX_SUB_SIZE
= 2;
917 if(right
.size() > MAX_SUB_SIZE
){
918 Debug("simplify") << "TheoryArithPrivate::solve(): did not substitute due to the right hand side containing too many terms: " << minVar
<< ":" << elim
<< endl
;
919 Debug("simplify") << right
.size() << endl
;
920 // cout << "TheoryArithPrivate::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
921 // cout << right.size() << endl;
922 }else if(elim
.hasSubterm(minVar
)){
923 Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute due to recursive pattern with sharing: " << minVar
<< ":" << elim
<< endl
;
924 // cout << "TheoryArithPrivate::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl;
926 }else if (!minVar
.getType().isInteger() || right
.isIntegral()) {
927 Assert(!elim
.hasSubterm(minVar
));
928 // cannot eliminate integers here unless we know the resulting
929 // substitution is integral
930 Debug("simplify") << "TheoryArithPrivate::solve(): substitution " << minVar
<< " |-> " << elim
<< endl
;
931 //cout << "TheoryArithPrivate::solve(): substitution " << minVar << " |-> " << elim << endl;
933 outSubstitutions
.addSubstitution(minVar
, elim
);
934 return Theory::PP_ASSERT_STATUS_SOLVED
;
936 Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute b/c it's integer: " << minVar
<< ":" << minVar
.getType() << " |-> " << elim
<< ":" << elim
.getType() << endl
;
937 //cout << "TheoryArithPrivate::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
943 // If a relation, remember the bound
944 switch(in
.getKind()) {
950 d_learner
.addBound(in
);
958 return Theory::PP_ASSERT_STATUS_UNSOLVED
;
961 void TheoryArithPrivate::ppStaticLearn(TNode n
, NodeBuilder
<>& learned
) {
962 TimerStat::CodeTimer
codeTimer(d_statistics
.d_staticLearningTimer
);
964 d_learner
.staticLearning(n
, learned
);
969 ArithVar
TheoryArithPrivate::findShortestBasicRow(ArithVar variable
){
970 ArithVar bestBasic
= ARITHVAR_SENTINEL
;
971 uint64_t bestRowLength
= std::numeric_limits
<uint64_t>::max();
973 Tableau::ColIterator basicIter
= d_tableau
.colIterator(variable
);
974 for(; !basicIter
.atEnd(); ++basicIter
){
975 const Tableau::Entry
& entry
= *basicIter
;
976 Assert(entry
.getColVar() == variable
);
977 RowIndex ridx
= entry
.getRowIndex();
978 ArithVar basic
= d_tableau
.rowIndexToBasic(ridx
);
979 uint32_t rowLength
= d_tableau
.getRowLength(ridx
);
980 if((rowLength
< bestRowLength
) ||
981 (rowLength
== bestRowLength
&& basic
< bestBasic
)){
983 bestRowLength
= rowLength
;
986 Assert(bestBasic
== ARITHVAR_SENTINEL
|| bestRowLength
< std::numeric_limits
<uint32_t>::max());
990 void TheoryArithPrivate::setupVariable(const Variable
& x
){
991 Node n
= x
.getNode();
995 ++(d_statistics
.d_statUserVariables
);
996 requestArithVar(n
,false);
997 //ArithVar varN = requestArithVar(n,false);
998 //setupInitialValue(varN);
1009 void TheoryArithPrivate::setupVariableList(const VarList
& vl
){
1010 Assert(!vl
.empty());
1012 TNode vlNode
= vl
.getNode();
1013 Assert(!isSetup(vlNode
));
1014 Assert(!d_partialModel
.hasArithVar(vlNode
));
1016 for(VarList::iterator i
= vl
.begin(), end
= vl
.end(); i
!= end
; ++i
){
1019 if(!isSetup(var
.getNode())){
1024 if(!vl
.singleton()){
1025 // vl is the product of at least 2 variables
1026 // vl : (* v1 v2 ...)
1027 if(getLogicInfo().isLinear()){
1028 throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic.");
1032 d_nlIncomplete
= true;
1034 ++(d_statistics
.d_statUserVariables
);
1035 requestArithVar(vlNode
, false);
1036 //ArithVar av = requestArithVar(vlNode, false);
1037 //setupInitialValue(av);
1043 * Only call markSetup if the VarList is not a singleton.
1044 * See the comment in setupPolynomail for more.
1048 void TheoryArithPrivate::cautiousSetupPolynomial(const Polynomial
& p
){
1049 if(p
.containsConstant()){
1050 if(!p
.isConstant()){
1051 Polynomial noConstant
= p
.getTail();
1052 if(!isSetup(noConstant
.getNode())){
1053 setupPolynomial(noConstant
);
1056 }else if(!isSetup(p
.getNode())){
1061 void TheoryArithPrivate::setupDivLike(const Variable
& v
){
1062 Assert(v
.isDivLike());
1064 if(getLogicInfo().isLinear()){
1065 throw LogicException("A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic;\nif you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.");
1068 Node vnode
= v
.getNode();
1069 Assert(isSetup(vnode
)); // Otherwise there is some invariant breaking recursion
1070 Polynomial m
= Polynomial::parsePolynomial(vnode
[0]);
1071 Polynomial n
= Polynomial::parsePolynomial(vnode
[1]);
1073 cautiousSetupPolynomial(m
);
1074 cautiousSetupPolynomial(n
);
1077 switch(vnode
.getKind()){
1081 lem
= definingIteForDivLike(vnode
);
1083 case DIVISION_TOTAL
:
1084 lem
= axiomIteForTotalDivision(vnode
);
1086 case INTS_DIVISION_TOTAL
:
1087 case INTS_MODULUS_TOTAL
:
1088 lem
= axiomIteForTotalIntDivision(vnode
);
1091 /* intentionally blank */
1096 Debug("arith::div") << lem
<< endl
;
1101 Node
TheoryArithPrivate::definingIteForDivLike(Node divLike
){
1102 Kind k
= divLike
.getKind();
1103 Assert(k
== DIVISION
|| k
== INTS_DIVISION
|| k
== INTS_MODULUS
);
1104 // (for all ((n Real) (d Real))
1108 // (APPLY [div_0_skolem_function] n)
1109 // (DIVISION_TOTAL x y))))
1111 Polynomial n
= Polynomial::parsePolynomial(divLike
[0]);
1112 Polynomial d
= Polynomial::parsePolynomial(divLike
[1]);
1114 NodeManager
* currNM
= NodeManager::currentNM();
1115 Node dEq0
= currNM
->mkNode(EQUAL
, d
.getNode(), mkRationalNode(0));
1117 Kind kTotal
= (k
== DIVISION
) ? DIVISION_TOTAL
:
1118 (k
== INTS_DIVISION
) ? INTS_DIVISION_TOTAL
: INTS_MODULUS_TOTAL
;
1120 Node by0Func
= (k
== DIVISION
) ? getRealDivideBy0Func():
1121 (k
== INTS_DIVISION
) ? getIntDivideBy0Func() : getIntModulusBy0Func();
1124 Debug("arith::div") << divLike
<< endl
;
1125 Debug("arith::div") << by0Func
<< endl
;
1127 Node divTotal
= currNM
->mkNode(kTotal
, n
.getNode(), d
.getNode());
1128 Node divZero
= currNM
->mkNode(APPLY_UF
, by0Func
, n
.getNode());
1130 Node defining
= divLike
.eqNode(dEq0
.iteNode( divZero
, divTotal
));
1135 Node
TheoryArithPrivate::axiomIteForTotalDivision(Node div_tot
){
1136 Assert(div_tot
.getKind() == DIVISION_TOTAL
);
1138 // Inverse of multiplication axiom:
1139 // (for all ((n Real) (d Real))
1141 // (= (DIVISION_TOTAL n d) 0)
1142 // (= (* d (DIVISION_TOTAL n d)) n)))
1145 Polynomial n
= Polynomial::parsePolynomial(div_tot
[0]);
1146 Polynomial d
= Polynomial::parsePolynomial(div_tot
[1]);
1147 Polynomial div_tot_p
= Polynomial::parsePolynomial(div_tot
);
1149 Comparison invEq
= Comparison::mkComparison(EQUAL
, n
, d
* div_tot_p
);
1150 Comparison zeroEq
= Comparison::mkComparison(EQUAL
, div_tot_p
, Polynomial::mkZero());
1151 Node dEq0
= (d
.getNode()).eqNode(mkRationalNode(0));
1152 Node ite
= dEq0
.iteNode(zeroEq
.getNode(), invEq
.getNode());
1157 Node
TheoryArithPrivate::axiomIteForTotalIntDivision(Node int_div_like
){
1158 Kind k
= int_div_like
.getKind();
1159 Assert(k
== INTS_DIVISION_TOTAL
|| k
== INTS_MODULUS_TOTAL
);
1161 // (for all ((m Int) (n Int))
1162 // (=> (distinct n 0)
1163 // (let ((q (div m n)) (r (mod m n)))
1164 // (and (= m (+ (* n q) r))
1165 // (<= 0 r (- (abs n) 1))))))
1167 // Updated for div 0 functions
1168 // (for all ((m Int) (n Int))
1169 // (let ((q (div m n)) (r (mod m n)))
1171 // (and (= q (div_0_func m)) (= r (mod_0_func m)))
1172 // (and (= m (+ (* n q) r))
1173 // (<= 0 r (- (abs n) 1)))))))
1175 Polynomial n
= Polynomial::parsePolynomial(int_div_like
[0]);
1176 Polynomial d
= Polynomial::parsePolynomial(int_div_like
[1]);
1178 NodeManager
* currNM
= NodeManager::currentNM();
1179 Node zero
= mkRationalNode(0);
1181 Node q
= (k
== INTS_DIVISION_TOTAL
) ? int_div_like
: currNM
->mkNode(INTS_DIVISION_TOTAL
, n
.getNode(), d
.getNode());
1182 Node r
= (k
== INTS_MODULUS_TOTAL
) ? int_div_like
: currNM
->mkNode(INTS_MODULUS_TOTAL
, n
.getNode(), d
.getNode());
1184 Node dEq0
= (d
.getNode()).eqNode(zero
);
1185 Node qEq0
= q
.eqNode(zero
);
1186 Node rEq0
= r
.eqNode(zero
);
1188 Polynomial rp
= Polynomial::parsePolynomial(r
);
1189 Polynomial qp
= Polynomial::parsePolynomial(q
);
1191 Node abs_d
= (n
.isConstant()) ?
1192 d
.getHead().getConstant().abs().getNode() : mkIntSkolem("abs_$$");
1194 Node eq
= Comparison::mkComparison(EQUAL
, n
, d
* qp
+ rp
).getNode();
1195 Node leq0
= currNM
->mkNode(LEQ
, zero
, r
);
1196 Node leq1
= currNM
->mkNode(LT
, r
, abs_d
);
1198 Node andE
= currNM
->mkNode(AND
, eq
, leq0
, leq1
);
1199 Node defDivMode
= dEq0
.iteNode(qEq0
.andNode(rEq0
), andE
);
1200 Node lem
= abs_d
.getMetaKind () == metakind::VARIABLE
?
1201 defDivMode
.andNode(d
.makeAbsCondition(Variable(abs_d
))) : defDivMode
;
1207 void TheoryArithPrivate::setupPolynomial(const Polynomial
& poly
) {
1208 Assert(!poly
.containsConstant());
1209 TNode polyNode
= poly
.getNode();
1210 Assert(!isSetup(polyNode
));
1211 Assert(!d_partialModel
.hasArithVar(polyNode
));
1213 for(Polynomial::iterator i
= poly
.begin(), end
= poly
.end(); i
!= end
; ++i
){
1215 const VarList
& vl
= mono
.getVarList();
1216 if(!isSetup(vl
.getNode())){
1217 setupVariableList(vl
);
1221 if(polyNode
.getKind() == PLUS
){
1222 d_tableauSizeHasBeenModified
= true;
1224 vector
<ArithVar
> variables
;
1225 vector
<Rational
> coefficients
;
1226 asVectors(poly
, coefficients
, variables
);
1228 ArithVar varSlack
= requestArithVar(polyNode
, true);
1229 d_tableau
.addRow(varSlack
, coefficients
, variables
);
1230 setupBasicValue(varSlack
);
1231 d_linEq
.trackRowIndex(d_tableau
.basicToRowIndex(varSlack
));
1233 //Add differences to the difference manager
1234 Polynomial::iterator i
= poly
.begin(), end
= poly
.end();
1236 Monomial first
= *i
;
1239 Monomial second
= *i
;
1242 if(first
.getConstant().isOne() && second
.getConstant().getValue() == -1){
1243 VarList vl0
= first
.getVarList();
1244 VarList vl1
= second
.getVarList();
1245 if(vl0
.singleton() && vl1
.singleton()){
1246 d_congruenceManager
.addWatchedPair(varSlack
, vl0
.getNode(), vl1
.getNode());
1253 ++(d_statistics
.d_statSlackVariables
);
1254 markSetup(polyNode
);
1258 * It is worth documenting that polyNode should only be marked as
1259 * being setup by this function if it has kind PLUS.
1260 * Other kinds will be marked as being setup by lower levels of setup
1261 * specifically setupVariableList.
1265 void TheoryArithPrivate::setupAtom(TNode atom
) {
1266 Assert(isRelationOperator(atom
.getKind()));
1267 Assert(Comparison::isNormalAtom(atom
));
1268 Assert(!isSetup(atom
));
1269 Assert(!d_constraintDatabase
.hasLiteral(atom
));
1271 Comparison cmp
= Comparison::parseNormalForm(atom
);
1272 Polynomial nvp
= cmp
.normalizedVariablePart();
1273 Assert(!nvp
.isZero());
1275 if(!isSetup(nvp
.getNode())){
1276 setupPolynomial(nvp
);
1279 d_constraintDatabase
.addLiteral(atom
);
1284 void TheoryArithPrivate::preRegisterTerm(TNode n
) {
1285 Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n
<<")"<< endl
;
1288 if(isRelationOperator(n
.getKind())){
1292 Constraint c
= d_constraintDatabase
.lookup(n
);
1293 Assert(c
!= NullConstraint
);
1295 Debug("arith::preregister") << "setup constraint" << c
<< endl
;
1296 Assert(!c
->canBePropagated());
1297 c
->setPreregistered();
1299 } catch(LogicException
& le
) {
1300 std::stringstream ss
;
1301 ss
<< le
.getMessage() << endl
<< "The fact in question: " << n
<< endl
;
1302 throw LogicException(ss
.str());
1305 Debug("arith::preregister") << "end arith::preRegisterTerm("<< n
<<")" << endl
;
1308 void TheoryArithPrivate::releaseArithVar(ArithVar v
){
1309 Assert(d_partialModel
.hasNode(v
));
1311 d_constraintDatabase
.removeVariable(v
);
1312 d_partialModel
.releaseArithVar(v
);
1315 ArithVar
TheoryArithPrivate::requestArithVar(TNode x
, bool slack
){
1316 //TODO : The VarList trick is good enough?
1317 Assert(isLeaf(x
) || VarList::isMember(x
) || x
.getKind() == PLUS
);
1318 if(getLogicInfo().isLinear() && Variable::isDivMember(x
)){
1320 ss
<< "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: " << x
<< endl
1321 << "if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.";
1322 throw LogicException(ss
.str());
1324 Assert(!d_partialModel
.hasArithVar(x
));
1325 Assert(x
.getType().isReal()); // real or integer
1327 ArithVar max
= d_partialModel
.getNumberOfVariables();
1328 ArithVar varX
= d_partialModel
.allocate(x
, slack
);
1330 bool reclaim
= max
>= d_partialModel
.getNumberOfVariables();;
1333 d_dualSimplex
.increaseMax();
1335 d_tableau
.increaseSize();
1336 d_tableauSizeHasBeenModified
= true;
1338 d_constraintDatabase
.addVariable(varX
);
1340 Debug("arith::arithvar") << x
<< " |-> " << varX
<< endl
;
1342 Assert(!d_partialModel
.hasUpperBound(varX
));
1343 Assert(!d_partialModel
.hasLowerBound(varX
));
1348 void TheoryArithPrivate::asVectors(const Polynomial
& p
, std::vector
<Rational
>& coeffs
, std::vector
<ArithVar
>& variables
) {
1349 for(Polynomial::iterator i
= p
.begin(), end
= p
.end(); i
!= end
; ++i
){
1350 const Monomial
& mono
= *i
;
1351 const Constant
& constant
= mono
.getConstant();
1352 const VarList
& variable
= mono
.getVarList();
1354 Node n
= variable
.getNode();
1356 Debug("rewriter") << "should be var: " << n
<< endl
;
1358 // TODO: This VarList::isMember(n) can be stronger
1359 Assert(isLeaf(n
) || VarList::isMember(n
));
1360 Assert(theoryOf(n
) != THEORY_ARITH
|| d_partialModel
.hasArithVar(n
));
1362 Assert(d_partialModel
.hasArithVar(n
));
1363 ArithVar av
= d_partialModel
.asArithVar(n
);
1365 coeffs
.push_back(constant
.getValue());
1366 variables
.push_back(av
);
1371 * For basic variables the row must have been added to the tableau.
1373 void TheoryArithPrivate::setupBasicValue(ArithVar x
){
1374 Assert(d_tableau
.isBasic(x
));
1375 //If the variable is basic, assertions may have already happened and updates
1376 //may have occured before setting this variable up.
1378 //This can go away if the tableau creation is done at preregister
1379 //time instead of register
1380 DeltaRational safeAssignment
= d_linEq
.computeRowValue(x
, true);
1381 DeltaRational assignment
= d_linEq
.computeRowValue(x
, false);
1382 d_partialModel
.setAssignment(x
,safeAssignment
,assignment
);
1384 Debug("arith") << "setupVariable("<<x
<<")"<<std::endl
;
1387 ArithVar
TheoryArithPrivate::determineArithVar(const Polynomial
& p
) const{
1388 Assert(!p
.containsConstant());
1389 Assert(p
.getHead().constantIsPositive());
1390 TNode n
= p
.getNode();
1391 Debug("determineArithVar") << "determineArithVar(" << n
<< ")" << endl
;
1392 return d_partialModel
.asArithVar(n
);
1395 ArithVar
TheoryArithPrivate::determineArithVar(TNode assertion
) const{
1396 Debug("determineArithVar") << "determineArithVar " << assertion
<< endl
;
1397 Comparison cmp
= Comparison::parseNormalForm(assertion
);
1398 Polynomial variablePart
= cmp
.normalizedVariablePart();
1399 return determineArithVar(variablePart
);
1403 bool TheoryArithPrivate::canSafelyAvoidEqualitySetup(TNode equality
){
1404 Assert(equality
.getKind() == EQUAL
);
1405 return d_partialModel
.hasArithVar(equality
[0]);
1408 Comparison
TheoryArithPrivate::mkIntegerEqualityFromAssignment(ArithVar v
){
1409 const DeltaRational
& beta
= d_partialModel
.getAssignment(v
);
1411 Assert(beta
.isIntegral());
1412 Polynomial
betaAsPolynomial( Constant::mkConstant(beta
.floor()) );
1414 TNode var
= d_partialModel
.asNode(v
);
1415 Polynomial varAsPolynomial
= Polynomial::parsePolynomial(var
);
1416 return Comparison::mkComparison(EQUAL
, varAsPolynomial
, betaAsPolynomial
);
1419 Node
TheoryArithPrivate::dioCutting(){
1420 context::Context::ScopedPush
speculativePush(getSatContext());
1421 //DO NOT TOUCH THE OUTPUTSTREAM
1423 for(var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
1426 if(d_partialModel
.cmpAssignmentUpperBound(v
) == 0 ||
1427 d_partialModel
.cmpAssignmentLowerBound(v
) == 0){
1428 if(!d_partialModel
.boundsAreEqual(v
)){
1429 // If the bounds are equal this is already in the dioSolver
1430 //Add v = dr as a speculation.
1431 Comparison eq
= mkIntegerEqualityFromAssignment(v
);
1432 Debug("dio::push") <<v
<< " " << eq
.getNode() << endl
;
1433 Assert(!eq
.isBoolean());
1434 d_diosolver
.pushInputConstraint(eq
, eq
.getNode());
1435 // It does not matter what the explanation of eq is.
1436 // It cannot be used in a conflict
1442 SumPair plane
= d_diosolver
.processEquationsForCut();
1444 return Node::null();
1446 Polynomial p
= plane
.getPolynomial();
1447 Polynomial
c(plane
.getConstant() * Constant::mkConstant(-1));
1448 Integer gcd
= p
.gcd();
1449 Assert(p
.isIntegral());
1450 Assert(c
.isIntegral());
1452 Assert(!gcd
.divides(c
.asConstant().getNumerator()));
1453 Comparison leq
= Comparison::mkComparison(LEQ
, p
, c
);
1454 Comparison geq
= Comparison::mkComparison(GEQ
, p
, c
);
1455 Node lemma
= NodeManager::currentNM()->mkNode(OR
, leq
.getNode(), geq
.getNode());
1456 Node rewrittenLemma
= Rewriter::rewrite(lemma
);
1457 Debug("arith::dio") << "dioCutting found the plane: " << plane
.getNode() << endl
;
1458 Debug("arith::dio") << "resulting in the cut: " << lemma
<< endl
;
1459 Debug("arith::dio") << "rewritten " << rewrittenLemma
<< endl
;
1460 return rewrittenLemma
;
1464 Node
TheoryArithPrivate::callDioSolver(){
1465 while(!d_constantIntegerVariables
.empty()){
1466 ArithVar v
= d_constantIntegerVariables
.front();
1467 d_constantIntegerVariables
.pop();
1469 Debug("arith::dio") << v
<< endl
;
1471 Assert(isInteger(v
));
1472 Assert(d_partialModel
.boundsAreEqual(v
));
1475 Constraint lb
= d_partialModel
.getLowerBoundConstraint(v
);
1476 Constraint ub
= d_partialModel
.getUpperBoundConstraint(v
);
1478 Node orig
= Node::null();
1479 if(lb
->isEquality()){
1480 orig
= lb
->explainForConflict();
1481 }else if(ub
->isEquality()){
1482 orig
= ub
->explainForConflict();
1484 orig
= ConstraintValue::explainConflict(ub
, lb
);
1487 Assert(d_partialModel
.assignmentIsConsistent(v
));
1489 Comparison eq
= mkIntegerEqualityFromAssignment(v
);
1492 //This can only be a conflict
1493 Assert(!eq
.getNode().getConst
<bool>());
1495 //This should be handled by the normal form earlier in the case of equality
1496 Assert(orig
.getKind() != EQUAL
);
1499 Debug("dio::push") << v
<< " " << eq
.getNode() << " with reason " << orig
<< endl
;
1500 d_diosolver
.pushInputConstraint(eq
, orig
);
1504 return d_diosolver
.processEquationsForConflict();
1507 Constraint
TheoryArithPrivate::constraintFromFactQueue(){
1509 TNode assertion
= get();
1511 if( options::finiteModelFind() && d_quantEngine
&& d_quantEngine
->getBoundedIntegers() ){
1512 d_quantEngine
->getBoundedIntegers()->assertNode(assertion
);
1515 Kind simpleKind
= Comparison::comparisonKind(assertion
);
1516 Constraint constraint
= d_constraintDatabase
.lookup(assertion
);
1517 if(constraint
== NullConstraint
){
1518 Assert(simpleKind
== EQUAL
|| simpleKind
== DISTINCT
);
1519 bool isDistinct
= simpleKind
== DISTINCT
;
1520 Node eq
= (simpleKind
== DISTINCT
) ? assertion
[0] : assertion
;
1521 Assert(!isSetup(eq
));
1522 Node reEq
= Rewriter::rewrite(eq
);
1523 if(reEq
.getKind() == CONST_BOOLEAN
){
1524 if(reEq
.getConst
<bool>() == isDistinct
){
1525 // if is (not true), or false
1526 Assert((reEq
.getConst
<bool>() && isDistinct
) ||
1527 (!reEq
.getConst
<bool>() && !isDistinct
));
1528 raiseConflict(assertion
);
1530 return NullConstraint
;
1532 Assert(reEq
.getKind() != CONST_BOOLEAN
);
1536 Node reAssertion
= isDistinct
? reEq
.notNode() : reEq
;
1537 constraint
= d_constraintDatabase
.lookup(reAssertion
);
1539 if(assertion
!= reAssertion
){
1540 Debug("arith::nf") << "getting non-nf assertion " << assertion
<< " |-> " << reAssertion
<< endl
;
1541 Assert(constraint
!= NullConstraint
);
1542 d_assertionsThatDoNotMatchTheirLiterals
.insert(assertion
, constraint
);
1546 Assert(constraint
!= NullConstraint
);
1548 if(constraint
->negationHasProof()){
1549 Constraint negation
= constraint
->getNegation();
1550 if(negation
->isSelfExplaining()){
1551 if(Debug
.isOn("whytheoryenginewhy")){
1555 Debug("arith::eq") << constraint
<< endl
;
1556 Debug("arith::eq") << negation
<< endl
;
1558 NodeBuilder
<> nb(kind::AND
);
1560 negation
->explainForConflict(nb
);
1562 Debug("arith::eq") << "conflict" << conflict
<< endl
;
1563 raiseConflict(conflict
);
1564 return NullConstraint
;
1566 Assert(!constraint
->negationHasProof());
1568 if(constraint
->assertedToTheTheory()){
1570 return NullConstraint
;
1572 Debug("arith::constraint") << "arith constraint " << constraint
<< std::endl
;
1573 constraint
->setAssertedToTheTheory(assertion
);
1575 if(!constraint
->hasProof()){
1576 Debug("arith::constraint") << "marking as constraint as self explaining " << endl
;
1577 constraint
->selfExplaining();
1579 Debug("arith::constraint") << "already has proof: " << constraint
->explainForConflict() << endl
;
1586 bool TheoryArithPrivate::assertionCases(Constraint constraint
){
1587 Assert(constraint
->hasProof());
1588 Assert(!constraint
->negationHasProof());
1590 ArithVar x_i
= constraint
->getVariable();
1592 switch(constraint
->getType()){
1594 if(isInteger(x_i
) && constraint
->isStrictUpperBound()){
1595 Constraint floorConstraint
= constraint
->getFloor();
1596 if(!floorConstraint
->isTrue()){
1597 if(floorConstraint
->negationHasProof()){
1598 Node conf
= ConstraintValue::explainConflict(constraint
, floorConstraint
->getNegation());
1599 raiseConflict(conf
);
1602 floorConstraint
->impliedBy(constraint
);
1603 // Do not need to add to d_learnedBounds
1606 return AssertUpper(floorConstraint
);
1608 return AssertUpper(constraint
);
1611 if(isInteger(x_i
) && constraint
->isStrictLowerBound()){
1612 Constraint ceilingConstraint
= constraint
->getCeiling();
1613 if(!ceilingConstraint
->isTrue()){
1614 if(ceilingConstraint
->negationHasProof()){
1615 Node conf
= ConstraintValue::explainConflict(constraint
, ceilingConstraint
->getNegation());
1616 raiseConflict(conf
);
1619 ceilingConstraint
->impliedBy(constraint
);
1620 // Do not need to add to learnedBounds
1622 return AssertLower(ceilingConstraint
);
1624 return AssertLower(constraint
);
1627 return AssertEquality(constraint
);
1629 return AssertDisequality(constraint
);
1637 * Looks for the next integer variable without an integer assignment in a round robin fashion.
1638 * Changes the value of d_nextIntegerCheckVar.
1640 * If this returns false, d_nextIntegerCheckVar does not have an integer assignment.
1641 * If this returns true, all integer variables have an integer assignment.
1643 bool TheoryArithPrivate::hasIntegerModel(){
1644 //if(d_variables.size() > 0){
1645 ArithVar numVars
= d_partialModel
.getNumberOfVariables();
1647 const ArithVar rrEnd
= d_nextIntegerCheckVar
;
1649 //Do not include slack variables
1650 if(isInteger(d_nextIntegerCheckVar
) && !isSlackVariable(d_nextIntegerCheckVar
)) { // integer
1651 const DeltaRational
& d
= d_partialModel
.getAssignment(d_nextIntegerCheckVar
);
1652 if(!d
.isIntegral()){
1656 } while((d_nextIntegerCheckVar
= (1 + d_nextIntegerCheckVar
== numVars
? 0 : 1 + d_nextIntegerCheckVar
)) != rrEnd
);
1661 /** Outputs conflicts to the output channel. */
1662 void TheoryArithPrivate::outputConflicts(){
1663 Assert(!d_conflicts
.empty());
1664 for(size_t i
= 0, i_end
= d_conflicts
.size(); i
< i_end
; ++i
){
1665 Node conflict
= d_conflicts
[i
];
1666 Debug("arith::conflict") << "d_conflicts[" << i
<< "] " << conflict
<< endl
;
1667 (d_containing
.d_out
)->conflict(conflict
);
1671 void TheoryArithPrivate::branchVector(const std::vector
<ArithVar
>& lemmas
){
1673 for(vector
<ArithVar
>::const_iterator i
= lemmas
.begin(); i
!= lemmas
.end(); ++i
){
1675 Assert(!d_cutInContext
.contains(v
));
1676 d_cutInContext
.insert(v
);
1677 d_cutCount
= d_cutCount
+ 1;
1678 Node lem
= branchIntegerVariable(v
);
1680 ++(d_statistics
.d_externalBranchAndBounds
);
1684 bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel
){
1685 Assert(d_qflraStatus
!= Result::SAT
);
1687 d_partialModel
.stopQueueingBoundCounts();
1688 UpdateTrackingCallback
utcb(&d_linEq
);
1689 d_partialModel
.processBoundsQueue(utcb
);
1690 d_linEq
.startTrackingBoundCounts();
1692 bool noPivotLimit
= Theory::fullEffort(effortLevel
) ||
1693 !options::restrictedPivots();
1695 bool emmittedConflictOrSplit
= false;
1697 SimplexDecisionProcedure
& simplex
=
1698 options::useFC() ? (SimplexDecisionProcedure
&)d_fcSimplex
:
1699 (options::useSOI() ? (SimplexDecisionProcedure
&)d_soiSimplex
:
1700 (SimplexDecisionProcedure
&)d_dualSimplex
);
1702 bool useFancyFinal
= options::fancyFinal() && ApproximateSimplex::enabled();
1705 d_qflraStatus
= simplex
.findModel(noPivotLimit
);
1707 // Fancy final tries the following strategy
1708 // At final check, try the preferred simplex solver with a pivot cap
1709 // If that failed, swap the the other simplex solver
1710 // If that failed, check if there are integer variables to cut
1711 // If that failed, do a simplex without a pivot limit
1713 int16_t oldCap
= options::arithStandardCheckVarOrderPivots();
1715 static const int32_t pass2Limit
= 10;
1716 static const int32_t relaxationLimit
= 10000;
1717 static const int32_t mipLimit
= 200000;
1719 //cout << "start" << endl;
1720 d_qflraStatus
= simplex
.findModel(false);
1721 //cout << "end" << endl;
1722 if(d_qflraStatus
== Result::SAT_UNKNOWN
||
1723 (d_qflraStatus
== Result::SAT
&& !hasIntegerModel() && !d_likelyIntegerInfeasible
)){
1725 ApproximateSimplex
* approxSolver
= ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel
);
1726 approxSolver
->setPivotLimit(relaxationLimit
);
1728 if(!d_guessedCoeffSet
){
1729 d_guessedCoeffs
= approxSolver
->heuristicOptCoeffs();
1730 d_guessedCoeffSet
= true;
1732 if(!d_guessedCoeffs
.empty()){
1733 approxSolver
->setOptCoeffs(d_guessedCoeffs
);
1736 ApproximateSimplex::ApproxResult relaxRes
, mipRes
;
1737 ApproximateSimplex::Solution relaxSolution
, mipSolution
;
1738 relaxRes
= approxSolver
->solveRelaxation();
1740 case ApproximateSimplex::ApproxSat
:
1742 relaxSolution
= approxSolver
->extractRelaxation();
1744 if(d_likelyIntegerInfeasible
){
1745 d_qflraStatus
= d_attemptSolSimplex
.attempt(relaxSolution
);
1747 approxSolver
->setPivotLimit(mipLimit
);
1748 mipRes
= approxSolver
->solveMIP();
1749 d_errorSet
.reduceToSignals();
1750 //Message() << "here" << endl;
1751 if(mipRes
== ApproximateSimplex::ApproxSat
){
1752 mipSolution
= approxSolver
->extractMIP();
1753 d_qflraStatus
= d_attemptSolSimplex
.attempt(mipSolution
);
1755 if(mipRes
== ApproximateSimplex::ApproxUnsat
){
1756 d_likelyIntegerInfeasible
= true;
1758 d_qflraStatus
= d_attemptSolSimplex
.attempt(relaxSolution
);
1761 options::arithStandardCheckVarOrderPivots
.set(pass2Limit
);
1762 if(d_qflraStatus
!= Result::UNSAT
){ d_qflraStatus
= simplex
.findModel(false); }
1763 //Message() << "done" << endl;
1766 case ApproximateSimplex::ApproxUnsat
:
1768 ApproximateSimplex::Solution sol
= approxSolver
->extractRelaxation();
1770 d_qflraStatus
= d_attemptSolSimplex
.attempt(sol
);
1771 options::arithStandardCheckVarOrderPivots
.set(pass2Limit
);
1773 if(d_qflraStatus
!= Result::UNSAT
){ d_qflraStatus
= simplex
.findModel(false); }
1779 delete approxSolver
;
1782 if(d_qflraStatus
== Result::SAT_UNKNOWN
){
1783 //Message() << "got sat unknown" << endl;
1784 vector
<ArithVar
> toCut
= cutAllBounded();
1785 if(toCut
.size() > 0){
1786 branchVector(toCut
);
1787 emmittedConflictOrSplit
= true;
1789 //Message() << "splitting" << endl;
1791 d_qflraStatus
= simplex
.findModel(noPivotLimit
);
1794 options::arithStandardCheckVarOrderPivots
.set(oldCap
);
1797 // TODO Save zeroes with no conflicts
1798 d_linEq
.stopTrackingBoundCounts();
1799 d_partialModel
.startQueueingBoundCounts();
1801 return emmittedConflictOrSplit
;
1804 void TheoryArithPrivate::check(Theory::Effort effortLevel
){
1805 Assert(d_currentPropagationList
.empty());
1806 Debug("effortlevel") << "TheoryArithPrivate::check " << effortLevel
<< std::endl
;
1807 Debug("arith") << "TheoryArithPrivate::check begun " << effortLevel
<< std::endl
;
1809 if(Debug
.isOn("arith::consistency")){
1810 Assert(unenqueuedVariablesAreConsistent());
1813 bool newFacts
= !done();
1814 //If previous == SAT, then reverts on conflicts are safe
1815 //Otherwise, they are not and must be committed.
1816 Result::Sat previous
= d_qflraStatus
;
1818 d_qflraStatus
= Result::SAT_UNKNOWN
;
1819 d_hasDoneWorkSinceCut
= true;
1823 Constraint curr
= constraintFromFactQueue();
1824 if(curr
!= NullConstraint
){
1825 bool res CVC4_UNUSED
= assertionCases(curr
);
1826 Assert(!res
|| inConflict());
1828 if(inConflict()){ break; }
1831 while(!d_learnedBounds
.empty()){
1832 // we may attempt some constraints twice. this is okay!
1833 Constraint curr
= d_learnedBounds
.front();
1834 d_learnedBounds
.pop();
1835 Debug("arith::learned") << curr
<< endl
;
1837 bool res CVC4_UNUSED
= assertionCases(curr
);
1838 Assert(!res
|| inConflict());
1840 if(inConflict()){ break; }
1845 d_qflraStatus
= Result::UNSAT
;
1846 if(options::revertArithModels() && previous
== Result::SAT
){
1847 ++d_statistics
.d_revertsOnConflicts
;
1848 Debug("arith::bt") << "clearing here " << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1849 revertOutOfConflict();
1852 ++d_statistics
.d_commitsOnConflicts
;
1853 Debug("arith::bt") << "committing here " << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1854 d_partialModel
.commitAssignmentChanges();
1855 revertOutOfConflict();
1862 if(Debug
.isOn("arith::print_assertions")) {
1863 debugPrintAssertions(Debug("arith::print_assertions"));
1866 bool emmittedConflictOrSplit
= false;
1867 Assert(d_conflicts
.empty());
1869 bool useSimplex
= d_qflraStatus
!= Result::SAT
;
1871 emmittedConflictOrSplit
= solveRealRelaxation(effortLevel
);
1874 switch(d_qflraStatus
){
1877 ++d_statistics
.d_nontrivialSatChecks
;
1880 Debug("arith::bt") << "committing sap inConflit" << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1881 d_partialModel
.commitAssignmentChanges();
1882 d_unknownsInARow
= 0;
1883 if(Debug
.isOn("arith::consistency")){
1884 Assert(entireStateIsConsistent("sat comit"));
1886 if(useSimplex
&& options::collectPivots()){
1887 if(options::useFC()){
1888 d_statistics
.d_satPivots
<< d_fcSimplex
.getPivots();
1890 d_statistics
.d_satPivots
<< d_dualSimplex
.getPivots();
1894 case Result::SAT_UNKNOWN
:
1896 ++(d_statistics
.d_unknownChecks
);
1897 Assert(!Theory::fullEffort(effortLevel
));
1898 Debug("arith::bt") << "committing unknown" << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1899 d_partialModel
.commitAssignmentChanges();
1900 d_statistics
.d_maxUnknownsInARow
.maxAssign(d_unknownsInARow
);
1902 if(useSimplex
&& options::collectPivots()){
1903 if(options::useFC()){
1904 d_statistics
.d_unknownPivots
<< d_fcSimplex
.getPivots();
1906 d_statistics
.d_unknownPivots
<< d_dualSimplex
.getPivots();
1911 d_unknownsInARow
= 0;
1912 if(false && previous
== Result::SAT
){
1913 ++d_statistics
.d_revertsOnConflicts
;
1914 Debug("arith::bt") << "clearing on conflict" << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1915 revertOutOfConflict();
1918 ++d_statistics
.d_commitsOnConflicts
;
1920 Debug("arith::bt") << "committing on conflict" << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1921 d_partialModel
.commitAssignmentChanges();
1922 revertOutOfConflict();
1924 if(Debug
.isOn("arith::consistency::comitonconflict")){
1925 entireStateIsConsistent("commit on conflict");
1929 emmittedConflictOrSplit
= true;
1931 if(useSimplex
&& options::collectPivots()){
1932 if(options::useFC()){
1933 d_statistics
.d_unsatPivots
<< d_fcSimplex
.getPivots();
1935 d_statistics
.d_unsatPivots
<< d_dualSimplex
.getPivots();
1942 d_statistics
.d_avgUnknownsInARow
.addEntry(d_unknownsInARow
);
1944 // This should be fine if sat or unknown
1945 if(!emmittedConflictOrSplit
&&
1946 (options::arithPropagationMode() == UNATE_PROP
||
1947 options::arithPropagationMode() == BOTH_PROP
)){
1948 TimerStat::CodeTimer
codeTimer(d_statistics
.d_newPropTime
);
1949 Assert(d_qflraStatus
!= Result::UNSAT
);
1951 while(!d_currentPropagationList
.empty() && !inConflict()){
1952 Constraint curr
= d_currentPropagationList
.front();
1953 d_currentPropagationList
.pop_front();
1955 ConstraintType t
= curr
->getType();
1956 Assert(t
!= Disequality
, "Disequalities are not allowed in d_currentPropagation");
1962 Constraint prev
= d_currentPropagationList
.front();
1963 d_currentPropagationList
.pop_front();
1964 d_constraintDatabase
.unatePropLowerBound(curr
, prev
);
1969 Constraint prev
= d_currentPropagationList
.front();
1970 d_currentPropagationList
.pop_front();
1971 d_constraintDatabase
.unatePropUpperBound(curr
, prev
);
1976 Constraint prevLB
= d_currentPropagationList
.front();
1977 d_currentPropagationList
.pop_front();
1978 Constraint prevUB
= d_currentPropagationList
.front();
1979 d_currentPropagationList
.pop_front();
1980 d_constraintDatabase
.unatePropEquality(curr
, prevLB
, prevUB
);
1984 Unhandled(curr
->getType());
1989 Debug("arith::unate") << "unate conflict" << endl
;
1990 revertOutOfConflict();
1991 d_qflraStatus
= Result::UNSAT
;
1993 emmittedConflictOrSplit
= true;
1994 Debug("arith::bt") << "committing on unate conflict" << " " << newFacts
<< " " << previous
<< " " << d_qflraStatus
<< endl
;
1998 TimerStat::CodeTimer
codeTimer(d_statistics
.d_newPropTime
);
1999 d_currentPropagationList
.clear();
2001 Assert( d_currentPropagationList
.empty());
2003 if(!emmittedConflictOrSplit
&& Theory::fullEffort(effortLevel
)){
2004 ++d_fullCheckCounter
;
2006 if(!emmittedConflictOrSplit
&& Theory::fullEffort(effortLevel
)){
2007 emmittedConflictOrSplit
= splitDisequalities();
2010 if(!emmittedConflictOrSplit
&& Theory::fullEffort(effortLevel
) && !hasIntegerModel()){
2011 Node possibleConflict
= Node::null();
2012 if(!emmittedConflictOrSplit
&& options::arithDioSolver()){
2013 possibleConflict
= callDioSolver();
2014 if(possibleConflict
!= Node::null()){
2015 revertOutOfConflict();
2016 Debug("arith::conflict") << "dio conflict " << possibleConflict
<< endl
;
2017 //cout << "dio conflict " << possibleConflict << endl;
2018 raiseConflict(possibleConflict
);
2020 emmittedConflictOrSplit
= true;
2024 if(!emmittedConflictOrSplit
&& d_hasDoneWorkSinceCut
&& options::arithDioSolver()){
2025 Node possibleLemma
= dioCutting();
2026 if(!possibleLemma
.isNull()){
2027 Debug("arith") << "dio cut " << possibleLemma
<< endl
;
2028 //cout << "dio cut " << possibleLemma << endl;
2029 emmittedConflictOrSplit
= true;
2030 d_hasDoneWorkSinceCut
= false;
2031 d_cutCount
= d_cutCount
+ 1;
2032 outputLemma(possibleLemma
);
2036 if(!emmittedConflictOrSplit
) {
2037 Node possibleLemma
= roundRobinBranch();
2038 if(!possibleLemma
.isNull()){
2039 ++(d_statistics
.d_externalBranchAndBounds
);
2040 d_cutCount
= d_cutCount
+ 1;
2041 emmittedConflictOrSplit
= true;
2042 outputLemma(possibleLemma
);
2046 if(options::maxCutsInContext() <= d_cutCount
){
2047 if(d_diosolver
.hasMoreDecompositionLemmas()){
2048 while(d_diosolver
.hasMoreDecompositionLemmas()){
2049 Node decompositionLemma
= d_diosolver
.nextDecompositionLemma();
2050 Debug("arith") << "dio decomposition lemma " << decompositionLemma
<< endl
;
2051 outputLemma(decompositionLemma
);
2057 }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
2058 if(Theory::fullEffort(effortLevel
) && d_nlIncomplete
){
2059 // TODO this is total paranoia
2063 if(Debug
.isOn("paranoid:check_tableau")){ d_linEq
.debugCheckTableau(); }
2064 if(Debug
.isOn("arith::print_model")) {
2065 debugPrintModel(Debug("arith::print_model"));
2067 Debug("arith") << "TheoryArithPrivate::check end" << std::endl
;
2070 Node
TheoryArithPrivate::branchIntegerVariable(ArithVar x
) const {
2071 const DeltaRational
& d
= d_partialModel
.getAssignment(x
);
2072 Assert(!d
.isIntegral());
2073 const Rational
& r
= d
.getNoninfinitesimalPart();
2074 const Rational
& i
= d
.getInfinitesimalPart();
2075 Trace("integers") << "integers: assignment to [[" << d_partialModel
.asNode(x
) << "]] is " << r
<< "[" << i
<< "]" << endl
;
2077 Assert(! (r
.getDenominator() == 1 && i
.getNumerator() == 0));
2078 Assert(!d
.isIntegral());
2079 TNode var
= d_partialModel
.asNode(x
);
2080 Integer floor_d
= d
.floor();
2082 //Node eq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, var, mkRationalNode(floor_d+1)));
2083 //Node diseq = eq.notNode();
2085 Node ub
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ
, var
, mkRationalNode(floor_d
)));
2086 Node lb
= ub
.notNode();
2089 //Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, diseq);
2090 Node lem
= NodeManager::currentNM()->mkNode(kind::OR
, ub
, lb
);
2091 Trace("integers") << "integers: branch & bound: " << lem
<< endl
;
2092 if(isSatLiteral(lem
[0])) {
2093 Debug("integers") << " " << lem
[0] << " == " << getSatValue(lem
[0]) << endl
;
2095 Debug("integers") << " " << lem
[0] << " is not assigned a SAT literal" << endl
;
2097 if(isSatLiteral(lem
[1])) {
2098 Debug("integers") << " " << lem
[1] << " == " << getSatValue(lem
[1]) << endl
;
2100 Debug("integers") << " " << lem
[1] << " is not assigned a SAT literal" << endl
;
2105 std::vector
<ArithVar
> TheoryArithPrivate::cutAllBounded() const{
2106 vector
<ArithVar
> lemmas
;
2107 ArithVar max
= d_partialModel
.getNumberOfVariables();
2109 if(options::doCutAllBounded() && max
> 0){
2110 for(ArithVar iter
= 0; iter
!= max
; ++iter
){
2111 //Do not include slack variables
2112 const DeltaRational
& d
= d_partialModel
.getAssignment(iter
);
2113 if(isInteger(iter
) && !isSlackVariable(iter
) &&
2114 !d_cutInContext
.contains(iter
) &&
2115 d_partialModel
.hasUpperBound(iter
) &&
2116 d_partialModel
.hasLowerBound(iter
) &&
2118 lemmas
.push_back(iter
);
2125 /** Returns true if the roundRobinBranching() issues a lemma. */
2126 Node
TheoryArithPrivate::roundRobinBranch(){
2127 if(hasIntegerModel()){
2128 return Node::null();
2130 ArithVar v
= d_nextIntegerCheckVar
;
2132 Assert(isInteger(v
));
2133 Assert(!isSlackVariable(v
));
2134 return branchIntegerVariable(v
);
2138 bool TheoryArithPrivate::splitDisequalities(){
2139 bool splitSomething
= false;
2141 vector
<Constraint
> save
;
2143 while(!d_diseqQueue
.empty()){
2144 Constraint front
= d_diseqQueue
.front();
2147 if(front
->isSplit()){
2148 Debug("eq") << "split already" << endl
;
2150 Debug("eq") << "not split already" << endl
;
2152 ArithVar lhsVar
= front
->getVariable();
2154 const DeltaRational
& lhsValue
= d_partialModel
.getAssignment(lhsVar
);
2155 const DeltaRational
& rhsValue
= front
->getValue();
2156 if(lhsValue
== rhsValue
){
2157 Debug("arith::lemma") << "Splitting on " << front
<< endl
;
2158 Debug("arith::lemma") << "LHS value = " << lhsValue
<< endl
;
2159 Debug("arith::lemma") << "RHS value = " << rhsValue
<< endl
;
2160 Node lemma
= front
->split();
2161 ++(d_statistics
.d_statDisequalitySplits
);
2163 Debug("arith::lemma") << "Now " << Rewriter::rewrite(lemma
) << endl
;
2165 splitSomething
= true;
2166 }else if(d_partialModel
.strictlyLessThanLowerBound(lhsVar
, rhsValue
)){
2167 Debug("eq") << "can drop as less than lb" << front
<< endl
;
2168 }else if(d_partialModel
.strictlyGreaterThanUpperBound(lhsVar
, rhsValue
)){
2169 Debug("eq") << "can drop as greater than ub" << front
<< endl
;
2171 Debug("eq") << "save" << front
<< ": " <<lhsValue
<< " != " << rhsValue
<< endl
;
2172 save
.push_back(front
);
2176 vector
<Constraint
>::const_iterator i
=save
.begin(), i_end
= save
.end();
2177 for(; i
!= i_end
; ++i
){
2178 d_diseqQueue
.push(*i
);
2180 return splitSomething
;
2184 * Should be guarded by at least Debug.isOn("arith::print_assertions").
2185 * Prints to Debug("arith::print_assertions")
2187 void TheoryArithPrivate::debugPrintAssertions(std::ostream
& out
) const {
2188 out
<< "Assertions:" << endl
;
2189 for (var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
2191 if (d_partialModel
.hasLowerBound(i
)) {
2192 Constraint lConstr
= d_partialModel
.getLowerBoundConstraint(i
);
2193 out
<< lConstr
<< endl
;
2196 if (d_partialModel
.hasUpperBound(i
)) {
2197 Constraint uConstr
= d_partialModel
.getUpperBoundConstraint(i
);
2198 out
<< uConstr
<< endl
;
2201 context::CDQueue
<Constraint
>::const_iterator it
= d_diseqQueue
.begin();
2202 context::CDQueue
<Constraint
>::const_iterator it_end
= d_diseqQueue
.end();
2203 for(; it
!= it_end
; ++ it
) {
2208 void TheoryArithPrivate::debugPrintModel(std::ostream
& out
) const{
2209 out
<< "Model:" << endl
;
2210 for (var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
2212 if(d_partialModel
.hasNode(i
)){
2213 out
<< d_partialModel
.asNode(i
) << " : " <<
2214 d_partialModel
.getAssignment(i
);
2215 if(d_tableau
.isBasic(i
)){
2225 Node
TheoryArithPrivate::explain(TNode n
) {
2227 Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n
<< endl
;
2229 Constraint c
= d_constraintDatabase
.lookup(n
);
2230 if(c
!= NullConstraint
){
2231 Assert(!c
->isSelfExplaining());
2232 Node exp
= c
->explainForPropagation();
2233 Debug("arith::explain") << "constraint explanation" << n
<< ":" << exp
<< endl
;
2235 }else if(d_assertionsThatDoNotMatchTheirLiterals
.find(n
) != d_assertionsThatDoNotMatchTheirLiterals
.end()){
2236 c
= d_assertionsThatDoNotMatchTheirLiterals
[n
];
2237 if(!c
->isSelfExplaining()){
2238 Node exp
= c
->explainForPropagation();
2239 Debug("arith::explain") << "assertions explanation" << n
<< ":" << exp
<< endl
;
2242 Debug("arith::explain") << "this is a strange mismatch" << n
<< endl
;
2243 Assert(d_congruenceManager
.canExplain(n
));
2244 Debug("arith::explain") << "this is a strange mismatch" << n
<< endl
;
2245 return d_congruenceManager
.explain(n
);
2248 Assert(d_congruenceManager
.canExplain(n
));
2249 Debug("arith::explain") << "dm explanation" << n
<< endl
;
2250 return d_congruenceManager
.explain(n
);
2255 void TheoryArithPrivate::propagate(Theory::Effort e
) {
2256 // This uses model values for safety. Disable for now.
2257 if(d_qflraStatus
== Result::SAT
&&
2258 (options::arithPropagationMode() == BOUND_INFERENCE_PROP
||
2259 options::arithPropagationMode() == BOTH_PROP
)
2260 && hasAnyUpdates()){
2261 if(options::newProp()){
2262 propagateCandidatesNew();
2264 propagateCandidates();
2270 while(d_constraintDatabase
.hasMorePropagations()){
2271 Constraint c
= d_constraintDatabase
.nextPropagation();
2272 Debug("arith::prop") << "next prop" << getSatContext()->getLevel() << ": " << c
<< endl
;
2274 if(c
->negationHasProof()){
2275 Debug("arith::prop") << "negation has proof " << c
->getNegation() << endl
2276 << c
->getNegation()->explainForConflict() << endl
;
2278 Assert(!c
->negationHasProof(), "A constraint has been propagated on the constraint propagation queue, but the negation has been set to true. Contact Tim now!");
2280 if(!c
->assertedToTheTheory()){
2281 Node literal
= c
->getLiteral();
2282 Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal
<< endl
;
2284 outputPropagate(literal
);
2286 Debug("arith::prop") << "already asserted to the theory " << c
->getLiteral() << endl
;
2290 while(d_congruenceManager
.hasMorePropagations()){
2291 TNode toProp
= d_congruenceManager
.getNextPropagation();
2293 //Currently if the flag is set this came from an equality detected by the
2294 //equality engine in the the difference manager.
2295 Node normalized
= Rewriter::rewrite(toProp
);
2297 Constraint constraint
= d_constraintDatabase
.lookup(normalized
);
2298 if(constraint
== NullConstraint
){
2299 Debug("arith::prop") << "propagating on non-constraint? " << toProp
<< endl
;
2301 outputPropagate(toProp
);
2302 }else if(constraint
->negationHasProof()){
2303 Node exp
= d_congruenceManager
.explain(toProp
);
2304 Node notNormalized
= normalized
.getKind() == NOT
?
2305 normalized
[0] : normalized
.notNode();
2306 Node lp
= flattenAnd(exp
.andNode(notNormalized
));
2307 Debug("arith::prop") << "propagate conflict" << lp
<< endl
;
2312 Debug("arith::prop") << "propagating still?" << toProp
<< endl
;
2313 outputPropagate(toProp
);
2318 DeltaRational
TheoryArithPrivate::getDeltaValue(TNode n
) const throw (DeltaRationalException
, ModelException
) {
2319 AlwaysAssert(d_qflraStatus
!= Result::SAT_UNKNOWN
);
2320 Debug("arith::value") << n
<< std::endl
;
2322 switch(n
.getKind()) {
2324 case kind::CONST_RATIONAL
:
2325 return n
.getConst
<Rational
>();
2327 case kind::PLUS
: { // 2+ args
2328 DeltaRational
value(0);
2329 for(TNode::iterator i
= n
.begin(), iend
= n
.end(); i
!= iend
; ++i
) {
2330 value
= value
+ getDeltaValue(*i
);
2335 case kind::MULT
: { // 2+ args
2336 DeltaRational
value(1);
2337 unsigned variableParts
= 0;
2338 for(TNode::iterator i
= n
.begin(), iend
= n
.end(); i
!= iend
; ++i
) {
2340 value
= value
* getDeltaValue(curr
);
2341 if(!curr
.isConst()){
2345 // TODO: This is a bit of a weak check
2347 ArithVar var
= d_partialModel
.asArithVar(n
);
2348 const DeltaRational
& assign
= d_partialModel
.getAssignment(var
);
2349 if(assign
!= value
){
2350 throw ModelException(n
, "Model disagrees on non-linear term.");
2355 case kind::MINUS
:{ // 2 args
2356 return getDeltaValue(n
[0]) - getDeltaValue(n
[1]);
2359 case kind::UMINUS
:{ // 1 arg
2360 return (- getDeltaValue(n
[0]));
2363 case kind::DIVISION
:{ // 2 args
2364 DeltaRational res
= getDeltaValue(n
[0]) / getDeltaValue(n
[1]);
2366 ArithVar var
= d_partialModel
.asArithVar(n
);
2367 if(d_partialModel
.getAssignment(var
) != res
){
2368 throw ModelException(n
, "Model disagrees on non-linear term.");
2373 case kind::DIVISION_TOTAL
:
2374 case kind::INTS_DIVISION_TOTAL
:
2375 case kind::INTS_MODULUS_TOTAL
: { // 2 args
2376 DeltaRational denom
= getDeltaValue(n
[1]);
2378 return DeltaRational(0,0);
2380 DeltaRational numer
= getDeltaValue(n
[0]);
2382 if(n
.getKind() == kind::DIVISION_TOTAL
){
2383 res
= numer
/ denom
;
2384 }else if(n
.getKind() == kind::INTS_DIVISION_TOTAL
){
2385 res
= Rational(numer
.euclidianDivideQuotient(denom
));
2387 Assert(n
.getKind() == kind::INTS_MODULUS_TOTAL
);
2388 res
= Rational(numer
.euclidianDivideRemainder(denom
));
2391 ArithVar var
= d_partialModel
.asArithVar(n
);
2392 if(d_partialModel
.getAssignment(var
) != res
){
2393 throw ModelException(n
, "Model disagrees on non-linear term.");
2402 ArithVar var
= d_partialModel
.asArithVar(n
);
2403 return d_partialModel
.getAssignment(var
);
2405 throw ModelException(n
, "Expected a setup node.");
2410 Rational
TheoryArithPrivate::deltaValueForTotalOrder() const{
2412 std::set
<DeltaRational
> relevantDeltaValues
;
2413 context::CDQueue
<Constraint
>::const_iterator qiter
= d_diseqQueue
.begin();
2414 context::CDQueue
<Constraint
>::const_iterator qiter_end
= d_diseqQueue
.end();
2416 for(; qiter
!= qiter_end
; ++qiter
){
2417 Constraint curr
= *qiter
;
2419 const DeltaRational
& rhsValue
= curr
->getValue();
2420 relevantDeltaValues
.insert(rhsValue
);
2423 Theory::shared_terms_iterator shared_iter
= d_containing
.shared_terms_begin();
2424 Theory::shared_terms_iterator shared_end
= d_containing
.shared_terms_end();
2425 for(; shared_iter
!= shared_end
; ++shared_iter
){
2426 Node sharedCurr
= *shared_iter
;
2428 // ModelException is fatal as this point. Don't catch!
2429 // DeltaRationalException is fatal as this point. Don't catch!
2430 DeltaRational val
= getDeltaValue(sharedCurr
);
2431 relevantDeltaValues
.insert(val
);
2434 for(var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
2436 const DeltaRational
& value
= d_partialModel
.getAssignment(v
);
2437 relevantDeltaValues
.insert(value
);
2438 if( d_partialModel
.hasLowerBound(v
)){
2439 const DeltaRational
& lb
= d_partialModel
.getLowerBound(v
);
2440 relevantDeltaValues
.insert(lb
);
2442 if( d_partialModel
.hasUpperBound(v
)){
2443 const DeltaRational
& ub
= d_partialModel
.getUpperBound(v
);
2444 relevantDeltaValues
.insert(ub
);
2448 if(relevantDeltaValues
.size() >= 2){
2449 std::set
<DeltaRational
>::const_iterator iter
= relevantDeltaValues
.begin();
2450 std::set
<DeltaRational
>::const_iterator iter_end
= relevantDeltaValues
.end();
2451 DeltaRational prev
= *iter
;
2453 for(; iter
!= iter_end
; ++iter
){
2454 const DeltaRational
& curr
= *iter
;
2456 Assert(prev
< curr
);
2458 DeltaRational::seperatingDelta(min
, prev
, curr
);
2463 Assert(min
.sgn() > 0);
2464 Rational belowMin
= min
/Rational(2);
2468 void TheoryArithPrivate::collectModelInfo( TheoryModel
* m
, bool fullModel
){
2469 AlwaysAssert(d_qflraStatus
== Result::SAT
);
2470 //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
2472 if(Debug
.isOn("arith::collectModelInfo")){
2476 Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl
;
2479 // Delta lasts at least the duration of the function call
2480 const Rational
& delta
= d_partialModel
.getDelta();
2481 std::hash_set
<TNode
, TNodeHashFunction
> shared
= d_containing
.currentlySharedTerms();
2484 // This is not very good for user push/pop....
2485 // Revisit when implementing push/pop
2486 for(var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
2489 if(!isSlackVariable(v
)){
2490 Node term
= d_partialModel
.asNode(v
);
2492 if(theoryOf(term
) == THEORY_ARITH
|| shared
.find(term
) != shared
.end()){
2493 const DeltaRational
& mod
= d_partialModel
.getAssignment(v
);
2494 Rational qmodel
= mod
.substituteDelta(delta
);
2496 Node qNode
= mkRationalNode(qmodel
);
2497 Debug("arith::collectModelInfo") << "m->assertEquality(" << term
<< ", " << qmodel
<< ", true)" << endl
;
2499 m
->assertEquality(term
, qNode
, true);
2501 Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term
<< ", true)" << endl
;
2507 // Iterate over equivalence classes in LinearEqualityModule
2508 // const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine();
2509 // m->assertEqualityEngine(&ee);
2511 Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl
;
2514 bool TheoryArithPrivate::safeToReset() const {
2515 Assert(!d_tableauSizeHasBeenModified
);
2516 Assert(d_errorSet
.noSignals());
2518 ErrorSet::error_iterator error_iter
= d_errorSet
.errorBegin();
2519 ErrorSet::error_iterator error_end
= d_errorSet
.errorEnd();
2520 for(; error_iter
!= error_end
; ++error_iter
){
2521 ArithVar basic
= *error_iter
;
2522 if(!d_smallTableauCopy
.isBasic(basic
)){
2530 void TheoryArithPrivate::notifyRestart(){
2531 TimerStat::CodeTimer
codeTimer(d_statistics
.d_restartTimer
);
2533 if(Debug
.isOn("paranoid:check_tableau")){ d_linEq
.debugCheckTableau(); }
2535 ++d_restartsCounter
;
2538 bool TheoryArithPrivate::entireStateIsConsistent(const string
& s
){
2540 for(var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
2542 //ArithVar var = d_partialModel.asArithVar(*i);
2543 if(!d_partialModel
.assignmentIsConsistent(var
)){
2544 d_partialModel
.printModel(var
);
2545 Warning() << s
<< ":" << "Assignment is not consistent for " << var
<< d_partialModel
.asNode(var
);
2546 if(d_tableau
.isBasic(var
)){
2547 Warning() << " (basic)";
2551 }else if(d_partialModel
.isInteger(var
) && !d_partialModel
.integralAssignment(var
)){
2552 d_partialModel
.printModel(var
);
2553 Warning() << s
<< ":" << "Assignment is not integer for integer variable " << var
<< d_partialModel
.asNode(var
);
2554 if(d_tableau
.isBasic(var
)){
2555 Warning() << " (basic)";
2564 bool TheoryArithPrivate::unenqueuedVariablesAreConsistent(){
2566 for(var_iterator vi
= var_begin(), vend
= var_end(); vi
!= vend
; ++vi
){
2568 if(!d_partialModel
.assignmentIsConsistent(var
)){
2569 if(!d_errorSet
.inError(var
)){
2571 d_partialModel
.printModel(var
);
2572 Warning() << "Unenqueued var is not consistent for " << var
<< d_partialModel
.asNode(var
);
2573 if(d_tableau
.isBasic(var
)){
2574 Warning() << " (basic)";
2578 } else if(Debug
.isOn("arith::consistency::initial")){
2579 d_partialModel
.printModel(var
);
2580 Warning() << "Initial var is not consistent for " << var
<< d_partialModel
.asNode(var
);
2581 if(d_tableau
.isBasic(var
)){
2582 Warning() << " (basic)";
2591 void TheoryArithPrivate::presolve(){
2592 TimerStat::CodeTimer
codeTimer(d_statistics
.d_presolveTime
);
2594 d_statistics
.d_initialTableauSize
.setData(d_tableau
.size());
2596 if(Debug
.isOn("paranoid:check_tableau")){ d_linEq
.debugCheckTableau(); }
2598 static CVC4_THREADLOCAL(unsigned) callCount
= 0;
2599 if(Debug
.isOn("arith::presolve")) {
2600 Debug("arith::presolve") << "TheoryArithPrivate::presolve #" << callCount
<< endl
;
2601 callCount
= callCount
+ 1;
2604 vector
<Node
> lemmas
;
2605 switch(options::arithUnateLemmaMode()){
2606 case NO_PRESOLVE_LEMMAS
:
2608 case INEQUALITY_PRESOLVE_LEMMAS
:
2609 d_constraintDatabase
.outputUnateInequalityLemmas(lemmas
);
2611 case EQUALITY_PRESOLVE_LEMMAS
:
2612 d_constraintDatabase
.outputUnateEqualityLemmas(lemmas
);
2614 case ALL_PRESOLVE_LEMMAS
:
2615 d_constraintDatabase
.outputUnateInequalityLemmas(lemmas
);
2616 d_constraintDatabase
.outputUnateEqualityLemmas(lemmas
);
2619 Unhandled(options::arithUnateLemmaMode());
2622 vector
<Node
>::const_iterator i
= lemmas
.begin(), i_end
= lemmas
.end();
2623 for(; i
!= i_end
; ++i
){
2625 Debug("arith::oldprop") << " lemma lemma duck " <<lem
<< endl
;
2630 EqualityStatus
TheoryArithPrivate::getEqualityStatus(TNode a
, TNode b
) {
2631 if(d_qflraStatus
== Result::SAT_UNKNOWN
){
2632 return EQUALITY_UNKNOWN
;
2635 if (getDeltaValue(a
) == getDeltaValue(b
)) {
2636 return EQUALITY_TRUE_IN_MODEL
;
2638 return EQUALITY_FALSE_IN_MODEL
;
2640 } catch (DeltaRationalException
& dr
) {
2641 return EQUALITY_UNKNOWN
;
2642 } catch (ModelException
& me
) {
2643 return EQUALITY_UNKNOWN
;
2648 bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic
, bool upperBound
){
2649 ++d_statistics
.d_boundComputations
;
2651 RowIndex ridx
= d_tableau
.basicToRowIndex(basic
);
2652 DeltaRational bound
= d_linEq
.computeRowBound(ridx
, upperBound
, basic
);
2654 if((upperBound
&& d_partialModel
.strictlyLessThanUpperBound(basic
, bound
)) ||
2655 (!upperBound
&& d_partialModel
.strictlyGreaterThanLowerBound(basic
, bound
))){
2657 // TODO: "Policy point"
2658 //We are only going to recreate the functionality for now.
2659 //In the future this can be improved to generate a temporary constraint
2661 //Experiment with doing this everytime or only when the new constraint
2662 //implies an unknown fact.
2664 ConstraintType t
= upperBound
? UpperBound
: LowerBound
;
2665 Constraint bestImplied
= d_constraintDatabase
.getBestImpliedBound(basic
, t
, bound
);
2667 // Node bestImplied = upperBound ?
2668 // d_apm.getBestImpliedUpperBound(basic, bound):
2669 // d_apm.getBestImpliedLowerBound(basic, bound);
2671 if(bestImplied
!= NullConstraint
){
2672 //This should be stronger
2673 Assert(!upperBound
|| bound
<= bestImplied
->getValue());
2674 Assert(!upperBound
|| d_partialModel
.lessThanUpperBound(basic
, bestImplied
->getValue()));
2676 Assert( upperBound
|| bound
>= bestImplied
->getValue());
2677 Assert( upperBound
|| d_partialModel
.greaterThanLowerBound(basic
, bestImplied
->getValue()));
2680 // Constraint c = d_constraintDatabase.lookup(bestImplied);
2681 // Assert(c != NullConstraint);
2683 bool assertedToTheTheory
= bestImplied
->assertedToTheTheory();
2684 bool canBePropagated
= bestImplied
->canBePropagated();
2685 bool hasProof
= bestImplied
->hasProof();
2687 Debug("arith::prop") << "arith::prop" << basic
2688 << " " << assertedToTheTheory
2689 << " " << canBePropagated
2693 if(bestImplied
->negationHasProof()){
2694 Warning() << "the negation of " << bestImplied
<< " : " << endl
2695 << "has proof " << bestImplied
->getNegation() << endl
2696 << bestImplied
->getNegation()->explainForConflict() << endl
;
2699 if(!assertedToTheTheory
&& canBePropagated
&& !hasProof
){
2700 d_linEq
.propagateBasicFromRow(bestImplied
);
2701 // I think this can be skipped if canBePropagated is true
2702 //d_learnedBounds.push(bestImplied);
2703 if(Debug
.isOn("arith::prop")){
2704 Debug("arith::prop") << "success " << bestImplied
<< endl
;
2705 d_partialModel
.printModel(basic
, Debug("arith::prop"));
2709 if(Debug
.isOn("arith::prop")){
2710 Debug("arith::prop") << "failed " << basic
<< " " << bound
<< assertedToTheTheory
<< " " <<
2711 canBePropagated
<< " " << hasProof
<< endl
;
2712 d_partialModel
.printModel(basic
, Debug("arith::prop"));
2715 }else if(Debug
.isOn("arith::prop")){
2716 Debug("arith::prop") << "false " << bound
<< " ";
2717 d_partialModel
.printModel(basic
, Debug("arith::prop"));
2722 void TheoryArithPrivate::propagateCandidate(ArithVar basic
){
2723 bool success
= false;
2724 RowIndex ridx
= d_tableau
.basicToRowIndex(basic
);
2726 bool tryLowerBound
=
2727 d_partialModel
.strictlyAboveLowerBound(basic
) &&
2728 d_linEq
.rowLacksBound(ridx
, false, basic
) == NULL
;
2730 bool tryUpperBound
=
2731 d_partialModel
.strictlyBelowUpperBound(basic
) &&
2732 d_linEq
.rowLacksBound(ridx
, true, basic
) == NULL
;
2735 success
|= propagateCandidateLowerBound(basic
);
2738 success
|= propagateCandidateUpperBound(basic
);
2741 ++d_statistics
.d_boundPropagations
;
2745 void TheoryArithPrivate::propagateCandidates(){
2746 TimerStat::CodeTimer
codeTimer(d_statistics
.d_boundComputationTime
);
2748 Debug("arith::prop") << "propagateCandidates begin" << endl
;
2750 Assert(d_candidateBasics
.empty());
2752 if(d_updatedBounds
.empty()){ return; }
2754 DenseSet::const_iterator i
= d_updatedBounds
.begin();
2755 DenseSet::const_iterator end
= d_updatedBounds
.end();
2756 for(; i
!= end
; ++i
){
2758 if(d_tableau
.isBasic(var
) &&
2759 d_tableau
.basicRowLength(var
) <= options::arithPropagateMaxLength()){
2760 d_candidateBasics
.softAdd(var
);
2762 Tableau::ColIterator basicIter
= d_tableau
.colIterator(var
);
2763 for(; !basicIter
.atEnd(); ++basicIter
){
2764 const Tableau::Entry
& entry
= *basicIter
;
2765 RowIndex ridx
= entry
.getRowIndex();
2766 ArithVar rowVar
= d_tableau
.rowIndexToBasic(ridx
);
2767 Assert(entry
.getColVar() == var
);
2768 Assert(d_tableau
.isBasic(rowVar
));
2769 if(d_tableau
.getRowLength(ridx
) <= options::arithPropagateMaxLength()){
2770 d_candidateBasics
.softAdd(rowVar
);
2775 d_updatedBounds
.purge();
2777 while(!d_candidateBasics
.empty()){
2778 ArithVar candidate
= d_candidateBasics
.back();
2779 d_candidateBasics
.pop_back();
2780 Assert(d_tableau
.isBasic(candidate
));
2781 propagateCandidate(candidate
);
2783 Debug("arith::prop") << "propagateCandidates end" << endl
<< endl
<< endl
;
2786 void TheoryArithPrivate::propagateCandidatesNew(){
2787 /* Four criteria must be met for progagation on a variable to happen using a row:
2788 * 0: A new bound has to have been added to the row.
2789 * 1: The hasBoundsCount for the row must be "full" or be full minus one variable
2790 * (This is O(1) to check, but requires book keeping.)
2791 * 2: The current assignment must be strictly smaller/greater than the current bound.
2792 * assign(x) < upper(x)
2793 * (This is O(1) to compute.)
2794 * 3: There is a bound that is strictly smaller/greater than the current assignment.
2795 * assign(x) < c for some x <= c literal
2796 * (This is O(log n) to compute.)
2797 * 4: The implied bound on x is strictly smaller/greater than the current bound.
2798 * (This is O(n) to compute.)
2801 TimerStat::CodeTimer
codeTimer(d_statistics
.d_boundComputationTime
);
2802 Debug("arith::prop") << "propagateCandidatesNew begin" << endl
;
2804 Assert(d_qflraStatus
== Result::SAT
);
2805 if(d_updatedBounds
.empty()){ return; }
2806 dumpUpdatedBoundsToRows();
2807 Assert(d_updatedBounds
.empty());
2809 if(!d_candidateRows
.empty()){
2810 UpdateTrackingCallback
utcb(&d_linEq
);
2811 d_partialModel
.processBoundsQueue(utcb
);
2814 while(!d_candidateRows
.empty()){
2815 RowIndex candidate
= d_candidateRows
.back();
2816 d_candidateRows
.pop_back();
2817 propagateCandidateRow(candidate
);
2819 Debug("arith::prop") << "propagateCandidatesNew end" << endl
<< endl
<< endl
;
2822 bool TheoryArithPrivate::propagateMightSucceed(ArithVar v
, bool ub
) const{
2823 int cmp
= ub
? d_partialModel
.cmpAssignmentUpperBound(v
)
2824 : d_partialModel
.cmpAssignmentLowerBound(v
);
2825 bool hasSlack
= ub
? cmp
< 0 : cmp
> 0;
2827 ConstraintType t
= ub
? UpperBound
: LowerBound
;
2828 const DeltaRational
& a
= d_partialModel
.getAssignment(v
);
2830 if(isInteger(v
) && !a
.isIntegral()){
2834 Constraint strongestPossible
= d_constraintDatabase
.getBestImpliedBound(v
, t
, a
);
2835 if(strongestPossible
== NullConstraint
){
2838 bool assertedToTheTheory
= strongestPossible
->assertedToTheTheory();
2839 bool canBePropagated
= strongestPossible
->canBePropagated();
2840 bool hasProof
= strongestPossible
->hasProof();
2842 return !assertedToTheTheory
&& canBePropagated
&& !hasProof
;
2849 bool TheoryArithPrivate::attemptSingleton(RowIndex ridx
, bool rowUp
){
2850 Debug("arith::prop") << " attemptSingleton" << ridx
;
2852 const Tableau::Entry
* ep
;
2853 ep
= d_linEq
.rowLacksBound(ridx
, rowUp
, ARITHVAR_SENTINEL
);
2856 ArithVar v
= ep
->getColVar();
2857 const Rational
& coeff
= ep
->getCoefficient();
2859 // 0 = c * v + \sum rest
2861 // - c * v = \sum rest \leq D
2862 // if c > 0, v \geq -D/c so !vUp
2863 // if c < 0, v \leq -D/c so vUp
2864 // Suppose not rowUp
2865 // - c * v = \sum rest \geq D
2866 // if c > 0, v \leq -D/c so vUp
2867 // if c < 0, v \geq -D/c so !vUp
2868 bool vUp
= (rowUp
== ( coeff
.sgn() < 0));
2870 Debug("arith::prop") << " " << rowUp
<< " " << v
<< " " << coeff
<< " " << vUp
<< endl
;
2871 Debug("arith::prop") << " " << propagateMightSucceed(v
, vUp
) << endl
;
2873 if(propagateMightSucceed(v
, vUp
)){
2874 DeltaRational dr
= d_linEq
.computeRowBound(ridx
, rowUp
, v
);
2875 DeltaRational bound
= dr
/ (- coeff
);
2876 return tryToPropagate(ridx
, rowUp
, v
, vUp
, bound
);
2881 bool TheoryArithPrivate::attemptFull(RowIndex ridx
, bool rowUp
){
2882 Debug("arith::prop") << " attemptFull" << ridx
<< endl
;
2884 vector
<const Tableau::Entry
*> candidates
;
2886 for(Tableau::RowIterator i
= d_tableau
.ridRowIterator(ridx
); !i
.atEnd(); ++i
){
2887 const Tableau::Entry
& e
=*i
;
2888 const Rational
& c
= e
.getCoefficient();
2889 ArithVar v
= e
.getColVar();
2890 bool vUp
= (rowUp
== (c
.sgn() < 0));
2891 if(propagateMightSucceed(v
, vUp
)){
2892 candidates
.push_back(&e
);
2895 if(candidates
.empty()){ return false; }
2897 const DeltaRational slack
=
2898 d_linEq
.computeRowBound(ridx
, rowUp
, ARITHVAR_SENTINEL
);
2900 vector
<const Tableau::Entry
*>::const_iterator i
, iend
;
2901 for(i
= candidates
.begin(), iend
= candidates
.end(); i
!= iend
; ++i
){
2902 const Tableau::Entry
* ep
= *i
;
2903 const Rational
& c
= ep
->getCoefficient();
2904 ArithVar v
= ep
->getColVar();
2906 // See the comment for attemptSingleton()
2907 bool activeUp
= (rowUp
== (c
.sgn() > 0));
2908 bool vUb
= (rowUp
== (c
.sgn() < 0));
2910 const DeltaRational
& activeBound
= activeUp
?
2911 d_partialModel
.getUpperBound(v
):
2912 d_partialModel
.getLowerBound(v
);
2914 DeltaRational contribution
= activeBound
* c
;
2915 DeltaRational impliedBound
= (slack
- contribution
)/(-c
);
2917 bool success
= tryToPropagate(ridx
, rowUp
, v
, vUb
, impliedBound
);
2923 bool TheoryArithPrivate::tryToPropagate(RowIndex ridx
, bool rowUp
, ArithVar v
, bool vUb
, const DeltaRational
& bound
){
2925 bool weaker
= vUb
? d_partialModel
.strictlyLessThanUpperBound(v
, bound
):
2926 d_partialModel
.strictlyGreaterThanLowerBound(v
, bound
);
2928 ConstraintType t
= vUb
? UpperBound
: LowerBound
;
2931 //cout << "maybe" << endl;
2932 //cout << bound << endl;
2934 Constraint implied
= d_constraintDatabase
.getBestImpliedBound(v
, t
, bound
);
2935 if(implied
!= NullConstraint
){
2936 return rowImplicationCanBeApplied(ridx
, rowUp
, implied
);
2942 Node
flattenImplication(Node imp
){
2943 NodeBuilder
<> nb(kind::OR
);
2945 Node right
= imp
[1];
2947 if(left
.getKind() == kind::AND
){
2948 for(Node::iterator i
= left
.begin(), iend
= left
.end(); i
!= iend
; ++i
) {
2949 nb
<< (*i
).negate();
2952 nb
<< left
.negate();
2955 if(right
.getKind() == kind::OR
){
2956 for(Node::iterator i
= right
.begin(), iend
= right
.end(); i
!= iend
; ++i
) {
2966 bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx
, bool rowUp
, Constraint implied
){
2967 Assert(implied
!= NullConstraint
);
2968 ArithVar v
= implied
->getVariable();
2970 bool assertedToTheTheory
= implied
->assertedToTheTheory();
2971 bool canBePropagated
= implied
->canBePropagated();
2972 bool hasProof
= implied
->hasProof();
2974 Debug("arith::prop") << "arith::prop" << v
2975 << " " << assertedToTheTheory
2976 << " " << canBePropagated
2980 if(implied
->negationHasProof()){
2981 Warning() << "the negation of " << implied
<< " : " << endl
2982 << "has proof " << implied
->getNegation() << endl
2983 << implied
->getNegation()->explainForConflict() << endl
;
2986 if(!assertedToTheTheory
&& canBePropagated
&& !hasProof
){
2987 vector
<Constraint
> explain
;
2988 d_linEq
.propagateRow(explain
, ridx
, rowUp
, implied
);
2989 if(d_tableau
.getRowLength(ridx
) <= options::arithPropAsLemmaLength()){
2990 Node implication
= implied
->makeImplication(explain
);
2991 Node clause
= flattenImplication(implication
);
2992 outputLemma(clause
);
2994 implied
->impliedBy(explain
);
2999 if(Debug
.isOn("arith::prop")){
3000 Debug("arith::prop")
3001 << "failed " << v
<< " " << assertedToTheTheory
<< " "
3002 << canBePropagated
<< " " << hasProof
<< " " << implied
<< endl
;
3003 d_partialModel
.printModel(v
, Debug("arith::prop"));
3008 double fRand(double fMin
, double fMax
)
3010 double f
= (double)rand() / RAND_MAX
;
3011 return fMin
+ f
* (fMax
- fMin
);
3014 bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx
){
3015 BoundCounts hasCount
= d_linEq
.hasBoundCount(ridx
);
3016 uint32_t rowLength
= d_tableau
.getRowLength(ridx
);
3018 bool success
= false;
3019 static int instance
= 0;
3022 Debug("arith::prop")
3023 << "propagateCandidateRow " << instance
<< " attempt " << rowLength
<< " " << hasCount
<< endl
;
3025 if(rowLength
>= options::arithPropagateMaxLength()){
3026 if(fRand(0.0,1.0) >= double(options::arithPropagateMaxLength())/rowLength
){
3031 if(hasCount
.lowerBoundCount() == rowLength
){
3032 success
|= attemptFull(ridx
, false);
3033 }else if(hasCount
.lowerBoundCount() + 1 == rowLength
){
3034 success
|= attemptSingleton(ridx
, false);
3037 if(hasCount
.upperBoundCount() == rowLength
){
3038 success
|= attemptFull(ridx
, true);
3039 }else if(hasCount
.upperBoundCount() + 1 == rowLength
){
3040 success
|= attemptSingleton(ridx
, true);
3045 void TheoryArithPrivate::dumpUpdatedBoundsToRows(){
3046 Assert(d_candidateRows
.empty());
3047 DenseSet::const_iterator i
= d_updatedBounds
.begin();
3048 DenseSet::const_iterator end
= d_updatedBounds
.end();
3049 for(; i
!= end
; ++i
){
3051 if(d_tableau
.isBasic(var
)){
3052 RowIndex ridx
= d_tableau
.basicToRowIndex(var
);
3053 d_candidateRows
.softAdd(ridx
);
3055 Tableau::ColIterator basicIter
= d_tableau
.colIterator(var
);
3056 for(; !basicIter
.atEnd(); ++basicIter
){
3057 const Tableau::Entry
& entry
= *basicIter
;
3058 RowIndex ridx
= entry
.getRowIndex();
3059 d_candidateRows
.softAdd(ridx
);
3063 d_updatedBounds
.purge();
3066 const BoundsInfo
& TheoryArithPrivate::boundsInfo(ArithVar basic
) const{
3067 RowIndex ridx
= d_tableau
.basicToRowIndex(basic
);
3068 return d_rowTracking
[ridx
];
3071 }/* CVC4::theory::arith namespace */
3072 }/* CVC4::theory namespace */
3073 }/* CVC4 namespace */