summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/proof_rule.cpp1
-rw-r--r--src/theory/arrays/inference_manager.cpp6
-rw-r--r--src/theory/theory_engine.cpp3
-rw-r--r--src/theory/theory_inference_manager.cpp3
-rw-r--r--test/regress/CMakeLists.txt3
-rw-r--r--test/regress/regress0/nl/tpp-fail-pf-012921.smt25
-rw-r--r--test/regress/regress0/preprocess/circuit-prop.smt294
-rw-r--r--test/regress/regress1/bv/min-pp-rewrite-error.smt24
8 files changed, 116 insertions, 3 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index a8b0c8b3d..4fce88a39 100644
--- 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 ec6890293..f2c805d38 100644
--- 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 66c9b9f20..9fb76ab44 100644
--- 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 83c7d212d..ebd68a982 100644
--- 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 4cee236c1..b9fb10267 100644
--- 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
index 000000000..c97a12074
--- /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
index 000000000..69271636d
--- /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
index 000000000..510612762
--- /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)))))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback