Use SAT context level for --bv-assert-input instead of decision level. (#6758)

The decision level as previously implemented was not accurate since it
did not consider the user context level. This resulted in facts being
incorrectly recognized as input assertions, which happened for
incremental benchmarks.

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 4adbbe7f703f3affce207943922e64b96699a519..e193bfb28a1991f1e765e4f6a92d950f4fb7fda9 100644 (file)
--- 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 15ef5cacbf0e41ee5f0e651fa1e21d7934e68651..984cc6479f15e35b3a6300b204fc2affb4d2bb71 100644 (file)
--- 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 74da49cf6c2007e72f73d2984e04d21dc50b1275..e458ca5e532aed5685be52b58d8bd59080d61324 100644 (file)
--- 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 3ae4a7f0ae87ece14f773461b7760644d338bd37..a5d89e37146c29721fb267ca9c6581b142fe6764 100644 (file)
--- 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 7438279b1c7f3d76f81e9ceb440e02322558c3d9..192b5dfc82944ed01a2958159be29ddbf1180c95 100644 (file)
--- 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 fe49d8b39c5ce97533e6110174e4703e26a6f8b7..e2e216567acca1fe3c6c5beb8ab8f9f7303cc7f9 100644 (file)
--- 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 (file)
index 0000000..905ae82
--- /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)
+