projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Merge branch '1.0.x', getting fix for bug 480
[cvc5.git] / src / theory / arith / theory_arith.cpp
1 /********************* */
2 /*! \file theory_arith.cpp
3 ** \verbatim
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
11 **
12 ** \brief [[ Add one-line brief description here ]]
13 **
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
16 **/
17
18 #include "expr/node.h"
19 #include "expr/kind.h"
20 #include "expr/metakind.h"
21 #include "expr/node_builder.h"
22
23 #include "theory/valuation.h"
24 #include "theory/rewriter.h"
25
26 #include "util/rational.h"
27 #include "util/integer.h"
28 #include "util/boolean_simplification.h"
29 #include "util/dense_map.h"
30
31 #include "smt/logic_exception.h"
32
33 #include "theory/arith/arith_utilities.h"
34 #include "theory/arith/delta_rational.h"
35 #include "theory/arith/partial_model.h"
36 #include "theory/arith/matrix.h"
37
38 #include "theory/arith/arith_rewriter.h"
39 #include "theory/arith/constraint.h"
40 #include "theory/arith/theory_arith.h"
41 #include "theory/arith/normal_form.h"
42 #include "theory/model.h"
43
44 #include "theory/arith/options.h"
45
46 #include <stdint.h>
47
48 using namespace std;
49 using namespace CVC4::kind;
50
51 namespace CVC4 {
52 namespace theory {
53 namespace arith {
54
55 const uint32_t RESET_START = 2;
56
57
58 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
59 Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe),
60 d_nlIncomplete( false),
61 d_qflraStatus(Result::SAT_UNKNOWN),
62 d_unknownsInARow(0),
63 d_hasDoneWorkSinceCut(false),
64 d_learner(u),
65 d_numberOfVariables(0),
66 d_pool(),
67 d_setupLiteralCallback(this),
68 d_assertionsThatDoNotMatchTheirLiterals(c),
69 d_nextIntegerCheckVar(0),
70 d_constantIntegerVariables(c),
71 d_diseqQueue(c, false),
72 d_currentPropagationList(),
73 d_learnedBounds(c),
74 d_partialModel(c, d_deltaComputeCallback),
75 d_tableau(),
76 d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack),
77 d_diosolver(c),
78 d_restartsCounter(0),
79 d_tableauSizeHasBeenModified(false),
80 d_tableauResetDensity(1.6),
81 d_tableauResetPeriod(10),
82 d_conflicts(c),
83 d_raiseConflict(d_conflicts),
84 d_tempVarMalloc(*this),
85 d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap, d_raiseConflict),
86 d_simplex(d_linEq, d_raiseConflict),
87 d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager, d_raiseConflict),
88 d_deltaComputeCallback(this),
89 d_basicVarModelUpdateCallBack(d_simplex),
90 d_DELTA_ZERO(0),
91 d_statistics()
92 {
93 }
94
95 TheoryArith::~TheoryArith(){}
96
97 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
98 d_congruenceManager.setMasterEqualityEngine(eq);
99 }
100
101 Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){
102 NodeManager* currNM = NodeManager::currentNM();
103 TypeNode functionType = currNM->mkFunctionType(dom, range);
104 return currNM->mkSkolem(name, functionType);
105 }
106
107 Node TheoryArith::getRealDivideBy0Func(){
108 Assert(!getLogicInfo().isLinear());
109 Assert(getLogicInfo().areRealsUsed());
110
111 if(d_realDivideBy0Func.isNull()){
112 TypeNode realType = NodeManager::currentNM()->realType();
113 d_realDivideBy0Func = skolemFunction("/by0_$$", realType, realType);
114 }
115 return d_realDivideBy0Func;
116 }
117
118 Node TheoryArith::getIntDivideBy0Func(){
119 Assert(!getLogicInfo().isLinear());
120 Assert(getLogicInfo().areIntegersUsed());
121
122 if(d_intDivideBy0Func.isNull()){
123 TypeNode intType = NodeManager::currentNM()->integerType();
124 d_intDivideBy0Func = skolemFunction("divby0_$$", intType, intType);
125 }
126 return d_intDivideBy0Func;
127 }
128
129 Node TheoryArith::getIntModulusBy0Func(){
130 Assert(!getLogicInfo().isLinear());
131 Assert(getLogicInfo().areIntegersUsed());
132
133 if(d_intModulusBy0Func.isNull()){
134 TypeNode intType = NodeManager::currentNM()->integerType();
135 d_intModulusBy0Func = skolemFunction("modby0_$$", intType, intType);
136 }
137 return d_intModulusBy0Func;
138 }
139
140 TheoryArith::ModelException::ModelException(TNode n, const char* msg) throw (){
141 stringstream ss;
142 ss << "Cannot construct a model for " << n << " as " << endl << msg;
143 setMessage(ss.str());
144 }
145 TheoryArith::ModelException::~ModelException() throw (){ }
146
147
148 TheoryArith::Statistics::Statistics():
149 d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0),
150 d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0),
151 d_statUserVariables("theory::arith::UserVariables", 0),
152 d_statSlackVariables("theory::arith::SlackVariables", 0),
153 d_statDisequalitySplits("theory::arith::DisequalitySplits", 0),
154 d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0),
155 d_simplifyTimer("theory::arith::simplifyTimer"),
156 d_staticLearningTimer("theory::arith::staticLearningTimer"),
157 d_presolveTime("theory::arith::presolveTime"),
158 d_newPropTime("theory::arith::newPropTimer"),
159 d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0),
160 d_initialTableauSize("theory::arith::initialTableauSize", 0),
161 d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
162 d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
163 d_restartTimer("theory::arith::restartTimer"),
164 d_boundComputationTime("theory::arith::bound::time"),
165 d_boundComputations("theory::arith::bound::boundComputations",0),
166 d_boundPropagations("theory::arith::bound::boundPropagations",0),
167 d_unknownChecks("theory::arith::status::unknowns", 0),
168 d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0),
169 d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow"),
170 d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0),
171 d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0),
172 d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0)
173 {
174 StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
175 StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
176
177 StatisticsRegistry::registerStat(&d_statUserVariables);
178 StatisticsRegistry::registerStat(&d_statSlackVariables);
179 StatisticsRegistry::registerStat(&d_statDisequalitySplits);
180 StatisticsRegistry::registerStat(&d_statDisequalityConflicts);
181 StatisticsRegistry::registerStat(&d_simplifyTimer);
182 StatisticsRegistry::registerStat(&d_staticLearningTimer);
183
184 StatisticsRegistry::registerStat(&d_presolveTime);
185 StatisticsRegistry::registerStat(&d_newPropTime);
186
187 StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
188
189 StatisticsRegistry::registerStat(&d_initialTableauSize);
190 StatisticsRegistry::registerStat(&d_currSetToSmaller);
191 StatisticsRegistry::registerStat(&d_smallerSetToCurr);
192 StatisticsRegistry::registerStat(&d_restartTimer);
193
194 StatisticsRegistry::registerStat(&d_boundComputationTime);
195 StatisticsRegistry::registerStat(&d_boundComputations);
196 StatisticsRegistry::registerStat(&d_boundPropagations);
197
198 StatisticsRegistry::registerStat(&d_unknownChecks);
199 StatisticsRegistry::registerStat(&d_maxUnknownsInARow);
200 StatisticsRegistry::registerStat(&d_avgUnknownsInARow);
201 StatisticsRegistry::registerStat(&d_revertsOnConflicts);
202 StatisticsRegistry::registerStat(&d_commitsOnConflicts);
203 StatisticsRegistry::registerStat(&d_nontrivialSatChecks);
204 }
205
206 TheoryArith::Statistics::~Statistics(){
207 StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
208 StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
209
210 StatisticsRegistry::unregisterStat(&d_statUserVariables);
211 StatisticsRegistry::unregisterStat(&d_statSlackVariables);
212 StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
213 StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts);
214 StatisticsRegistry::unregisterStat(&d_simplifyTimer);
215 StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
216
217 StatisticsRegistry::unregisterStat(&d_presolveTime);
218 StatisticsRegistry::unregisterStat(&d_newPropTime);
219
220 StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
221
222 StatisticsRegistry::unregisterStat(&d_initialTableauSize);
223 StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
224 StatisticsRegistry::unregisterStat(&d_smallerSetToCurr);
225 StatisticsRegistry::unregisterStat(&d_restartTimer);
226
227 StatisticsRegistry::unregisterStat(&d_boundComputationTime);
228 StatisticsRegistry::unregisterStat(&d_boundComputations);
229 StatisticsRegistry::unregisterStat(&d_boundPropagations);
230
231 StatisticsRegistry::unregisterStat(&d_unknownChecks);
232 StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow);
233 StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow);
234 StatisticsRegistry::unregisterStat(&d_revertsOnConflicts);
235 StatisticsRegistry::unregisterStat(&d_commitsOnConflicts);
236 StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks);
237 }
238
239 void TheoryArith::revertOutOfConflict(){
240 d_partialModel.revertAssignmentChanges();
241 clearUpdates();
242 d_currentPropagationList.clear();
243 }
244
245 void TheoryArith::clearUpdates(){
246 d_updatedBounds.purge();
247 }
248
249 void TheoryArith::zeroDifferenceDetected(ArithVar x){
250 Assert(d_congruenceManager.isWatchedVariable(x));
251 Assert(d_partialModel.upperBoundIsZero(x));
252 Assert(d_partialModel.lowerBoundIsZero(x));
253
254 Constraint lb = d_partialModel.getLowerBoundConstraint(x);
255 Constraint ub = d_partialModel.getUpperBoundConstraint(x);
256
257 if(lb->isEquality()){
258 d_congruenceManager.watchedVariableIsZero(lb);
259 }else if(ub->isEquality()){
260 d_congruenceManager.watchedVariableIsZero(ub);
261 }else{
262 d_congruenceManager.watchedVariableIsZero(lb, ub);
263 }
264 }
265
266 /* procedure AssertLower( x_i >= c_i ) */
267 bool TheoryArith::AssertLower(Constraint constraint){
268 Assert(constraint != NullConstraint);
269 Assert(constraint->isLowerBound());
270
271 ArithVar x_i = constraint->getVariable();
272 const DeltaRational& c_i = constraint->getValue();
273
274 Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
275
276 Assert(!isInteger(x_i) || c_i.isIntegral());
277
278 //TODO Relax to less than?
279 if(d_partialModel.lessThanLowerBound(x_i, c_i)){
280 return false; //sat
281 }
282
283 int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
284 if(cmpToUB > 0){ // c_i < \lowerbound(x_i)
285 Constraint ubc = d_partialModel.getUpperBoundConstraint(x_i);
286 Node conflict = ConstraintValue::explainConflict(ubc, constraint);
287 Debug("arith") << "AssertLower conflict " << conflict << endl;
288 ++(d_statistics.d_statAssertLowerConflicts);
289 d_raiseConflict(conflict);
290 return true;
291 }else if(cmpToUB == 0){
292 if(isInteger(x_i)){
293 d_constantIntegerVariables.push_back(x_i);
294 Debug("dio::push") << x_i << endl;
295 }
296 Constraint ub = d_partialModel.getUpperBoundConstraint(x_i);
297
298 if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
299 // if it is not a watched variable report it
300 // if it is is a watched variable and c_i == 0,
301 // let zeroDifferenceDetected(x_i) catch this
302 d_congruenceManager.equalsConstant(constraint, ub);
303 }
304
305 const ValueCollection& vc = constraint->getValueCollection();
306 if(vc.hasDisequality()){
307 Assert(vc.hasEquality());
308 const Constraint eq = vc.getEquality();
309 const Constraint diseq = vc.getDisequality();
310 if(diseq->isTrue()){
311 //const Constraint ub = vc.getUpperBound();
312 Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
313
314 ++(d_statistics.d_statDisequalityConflicts);
315 Debug("eq") << " assert lower conflict " << conflict << endl;
316 d_raiseConflict(conflict);
317 return true;
318 }else if(!eq->isTrue()){
319 Debug("eq") << "lb == ub, propagate eq" << eq << endl;
320 eq->impliedBy(constraint, d_partialModel.getUpperBoundConstraint(x_i));
321 // do not need to add to d_learnedBounds
322 }
323 }
324 }else{
325 Assert(cmpToUB < 0);
326 const ValueCollection& vc = constraint->getValueCollection();
327
328 if(vc.hasDisequality()){
329 const Constraint diseq = vc.getDisequality();
330 if(diseq->isTrue()){
331 const Constraint ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
332
333 if(ub->hasProof()){
334 Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
335 Debug("eq") << " assert upper conflict " << conflict << endl;
336 d_raiseConflict(conflict);
337 return true;
338 }else if(!ub->negationHasProof()){
339 Constraint negUb = ub->getNegation();
340 negUb->impliedBy(constraint, diseq);
341 d_learnedBounds.push_back(negUb);
342 }
343 }
344 }
345 }
346
347 d_currentPropagationList.push_back(constraint);
348 d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
349
350 d_partialModel.setLowerBoundConstraint(constraint);
351
352 if(d_congruenceManager.isWatchedVariable(x_i)){
353 int sgn = c_i.sgn();
354 if(sgn > 0){
355 d_congruenceManager.watchedVariableCannotBeZero(constraint);
356 }else if(sgn == 0 && d_partialModel.upperBoundIsZero(x_i)){
357 zeroDifferenceDetected(x_i);
358 }
359 }
360
361 d_updatedBounds.softAdd(x_i);
362
363 if(Debug.isOn("model")) {
364 Debug("model") << "before" << endl;
365 d_partialModel.printModel(x_i);
366 d_tableau.debugPrintIsBasic(x_i);
367 }
368
369 if(!d_tableau.isBasic(x_i)){
370 if(d_partialModel.getAssignment(x_i) < c_i){
371 d_linEq.update(x_i, c_i);
372 }
373 }else{
374 d_simplex.updateBasic(x_i);
375 }
376
377 if(Debug.isOn("model")) {
378 Debug("model") << "after" << endl;
379 d_partialModel.printModel(x_i);
380 d_tableau.debugPrintIsBasic(x_i);
381 }
382
383 return false; //sat
384 }
385
386 /* procedure AssertUpper( x_i <= c_i) */
387 bool TheoryArith::AssertUpper(Constraint constraint){
388 ArithVar x_i = constraint->getVariable();
389 const DeltaRational& c_i = constraint->getValue();
390
391 Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
392 AssertArgument(constraint != NullConstraint,
393 "AssertUpper() called on a NullConstraint.");
394 Assert(constraint->isUpperBound());
395
396 //Too strong because of rounding with integers
397 //Assert(!constraint->hasLiteral() || original == constraint->getLiteral());
398 Assert(!isInteger(x_i) || c_i.isIntegral());
399
400 Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
401
402 if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
403 return false; //sat
404 }
405
406 // cmpToLb = \lowerbound(x_i).cmp(c_i)
407 int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
408 if( cmpToLB < 0 ){ // \upperbound(x_i) < \lowerbound(x_i)
409 Constraint lbc = d_partialModel.getLowerBoundConstraint(x_i);
410 Node conflict = ConstraintValue::explainConflict(lbc, constraint);
411 Debug("arith") << "AssertUpper conflict " << conflict << endl;
412 ++(d_statistics.d_statAssertUpperConflicts);
413 d_raiseConflict(conflict);
414 return true;
415 }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
416 if(isInteger(x_i)){
417 d_constantIntegerVariables.push_back(x_i);
418 Debug("dio::push") << x_i << endl;
419 }
420 Constraint lb = d_partialModel.getLowerBoundConstraint(x_i);
421 if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
422 // if it is not a watched variable report it
423 // if it is is a watched variable and c_i == 0,
424 // let zeroDifferenceDetected(x_i) catch this
425 d_congruenceManager.equalsConstant(lb, constraint);
426 }
427
428 const ValueCollection& vc = constraint->getValueCollection();
429 if(vc.hasDisequality()){
430 Assert(vc.hasEquality());
431 const Constraint diseq = vc.getDisequality();
432 const Constraint eq = vc.getEquality();
433 if(diseq->isTrue()){
434 Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
435 Debug("eq") << " assert upper conflict " << conflict << endl;
436 d_raiseConflict(conflict);
437 return true;
438 }else if(!eq->isTrue()){
439 Debug("eq") << "lb == ub, propagate eq" << eq << endl;
440 eq->impliedBy(constraint, d_partialModel.getLowerBoundConstraint(x_i));
441 //do not bother to add to d_learnedBounds
442 }
443 }
444 }else if(cmpToLB > 0){
445 const ValueCollection& vc = constraint->getValueCollection();
446 if(vc.hasDisequality()){
447 const Constraint diseq = vc.getDisequality();
448 if(diseq->isTrue()){
449 const Constraint lb =
450 d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
451 if(lb->hasProof()){
452 Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
453 Debug("eq") << " assert upper conflict " << conflict << endl;
454 d_raiseConflict(conflict);
455 return true;
456 }else if(!lb->negationHasProof()){
457 Constraint negLb = lb->getNegation();
458 negLb->impliedBy(constraint, diseq);
459 //if(!negLb->canBePropagated()){
460 d_learnedBounds.push_back(negLb);
461 //}//otherwise let this be propagated/asserted later
462 }
463 }
464 }
465 }
466
467 d_currentPropagationList.push_back(constraint);
468 d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
469 //It is fine if this is NullConstraint
470
471 d_partialModel.setUpperBoundConstraint(constraint);
472
473 if(d_congruenceManager.isWatchedVariable(x_i)){
474 int sgn = c_i.sgn();
475 if(sgn < 0){
476 d_congruenceManager.watchedVariableCannotBeZero(constraint);
477 }else if(sgn == 0 && d_partialModel.lowerBoundIsZero(x_i)){
478 zeroDifferenceDetected(x_i);
479 }
480 }
481
482 d_updatedBounds.softAdd(x_i);
483
484 if(Debug.isOn("model")) {
485 Debug("model") << "before" << endl;
486 d_partialModel.printModel(x_i);
487 d_tableau.debugPrintIsBasic(x_i);
488 }
489
490 if(!d_tableau.isBasic(x_i)){
491 if(d_partialModel.getAssignment(x_i) > c_i){
492 d_linEq.update(x_i, c_i);
493 }
494 }else{
495 d_simplex.updateBasic(x_i);
496 }
497
498 if(Debug.isOn("model")) {
499 Debug("model") << "after" << endl;
500 d_partialModel.printModel(x_i);
501 d_tableau.debugPrintIsBasic(x_i);
502 }
503
504 return false; //sat
505 }
506
507
508 /* procedure AssertEquality( x_i == c_i ) */
509 bool TheoryArith::AssertEquality(Constraint constraint){
510 AssertArgument(constraint != NullConstraint,
511 "AssertUpper() called on a NullConstraint.");
512
513 ArithVar x_i = constraint->getVariable();
514 const DeltaRational& c_i = constraint->getValue();
515
516 Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
517
518 //Should be fine in integers
519 Assert(!isInteger(x_i) || c_i.isIntegral());
520
521 int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
522 int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
523
524 // u_i <= c_i <= l_i
525 // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
526 if(cmpToUB >= 0 && cmpToLB <= 0){
527 return false; //sat
528 }
529
530 if(cmpToUB > 0){
531 Constraint ubc = d_partialModel.getUpperBoundConstraint(x_i);
532 Node conflict = ConstraintValue::explainConflict(ubc, constraint);
533 Debug("arith") << "AssertEquality conflicts with upper bound " << conflict << endl;
534 d_raiseConflict(conflict);
535 return true;
536 }
537
538 if(cmpToLB < 0){
539 Constraint lbc = d_partialModel.getLowerBoundConstraint(x_i);
540 Node conflict = ConstraintValue::explainConflict(lbc, constraint);
541 Debug("arith") << "AssertEquality conflicts with lower bound" << conflict << endl;
542 d_raiseConflict(conflict);
543 return true;
544 }
545
546 Assert(cmpToUB <= 0);
547 Assert(cmpToLB >= 0);
548 Assert(cmpToUB < 0 || cmpToLB > 0);
549
550
551 if(isInteger(x_i)){
552 d_constantIntegerVariables.push_back(x_i);
553 Debug("dio::push") << x_i << endl;
554 }
555
556 // Don't bother to check whether x_i != c_i is in d_diseq
557 // The a and (not a) should never be on the fact queue
558 d_currentPropagationList.push_back(constraint);
559 d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
560 d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
561
562 d_partialModel.setUpperBoundConstraint(constraint);
563 d_partialModel.setLowerBoundConstraint(constraint);
564
565 if(d_congruenceManager.isWatchedVariable(x_i)){
566 int sgn = c_i.sgn();
567 if(sgn == 0){
568 zeroDifferenceDetected(x_i);
569 }else{
570 d_congruenceManager.watchedVariableCannotBeZero(constraint);
571 d_congruenceManager.equalsConstant(constraint);
572 }
573 }else{
574 d_congruenceManager.equalsConstant(constraint);
575 }
576
577 d_updatedBounds.softAdd(x_i);
578
579 if(Debug.isOn("model")) {
580 Debug("model") << "before" << endl;
581 d_partialModel.printModel(x_i);
582 d_tableau.debugPrintIsBasic(x_i);
583 }
584
585 if(!d_tableau.isBasic(x_i)){
586 if(!(d_partialModel.getAssignment(x_i) == c_i)){
587 d_linEq.update(x_i, c_i);
588 }
589 }else{
590 d_simplex.updateBasic(x_i);
591 }
592
593 if(Debug.isOn("model")) {
594 Debug("model") << "after" << endl;
595 d_partialModel.printModel(x_i);
596 d_tableau.debugPrintIsBasic(x_i);
597 }
598
599 return false;
600 }
601
602
603 /* procedure AssertDisequality( x_i != c_i ) */
604 bool TheoryArith::AssertDisequality(Constraint constraint){
605
606 AssertArgument(constraint != NullConstraint,
607 "AssertUpper() called on a NullConstraint.");
608 ArithVar x_i = constraint->getVariable();
609 const DeltaRational& c_i = constraint->getValue();
610
611 Debug("arith") << "AssertDisequality(" << x_i << " " << c_i << ")"<< std::endl;
612
613 //Should be fine in integers
614 Assert(!isInteger(x_i) || c_i.isIntegral());
615
616 if(d_congruenceManager.isWatchedVariable(x_i)){
617 int sgn = c_i.sgn();
618 if(sgn == 0){
619 d_congruenceManager.watchedVariableCannotBeZero(constraint);
620 }
621 }
622
623 const ValueCollection& vc = constraint->getValueCollection();
624 if(vc.hasLowerBound() && vc.hasUpperBound()){
625 const Constraint lb = vc.getLowerBound();
626 const Constraint ub = vc.getUpperBound();
627 if(lb->isTrue() && ub->isTrue()){
628 //in conflict
629 Debug("eq") << "explaining" << endl;
630 ++(d_statistics.d_statDisequalityConflicts);
631 Node conflict = ConstraintValue::explainConflict(constraint, lb, ub);
632 d_raiseConflict(conflict);
633 return true;
634 }
635 }
636 if(vc.hasLowerBound() ){
637 const Constraint lb = vc.getLowerBound();
638 if(lb->isTrue()){
639 const Constraint ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
640 Debug("eq") << "propagate UpperBound " << constraint << lb << ub << endl;
641 const Constraint negUb = ub->getNegation();
642 if(!negUb->isTrue()){
643 negUb->impliedBy(constraint, lb);
644 d_learnedBounds.push_back(negUb);
645 }
646 }
647 }
648 if(vc.hasUpperBound()){
649 const Constraint ub = vc.getUpperBound();
650 if(ub->isTrue()){
651 const Constraint lb = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
652
653 Debug("eq") << "propagate LowerBound " << constraint << lb << ub << endl;
654 const Constraint negLb = lb->getNegation();
655 if(!negLb->isTrue()){
656 negLb->impliedBy(constraint, ub);
657 d_learnedBounds.push_back(negLb);
658 }
659 }
660 }
661
662 bool split = constraint->isSplit();
663
664 if(!split && c_i == d_partialModel.getAssignment(x_i)){
665 Debug("eq") << "lemma now! " << constraint << endl;
666 d_out->lemma(constraint->split());
667 return false;
668 }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
669 Debug("eq") << "can drop as less than lb" << constraint << endl;
670 }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i)){
671 Debug("eq") << "can drop as less than ub" << constraint << endl;
672 }else if(!split){
673 Debug("eq") << "push back" << constraint << endl;
674 d_diseqQueue.push(constraint);
675 d_partialModel.invalidateDelta();
676 }else{
677 Debug("eq") << "skipping already split " << constraint << endl;
678 }
679 return false;
680 }
681
682 void TheoryArith::addSharedTerm(TNode n){
683 Debug("arith::addSharedTerm") << "addSharedTerm: " << n << endl;
684 if(n.isConst()){
685 d_partialModel.invalidateDelta();
686 }
687
688 d_congruenceManager.addSharedTerm(n);
689 if(!n.isConst() && !isSetup(n)){
690 Polynomial poly = Polynomial::parsePolynomial(n);
691 Polynomial::iterator it = poly.begin();
692 Polynomial::iterator it_end = poly.end();
693 for (; it != it_end; ++ it) {
694 Monomial m = *it;
695 if (!m.isConstant() && !isSetup(m.getVarList().getNode())) {
696 setupVariableList(m.getVarList());
697 }
698 }
699 }
700 }
701
702 Node TheoryArith::ppRewrite(TNode atom) {
703 Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
704
705
706 if (atom.getKind() == kind::EQUAL && options::arithRewriteEq()) {
707 Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
708 Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
709 Node rewritten = Rewriter::rewrite(leq.andNode(geq));
710 Debug("arith::preprocess") << "arith::preprocess() : returning "
711 << rewritten << endl;
712 return rewritten;
713 } else {
714 return atom;
715 }
716 }
717
718 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
719 TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
720 Debug("simplify") << "TheoryArith::solve(" << in << ")" << endl;
721
722
723 // Solve equalities
724 Rational minConstant = 0;
725 Node minMonomial;
726 Node minVar;
727 if (in.getKind() == kind::EQUAL) {
728 Comparison cmp = Comparison::parseNormalForm(in);
729
730 Polynomial left = cmp.getLeft();
731 Polynomial right = cmp.getRight();
732
733 Monomial m = left.getHead();
734 if (m.getVarList().singleton()){
735 VarList vl = m.getVarList();
736 Node var = vl.getNode();
737 if (var.getKind() == kind::VARIABLE){
738 // if vl.isIntegral then m.getConstant().isOne()
739 if(!vl.isIntegral() || m.getConstant().isOne()){
740 minVar = var;
741 }
742 }
743 }
744
745 // Solve for variable
746 if (!minVar.isNull()) {
747 Polynomial right = cmp.getRight();
748 Node elim = right.getNode();
749 // ax + p = c -> (ax + p) -ax - c = -ax
750 // x = (p - ax - c) * -1/a
751 // Add the substitution if not recursive
752 Assert(elim == Rewriter::rewrite(elim));
753
754
755 static const unsigned MAX_SUB_SIZE = 20;
756 if(false && right.size() > MAX_SUB_SIZE){
757 Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
758 Debug("simplify") << right.size() << endl;
759 }else if(elim.hasSubterm(minVar)){
760 Debug("simplify") << "TheoryArith::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl;
761 }else if (!minVar.getType().isInteger() || right.isIntegral()) {
762 Assert(!elim.hasSubterm(minVar));
763 // cannot eliminate integers here unless we know the resulting
764 // substitution is integral
765 Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl;
766
767 outSubstitutions.addSubstitution(minVar, elim);
768 return PP_ASSERT_STATUS_SOLVED;
769 } else {
770 Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
771 }
772 }
773 }
774
775 // If a relation, remember the bound
776 switch(in.getKind()) {
777 case kind::LEQ:
778 case kind::LT:
779 case kind::GEQ:
780 case kind::GT:
781 if (in[0].isVar()) {
782 d_learner.addBound(in);
783 }
784 break;
785 default:
786 // Do nothing
787 break;
788 }
789
790 return PP_ASSERT_STATUS_UNSOLVED;
791 }
792
793 void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
794 TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
795
796 d_learner.staticLearning(n, learned);
797 }
798
799
800
801 ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){
802 ArithVar bestBasic = ARITHVAR_SENTINEL;
803 uint64_t bestRowLength = std::numeric_limits<uint64_t>::max();
804
805 Tableau::ColIterator basicIter = d_tableau.colIterator(variable);
806 for(; !basicIter.atEnd(); ++basicIter){
807 const Tableau::Entry& entry = *basicIter;
808 Assert(entry.getColVar() == variable);
809 RowIndex ridx = entry.getRowIndex();
810 ArithVar basic = d_tableau.rowIndexToBasic(ridx);
811 uint32_t rowLength = d_tableau.getRowLength(ridx);
812 if((rowLength < bestRowLength) ||
813 (rowLength == bestRowLength && basic < bestBasic)){
814 bestBasic = basic;
815 bestRowLength = rowLength;
816 }
817 }
818 Assert(bestBasic == ARITHVAR_SENTINEL || bestRowLength < std::numeric_limits<uint32_t>::max());
819 return bestBasic;
820 }
821
822 void TheoryArith::setupVariable(const Variable& x){
823 Node n = x.getNode();
824
825 Assert(!isSetup(n));
826
827 ++(d_statistics.d_statUserVariables);
828 requestArithVar(n,false);
829 //ArithVar varN = requestArithVar(n,false);
830 //setupInitialValue(varN);
831
832 markSetup(n);
833
834
835 if(x.isDivLike()){
836 setupDivLike(x);
837 }
838
839 }
840
841 void TheoryArith::setupVariableList(const VarList& vl){
842 Assert(!vl.empty());
843
844 TNode vlNode = vl.getNode();
845 Assert(!isSetup(vlNode));
846 Assert(!d_arithvarNodeMap.hasArithVar(vlNode));
847
848 for(VarList::iterator i = vl.begin(), end = vl.end(); i != end; ++i){
849 Variable var = *i;
850
851 if(!isSetup(var.getNode())){
852 setupVariable(var);
853 }
854 }
855
856 if(!vl.singleton()){
857 // vl is the product of at least 2 variables
858 // vl : (* v1 v2 ...)
859 if(getLogicInfo().isLinear()){
860 throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
861 }
862
863 d_out->setIncomplete();
864 d_nlIncomplete = true;
865
866 ++(d_statistics.d_statUserVariables);
867 requestArithVar(vlNode, false);
868 //ArithVar av = requestArithVar(vlNode, false);
869 //setupInitialValue(av);
870
871 markSetup(vlNode);
872 }
873
874 /* Note:
875 * Only call markSetup if the VarList is not a singleton.
876 * See the comment in setupPolynomail for more.
877 */
878 }
879
880 void TheoryArith::cautiousSetupPolynomial(const Polynomial& p){
881 if(p.containsConstant()){
882 if(!p.isConstant()){
883 Polynomial noConstant = p.getTail();
884 if(!isSetup(noConstant.getNode())){
885 setupPolynomial(noConstant);
886 }
887 }
888 }else if(!isSetup(p.getNode())){
889 setupPolynomial(p);
890 }
891 }
892
893 void TheoryArith::setupDivLike(const Variable& v){
894 Assert(v.isDivLike());
895
896 if(getLogicInfo().isLinear()){
897 throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
898 }
899
900 Node vnode = v.getNode();
901 Assert(isSetup(vnode)); // Otherwise there is some invariant breaking recursion
902 Polynomial m = Polynomial::parsePolynomial(vnode[0]);
903 Polynomial n = Polynomial::parsePolynomial(vnode[1]);
904
905 cautiousSetupPolynomial(m);
906 cautiousSetupPolynomial(n);
907
908 Node lem;
909 switch(vnode.getKind()){
910 case DIVISION:
911 case INTS_DIVISION:
912 case INTS_MODULUS:
913 lem = definingIteForDivLike(vnode);
914 break;
915 case DIVISION_TOTAL:
916 lem = axiomIteForTotalDivision(vnode);
917 break;
918 case INTS_DIVISION_TOTAL:
919 case INTS_MODULUS_TOTAL:
920 lem = axiomIteForTotalIntDivision(vnode);
921 break;
922 default:
923 /* intentionally blank */
924 break;
925 }
926
927 if(!lem.isNull()){
928 Debug("arith::div") << lem << endl;
929 d_out->lemma(lem);
930 }
931 }
932
933 Node TheoryArith::definingIteForDivLike(Node divLike){
934 Kind k = divLike.getKind();
935 Assert(k == DIVISION || k == INTS_DIVISION || k == INTS_MODULUS);
936 // (for all ((n Real) (d Real))
937 // (=
938 // (DIVISION n d)
939 // (ite (= d 0)
940 // (APPLY [div_0_skolem_function] n)
941 // (DIVISION_TOTAL x y))))
942
943 Polynomial n = Polynomial::parsePolynomial(divLike[0]);
944 Polynomial d = Polynomial::parsePolynomial(divLike[1]);
945
946 NodeManager* currNM = NodeManager::currentNM();
947 Node dEq0 = currNM->mkNode(EQUAL, d.getNode(), mkRationalNode(0));
948
949 Kind kTotal = (k == DIVISION) ? DIVISION_TOTAL :
950 (k == INTS_DIVISION) ? INTS_DIVISION_TOTAL : INTS_MODULUS_TOTAL;
951
952 Node by0Func = (k == DIVISION) ? getRealDivideBy0Func():
953 (k == INTS_DIVISION) ? getIntDivideBy0Func() : getIntModulusBy0Func();
954
955
956 Debug("arith::div") << divLike << endl;
957 Debug("arith::div") << by0Func << endl;
958
959 Node divTotal = currNM->mkNode(kTotal, n.getNode(), d.getNode());
960 Node divZero = currNM->mkNode(APPLY_UF, by0Func, n.getNode());
961
962 Node defining = divLike.eqNode(dEq0.iteNode( divZero, divTotal));
963
964 return defining;
965 }
966
967 Node TheoryArith::axiomIteForTotalDivision(Node div_tot){
968 Assert(div_tot.getKind() == DIVISION_TOTAL);
969
970 // Inverse of multiplication axiom:
971 // (for all ((n Real) (d Real))
972 // (ite (= d 0)
973 // (= (DIVISION_TOTAL n d) 0)
974 // (= (* d (DIVISION_TOTAL n d)) n)))
975
976
977 Polynomial n = Polynomial::parsePolynomial(div_tot[0]);
978 Polynomial d = Polynomial::parsePolynomial(div_tot[1]);
979 Polynomial div_tot_p = Polynomial::parsePolynomial(div_tot);
980
981 Comparison invEq = Comparison::mkComparison(EQUAL, n, d * div_tot_p);
982 Comparison zeroEq = Comparison::mkComparison(EQUAL, div_tot_p, Polynomial::mkZero());
983 Node dEq0 = (d.getNode()).eqNode(mkRationalNode(0));
984 Node ite = dEq0.iteNode(zeroEq.getNode(), invEq.getNode());
985
986 return ite;
987 }
988
989 Node TheoryArith::axiomIteForTotalIntDivision(Node int_div_like){
990 Kind k = int_div_like.getKind();
991 Assert(k == INTS_DIVISION_TOTAL || k == INTS_MODULUS_TOTAL);
992
993 // (for all ((m Int) (n Int))
994 // (=> (distinct n 0)
995 // (let ((q (div m n)) (r (mod m n)))
996 // (and (= m (+ (* n q) r))
997 // (<= 0 r (- (abs n) 1))))))
998
999 // Updated for div 0 functions
1000 // (for all ((m Int) (n Int))
1001 // (let ((q (div m n)) (r (mod m n)))
1002 // (ite (= n 0)
1003 // (and (= q (div_0_func m)) (= r (mod_0_func m)))
1004 // (and (= m (+ (* n q) r))
1005 // (<= 0 r (- (abs n) 1)))))))
1006
1007 Polynomial n = Polynomial::parsePolynomial(int_div_like[0]);
1008 Polynomial d = Polynomial::parsePolynomial(int_div_like[1]);
1009
1010 NodeManager* currNM = NodeManager::currentNM();
1011 Node zero = mkRationalNode(0);
1012
1013 Node q = (k == INTS_DIVISION_TOTAL) ? int_div_like : currNM->mkNode(INTS_DIVISION_TOTAL, n.getNode(), d.getNode());
1014 Node r = (k == INTS_MODULUS_TOTAL) ? int_div_like : currNM->mkNode(INTS_MODULUS_TOTAL, n.getNode(), d.getNode());
1015
1016 Node dEq0 = (d.getNode()).eqNode(zero);
1017 Node qEq0 = q.eqNode(zero);
1018 Node rEq0 = r.eqNode(zero);
1019
1020 Polynomial rp = Polynomial::parsePolynomial(r);
1021 Polynomial qp = Polynomial::parsePolynomial(q);
1022
1023 Node abs_d = (n.isConstant()) ?
1024 d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs_$$");
1025
1026 Node eq = Comparison::mkComparison(EQUAL, n, d * qp + rp).getNode();
1027 Node leq0 = currNM->mkNode(LEQ, zero, r);
1028 Node leq1 = currNM->mkNode(LT, r, abs_d);
1029
1030 Node andE = currNM->mkNode(AND, eq, leq0, leq1);
1031 Node defDivMode = dEq0.iteNode(qEq0.andNode(rEq0), andE);
1032 Node lem = abs_d.getMetaKind () == metakind::VARIABLE ?
1033 defDivMode.andNode(d.makeAbsCondition(Variable(abs_d))) : defDivMode;
1034
1035 return lem;
1036 }
1037
1038
1039 void TheoryArith::setupPolynomial(const Polynomial& poly) {
1040 Assert(!poly.containsConstant());
1041 TNode polyNode = poly.getNode();
1042 Assert(!isSetup(polyNode));
1043 Assert(!d_arithvarNodeMap.hasArithVar(polyNode));
1044
1045 for(Polynomial::iterator i = poly.begin(), end = poly.end(); i != end; ++i){
1046 Monomial mono = *i;
1047 const VarList& vl = mono.getVarList();
1048 if(!isSetup(vl.getNode())){
1049 setupVariableList(vl);
1050 }
1051 }
1052
1053 if(polyNode.getKind() == PLUS){
1054 d_tableauSizeHasBeenModified = true;
1055
1056 vector<ArithVar> variables;
1057 vector<Rational> coefficients;
1058 asVectors(poly, coefficients, variables);
1059
1060 ArithVar varSlack = requestArithVar(polyNode, true);
1061 d_tableau.addRow(varSlack, coefficients, variables);
1062 setupBasicValue(varSlack);
1063
1064 //Add differences to the difference manager
1065 Polynomial::iterator i = poly.begin(), end = poly.end();
1066 if(i != end){
1067 Monomial first = *i;
1068 ++i;
1069 if(i != end){
1070 Monomial second = *i;
1071 ++i;
1072 if(i == end){
1073 if(first.getConstant().isOne() && second.getConstant().getValue() == -1){
1074 VarList vl0 = first.getVarList();
1075 VarList vl1 = second.getVarList();
1076 if(vl0.singleton() && vl1.singleton()){
1077 d_congruenceManager.addWatchedPair(varSlack, vl0.getNode(), vl1.getNode());
1078 }
1079 }
1080 }
1081 }
1082 }
1083
1084 ++(d_statistics.d_statSlackVariables);
1085 markSetup(polyNode);
1086 }
1087
1088 /* Note:
1089 * It is worth documenting that polyNode should only be marked as
1090 * being setup by this function if it has kind PLUS.
1091 * Other kinds will be marked as being setup by lower levels of setup
1092 * specifically setupVariableList.
1093 */
1094 }
1095
1096 void TheoryArith::setupAtom(TNode atom) {
1097 Assert(isRelationOperator(atom.getKind()));
1098 Assert(Comparison::isNormalAtom(atom));
1099 Assert(!isSetup(atom));
1100 Assert(!d_constraintDatabase.hasLiteral(atom));
1101
1102 Comparison cmp = Comparison::parseNormalForm(atom);
1103 Polynomial nvp = cmp.normalizedVariablePart();
1104 Assert(!nvp.isZero());
1105
1106 if(!isSetup(nvp.getNode())){
1107 setupPolynomial(nvp);
1108 }
1109
1110 d_constraintDatabase.addLiteral(atom);
1111
1112 markSetup(atom);
1113 }
1114
1115 void TheoryArith::preRegisterTerm(TNode n) {
1116 Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
1117
1118 if(isRelationOperator(n.getKind())){
1119 if(!isSetup(n)){
1120 setupAtom(n);
1121 }
1122 Constraint c = d_constraintDatabase.lookup(n);
1123 Assert(c != NullConstraint);
1124
1125 Debug("arith::preregister") << "setup constraint" << c << endl;
1126 Assert(!c->canBePropagated());
1127 c->setPreregistered();
1128 }
1129
1130 Debug("arith::preregister") << "end arith::preRegisterTerm("<< n <<")" << endl;
1131 }
1132
1133 void TheoryArith::releaseArithVar(ArithVar v){
1134 Assert(d_arithvarNodeMap.hasNode(v));
1135
1136 d_constraintDatabase.removeVariable(v);
1137 d_arithvarNodeMap.remove(v);
1138
1139 d_pool.push_back(v);
1140 }
1141
1142 ArithVar TheoryArith::requestArithVar(TNode x, bool slack){
1143 //TODO : The VarList trick is good enough?
1144 Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS);
1145 if(getLogicInfo().isLinear() && Variable::isDivMember(x)){
1146 throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
1147 }
1148 Assert(!d_arithvarNodeMap.hasArithVar(x));
1149 Assert(x.getType().isReal());// real or integer
1150
1151 // ArithVar varX = d_variables.size();
1152 // d_variables.push_back(Node(x));
1153
1154 bool reclaim = !d_pool.empty();
1155 ArithVar varX;
1156
1157 if(reclaim){
1158 varX = d_pool.back();
1159 d_pool.pop_back();
1160
1161 d_partialModel.setAssignment(varX, d_DELTA_ZERO, d_DELTA_ZERO);
1162 }else{
1163 varX = d_numberOfVariables;
1164 ++d_numberOfVariables;
1165
1166 d_slackVars.push_back(true);
1167 d_variableTypes.push_back(ATReal);
1168
1169 d_simplex.increaseMax();
1170
1171 d_tableau.increaseSize();
1172 d_tableauSizeHasBeenModified = true;
1173
1174 d_partialModel.initialize(varX, d_DELTA_ZERO);
1175 }
1176
1177 ArithType type;
1178 if(slack){
1179 //The type computation is not quite accurate for Rationals that are integral.
1180 //We'll use the isIntegral check from the polynomial package instead.
1181 Polynomial p = Polynomial::parsePolynomial(x);
1182 type = p.isIntegral() ? ATInteger : ATReal;
1183 }else{
1184 type = nodeToArithType(x);
1185 }
1186 d_variableTypes[varX] = type;
1187 d_slackVars[varX] = slack;
1188
1189 d_constraintDatabase.addVariable(varX);
1190
1191 d_arithvarNodeMap.setArithVar(x,varX);
1192
1193 // Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl;
1194
1195 // if(slack){
1196 // //The type computation is not quite accurate for Rationals that are integral.
1197 // //We'll use the isIntegral check from the polynomial package instead.
1198 // Polynomial p = Polynomial::parsePolynomial(x);
1199 // d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal);
1200 // }else{
1201 // d_variableTypes.push_back(nodeToArithType(x));
1202 // }
1203
1204 // d_slackVars.push_back(slack);
1205
1206 // d_simplex.increaseMax();
1207
1208 // d_tableau.increaseSize();
1209 // d_tableauSizeHasBeenModified = true;
1210
1211 // d_constraintDatabase.addVariable(varX);
1212
1213 Debug("arith::arithvar") << x << " |-> " << varX << endl;
1214
1215 Assert(!d_partialModel.hasUpperBound(varX));
1216 Assert(!d_partialModel.hasLowerBound(varX));
1217
1218 return varX;
1219 }
1220
1221 void TheoryArith::asVectors(const Polynomial& p, std::vector<Rational>& coeffs, std::vector<ArithVar>& variables) {
1222 for(Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i){
1223 const Monomial& mono = *i;
1224 const Constant& constant = mono.getConstant();
1225 const VarList& variable = mono.getVarList();
1226
1227 Node n = variable.getNode();
1228
1229 Debug("rewriter") << "should be var: " << n << endl;
1230
1231 // TODO: This VarList::isMember(n) can be stronger
1232 Assert(isLeaf(n) || VarList::isMember(n));
1233 Assert(theoryOf(n) != THEORY_ARITH || d_arithvarNodeMap.hasArithVar(n));
1234
1235 Assert(d_arithvarNodeMap.hasArithVar(n));
1236 ArithVar av = d_arithvarNodeMap.asArithVar(n);
1237
1238 coeffs.push_back(constant.getValue());
1239 variables.push_back(av);
1240 }
1241 }
1242
1243 /* Requirements:
1244 * For basic variables the row must have been added to the tableau.
1245 */
1246 void TheoryArith::setupBasicValue(ArithVar x){
1247 Assert(d_tableau.isBasic(x));
1248
1249 // if(!d_tableau.isBasic(x)){
1250 // d_partialModel.setAssignment(x, d_DELTA_ZERO, d_DELTA_ZERO);
1251 // }else{
1252 //If the variable is basic, assertions may have already happened and updates
1253 //may have occured before setting this variable up.
1254
1255 //This can go away if the tableau creation is done at preregister
1256 //time instead of register
1257 DeltaRational safeAssignment = d_linEq.computeRowValue(x, true);
1258 DeltaRational assignment = d_linEq.computeRowValue(x, false);
1259 //d_partialModel.initialize(x,safeAssignment);
1260 //d_partialModel.setAssignment(x,assignment);
1261 d_partialModel.setAssignment(x,safeAssignment,assignment);
1262
1263 // }
1264 Debug("arith") << "setupVariable("<<x<<")"<<std::endl;
1265 }
1266
1267 ArithVar TheoryArith::determineArithVar(const Polynomial& p) const{
1268 Assert(!p.containsConstant());
1269 Assert(p.getHead().constantIsPositive());
1270 TNode n = p.getNode();
1271 Debug("determineArithVar") << "determineArithVar(" << n << ")" << endl;
1272 return d_arithvarNodeMap.asArithVar(n);
1273 }
1274
1275 ArithVar TheoryArith::determineArithVar(TNode assertion) const{
1276 Debug("determineArithVar") << "determineArithVar " << assertion << endl;
1277 Comparison cmp = Comparison::parseNormalForm(assertion);
1278 Polynomial variablePart = cmp.normalizedVariablePart();
1279 return determineArithVar(variablePart);
1280 }
1281
1282
1283 bool TheoryArith::canSafelyAvoidEqualitySetup(TNode equality){
1284 Assert(equality.getKind() == EQUAL);
1285 return d_arithvarNodeMap.hasArithVar(equality[0]);
1286 }
1287
1288 Comparison TheoryArith::mkIntegerEqualityFromAssignment(ArithVar v){
1289 const DeltaRational& beta = d_partialModel.getAssignment(v);
1290
1291 Assert(beta.isIntegral());
1292 Polynomial betaAsPolynomial( Constant::mkConstant(beta.floor()) );
1293
1294 TNode var = d_arithvarNodeMap.asNode(v);
1295 Polynomial varAsPolynomial = Polynomial::parsePolynomial(var);
1296 return Comparison::mkComparison(EQUAL, varAsPolynomial, betaAsPolynomial);
1297 }
1298
1299 Node TheoryArith::dioCutting(){
1300 context::Context::ScopedPush speculativePush(getSatContext());
1301 //DO NOT TOUCH THE OUTPUTSTREAM
1302
1303 for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
1304 ArithVar v = *vi;
1305 if(isInteger(v)){
1306 const DeltaRational& dr = d_partialModel.getAssignment(v);
1307 if(d_partialModel.equalsUpperBound(v, dr) || d_partialModel.equalsLowerBound(v, dr)){
1308 if(!d_partialModel.boundsAreEqual(v)){
1309 // If the bounds are equal this is already in the dioSolver
1310 //Add v = dr as a speculation.
1311 Comparison eq = mkIntegerEqualityFromAssignment(v);
1312 Debug("dio::push") <<v << " " << eq.getNode() << endl;
1313 Assert(!eq.isBoolean());
1314 d_diosolver.pushInputConstraint(eq, eq.getNode());
1315 // It does not matter what the explanation of eq is.
1316 // It cannot be used in a conflict
1317 }
1318 }
1319 }
1320 }
1321
1322 SumPair plane = d_diosolver.processEquationsForCut();
1323 if(plane.isZero()){
1324 return Node::null();
1325 }else{
1326 Polynomial p = plane.getPolynomial();
1327 Polynomial c(plane.getConstant() * Constant::mkConstant(-1));
1328 Integer gcd = p.gcd();
1329 Assert(p.isIntegral());
1330 Assert(c.isIntegral());
1331 Assert(gcd > 1);
1332 Assert(!gcd.divides(c.asConstant().getNumerator()));
1333 Comparison leq = Comparison::mkComparison(LEQ, p, c);
1334 Comparison geq = Comparison::mkComparison(GEQ, p, c);
1335 Node lemma = NodeManager::currentNM()->mkNode(OR, leq.getNode(), geq.getNode());
1336 Node rewrittenLemma = Rewriter::rewrite(lemma);
1337 Debug("arith::dio") << "dioCutting found the plane: " << plane.getNode() << endl;
1338 Debug("arith::dio") << "resulting in the cut: " << lemma << endl;
1339 Debug("arith::dio") << "rewritten " << rewrittenLemma << endl;
1340 return rewrittenLemma;
1341 }
1342 }
1343
1344 Node TheoryArith::callDioSolver(){
1345 while(!d_constantIntegerVariables.empty()){
1346 ArithVar v = d_constantIntegerVariables.front();
1347 d_constantIntegerVariables.pop();
1348
1349 Debug("arith::dio") << v << endl;
1350
1351 Assert(isInteger(v));
1352 Assert(d_partialModel.boundsAreEqual(v));
1353
1354
1355 Constraint lb = d_partialModel.getLowerBoundConstraint(v);
1356 Constraint ub = d_partialModel.getUpperBoundConstraint(v);
1357
1358 Node orig = Node::null();
1359 if(lb->isEquality()){
1360 orig = lb->explainForConflict();
1361 }else if(ub->isEquality()){
1362 orig = ub->explainForConflict();
1363 }else {
1364 orig = ConstraintValue::explainConflict(ub, lb);
1365 }
1366
1367 Assert(d_partialModel.assignmentIsConsistent(v));
1368
1369 Comparison eq = mkIntegerEqualityFromAssignment(v);
1370
1371 if(eq.isBoolean()){
1372 //This can only be a conflict
1373 Assert(!eq.getNode().getConst<bool>());
1374
1375 //This should be handled by the normal form earlier in the case of equality
1376 Assert(orig.getKind() != EQUAL);
1377 return orig;
1378 }else{
1379 Debug("dio::push") << v << " " << eq.getNode() << " with reason " << orig << endl;
1380 d_diosolver.pushInputConstraint(eq, orig);
1381 }
1382 }
1383
1384 return d_diosolver.processEquationsForConflict();
1385 }
1386
1387 Constraint TheoryArith::constraintFromFactQueue(){
1388 Assert(!done());
1389 TNode assertion = get();
1390
1391 Kind simpleKind = Comparison::comparisonKind(assertion);
1392 Constraint constraint = d_constraintDatabase.lookup(assertion);
1393 if(constraint == NullConstraint){
1394 Assert(simpleKind == EQUAL || simpleKind == DISTINCT );
1395 bool isDistinct = simpleKind == DISTINCT;
1396 Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
1397 Assert(!isSetup(eq));
1398 Node reEq = Rewriter::rewrite(eq);
1399 if(reEq.getKind() == CONST_BOOLEAN){
1400 if(reEq.getConst<bool>() == isDistinct){
1401 // if is (not true), or false
1402 Assert((reEq.getConst<bool>() && isDistinct) ||
1403 (!reEq.getConst<bool>() && !isDistinct));
1404 d_raiseConflict(assertion);
1405 }
1406 return NullConstraint;
1407 }
1408 Assert(reEq.getKind() != CONST_BOOLEAN);
1409 if(!isSetup(reEq)){
1410 setupAtom(reEq);
1411 }
1412 Node reAssertion = isDistinct ? reEq.notNode() : reEq;
1413 constraint = d_constraintDatabase.lookup(reAssertion);
1414
1415 if(assertion != reAssertion){
1416 Debug("arith::nf") << "getting non-nf assertion " << assertion << " |-> " << reAssertion << endl;
1417 Assert(constraint != NullConstraint);
1418 d_assertionsThatDoNotMatchTheirLiterals.insert(assertion, constraint);
1419 }
1420 }
1421
1422 // Kind simpleKind = Comparison::comparisonKind(assertion);
1423 // Assert(simpleKind != UNDEFINED_KIND);
1424 // Assert(constraint != NullConstraint ||
1425 // simpleKind == EQUAL ||
1426 // simpleKind == DISTINCT );
1427 // if(simpleKind == EQUAL || simpleKind == DISTINCT){
1428 // Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
1429
1430 // if(!isSetup(eq)){
1431 // //The previous code was equivalent to:
1432 // setupAtom(eq);
1433 // constraint = d_constraintDatabase.lookup(assertion);
1434 // }
1435 // }
1436 Assert(constraint != NullConstraint);
1437
1438 if(constraint->negationHasProof()){
1439 Constraint negation = constraint->getNegation();
1440 if(negation->isSelfExplaining()){
1441 if(Debug.isOn("whytheoryenginewhy")){
1442 debugPrintFacts();
1443 }
1444 }
1445 Debug("arith::eq") << constraint << endl;
1446 Debug("arith::eq") << negation << endl;
1447
1448 NodeBuilder<> nb(kind::AND);
1449 nb << assertion;
1450 negation->explainForConflict(nb);
1451 Node conflict = nb;
1452 Debug("arith::eq") << "conflict" << conflict << endl;
1453 d_raiseConflict(conflict);
1454 return NullConstraint;
1455 }
1456 Assert(!constraint->negationHasProof());
1457
1458 if(constraint->assertedToTheTheory()){
1459 //Do nothing
1460 return NullConstraint;
1461 }else{
1462 Debug("arith::constraint") << "arith constraint " << constraint << std::endl;
1463 constraint->setAssertedToTheTheory(assertion);
1464
1465 if(!constraint->hasProof()){
1466 Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
1467 constraint->selfExplaining();
1468 }else{
1469 Debug("arith::constraint") << "already has proof: " << constraint->explainForConflict() << endl;
1470 }
1471
1472 return constraint;
1473 }
1474 }
1475
1476 bool TheoryArith::assertionCases(Constraint constraint){
1477 Assert(constraint->hasProof());
1478 Assert(!constraint->negationHasProof());
1479
1480 ArithVar x_i = constraint->getVariable();
1481
1482 switch(constraint->getType()){
1483 case UpperBound:
1484 if(isInteger(x_i) && constraint->isStrictUpperBound()){
1485 Constraint floorConstraint = constraint->getFloor();
1486 if(!floorConstraint->isTrue()){
1487 if(floorConstraint->negationHasProof()){
1488 Node conf = ConstraintValue::explainConflict(constraint, floorConstraint->getNegation());
1489 d_raiseConflict(conf);
1490 return true;
1491 }else{
1492 floorConstraint->impliedBy(constraint);
1493 // Do not need to add to d_learnedBounds
1494 }
1495 }
1496 return AssertUpper(floorConstraint);
1497 }else{
1498 return AssertUpper(constraint);
1499 }
1500 case LowerBound:
1501 if(isInteger(x_i) && constraint->isStrictLowerBound()){
1502 Constraint ceilingConstraint = constraint->getCeiling();
1503 if(!ceilingConstraint->isTrue()){
1504 if(ceilingConstraint->negationHasProof()){
1505 Node conf = ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation());
1506 d_raiseConflict(conf);
1507 return true;
1508 }
1509 ceilingConstraint->impliedBy(constraint);
1510 // Do not need to add to learnedBounds
1511 }
1512 return AssertLower(ceilingConstraint);
1513 }else{
1514 return AssertLower(constraint);
1515 }
1516 case Equality:
1517 return AssertEquality(constraint);
1518 case Disequality:
1519 return AssertDisequality(constraint);
1520 default:
1521 Unreachable();
1522 return false;
1523 }
1524 }
1525
1526 /**
1527 * Looks for the next integer variable without an integer assignment in a round robin fashion.
1528 * Changes the value of d_nextIntegerCheckVar.
1529 *
1530 * If this returns false, d_nextIntegerCheckVar does not have an integer assignment.
1531 * If this returns true, all integer variables have an integer assignment.
1532 */
1533 bool TheoryArith::hasIntegerModel(){
1534 //if(d_variables.size() > 0){
1535 if(getNumberOfVariables()){
1536 const ArithVar rrEnd = d_nextIntegerCheckVar;
1537 do {
1538 //Do not include slack variables
1539 if(isInteger(d_nextIntegerCheckVar) && !isSlackVariable(d_nextIntegerCheckVar)) { // integer
1540 const DeltaRational& d = d_partialModel.getAssignment(d_nextIntegerCheckVar);
1541 if(!d.isIntegral()){
1542 return false;
1543 }
1544 }
1545 } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == getNumberOfVariables() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd);
1546 }
1547 return true;
1548 }
1549
1550 /** Outputs conflicts to the output channel. */
1551 void TheoryArith::outputConflicts(){
1552 Assert(!d_conflicts.empty());
1553 for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
1554 Node conflict = d_conflicts[i];
1555 Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl;
1556 d_out->conflict(conflict);
1557 }
1558 }
1559
1560 void TheoryArith::check(Effort effortLevel){
1561 Assert(d_currentPropagationList.empty());
1562 Debug("effortlevel") << "TheoryArith::check " << effortLevel << std::endl;
1563 Debug("arith") << "TheoryArith::check begun " << effortLevel << std::endl;
1564
1565 if(Debug.isOn("arith::consistency")){
1566 Assert(unenqueuedVariablesAreConsistent());
1567 }
1568
1569 bool newFacts = !done();
1570 //If previous == SAT, then reverts on conflicts are safe
1571 //Otherwise, they are not and must be committed.
1572 Result::Sat previous = d_qflraStatus;
1573 if(newFacts){
1574 d_qflraStatus = Result::SAT_UNKNOWN;
1575 d_hasDoneWorkSinceCut = true;
1576 }
1577
1578 while(!done()){
1579 Constraint curr = constraintFromFactQueue();
1580 if(curr != NullConstraint){
1581 bool res CVC4_UNUSED = assertionCases(curr);
1582 Assert(!res || inConflict());
1583 }
1584 if(inConflict()){ break; }
1585 }
1586 if(!inConflict()){
1587 while(!d_learnedBounds.empty()){
1588 // we may attempt some constraints twice. this is okay!
1589 Constraint curr = d_learnedBounds.front();
1590 d_learnedBounds.pop();
1591 Debug("arith::learned") << curr << endl;
1592
1593 bool res CVC4_UNUSED = assertionCases(curr);
1594 Assert(!res || inConflict());
1595
1596 if(inConflict()){ break; }
1597 }
1598 }
1599
1600 if(inConflict()){
1601 d_qflraStatus = Result::UNSAT;
1602 if(previous == Result::SAT){
1603 ++d_statistics.d_revertsOnConflicts;
1604 Debug("arith::bt") << "clearing here " << " " << newFacts << " " << previous << " " << d_qflraStatus << endl;
1605 revertOutOfConflict();
1606 d_simplex.clearQueue();
1607 }else{
1608 ++d_statistics.d_commitsOnConflicts;
1609 Debug("arith::bt") << "committing here " << " " << newFacts << " " << previous << " " << d_qflraStatus << endl;
1610 d_partialModel.commitAssignmentChanges();
1611 revertOutOfConflict();
1612 }
1613 outputConflicts();
1614 return;
1615 }
1616
1617
1618 if(Debug.isOn("arith::print_assertions")) {
1619 debugPrintAssertions();
1620 }
1621
1622 bool emmittedConflictOrSplit = false;
1623 Assert(d_conflicts.empty());
1624
1625 d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel));
1626
1627 switch(d_qflraStatus){
1628 case Result::SAT:
1629 if(newFacts){
1630 ++d_statistics.d_nontrivialSatChecks;
1631 }
1632
1633 Debug("arith::bt") << "committing sap inConflit" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl;
1634 d_partialModel.commitAssignmentChanges();
1635 d_unknownsInARow = 0;
1636 if(Debug.isOn("arith::consistency")){
1637 Assert(entireStateIsConsistent("sat comit"));
1638 }
1639 break;
1640 case Result::SAT_UNKNOWN:
1641 ++d_unknownsInARow;
1642 ++(d_statistics.d_unknownChecks);
1643 Assert(!fullEffort(effortLevel));
1644 Debug("arith::bt") << "committing unknown" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl;
1645 d_partialModel.commitAssignmentChanges();
1646 d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow);
1647 break;
1648 case Result::UNSAT:
1649 d_unknownsInARow = 0;
1650 if(previous == Result::SAT){
1651 ++d_statistics.d_revertsOnConflicts;
1652 Debug("arith::bt") << "clearing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl;
1653 revertOutOfConflict();
1654 d_simplex.clearQueue();
1655 }else{
1656 ++d_statistics.d_commitsOnConflicts;
1657
1658 Debug("arith::bt") << "committing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl;
1659 d_partialModel.commitAssignmentChanges();
1660 revertOutOfConflict();
1661
1662 if(Debug.isOn("arith::consistency::comitonconflict")){
1663 entireStateIsConsistent("commit on conflict");
1664 }
1665 }
1666 outputConflicts();
1667 emmittedConflictOrSplit = true;
1668 break;
1669 default:
1670 Unimplemented();
1671 }
1672 d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
1673
1674 // This should be fine if sat or unknown
1675 if(!emmittedConflictOrSplit &&
1676 (options::arithPropagationMode() == UNATE_PROP ||
1677 options::arithPropagationMode() == BOTH_PROP)){
1678 TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
1679 Assert(d_qflraStatus != Result::UNSAT);
1680
1681 while(!d_currentPropagationList.empty() && !inConflict()){
1682 Constraint curr = d_currentPropagationList.front();
1683 d_currentPropagationList.pop_front();
1684
1685 ConstraintType t = curr->getType();
1686 Assert(t != Disequality, "Disequalities are not allowed in d_currentPropagation");
1687
1688
1689 switch(t){
1690 case LowerBound:
1691 {
1692 Constraint prev = d_currentPropagationList.front();
1693 d_currentPropagationList.pop_front();
1694 d_constraintDatabase.unatePropLowerBound(curr, prev);
1695 break;
1696 }
1697 case UpperBound:
1698 {
1699 Constraint prev = d_currentPropagationList.front();
1700 d_currentPropagationList.pop_front();
1701 d_constraintDatabase.unatePropUpperBound(curr, prev);
1702 break;
1703 }
1704 case Equality:
1705 {
1706 Constraint prevLB = d_currentPropagationList.front();
1707 d_currentPropagationList.pop_front();
1708 Constraint prevUB = d_currentPropagationList.front();
1709 d_currentPropagationList.pop_front();
1710 d_constraintDatabase.unatePropEquality(curr, prevLB, prevUB);
1711 break;
1712 }
1713 default:
1714 Unhandled(curr->getType());
1715 }
1716 }
1717
1718 if(inConflict()){
1719 Debug("arith::unate") << "unate conflict" << endl;
1720 revertOutOfConflict();
1721 d_qflraStatus = Result::UNSAT;
1722 outputConflicts();
1723 emmittedConflictOrSplit = true;
1724 Debug("arith::bt") << "committing on unate conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl;
1725
1726 }
1727 }else{
1728 TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
1729 d_currentPropagationList.clear();
1730 }
1731 Assert( d_currentPropagationList.empty());
1732
1733
1734 if(!emmittedConflictOrSplit && fullEffort(effortLevel)){
1735 emmittedConflictOrSplit = splitDisequalities();
1736 }
1737
1738 if(!emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()){
1739 Node possibleConflict = Node::null();
1740 if(!emmittedConflictOrSplit && options::arithDioSolver()){
1741 possibleConflict = callDioSolver();
1742 if(possibleConflict != Node::null()){
1743 revertOutOfConflict();
1744 Debug("arith::conflict") << "dio conflict " << possibleConflict << endl;
1745 d_out->conflict(possibleConflict);
1746 emmittedConflictOrSplit = true;
1747 }
1748 }
1749
1750 if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && options::arithDioSolver()){
1751 Node possibleLemma = dioCutting();
1752 if(!possibleLemma.isNull()){
1753 Debug("arith") << "dio cut " << possibleLemma << endl;
1754 emmittedConflictOrSplit = true;
1755 d_hasDoneWorkSinceCut = false;
1756 d_out->lemma(possibleLemma);
1757 }
1758 }
1759
1760 if(!emmittedConflictOrSplit) {
1761 Node possibleLemma = roundRobinBranch();
1762 if(!possibleLemma.isNull()){
1763 ++(d_statistics.d_externalBranchAndBounds);
1764 emmittedConflictOrSplit = true;
1765 d_out->lemma(possibleLemma);
1766 }
1767 }
1768 }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
1769 if(fullEffort(effortLevel) && d_nlIncomplete){
1770 // TODO this is total paranoia
1771 d_out->setIncomplete();
1772 }
1773
1774 if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
1775 if(Debug.isOn("arith::print_model")) { debugPrintModel(); }
1776 Debug("arith") << "TheoryArith::check end" << std::endl;
1777 }
1778
1779 /** Returns true if the roundRobinBranching() issues a lemma. */
1780 Node TheoryArith::roundRobinBranch(){
1781 if(hasIntegerModel()){
1782 return Node::null();
1783 }else{
1784 ArithVar v = d_nextIntegerCheckVar;
1785
1786 Assert(isInteger(v));
1787 Assert(!isSlackVariable(v));
1788
1789 const DeltaRational& d = d_partialModel.getAssignment(v);
1790 const Rational& r = d.getNoninfinitesimalPart();
1791 const Rational& i = d.getInfinitesimalPart();
1792 Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(v) << "]] is " << r << "[" << i << "]" << endl;
1793
1794 Assert(! (r.getDenominator() == 1 && i.getNumerator() == 0));
1795 Assert(!d.isIntegral());
1796
1797 TNode var = d_arithvarNodeMap.asNode(v);
1798 Integer floor_d = d.floor();
1799 Integer ceil_d = d.ceiling();
1800
1801 Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
1802 Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkRationalNode(ceil_d)));
1803
1804
1805 Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
1806 Trace("integers") << "integers: branch & bound: " << lem << endl;
1807 if(d_valuation.isSatLiteral(lem[0])) {
1808 Debug("integers") << " " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
1809 } else {
1810 Debug("integers") << " " << lem[0] << " is not assigned a SAT literal" << endl;
1811 }
1812 if(d_valuation.isSatLiteral(lem[1])) {
1813 Debug("integers") << " " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
1814 } else {
1815 Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl;
1816 }
1817 return lem;
1818 }
1819 }
1820
1821 bool TheoryArith::splitDisequalities(){
1822 bool splitSomething = false;
1823
1824 vector<Constraint> save;
1825
1826 while(!d_diseqQueue.empty()){
1827 Constraint front = d_diseqQueue.front();
1828 d_diseqQueue.pop();
1829
1830 if(front->isSplit()){
1831 Debug("eq") << "split already" << endl;
1832 }else{
1833 Debug("eq") << "not split already" << endl;
1834
1835 ArithVar lhsVar = front->getVariable();
1836
1837 const DeltaRational& lhsValue = d_partialModel.getAssignment(lhsVar);
1838 const DeltaRational& rhsValue = front->getValue();
1839 if(lhsValue == rhsValue){
1840 Debug("arith::lemma") << "Splitting on " << front << endl;
1841 Debug("arith::lemma") << "LHS value = " << lhsValue << endl;
1842 Debug("arith::lemma") << "RHS value = " << rhsValue << endl;
1843 Node lemma = front->split();
1844 ++(d_statistics.d_statDisequalitySplits);
1845 Node relem = Rewriter::rewrite(lemma);
1846
1847 Debug("arith::lemma") << "Now " << relem << endl;
1848 d_out->lemma(lemma);
1849 splitSomething = true;
1850 }else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){
1851 Debug("eq") << "can drop as less than lb" << front << endl;
1852 }else if(d_partialModel.strictlyGreaterThanUpperBound(lhsVar, rhsValue)){
1853 Debug("eq") << "can drop as greater than ub" << front << endl;
1854 }else{
1855 Debug("eq") << "save" << front << ": " <<lhsValue << " != " << rhsValue << endl;
1856 save.push_back(front);
1857 }
1858 }
1859 }
1860 vector<Constraint>::const_iterator i=save.begin(), i_end = save.end();
1861 for(; i != i_end; ++i){
1862 d_diseqQueue.push(*i);
1863 }
1864 return splitSomething;
1865 }
1866
1867 /**
1868 * Should be guarded by at least Debug.isOn("arith::print_assertions").
1869 * Prints to Debug("arith::print_assertions")
1870 */
1871 void TheoryArith::debugPrintAssertions() {
1872 Debug("arith::print_assertions") << "Assertions:" << endl;
1873 for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
1874 ArithVar i = *vi;
1875 if (d_partialModel.hasLowerBound(i)) {
1876 Constraint lConstr = d_partialModel.getLowerBoundConstraint(i);
1877 Debug("arith::print_assertions") << lConstr << endl;
1878 }
1879
1880 if (d_partialModel.hasUpperBound(i)) {
1881 Constraint uConstr = d_partialModel.getUpperBoundConstraint(i);
1882 Debug("arith::print_assertions") << uConstr << endl;
1883 }
1884 }
1885 context::CDQueue<Constraint>::const_iterator it = d_diseqQueue.begin();
1886 context::CDQueue<Constraint>::const_iterator it_end = d_diseqQueue.end();
1887 for(; it != it_end; ++ it) {
1888 Debug("arith::print_assertions") << *it << endl;
1889 }
1890 }
1891
1892 void TheoryArith::debugPrintModel(){
1893 Debug("arith::print_model") << "Model:" << endl;
1894 for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
1895 ArithVar i = *vi;
1896 if(d_arithvarNodeMap.hasNode(i)){
1897 Debug("arith::print_model") << d_arithvarNodeMap.asNode(i) << " : " <<
1898 d_partialModel.getAssignment(i);
1899 if(d_tableau.isBasic(i))
1900 Debug("arith::print_model") << " (basic)";
1901 Debug("arith::print_model") << endl;
1902 }
1903 }
1904 }
1905
1906
1907
1908 Node TheoryArith::explain(TNode n) {
1909
1910 Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
1911
1912 Constraint c = d_constraintDatabase.lookup(n);
1913 if(c != NullConstraint){
1914 Assert(!c->isSelfExplaining());
1915 Node exp = c->explainForPropagation();
1916 Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl;
1917 return exp;
1918 }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){
1919 c = d_assertionsThatDoNotMatchTheirLiterals[n];
1920 if(!c->isSelfExplaining()){
1921 Node exp = c->explainForPropagation();
1922 Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
1923 return exp;
1924 }else{
1925 Debug("arith::explain") << "this is a strange mismatch" << n << endl;
1926 Assert(d_congruenceManager.canExplain(n));
1927 Debug("arith::explain") << "this is a strange mismatch" << n << endl;
1928 return d_congruenceManager.explain(n);
1929 }
1930 }else{
1931 Assert(d_congruenceManager.canExplain(n));
1932 Debug("arith::explain") << "dm explanation" << n << endl;
1933 return d_congruenceManager.explain(n);
1934 }
1935 }
1936
1937
1938 void TheoryArith::propagate(Effort e) {
1939 // This uses model values for safety. Disable for now.
1940 if(d_qflraStatus == Result::SAT &&
1941 (options::arithPropagationMode() == BOUND_INFERENCE_PROP ||
1942 options::arithPropagationMode() == BOTH_PROP)
1943 && hasAnyUpdates()){
1944 propagateCandidates();
1945 }else{
1946 clearUpdates();
1947 }
1948
1949 while(d_constraintDatabase.hasMorePropagations()){
1950 Constraint c = d_constraintDatabase.nextPropagation();
1951 Debug("arith::prop") << "next prop" << getSatContext()->getLevel() << ": " << c << endl;
1952
1953 if(c->negationHasProof()){
1954 Debug("arith::prop") << "negation has proof " << c->getNegation() << endl
1955 << c->getNegation()->explainForConflict() << endl;
1956 }
1957 Assert(!c->negationHasProof(), "A constraint has been propagated on the constraint propagation queue, but the negation has been set to true. Contact Tim now!");
1958
1959 if(!c->assertedToTheTheory()){
1960 Node literal = c->getLiteral();
1961 Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl;
1962
1963 d_out->propagate(literal);
1964 }else{
1965 Debug("arith::prop") << "already asserted to the theory " << c->getLiteral() << endl;
1966 }
1967 }
1968
1969 while(d_congruenceManager.hasMorePropagations()){
1970 TNode toProp = d_congruenceManager.getNextPropagation();
1971
1972 //Currently if the flag is set this came from an equality detected by the
1973 //equality engine in the the difference manager.
1974 Node normalized = Rewriter::rewrite(toProp);
1975
1976 Constraint constraint = d_constraintDatabase.lookup(normalized);
1977 if(constraint == NullConstraint){
1978 Debug("arith::prop") << "propagating on non-constraint? " << toProp << endl;
1979 d_out->propagate(toProp);
1980 }else if(constraint->negationHasProof()){
1981 Node exp = d_congruenceManager.explain(toProp);
1982 Node notNormalized = normalized.getKind() == NOT ?
1983 normalized[0] : normalized.notNode();
1984 Node lp = flattenAnd(exp.andNode(notNormalized));
1985 Debug("arith::prop") << "propagate conflict" << lp << endl;
1986 d_out->conflict(lp);
1987 return;
1988 }else{
1989 Debug("arith::prop") << "propagating still?" << toProp << endl;
1990
1991 d_out->propagate(toProp);
1992 }
1993 }
1994 }
1995
1996 DeltaRational TheoryArith::getDeltaValue(TNode n) const throw (DeltaRationalException, ModelException) {
1997 AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN);
1998 Debug("arith::value") << n << std::endl;
1999
2000 switch(n.getKind()) {
2001
2002 case kind::CONST_RATIONAL:
2003 return n.getConst<Rational>();
2004
2005 case kind::PLUS: { // 2+ args
2006 DeltaRational value(0);
2007 for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
2008 value = value + getDeltaValue(*i);
2009 }
2010 return value;
2011 }
2012
2013 case kind::MULT: { // 2+ args
2014 DeltaRational value(1);
2015 unsigned variableParts = 0;
2016 for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
2017 TNode curr = *i;
2018 value = value * getDeltaValue(curr);
2019 if(!curr.isConst()){
2020 ++variableParts;
2021 }
2022 }
2023 // TODO: This is a bit of a weak check
2024 if(isSetup(n)){
2025 ArithVar var = d_arithvarNodeMap.asArithVar(n);
2026 const DeltaRational& assign = d_partialModel.getAssignment(var);
2027 if(assign != value){
2028 throw ModelException(n, "Model disagrees on non-linear term.");
2029 }
2030 }
2031 return value;
2032 }
2033 case kind::MINUS:{ // 2 args
2034 return getDeltaValue(n[0]) - getDeltaValue(n[1]);
2035 }
2036
2037 case kind::UMINUS:{ // 1 arg
2038 return (- getDeltaValue(n[0]));
2039 }
2040
2041 case kind::DIVISION:{ // 2 args
2042 DeltaRational res = getDeltaValue(n[0]) / getDeltaValue(n[1]);
2043 if(isSetup(n)){
2044 ArithVar var = d_arithvarNodeMap.asArithVar(n);
2045 if(d_partialModel.getAssignment(var) != res){
2046 throw ModelException(n, "Model disagrees on non-linear term.");
2047 }
2048 }
2049 return res;
2050 }
2051 case kind::DIVISION_TOTAL:
2052 case kind::INTS_DIVISION_TOTAL:
2053 case kind::INTS_MODULUS_TOTAL: { // 2 args
2054 DeltaRational denom = getDeltaValue(n[1]);
2055 if(denom.isZero()){
2056 return DeltaRational(0,0);
2057 }else{
2058 DeltaRational numer = getDeltaValue(n[0]);
2059 DeltaRational res;
2060 if(n.getKind() == kind::DIVISION_TOTAL){
2061 res = numer / denom;
2062 }else if(n.getKind() == kind::INTS_DIVISION_TOTAL){
2063 res = Rational(numer.floorDivideQuotient(denom));
2064 }else{
2065 Assert(n.getKind() == kind::INTS_MODULUS_TOTAL);
2066 res = Rational(numer.floorDivideRemainder(denom));
2067 }
2068 if(isSetup(n)){
2069 ArithVar var = d_arithvarNodeMap.asArithVar(n);
2070 if(d_partialModel.getAssignment(var) != res){
2071 throw ModelException(n, "Model disagrees on non-linear term.");
2072 }
2073 }
2074 return res;
2075 }
2076 }
2077
2078 default:
2079 if(isSetup(n)){
2080 ArithVar var = d_arithvarNodeMap.asArithVar(n);
2081 return d_partialModel.getAssignment(var);
2082 }else{
2083 throw ModelException(n, "Expected a setup node.");
2084 }
2085 }
2086 }
2087
2088 Rational TheoryArith::deltaValueForTotalOrder() const{
2089 Rational min(2);
2090 std::set<DeltaRational> relevantDeltaValues;
2091 context::CDQueue<Constraint>::const_iterator qiter = d_diseqQueue.begin();
2092 context::CDQueue<Constraint>::const_iterator qiter_end = d_diseqQueue.end();
2093
2094 for(; qiter != qiter_end; ++qiter){
2095 Constraint curr = *qiter;
2096
2097 const DeltaRational& rhsValue = curr->getValue();
2098 relevantDeltaValues.insert(rhsValue);
2099 }
2100
2101 for(shared_terms_iterator shared_iter = shared_terms_begin(),
2102 shared_end = shared_terms_end(); shared_iter != shared_end; ++shared_iter){
2103 Node sharedCurr = *shared_iter;
2104
2105 // ModelException is fatal as this point. Don't catch!
2106 // DeltaRationalException is fatal as this point. Don't catch!
2107 DeltaRational val = getDeltaValue(sharedCurr);
2108 relevantDeltaValues.insert(val);
2109 }
2110
2111 for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
2112 ArithVar v = *vi;
2113 const DeltaRational& value = d_partialModel.getAssignment(v);
2114 relevantDeltaValues.insert(value);
2115 if( d_partialModel.hasLowerBound(v)){
2116 const DeltaRational& lb = d_partialModel.getLowerBound(v);
2117 relevantDeltaValues.insert(lb);
2118 }
2119 if( d_partialModel.hasUpperBound(v)){
2120 const DeltaRational& ub = d_partialModel.getUpperBound(v);
2121 relevantDeltaValues.insert(ub);
2122 }
2123 }
2124
2125 if(relevantDeltaValues.size() >= 2){
2126 std::set<DeltaRational>::const_iterator iter = relevantDeltaValues.begin();
2127 std::set<DeltaRational>::const_iterator iter_end = relevantDeltaValues.end();
2128 DeltaRational prev = *iter;
2129 ++iter;
2130 for(; iter != iter_end; ++iter){
2131 const DeltaRational& curr = *iter;
2132
2133 Assert(prev < curr);
2134
2135 DeltaRational::seperatingDelta(min, prev, curr);
2136 prev = curr;
2137 }
2138 }
2139
2140 Assert(min.sgn() > 0);
2141 Rational belowMin = min/Rational(2);
2142 return belowMin;
2143 }
2144
2145 void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
2146 AlwaysAssert(d_qflraStatus == Result::SAT);
2147 //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
2148
2149 if(Debug.isOn("arith::collectModelInfo")){
2150 debugPrintFacts();
2151 }
2152
2153 Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
2154
2155
2156 // Delta lasts at least the duration of the function call
2157 const Rational& delta = d_partialModel.getDelta();
2158 std::hash_set<TNode, TNodeHashFunction> shared = currentlySharedTerms();
2159
2160 // TODO:
2161 // This is not very good for user push/pop....
2162 // Revisit when implementing push/pop
2163 for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
2164 ArithVar v = *vi;
2165 if(!isSlackVariable(v)){
2166 Node term = d_arithvarNodeMap.asNode(v);
2167
2168 if(theoryOf(term) == THEORY_ARITH || shared.find(term) != shared.end()){
2169 const DeltaRational& mod = d_partialModel.getAssignment(v);
2170 Rational qmodel = mod.substituteDelta(delta);
2171
2172 Node qNode = mkRationalNode(qmodel);
2173 Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
2174
2175 m->assertEquality(term, qNode, true);
2176 }else{
2177 Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl;
2178
2179 }
2180 }
2181 }
2182
2183 // Iterate over equivalence classes in LinearEqualityModule
2184 // const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine();
2185 // m->assertEqualityEngine(&ee);
2186
2187 Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl;
2188 }
2189
2190 bool TheoryArith::safeToReset() const {
2191 Assert(!d_tableauSizeHasBeenModified);
2192
2193 ArithPriorityQueue::const_iterator conf_iter = d_simplex.queueBegin();
2194 ArithPriorityQueue::const_iterator conf_end = d_simplex.queueEnd();
2195 for(; conf_iter != conf_end; ++conf_iter){
2196 ArithVar basic = *conf_iter;
2197 if(!d_smallTableauCopy.isBasic(basic)){
2198 return false;
2199 }
2200 }
2201
2202 return true;
2203 }
2204
2205 void TheoryArith::notifyRestart(){
2206 TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
2207
2208 if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
2209
2210 ++d_restartsCounter;
2211
2212 uint32_t currSize = d_tableau.size();
2213 uint32_t copySize = d_smallTableauCopy.size();
2214
2215 Debug("arith::reset") << "resetting" << d_restartsCounter << endl;
2216 Debug("arith::reset") << "curr " << currSize << " copy " << copySize << endl;
2217 Debug("arith::reset") << "tableauSizeHasBeenModified " << d_tableauSizeHasBeenModified << endl;
2218
2219 if(d_tableauSizeHasBeenModified){
2220 Debug("arith::reset") << "row has been added must copy " << d_restartsCounter << endl;
2221 d_smallTableauCopy = d_tableau;
2222 d_tableauSizeHasBeenModified = false;
2223 }else if( d_restartsCounter >= RESET_START){
2224 if(copySize >= currSize * 1.1 ){
2225 Debug("arith::reset") << "size has shrunk " << d_restartsCounter << endl;
2226 ++d_statistics.d_smallerSetToCurr;
2227 d_smallTableauCopy = d_tableau;
2228 }else if(d_tableauResetDensity * copySize <= currSize){
2229 d_simplex.reduceQueue();
2230 if(safeToReset()){
2231 Debug("arith::reset") << "resetting " << d_restartsCounter << endl;
2232 ++d_statistics.d_currSetToSmaller;
2233 d_tableau = d_smallTableauCopy;
2234 }else{
2235 Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter << endl;
2236 }
2237 }
2238 }
2239 Assert(unenqueuedVariablesAreConsistent());
2240 }
2241
2242 bool TheoryArith::entireStateIsConsistent(const string& s){
2243 bool result = true;
2244 for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
2245 ArithVar var = *vi;
2246 //ArithVar var = d_arithvarNodeMap.asArithVar(*i);
2247 if(!d_partialModel.assignmentIsConsistent(var)){
2248 d_partialModel.printModel(var);
2249 Warning() << s << ":" << "Assignment is not consistent for " << var << d_arithvarNodeMap.asNode(var);
2250 if(d_tableau.isBasic(var)){
2251 Warning() << " (basic)";
2252 }
2253 Warning() << endl;
2254 result = false;
2255 }
2256 }
2257 return result;
2258 }
2259
2260 bool TheoryArith::unenqueuedVariablesAreConsistent(){
2261 bool result = true;
2262 for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
2263 ArithVar var = *vi;
2264 if(!d_partialModel.assignmentIsConsistent(var)){
2265 if(!d_simplex.debugIsInCollectionQueue(var)){
2266
2267 d_partialModel.printModel(var);
2268 Warning() << "Unenqueued var is not consistent for " << var << d_arithvarNodeMap.asNode(var);
2269 if(d_tableau.isBasic(var)){
2270 Warning() << " (basic)";
2271 }
2272 Warning() << endl;
2273 result = false;
2274 } else if(Debug.isOn("arith::consistency::initial")){
2275 d_partialModel.printModel(var);
2276 Warning() << "Initial var is not consistent for " << var << d_arithvarNodeMap.asNode(var);
2277 if(d_tableau.isBasic(var)){
2278 Warning() << " (basic)";
2279 }
2280 Warning() << endl;
2281 }
2282 }
2283 }
2284 return result;
2285 }
2286
2287 void TheoryArith::presolve(){
2288 TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
2289
2290 d_statistics.d_initialTableauSize.setData(d_tableau.size());
2291
2292 if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
2293
2294 static CVC4_THREADLOCAL(unsigned) callCount = 0;
2295 if(Debug.isOn("arith::presolve")) {
2296 Debug("arith::presolve") << "TheoryArith::presolve #" << callCount << endl;
2297 callCount = callCount + 1;
2298 }
2299
2300 vector<Node> lemmas;
2301 switch(options::arithUnateLemmaMode()){
2302 case NO_PRESOLVE_LEMMAS:
2303 break;
2304 case INEQUALITY_PRESOLVE_LEMMAS:
2305 d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
2306 break;
2307 case EQUALITY_PRESOLVE_LEMMAS:
2308 d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
2309 break;
2310 case ALL_PRESOLVE_LEMMAS:
2311 d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
2312 d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
2313 break;
2314 default:
2315 Unhandled(options::arithUnateLemmaMode());
2316 }
2317
2318 vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
2319 for(; i != i_end; ++i){
2320 Node lem = *i;
2321 Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
2322 d_out->lemma(lem);
2323 }
2324
2325 // if(options::arithUnateLemmaMode() == Options::ALL_UNATE){
2326 // vector<Node> lemmas;
2327 // d_constraintDatabase.outputAllUnateLemmas(lemmas);
2328 // vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
2329 // for(; i != i_end; ++i){
2330 // Node lem = *i;
2331 // Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
2332 // d_out->lemma(lem);
2333 // }
2334 // }
2335 }
2336
2337 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
2338 if(d_qflraStatus == Result::SAT_UNKNOWN){
2339 return EQUALITY_UNKNOWN;
2340 }else{
2341 try {
2342 if (getDeltaValue(a) == getDeltaValue(b)) {
2343 return EQUALITY_TRUE_IN_MODEL;
2344 } else {
2345 return EQUALITY_FALSE_IN_MODEL;
2346 }
2347 } catch (DeltaRationalException& dr) {
2348 return EQUALITY_UNKNOWN;
2349 } catch (ModelException& me) {
2350 return EQUALITY_UNKNOWN;
2351 }
2352 }
2353 }
2354
2355 bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){
2356 ++d_statistics.d_boundComputations;
2357
2358 DeltaRational bound = upperBound ?
2359 d_linEq.computeUpperBound(basic):
2360 d_linEq.computeLowerBound(basic);
2361
2362 if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) ||
2363 (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){
2364
2365 // TODO: "Policy point"
2366 //We are only going to recreate the functionality for now.
2367 //In the future this can be improved to generate a temporary constraint
2368 //if none exists.
2369 //Experiment with doing this everytime or only when the new constraint
2370 //implies an unknown fact.
2371
2372 ConstraintType t = upperBound ? UpperBound : LowerBound;
2373 Constraint bestImplied = d_constraintDatabase.getBestImpliedBound(basic, t, bound);
2374
2375 // Node bestImplied = upperBound ?
2376 // d_apm.getBestImpliedUpperBound(basic, bound):
2377 // d_apm.getBestImpliedLowerBound(basic, bound);
2378
2379 if(bestImplied != NullConstraint){
2380 //This should be stronger
2381 Assert(!upperBound || bound <= bestImplied->getValue());
2382 Assert(!upperBound || d_partialModel.lessThanUpperBound(basic, bestImplied->getValue()));
2383
2384 Assert( upperBound || bound >= bestImplied->getValue());
2385 Assert( upperBound || d_partialModel.greaterThanLowerBound(basic, bestImplied->getValue()));
2386 //slightly changed
2387
2388 // Constraint c = d_constraintDatabase.lookup(bestImplied);
2389 // Assert(c != NullConstraint);
2390
2391 bool assertedToTheTheory = bestImplied->assertedToTheTheory();
2392 bool canBePropagated = bestImplied->canBePropagated();
2393 bool hasProof = bestImplied->hasProof();
2394
2395 Debug("arith::prop") << "arith::prop" << basic
2396 << " " << assertedToTheTheory
2397 << " " << canBePropagated
2398 << " " << hasProof
2399 << endl;
2400
2401 if(bestImplied->negationHasProof()){
2402 Warning() << "the negation of " << bestImplied << " : " << endl
2403 << "has proof " << bestImplied->getNegation() << endl
2404 << bestImplied->getNegation()->explainForConflict() << endl;
2405 }
2406
2407 if(!assertedToTheTheory && canBePropagated && !hasProof ){
2408 if(upperBound){
2409 Assert(bestImplied != d_partialModel.getUpperBoundConstraint(basic));
2410 d_linEq.propagateNonbasicsUpperBound(basic, bestImplied);
2411 }else{
2412 Assert(bestImplied != d_partialModel.getLowerBoundConstraint(basic));
2413 d_linEq.propagateNonbasicsLowerBound(basic, bestImplied);
2414 }
2415 // I think this can be skipped if canBePropagated is true
2416 //d_learnedBounds.push(bestImplied);
2417 return true;
2418 }
2419 }
2420 }
2421 return false;
2422 }
2423
2424 void TheoryArith::propagateCandidate(ArithVar basic){
2425 bool success = false;
2426 if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasLowerBounds(basic)){
2427 success |= propagateCandidateLowerBound(basic);
2428 }
2429 if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasUpperBounds(basic)){
2430 success |= propagateCandidateUpperBound(basic);
2431 }
2432 if(success){
2433 ++d_statistics.d_boundPropagations;
2434 }
2435 }
2436
2437 void TheoryArith::propagateCandidates(){
2438 TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
2439
2440 Assert(d_candidateBasics.empty());
2441
2442 if(d_updatedBounds.empty()){ return; }
2443
2444 DenseSet::const_iterator i = d_updatedBounds.begin();
2445 DenseSet::const_iterator end = d_updatedBounds.end();
2446 for(; i != end; ++i){
2447 ArithVar var = *i;
2448 if(d_tableau.isBasic(var) &&
2449 d_tableau.getRowLength(d_tableau.basicToRowIndex(var)) <= options::arithPropagateMaxLength()){
2450 d_candidateBasics.softAdd(var);
2451 }else{
2452 Tableau::ColIterator basicIter = d_tableau.colIterator(var);
2453 for(; !basicIter.atEnd(); ++basicIter){
2454 const Tableau::Entry& entry = *basicIter;
2455 RowIndex ridx = entry.getRowIndex();
2456 ArithVar rowVar = d_tableau.rowIndexToBasic(ridx);
2457 Assert(entry.getColVar() == var);
2458 Assert(d_tableau.isBasic(rowVar));
2459 if(d_tableau.getRowLength(ridx) <= options::arithPropagateMaxLength()){
2460 d_candidateBasics.softAdd(rowVar);
2461 }
2462 }
2463 }
2464 }
2465 d_updatedBounds.purge();
2466
2467 while(!d_candidateBasics.empty()){
2468 ArithVar candidate = d_candidateBasics.back();
2469 d_candidateBasics.pop_back();
2470 Assert(d_tableau.isBasic(candidate));
2471 propagateCandidate(candidate);
2472 }
2473 }
2474
2475 }/* CVC4::theory::arith namespace */
2476 }/* CVC4::theory namespace */
2477 }/* CVC4 namespace */