From c5a6aa2e03b05a5db6150563a4d5994abf5b24e9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 10 Jul 2020 19:03:24 -0500 Subject: (proof-new) Update Theory interface for proof-new (#4648) This includes 4 changes: Theory constructor takes a ProofNodeManager, Theory::explain returns a TrustNode (of kind PROP_EXP), Theory::expandDefinitions returns a TrustNode (of kind REWRITE), Theory::ppRewrite returns a TrustNode (of kind REWRITE). These are all currently planned updates to the interface of Theory. This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support. This PR is also contingent on the performance tests for proof-new on SMT-LIB. --- src/theory/arith/theory_arith.cpp | 39 ++++++++++++++++++++++++++------------- src/theory/arith/theory_arith.h | 20 ++++++++++++-------- 2 files changed, 38 insertions(+), 21 deletions(-) (limited to 'src/theory/arith') 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& vars, std::vector& 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; } -- cgit v1.2.3