src/theory/arith/theory_arith_private.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 "theory/arith/theory_arith_private.h"
  19
  20 #include "expr/node.h"
  21 #include "expr/kind.h"
  22 #include "expr/metakind.h"
  23 #include "expr/node_builder.h"
  24
  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"
  30
  31 #include "theory/valuation.h"
  32 #include "theory/rewriter.h"
  33
  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"
  40
  41 #include "smt/logic_exception.h"
  42
  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"
  53
  54 #include "theory/arith/approx_simplex.h"
  55 #include "theory/arith/constraint.h"
  56
  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"
  61
  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"
  67
  68 #include "theory/arith/options.h"
  69
  70 #include "theory/quantifiers/bounded_integers.h"
  71
  72 #include <stdint.h>
  73
  74 #include <vector>
  75 #include <map>
  76 #include <queue>
  77
  78 using namespace std;
  79 using namespace CVC4::kind;
  80
  81 namespace CVC4 {
  82 namespace theory {
  83 namespace arith {
  84
  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),
  88   d_rowTracking(),
  89   d_constraintDatabase(c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this)),
  90   d_qflraStatus(Result::SAT_UNKNOWN),
  91   d_unknownsInARow(0),
  92   d_hasDoneWorkSinceCut(false),
  93   d_learner(u),
  94   d_quantEngine(qe),
  95   d_assertionsThatDoNotMatchTheirLiterals(c),
  96   d_nextIntegerCheckVar(0),
  97   d_constantIntegerVariables(c),
  98   d_diseqQueue(c, false),
  99   d_currentPropagationList(),
 100   d_learnedBounds(c),
 101   d_partialModel(c, DeltaComputeCallback(*this)),
 102   d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)),
 103   d_tableau(),
 104   d_linEq(d_partialModel, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)),
 105   d_diosolver(c),
 106   d_restartsCounter(0),
 107   d_tableauSizeHasBeenModified(false),
 108   d_tableauResetDensity(1.6),
 109   d_tableauResetPeriod(10),
 110   d_conflicts(c),
 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)),
 116   d_DELTA_ZERO(0),
 117   d_fullCheckCounter(0),
 118   d_cutCount(c, 0),
 119   d_cutInContext(c),
 120   d_likelyIntegerInfeasible(c, false),
 121   d_guessedCoeffSet(c, false),
 122   d_guessedCoeffs(),
 123   d_statistics()
 124 {
 125   srand(79);
 126 }
 127
 128 TheoryArithPrivate::~TheoryArithPrivate(){ }
 129
 130
 131 void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 132   d_congruenceManager.setMasterEqualityEngine(eq);
 133 }
 134
 135 Node TheoryArithPrivate::getRealDivideBy0Func(){
 136   Assert(!getLogicInfo().isLinear());
 137   Assert(getLogicInfo().areRealsUsed());
 138
 139   if(d_realDivideBy0Func.isNull()){
 140     TypeNode realType = NodeManager::currentNM()->realType();
 141     d_realDivideBy0Func = skolemFunction("/by0_$$", realType, realType);
 142   }
 143   return d_realDivideBy0Func;
 144 }
 145
 146 Node TheoryArithPrivate::getIntDivideBy0Func(){
 147   Assert(!getLogicInfo().isLinear());
 148   Assert(getLogicInfo().areIntegersUsed());
 149
 150   if(d_intDivideBy0Func.isNull()){
 151     TypeNode intType = NodeManager::currentNM()->integerType();
 152     d_intDivideBy0Func = skolemFunction("divby0_$$", intType, intType);
 153   }
 154   return d_intDivideBy0Func;
 155 }
 156
 157 Node TheoryArithPrivate::getIntModulusBy0Func(){
 158   Assert(!getLogicInfo().isLinear());
 159   Assert(getLogicInfo().areIntegersUsed());
 160
 161   if(d_intModulusBy0Func.isNull()){
 162     TypeNode intType = NodeManager::currentNM()->integerType();
 163     d_intModulusBy0Func = skolemFunction("modby0_$$", intType, intType);
 164   }
 165   return d_intModulusBy0Func;
 166 }
 167
 168 TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg) throw (){
 169   stringstream ss;
 170   ss << "Cannot construct a model for " << n << " as " << endl << msg;
 171   setMessage(ss.str());
 172 }
 173 TheoryArithPrivate::ModelException::~ModelException() throw (){ }
 174
 175
 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")
 204 {
 205   StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
 206   StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
 207
 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);
 214
 215   StatisticsRegistry::registerStat(&d_presolveTime);
 216   StatisticsRegistry::registerStat(&d_newPropTime);
 217
 218   StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
 219
 220   StatisticsRegistry::registerStat(&d_initialTableauSize);
 221   StatisticsRegistry::registerStat(&d_currSetToSmaller);
 222   StatisticsRegistry::registerStat(&d_smallerSetToCurr);
 223   StatisticsRegistry::registerStat(&d_restartTimer);
 224
 225   StatisticsRegistry::registerStat(&d_boundComputationTime);
 226   StatisticsRegistry::registerStat(&d_boundComputations);
 227   StatisticsRegistry::registerStat(&d_boundPropagations);
 228
 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);
 235
 236
 237   StatisticsRegistry::registerStat(&d_satPivots);
 238   StatisticsRegistry::registerStat(&d_unsatPivots);
 239   StatisticsRegistry::registerStat(&d_unknownPivots);
 240 }
 241
 242 TheoryArithPrivate::Statistics::~Statistics(){
 243   StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts);
 244   StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts);
 245
 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);
 252
 253   StatisticsRegistry::unregisterStat(&d_presolveTime);
 254   StatisticsRegistry::unregisterStat(&d_newPropTime);
 255
 256   StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
 257
 258   StatisticsRegistry::unregisterStat(&d_initialTableauSize);
 259   StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
 260   StatisticsRegistry::unregisterStat(&d_smallerSetToCurr);
 261   StatisticsRegistry::unregisterStat(&d_restartTimer);
 262
 263   StatisticsRegistry::unregisterStat(&d_boundComputationTime);
 264   StatisticsRegistry::unregisterStat(&d_boundComputations);
 265   StatisticsRegistry::unregisterStat(&d_boundPropagations);
 266
 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);
 273
 274   StatisticsRegistry::unregisterStat(&d_satPivots);
 275   StatisticsRegistry::unregisterStat(&d_unsatPivots);
 276   StatisticsRegistry::unregisterStat(&d_unknownPivots);
 277 }
 278
 279 void TheoryArithPrivate::revertOutOfConflict(){
 280   d_partialModel.revertAssignmentChanges();
 281   clearUpdates();
 282   d_currentPropagationList.clear();
 283 }
 284
 285 void TheoryArithPrivate::clearUpdates(){
 286   d_updatedBounds.purge();
 287 }
 288
 289 void TheoryArithPrivate::zeroDifferenceDetected(ArithVar x){
 290   Assert(d_congruenceManager.isWatchedVariable(x));
 291   Assert(d_partialModel.upperBoundIsZero(x));
 292   Assert(d_partialModel.lowerBoundIsZero(x));
 293
 294   Constraint lb = d_partialModel.getLowerBoundConstraint(x);
 295   Constraint ub = d_partialModel.getUpperBoundConstraint(x);
 296
 297   if(lb->isEquality()){
 298     d_congruenceManager.watchedVariableIsZero(lb);
 299   }else if(ub->isEquality()){
 300     d_congruenceManager.watchedVariableIsZero(ub);
 301   }else{
 302     d_congruenceManager.watchedVariableIsZero(lb, ub);
 303   }
 304 }
 305
 306 /* procedure AssertLower( x_i >= c_i ) */
 307 bool TheoryArithPrivate::AssertLower(Constraint constraint){
 308   Assert(constraint != NullConstraint);
 309   Assert(constraint->isLowerBound());
 310
 311   ArithVar x_i = constraint->getVariable();
 312   const DeltaRational& c_i = constraint->getValue();
 313
 314   Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
 315
 316   Assert(!isInteger(x_i) || c_i.isIntegral());
 317
 318   //TODO Relax to less than?
 319   if(d_partialModel.lessThanLowerBound(x_i, c_i)){
 320     return false; //sat
 321   }
 322
 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);
 330     return true;
 331   }else if(cmpToUB == 0){
 332     if(isInteger(x_i)){
 333       d_constantIntegerVariables.push_back(x_i);
 334       Debug("dio::push") << x_i << endl;
 335     }
 336     Constraint ub = d_partialModel.getUpperBoundConstraint(x_i);
 337
 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);
 343     }
 344
 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();
 350       if(diseq->isTrue()){
 351         //const Constraint ub = vc.getUpperBound();
 352         Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
 353
 354         ++(d_statistics.d_statDisequalityConflicts);
 355         Debug("eq") << " assert lower conflict " << conflict << endl;
 356         raiseConflict(conflict);
 357         return true;
 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
 362       }
 363     }
 364   }else{
 365     Assert(cmpToUB < 0);
 366     const ValueCollection& vc = constraint->getValueCollection();
 367
 368     if(vc.hasDisequality()){
 369       const Constraint diseq = vc.getDisequality();
 370       if(diseq->isTrue()){
 371         const Constraint ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
 372
 373         if(ub->hasProof()){
 374           Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
 375           Debug("eq") << " assert upper conflict " << conflict << endl;
 376           raiseConflict(conflict);
 377           return true;
 378         }else if(!ub->negationHasProof()){
 379           Constraint negUb = ub->getNegation();
 380           negUb->impliedBy(constraint, diseq);
 381           d_learnedBounds.push_back(negUb);
 382         }
 383       }
 384     }
 385   }
 386
 387   d_currentPropagationList.push_back(constraint);
 388   d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
 389
 390   d_partialModel.setLowerBoundConstraint(constraint);
 391
 392   if(d_congruenceManager.isWatchedVariable(x_i)){
 393     int sgn = c_i.sgn();
 394     if(sgn > 0){
 395       d_congruenceManager.watchedVariableCannotBeZero(constraint);
 396     }else if(sgn == 0 && d_partialModel.upperBoundIsZero(x_i)){
 397       zeroDifferenceDetected(x_i);
 398     }
 399   }
 400
 401   d_updatedBounds.softAdd(x_i);
 402
 403   if(Debug.isOn("model")) {
 404     Debug("model") << "before" << endl;
 405     d_partialModel.printModel(x_i);
 406     d_tableau.debugPrintIsBasic(x_i);
 407   }
 408
 409   if(!d_tableau.isBasic(x_i)){
 410     if(d_partialModel.getAssignment(x_i) < c_i){
 411       d_linEq.update(x_i, c_i);
 412     }
 413   }else{
 414     d_errorSet.signalVariable(x_i);
 415   }
 416
 417   if(Debug.isOn("model")) {
 418     Debug("model") << "after" << endl;
 419     d_partialModel.printModel(x_i);
 420     d_tableau.debugPrintIsBasic(x_i);
 421  }
 422
 423   return false; //sat
 424 }
 425
 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();
 430
 431   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
 432   AssertArgument(constraint != NullConstraint,
 433                  "AssertUpper() called on a NullConstraint.");
 434   Assert(constraint->isUpperBound());
 435
 436   //Too strong because of rounding with integers
 437   //Assert(!constraint->hasLiteral() || original == constraint->getLiteral());
 438   Assert(!isInteger(x_i) || c_i.isIntegral());
 439
 440   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
 441
 442   if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
 443     return false; //sat
 444   }
 445
 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);
 454     return true;
 455   }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
 456     if(isInteger(x_i)){
 457       d_constantIntegerVariables.push_back(x_i);
 458       Debug("dio::push") << x_i << endl;
 459     }
 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);
 466     }
 467
 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();
 473       if(diseq->isTrue()){
 474         Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
 475         Debug("eq") << " assert upper conflict " << conflict << endl;
 476         raiseConflict(conflict);
 477         return true;
 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
 482       }
 483     }
 484   }else if(cmpToLB > 0){
 485     const ValueCollection& vc = constraint->getValueCollection();
 486     if(vc.hasDisequality()){
 487       const Constraint diseq = vc.getDisequality();
 488       if(diseq->isTrue()){
 489         const Constraint lb =
 490           d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
 491         if(lb->hasProof()){
 492           Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
 493           Debug("eq") << " assert upper conflict " << conflict << endl;
 494           raiseConflict(conflict);
 495           return true;
 496         }else if(!lb->negationHasProof()){
 497           Constraint negLb = lb->getNegation();
 498           negLb->impliedBy(constraint, diseq);
 499           d_learnedBounds.push_back(negLb);
 500         }
 501       }
 502     }
 503   }
 504
 505   d_currentPropagationList.push_back(constraint);
 506   d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
 507   //It is fine if this is NullConstraint
 508
 509   d_partialModel.setUpperBoundConstraint(constraint);
 510
 511   if(d_congruenceManager.isWatchedVariable(x_i)){
 512     int sgn = c_i.sgn();
 513      if(sgn < 0){
 514        d_congruenceManager.watchedVariableCannotBeZero(constraint);
 515      }else if(sgn == 0 && d_partialModel.lowerBoundIsZero(x_i)){
 516        zeroDifferenceDetected(x_i);
 517      }
 518   }
 519
 520   d_updatedBounds.softAdd(x_i);
 521
 522   if(Debug.isOn("model")) {
 523     Debug("model") << "before" << endl;
 524     d_partialModel.printModel(x_i);
 525     d_tableau.debugPrintIsBasic(x_i);
 526   }
 527
 528   if(!d_tableau.isBasic(x_i)){
 529     if(d_partialModel.getAssignment(x_i) > c_i){
 530       d_linEq.update(x_i, c_i);
 531     }
 532   }else{
 533     d_errorSet.signalVariable(x_i);
 534   }
 535
 536   if(Debug.isOn("model")) {
 537     Debug("model") << "after" << endl;
 538     d_partialModel.printModel(x_i);
 539     d_tableau.debugPrintIsBasic(x_i);
 540   }
 541
 542   return false; //sat
 543 }
 544
 545
 546 /* procedure AssertEquality( x_i == c_i ) */
 547 bool TheoryArithPrivate::AssertEquality(Constraint constraint){
 548   AssertArgument(constraint != NullConstraint,
 549                  "AssertUpper() called on a NullConstraint.");
 550
 551   ArithVar x_i = constraint->getVariable();
 552   const DeltaRational& c_i = constraint->getValue();
 553
 554   Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
 555
 556   //Should be fine in integers
 557   Assert(!isInteger(x_i) || c_i.isIntegral());
 558
 559   int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
 560   int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
 561
 562   // u_i <= c_i <= l_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){
 565     return false; //sat
 566   }
 567
 568   if(cmpToUB > 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);
 573     return true;
 574   }
 575
 576   if(cmpToLB < 0){
 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);
 581     return true;
 582   }
 583
 584   Assert(cmpToUB <= 0);
 585   Assert(cmpToLB >= 0);
 586   Assert(cmpToUB < 0 || cmpToLB > 0);
 587
 588
 589   if(isInteger(x_i)){
 590     d_constantIntegerVariables.push_back(x_i);
 591     Debug("dio::push") << x_i << endl;
 592   }
 593
 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));
 599
 600   d_partialModel.setUpperBoundConstraint(constraint);
 601   d_partialModel.setLowerBoundConstraint(constraint);
 602
 603   if(d_congruenceManager.isWatchedVariable(x_i)){
 604     int sgn = c_i.sgn();
 605     if(sgn == 0){
 606       zeroDifferenceDetected(x_i);
 607     }else{
 608       d_congruenceManager.watchedVariableCannotBeZero(constraint);
 609       d_congruenceManager.equalsConstant(constraint);
 610     }
 611   }else{
 612     d_congruenceManager.equalsConstant(constraint);
 613   }
 614
 615   d_updatedBounds.softAdd(x_i);
 616
 617   if(Debug.isOn("model")) {
 618     Debug("model") << "before" << endl;
 619     d_partialModel.printModel(x_i);
 620     d_tableau.debugPrintIsBasic(x_i);
 621   }
 622
 623   if(!d_tableau.isBasic(x_i)){
 624     if(!(d_partialModel.getAssignment(x_i) == c_i)){
 625       d_linEq.update(x_i, c_i);
 626     }
 627   }else{
 628     d_errorSet.signalVariable(x_i);
 629   }
 630
 631   if(Debug.isOn("model")) {
 632     Debug("model") << "after" << endl;
 633     d_partialModel.printModel(x_i);
 634     d_tableau.debugPrintIsBasic(x_i);
 635   }
 636
 637   return false;
 638 }
 639
 640
 641 /* procedure AssertDisequality( x_i != c_i ) */
 642 bool TheoryArithPrivate::AssertDisequality(Constraint constraint){
 643
 644   AssertArgument(constraint != NullConstraint,
 645                  "AssertUpper() called on a NullConstraint.");
 646   ArithVar x_i = constraint->getVariable();
 647   const DeltaRational& c_i = constraint->getValue();
 648
 649   Debug("arith") << "AssertDisequality(" << x_i << " " << c_i << ")"<< std::endl;
 650
 651   //Should be fine in integers
 652   Assert(!isInteger(x_i) || c_i.isIntegral());
 653
 654   if(d_congruenceManager.isWatchedVariable(x_i)){
 655     int sgn = c_i.sgn();
 656     if(sgn == 0){
 657       d_congruenceManager.watchedVariableCannotBeZero(constraint);
 658     }
 659   }
 660
 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()){
 666       //in conflict
 667       Debug("eq") << "explaining" << endl;
 668       ++(d_statistics.d_statDisequalityConflicts);
 669       Node conflict = ConstraintValue::explainConflict(constraint, lb, ub);
 670       raiseConflict(conflict);
 671       return true;
 672     }
 673   }
 674   if(vc.hasLowerBound() ){
 675     const Constraint lb = vc.getLowerBound();
 676     if(lb->isTrue()){
 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);
 683       }
 684     }
 685   }
 686   if(vc.hasUpperBound()){
 687     const Constraint ub = vc.getUpperBound();
 688     if(ub->isTrue()){
 689       const Constraint lb = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
 690
 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);
 696       }
 697     }
 698   }
 699
 700   bool split = constraint->isSplit();
 701
 702   if(!split && c_i == d_partialModel.getAssignment(x_i)){
 703     Debug("eq") << "lemma now! " << constraint << endl;
 704     outputLemma(constraint->split());
 705     return false;
 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;
 710   }else if(!split){
 711     Debug("eq") << "push back" << constraint << endl;
 712     d_diseqQueue.push(constraint);
 713     d_partialModel.invalidateDelta();
 714   }else{
 715     Debug("eq") << "skipping already split " << constraint << endl;
 716   }
 717   return false;
 718 }
 719
 720 void TheoryArithPrivate::addSharedTerm(TNode n){
 721   Debug("arith::addSharedTerm") << "addSharedTerm: " << n << endl;
 722   if(n.isConst()){
 723     d_partialModel.invalidateDelta();
 724   }
 725
 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) {
 732       Monomial m = *it;
 733       if (!m.isConstant() && !isSetup(m.getVarList().getNode())) {
 734         setupVariableList(m.getVarList());
 735       }
 736     }
 737   }
 738 }
 739
 740 namespace attr {
 741   struct ToIntegerTag { };
 742   struct LinearIntDivTag { };
 743 }/* CVC4::theory::arith::attr namespace */
 744
 745 /**
 746  * This attribute maps the child of a to_int / is_int to the
 747  * corresponding integer skolem.
 748  */
 749 typedef expr::Attribute<attr::ToIntegerTag, Node> ToIntegerAttr;
 750
 751 /**
 752  * This attribute maps division-by-constant-k terms to a variable
 753  * used to eliminate them.
 754  */
 755 typedef expr::Attribute<attr::LinearIntDivTag, Node> LinearIntDivAttr;
 756
 757 Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
 758   if(Theory::theoryOf(n) != THEORY_ARITH) {
 759     return n;
 760   }
 761
 762   NodeManager* nm = NodeManager::currentNM();
 763
 764   switch(Kind k = n.getKind()) {
 765
 766   case kind::TO_INTEGER:
 767   case kind::IS_INTEGER: {
 768     Node intVar;
 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])));
 773     }
 774     if(n.getKind() == kind::TO_INTEGER) {
 775       Node node = intVar;
 776       return node;
 777     } else {
 778       Node node = nm->mkNode(kind::EQUAL, node[0], intVar);
 779       return node;
 780     }
 781     Unreachable();
 782   }
 783
 784   case kind::INTS_DIVISION:
 785   case kind::INTS_DIVISION_TOTAL: {
 786     if(!options::rewriteDivk()) {
 787       return n;
 788     }
 789     Node num = Rewriter::rewrite(n[0]);
 790     Node den = Rewriter::rewrite(n[1]);
 791     if(den.isConst()) {
 792       const Rational& rat = den.getConst<Rational>();
 793       Assert(!num.isConst());
 794       if(rat != 0) {
 795         Node intVar;
 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);
 800           if(rat > 0) {
 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)))))));
 802           } else {
 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)))))));
 804           }
 805         }
 806         return intVar;
 807       }
 808     }
 809     break;
 810   }
 811
 812   case kind::INTS_MODULUS:
 813   case kind::INTS_MODULUS_TOTAL: {
 814     if(!options::rewriteDivk()) {
 815       return n;
 816     }
 817     Node num = Rewriter::rewrite(n[0]);
 818     Node den = Rewriter::rewrite(n[1]);
 819     if(den.isConst()) {
 820       const Rational& rat = den.getConst<Rational>();
 821       Assert(!num.isConst());
 822       if(rat != 0) {
 823         Node intVar;
 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);
 828           if(rat > 0) {
 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)))))));
 830           } else {
 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)))))));
 832           }
 833         }
 834         Node node = nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar));
 835         return node;
 836       }
 837     }
 838     break;
 839   }
 840
 841   default:
 842     ;
 843   }
 844
 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);
 850       b << rewritten;
 851       for(++i; i != n.end(); ++i) {
 852         b << ppRewriteTerms(*i);
 853       }
 854       rewritten = b;
 855       return rewritten;
 856     }
 857   }
 858
 859   return n;
 860 }
 861
 862 Node TheoryArithPrivate::ppRewrite(TNode atom) {
 863   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 864
 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;
 873     return rewritten;
 874   } else {
 875     return ppRewriteTerms(atom);
 876   }
 877 }
 878
 879 Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
 880   TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
 881   Debug("simplify") << "TheoryArithPrivate::solve(" << in << ")" << endl;
 882
 883
 884   // Solve equalities
 885   Rational minConstant = 0;
 886   Node minMonomial;
 887   Node minVar;
 888   if (in.getKind() == kind::EQUAL) {
 889     Comparison cmp = Comparison::parseNormalForm(in);
 890
 891     Polynomial left = cmp.getLeft();
 892     Polynomial right = cmp.getRight();
 893
 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()){
 901           minVar = var;
 902         }
 903       }
 904     }
 905
 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));
 914
 915
 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;
 925
 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;
 932
 933         outSubstitutions.addSubstitution(minVar, elim);
 934         return Theory::PP_ASSERT_STATUS_SOLVED;
 935       } else {
 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;
 938
 939       }
 940     }
 941   }
 942
 943   // If a relation, remember the bound
 944   switch(in.getKind()) {
 945   case kind::LEQ:
 946   case kind::LT:
 947   case kind::GEQ:
 948   case kind::GT:
 949     if (in[0].isVar()) {
 950       d_learner.addBound(in);
 951     }
 952     break;
 953   default:
 954     // Do nothing
 955     break;
 956   }
 957
 958   return Theory::PP_ASSERT_STATUS_UNSOLVED;
 959 }
 960
 961 void TheoryArithPrivate::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 962   TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
 963
 964   d_learner.staticLearning(n, learned);
 965 }
 966
 967
 968
 969 ArithVar TheoryArithPrivate::findShortestBasicRow(ArithVar variable){
 970   ArithVar bestBasic = ARITHVAR_SENTINEL;
 971   uint64_t bestRowLength = std::numeric_limits<uint64_t>::max();
 972
 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)){
 982       bestBasic = basic;
 983       bestRowLength = rowLength;
 984     }
 985   }
 986   Assert(bestBasic == ARITHVAR_SENTINEL || bestRowLength < std::numeric_limits<uint32_t>::max());
 987   return bestBasic;
 988 }
 989
 990 void TheoryArithPrivate::setupVariable(const Variable& x){
 991   Node n = x.getNode();
 992
 993   Assert(!isSetup(n));
 994
 995   ++(d_statistics.d_statUserVariables);
 996   requestArithVar(n,false);
 997   //ArithVar varN = requestArithVar(n,false);
 998   //setupInitialValue(varN);
 999
1000   markSetup(n);
1001
1002
1003   if(x.isDivLike()){
1004     setupDivLike(x);
1005   }
1006
1007 }
1008
1009 void TheoryArithPrivate::setupVariableList(const VarList& vl){
1010   Assert(!vl.empty());
1011
1012   TNode vlNode = vl.getNode();
1013   Assert(!isSetup(vlNode));
1014   Assert(!d_partialModel.hasArithVar(vlNode));
1015
1016   for(VarList::iterator i = vl.begin(), end = vl.end(); i != end; ++i){
1017     Variable var = *i;
1018
1019     if(!isSetup(var.getNode())){
1020       setupVariable(var);
1021     }
1022   }
1023
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.");
1029     }
1030
1031     setIncomplete();
1032     d_nlIncomplete = true;
1033
1034     ++(d_statistics.d_statUserVariables);
1035     requestArithVar(vlNode, false);
1036     //ArithVar av = requestArithVar(vlNode, false);
1037     //setupInitialValue(av);
1038
1039     markSetup(vlNode);
1040   }
1041
1042   /* Note:
1043    * Only call markSetup if the VarList is not a singleton.
1044    * See the comment in setupPolynomail for more.
1045    */
1046 }
1047
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);
1054       }
1055     }
1056   }else if(!isSetup(p.getNode())){
1057     setupPolynomial(p);
1058   }
1059 }
1060
1061 void TheoryArithPrivate::setupDivLike(const Variable& v){
1062   Assert(v.isDivLike());
1063
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.");
1066   }
1067
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]);
1072
1073   cautiousSetupPolynomial(m);
1074   cautiousSetupPolynomial(n);
1075
1076   Node lem;
1077   switch(vnode.getKind()){
1078   case DIVISION:
1079   case INTS_DIVISION:
1080   case INTS_MODULUS:
1081     lem = definingIteForDivLike(vnode);
1082     break;
1083   case DIVISION_TOTAL:
1084     lem = axiomIteForTotalDivision(vnode);
1085     break;
1086   case INTS_DIVISION_TOTAL:
1087   case INTS_MODULUS_TOTAL:
1088     lem = axiomIteForTotalIntDivision(vnode);
1089     break;
1090   default:
1091     /* intentionally blank */
1092     break;
1093   }
1094
1095   if(!lem.isNull()){
1096     Debug("arith::div") << lem << endl;
1097     outputLemma(lem);
1098   }
1099 }
1100
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))
1105   //  (=
1106   //   (DIVISION n d)
1107   //   (ite (= d 0)
1108   //    (APPLY [div_0_skolem_function] n)
1109   //    (DIVISION_TOTAL x y))))
1110
1111   Polynomial n = Polynomial::parsePolynomial(divLike[0]);
1112   Polynomial d = Polynomial::parsePolynomial(divLike[1]);
1113
1114   NodeManager* currNM = NodeManager::currentNM();
1115   Node dEq0 = currNM->mkNode(EQUAL, d.getNode(), mkRationalNode(0));
1116
1117   Kind kTotal = (k == DIVISION) ? DIVISION_TOTAL :
1118     (k == INTS_DIVISION) ? INTS_DIVISION_TOTAL : INTS_MODULUS_TOTAL;
1119
1120   Node by0Func = (k == DIVISION) ?  getRealDivideBy0Func():
1121     (k == INTS_DIVISION) ? getIntDivideBy0Func() : getIntModulusBy0Func();
1122
1123
1124   Debug("arith::div") << divLike << endl;
1125   Debug("arith::div") << by0Func << endl;
1126
1127   Node divTotal = currNM->mkNode(kTotal, n.getNode(), d.getNode());
1128   Node divZero = currNM->mkNode(APPLY_UF, by0Func, n.getNode());
1129
1130   Node defining = divLike.eqNode(dEq0.iteNode( divZero, divTotal));
1131
1132   return defining;
1133 }
1134
1135 Node TheoryArithPrivate::axiomIteForTotalDivision(Node div_tot){
1136   Assert(div_tot.getKind() == DIVISION_TOTAL);
1137
1138   // Inverse of multiplication axiom:
1139   //   (for all ((n Real) (d Real))
1140   //    (ite (= d 0)
1141   //     (= (DIVISION_TOTAL n d) 0)
1142   //     (= (* d (DIVISION_TOTAL n d)) n)))
1143
1144
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);
1148
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());
1153
1154   return ite;
1155 }
1156
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);
1160
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))))))
1166
1167   // Updated for div 0 functions
1168   // (for all ((m Int) (n Int))
1169   //   (let ((q (div m n)) (r (mod m n)))
1170   //     (ite (= n 0)
1171   //          (and (= q (div_0_func m)) (= r (mod_0_func m)))
1172   //          (and (= m (+ (* n q) r))
1173   //               (<= 0 r (- (abs n) 1)))))))
1174
1175   Polynomial n = Polynomial::parsePolynomial(int_div_like[0]);
1176   Polynomial d = Polynomial::parsePolynomial(int_div_like[1]);
1177
1178   NodeManager* currNM = NodeManager::currentNM();
1179   Node zero = mkRationalNode(0);
1180
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());
1183
1184   Node dEq0 = (d.getNode()).eqNode(zero);
1185   Node qEq0 = q.eqNode(zero);
1186   Node rEq0 = r.eqNode(zero);
1187
1188   Polynomial rp = Polynomial::parsePolynomial(r);
1189   Polynomial qp = Polynomial::parsePolynomial(q);
1190
1191   Node abs_d = (n.isConstant()) ?
1192     d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs_$$");
1193
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);
1197
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;
1202
1203   return lem;
1204 }
1205
1206
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));
1212
1213   for(Polynomial::iterator i = poly.begin(), end = poly.end(); i != end; ++i){
1214     Monomial mono = *i;
1215     const VarList& vl = mono.getVarList();
1216     if(!isSetup(vl.getNode())){
1217       setupVariableList(vl);
1218     }
1219   }
1220
1221   if(polyNode.getKind() == PLUS){
1222     d_tableauSizeHasBeenModified = true;
1223
1224     vector<ArithVar> variables;
1225     vector<Rational> coefficients;
1226     asVectors(poly, coefficients, variables);
1227
1228     ArithVar varSlack = requestArithVar(polyNode, true);
1229     d_tableau.addRow(varSlack, coefficients, variables);
1230     setupBasicValue(varSlack);
1231     d_linEq.trackRowIndex(d_tableau.basicToRowIndex(varSlack));
1232
1233     //Add differences to the difference manager
1234     Polynomial::iterator i = poly.begin(), end = poly.end();
1235     if(i != end){
1236       Monomial first = *i;
1237       ++i;
1238       if(i != end){
1239         Monomial second = *i;
1240         ++i;
1241         if(i == end){
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());
1247             }
1248           }
1249         }
1250       }
1251     }
1252
1253     ++(d_statistics.d_statSlackVariables);
1254     markSetup(polyNode);
1255   }
1256
1257   /* Note:
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.
1262    */
1263 }
1264
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));
1270
1271   Comparison cmp = Comparison::parseNormalForm(atom);
1272   Polynomial nvp = cmp.normalizedVariablePart();
1273   Assert(!nvp.isZero());
1274
1275   if(!isSetup(nvp.getNode())){
1276     setupPolynomial(nvp);
1277   }
1278
1279   d_constraintDatabase.addLiteral(atom);
1280
1281   markSetup(atom);
1282 }
1283
1284 void TheoryArithPrivate::preRegisterTerm(TNode n) {
1285   Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
1286
1287   try {
1288     if(isRelationOperator(n.getKind())){
1289       if(!isSetup(n)){
1290         setupAtom(n);
1291       }
1292       Constraint c = d_constraintDatabase.lookup(n);
1293       Assert(c != NullConstraint);
1294
1295       Debug("arith::preregister") << "setup constraint" << c << endl;
1296       Assert(!c->canBePropagated());
1297       c->setPreregistered();
1298     }
1299   } catch(LogicException& le) {
1300     std::stringstream ss;
1301     ss << le.getMessage() << endl << "The fact in question: " << n << endl;
1302     throw LogicException(ss.str());
1303   }
1304
1305   Debug("arith::preregister") << "end arith::preRegisterTerm("<< n <<")" << endl;
1306 }
1307
1308 void TheoryArithPrivate::releaseArithVar(ArithVar v){
1309   Assert(d_partialModel.hasNode(v));
1310
1311   d_constraintDatabase.removeVariable(v);
1312   d_partialModel.releaseArithVar(v);
1313 }
1314
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)){
1319     stringstream ss;
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());
1323   }
1324   Assert(!d_partialModel.hasArithVar(x));
1325   Assert(x.getType().isReal()); // real or integer
1326
1327   ArithVar max = d_partialModel.getNumberOfVariables();
1328   ArithVar varX = d_partialModel.allocate(x, slack);
1329
1330   bool reclaim =  max >= d_partialModel.getNumberOfVariables();;
1331
1332   if(!reclaim){
1333     d_dualSimplex.increaseMax();
1334
1335     d_tableau.increaseSize();
1336     d_tableauSizeHasBeenModified = true;
1337   }
1338   d_constraintDatabase.addVariable(varX);
1339
1340   Debug("arith::arithvar") << x << " |-> " << varX << endl;
1341
1342   Assert(!d_partialModel.hasUpperBound(varX));
1343   Assert(!d_partialModel.hasLowerBound(varX));
1344
1345   return varX;
1346 }
1347
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();
1353
1354     Node n = variable.getNode();
1355
1356     Debug("rewriter") << "should be var: " << n << endl;
1357
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));
1361
1362     Assert(d_partialModel.hasArithVar(n));
1363     ArithVar av = d_partialModel.asArithVar(n);
1364
1365     coeffs.push_back(constant.getValue());
1366     variables.push_back(av);
1367   }
1368 }
1369
1370 /* Requirements:
1371  * For basic variables the row must have been added to the tableau.
1372  */
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.
1377
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);
1383
1384   Debug("arith") << "setupVariable("<<x<<")"<<std::endl;
1385 }
1386
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);
1393 }
1394
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);
1400 }
1401
1402
1403 bool TheoryArithPrivate::canSafelyAvoidEqualitySetup(TNode equality){
1404   Assert(equality.getKind() == EQUAL);
1405   return d_partialModel.hasArithVar(equality[0]);
1406 }
1407
1408 Comparison TheoryArithPrivate::mkIntegerEqualityFromAssignment(ArithVar v){
1409   const DeltaRational& beta = d_partialModel.getAssignment(v);
1410
1411   Assert(beta.isIntegral());
1412   Polynomial betaAsPolynomial( Constant::mkConstant(beta.floor()) );
1413
1414   TNode var = d_partialModel.asNode(v);
1415   Polynomial varAsPolynomial = Polynomial::parsePolynomial(var);
1416   return Comparison::mkComparison(EQUAL, varAsPolynomial, betaAsPolynomial);
1417 }
1418
1419 Node TheoryArithPrivate::dioCutting(){
1420   context::Context::ScopedPush speculativePush(getSatContext());
1421   //DO NOT TOUCH THE OUTPUTSTREAM
1422
1423   for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
1424     ArithVar v = *vi;
1425     if(isInteger(v)){
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
1437         }
1438       }
1439     }
1440   }
1441
1442   SumPair plane = d_diosolver.processEquationsForCut();
1443   if(plane.isZero()){
1444     return Node::null();
1445   }else{
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());
1451     Assert(gcd > 1);
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;
1461   }
1462 }
1463
1464 Node TheoryArithPrivate::callDioSolver(){
1465   while(!d_constantIntegerVariables.empty()){
1466     ArithVar v = d_constantIntegerVariables.front();
1467     d_constantIntegerVariables.pop();
1468
1469     Debug("arith::dio")  << v << endl;
1470
1471     Assert(isInteger(v));
1472     Assert(d_partialModel.boundsAreEqual(v));
1473
1474
1475     Constraint lb = d_partialModel.getLowerBoundConstraint(v);
1476     Constraint ub = d_partialModel.getUpperBoundConstraint(v);
1477
1478     Node orig = Node::null();
1479     if(lb->isEquality()){
1480       orig = lb->explainForConflict();
1481     }else if(ub->isEquality()){
1482       orig = ub->explainForConflict();
1483     }else {
1484       orig = ConstraintValue::explainConflict(ub, lb);
1485     }
1486
1487     Assert(d_partialModel.assignmentIsConsistent(v));
1488
1489     Comparison eq = mkIntegerEqualityFromAssignment(v);
1490
1491     if(eq.isBoolean()){
1492       //This can only be a conflict
1493       Assert(!eq.getNode().getConst<bool>());
1494
1495       //This should be handled by the normal form earlier in the case of equality
1496       Assert(orig.getKind() != EQUAL);
1497       return orig;
1498     }else{
1499       Debug("dio::push") << v << " " << eq.getNode() << " with reason " << orig << endl;
1500       d_diosolver.pushInputConstraint(eq, orig);
1501     }
1502   }
1503
1504   return d_diosolver.processEquationsForConflict();
1505 }
1506
1507 Constraint TheoryArithPrivate::constraintFromFactQueue(){
1508   Assert(!done());
1509   TNode assertion = get();
1510
1511   if( options::finiteModelFind() && d_quantEngine && d_quantEngine->getBoundedIntegers() ){
1512     d_quantEngine->getBoundedIntegers()->assertNode(assertion);
1513   }
1514
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);
1529       }
1530       return NullConstraint;
1531     }
1532     Assert(reEq.getKind() != CONST_BOOLEAN);
1533     if(!isSetup(reEq)){
1534       setupAtom(reEq);
1535     }
1536     Node reAssertion = isDistinct ? reEq.notNode() : reEq;
1537     constraint = d_constraintDatabase.lookup(reAssertion);
1538
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);
1543     }
1544   }
1545
1546   Assert(constraint != NullConstraint);
1547
1548   if(constraint->negationHasProof()){
1549     Constraint negation = constraint->getNegation();
1550     if(negation->isSelfExplaining()){
1551       if(Debug.isOn("whytheoryenginewhy")){
1552         debugPrintFacts();
1553       }
1554     }
1555     Debug("arith::eq") << constraint << endl;
1556     Debug("arith::eq") << negation << endl;
1557
1558     NodeBuilder<> nb(kind::AND);
1559     nb << assertion;
1560     negation->explainForConflict(nb);
1561     Node conflict = nb;
1562     Debug("arith::eq") << "conflict" << conflict << endl;
1563     raiseConflict(conflict);
1564     return NullConstraint;
1565   }
1566   Assert(!constraint->negationHasProof());
1567
1568   if(constraint->assertedToTheTheory()){
1569     //Do nothing
1570     return NullConstraint;
1571   }else{
1572     Debug("arith::constraint") << "arith constraint " << constraint << std::endl;
1573     constraint->setAssertedToTheTheory(assertion);
1574
1575     if(!constraint->hasProof()){
1576       Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
1577       constraint->selfExplaining();
1578     }else{
1579       Debug("arith::constraint") << "already has proof: " << constraint->explainForConflict() << endl;
1580     }
1581
1582     return constraint;
1583   }
1584 }
1585
1586 bool TheoryArithPrivate::assertionCases(Constraint constraint){
1587   Assert(constraint->hasProof());
1588   Assert(!constraint->negationHasProof());
1589
1590   ArithVar x_i = constraint->getVariable();
1591
1592   switch(constraint->getType()){
1593   case UpperBound:
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);
1600           return true;
1601         }else{
1602           floorConstraint->impliedBy(constraint);
1603           // Do not need to add to d_learnedBounds
1604         }
1605       }
1606       return AssertUpper(floorConstraint);
1607     }else{
1608       return AssertUpper(constraint);
1609     }
1610   case LowerBound:
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);
1617           return true;
1618         }
1619         ceilingConstraint->impliedBy(constraint);
1620         // Do not need to add to learnedBounds
1621       }
1622       return AssertLower(ceilingConstraint);
1623     }else{
1624       return AssertLower(constraint);
1625     }
1626   case Equality:
1627     return AssertEquality(constraint);
1628   case Disequality:
1629     return AssertDisequality(constraint);
1630   default:
1631     Unreachable();
1632     return false;
1633   }
1634 }
1635
1636 /**
1637  * Looks for the next integer variable without an integer assignment in a round robin fashion.
1638  * Changes the value of d_nextIntegerCheckVar.
1639  *
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.
1642  */
1643 bool TheoryArithPrivate::hasIntegerModel(){
1644   //if(d_variables.size() > 0){
1645   ArithVar numVars = d_partialModel.getNumberOfVariables();
1646   if(numVars > 0){
1647     const ArithVar rrEnd = d_nextIntegerCheckVar;
1648     do {
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()){
1653           return false;
1654         }
1655       }
1656     } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == numVars ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd);
1657   }
1658   return true;
1659 }
1660
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);
1668   }
1669 }
1670
1671 void TheoryArithPrivate::branchVector(const std::vector<ArithVar>& lemmas){
1672   //output the lemmas
1673   for(vector<ArithVar>::const_iterator i = lemmas.begin(); i != lemmas.end(); ++i){
1674     ArithVar v = *i;
1675     Assert(!d_cutInContext.contains(v));
1676     d_cutInContext.insert(v);
1677     d_cutCount = d_cutCount + 1;
1678     Node lem = branchIntegerVariable(v);
1679     outputLemma(lem);
1680     ++(d_statistics.d_externalBranchAndBounds);
1681   }
1682 }
1683
1684 bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
1685   Assert(d_qflraStatus != Result::SAT);
1686
1687   d_partialModel.stopQueueingBoundCounts();
1688   UpdateTrackingCallback utcb(&d_linEq);
1689   d_partialModel.processBoundsQueue(utcb);
1690   d_linEq.startTrackingBoundCounts();
1691
1692   bool noPivotLimit = Theory::fullEffort(effortLevel) ||
1693     !options::restrictedPivots();
1694
1695   bool emmittedConflictOrSplit = false;
1696
1697   SimplexDecisionProcedure& simplex =
1698     options::useFC() ? (SimplexDecisionProcedure&)d_fcSimplex :
1699     (options::useSOI() ? (SimplexDecisionProcedure&)d_soiSimplex :
1700      (SimplexDecisionProcedure&)d_dualSimplex);
1701
1702   bool useFancyFinal = options::fancyFinal() && ApproximateSimplex::enabled();
1703
1704   if(!useFancyFinal){
1705     d_qflraStatus = simplex.findModel(noPivotLimit);
1706   }else{
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
1712
1713     int16_t oldCap = options::arithStandardCheckVarOrderPivots();
1714
1715     static const int32_t pass2Limit = 10;
1716     static const int32_t relaxationLimit = 10000;
1717     static const int32_t mipLimit = 200000;
1718
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)){
1724
1725       ApproximateSimplex* approxSolver = ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel);
1726       approxSolver->setPivotLimit(relaxationLimit);
1727
1728       if(!d_guessedCoeffSet){
1729         d_guessedCoeffs = approxSolver->heuristicOptCoeffs();
1730         d_guessedCoeffSet = true;
1731       }
1732       if(!d_guessedCoeffs.empty()){
1733         approxSolver->setOptCoeffs(d_guessedCoeffs);
1734       }
1735
1736       ApproximateSimplex::ApproxResult relaxRes, mipRes;
1737       ApproximateSimplex::Solution relaxSolution, mipSolution;
1738       relaxRes = approxSolver->solveRelaxation();
1739       switch(relaxRes){
1740       case ApproximateSimplex::ApproxSat:
1741         {
1742           relaxSolution = approxSolver->extractRelaxation();
1743
1744           if(d_likelyIntegerInfeasible){
1745             d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
1746           }else{
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);
1754             }else{
1755               if(mipRes == ApproximateSimplex::ApproxUnsat){
1756                 d_likelyIntegerInfeasible = true;
1757               }
1758               d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
1759             }
1760           }
1761           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
1762           if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); }
1763           //Message() << "done" << endl;
1764         }
1765         break;
1766       case ApproximateSimplex::ApproxUnsat:
1767         {
1768           ApproximateSimplex::Solution sol = approxSolver->extractRelaxation();
1769
1770           d_qflraStatus = d_attemptSolSimplex.attempt(sol);
1771           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
1772
1773           if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); }
1774         }
1775         break;
1776       default:
1777         break;
1778       }
1779       delete approxSolver;
1780     }
1781
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;
1788       }else{
1789         //Message() << "splitting" << endl;
1790
1791         d_qflraStatus = simplex.findModel(noPivotLimit);
1792       }
1793     }
1794     options::arithStandardCheckVarOrderPivots.set(oldCap);
1795   }
1796
1797   // TODO Save zeroes with no conflicts
1798   d_linEq.stopTrackingBoundCounts();
1799   d_partialModel.startQueueingBoundCounts();
1800
1801   return emmittedConflictOrSplit;
1802 }
1803
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;
1808
1809   if(Debug.isOn("arith::consistency")){
1810     Assert(unenqueuedVariablesAreConsistent());
1811   }
1812
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;
1817   if(newFacts){
1818     d_qflraStatus = Result::SAT_UNKNOWN;
1819     d_hasDoneWorkSinceCut = true;
1820   }
1821
1822   while(!done()){
1823     Constraint curr = constraintFromFactQueue();
1824     if(curr != NullConstraint){
1825       bool res CVC4_UNUSED = assertionCases(curr);
1826       Assert(!res || inConflict());
1827     }
1828     if(inConflict()){ break; }
1829   }
1830   if(!inConflict()){
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;
1836
1837       bool res CVC4_UNUSED = assertionCases(curr);
1838       Assert(!res || inConflict());
1839
1840       if(inConflict()){ break; }
1841     }
1842   }
1843
1844   if(inConflict()){
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();
1850       d_errorSet.clear();
1851     }else{
1852       ++d_statistics.d_commitsOnConflicts;
1853       Debug("arith::bt") << "committing here " << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
1854       d_partialModel.commitAssignmentChanges();
1855       revertOutOfConflict();
1856     }
1857     outputConflicts();
1858     return;
1859   }
1860
1861
1862   if(Debug.isOn("arith::print_assertions")) {
1863     debugPrintAssertions(Debug("arith::print_assertions"));
1864   }
1865
1866   bool emmittedConflictOrSplit = false;
1867   Assert(d_conflicts.empty());
1868
1869   bool useSimplex = d_qflraStatus != Result::SAT;
1870   if(useSimplex){
1871     emmittedConflictOrSplit = solveRealRelaxation(effortLevel);
1872   }
1873
1874   switch(d_qflraStatus){
1875   case Result::SAT:
1876     if(newFacts){
1877       ++d_statistics.d_nontrivialSatChecks;
1878     }
1879
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"));
1885     }
1886     if(useSimplex && options::collectPivots()){
1887       if(options::useFC()){
1888         d_statistics.d_satPivots << d_fcSimplex.getPivots();
1889       }else{
1890         d_statistics.d_satPivots << d_dualSimplex.getPivots();
1891       }
1892     }
1893     break;
1894   case Result::SAT_UNKNOWN:
1895     ++d_unknownsInARow;
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);
1901
1902     if(useSimplex && options::collectPivots()){
1903       if(options::useFC()){
1904         d_statistics.d_unknownPivots << d_fcSimplex.getPivots();
1905       }else{
1906         d_statistics.d_unknownPivots << d_dualSimplex.getPivots();
1907       }
1908     }
1909     break;
1910   case Result::UNSAT:
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();
1916       d_errorSet.clear();
1917     }else{
1918       ++d_statistics.d_commitsOnConflicts;
1919
1920       Debug("arith::bt") << "committing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
1921       d_partialModel.commitAssignmentChanges();
1922       revertOutOfConflict();
1923
1924       if(Debug.isOn("arith::consistency::comitonconflict")){
1925         entireStateIsConsistent("commit on conflict");
1926       }
1927     }
1928     outputConflicts();
1929     emmittedConflictOrSplit = true;
1930
1931     if(useSimplex && options::collectPivots()){
1932       if(options::useFC()){
1933         d_statistics.d_unsatPivots << d_fcSimplex.getPivots();
1934       }else{
1935         d_statistics.d_unsatPivots << d_dualSimplex.getPivots();
1936       }
1937     }
1938     break;
1939   default:
1940     Unimplemented();
1941   }
1942   d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
1943
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);
1950
1951     while(!d_currentPropagationList.empty()  && !inConflict()){
1952       Constraint curr = d_currentPropagationList.front();
1953       d_currentPropagationList.pop_front();
1954
1955       ConstraintType t = curr->getType();
1956       Assert(t != Disequality, "Disequalities are not allowed in d_currentPropagation");
1957
1958
1959       switch(t){
1960       case LowerBound:
1961         {
1962           Constraint prev = d_currentPropagationList.front();
1963           d_currentPropagationList.pop_front();
1964           d_constraintDatabase.unatePropLowerBound(curr, prev);
1965           break;
1966         }
1967       case UpperBound:
1968         {
1969           Constraint prev = d_currentPropagationList.front();
1970           d_currentPropagationList.pop_front();
1971           d_constraintDatabase.unatePropUpperBound(curr, prev);
1972           break;
1973         }
1974       case Equality:
1975         {
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);
1981           break;
1982         }
1983       default:
1984         Unhandled(curr->getType());
1985       }
1986     }
1987
1988     if(inConflict()){
1989       Debug("arith::unate") << "unate conflict" << endl;
1990       revertOutOfConflict();
1991       d_qflraStatus = Result::UNSAT;
1992       outputConflicts();
1993       emmittedConflictOrSplit = true;
1994       Debug("arith::bt") << "committing on unate conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
1995
1996     }
1997   }else{
1998     TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
1999     d_currentPropagationList.clear();
2000   }
2001   Assert( d_currentPropagationList.empty());
2002
2003   if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel)){
2004     ++d_fullCheckCounter;
2005   }
2006   if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel)){
2007     emmittedConflictOrSplit = splitDisequalities();
2008   }
2009
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);
2019         outputConflicts();
2020         emmittedConflictOrSplit = true;
2021       }
2022     }
2023
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);
2033       }
2034     }
2035
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);
2043       }
2044     }
2045
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);
2052         }
2053       }else{
2054         outputRestart();
2055       }
2056     }
2057   }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
2058   if(Theory::fullEffort(effortLevel) && d_nlIncomplete){
2059     // TODO this is total paranoia
2060     setIncomplete();
2061   }
2062
2063   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
2064   if(Debug.isOn("arith::print_model")) {
2065     debugPrintModel(Debug("arith::print_model"));
2066   }
2067   Debug("arith") << "TheoryArithPrivate::check end" << std::endl;
2068 }
2069
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;
2076
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();
2081
2082   //Node eq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, var, mkRationalNode(floor_d+1)));
2083   //Node diseq = eq.notNode();
2084
2085   Node ub = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
2086   Node lb = ub.notNode();
2087
2088
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;
2094   } else {
2095     Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
2096   }
2097   if(isSatLiteral(lem[1])) {
2098     Debug("integers") << "    " << lem[1] << " == " << getSatValue(lem[1]) << endl;
2099     } else {
2100     Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
2101   }
2102   return lem;
2103 }
2104
2105 std::vector<ArithVar> TheoryArithPrivate::cutAllBounded() const{
2106   vector<ArithVar> lemmas;
2107   ArithVar max = d_partialModel.getNumberOfVariables();
2108
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) &&
2117          !d.isIntegral()){
2118         lemmas.push_back(iter);
2119       }
2120     }
2121   }
2122   return lemmas;
2123 }
2124
2125 /** Returns true if the roundRobinBranching() issues a lemma. */
2126 Node TheoryArithPrivate::roundRobinBranch(){
2127   if(hasIntegerModel()){
2128     return Node::null();
2129   }else{
2130     ArithVar v = d_nextIntegerCheckVar;
2131
2132     Assert(isInteger(v));
2133     Assert(!isSlackVariable(v));
2134     return branchIntegerVariable(v);
2135   }
2136 }
2137
2138 bool TheoryArithPrivate::splitDisequalities(){
2139   bool splitSomething = false;
2140
2141   vector<Constraint> save;
2142
2143   while(!d_diseqQueue.empty()){
2144     Constraint front = d_diseqQueue.front();
2145     d_diseqQueue.pop();
2146
2147     if(front->isSplit()){
2148       Debug("eq") << "split already" << endl;
2149     }else{
2150       Debug("eq") << "not split already" << endl;
2151
2152       ArithVar lhsVar = front->getVariable();
2153
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);
2162
2163         Debug("arith::lemma") << "Now " << Rewriter::rewrite(lemma) << endl;
2164         outputLemma(lemma);
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;
2170       }else{
2171         Debug("eq") << "save" << front << ": " <<lhsValue << " != " << rhsValue << endl;
2172         save.push_back(front);
2173       }
2174     }
2175   }
2176   vector<Constraint>::const_iterator i=save.begin(), i_end = save.end();
2177   for(; i != i_end; ++i){
2178     d_diseqQueue.push(*i);
2179   }
2180   return splitSomething;
2181 }
2182
2183 /**
2184  * Should be guarded by at least Debug.isOn("arith::print_assertions").
2185  * Prints to Debug("arith::print_assertions")
2186  */
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){
2190     ArithVar i = *vi;
2191     if (d_partialModel.hasLowerBound(i)) {
2192       Constraint lConstr = d_partialModel.getLowerBoundConstraint(i);
2193       out << lConstr << endl;
2194     }
2195
2196     if (d_partialModel.hasUpperBound(i)) {
2197       Constraint uConstr = d_partialModel.getUpperBoundConstraint(i);
2198       out << uConstr << endl;
2199     }
2200   }
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) {
2204     out << *it << endl;
2205   }
2206 }
2207
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){
2211     ArithVar i = *vi;
2212     if(d_partialModel.hasNode(i)){
2213       out << d_partialModel.asNode(i) << " : " <<
2214         d_partialModel.getAssignment(i);
2215       if(d_tableau.isBasic(i)){
2216         out << " (basic)";
2217       }
2218       out << endl;
2219     }
2220   }
2221 }
2222
2223
2224
2225 Node TheoryArithPrivate::explain(TNode n) {
2226
2227   Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
2228
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;
2234     return exp;
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;
2240       return exp;
2241     }else{
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);
2246     }
2247   }else{
2248     Assert(d_congruenceManager.canExplain(n));
2249     Debug("arith::explain") << "dm explanation" << n << endl;
2250     return d_congruenceManager.explain(n);
2251   }
2252 }
2253
2254
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();
2263     }else{
2264       propagateCandidates();
2265     }
2266   }else{
2267     clearUpdates();
2268   }
2269
2270   while(d_constraintDatabase.hasMorePropagations()){
2271     Constraint c = d_constraintDatabase.nextPropagation();
2272     Debug("arith::prop") << "next prop" << getSatContext()->getLevel() << ": " << c << endl;
2273
2274     if(c->negationHasProof()){
2275       Debug("arith::prop") << "negation has proof " << c->getNegation() << endl
2276                            << c->getNegation()->explainForConflict() << endl;
2277     }
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!");
2279
2280     if(!c->assertedToTheTheory()){
2281       Node literal = c->getLiteral();
2282       Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl;
2283
2284       outputPropagate(literal);
2285     }else{
2286       Debug("arith::prop") << "already asserted to the theory " <<  c->getLiteral() << endl;
2287     }
2288   }
2289
2290   while(d_congruenceManager.hasMorePropagations()){
2291     TNode toProp = d_congruenceManager.getNextPropagation();
2292
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);
2296
2297     Constraint constraint = d_constraintDatabase.lookup(normalized);
2298     if(constraint == NullConstraint){
2299       Debug("arith::prop") << "propagating on non-constraint? "  << toProp << endl;
2300
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;
2308       raiseConflict(lp);
2309       outputConflicts();
2310       return;
2311     }else{
2312       Debug("arith::prop") << "propagating still?" <<  toProp << endl;
2313       outputPropagate(toProp);
2314     }
2315   }
2316 }
2317
2318 DeltaRational TheoryArithPrivate::getDeltaValue(TNode n) const throw (DeltaRationalException, ModelException) {
2319   AlwaysAssert(d_qflraStatus != Result::SAT_UNKNOWN);
2320   Debug("arith::value") << n << std::endl;
2321
2322   switch(n.getKind()) {
2323
2324   case kind::CONST_RATIONAL:
2325     return n.getConst<Rational>();
2326
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);
2331     }
2332     return value;
2333   }
2334
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) {
2339       TNode curr = *i;
2340       value = value * getDeltaValue(curr);
2341       if(!curr.isConst()){
2342         ++variableParts;
2343       }
2344     }
2345     // TODO: This is a bit of a weak check
2346     if(isSetup(n)){
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.");
2351       }
2352     }
2353     return value;
2354   }
2355   case kind::MINUS:{ // 2 args
2356     return getDeltaValue(n[0]) - getDeltaValue(n[1]);
2357   }
2358
2359   case kind::UMINUS:{ // 1 arg
2360     return (- getDeltaValue(n[0]));
2361   }
2362
2363   case kind::DIVISION:{ // 2 args
2364     DeltaRational res = getDeltaValue(n[0]) / getDeltaValue(n[1]);
2365     if(isSetup(n)){
2366       ArithVar var = d_partialModel.asArithVar(n);
2367       if(d_partialModel.getAssignment(var) != res){
2368         throw ModelException(n, "Model disagrees on non-linear term.");
2369       }
2370     }
2371     return res;
2372   }
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]);
2377     if(denom.isZero()){
2378       return DeltaRational(0,0);
2379     }else{
2380       DeltaRational numer = getDeltaValue(n[0]);
2381       DeltaRational res;
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));
2386       }else{
2387         Assert(n.getKind() == kind::INTS_MODULUS_TOTAL);
2388         res = Rational(numer.euclidianDivideRemainder(denom));
2389       }
2390       if(isSetup(n)){
2391         ArithVar var = d_partialModel.asArithVar(n);
2392         if(d_partialModel.getAssignment(var) != res){
2393           throw ModelException(n, "Model disagrees on non-linear term.");
2394         }
2395       }
2396       return res;
2397     }
2398   }
2399
2400   default:
2401     if(isSetup(n)){
2402       ArithVar var = d_partialModel.asArithVar(n);
2403       return d_partialModel.getAssignment(var);
2404     }else{
2405       throw ModelException(n, "Expected a setup node.");
2406     }
2407   }
2408 }
2409
2410 Rational TheoryArithPrivate::deltaValueForTotalOrder() const{
2411   Rational min(2);
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();
2415
2416   for(; qiter != qiter_end; ++qiter){
2417     Constraint curr = *qiter;
2418
2419     const DeltaRational& rhsValue = curr->getValue();
2420     relevantDeltaValues.insert(rhsValue);
2421   }
2422
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;
2427
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);
2432   }
2433
2434   for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
2435     ArithVar v = *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);
2441     }
2442     if( d_partialModel.hasUpperBound(v)){
2443       const DeltaRational& ub = d_partialModel.getUpperBound(v);
2444       relevantDeltaValues.insert(ub);
2445     }
2446   }
2447
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;
2452     ++iter;
2453     for(; iter != iter_end; ++iter){
2454       const DeltaRational& curr = *iter;
2455
2456       Assert(prev < curr);
2457
2458       DeltaRational::seperatingDelta(min, prev, curr);
2459       prev = curr;
2460     }
2461   }
2462
2463   Assert(min.sgn() > 0);
2464   Rational belowMin = min/Rational(2);
2465   return belowMin;
2466 }
2467
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");
2471
2472   if(Debug.isOn("arith::collectModelInfo")){
2473     debugPrintFacts();
2474   }
2475
2476   Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
2477
2478
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();
2482
2483   // TODO:
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){
2487     ArithVar v = *vi;
2488
2489     if(!isSlackVariable(v)){
2490       Node term = d_partialModel.asNode(v);
2491
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);
2495
2496         Node qNode = mkRationalNode(qmodel);
2497         Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
2498
2499         m->assertEquality(term, qNode, true);
2500       }else{
2501         Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl;
2502
2503       }
2504     }
2505   }
2506
2507   // Iterate over equivalence classes in LinearEqualityModule
2508   // const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine();
2509   // m->assertEqualityEngine(&ee);
2510
2511   Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl;
2512 }
2513
2514 bool TheoryArithPrivate::safeToReset() const {
2515   Assert(!d_tableauSizeHasBeenModified);
2516   Assert(d_errorSet.noSignals());
2517
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)){
2523       return false;
2524     }
2525   }
2526
2527   return true;
2528 }
2529
2530 void TheoryArithPrivate::notifyRestart(){
2531   TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer);
2532
2533   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
2534
2535   ++d_restartsCounter;
2536 }
2537
2538 bool TheoryArithPrivate::entireStateIsConsistent(const string& s){
2539   bool result = true;
2540   for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
2541     ArithVar var = *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)";
2548       }
2549       Warning() << endl;
2550       result = false;
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)";
2556       }
2557       Warning() << endl;
2558       result = false;
2559     }
2560   }
2561   return result;
2562 }
2563
2564 bool TheoryArithPrivate::unenqueuedVariablesAreConsistent(){
2565   bool result = true;
2566   for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
2567     ArithVar var = *vi;
2568     if(!d_partialModel.assignmentIsConsistent(var)){
2569       if(!d_errorSet.inError(var)){
2570
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)";
2575         }
2576         Warning() << endl;
2577         result = false;
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)";
2583         }
2584         Warning() << endl;
2585       }
2586      }
2587   }
2588   return result;
2589 }
2590
2591 void TheoryArithPrivate::presolve(){
2592   TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
2593
2594   d_statistics.d_initialTableauSize.setData(d_tableau.size());
2595
2596   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
2597
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;
2602   }
2603
2604   vector<Node> lemmas;
2605   switch(options::arithUnateLemmaMode()){
2606   case NO_PRESOLVE_LEMMAS:
2607     break;
2608   case INEQUALITY_PRESOLVE_LEMMAS:
2609     d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
2610     break;
2611   case EQUALITY_PRESOLVE_LEMMAS:
2612     d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
2613     break;
2614   case ALL_PRESOLVE_LEMMAS:
2615     d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
2616     d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
2617     break;
2618   default:
2619     Unhandled(options::arithUnateLemmaMode());
2620   }
2621
2622   vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
2623   for(; i != i_end; ++i){
2624     Node lem = *i;
2625     Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
2626     outputLemma(lem);
2627   }
2628 }
2629
2630 EqualityStatus TheoryArithPrivate::getEqualityStatus(TNode a, TNode b) {
2631   if(d_qflraStatus == Result::SAT_UNKNOWN){
2632     return EQUALITY_UNKNOWN;
2633   }else{
2634     try {
2635       if (getDeltaValue(a) == getDeltaValue(b)) {
2636         return EQUALITY_TRUE_IN_MODEL;
2637       } else {
2638         return EQUALITY_FALSE_IN_MODEL;
2639       }
2640     } catch (DeltaRationalException& dr) {
2641       return EQUALITY_UNKNOWN;
2642     } catch (ModelException& me) {
2643       return EQUALITY_UNKNOWN;
2644     }
2645   }
2646 }
2647
2648 bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound){
2649   ++d_statistics.d_boundComputations;
2650
2651   RowIndex ridx = d_tableau.basicToRowIndex(basic);
2652   DeltaRational bound = d_linEq.computeRowBound(ridx, upperBound, basic);
2653
2654   if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) ||
2655      (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){
2656
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
2660     //if none exists.
2661     //Experiment with doing this everytime or only when the new constraint
2662     //implies an unknown fact.
2663
2664     ConstraintType t = upperBound ? UpperBound : LowerBound;
2665     Constraint bestImplied = d_constraintDatabase.getBestImpliedBound(basic, t, bound);
2666
2667     // Node bestImplied = upperBound ?
2668     //   d_apm.getBestImpliedUpperBound(basic, bound):
2669     //   d_apm.getBestImpliedLowerBound(basic, bound);
2670
2671     if(bestImplied != NullConstraint){
2672       //This should be stronger
2673       Assert(!upperBound || bound <= bestImplied->getValue());
2674       Assert(!upperBound || d_partialModel.lessThanUpperBound(basic, bestImplied->getValue()));
2675
2676       Assert( upperBound || bound >= bestImplied->getValue());
2677       Assert( upperBound || d_partialModel.greaterThanLowerBound(basic, bestImplied->getValue()));
2678       //slightly changed
2679
2680       // Constraint c = d_constraintDatabase.lookup(bestImplied);
2681       // Assert(c != NullConstraint);
2682
2683       bool assertedToTheTheory = bestImplied->assertedToTheTheory();
2684       bool canBePropagated = bestImplied->canBePropagated();
2685       bool hasProof = bestImplied->hasProof();
2686
2687       Debug("arith::prop") << "arith::prop" << basic
2688                            << " " << assertedToTheTheory
2689                            << " " << canBePropagated
2690                            << " " << hasProof
2691                            << endl;
2692
2693       if(bestImplied->negationHasProof()){
2694         Warning() << "the negation of " <<  bestImplied << " : " << endl
2695                   << "has proof " << bestImplied->getNegation() << endl
2696                   << bestImplied->getNegation()->explainForConflict() << endl;
2697       }
2698
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"));
2706         }
2707         return true;
2708       }
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"));
2713       }
2714     }
2715   }else if(Debug.isOn("arith::prop")){
2716     Debug("arith::prop") << "false " << bound << " ";
2717     d_partialModel.printModel(basic, Debug("arith::prop"));
2718   }
2719   return false;
2720 }
2721
2722 void TheoryArithPrivate::propagateCandidate(ArithVar basic){
2723   bool success = false;
2724   RowIndex ridx = d_tableau.basicToRowIndex(basic);
2725
2726   bool tryLowerBound =
2727     d_partialModel.strictlyAboveLowerBound(basic) &&
2728     d_linEq.rowLacksBound(ridx, false, basic) == NULL;
2729
2730   bool tryUpperBound =
2731     d_partialModel.strictlyBelowUpperBound(basic) &&
2732     d_linEq.rowLacksBound(ridx, true, basic) == NULL;
2733
2734   if(tryLowerBound){
2735     success |= propagateCandidateLowerBound(basic);
2736   }
2737   if(tryUpperBound){
2738     success |= propagateCandidateUpperBound(basic);
2739   }
2740   if(success){
2741     ++d_statistics.d_boundPropagations;
2742   }
2743 }
2744
2745 void TheoryArithPrivate::propagateCandidates(){
2746   TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
2747
2748   Debug("arith::prop") << "propagateCandidates begin" << endl;
2749
2750   Assert(d_candidateBasics.empty());
2751
2752   if(d_updatedBounds.empty()){ return; }
2753
2754   DenseSet::const_iterator i = d_updatedBounds.begin();
2755   DenseSet::const_iterator end = d_updatedBounds.end();
2756   for(; i != end; ++i){
2757     ArithVar var = *i;
2758     if(d_tableau.isBasic(var) &&
2759        d_tableau.basicRowLength(var) <= options::arithPropagateMaxLength()){
2760       d_candidateBasics.softAdd(var);
2761     }else{
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);
2771         }
2772       }
2773     }
2774   }
2775   d_updatedBounds.purge();
2776
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);
2782   }
2783   Debug("arith::prop") << "propagateCandidates end" << endl << endl << endl;
2784 }
2785
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.)
2799    */
2800
2801   TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
2802   Debug("arith::prop") << "propagateCandidatesNew begin" << endl;
2803
2804   Assert(d_qflraStatus == Result::SAT);
2805   if(d_updatedBounds.empty()){ return; }
2806   dumpUpdatedBoundsToRows();
2807   Assert(d_updatedBounds.empty());
2808
2809   if(!d_candidateRows.empty()){
2810     UpdateTrackingCallback utcb(&d_linEq);
2811     d_partialModel.processBoundsQueue(utcb);
2812   }
2813
2814   while(!d_candidateRows.empty()){
2815     RowIndex candidate = d_candidateRows.back();
2816     d_candidateRows.pop_back();
2817     propagateCandidateRow(candidate);
2818   }
2819   Debug("arith::prop") << "propagateCandidatesNew end" << endl << endl << endl;
2820 }
2821
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;
2826   if(hasSlack){
2827     ConstraintType t = ub ? UpperBound : LowerBound;
2828     const DeltaRational& a = d_partialModel.getAssignment(v);
2829
2830     if(isInteger(v) && !a.isIntegral()){
2831       return true;
2832     }
2833
2834     Constraint strongestPossible = d_constraintDatabase.getBestImpliedBound(v, t, a);
2835     if(strongestPossible == NullConstraint){
2836       return false;
2837     }else{
2838       bool assertedToTheTheory = strongestPossible->assertedToTheTheory();
2839       bool canBePropagated = strongestPossible->canBePropagated();
2840       bool hasProof = strongestPossible->hasProof();
2841
2842       return !assertedToTheTheory && canBePropagated && !hasProof;
2843     }
2844   }else{
2845     return false;
2846   }
2847 }
2848
2849 bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){
2850   Debug("arith::prop") << "  attemptSingleton" << ridx;
2851
2852   const Tableau::Entry* ep;
2853   ep = d_linEq.rowLacksBound(ridx, rowUp, ARITHVAR_SENTINEL);
2854   Assert(ep != NULL);
2855
2856   ArithVar v = ep->getColVar();
2857   const Rational& coeff = ep->getCoefficient();
2858
2859   // 0 = c * v + \sum rest
2860   // Suppose rowUp
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));
2869
2870   Debug("arith::prop") << "  " << rowUp << " " << v << " " << coeff << " " << vUp << endl;
2871   Debug("arith::prop") << "  " << propagateMightSucceed(v, vUp) << endl;
2872
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);
2877   }
2878   return false;
2879 }
2880
2881 bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){
2882   Debug("arith::prop") << "  attemptFull" << ridx << endl;
2883
2884   vector<const Tableau::Entry*> candidates;
2885
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);
2893     }
2894   }
2895   if(candidates.empty()){ return false; }
2896
2897   const DeltaRational slack =
2898     d_linEq.computeRowBound(ridx, rowUp, ARITHVAR_SENTINEL);
2899   bool any = false;
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();
2905
2906     // See the comment for attemptSingleton()
2907     bool activeUp = (rowUp == (c.sgn() > 0));
2908     bool vUb = (rowUp == (c.sgn() < 0));
2909
2910     const DeltaRational& activeBound = activeUp ?
2911       d_partialModel.getUpperBound(v):
2912       d_partialModel.getLowerBound(v);
2913
2914     DeltaRational contribution = activeBound * c;
2915     DeltaRational impliedBound = (slack - contribution)/(-c);
2916
2917     bool success = tryToPropagate(ridx, rowUp, v, vUb, impliedBound);
2918     any |= success;
2919   }
2920   return any;
2921 }
2922
2923 bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, bool vUb, const DeltaRational& bound){
2924
2925   bool weaker = vUb ? d_partialModel.strictlyLessThanUpperBound(v, bound):
2926     d_partialModel.strictlyGreaterThanLowerBound(v, bound);
2927   if(weaker){
2928     ConstraintType t = vUb ? UpperBound : LowerBound;
2929
2930     if(isInteger(v)){
2931       //cout << "maybe" << endl;
2932       //cout << bound << endl;
2933     }
2934     Constraint implied = d_constraintDatabase.getBestImpliedBound(v, t, bound);
2935     if(implied != NullConstraint){
2936       return rowImplicationCanBeApplied(ridx, rowUp, implied);
2937     }
2938   }
2939   return false;
2940 }
2941
2942 Node flattenImplication(Node imp){
2943   NodeBuilder<> nb(kind::OR);
2944   Node left = imp[0];
2945   Node right = imp[1];
2946
2947   if(left.getKind() == kind::AND){
2948     for(Node::iterator i = left.begin(), iend = left.end(); i != iend; ++i) {
2949       nb << (*i).negate();
2950     }
2951   }else{
2952     nb << left.negate();
2953   }
2954
2955   if(right.getKind() == kind::OR){
2956     for(Node::iterator i = right.begin(), iend = right.end(); i != iend; ++i) {
2957       nb << *i;
2958     }
2959   }else{
2960     nb << right;
2961   }
2962
2963   return nb;
2964 }
2965
2966 bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, Constraint implied){
2967   Assert(implied != NullConstraint);
2968   ArithVar v = implied->getVariable();
2969
2970   bool assertedToTheTheory = implied->assertedToTheTheory();
2971   bool canBePropagated = implied->canBePropagated();
2972   bool hasProof = implied->hasProof();
2973
2974   Debug("arith::prop") << "arith::prop" << v
2975                        << " " << assertedToTheTheory
2976                        << " " << canBePropagated
2977                        << " " << hasProof
2978                        << endl;
2979
2980   if(implied->negationHasProof()){
2981     Warning() << "the negation of " <<  implied << " : " << endl
2982               << "has proof " << implied->getNegation() << endl
2983               << implied->getNegation()->explainForConflict() << endl;
2984   }
2985
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);
2993     }else{
2994       implied->impliedBy(explain);
2995     }
2996     return true;
2997   }
2998
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"));
3004   }
3005   return false;
3006 }
3007
3008 double fRand(double fMin, double fMax)
3009 {
3010     double f = (double)rand() / RAND_MAX;
3011     return fMin + f * (fMax - fMin);
3012 }
3013
3014 bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
3015   BoundCounts hasCount = d_linEq.hasBoundCount(ridx);
3016   uint32_t rowLength = d_tableau.getRowLength(ridx);
3017
3018   bool success = false;
3019   static int instance = 0;
3020   ++instance;
3021
3022   Debug("arith::prop")
3023     << "propagateCandidateRow " << instance << " attempt " << rowLength << " " <<  hasCount << endl;
3024
3025   if(rowLength >= options::arithPropagateMaxLength()){
3026     if(fRand(0.0,1.0) >= double(options::arithPropagateMaxLength())/rowLength){
3027       return false;
3028     }
3029   }
3030
3031   if(hasCount.lowerBoundCount() == rowLength){
3032     success |= attemptFull(ridx, false);
3033   }else if(hasCount.lowerBoundCount() + 1 == rowLength){
3034     success |= attemptSingleton(ridx, false);
3035   }
3036
3037   if(hasCount.upperBoundCount() == rowLength){
3038     success |= attemptFull(ridx, true);
3039   }else if(hasCount.upperBoundCount() + 1 == rowLength){
3040     success |= attemptSingleton(ridx, true);
3041   }
3042   return success;
3043 }
3044
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){
3050     ArithVar var = *i;
3051     if(d_tableau.isBasic(var)){
3052       RowIndex ridx = d_tableau.basicToRowIndex(var);
3053       d_candidateRows.softAdd(ridx);
3054     }else{
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);
3060       }
3061     }
3062   }
3063   d_updatedBounds.purge();
3064 }
3065
3066 const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
3067   RowIndex ridx = d_tableau.basicToRowIndex(basic);
3068   return d_rowTracking[ridx];
3069 }
3070
3071 }/* CVC4::theory::arith namespace */
3072 }/* CVC4::theory namespace */
3073 }/* CVC4 namespace */