diff options
35 files changed, 438 insertions, 251 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 66109bfac..3103557c8 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -1069,13 +1069,22 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; if (d_theory->getId()==theory::THEORY_UF) { - th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v, + th = new theory::uf::TheoryUF(&fakeContext, + &fakeContext, + oc, + v, ProofManager::currentPM()->getLogicInfo(), + nullptr, "replay::"); } else if (d_theory->getId()==theory::THEORY_ARRAYS) { - th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v, - ProofManager::currentPM()->getLogicInfo(), - "replay::"); + th = new theory::arrays::TheoryArrays( + &fakeContext, + &fakeContext, + oc, + v, + ProofManager::currentPM()->getLogicInfo(), + nullptr, + "replay::"); } else if (d_theory->getId() == theory::THEORY_ARITH) { Trace("theory-proof-debug") << "Arith proofs currently not supported. Use 'trust'" << std::endl; os << " (clausify_false trust)"; diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 44944d0c2..4eedfd863 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -738,7 +738,8 @@ Node ProcessAssertions::expandDefinitions( theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node); Assert(t != NULL); - node = t->expandDefinition(n); + TrustNode trn = t->expandDefinition(n); + node = trn.isNull() ? Node(n) : trn.getNode(); } // the partial functions can fall through, in which case we still diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 8b4747927..83ae5a032 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -31,13 +31,17 @@ namespace CVC4 { namespace theory { namespace arith { -TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) - , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) - , d_ppRewriteTimer("theory::arith::ppRewriteTimer") - , d_proofRecorder(nullptr) +TheoryArith::TheoryArith(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm), + d_internal( + new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)), + d_ppRewriteTimer("theory::arith::ppRewriteTimer"), + d_proofRecorder(nullptr) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); // if logic is non-linear @@ -82,9 +86,10 @@ void TheoryArith::finishInit() } } -Node TheoryArith::expandDefinition(Node node) +TrustNode TheoryArith::expandDefinition(Node node) { - return d_internal->expandDefinition(node); + Node expNode = d_internal->expandDefinition(node); + return TrustNode::mkTrustRewrite(node, expNode, nullptr); } void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -95,9 +100,15 @@ void TheoryArith::addSharedTerm(TNode n){ d_internal->addSharedTerm(n); } -Node TheoryArith::ppRewrite(TNode atom) { +TrustNode TheoryArith::ppRewrite(TNode atom) +{ CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true); - return d_internal->ppRewrite(atom); + Node ret = d_internal->ppRewrite(atom); + if (ret != atom) + { + return TrustNode::mkTrustRewrite(atom, ret, nullptr); + } + return TrustNode::null(); } Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { @@ -117,8 +128,10 @@ bool TheoryArith::needsCheckLastEffort() { return d_internal->needsCheckLastEffort(); } -Node TheoryArith::explain(TNode n) { - return d_internal->explain(n); +TrustNode TheoryArith::explain(TNode n) +{ + Node exp = d_internal->explain(n); + return TrustNode::mkTrustPropExp(n, exp, nullptr); } bool TheoryArith::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 5b68e3e7a..9381b7341 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -34,7 +34,7 @@ namespace arith { * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf */ class TheoryArith : public Theory { -private: + private: friend class TheoryArithPrivate; TheoryArithPrivate* d_internal; @@ -46,9 +46,13 @@ private: */ proof::ArithProofRecorder * d_proofRecorder; -public: - TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo); + public: + TheoryArith(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr); virtual ~TheoryArith(); TheoryRewriter* getTheoryRewriter() override; @@ -60,14 +64,14 @@ public: void finishInit() override; - Node expandDefinition(Node node) override; + TrustNode expandDefinition(Node node) override; void setMasterEqualityEngine(eq::EqualityEngine* eq) override; void check(Effort e) override; bool needsCheckLastEffort() override; void propagate(Effort e) override; - Node explain(TNode n) override; + TrustNode explain(TNode n) override; bool getCurrentSubstitution(int effort, std::vector<Node>& vars, std::vector<Node>& subs, @@ -84,7 +88,7 @@ public: void presolve() override; void notifyRestart() override; PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; - Node ppRewrite(TNode atom) override; + TrustNode ppRewrite(TNode atom) override; void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; std::string identify() const override { return std::string("TheoryArith"); } @@ -100,7 +104,7 @@ public: const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) override; - void setProofRecorder(proof::ArithProofRecorder * proofRecorder) + void setProofRecorder(proof::ArithProofRecorder* proofRecorder) { d_proofRecorder = proofRecorder; } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 71e040ccc..49f93286e 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -62,8 +62,9 @@ TheoryArrays::TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + ProofNodeManager* pnm, std::string name) - : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, name), + : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name), d_numRow(name + "theory::arrays::number of Row lemmas", 0), d_numExt(name + "theory::arrays::number of Ext lemmas", 0), d_numProp(name + "theory::arrays::number of propagations", 0), @@ -315,16 +316,20 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck return term; } - -Node TheoryArrays::ppRewrite(TNode term) { - if (!d_preprocess) return term; +TrustNode TheoryArrays::ppRewrite(TNode term) +{ + if (!d_preprocess) + { + return TrustNode::null(); + } d_ppEqualityEngine.addTerm(term); + Node ret; switch (term.getKind()) { case kind::SELECT: { // select(store(a,i,v),j) = select(a,j) // IF i != j if (term[0].getKind() == kind::STORE && ppDisequal(term[0][1], term[1])) { - return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1]; + ret = NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1]; } break; } @@ -334,18 +339,22 @@ Node TheoryArrays::ppRewrite(TNode term) { if (term[0].getKind() == kind::STORE && (term[1] < term[0][1]) && ppDisequal(term[1],term[0][1])) { Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2]; Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2]; - return outer; + ret = outer; } break; } case kind::EQUAL: { - return solveWrite(term, d_solveWrite, d_solveWrite2, true); + ret = solveWrite(term, d_solveWrite, d_solveWrite2, true); break; } default: break; } - return term; + if (!ret.isNull() && ret != term) + { + return TrustNode::mkTrustRewrite(term, ret, nullptr); + } + return TrustNode::null(); } @@ -848,10 +857,10 @@ void TheoryArrays::propagate(Effort e) // direct propagation now } - -Node TheoryArrays::explain(TNode literal) { +TrustNode TheoryArrays::explain(TNode literal) +{ Node explanation = explain(literal, NULL); - return explanation; + return TrustNode::mkTrustPropExp(literal, explanation, nullptr); } Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) { @@ -2312,7 +2321,7 @@ std::string TheoryArrays::TheoryArraysDecisionStrategy::identify() const return std::string("th_arrays_dec"); } -Node TheoryArrays::expandDefinition(Node node) +TrustNode TheoryArrays::expandDefinition(Node node) { NodeManager* nm = NodeManager::currentNM(); Kind kind = node.getKind(); @@ -2362,9 +2371,10 @@ Node TheoryArrays::expandDefinition(Node node) nm->mkNode(kind::SELECT, a, k), nm->mkNode(kind::SELECT, b, k)); Node implies = nm->mkNode(kind::IMPLIES, range, eq); - return nm->mkNode(kind::FORALL, bvl, implies); + Node ret = nm->mkNode(kind::FORALL, bvl, implies); + return TrustNode::mkTrustRewrite(node, ret, nullptr); } - return node; + return TrustNode::null(); } }/* CVC4::theory::arrays namespace */ diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index c5cd24fd3..a4416ab8c 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -139,9 +139,12 @@ class TheoryArrays : public Theory { unsigned d_reasonExt; public: - - TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, + TheoryArrays(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr, std::string name = ""); ~TheoryArrays(); @@ -151,7 +154,7 @@ class TheoryArrays : public Theory { std::string identify() const override { return std::string("TheoryArrays"); } - Node expandDefinition(Node node) override; + TrustNode expandDefinition(Node node) override; ///////////////////////////////////////////////////////////////////////////// // PREPROCESSING @@ -185,7 +188,7 @@ class TheoryArrays : public Theory { public: PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; - Node ppRewrite(TNode atom) override; + TrustNode ppRewrite(TNode atom) override; ///////////////////////////////////////////////////////////////////////////// // T-PROPAGATION / REGISTRATION @@ -215,7 +218,7 @@ class TheoryArrays : public Theory { void preRegisterTerm(TNode n) override; void propagate(Effort e) override; Node explain(TNode n, eq::EqProof* proof); - Node explain(TNode n) override; + TrustNode explain(TNode n) override; ///////////////////////////////////////////////////////////////////////////// // SHARING diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 04a1675a4..022249808 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -19,6 +19,7 @@ #include <stack> #include <vector> +#include "expr/proof_node_manager.h" #include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" #include "theory/booleans/theory_bool_rewriter.h" @@ -37,9 +38,16 @@ TheoryBool::TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm) { + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + // add checkers + d_bProofChecker.registerTo(pc); + } } Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { @@ -67,22 +75,6 @@ Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubsti return Theory::ppAssert(in, outSubstitutions); } -/* -void TheoryBool::check(Effort level) { - if (done() && !fullEffort(level)) { - return; - } - while (!done()) - { - // Get all the assertions - Assertion assertion = get(); - TNode fact = assertion.assertion; - } - if( Theory::fullEffort(level) ){ - } -} -*/ - }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 99c80dd4a..2f882e257 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -20,6 +20,7 @@ #define CVC4__THEORY__BOOLEANS__THEORY_BOOL_H #include "context/context.h" +#include "theory/booleans/proof_checker.h" #include "theory/booleans/theory_bool_rewriter.h" #include "theory/theory.h" @@ -33,19 +34,20 @@ class TheoryBool : public Theory { context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo); + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr); TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; - //void check(Effort); - std::string identify() const override { return std::string("TheoryBool"); } private: /** The theory rewriter for this theory. */ TheoryBoolRewriter d_rewriter; + /** Proof rule checker */ + BoolProofRuleChecker d_bProofChecker; };/* class TheoryBool */ }/* CVC4::theory::booleans namespace */ diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 695d5b91b..f6ce4414e 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -17,6 +17,7 @@ #include "theory/builtin/theory_builtin.h" #include "expr/kind.h" +#include "expr/proof_node_manager.h" #include "theory/builtin/theory_builtin_rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" @@ -31,9 +32,16 @@ TheoryBuiltin::TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm) { + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + // add checkers + d_bProofChecker.registerTo(pc); + } } std::string TheoryBuiltin::identify() const diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index e4767645e..beca0b76a 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -19,6 +19,7 @@ #ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H #define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H +#include "theory/builtin/proof_checker.h" #include "theory/builtin/theory_builtin_rewriter.h" #include "theory/theory.h" @@ -33,7 +34,8 @@ class TheoryBuiltin : public Theory context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo); + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr); TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } @@ -45,6 +47,8 @@ class TheoryBuiltin : public Theory private: /** The theory rewriter for this theory. */ TheoryBuiltinRewriter d_rewriter; + /** Proof rule checker */ + BuiltinProofRuleChecker d_bProofChecker; }; /* class TheoryBuiltin */ } // namespace builtin diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 1bbcc05ce..c8e585d88 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -49,8 +49,9 @@ TheoryBV::TheoryBV(context::Context* c, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + ProofNodeManager* pnm, std::string name) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name), + : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name), d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), @@ -194,15 +195,16 @@ void TheoryBV::finishInit() tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM); } -Node TheoryBV::expandDefinition(Node node) +TrustNode TheoryBV::expandDefinition(Node node) { Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl; + Node ret; switch (node.getKind()) { case kind::BITVECTOR_SDIV: case kind::BITVECTOR_SREM: case kind::BITVECTOR_SMOD: - return TheoryBVRewriter::eliminateBVSDiv(node); + ret = TheoryBVRewriter::eliminateBVSDiv(node); break; case kind::BITVECTOR_UDIV: @@ -212,7 +214,8 @@ Node TheoryBV::expandDefinition(Node node) if (options::bitvectorDivByZeroConst()) { Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL; - return nm->mkNode(kind, node[0], node[1]); + ret = nm->mkNode(kind, node[0], node[1]); + break; } TNode num = node[0], den = node[1]; @@ -221,17 +224,18 @@ Node TheoryBV::expandDefinition(Node node) kind::BITVECTOR_UREM_TOTAL, num, den); Node divByZero = getBVDivByZero(node.getKind(), width); Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); - node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); - return node; + ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); } break; default: - return node; break; } - - Unreachable(); + if (!ret.isNull() && node != ret) + { + return TrustNode::mkTrustRewrite(node, ret, nullptr); + } + return TrustNode::null(); } void TheoryBV::preRegisterTerm(TNode node) { @@ -709,7 +713,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, return PP_ASSERT_STATUS_UNSOLVED; } -Node TheoryBV::ppRewrite(TNode t) +TrustNode TheoryBV::ppRewrite(TNode t) { Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; Node res = t; @@ -790,7 +794,11 @@ Node TheoryBV::ppRewrite(TNode t) d_abstractionModule->addInputAtom(res); } Debug("bv-pp-rewrite") << "to " << res << "\n"; - return res; + if (res != t) + { + return TrustNode::mkTrustRewrite(t, res, nullptr); + } + return TrustNode::null(); } void TheoryBV::presolve() { @@ -851,22 +859,26 @@ void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) { d_subtheoryMap[sub]->explain(literal, assumptions); } - -Node TheoryBV::explain(TNode node) { +TrustNode TheoryBV::explain(TNode node) +{ Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl; std::vector<TNode> assumptions; // Ask for the explanation explain(node, assumptions); // this means that it is something true at level 0 + Node explanation; if (assumptions.size() == 0) { - return utils::mkTrue(); + explanation = utils::mkTrue(); + } + else + { + // return the explanation + explanation = utils::mkAnd(assumptions); } - // return the explanation - Node explanation = utils::mkAnd(assumptions); Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl; Debug("bitvector::explain") << "TheoryBV::explain done. \n"; - return explanation; + return TrustNode::mkTrustPropExp(node, explanation, nullptr); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 513ed6bc0..c98de0f18 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -65,10 +65,13 @@ class TheoryBV : public Theory { std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories; std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; -public: - - TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, + public: + TheoryBV(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr, std::string name = ""); ~TheoryBV(); @@ -79,7 +82,7 @@ public: void finishInit() override; - Node expandDefinition(Node node) override; + TrustNode expandDefinition(Node node) override; void preRegisterTerm(TNode n) override; @@ -89,7 +92,7 @@ public: void propagate(Effort e) override; - Node explain(TNode n) override; + TrustNode explain(TNode n) override; bool collectModelInfo(TheoryModel* m) override; @@ -100,27 +103,28 @@ public: bool getCurrentSubstitution(int effort, std::vector<Node>& vars, std::vector<Node>& subs, - std::map<Node, std::vector<Node> >& exp) override; + std::map<Node, std::vector<Node>>& exp) override; int getReduction(int effort, Node n, Node& nr) override; PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; void enableCoreTheorySlicer(); - Node ppRewrite(TNode t) override; + TrustNode ppRewrite(TNode t) override; void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; void presolve() override; - bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + bool applyAbstraction(const std::vector<Node>& assertions, + std::vector<Node>& new_assertions); void setProofLog(proof::BitVectorProof* bvp); private: - - class Statistics { - public: + class Statistics + { + public: AverageStat d_avgConflictSize; IntStat d_solveSubstitutions; TimerStat d_solveTimer; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 30ee07d27..e19beb7f3 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -45,8 +45,9 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo), + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, pnm), d_infer(c), d_infer_exp(c), d_term_sk(u), @@ -558,7 +559,7 @@ void TheoryDatatypes::finishInit() { } } -Node TheoryDatatypes::expandDefinition(Node n) +TrustNode TheoryDatatypes::expandDefinition(Node n) { NodeManager* nm = NodeManager::currentNM(); // must ensure the type is well founded and has no nested recursion if @@ -583,6 +584,7 @@ Node TheoryDatatypes::expandDefinition(Node n) } } } + Node ret; switch (n.getKind()) { case kind::APPLY_SELECTOR: @@ -608,34 +610,31 @@ Node TheoryDatatypes::expandDefinition(Node n) Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]); if (options::dtRewriteErrorSel()) { - return sel; + ret = sel; } else { Node tester = c.getTester(); Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]); tst = Rewriter::rewrite(tst); - Node n_ret; if (tst == d_true) { - n_ret = sel; + ret = sel; }else{ mkExpDefSkolem(selector, ndt, n.getType()); Node sk = nm->mkNode(kind::APPLY_UF, d_exp_def_skolem[ndt][selector], n[0]); if (tst == nm->mkConst(false)) { - n_ret = sk; + ret = sk; } else { - n_ret = nm->mkNode(kind::ITE, tst, sel, sk); + ret = nm->mkNode(kind::ITE, tst, sel, sk); } } - // n_ret = Rewriter::rewrite( n_ret ); - Trace("dt-expand") << "Expand def : " << n << " to " << n_ret + Trace("dt-expand") << "Expand def : " << n << " to " << ret << std::endl; - return n_ret; } } break; @@ -681,14 +680,17 @@ Node TheoryDatatypes::expandDefinition(Node n) << b[b.getNumChildren() - 1] << std::endl; } } - Node n_ret = b; - Debug("tuprec") << "return " << n_ret << std::endl; - return n_ret; + ret = b; + Debug("tuprec") << "return " << ret << std::endl; } break; - default: return n; break; + default: break; } - Unreachable(); + if (!ret.isNull() && n != ret) + { + return TrustNode::mkTrustRewrite(n, ret, nullptr); + } + return TrustNode::null(); } void TheoryDatatypes::presolve() @@ -696,7 +698,7 @@ void TheoryDatatypes::presolve() Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; } -Node TheoryDatatypes::ppRewrite(TNode in) +TrustNode TheoryDatatypes::ppRewrite(TNode in) { Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl; @@ -712,12 +714,14 @@ Node TheoryDatatypes::ppRewrite(TNode in) nn = rew.size()==0 ? d_true : ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); } - return nn; + if (in != nn) + { + return TrustNode::mkTrustRewrite(in, nn, nullptr); + } } // nothing to do - return in; - + return TrustNode::null(); } void TheoryDatatypes::addSharedTerm(TNode t) { @@ -800,7 +804,14 @@ void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){ } } -Node TheoryDatatypes::explain( TNode literal ){ +TrustNode TheoryDatatypes::explain(TNode literal) +{ + Node exp = explainLit(literal); + return TrustNode::mkTrustPropExp(literal, exp, nullptr); +} + +Node TheoryDatatypes::explainLit(TNode literal) +{ std::vector< TNode > assumptions; explain( literal, assumptions ); return mkAnd( assumptions ); @@ -816,7 +827,8 @@ Node TheoryDatatypes::explain( std::vector< Node >& lits ) { /** Conflict when merging two constants */ void TheoryDatatypes::conflict(TNode a, TNode b){ - d_conflictNode = explain( a.eqNode(b) ); + Node eq = a.eqNode(b); + d_conflictNode = explainLit(eq); Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; @@ -869,7 +881,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ std::vector< Node > rew; if (utils::checkClash(cons1, cons2, rew)) { - d_conflictNode = explain( unifEq ); + d_conflictNode = explainLit(unifEq); Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 11c6b5f36..b2d416ecf 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -267,9 +267,12 @@ private: void computeCareGraph() override; public: - TheoryDatatypes(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo); + TheoryDatatypes(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr); ~TheoryDatatypes(); TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } @@ -285,7 +288,8 @@ private: void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions ); void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions ); void explain( TNode literal, std::vector<TNode>& assumptions ); - Node explain(TNode literal) override; + TrustNode explain(TNode literal) override; + Node explainLit(TNode literal); Node explain( std::vector< Node >& lits ); /** Conflict when merging two constants */ void conflict(TNode a, TNode b); @@ -302,8 +306,8 @@ private: bool needsCheckLastEffort() override; void preRegisterTerm(TNode n) override; void finishInit() override; - Node expandDefinition(Node n) override; - Node ppRewrite(TNode n) override; + TrustNode expandDefinition(Node n) override; + TrustNode ppRewrite(TNode n) override; void presolve() override; void addSharedTerm(TNode t) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 50c66919f..bffcda7bc 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -99,12 +99,13 @@ Node buildConjunct(const std::vector<TNode> &assumptions) { } // namespace helper /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ -TheoryFp::TheoryFp(context::Context *c, - context::UserContext *u, - OutputChannel &out, +TheoryFp::TheoryFp(context::Context* c, + context::UserContext* u, + OutputChannel& out, Valuation valuation, - const LogicInfo &logicInfo) - : Theory(THEORY_FP, c, u, out, valuation, logicInfo), + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm), d_notification(*this), d_equalityEngine(d_notification, c, "theory::fp::ee", true), d_registeredTerms(u), @@ -382,7 +383,7 @@ Node TheoryFp::abstractFloatToReal(Node node) return uf; } -Node TheoryFp::expandDefinition(Node node) +TrustNode TheoryFp::expandDefinition(Node node) { Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << std::endl; @@ -429,12 +430,12 @@ Node TheoryFp::expandDefinition(Node node) if (res != node) { Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << " rewritten to " << res << std::endl; + return TrustNode::mkTrustRewrite(node, res, nullptr); } - - return res; + return TrustNode::null(); } -Node TheoryFp::ppRewrite(TNode node) +TrustNode TheoryFp::ppRewrite(TNode node) { Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl; @@ -492,9 +493,10 @@ Node TheoryFp::ppRewrite(TNode node) { Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): node " << node << " rewritten to " << res << std::endl; + return TrustNode::mkTrustRewrite(node, res, nullptr); } - return res; + return TrustNode::null(); } bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) @@ -1010,7 +1012,8 @@ void TheoryFp::setMasterEqualityEngine(eq::EqualityEngine *eq) { d_equalityEngine.setMasterEqualityEngine(eq); } -Node TheoryFp::explain(TNode n) { +TrustNode TheoryFp::explain(TNode n) +{ Trace("fp") << "TheoryFp::explain(): explain " << n << std::endl; // All things we assert directly (and not via bit-vector) should @@ -1025,7 +1028,8 @@ Node TheoryFp::explain(TNode n) { d_equalityEngine.explainPredicate(atom, polarity, assumptions); } - return helper::buildConjunct(assumptions); + Node exp = helper::buildConjunct(assumptions); + return TrustNode::mkTrustPropExp(n, exp, nullptr); } Node TheoryFp::getModelValue(TNode var) { diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 52cd39863..a3e0dd94a 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -36,17 +36,21 @@ namespace fp { class TheoryFp : public Theory { public: /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ - TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo); + TheoryFp(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr); TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } - Node expandDefinition(Node node) override; + TrustNode expandDefinition(Node node) override; void preRegisterTerm(TNode node) override; void addSharedTerm(TNode node) override; - Node ppRewrite(TNode node) override; + TrustNode ppRewrite(TNode node) override; void check(Effort) override; @@ -58,7 +62,7 @@ class TheoryFp : public Theory { void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - Node explain(TNode n) override; + TrustNode explain(TNode n) override; protected: /** Equality engine */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 5a8cde21e..e7d5d36a3 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -18,6 +18,7 @@ #include "base/check.h" #include "expr/kind.h" +#include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/instantiation_engine.h" #include "theory/quantifiers/fmf/model_engine.h" @@ -35,8 +36,13 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo) +TheoryQuantifiers::TheoryQuantifiers(Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm) { out.handleUserAttribute( "fun-def", this ); out.handleUserAttribute( "sygus", this ); @@ -46,6 +52,13 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output out.handleUserAttribute( "quant-inst-max-level", this ); out.handleUserAttribute( "quant-elim", this ); out.handleUserAttribute( "quant-elim-partial", this ); + + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + // add the proof rules + d_qChecker.registerTo(pc); + } } TheoryQuantifiers::~TheoryQuantifiers() { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 0dab150ed..3168af195 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -19,13 +19,12 @@ #ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H -#include "context/cdhashmap.h" #include "context/context.h" #include "expr/node.h" #include "theory/output_channel.h" +#include "theory/quantifiers/proof_checker.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/theory.h" -#include "theory/theory_engine.h" #include "theory/valuation.h" #include "util/statistics_registry.h" @@ -35,9 +34,12 @@ namespace quantifiers { class TheoryQuantifiers : public Theory { public: - TheoryQuantifiers(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo); + TheoryQuantifiers(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr); ~TheoryQuantifiers(); TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } @@ -62,6 +64,8 @@ class TheoryQuantifiers : public Theory { private: /** The theory rewriter for this theory. */ QuantifiersRewriter d_rewriter; + /** The proof rule checker */ + QuantifiersProofRuleChecker d_qChecker; };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 4becfe731..372800b2b 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -39,16 +39,21 @@ namespace CVC4 { namespace theory { namespace sep { -TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_SEP, c, u, out, valuation, logicInfo), - d_lemmas_produced_c(u), - d_notify(*this), - d_equalityEngine(d_notify, c, "theory::sep::ee", true), - d_conflict(c, false), - d_reduce(u), - d_infer(c), - d_infer_exp(c), - d_spatial_assertions(c) +TheorySep::TheorySep(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_SEP, c, u, out, valuation, logicInfo, pnm), + d_lemmas_produced_c(u), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::sep::ee", true), + d_conflict(c, false), + d_reduce(u), + d_infer(c), + d_infer_exp(c), + d_spatial_assertions(c) { d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); @@ -84,12 +89,6 @@ Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) { ///////////////////////////////////////////////////////////////////////////// - -Node TheorySep::ppRewrite(TNode term) { - Trace("sep-pp") << "ppRewrite : " << term << std::endl; - return term; -} - Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { return PP_ASSERT_STATUS_UNSOLVED; @@ -139,13 +138,13 @@ void TheorySep::propagate(Effort e){ } - -Node TheorySep::explain(TNode literal) +TrustNode TheorySep::explain(TNode literal) { Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl; std::vector<TNode> assumptions; explain(literal, assumptions); - return mkAnd(assumptions); + Node exp = mkAnd(assumptions); + return TrustNode::mkTrustPropExp(literal, exp, nullptr); } @@ -833,7 +832,10 @@ bool TheorySep::needsCheckLastEffort() { void TheorySep::conflict(TNode a, TNode b) { Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl; - Node conflictNode = explain(a.eqNode(b)); + Node eq = a.eqNode(b); + std::vector<TNode> assumptions; + explain(eq, assumptions); + Node conflictNode = mkAnd(assumptions); d_conflict = true; d_out->conflict( conflictNode ); } diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 935170adf..3685ea063 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -66,7 +66,12 @@ class TheorySep : public Theory { bool pol, bool hasPol, bool underSpatial ); public: - TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheorySep(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr); ~TheorySep(); TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } @@ -81,7 +86,6 @@ class TheorySep : public Theory { public: PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; - Node ppRewrite(TNode atom) override; void ppNotifyAssertions(const std::vector<Node>& assertions) override; ///////////////////////////////////////////////////////////////////////////// @@ -97,7 +101,7 @@ class TheorySep : public Theory { public: void propagate(Effort e) override; - Node explain(TNode n) override; + TrustNode explain(TNode n) override; public: void addSharedTerm(TNode t) override; diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 7eea7926b..c4e3e9add 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -31,8 +31,9 @@ TheorySets::TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_SETS, c, u, out, valuation, logicInfo), + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm), d_internal(new TheorySetsPrivate(*this, c, u)) { // Do not move me to the header. @@ -81,8 +82,10 @@ void TheorySets::computeCareGraph() { d_internal->computeCareGraph(); } -Node TheorySets::explain(TNode node) { - return d_internal->explain(node); +TrustNode TheorySets::explain(TNode node) +{ + Node exp = d_internal->explain(node); + return TrustNode::mkTrustPropExp(node, exp, nullptr); } EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) { @@ -97,7 +100,7 @@ void TheorySets::preRegisterTerm(TNode node) { d_internal->preRegisterTerm(node); } -Node TheorySets::expandDefinition(Node n) +TrustNode TheorySets::expandDefinition(Node n) { Kind nk = n.getKind(); if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 2fd1c2145..e81412ba9 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -39,7 +39,8 @@ class TheorySets : public Theory context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo); + const LogicInfo& logicInfo, + ProofNodeManager* pnm); ~TheorySets() override; TheoryRewriter* getTheoryRewriter() override; @@ -50,12 +51,12 @@ class TheorySets : public Theory void check(Effort) override; bool collectModelInfo(TheoryModel* m) override; void computeCareGraph() override; - Node explain(TNode) override; + TrustNode explain(TNode) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; Node getModelValue(TNode) override; std::string identify() const override { return "THEORY_SETS"; } void preRegisterTerm(TNode node) override; - Node expandDefinition(Node n) override; + TrustNode expandDefinition(Node n) override; PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; void presolve() override; void propagate(Effort) override; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 83b5b1c25..fc2a992a9 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1482,7 +1482,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) } } -Node TheorySetsPrivate::expandDefinition(Node node) +TrustNode TheorySetsPrivate::expandDefinition(Node node) { Debug("sets-proc") << "expandDefinition : " << node << std::endl; @@ -1511,10 +1511,10 @@ Node TheorySetsPrivate::expandDefinition(Node node) Node ite = nm->mkNode(kind::ITE, isEmpty, equal, memberAndEqual); Node witnessVariables = nm->mkNode(BOUND_VAR_LIST, witnessVariable); Node witness = nm->mkNode(WITNESS, witnessVariables, ite); - return witness; + return TrustNode::mkTrustRewrite(node, witness, nullptr); } - return node; + return TrustNode::null(); } Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType) diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 83c58f094..c65c86795 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -208,8 +208,8 @@ class TheorySetsPrivate { * Another option to fix this is to make TheoryModel::getValue more general * so that it makes theory-specific calls to evaluate interpreted symbols. */ - Node expandDefinition(Node n); - + TrustNode expandDefinition(Node n); + void presolve(); void propagate(Theory::Effort); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d1b18df13..942c8d216 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -38,8 +38,9 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm), d_notify(*this), d_statistics(), d_equalityEngine(d_notify, c, "theory::strings::ee", true), @@ -189,18 +190,20 @@ bool TheoryStrings::propagate(TNode literal) { return ok; } - -Node TheoryStrings::explain( TNode literal ){ +TrustNode TheoryStrings::explain(TNode literal) +{ Debug("strings-explain") << "explain called on " << literal << std::endl; std::vector< TNode > assumptions; d_im->explain(literal, assumptions); + Node ret; if( assumptions.empty() ){ - return d_true; + ret = d_true; }else if( assumptions.size()==1 ){ - return assumptions[0]; + ret = assumptions[0]; }else{ - return NodeManager::currentNM()->mkNode( kind::AND, assumptions ); + ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions); } + return TrustNode::mkTrustPropExp(literal, ret, nullptr); } bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& vars, @@ -577,7 +580,7 @@ void TheoryStrings::preRegisterTerm(TNode n) d_termReg.preRegisterTerm(n); } -Node TheoryStrings::expandDefinition(Node node) +TrustNode TheoryStrings::expandDefinition(Node node) { Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl; @@ -593,14 +596,15 @@ Node TheoryStrings::expandDefinition(Node node) Node k = nm->mkBoundVar(nm->stringType()); Node bvl = nm->mkNode(BOUND_VAR_LIST, k); Node emp = Word::mkEmptyWord(node.getType()); - node = nm->mkNode( + Node ret = nm->mkNode( WITNESS, bvl, nm->mkNode( ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); + return TrustNode::mkTrustRewrite(node, ret, nullptr); } - return node; + return TrustNode::null(); } void TheoryStrings::check(Effort e) { @@ -712,11 +716,12 @@ void TheoryStrings::conflict(TNode a, TNode b){ { Debug("strings-conflict") << "Making conflict..." << std::endl; d_state.setConflict(); - Node conflictNode; - conflictNode = explain( a.eqNode(b) ); - Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; + TrustNode conflictNode = explain(a.eqNode(b)); + Trace("strings-conflict") + << "CONFLICT: Eq engine conflict : " << conflictNode.getNode() + << std::endl; ++(d_statistics.d_conflictsEqEngine); - d_out->conflict( conflictNode ); + d_out->conflict(conflictNode.getNode()); } } @@ -957,39 +962,48 @@ void TheoryStrings::checkRegisterTermsNormalForms() } } -Node TheoryStrings::ppRewrite(TNode atom) { +TrustNode TheoryStrings::ppRewrite(TNode atom) +{ Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; - Node atomElim; + Node atomRet = atom; if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP) { // aggressive elimination of regular expression membership - atomElim = d_regexp_elim.eliminate(atom); + Node atomElim = d_regexp_elim.eliminate(atomRet); if (!atomElim.isNull()) { Trace("strings-ppr") << " rewrote " << atom << " -> " << atomElim << " via regular expression elimination." << std::endl; - atom = atomElim; + atomRet = atomElim; } } if( !options::stringLazyPreproc() ){ //eager preprocess here std::vector< Node > new_nodes; StringsPreprocess* p = d_esolver->getPreprocess(); - Node ret = p->processAssertion(atom, new_nodes); - if( ret!=atom ){ - Trace("strings-ppr") << " rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl; - for( unsigned i=0; i<new_nodes.size(); i++ ){ - Trace("strings-ppr") << " lemma : " << new_nodes[i] << std::endl; + Node ret = p->processAssertion(atomRet, new_nodes); + if (ret != atomRet) + { + Trace("strings-ppr") << " rewrote " << atomRet << " -> " << ret + << ", with " << new_nodes.size() << " lemmas." + << std::endl; + for (const Node& lem : new_nodes) + { + Trace("strings-ppr") << " lemma : " << lem << std::endl; ++(d_statistics.d_lemmasEagerPreproc); - d_out->lemma( new_nodes[i] ); + d_out->lemma(lem); } - return ret; + atomRet = ret; }else{ Assert(new_nodes.empty()); } } - return atom; + if (atomRet != atom) + { + return TrustNode::mkTrustRewrite(atom, atomRet, nullptr); + } + return TrustNode::null(); } /** run the given inference step */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 368c13a2d..dfaa99c06 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -61,9 +61,12 @@ class TheoryStrings : public Theory { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet; public: - TheoryStrings(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo); + TheoryStrings(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm); ~TheoryStrings(); /** finish initialization */ void finishInit() override; @@ -76,7 +79,7 @@ class TheoryStrings : public Theory { /** Propagate */ void propagate(Effort e) override; /** Explain */ - Node explain(TNode literal) override; + TrustNode explain(TNode literal) override; /** Get the equality engine */ eq::EqualityEngine* getEqualityEngine() override; /** Get current substitution */ @@ -95,7 +98,7 @@ class TheoryStrings : public Theory { /** preregister term */ void preRegisterTerm(TNode n) override; /** Expand definition */ - Node expandDefinition(Node n) override; + TrustNode expandDefinition(Node n) override; /** Check at effort e */ void check(Effort e) override; /** needs check last effort */ @@ -105,7 +108,7 @@ class TheoryStrings : public Theory { /** called when a new equivalence class is created */ void eqNotifyNewClass(TNode t); /** preprocess rewrite */ - Node ppRewrite(TNode atom) override; + TrustNode ppRewrite(TNode atom) override; /** * Get all relevant information in this theory regarding the current * model. Return false if a contradiction is discovered. diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 9e72371d0..6fb739aa4 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -60,12 +60,14 @@ Theory::Theory(TheoryId id, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + ProofNodeManager* pnm, std::string name) : d_id(id), d_instanceName(name), d_satContext(satContext), d_userContext(userContext), d_logicInfo(logicInfo), + d_pnm(pnm), d_facts(satContext), d_factsHead(satContext, 0), d_sharedTermsIndex(satContext, 0), diff --git a/src/theory/theory.h b/src/theory/theory.h index a5234cf25..0cea604bf 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -43,12 +43,14 @@ #include "theory/output_channel.h" #include "theory/theory_id.h" #include "theory/theory_rewriter.h" +#include "theory/trust_node.h" #include "theory/valuation.h" #include "util/statistics_registry.h" namespace CVC4 { class TheoryEngine; +class ProofNodeManager; namespace theory { @@ -105,6 +107,9 @@ class Theory { /** Information about the logic we're operating within. */ const LogicInfo& d_logicInfo; + /** Pointer to proof node manager */ + ProofNodeManager* d_pnm; + /** * The assertFact() queue. * @@ -199,6 +204,7 @@ class Theory { OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + ProofNodeManager* pnm, std::string instance = ""); // taking : No default. /** @@ -440,6 +446,19 @@ class Theory { virtual void finishInit() { } /** + * Expand definitions in the term node. This returns a term that is + * equivalent to node. It wraps this term in a TrustNode of kind + * TrustNodeKind::REWRITE. If node is unchanged by this method, the + * null TrustNode may be returned. This is an optimization to avoid + * constructing the trivial equality (= node node) internally within + * TrustNode. + * + * The purpose of this method is typically to eliminate the operators in node + * that are syntax sugar that cannot otherwise be eliminated during rewriting. + * For example, division relies on the introduction of an uninterpreted + * function for the divide-by-zero case, which we do not introduce with + * the rewriter, since this function may be cached in a non-global fashion. + * * Some theories have kinds that are effectively definitions and should be * expanded before they are handled. Definitions allow a much wider range of * actions than the normal forms given by the rewriter. However no @@ -453,10 +472,10 @@ class Theory { * a theory wants to be notified about a term before preprocessing * and simplification but doesn't necessarily want to rewrite it. */ - virtual Node expandDefinition(Node node) + virtual TrustNode expandDefinition(Node node) { // by default, do nothing - return node; + return TrustNode::null(); } /** @@ -534,7 +553,8 @@ class Theory { * Return an explanation for the literal represented by parameter n * (which was previously propagated by this theory). */ - virtual Node explain(TNode n) { + virtual TrustNode explain(TNode n) + { Unimplemented() << "Theory " << identify() << " propagated a node but doesn't implement the " "Theory::explain() interface!"; @@ -579,9 +599,12 @@ class Theory { * Given an atom of the theory coming from the input formula, this * method can be overridden in a theory implementation to rewrite * the atom into an equivalent form. This is only called just - * before an input atom to the engine. + * before an input atom to the engine. This method returns a TrustNode of + * kind TrustNodeKind::REWRITE, which carries information about the proof + * generator for the rewrite. Similarly to expandDefinition, this method may + * return the null TrustNode if atom is unchanged. */ - virtual Node ppRewrite(TNode atom) { return atom; } + virtual TrustNode ppRewrite(TNode atom) { return TrustNode::null(); } /** * Notify preprocessed assertions. Called on new assertions after diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0b84893ae..851ae414e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1402,7 +1402,8 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe << " Responsible theory is: " << theoryOf(atom)->getId() << std::endl; - Node explanation = theoryOf(atom)->explain(node); + TrustNode texplanation = theoryOf(atom)->explain(node); + Node explanation = texplanation.getNode(); Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl; PROOF({ if(proofRecipe) { @@ -1877,7 +1878,8 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector } else { - explanation = theoryOf(toExplain.d_theory)->explain(toExplain.d_node); + TrustNode texp = theoryOf(toExplain.d_theory)->explain(toExplain.d_node); + explanation = texp.getNode(); Debug("theory::explain") << "\tTerm was propagated by owner theory: " << theoryOf(toExplain.d_theory)->getId() << ". Explanation: " << explanation << std::endl; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index c29ba1b4d..59d6f9583 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -388,7 +388,8 @@ class TheoryEngine { d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), - d_logicInfo); + d_logicInfo, + nullptr); theory::Rewriter::registerTheoryRewriter( theoryId, d_theoryTable[theoryId]->getTheoryRewriter()); } diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index d5a66ef9b..b12916b7d 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -201,7 +201,8 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term) unsigned nc = term.getNumChildren(); if (nc == 0) { - return d_engine.theoryOf(term)->ppRewrite(term); + TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term); + return trn.isNull() ? Node(term) : trn.getNode(); } Trace("theory-pp") << "ppTheoryRewrite { " << term << endl; @@ -225,7 +226,8 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term) } newTerm = Rewriter::rewrite(Node(newNode)); } - Node newTerm2 = d_engine.theoryOf(newTerm)->ppRewrite(newTerm); + TrustNode trn = d_engine.theoryOf(newTerm)->ppRewrite(newTerm); + Node newTerm2 = trn.isNull() ? newTerm : trn.getNode(); if (newTerm != newTerm2) { newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2)); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 8334f29d1..5d47cef4a 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -20,6 +20,7 @@ #include <memory> #include "expr/node_algorithm.h" +#include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" @@ -45,8 +46,9 @@ TheoryUF::TheoryUF(context::Context* c, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + ProofNodeManager* pnm, std::string instanceName) - : Theory(THEORY_UF, c, u, out, valuation, logicInfo, instanceName), + : Theory(THEORY_UF, c, u, out, valuation, logicInfo, pnm, instanceName), d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ @@ -61,6 +63,12 @@ TheoryUF::TheoryUF(context::Context* c, // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo()); + + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + d_ufProofChecker.registerTo(pc); + } } TheoryUF::~TheoryUF() { @@ -159,7 +167,7 @@ void TheoryUF::check(Effort level) { }else{ // support for cardinality constraints is not enabled, set incomplete d_out->setIncomplete(); - } + } } //needed for models if( options::produceModels() ){ @@ -201,7 +209,7 @@ unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) { return node.getKind()==kind::APPLY_UF ? 0 : 1; } -Node TheoryUF::expandDefinition(Node node) +TrustNode TheoryUF::expandDefinition(Node node) { Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : " << node << std::endl; @@ -216,10 +224,10 @@ Node TheoryUF::expandDefinition(Node node) { Trace("uf-exp-def") << "TheoryUF::expandDefinition: higher-order: " << node << " to " << ret << std::endl; - return ret; + return TrustNode::mkTrustRewrite(node, ret, nullptr); } } - return node; + return TrustNode::null(); } void TheoryUF::preRegisterTerm(TNode node) { @@ -304,8 +312,10 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro Debug("pf::uf") << std::endl; } -Node TheoryUF::explain(TNode literal) { - return explain(literal, NULL); +TrustNode TheoryUF::explain(TNode literal) +{ + Node exp = explain(literal, NULL); + return TrustNode::mkTrustPropExp(literal, exp, nullptr); } Node TheoryUF::explain(TNode literal, eq::EqProof* pf) { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index a3e908b1f..58f4f18a5 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -25,6 +25,7 @@ #include "expr/node_trie.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "theory/uf/proof_checker.h" #include "theory/uf/symmetry_breaker.h" #include "theory/uf/theory_uf_rewriter.h" @@ -183,8 +184,12 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, + TheoryUF(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm = nullptr, std::string instanceName = ""); ~TheoryUF(); @@ -195,9 +200,9 @@ private: void finishInit() override; void check(Effort) override; - Node expandDefinition(Node node) override; + TrustNode expandDefinition(Node node) override; void preRegisterTerm(TNode term) override; - Node explain(TNode n) override; + TrustNode explain(TNode n) override; bool collectModelInfo(TheoryModel* m) override; @@ -228,6 +233,8 @@ private: unsigned depth); TheoryUfRewriter d_rewriter; + /** Proof rule checker */ + UfProofRuleChecker d_ufProofChecker; };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 369447249..5a16fdc20 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -118,8 +118,9 @@ class FakeTheory : public Theory context::UserContext* uctxt, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo) + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm) { } @@ -155,10 +156,10 @@ class FakeTheory : public Theory void registerTerm(TNode) { Unimplemented(); } void check(Theory::Effort) override { Unimplemented(); } void propagate(Theory::Effort) override { Unimplemented(); } - Node explain(TNode) override + TrustNode explain(TNode) override { Unimplemented(); - return Node::null(); + return TrustNode::null(); } Node getValue(TNode n) { return Node::null(); } diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 2722c4df9..0ff4e918b 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -97,9 +97,14 @@ class DummyTheory : public Theory { set<Node> d_registered; vector<Node> d_getSequence; - DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo) - : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo) + DummyTheory(Context* ctxt, + UserContext* uctxt, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory( + theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, pnm) {} TheoryRewriter* getTheoryRewriter() { return nullptr; } @@ -136,7 +141,7 @@ class DummyTheory : public Theory { void presolve() override { Unimplemented(); } void preRegisterTerm(TNode n) override {} void propagate(Effort level) override {} - Node explain(TNode n) override { return Node::null(); } + TrustNode explain(TNode n) override { return TrustNode::null(); } Node getValue(TNode n) { return Node::null(); } string identify() const override { return "DummyTheory"; } };/* class DummyTheory */ @@ -180,8 +185,12 @@ class TheoryBlack : public CxxTest::TestSuite { d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL; d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL; - d_dummy = new DummyTheory( - d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo); + d_dummy = new DummyTheory(d_ctxt, + d_uctxt, + d_outputChannel, + Valuation(NULL), + *d_logicInfo, + nullptr); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); atom1 = d_nm->mkConst(false); |