From cfe207563479a1e9e13d52bdd93446a8c816636a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 24 Mar 2021 16:24:25 +0100 Subject: [PATCH] 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. --- src/theory/arith/theory_arith_private.cpp | 67 ++++++++++++------- src/theory/arith/theory_arith_private.h | 13 +++- test/regress/CMakeLists.txt | 1 + .../arith/integers/issue6146-stale-vars.smt2 | 18 +++++ 4 files changed, 73 insertions(+), 26 deletions(-) create mode 100644 test/regress/regress0/arith/integers/issue6146-stale-vars.smt2 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index f6278d3a1..b85aeb135 100644 --- 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 181861b00..4b2fcf8a8 100644 --- 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 d_learnedBounds; + /** + * Contains all nodes that have been preregistered + */ + context::CDHashSet 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 2aa8861fd..c7d97d0fd 100644 --- 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 index 000000000..3f23e0367 --- /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) -- 2.30.2