1 files changed, 88 insertions, 12 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 3ba987124..62a258fe2 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -55,6 +55,8 @@ const uint32_t RESET_START = 2;
 
 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe),
+  d_qflraStatus(Result::SAT_UNKNOWN),
+  d_unknownsInARow(0),
   d_hasDoneWorkSinceCut(false),
   d_learner(d_pbSubstitutions),
   d_setupLiteralCallback(this),
@@ -102,7 +104,13 @@ TheoryArith::Statistics::Statistics():
   d_restartTimer("theory::arith::restartTimer"),
   d_boundComputationTime("theory::arith::bound::time"),
   d_boundComputations("theory::arith::bound::boundComputations",0),
-  d_boundPropagations("theory::arith::bound::boundPropagations",0)
+  d_boundPropagations("theory::arith::bound::boundPropagations",0),
+  d_unknownChecks("theory::arith::status::unknowns", 0),
+  d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0),
+  d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow"),
+  d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0),
+  d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0),
+  d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0)
 {
   StatisticsRegistry::registerStat(&d_statAssertUpperConflicts);
   StatisticsRegistry::registerStat(&d_statAssertLowerConflicts);
@@ -127,6 +135,13 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_boundComputationTime);
   StatisticsRegistry::registerStat(&d_boundComputations);
   StatisticsRegistry::registerStat(&d_boundPropagations);
+
+  StatisticsRegistry::registerStat(&d_unknownChecks);
+  StatisticsRegistry::registerStat(&d_maxUnknownsInARow);
+  StatisticsRegistry::registerStat(&d_avgUnknownsInARow);
+  StatisticsRegistry::registerStat(&d_revertsOnConflicts);
+  StatisticsRegistry::registerStat(&d_commitsOnConflicts);
+  StatisticsRegistry::registerStat(&d_nontrivialSatChecks);
 }
 
 TheoryArith::Statistics::~Statistics(){
@@ -153,6 +168,13 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_boundComputationTime);
   StatisticsRegistry::unregisterStat(&d_boundComputations);
   StatisticsRegistry::unregisterStat(&d_boundPropagations);
+
+  StatisticsRegistry::unregisterStat(&d_unknownChecks);
+  StatisticsRegistry::unregisterStat(&d_maxUnknownsInARow);
+  StatisticsRegistry::unregisterStat(&d_avgUnknownsInARow);
+  StatisticsRegistry::unregisterStat(&d_revertsOnConflicts);
+  StatisticsRegistry::unregisterStat(&d_commitsOnConflicts);
+  StatisticsRegistry::unregisterStat(&d_nontrivialSatChecks);
 }
 
 void TheoryArith::revertOutOfConflict(){
@@ -655,7 +677,12 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst
       // Add the substitution if not recursive
       Assert(elim == Rewriter::rewrite(elim));
 
-      if(elim.hasSubterm(minVar)){
+
+      static const int MAX_SUB_SIZE = 20;
+      if(false && right.size() > MAX_SUB_SIZE){
+        Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
+        Debug("simplify") << right.size() << endl;
+      }else if(elim.hasSubterm(minVar)){
         Debug("simplify") << "TheoryArith::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl;
       }else if (!minVar.getType().isInteger() || right.isIntegral()) {
         Assert(!elim.hasSubterm(minVar));
@@ -1354,9 +1381,16 @@ void TheoryArith::outputConflicts(){
 
 void TheoryArith::check(Effort effortLevel){
   Assert(d_currentPropagationList.empty());
-  Debug("arith") << "TheoryArith::check begun" << std::endl;
+  Debug("effortlevel") << "TheoryArith::check " << effortLevel << std::endl;
+  Debug("arith") << "TheoryArith::check begun " << effortLevel << std::endl;
+
+  bool newFacts = !done();
+  Result::Sat previous = d_qflraStatus;
+  if(newFacts){
+    d_qflraStatus = Result::SAT_UNKNOWN;
+    d_hasDoneWorkSinceCut = true;
+  }
 
-  d_hasDoneWorkSinceCut = d_hasDoneWorkSinceCut || !done();
   while(!done()){
     Constraint curr = constraintFromFactQueue();
     if(curr != NullConstraint){
@@ -1366,6 +1400,7 @@ void TheoryArith::check(Effort effortLevel){
     if(inConflict()){
       revertOutOfConflict();
       outputConflicts();
+      d_qflraStatus = Result::UNSAT;
       return;
     }
   }
@@ -1379,6 +1414,7 @@ void TheoryArith::check(Effort effortLevel){
     Assert(!res || inConflict());
 
     if(inConflict()){
+      d_qflraStatus = Result::UNSAT;
       revertOutOfConflict();
       outputConflicts();
       return;
@@ -1391,20 +1427,53 @@ void TheoryArith::check(Effort effortLevel){
   }
 
   bool emmittedConflictOrSplit = false;
+
+
   Assert(d_conflicts.empty());
-  bool foundConflict = d_simplex.findModel();
-  if(foundConflict){
-    revertOutOfConflict();
+
+  d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel));
+  switch(d_qflraStatus){
+  case Result::SAT:
+    if(newFacts){
+      ++d_statistics.d_nontrivialSatChecks;
+    }
+    d_partialModel.commitAssignmentChanges();
+    d_unknownsInARow = 0;
+    break;
+  case Result::SAT_UNKNOWN:
+    ++d_unknownsInARow;
+    ++(d_statistics.d_unknownChecks);
+    Assert(!fullEffort(effortLevel));
+    d_partialModel.commitAssignmentChanges();
+    d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow);
+    break;
+  case Result::UNSAT:
+    d_unknownsInARow = 0;
+    if(previous == Result::SAT){
+      ++d_statistics.d_revertsOnConflicts;
+
+      revertOutOfConflict();
+      d_simplex.clearQueue();
+    }else{
+      ++d_statistics.d_commitsOnConflicts;
+
+      d_partialModel.commitAssignmentChanges();
+      revertOutOfConflict();
+    }
     outputConflicts();
     emmittedConflictOrSplit = true;
-  }else{
-    d_partialModel.commitAssignmentChanges();
+    break;
+  default:
+    Unimplemented();
   }
+  d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
 
+  // This should be fine if sat or unknown
   if(!emmittedConflictOrSplit &&
      (Options::current()->arithPropagationMode == Options::UNATE_PROP ||
       Options::current()->arithPropagationMode == Options::BOTH_PROP)){
     TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
+    Assert(d_qflraStatus != Result::UNSAT);
 
     while(!d_currentPropagationList.empty()  && !inConflict()){
       Constraint curr = d_currentPropagationList.front();
@@ -1618,6 +1687,8 @@ void TheoryArith::debugPrintModel(){
   }
 }
 
+
+
 Node TheoryArith::explain(TNode n) {
 
   Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
@@ -1637,7 +1708,9 @@ Node TheoryArith::explain(TNode n) {
 
 
 void TheoryArith::propagate(Effort e) {
-  if((Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP ||
+  // This uses model values for safety. Disable for now.
+  if(d_qflraStatus == Result::SAT &&
+     (Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP ||
       Options::current()->arithPropagationMode == Options::BOTH_PROP)
      && hasAnyUpdates()){
     propagateCandidates();
@@ -1693,6 +1766,7 @@ void TheoryArith::propagate(Effort e) {
 }
 
 bool TheoryArith::getDeltaAtomValue(TNode n) {
+  Assert(d_qflraStatus != Result::SAT_UNKNOWN);
 
   switch (n.getKind()) {
     case kind::EQUAL: // 2 args
@@ -1712,7 +1786,7 @@ bool TheoryArith::getDeltaAtomValue(TNode n) {
 
 
 DeltaRational TheoryArith::getDeltaValue(TNode n) {
-
+  Assert(d_qflraStatus != Result::SAT_UNKNOWN);
   Debug("arith::value") << n << std::endl;
 
   switch(n.getKind()) {
@@ -1936,7 +2010,9 @@ void TheoryArith::presolve(){
 }
 
 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
-  if (getDeltaValue(a) == getDeltaValue(b)) {
+  if(d_qflraStatus == Result::SAT_UNKNOWN){
+    return EQUALITY_UNKNOWN;
+  }else if (getDeltaValue(a) == getDeltaValue(b)) {
     return EQUALITY_TRUE_IN_MODEL;
   } else {
     return EQUALITY_FALSE_IN_MODEL;