Potential fix for non-linear axioms in incremental mode.

2 files changed, 35 insertions, 0 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index a4825c1c4..7301da220 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -122,6 +122,10 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_tableauResetPeriod(10),
   d_conflicts(c),
   d_blackBoxConflict(c, Node::null()),
+
+  d_divlikeAxioms(),
+  d_lastDivAxiomExpanded(u,0),
+
   d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseEqualityEngineConflict(*this)),
   d_cmEnabled(c, true),
 
@@ -1460,6 +1464,7 @@ void TheoryArithPrivate::setupDivLike(const Variable& v){
   if(!lem.isNull()){
     Debug("arith::div") << lem << endl;
     outputLemma(lem);
+    d_divlikeAxioms.push_back(lem);
   }
 }
 
@@ -3783,18 +3788,38 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
   }
 
   if(Theory::fullEffort(effortLevel)){
+    uint32_t N = d_divlikeAxioms.size();
+    AlwaysAssert(N == d_divlikeAxioms.size());
+    while(d_lastDivAxiomExpanded < N){
+      Node divaxiom = d_divlikeAxioms[d_lastDivAxiomExpanded];
+      d_lastDivAxiomExpanded = d_lastDivAxiomExpanded + 1;
+      outputLemma(divaxiom);
+    }
+  }
+
+
+  if(Theory::fullEffort(effortLevel)){
     if(Debug.isOn("arith::consistency::final")){
       entireStateIsConsistent("arith::consistency::final");
     }
     // cout << "fulleffort" << getSatContext()->getLevel() << endl;
     // entireStateIsConsistent("arith::consistency::final");
     // cout << "emmittedConflictOrSplit" << emmittedConflictOrSplit << endl;
+
+    // static int instance = 0;
+    // ++instance;
+    // cout << "Theory arith full effort check" <<  instance << endl;
+    // debugPrintAssertions(cout);
+    // debugPrintModel(cout);
+    // cout << "Theory arith full effort check" <<  instance << " done()" << endl;
   }
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
   if(Debug.isOn("arith::print_model")) {
     debugPrintModel(Debug("arith::print_model"));
   }
+  
+
   Debug("arith") << "TheoryArithPrivate::check end" << std::endl;
 }
 
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 4c539c60d..d2cc33bfa 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -329,6 +329,16 @@ private:
 
   /** This is only used by simplex at the moment. */
   context::CDO<Node> d_blackBoxConflict;
+
+  /** The list of all instantiated division by 0 axioms.
+   * Due to a problem with setup() and garbageCollection
+   * if incremental is on, this list must be expanded
+   * every user context.
+   * This is regardless of the symbol reappearing in the assertions.
+   */
+  std::vector<Node> d_divlikeAxioms;
+  context::CDO<uint32_t> d_lastDivAxiomExpanded;
+
 public:
 
   /**