(proof-new) Miscellaneous fixes and regressions (#5841)

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index a8b0c8b3db667e3f4b6d9eaf06d7067f537dad6e..4fce88a391ea6fcd6401d0e4975be798636cc6ce 100644 (file)
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -50,6 +50,7 @@ const char* toString(PfRule id)
     case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION";
     case PfRule::FACTORING: return "FACTORING";
     case PfRule::REORDERING: return "REORDERING";
+    case PfRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION";
     case PfRule::SPLIT: return "SPLIT";
     case PfRule::EQ_RESOLVE: return "EQ_RESOLVE";
     case PfRule::MODUS_PONENS: return "MODUS_PONENS";

diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index ec6890293027f8dda484ab333a7088b35abfbe9f..f2c805d38dab5566166020ffb96ace7d1c5b8c68 100644 (file)
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -114,8 +114,10 @@ void InferenceManager::convert(PfRule& id,
       break;
     case PfRule::ARRAYS_EXT: children.push_back(exp); break;
     default:
-      // unknown rule, should never happen
-      Assert(false);
+      if (id != PfRule::ARRAYS_TRUST)
+      {
+        Assert(false) << "Unknown rule " << id << "\n";
+      }
       children.push_back(exp);
       args.push_back(conc);
       id = PfRule::ARRAYS_TRUST;

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 66c9b9f20a1d5dcb44aea4dd1fece6732c9ae70f..9fb76ab44adfbf6a02be44df3cf271c60fdabb0c 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1622,6 +1622,9 @@ theory::TrustNode TheoryEngine::getExplanation(
       Trace("te-proof-exp")
           << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node
           << " by " << texplanation.getNode() << std::endl;
+      // should prove the propagation we asked for
+      Assert(texplanation.getKind() == TrustNodeKind::PROP_EXP
+             && texplanation.getProven()[1] == toExplain.d_node);
       // if not a trivial explanation
       if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node))
       {

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 83c7d212d0b95001e79cf54e30f8a9432b8d49c9..ebd68a9829f139306f28a87e1d517a0e5026fdac 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -42,7 +42,8 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
 {
   d_ee = ee;
   // if proofs are enabled, also make a proof equality engine to wrap ee
-  if (d_pnm != nullptr)
+  // if it is non-null
+  if (d_pnm != nullptr && d_ee != nullptr)
   {
     d_pfee.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
                                        d_theoryState.getUserContext(),

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4cee236c19d653bbe53cb4d9945a36c66a2bc738..b9fb102676512df4ade390412df6d52af1cd135b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -709,6 +709,7 @@ set(regress_0_tests
   regress0/nl/sqrt.smt2
   regress0/nl/sqrt2-value.smt2
   regress0/nl/subs0-unsat-confirm.smt2
+  regress0/nl/tpp-fail-pf-012921.smt2
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
   regress0/opt-abd-no-use.smt2
@@ -749,6 +750,7 @@ set(regress_0_tests
   regress0/precedence/xor-and.cvc
   regress0/precedence/xor-assoc.cvc
   regress0/precedence/xor-or.cvc
+  regress0/preprocess/circuit-prop.smt2
   regress0/preprocess/preprocess_00.cvc
   regress0/preprocess/preprocess_01.cvc
   regress0/preprocess/preprocess_02.cvc
@@ -1457,6 +1459,7 @@ set(regress_1_tests
   regress1/bv/incorrect1.smtv1.smt2
   regress1/bv/issue3654.smt2
   regress1/bv/issue3776.smt2
+  regress1/bv/min-pp-rewrite-error.smt2
   regress1/bv/test-bv-abstraction.smt2
   regress1/bv/unsound1.smt2
   regress1/bvdiv2.smt2

diff --git a/test/regress/regress0/nl/tpp-fail-pf-012921.smt2 b/test/regress/regress0/nl/tpp-fail-pf-012921.smt2
new file mode 100644 (file)
index 0000000..c97a120
--- /dev/null
+++ b/test/regress/regress0/nl/tpp-fail-pf-012921.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (and (> 0.0 x) (not (= 0.0 (/ 0.0 (* 2 x))))))
+(check-sat)

diff --git a/test/regress/regress0/preprocess/circuit-prop.smt2 b/test/regress/regress0/preprocess/circuit-prop.smt2
new file mode 100644 (file)
index 0000000..6927163
--- /dev/null
+++ b/test/regress/regress0/preprocess/circuit-prop.smt2
@@ -0,0 +1,94 @@
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+
+;;;;; iteEvalThen(true)
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert a)
+(assert b)
+(assert (not (ite a b c)))
+(check-sat)
+
+(reset)
+
+;;;;; iteEvalThen(false)
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert a)
+(assert (not b))
+(assert (or (ite a b c) d))
+(check-sat)
+
+(reset)
+
+;;;;; iteEvalElse(true)
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert (not a))
+(assert c)
+(assert (not (ite a b c)))
+(check-sat)
+
+(reset)
+
+;;;;; iteEvalElse(false)
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert (not a))
+(assert (not c))
+(assert (or (ite a b c) d))
+(check-sat)
+
+(reset)
+
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert a)
+(assert b)
+(assert (=> a c))
+(assert (=> b (not c)))
+(check-sat)
+
+(reset)
+
+(set-logic ALL)
+(assert false)
+(check-sat)
+
+(reset)
+
+(set-logic ALL)
+(declare-fun x () Bool)
+(declare-fun z () Bool)
+(assert (= x z))
+(assert (not x))
+(assert z)
+(check-sat)
+
+(reset)
+
+(set-logic ALL)
+(declare-fun x3 () Bool)
+(declare-fun x9 () Bool)
+(assert (not x3))
+(assert (or x3 (and x9 x3)))
+(check-sat)

diff --git a/test/regress/regress1/bv/min-pp-rewrite-error.smt2 b/test/regress/regress1/bv/min-pp-rewrite-error.smt2
new file mode 100644 (file)
index 0000000..5106127
--- /dev/null
+++ b/test/regress/regress1/bv/min-pp-rewrite-error.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_BV)
+(set-info :status unsat)
+(declare-fun v2 () (_ BitVec 4))
+(check-sat-assuming ((and (not (= (_ bv1 4) ((_ sign_extend 3) (ite (bvsgt v2 (_ bv0 4)) (_ bv1 1) (_ bv0 1))))) (bvsge (_ bv1 1) (bvnand (_ bv1 1) (ite (= (_ bv1 4) ((_ sign_extend 3) (ite (bvslt v2 (_ bv0 4)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (bvsgt (_ bv0 4) ((_ sign_extend 3) (ite (bvsle (_ bv0 1) (ite (bvsle (_ bv1 1) (ite (bvugt (_ bv1 4) ((_ sign_extend 3) (ite (bvuge v2 (_ bv1 4)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))))))