diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 130 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 59 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 30 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 27 |
4 files changed, 192 insertions, 54 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index a8a92096c..8352373c5 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -36,6 +36,7 @@ #include "prop/sat_solver_factory.h" #include "prop/theory_proxy.h" #include "smt/smt_statistics_registry.h" +#include "theory/output_channel.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" #include "util/resource_manager.h" @@ -94,8 +95,14 @@ PropEngine::PropEngine(TheoryEngine* te, d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::CnfStream( d_satSolver, d_registrar, userContext, &d_outMgr, rm, true); - d_theoryProxy = new TheoryProxy( - this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream); + + d_theoryProxy = new TheoryProxy(this, + d_theoryEngine, + d_decisionEngine.get(), + d_context, + userContext, + d_cnfStream, + pnm); d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm); d_decisionEngine->setSatSolver(d_satSolver); @@ -143,6 +150,16 @@ PropEngine::~PropEngine() { delete d_theoryProxy; } +theory::TrustNode PropEngine::preprocess( + TNode node, + std::vector<theory::TrustNode>& newLemmas, + std::vector<Node>& newSkolems, + bool doTheoryPreprocess) +{ + return d_theoryProxy->preprocess( + node, newLemmas, newSkolems, doTheoryPreprocess); +} + void PropEngine::notifyPreprocessedAssertions( const preprocessing::AssertionPipeline& ap) { @@ -168,7 +185,6 @@ void PropEngine::notifyPreprocessedAssertions( void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; Debug("prop") << "assertFormula(" << node << ")" << endl; - // Assert as non-removable if (isProofEnabled()) { d_pfCnfStream->convertAndAssert(node, false, false, nullptr); @@ -181,35 +197,47 @@ void PropEngine::assertFormula(TNode node) { } } -void PropEngine::assertLemma(theory::TrustNode trn, bool removable) +Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) { - Node node = trn.getNode(); - bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; - Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; - // Assert as (possibly) removable - if (isProofEnabled()) + bool removable = isLemmaPropertyRemovable(p); + bool preprocess = isLemmaPropertyPreprocess(p); + + // call preprocessor + std::vector<theory::TrustNode> ppLemmas; + std::vector<Node> ppSkolems; + theory::TrustNode tplemma = + d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems, preprocess); + + Assert(ppSkolems.size() == ppLemmas.size()); + + // do final checks on the lemmas we are about to send + if (isProofEnabled() && options::proofNewEagerChecking()) { - Assert(trn.getGenerator()); - d_pfCnfStream->convertAndAssert( - node, negated, removable, trn.getGenerator()); + Assert(tplemma.getGenerator() != nullptr); + // ensure closed, make the proof node eagerly here to debug + tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma"); + for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) + { + Assert(ppLemmas[i].getGenerator() != nullptr); + ppLemmas[i].debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new"); + } } - else + + if (Trace.isOn("te-lemma")) { - d_cnfStream->convertAndAssert(node, removable, negated); + Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl; + for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) + { + Trace("te-lemma") << "Lemma, new lemma: " << ppLemmas[i].getProven() + << " (skolem is " << ppSkolems[i] << ")" << std::endl; + } } -} -void PropEngine::assertLemmas(theory::TrustNode lem, - std::vector<theory::TrustNode>& ppLemmas, - std::vector<Node>& ppSkolems, - bool removable) -{ - Assert(ppSkolems.size() == ppLemmas.size()); - // assert the lemmas - assertLemma(lem, removable); + // now, assert the lemmas + assertLemmaInternal(tplemma, removable); for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) { - assertLemma(ppLemmas[i], removable); + assertLemmaInternal(ppLemmas[i], removable); } // assert to decision engine @@ -217,7 +245,7 @@ void PropEngine::assertLemmas(theory::TrustNode lem, { // also add to the decision engine, where notice we don't need proofs std::vector<Node> assertions; - assertions.push_back(lem.getProven()); + assertions.push_back(tplemma.getProven()); std::vector<Node> ppLemmasF; for (const theory::TrustNode& tnl : ppLemmas) { @@ -225,6 +253,38 @@ void PropEngine::assertLemmas(theory::TrustNode lem, } d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems); } + + // make the return lemma, which the theory engine will use + Node retLemma = tplemma.getProven(); + if (!ppLemmas.empty()) + { + std::vector<Node> lemmas{retLemma}; + for (const theory::TrustNode& tnl : ppLemmas) + { + lemmas.push_back(tnl.getProven()); + } + // the returned lemma is the conjunction of all additional lemmas. + retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas); + } + return retLemma; +} + +void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable) +{ + Node node = trn.getNode(); + bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; + Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; + // Assert as (possibly) removable + if (isProofEnabled()) + { + Assert(trn.getGenerator()); + d_pfCnfStream->convertAndAssert( + node, negated, removable, trn.getGenerator()); + } + else + { + d_cnfStream->convertAndAssert(node, removable, negated); + } } void PropEngine::requirePhase(TNode n, bool phase) { @@ -361,7 +421,25 @@ void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const d_cnfStream->getBooleanVariables(outputVariables); } -void PropEngine::ensureLiteral(TNode n) { d_cnfStream->ensureLiteral(n); } +Node PropEngine::ensureLiteral(TNode n) +{ + // must preprocess + std::vector<theory::TrustNode> newLemmas; + std::vector<Node> newSkolems; + theory::TrustNode tpn = + d_theoryProxy->preprocess(n, newLemmas, newSkolems, true); + // send lemmas corresponding to the skolems introduced by preprocessing n + for (const theory::TrustNode& tnl : newLemmas) + { + Trace("ensureLiteral") << " lemma: " << tnl.getNode() << std::endl; + assertLemma(tnl, theory::LemmaProperty::NONE); + } + Node preprocessed = tpn.isNull() ? Node(n) : tpn.getNode(); + Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed + << std::endl; + d_cnfStream->ensureLiteral(preprocessed); + return preprocessed; +} void PropEngine::push() { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 55a42c2a7..ac2b35ad6 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -95,6 +95,23 @@ class PropEngine void shutdown() {} /** + * Preprocess the given node. Return the REWRITE trust node corresponding to + * rewriting node. New lemmas and skolems are added to ppLemmas and + * ppSkolems respectively. + * + * @param node The assertion to preprocess, + * @param ppLemmas The lemmas to add to the set of assertions, + * @param ppSkolems The skolems that newLemmas correspond to, + * @param doTheoryPreprocess whether to run theory-specific preprocessing. + * @return The (REWRITE) trust node corresponding to rewritten node via + * preprocessing. + */ + theory::TrustNode preprocess(TNode node, + std::vector<theory::TrustNode>& ppLemmas, + std::vector<Node>& ppSkolems, + bool doTheoryPreprocess); + + /** * Notify preprocessed assertions. This method is called just before the * assertions are asserted to this prop engine. This method notifies the * decision engine and the theory engine of the assertions in ap. @@ -114,27 +131,10 @@ class PropEngine * than the (SAT and SMT) level at which it was asserted. * * @param trn the trust node storing the formula to assert - * @param removable whether this lemma can be quietly removed based - * on an activity heuristic + * @param p the properties of the lemma + * @return the (preprocessed) lemma */ - void assertLemma(theory::TrustNode trn, bool removable); - - /** - * Assert lemma trn with preprocessing lemmas ppLemmas which correspond - * to lemmas for skolems in ppSkolems. - * - * @param trn the trust node storing the formula to assert - * @param ppLemmas the lemmas from preprocessing and term formula removal on - * the proven node of trn - * @param ppSkolem the skolem that each lemma in ppLemma constrains. It should - * be the case that ppLemmas.size()==ppSkolems.size(). - * @param removable whether this lemma can be quietly removed based - * on an activity heuristic - */ - void assertLemmas(theory::TrustNode trn, - std::vector<theory::TrustNode>& ppLemmas, - std::vector<Node>& ppSkolems, - bool removable); + Node assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p); /** * If ever n is decided upon, it must be in the given phase. This @@ -185,10 +185,11 @@ class PropEngine /** * Ensure that the given node will have a designated SAT literal - * that is definitionally equal to it. The result of this function - * is that the Node can be queried via getSatValue(). + * that is definitionally equal to it. Note that theory preprocessing is + * applied to n. The node returned by this method can be subsequently queried + * via getSatValue(). */ - void ensureLiteral(TNode n); + Node ensureLiteral(TNode n); /** * Push the context level. @@ -261,6 +262,18 @@ class PropEngine private: /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); + + /** + * Converts the given formula to CNF and asserts the CNF to the SAT solver. + * The formula can be removed by the SAT solver after backtracking lower + * than the (SAT and SMT) level at which it was asserted. + * + * @param trn the trust node storing the formula to assert + * @param removable whether this lemma can be quietly removed based + * on an activity heuristic + */ + void assertLemmaInternal(theory::TrustNode trn, bool removable); + /** * Indicates that the SAT solver is currently solving something and we should * not mess with it's internal state. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 1b9e78d80..23405675a 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -19,15 +19,14 @@ #include "context/context.h" #include "decision/decision_engine.h" #include "options/decision_options.h" +#include "proof/cnf_proof.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" -#include "proof/cnf_proof.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" #include "util/statistics_registry.h" - namespace CVC4 { namespace prop { @@ -35,12 +34,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream) + context::UserContext* userContext, + CnfStream* cnfStream, + ProofNodeManager* pnm) : d_propEngine(propEngine), d_cnfStream(cnfStream), d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), - d_queue(context) + d_queue(context), + d_tpp(*theoryEngine, userContext, pnm) { } @@ -165,5 +167,25 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; } +theory::TrustNode TheoryProxy::preprocessLemma( + theory::TrustNode trn, + std::vector<theory::TrustNode>& newLemmas, + std::vector<Node>& newSkolems, + bool doTheoryPreprocess) +{ + return d_tpp.preprocessLemma(trn, newLemmas, newSkolems, doTheoryPreprocess); +} + +theory::TrustNode TheoryProxy::preprocess( + TNode node, + std::vector<theory::TrustNode>& newLemmas, + std::vector<Node>& newSkolems, + bool doTheoryPreprocess) +{ + theory::TrustNode pnode = + d_tpp.preprocess(node, newLemmas, newSkolems, doTheoryPreprocess); + return pnode; +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index e16728d0d..4d460434d 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -26,10 +26,13 @@ #include <iosfwd> #include <unordered_set> +#include "context/cdhashmap.h" #include "context/cdqueue.h" #include "expr/node.h" #include "prop/sat_solver.h" #include "theory/theory.h" +#include "theory/theory_preprocessor.h" +#include "theory/trust_node.h" #include "util/resource_manager.h" #include "util/statistics_registry.h" @@ -53,7 +56,9 @@ class TheoryProxy TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream); + context::UserContext* userContext, + CnfStream* cnfStream, + ProofNodeManager* pnm); ~TheoryProxy(); @@ -90,6 +95,23 @@ class TheoryProxy CnfStream* getCnfStream(); + /** + * Call the preprocessor on node, return trust node corresponding to the + * rewrite. + */ + theory::TrustNode preprocessLemma(theory::TrustNode trn, + std::vector<theory::TrustNode>& newLemmas, + std::vector<Node>& newSkolems, + bool doTheoryPreprocess); + /** + * Call the preprocessor on node, return trust node corresponding to the + * rewrite. + */ + theory::TrustNode preprocess(TNode node, + std::vector<theory::TrustNode>& newLemmas, + std::vector<Node>& newSkolems, + bool doTheoryPreprocess); + private: /** The prop engine we are using. */ PropEngine* d_propEngine; @@ -111,6 +133,9 @@ class TheoryProxy * all imported and exported lemmas. */ std::unordered_set<Node, NodeHashFunction> d_shared; + + /** The theory preprocessor */ + theory::TheoryPreprocessor d_tpp; }; /* class TheoryProxy */ }/* CVC4::prop namespace */ |