diff options
27 files changed, 234 insertions, 67 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4ca57effd..7366d6eb2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -896,6 +896,8 @@ libcvc4_add_sources( theory/theory_test_utils.h theory/trust_node.cpp theory/trust_node.h + theory/trust_substitutions.cpp + theory/trust_substitutions.h theory/type_enumerator.h theory/type_set.cpp theory/type_set.h diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 4c91297a1..3d7fd120a 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -23,6 +23,7 @@ #include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" namespace CVC4 { namespace preprocessing { @@ -187,6 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( const booleans::CircuitPropagator::BackEdgesMap& backEdges = propagator->getBackEdges(); unordered_set<unsigned long> removeAssertions; + SubstitutionMap& top_level_substs = d_preprocContext->getTopLevelSubstitutions(); @@ -519,6 +521,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( NodeManager::SKOLEM_EXACT_NAME); Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero)); Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one)); + TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr); + TrustNode tleq = TrustNode::mkTrustLemma(leq, nullptr); Node n = Rewriter::rewrite(geq.andNode(leq)); assertionsToPreprocess->push_back(n); @@ -526,14 +530,15 @@ PreprocessingPassResult MipLibTrick::applyInternal( { ProofManager::currentPM()->addDependence(n, Node::null()); } - SubstitutionMap nullMap(&fakeContext); + TrustSubstitutionMap tnullMap(&fakeContext, nullptr); + CVC4_UNUSED SubstitutionMap& nullMap = tnullMap.get(); Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions - status = te->solve(geq, nullMap); + status = te->solve(tgeq, tnullMap); Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED) << "unexpected solution from arith's ppAssert()"; Assert(nullMap.empty()) << "unexpected substitution from arith's ppAssert()"; - status = te->solve(leq, nullMap); + status = te->solve(tleq, tnullMap); Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED) << "unexpected solution from arith's ppAssert()"; Assert(nullMap.empty()) diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index fcb6dd171..823e93f52 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -21,6 +21,7 @@ #include "context/cdo.h" #include "smt/smt_statistics_registry.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" using namespace CVC4; using namespace CVC4::theory; @@ -116,7 +117,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal( SubstitutionMap& top_level_substs = d_preprocContext->getTopLevelSubstitutions(); SubstitutionMap constantPropagations(d_preprocContext->getUserContext()); - SubstitutionMap newSubstitutions(d_preprocContext->getUserContext()); + TrustSubstitutionMap tnewSubstituions(d_preprocContext->getUserContext(), + nullptr); + SubstitutionMap& newSubstitutions = tnewSubstituions.get(); SubstitutionMap::iterator pos; size_t j = 0; std::vector<Node>& learned_literals = propagator->getLearnedLiterals(); @@ -178,10 +181,11 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // Solve it with the corresponding theory, possibly adding new // substitutions to newSubstitutions Trace("non-clausal-simplify") << "solving " << learnedLiteral << std::endl; - + TrustNode tlearnedLiteral = + TrustNode::mkTrustLemma(learnedLiteral, nullptr); Theory::PPAssertStatus solveStatus = - d_preprocContext->getTheoryEngine()->solve(learnedLiteral, - newSubstitutions); + d_preprocContext->getTheoryEngine()->solve(tlearnedLiteral, + tnewSubstituions); switch (solveStatus) { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e2313e10a..47595e0bb 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -150,8 +150,10 @@ TrustNode TheoryArith::ppRewriteTerms(TNode n) return d_arithPreproc.eliminate(n); } -Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { - return d_internal->ppAssert(in, outSubstitutions); +Theory::PPAssertStatus TheoryArith::ppAssert( + TrustNode tin, TrustSubstitutionMap& outSubstitutions) +{ + return d_internal->ppAssert(tin, outSubstitutions); } void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index b8f2b18fd..0055273e4 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -103,7 +103,8 @@ class TheoryArith : public Theory { void presolve() override; void notifyRestart() override; - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; + PPAssertStatus ppAssert(TrustNode tin, + TrustSubstitutionMap& outSubstitutions) override; TrustNode ppRewrite(TNode atom) override; void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index bb6ab0b9c..4e4259482 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1102,8 +1102,11 @@ Node TheoryArithPrivate::getModelValue(TNode term) { } } -Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { +Theory::PPAssertStatus TheoryArithPrivate::ppAssert( + TrustNode tin, TrustSubstitutionMap& outSubstitutions) +{ TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer); + TNode in = tin.getNode(); Debug("simplify") << "TheoryArithPrivate::solve(" << in << ")" << endl; @@ -1154,7 +1157,7 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o Debug("simplify") << "TheoryArithPrivate::solve(): substitution " << minVar << " |-> " << elim << endl; - outSubstitutions.addSubstitution(minVar, elim); + outSubstitutions.addSubstitutionSolved(minVar, elim, tin); return Theory::PP_ASSERT_STATUS_SOLVED; } else diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 1d840a81f..5cb281b36 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -465,7 +465,8 @@ private: void presolve(); void notifyRestart(); - Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + Theory::PPAssertStatus ppAssert(TrustNode tin, + TrustSubstitutionMap& outSubstitutions); void ppStaticLearn(TNode in, NodeBuilder<>& learned); std::string identify() const { return std::string("TheoryArith"); } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 3270c1c07..3e59aebe6 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -357,8 +357,10 @@ TrustNode TheoryArrays::ppRewrite(TNode term) return TrustNode::null(); } - -Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { +Theory::PPAssertStatus TheoryArrays::ppAssert( + TrustNode tin, TrustSubstitutionMap& outSubstitutions) +{ + TNode in = tin.getNode(); switch(in.getKind()) { case kind::EQUAL: { @@ -366,12 +368,12 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs d_ppEqualityEngine.assertEquality(in, true, in); if (in[0].isVar() && isLegalElimination(in[0], in[1])) { - outSubstitutions.addSubstitution(in[0], in[1]); + outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); return PP_ASSERT_STATUS_SOLVED; } if (in[1].isVar() && isLegalElimination(in[1], in[0])) { - outSubstitutions.addSubstitution(in[1], in[0]); + outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); return PP_ASSERT_STATUS_SOLVED; } break; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 0dd95795b..5236324bc 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -193,7 +193,8 @@ class TheoryArrays : public Theory { InferenceManager d_im; public: - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; + PPAssertStatus ppAssert(TrustNode tin, + TrustSubstitutionMap& outSubstitutions) override; TrustNode ppRewrite(TNode atom) override; ///////////////////////////////////////////////////////////////////////////// diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 8ce0c077a..c08012b61 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -50,8 +50,10 @@ TheoryBool::TheoryBool(context::Context* c, } } -Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { - +Theory::PPAssertStatus TheoryBool::ppAssert( + TrustNode tin, TrustSubstitutionMap& outSubstitutions) +{ + TNode in = tin.getNode(); if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) { // If we get a false literal, we're in conflict return PP_ASSERT_STATUS_CONFLICT; @@ -61,18 +63,20 @@ Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubsti if (in.getKind() == kind::NOT) { if (in[0].isVar()) { - outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false)); + outSubstitutions.addSubstitutionSolved( + in[0], NodeManager::currentNM()->mkConst<bool>(false), tin); return PP_ASSERT_STATUS_SOLVED; } } else { if (in.isVar()) { - outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst<bool>(true)); + outSubstitutions.addSubstitutionSolved( + in, NodeManager::currentNM()->mkConst<bool>(true), tin); return PP_ASSERT_STATUS_SOLVED; } } - return Theory::ppAssert(in, outSubstitutions); + return Theory::ppAssert(tin, outSubstitutions); } }/* CVC4::theory::booleans namespace */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 720ba4ed4..0a8ca2766 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -39,7 +39,8 @@ class TheoryBool : public Theory { TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; + PPAssertStatus ppAssert(TrustNode tin, + TrustSubstitutionMap& outSubstitutions) override; std::string identify() const override { return std::string("TheoryBool"); } diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index 6e251fc2d..f4b5a9d11 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -86,7 +86,7 @@ class BVSolver virtual std::string identify() const = 0; virtual Theory::PPAssertStatus ppAssert( - TNode in, SubstitutionMap& outSubstitutions) = 0; + TrustNode in, TrustSubstitutionMap& outSubstitutions) = 0; virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }; diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index 417cf0c15..a19af44ac 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -439,9 +439,10 @@ void BVSolverLazy::propagate(Theory::Effort e) } } -Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in, - SubstitutionMap& outSubstitutions) +Theory::PPAssertStatus BVSolverLazy::ppAssert( + TrustNode tin, TrustSubstitutionMap& outSubstitutions) { + TNode in = tin.getNode(); switch (in.getKind()) { case kind::EQUAL: @@ -449,13 +450,13 @@ Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in, if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1])) { ++(d_statistics.d_solveSubstitutions); - outSubstitutions.addSubstitution(in[0], in[1]); + outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); return Theory::PP_ASSERT_STATUS_SOLVED; } if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0])) { ++(d_statistics.d_solveSubstitutions); - outSubstitutions.addSubstitution(in[1], in[0]); + outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); return Theory::PP_ASSERT_STATUS_SOLVED; } Node node = Rewriter::rewrite(in); @@ -502,7 +503,7 @@ Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in, Assert(utils::getSize(concat) == utils::getSize(extract[0])); if (d_bv.isLegalElimination(extract[0], concat)) { - outSubstitutions.addSubstitution(extract[0], concat); + outSubstitutions.addSubstitutionSolved(extract[0], concat, tin); return Theory::PP_ASSERT_STATUS_SOLVED; } } diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h index b72d53e58..6885dbba4 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_lazy.h @@ -92,8 +92,8 @@ class BVSolverLazy : public BVSolver std::string identify() const override { return std::string("BVSolverLazy"); } - Theory::PPAssertStatus ppAssert(TNode in, - SubstitutionMap& outSubstitutions) override; + Theory::PPAssertStatus ppAssert( + TrustNode tin, TrustSubstitutionMap& outSubstitutions) override; TrustNode ppRewrite(TNode t) override; diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h index b7d86cf67..59239a52c 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_simple.h @@ -53,8 +53,8 @@ class BVSolverSimple : public BVSolver std::string identify() const override { return "BVSolverSimple"; }; - Theory::PPAssertStatus ppAssert(TNode in, - SubstitutionMap& outSubstitutions) override + Theory::PPAssertStatus ppAssert( + TrustNode in, TrustSubstitutionMap& outSubstitutions) override { return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED; } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 79a20c9c9..d43fa3927 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -37,7 +37,7 @@ TheoryBV::TheoryBV(context::Context* c, d_ufRemByZero(), d_rewriter(), d_state(c, u, valuation), - d_inferMgr(*this, d_state, pnm) + d_inferMgr(*this, d_state, nullptr) { switch (options::bvSolver()) { @@ -194,10 +194,10 @@ bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); } -Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, - SubstitutionMap& outSubstitutions) +Theory::PPAssertStatus TheoryBV::ppAssert( + TrustNode tin, TrustSubstitutionMap& outSubstitutions) { - return d_internal->ppAssert(in, outSubstitutions); + return d_internal->ppAssert(tin, outSubstitutions); } TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index a01c74382..fa228131c 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -87,7 +87,8 @@ class TheoryBV : public Theory std::string identify() const override { return std::string("TheoryBV"); } - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; + PPAssertStatus ppAssert(TrustNode in, + TrustSubstitutionMap& outSubstitutions) override; TrustNode ppRewrite(TNode t) override; diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index b18ae5b95..013c61e52 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -50,7 +50,7 @@ TheorySep::TheorySep(context::Context* c, d_lemmas_produced_c(u), d_bounds_init(false), d_state(c, u, valuation), - d_im(*this, d_state, pnm), + d_im(*this, d_state, nullptr), d_notify(*this), d_reduce(u), d_spatial_assertions(c) @@ -96,16 +96,6 @@ Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) { } } -///////////////////////////////////////////////////////////////////////////// -// PREPROCESSING -///////////////////////////////////////////////////////////////////////////// - - -Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { - - return PP_ASSERT_STATUS_UNSOLVED; -} - ///////////////////////////////////////////////////////////////////////////// // T-PROPAGATION / REGISTRATION diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 58c3a4b28..ac87ebe67 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -99,8 +99,6 @@ class TheorySep : public Theory { ///////////////////////////////////////////////////////////////////////////// public: - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; - void ppNotifyAssertions(const std::vector<Node>& assertions) override; ///////////////////////////////////////////////////////////////////////////// // T-PROPAGATION / REGISTRATION diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 9823434c6..763024d5f 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -36,7 +36,7 @@ TheorySets::TheorySets(context::Context* c, : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm), d_skCache(), d_state(c, u, valuation, d_skCache), - d_im(*this, d_state, pnm), + d_im(*this, d_state, nullptr), d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)), d_notify(*d_internal.get(), d_im) { @@ -153,7 +153,10 @@ TrustNode TheorySets::expandDefinition(Node n) return d_internal->expandDefinition(n); } -Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { +Theory::PPAssertStatus TheorySets::ppAssert( + TrustNode tin, TrustSubstitutionMap& outSubstitutions) +{ + TNode in = tin.getNode(); Debug("sets-proc") << "ppAssert : " << in << std::endl; Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED; @@ -168,7 +171,7 @@ Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubsti // regress0/sets/pre-proc-univ.smt2 if (!in[0].getType().isSet() || !options::setsExt()) { - outSubstitutions.addSubstitution(in[0], in[1]); + outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); status = Theory::PP_ASSERT_STATUS_SOLVED; } } @@ -176,7 +179,7 @@ Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubsti { if (!in[0].getType().isSet() || !options::setsExt()) { - outSubstitutions.addSubstitution(in[1], in[0]); + outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); status = Theory::PP_ASSERT_STATUS_SOLVED; } } diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index ddc0bd45e..a5f8fa4d8 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -77,7 +77,8 @@ class TheorySets : public Theory std::string identify() const override { return "THEORY_SETS"; } void preRegisterTerm(TNode node) override; TrustNode expandDefinition(Node n) override; - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; + PPAssertStatus ppAssert(TrustNode tin, + TrustSubstitutionMap& outSubstitutions) override; void presolve() override; bool isEntailed(Node n, bool pol); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 2a471ec0d..757f94d5b 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -375,9 +375,10 @@ bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) return true; } -Theory::PPAssertStatus Theory::ppAssert(TNode in, - SubstitutionMap& outSubstitutions) +Theory::PPAssertStatus Theory::ppAssert(TrustNode tin, + TrustSubstitutionMap& outSubstitutions) { + TNode in = tin.getNode(); if (in.getKind() == kind::EQUAL) { // (and (= x t) phi) can be replaced by phi[x/t] if diff --git a/src/theory/theory.h b/src/theory/theory.h index 6f6c863df..86dbb60d6 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -44,6 +44,7 @@ #include "theory/theory_rewriter.h" #include "theory/theory_state.h" #include "theory/trust_node.h" +#include "theory/trust_substitutions.h" #include "theory/valuation.h" #include "util/statistics_registry.h" @@ -699,10 +700,16 @@ class Theory { }; /** - * Given a literal, add the solved substitutions to the map, if any. - * The method should return true if the literal can be safely removed. + * Given a literal and its proof generator (encapsulated by trust node tin), + * add the solved substitutions to the map, if any. The method should return + * true if the literal can be safely removed from the input problem. + * + * Note that tin has trude node kind LEMMA. Its proof generator should be + * take into account when adding a substitution to outSubstitutions when + * proofs are enabled. */ - virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + virtual PPAssertStatus ppAssert(TrustNode tin, + TrustSubstitutionMap& outSubstitutions); /** * Given an atom of the theory coming from the input formula, this diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 47dca7d66..4722251a3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -823,10 +823,13 @@ void TheoryEngine::shutdown() { d_tpp.clearCache(); } -theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) { +theory::Theory::PPAssertStatus TheoryEngine::solve( + TrustNode tliteral, TrustSubstitutionMap& substitutionOut) +{ // Reset the interrupt flag d_interrupted = false; + TNode literal = tliteral.getNode(); TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl; @@ -841,7 +844,8 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa throw LogicException(ss.str()); } - Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut); + Theory::PPAssertStatus solveStatus = + theoryOf(atom)->ppAssert(tliteral, substitutionOut); Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl; return solveStatus; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index cfca03515..e410bddd5 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -494,10 +494,13 @@ class TheoryEngine { void shutdown(); /** - * Solve the given literal with a theory that owns it. + * Solve the given literal with a theory that owns it. The proof of tliteral + * is carried in the trust node. The proof added to substitutionOut should + * take this proof into account (when proofs are enabled). */ - theory::Theory::PPAssertStatus solve(TNode literal, - theory::SubstitutionMap& substitutionOut); + theory::Theory::PPAssertStatus solve( + theory::TrustNode tliteral, + theory::TrustSubstitutionMap& substitutionOut); /** * Preregister a Theory atom with the responsible theory (or diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp new file mode 100644 index 000000000..de8fc2ceb --- /dev/null +++ b/src/theory/trust_substitutions.cpp @@ -0,0 +1,60 @@ +/********************* */ +/*! \file trust_substitutions.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Trust substitutions + **/ + +#include "theory/trust_substitutions.h" + +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { + +TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, + ProofNodeManager* pnm) + : d_subs(c) +{ +} + +void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg) +{ + d_subs.addSubstitution(x, t); +} + +TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite) +{ + Node ns = d_subs.apply(n); + if (doRewrite) + { + ns = Rewriter::rewrite(ns); + } + return TrustNode::mkTrustRewrite(n, ns, nullptr); +} + +void TrustSubstitutionMap::addSubstitutionSolved(TNode x, TNode t, TrustNode tn) +{ + if (!isProofEnabled() || tn.getGenerator() == nullptr) + { + // no generator or not proof enabled, nothing to do + addSubstitution(x, t, nullptr); + return; + } + // NOTE: can try to transform tn.getProven() to (= x t) here + addSubstitution(x, t, nullptr); +} + +SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; } + +bool TrustSubstitutionMap::isProofEnabled() const { return false; } + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h new file mode 100644 index 000000000..0eacc50f5 --- /dev/null +++ b/src/theory/trust_substitutions.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file trust_substitutions.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Trust substitutions + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__TRUST_SUBSTITUTIONS_H +#define CVC4__THEORY__TRUST_SUBSTITUTIONS_H + +#include "context/context.h" +#include "expr/proof_node_manager.h" +#include "theory/substitutions.h" +#include "theory/trust_node.h" + +namespace CVC4 { +namespace theory { + +/** + * A layer on top of SubstitutionMap that tracks proofs. + */ +class TrustSubstitutionMap +{ + public: + TrustSubstitutionMap(context::Context* c, ProofNodeManager* pnm); + /** Gets a reference to the underlying substitution map */ + SubstitutionMap& get(); + /** + * Add substitution x -> t, where pg can provide a closed proof of (= x t) + * in the remainder of this user context. + */ + void addSubstitution(TNode x, TNode t, ProofGenerator* pg = nullptr); + /** + * Add substitution x -> t, which was derived from the proven field of + * trust node tn. In other words, (= x t) is the solved form of + * tn.getProven(). This method is a helper function for methods (e.g. + * ppAssert) that put literals into solved form. It should be the case + * that (= x t) and tn.getProven() can be shown equivalent by rewriting. + * + * This ensures that we add a substitution with a proof + * based on transforming the tn.getProven() to (= x t) if tn has a + * non-null proof generator; otherwise if tn has no proof generator + * we simply add the substitution. + */ + void addSubstitutionSolved(TNode x, TNode t, TrustNode tn); + /** + * Apply substitutions in this class to node n. Returns a trust node + * proving n = n*sigma, where the proof generator is provided by this class + * (when proofs are enabled). + */ + TrustNode apply(Node n, bool doRewrite = true); + + private: + /** Are proofs enabled? */ + bool isProofEnabled() const; + /** The substitution map */ + SubstitutionMap d_subs; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__TRUST_SUBSTITUTIONS_H */ |