Only consider relevant terms for integer branches (#6181)

Linear arithmetic simply tried to branch on the first integer variable that had a non-integral assignment.
If it holds stale variables that are not part of the current input, these branches can be emitted and are processed by the solver, but the resulting new assertions will not be considered relevant and thus not added to the theory.
As it still triggers a new theory check, linear arithmetic repeats the same procedure and causes an infinite loop.
This PR explicitly tracks the currently relevant nodes by storing all preregistered nodes and only allows branching on variables from this set.
Fixes #6146.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index f6278d3a1d1d5004126c386600a32abb1ff43f49..b85aeb1352106ce1e6b90c9535f5193411b8e99a 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -113,6 +113,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_diseqQueue(c, false),
       d_currentPropagationList(),
       d_learnedBounds(c),
+      d_preregisteredNodes(u),
       d_partialModel(c, DeltaComputeCallback(*this)),
       d_errorSet(
           d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)),
@@ -1380,6 +1381,8 @@ void TheoryArithPrivate::setupAtom(TNode atom) {
 void TheoryArithPrivate::preRegisterTerm(TNode n) {
   Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
 
+  d_preregisteredNodes.insert(n);
+
   try {
     if(isRelationOperator(n.getKind())){
       if(!isSetup(n)){
@@ -1793,21 +1796,27 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
  *
  * If there is no such variable, returns ARITHVAR_SENTINEL;
  */
-ArithVar TheoryArithPrivate::nextIntegerViolatation(bool assumeBounds) const {
+ArithVar TheoryArithPrivate::nextIntegerViolation(bool assumeBounds) const
+{
   ArithVar numVars = d_partialModel.getNumberOfVariables();
   ArithVar v = d_nextIntegerCheckVar;
-  if(numVars > 0){
+  if (numVars > 0)
+  {
     const ArithVar rrEnd = d_nextIntegerCheckVar;
-    do {
-      if(isIntegerInput(v)){
-        if(!d_partialModel.integralAssignment(v)){
-          if( assumeBounds || d_partialModel.assignmentIsConsistent(v) ){
+    do
+    {
+      if (isIntegerInput(v))
+      {
+        if (!d_partialModel.integralAssignment(v))
+        {
+          if (assumeBounds || d_partialModel.assignmentIsConsistent(v))
+          {
             return v;
           }
         }
       }
-      v= (1 + v == numVars) ? 0 : (1 + v);
-    }while(v != rrEnd);
+      v = (1 + v == numVars) ? 0 : (1 + v);
+    } while (v != rrEnd);
   }
   return ARITHVAR_SENTINEL;
 }
@@ -1816,21 +1825,25 @@ ArithVar TheoryArithPrivate::nextIntegerViolatation(bool assumeBounds) const {
  * Checks the set of integer variables I to see if each variable
  * in I has an integer assignment.
  */
-bool TheoryArithPrivate::hasIntegerModel(){
-  ArithVar next = nextIntegerViolatation(true);
-  if(next != ARITHVAR_SENTINEL){
+bool TheoryArithPrivate::hasIntegerModel()
+{
+  ArithVar next = nextIntegerViolation(true);
+  if (next != ARITHVAR_SENTINEL)
+  {
     d_nextIntegerCheckVar = next;
-    if(Debug.isOn("arith::hasIntegerModel")){
+    if (Debug.isOn("arith::hasIntegerModel"))
+    {
       Debug("arith::hasIntegerModel") << "has int model? " << next << endl;
       d_partialModel.printModel(next, Debug("arith::hasIntegerModel"));
     }
     return false;
-  }else{
+  }
+  else
+  {
     return true;
   }
 }
 
-
 Node flattenAndSort(Node n){
   Kind k = n.getKind();
   switch(k){
@@ -2894,9 +2907,12 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
           importSolution(mipSolution);
           solveRelaxationOrPanic(effortLevel);
 
-          if(d_qflraStatus == Result::SAT){
-            if(!anyConflict()){
-              if(ARITHVAR_SENTINEL == nextIntegerViolatation(false)){
+          if (d_qflraStatus == Result::SAT)
+          {
+            if (!anyConflict())
+            {
+              if (ARITHVAR_SENTINEL == nextIntegerViolation(false))
+              {
                 ++(d_statistics.d_solveIntModelsSuccessful);
               }
             }
@@ -3019,21 +3035,26 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu
   }
 }
 
-bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel){
+bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel)
+{
   // if at this point the linear relaxation is still unknown,
   //  attempt to branch an integer variable as a last ditch effort on full check
-  if(d_qflraStatus == Result::SAT_UNKNOWN){
+  if (d_qflraStatus == Result::SAT_UNKNOWN)
+  {
     d_qflraStatus = selectSimplex(true).findModel(false);
   }
 
-  if(Theory::fullEffort(effortLevel)  && d_qflraStatus == Result::SAT_UNKNOWN){
-    ArithVar canBranch = nextIntegerViolatation(false);
-    if(canBranch != ARITHVAR_SENTINEL){
+  if (Theory::fullEffort(effortLevel) && d_qflraStatus == Result::SAT_UNKNOWN)
+  {
+    ArithVar canBranch = nextIntegerViolation(false);
+    if (canBranch != ARITHVAR_SENTINEL)
+    {
       ++d_statistics.d_panicBranches;
       TrustNode branch = branchIntegerVariable(canBranch);
       Assert(branch.getNode().getKind() == kind::OR);
       Node rwbranch = Rewriter::rewrite(branch.getNode()[0]);
-      if(!isSatLiteral(rwbranch)){
+      if (!isSatLiteral(rwbranch))
+      {
         d_approxCuts.push_back(branch);
         return true;
       }

diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 181861b00f13951f9b6f3f58bc04faa8efeb25b8..4b2fcf8a8a42efc40907f163701e318fb24273c0 100644 (file)
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -212,8 +212,10 @@ private:
     return d_partialModel.isAuxiliary(x);
   }
 
-  inline bool isIntegerInput(ArithVar x) const {
-    return d_partialModel.isIntegerInput(x);
+  inline bool isIntegerInput(ArithVar x) const
+  {
+    return d_partialModel.isIntegerInput(x)
+           && d_preregisteredNodes.contains(d_partialModel.asNode(x));
   }
 
   /**
@@ -267,6 +269,11 @@ private:
 
   context::CDQueue<ConstraintP> d_learnedBounds;
 
+  /**
+   * Contains all nodes that have been preregistered
+   */
+  context::CDHashSet<Node, NodeHashFunction> d_preregisteredNodes;
+
 
   /**
    * Manages information about the assignment and upper and lower bounds on
@@ -544,7 +551,7 @@ private:
    *
    * If there is no such variable, returns ARITHVAR_SENTINEL;
    */
-  ArithVar nextIntegerViolatation(bool assumeBounds) const;
+  ArithVar nextIntegerViolation(bool assumeBounds) const;
 
   /**
    * Issues branches for non-auxiliary integer variables with non-integer assignments.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2aa8861fd7fc6a896059cdfe7bae7fe8d3f03a79..c7d97d0fd55dfeb3132d065dd973e05fbcb742f3 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -51,6 +51,7 @@ set(regress_0_tests
   regress0/arith/integers/arith-int-042.min.cvc
   regress0/arith/integers/arith-int-079.cvc
   regress0/arith/integers/arith-interval.cvc
+  regress0/arith/integers/issue6146-stale-vars.smt2
   regress0/arith/issue1399.smt2
   regress0/arith/issue3412.smt2
   regress0/arith/issue3413.smt2

diff --git a/test/regress/regress0/arith/integers/issue6146-stale-vars.smt2 b/test/regress/regress0/arith/integers/issue6146-stale-vars.smt2
new file mode 100644 (file)
index 0000000..3f23e03
--- /dev/null
+++ b/test/regress/regress0/arith/integers/issue6146-stale-vars.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: -i --check-models
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic NIRA)
+(declare-fun i8 () Int)
+(declare-fun i12 () Int)
+(declare-fun r11 () Real)
+(declare-fun r18 () Real)
+(declare-fun i19 () Int)
+(push)
+(assert (= 1 (* i8 (to_int r18))))
+(check-sat)
+(pop)
+(assert (is_int (- r18)))
+(check-sat)
+(assert (and (< i12 i19) (< 0 (+ i12 2)) (= i19 (* 3 (to_int r11)))))
+(check-sat)