diff options
| -rw-r--r-- | src/prop/minisat/minisat.cpp | 2 | ||||
| -rw-r--r-- | src/prop/minisat/minisat.h | 11 | ||||
| -rw-r--r-- | src/prop/prop_engine.h | 2 | ||||
| -rw-r--r-- | src/theory/bv/bv_solver_bitblast.cpp | 4 | ||||
| -rw-r--r-- | src/theory/valuation.h | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/issue6738.smt2 | 12 |
7 files changed, 28 insertions, 6 deletions
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 4adbbe7f7..e193bfb28 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -260,7 +260,7 @@ bool MinisatSatSolver::isDecision(SatVariable decn) const { int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const { - return d_minisat->level(v); + return d_minisat->level(v) + d_minisat->user_level(v); } int32_t MinisatSatSolver::getIntroLevel(SatVariable v) const diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 15ef5cacb..984cc6479 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -93,11 +93,20 @@ class MinisatSatSolver : public CDCLTSatSolverInterface bool isDecision(SatVariable decn) const override; + /** Return decision level at which `lit` was decided on. */ int32_t getDecisionLevel(SatVariable v) const override; + /** + * Return user level at which `lit` was introduced. + * + * Note: The user level is tracked independently in the SAT solver and does + * not query the user-context for the user level. The user level in the SAT + * solver starts at level 0 and does not include the global push/pop in + * the SMT engine. + */ int32_t getIntroLevel(SatVariable v) const override; - /** Retrieve a pointer to the unerlying solver. */ + /** Retrieve a pointer to the underlying solver. */ Minisat::SimpSolver* getSolver() { return d_minisat; } /** Retrieve the proof manager of this SAT solver. */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 74da49cf6..e458ca5e5 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -157,7 +157,7 @@ class PropEngine bool isDecision(Node lit) const; /** - * Return the current decision level of `lit`. + * Return SAT context level at which `lit` was decided on. * * @param lit: The node in question, must have an associated SAT literal. * @return Decision level of the SAT variable of `lit` (phase is disregarded), diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index 3ae4a7f0a..a5d89e371 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -219,9 +219,9 @@ bool BVSolverBitblast::preNotifyFact( * using assumptions. */ if (options::bvAssertInput() && val.isSatLiteral(fact) - && !val.isDecision(fact) && val.getDecisionLevel(fact) == 0 - && val.getIntroLevel(fact) == 0) + && val.getDecisionLevel(fact) == 0 && val.getIntroLevel(fact) == 0) { + Assert(!val.isDecision(fact)); d_bbInputFacts.push_back(fact); } else diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 7438279b1..192b5dfc8 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -185,7 +185,7 @@ public: bool isDecision(Node lit) const; /** - * Return the current decision level of `lit`. + * Return SAT context level at which `lit` was decided on. * * @param lit: The node in question, must have an associated SAT literal. * @return Decision level of the SAT variable of `lit` (phase is disregarded), diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fe49d8b39..e2e216567 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -674,6 +674,7 @@ set(regress_0_tests regress0/issue5743.smt2 regress0/issue5947.smt2 regress0/issue6605-2-abd-triv.smt2 + regress0/issue6738.smt2 regress0/issue6741.smt2 regress0/ite_arith.smt2 regress0/ite_real_int_type.smtv1.smt2 diff --git a/test/regress/regress0/issue6738.smt2 b/test/regress/regress0/issue6738.smt2 new file mode 100644 index 000000000..905ae823c --- /dev/null +++ b/test/regress/regress0/issue6738.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: -i --bv-solver=bitblast --bv-assert-input +(set-logic QF_BV) +(declare-fun N () Bool) +(assert (not (= (_ bv1 1) (bvnot (ite N (_ bv1 1) (_ bv0 1)))))) +(push 1) +(assert (not N)) +(set-info :status unsat) +(check-sat) +(pop 1) +(set-info :status sat) +(check-sat) + |