From d97cee1a7c1a688d1ad9c748247bd9da1d86973f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 2 Feb 2021 15:12:45 -0600 Subject: [PATCH] (proof-new) Miscellaneous fixes and regressions (#5841) --- src/expr/proof_rule.cpp | 1 + src/theory/arrays/inference_manager.cpp | 6 +- src/theory/theory_engine.cpp | 3 + src/theory/theory_inference_manager.cpp | 3 +- test/regress/CMakeLists.txt | 3 + .../regress0/nl/tpp-fail-pf-012921.smt2 | 5 + .../regress0/preprocess/circuit-prop.smt2 | 94 +++++++++++++++++++ .../regress1/bv/min-pp-rewrite-error.smt2 | 4 + 8 files changed, 116 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/nl/tpp-fail-pf-012921.smt2 create mode 100644 test/regress/regress0/preprocess/circuit-prop.smt2 create mode 100644 test/regress/regress1/bv/min-pp-rewrite-error.smt2 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))))))) -- 2.30.2