From d4c7b0b250a419ec149f973abcb1c1bf3886cef3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 11 Jun 2020 23:25:15 -0500 Subject: [PATCH] (proof-new) Split TheoryEngine (#4558) This PR splits two classes from TheoryEngine (EngineOutputChannel and TheoryPreprocess) that will be undergoing further refactoring for proofs. This PR does not change their behavior and is code-move only modulo a few cosmetic changes. --- src/CMakeLists.txt | 4 + src/theory/engine_output_channel.cpp | 302 +++++++++++++++++++++++ src/theory/engine_output_channel.h | 100 ++++++++ src/theory/theory_engine.cpp | 356 ++------------------------- src/theory/theory_engine.h | 127 +--------- src/theory/theory_preprocessor.cpp | 239 ++++++++++++++++++ src/theory/theory_preprocessor.h | 81 ++++++ 7 files changed, 753 insertions(+), 456 deletions(-) create mode 100644 src/theory/engine_output_channel.cpp create mode 100644 src/theory/engine_output_channel.h create mode 100644 src/theory/theory_preprocessor.cpp create mode 100644 src/theory/theory_preprocessor.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3872e2b42..08725409b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -434,6 +434,8 @@ libcvc4_add_sources( theory/decision_strategy.h theory/eager_proof_generator.cpp theory/eager_proof_generator.h + theory/engine_output_channel.cpp + theory/engine_output_channel.h theory/evaluator.cpp theory/evaluator.h theory/ext_theory.cpp @@ -745,6 +747,8 @@ libcvc4_add_sources( theory/theory_model.h theory/theory_model_builder.cpp theory/theory_model_builder.h + theory/theory_preprocessor.cpp + theory/theory_preprocessor.h theory/theory_proof_step_buffer.cpp theory/theory_proof_step_buffer.h theory/theory_rewriter.h diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp new file mode 100644 index 000000000..176d08acf --- /dev/null +++ b/src/theory/engine_output_channel.cpp @@ -0,0 +1,302 @@ +/********************* */ +/*! \file engine_output_channel.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 The theory engine output channel. + **/ + +#include "theory/engine_output_channel.h" + +#include "proof/cnf_proof.h" +#include "proof/lemma_proof.h" +#include "proof/proof_manager.h" +#include "proof/theory_proof.h" +#include "prop/prop_engine.h" +#include "smt/smt_statistics_registry.h" +#include "theory/theory_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory) + : conflicts(getStatsPrefix(theory) + "::conflicts", 0), + propagations(getStatsPrefix(theory) + "::propagations", 0), + lemmas(getStatsPrefix(theory) + "::lemmas", 0), + requirePhase(getStatsPrefix(theory) + "::requirePhase", 0), + restartDemands(getStatsPrefix(theory) + "::restartDemands", 0), + trustedConflicts(getStatsPrefix(theory) + "::trustedConflicts", 0), + trustedLemmas(getStatsPrefix(theory) + "::trustedLemmas", 0) +{ + smtStatisticsRegistry()->registerStat(&conflicts); + smtStatisticsRegistry()->registerStat(&propagations); + smtStatisticsRegistry()->registerStat(&lemmas); + smtStatisticsRegistry()->registerStat(&requirePhase); + smtStatisticsRegistry()->registerStat(&restartDemands); + smtStatisticsRegistry()->registerStat(&trustedConflicts); + smtStatisticsRegistry()->registerStat(&trustedLemmas); +} + +EngineOutputChannel::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&conflicts); + smtStatisticsRegistry()->unregisterStat(&propagations); + smtStatisticsRegistry()->unregisterStat(&lemmas); + smtStatisticsRegistry()->unregisterStat(&requirePhase); + smtStatisticsRegistry()->unregisterStat(&restartDemands); + smtStatisticsRegistry()->unregisterStat(&trustedConflicts); + smtStatisticsRegistry()->unregisterStat(&trustedLemmas); +} + +EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine, + theory::TheoryId theory) + : d_engine(engine), d_statistics(theory), d_theory(theory) +{ +} + +void EngineOutputChannel::safePoint(ResourceManager::Resource r) +{ + spendResource(r); + if (d_engine->d_interrupted) + { + throw theory::Interrupted(); + } +} + +theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, + ProofRule rule, + bool removable, + bool preprocess, + bool sendAtoms) +{ + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" + << lemma << ")" + << ", preprocess = " << preprocess << std::endl; + ++d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + + PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); }); + + theory::LemmaStatus result = + d_engine->lemma(lemma, + rule, + false, + removable, + preprocess, + sendAtoms ? d_theory : theory::THEORY_LAST); + return result; +} + +void EngineOutputChannel::registerLemmaRecipe(Node lemma, + Node originalLemma, + bool preprocess, + theory::TheoryId theoryId) +{ + // During CNF conversion, conjunctions will be broken down into + // multiple lemmas. In order for the recipes to match, we have to do + // the same here. + NodeManager* nm = NodeManager::currentNM(); + + if (preprocess) lemma = d_engine->preprocess(lemma); + + bool negated = (lemma.getKind() == NOT); + Node nnLemma = negated ? lemma[0] : lemma; + + switch (nnLemma.getKind()) + { + case AND: + if (!negated) + { + for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) + registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId); + } + else + { + NodeBuilder<> builder(OR); + for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) + builder << nnLemma[i].negate(); + + Node disjunction = + (builder.getNumChildren() == 1) ? builder[0] : builder; + registerLemmaRecipe(disjunction, originalLemma, false, theoryId); + } + break; + + case EQUAL: + if (nnLemma[0].getType().isBoolean()) + { + if (!negated) + { + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1].negate()), + originalLemma, + false, + theoryId); + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]), + originalLemma, + false, + theoryId); + } + else + { + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1]), + originalLemma, + false, + theoryId); + registerLemmaRecipe( + nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()), + originalLemma, + false, + theoryId); + } + } + break; + + case ITE: + if (!negated) + { + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]), + originalLemma, + false, + theoryId); + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2]), + originalLemma, + false, + theoryId); + } + else + { + registerLemmaRecipe( + nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()), + originalLemma, + false, + theoryId); + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2].negate()), + originalLemma, + false, + theoryId); + } + break; + + default: break; + } + + // Theory lemmas have one step that proves the empty clause + LemmaProofRecipe proofRecipe; + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); + + // Remember the original lemma, so we can report this later when asked to + proofRecipe.setOriginalLemma(originalLemma); + + // Record the assertions and rewrites + Node rewritten; + if (lemma.getKind() == OR) + { + for (unsigned i = 0; i < lemma.getNumChildren(); ++i) + { + rewritten = theory::Rewriter::rewrite(lemma[i]); + if (rewritten != lemma[i]) + { + proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma[i]); + proofRecipe.addBaseAssertion(rewritten); + } + } + else + { + rewritten = theory::Rewriter::rewrite(lemma); + if (rewritten != lemma) + { + proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma); + proofRecipe.addBaseAssertion(rewritten); + } + proofRecipe.addStep(proofStep); + ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); +} + +theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) +{ + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" + << lemma << ")" << std::endl; + ++d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + + Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )" + << std::endl; + theory::LemmaStatus result = + d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory); + return result; +} + +bool EngineOutputChannel::propagate(TNode literal) +{ + Debug("theory::propagate") << "EngineOutputChannel<" << d_theory + << ">::propagate(" << literal << ")" << std::endl; + ++d_statistics.propagations; + d_engine->d_outputChannelUsed = true; + return d_engine->propagate(literal, d_theory); +} + +void EngineOutputChannel::conflict(TNode conflictNode, + std::unique_ptr proof) +{ + Trace("theory::conflict") + << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode + << ")" << std::endl; + Assert(!proof); // Theory shouldn't be producing proofs yet + ++d_statistics.conflicts; + d_engine->d_outputChannelUsed = true; + d_engine->conflict(conflictNode, d_theory); +} + +void EngineOutputChannel::demandRestart() +{ + NodeManager* curr = NodeManager::currentNM(); + Node restartVar = curr->mkSkolem( + "restartVar", + curr->booleanType(), + "A boolean variable asserted to be true to force a restart"); + Trace("theory::restart") << "EngineOutputChannel<" << d_theory + << ">::restart(" << restartVar << ")" << std::endl; + ++d_statistics.restartDemands; + lemma(restartVar, RULE_INVALID, true); +} + +void EngineOutputChannel::requirePhase(TNode n, bool phase) +{ + Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase + << ")" << std::endl; + ++d_statistics.requirePhase; + d_engine->getPropEngine()->requirePhase(n, phase); +} + +void EngineOutputChannel::setIncomplete() +{ + Trace("theory") << "setIncomplete()" << std::endl; + d_engine->setIncomplete(d_theory); +} + +void EngineOutputChannel::spendResource(ResourceManager::Resource r) +{ + d_engine->spendResource(r); +} + +void EngineOutputChannel::handleUserAttribute(const char* attr, + theory::Theory* t) +{ + d_engine->handleUserAttribute(attr, t); +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h new file mode 100644 index 000000000..714a206c2 --- /dev/null +++ b/src/theory/engine_output_channel.h @@ -0,0 +1,100 @@ +/********************* */ +/*! \file engine_output_channel.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 The theory engine output channel. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H +#define CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H + +#include "expr/node.h" +#include "theory/output_channel.h" +#include "theory/theory.h" +#include "util/statistics_registry.h" + +namespace CVC4 { + +class TheoryEngine; + +namespace theory { + +/** + * An output channel for Theory that passes messages back to a TheoryEngine + * for a given Theory. + * + * Notice that it has interfaces trustedConflict and trustedLemma which are + * used for ensuring that proof generators are associated with the lemmas + * and conflicts sent on this output channel. + */ +class EngineOutputChannel : public theory::OutputChannel +{ + friend class TheoryEngine; + + public: + EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory); + + void safePoint(ResourceManager::Resource r) override; + + void conflict(TNode conflictNode, + std::unique_ptr pf = nullptr) override; + bool propagate(TNode literal) override; + + theory::LemmaStatus lemma(TNode lemma, + ProofRule rule, + bool removable = false, + bool preprocess = false, + bool sendAtoms = false) override; + + theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) override; + + void demandRestart() override; + + void requirePhase(TNode n, bool phase) override; + + void setIncomplete() override; + + void spendResource(ResourceManager::Resource r) override; + + void handleUserAttribute(const char* attr, theory::Theory* t) override; + + protected: + /** + * Statistics for a particular theory. + */ + class Statistics + { + public: + Statistics(theory::TheoryId theory); + ~Statistics(); + /** Number of calls to conflict, propagate, lemma, requirePhase, + * restartDemands */ + IntStat conflicts, propagations, lemmas, requirePhase, restartDemands, + trustedConflicts, trustedLemmas; + }; + /** The theory engine we're communicating with. */ + TheoryEngine* d_engine; + /** The statistics of the theory interractions. */ + Statistics d_statistics; + /** The theory owning this channel. */ + theory::TheoryId d_theory; + /** A helper function for registering lemma recipes with the proof engine */ + void registerLemmaRecipe(Node lemma, + Node originalLemma, + bool preprocess, + theory::TheoryId theoryId); +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 71c144daa..1e4f2a7ac 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -127,144 +127,6 @@ std::string getTheoryString(theory::TheoryId id) } } -theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, - ProofRule rule, - bool removable, - bool preprocess, - bool sendAtoms) { - Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" - << lemma << ")" - << ", preprocess = " << preprocess << std::endl; - ++d_statistics.lemmas; - d_engine->d_outputChannelUsed = true; - - PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); }); - - theory::LemmaStatus result = - d_engine->lemma(lemma, rule, false, removable, preprocess, - sendAtoms ? d_theory : theory::THEORY_LAST); - return result; -} - -void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, theory::TheoryId theoryId) { - // During CNF conversion, conjunctions will be broken down into - // multiple lemmas. In order for the recipes to match, we have to do - // the same here. - NodeManager* nm = NodeManager::currentNM(); - - if (preprocess) - lemma = d_engine->preprocess(lemma); - - bool negated = (lemma.getKind() == kind::NOT); - Node nnLemma = negated ? lemma[0] : lemma; - - switch (nnLemma.getKind()) { - - case kind::AND: - if (!negated) { - for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) - registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId); - } else { - NodeBuilder<> builder(kind::OR); - for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) - builder << nnLemma[i].negate(); - - Node disjunction = (builder.getNumChildren() == 1) ? builder[0] : builder; - registerLemmaRecipe(disjunction, originalLemma, false, theoryId); - } - break; - - case kind::EQUAL: - if( nnLemma[0].getType().isBoolean() ){ - if (!negated) { - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId); - } else { - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId); - } - } - break; - - case kind::ITE: - if (!negated) { - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2]), originalLemma, false, theoryId); - } else { - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2].negate()), originalLemma, false, theoryId); - } - break; - - default: - break; - } - - // Theory lemmas have one step that proves the empty clause - LemmaProofRecipe proofRecipe; - Node emptyNode; - LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); - - // Remember the original lemma, so we can report this later when asked to - proofRecipe.setOriginalLemma(originalLemma); - - // Record the assertions and rewrites - Node rewritten; - if (lemma.getKind() == kind::OR) { - for (unsigned i = 0; i < lemma.getNumChildren(); ++i) { - rewritten = theory::Rewriter::rewrite(lemma[i]); - if (rewritten != lemma[i]) { - proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate()); - } - proofStep.addAssertion(lemma[i]); - proofRecipe.addBaseAssertion(rewritten); - } - } else { - rewritten = theory::Rewriter::rewrite(lemma); - if (rewritten != lemma) { - proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate()); - } - proofStep.addAssertion(lemma); - proofRecipe.addBaseAssertion(rewritten); - } - proofRecipe.addStep(proofStep); - ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); -} - -theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma( - TNode lemma, bool removable) { - Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" - << lemma << ")" << std::endl; - ++d_statistics.lemmas; - d_engine->d_outputChannelUsed = true; - - Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " - << lemma << " )" << std::endl; - theory::LemmaStatus result = - d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory); - return result; -} - -bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) { - Debug("theory::propagate") << "EngineOutputChannel<" << d_theory - << ">::propagate(" << literal << ")" << std::endl; - ++d_statistics.propagations; - d_engine->d_outputChannelUsed = true; - return d_engine->propagate(literal, d_theory); -} - -void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, - std::unique_ptr proof) -{ - Trace("theory::conflict") - << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode - << ")" << std::endl; - Assert(!proof); // Theory shouldn't be producing proofs yet - ++d_statistics.conflicts; - d_engine->d_outputChannelUsed = true; - d_engine->conflict(conflictNode, d_theory); -} - void TheoryEngine::finishInit() { //initialize the quantifiers engine, master equality engine, model, model builder if( d_logicInfo.isQuantified() ) { @@ -327,7 +189,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_curr_model_builder(nullptr), d_aloc_curr_model_builder(false), d_eager_model_building(false), - d_ppCache(), d_possiblePropagations(context), d_hasPropagated(context), d_inConflict(context, false), @@ -339,7 +200,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_atomRequests(context), - d_tform_remover(iteRemover), + d_tpp(*this, iteRemover), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_true(), d_false(), @@ -1073,7 +934,7 @@ void TheoryEngine::shutdown() { } } - d_ppCache.clear(); + d_tpp.clearCache(); } theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) { @@ -1099,144 +960,10 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa return solveStatus; } -// Recursively traverse a term and call the theory rewriter on its sub-terms -Node TheoryEngine::ppTheoryRewrite(TNode term) { - NodeMap::iterator find = d_ppCache.find(term); - if (find != d_ppCache.end()) { - return (*find).second; - } - unsigned nc = term.getNumChildren(); - if (nc == 0) { - return theoryOf(term)->ppRewrite(term); - } - Trace("theory-pp") << "ppTheoryRewrite { " << term << endl; - - Node newTerm; - // do not rewrite inside quantifiers - if (term.isClosure()) - { - newTerm = Rewriter::rewrite(term); - } - else - { - NodeBuilder<> newNode(term.getKind()); - if (term.getMetaKind() == kind::metakind::PARAMETERIZED) { - newNode << term.getOperator(); - } - unsigned i; - for (i = 0; i < nc; ++i) { - newNode << ppTheoryRewrite(term[i]); - } - newTerm = Rewriter::rewrite(Node(newNode)); - } - Node newTerm2 = theoryOf(newTerm)->ppRewrite(newTerm); - if (newTerm != newTerm2) { - newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2)); - } - d_ppCache[term] = newTerm; - Trace("theory-pp")<< "ppTheoryRewrite returning " << newTerm << "}" << endl; - return newTerm; -} - - -void TheoryEngine::preprocessStart() -{ - d_ppCache.clear(); -} - - -struct preprocess_stack_element { - TNode node; - bool children_added; - preprocess_stack_element(TNode n) : node(n), children_added(false) {} -};/* struct preprocess_stack_element */ - +void TheoryEngine::preprocessStart() { d_tpp.clearCache(); } Node TheoryEngine::preprocess(TNode assertion) { - - Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion << ")" << endl; - // spendResource(); - - // Do a topological sort of the subexpressions and substitute them - vector toVisit; - toVisit.push_back(assertion); - - while (!toVisit.empty()) - { - // The current node we are processing - preprocess_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.node; - - Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << endl; - - // If node already in the cache we're done, pop from the stack - NodeMap::iterator find = d_ppCache.find(current); - if (find != d_ppCache.end()) { - toVisit.pop_back(); - continue; - } - - if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(current)) && - Theory::theoryOf(current) != THEORY_SAT_SOLVER) { - stringstream ss; - ss << "The logic was specified as " << d_logicInfo.getLogicString() - << ", which doesn't include " << Theory::theoryOf(current) - << ", but got a preprocessing-time fact for that theory." << endl - << "The fact:" << endl - << current; - throw LogicException(ss.str()); - } - - // If this is an atom, we preprocess its terms with the theory ppRewriter - if (Theory::theoryOf(current) != THEORY_BOOL) { - Node ppRewritten = ppTheoryRewrite(current); - d_ppCache[current] = ppRewritten; - Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]); - continue; - } - - // Not yet substituted, so process - if (stackHead.children_added) { - // Children have been processed, so substitute - NodeBuilder<> builder(current.getKind()); - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << current.getOperator(); - } - for (unsigned i = 0; i < current.getNumChildren(); ++ i) { - Assert(d_ppCache.find(current[i]) != d_ppCache.end()); - builder << d_ppCache[current[i]]; - } - // Mark the substitution and continue - Node result = builder; - if (result != current) { - result = Rewriter::rewrite(result); - } - Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << endl; - d_ppCache[current] = result; - toVisit.pop_back(); - } else { - // Mark that we have added the children if any - if (current.getNumChildren() > 0) { - stackHead.children_added = true; - // We need to add the children - for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { - TNode childNode = *child_it; - NodeMap::iterator childFind = d_ppCache.find(childNode); - if (childFind == d_ppCache.end()) { - toVisit.push_back(childNode); - } - } - } else { - // No children, so we're done - Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << endl; - d_ppCache[current] = current; - toVisit.pop_back(); - } - } - } - - // Return the substituted version - return d_ppCache[assertion]; + return d_tpp.theoryPreprocess(assertion); } void TheoryEngine::notifyPreprocessedAssertions( @@ -1881,49 +1608,27 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, << CheckSatCommand(n.toExpr()); } - AssertionPipeline additionalLemmas; - - // Run theory preprocessing, maybe - Node ppNode = preprocess ? this->preprocess(node) : Node(node); - - // Remove the ITEs - Debug("ite") << "Remove ITE from " << ppNode << std::endl; - additionalLemmas.push_back(ppNode); - additionalLemmas.updateRealAssertionsEnd(); - d_tform_remover.run(additionalLemmas.ref(), - additionalLemmas.getIteSkolemMap()); - Debug("ite") << "..done " << additionalLemmas[0] << std::endl; - additionalLemmas.replace(0, theory::Rewriter::rewrite(additionalLemmas[0])); - - if(Debug.isOn("lemma-ites")) { - Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl; - Debug("lemma-ites") << " + now have the following " - << additionalLemmas.size() << " lemma(s):" << endl; - for(std::vector::const_iterator i = additionalLemmas.begin(); - i != additionalLemmas.end(); - ++i) { - Debug("lemma-ites") << " + " << *i << endl; - } - Debug("lemma-ites") << endl; - } - - // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node); - for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { - additionalLemmas.replace(i, theory::Rewriter::rewrite(additionalLemmas[i])); - d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node); + // the assertion pipeline storing the lemmas + AssertionPipeline lemmas; + // call preprocessor + d_tpp.preprocess(node, lemmas, preprocess); + // assert lemmas to prop engine + for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i) + { + d_propEngine->assertLemma( + lemmas[i], i == 0 && negated, removable, rule, node); } - // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + // WARNING: Below this point don't assume lemmas[0] to be not negated. if(negated) { - additionalLemmas.replace(0, additionalLemmas[0].notNode()); + lemmas.replace(0, lemmas[0].notNode()); negated = false; } // assert to decision engine if (!removable) { - d_propEngine->addAssertionsToDecisionEngine(additionalLemmas); + d_propEngine->addAssertionsToDecisionEngine(lemmas); } // Mark that we added some lemmas @@ -1931,12 +1636,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // Lemma analysis isn't online yet; this lemma may only live for this // user level. - Node retLemma = additionalLemmas[0]; - if (additionalLemmas.size() > 1) + Node retLemma = lemmas[0]; + if (lemmas.size() > 1) { // the returned lemma is the conjunction of all additional lemmas. - retLemma = - NodeManager::currentNM()->mkNode(kind::AND, additionalLemmas.ref()); + retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas.ref()); } return theory::LemmaStatus(retLemma, d_userContext->getLevel()); } @@ -2379,26 +2083,4 @@ void TheoryEngine::spendResource(ResourceManager::Resource r) d_resourceManager->spendResource(r); } -TheoryEngine::Statistics::Statistics(theory::TheoryId theory): - conflicts(getStatsPrefix(theory) + "::conflicts", 0), - propagations(getStatsPrefix(theory) + "::propagations", 0), - lemmas(getStatsPrefix(theory) + "::lemmas", 0), - requirePhase(getStatsPrefix(theory) + "::requirePhase", 0), - restartDemands(getStatsPrefix(theory) + "::restartDemands", 0) -{ - smtStatisticsRegistry()->registerStat(&conflicts); - smtStatisticsRegistry()->registerStat(&propagations); - smtStatisticsRegistry()->registerStat(&lemmas); - smtStatisticsRegistry()->registerStat(&requirePhase); - smtStatisticsRegistry()->registerStat(&restartDemands); -} - -TheoryEngine::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&conflicts); - smtStatisticsRegistry()->unregisterStat(&propagations); - smtStatisticsRegistry()->unregisterStat(&lemmas); - smtStatisticsRegistry()->unregisterStat(&requirePhase); - smtStatisticsRegistry()->unregisterStat(&restartDemands); -} - }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 233047321..1557495a0 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -36,6 +36,7 @@ #include "smt/command.h" #include "theory/atom_requests.h" #include "theory/decision_manager.h" +#include "theory/engine_output_channel.h" #include "theory/interrupted.h" #include "theory/rewriter.h" #include "theory/shared_terms_database.h" @@ -43,6 +44,7 @@ #include "theory/substitutions.h" #include "theory/term_registration_visitor.h" #include "theory/theory.h" +#include "theory/theory_preprocessor.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" #include "util/hash.h" @@ -114,6 +116,7 @@ class TheoryEngine { /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; friend class theory::quantifiers::TermDb; + friend class theory::EngineOutputChannel; /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; @@ -216,11 +219,6 @@ class TheoryEngine { typedef std::unordered_map NodeMap; typedef std::unordered_map TNodeMap; - /** - * Cache for theory-preprocessing of assertions - */ - NodeMap d_ppCache; - /** * Used for "missed-t-propagations" dumping mode only. A set of all * theory-propagable literals. @@ -234,115 +232,10 @@ class TheoryEngine { */ context::CDHashSet d_hasPropagated; - - /** - * Statistics for a particular theory. - */ - class Statistics { - - static std::string mkName(std::string prefix, - theory::TheoryId theory, - std::string suffix) { - std::stringstream ss; - ss << prefix << theory << suffix; - return ss.str(); - } - - public: - IntStat conflicts, propagations, lemmas, requirePhase, restartDemands; - - Statistics(theory::TheoryId theory); - ~Statistics(); - };/* class TheoryEngine::Statistics */ - - /** - * An output channel for Theory that passes messages - * back to a TheoryEngine. - */ - class EngineOutputChannel : public theory::OutputChannel { - friend class TheoryEngine; - - /** - * The theory engine we're communicating with. - */ - TheoryEngine* d_engine; - - /** - * The statistics of the theory interractions. - */ - Statistics d_statistics; - - /** The theory owning this channel. */ - theory::TheoryId d_theory; - - public: - EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory) - : d_engine(engine), d_statistics(theory), d_theory(theory) {} - - void safePoint(ResourceManager::Resource r) override - { - spendResource(r); - if (d_engine->d_interrupted) { - throw theory::Interrupted(); - } - } - - void conflict(TNode conflictNode, - std::unique_ptr pf = nullptr) override; - bool propagate(TNode literal) override; - - theory::LemmaStatus lemma(TNode lemma, ProofRule rule, - bool removable = false, bool preprocess = false, - bool sendAtoms = false) override; - - theory::LemmaStatus splitLemma(TNode lemma, - bool removable = false) override; - - void demandRestart() override { - NodeManager* curr = NodeManager::currentNM(); - Node restartVar = curr->mkSkolem( - "restartVar", curr->booleanType(), - "A boolean variable asserted to be true to force a restart"); - Trace("theory::restart") - << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar - << ")" << std::endl; - ++d_statistics.restartDemands; - lemma(restartVar, RULE_INVALID, true); - } - - void requirePhase(TNode n, bool phase) override { - Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " - << phase << ")" << std::endl; - ++d_statistics.requirePhase; - d_engine->d_propEngine->requirePhase(n, phase); - } - - void setIncomplete() override { - Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl; - d_engine->setIncomplete(d_theory); - } - - void spendResource(ResourceManager::Resource r) override - { - d_engine->spendResource(r); - } - - void handleUserAttribute(const char* attr, theory::Theory* t) override { - d_engine->handleUserAttribute(attr, t); - } - - private: - /** - * A helper function for registering lemma recipes with the proof engine - */ - void registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, - theory::TheoryId theoryId); - }; /* class TheoryEngine::EngineOutputChannel */ - /** * Output channels for individual theories. */ - EngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; + theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; /** * Are we in conflict. @@ -450,11 +343,12 @@ class TheoryEngine { /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId theory); - RemoveTermFormulas& d_tform_remover; - /** sort inference module */ SortInference d_sortInfer; + /** The theory preprocessor */ + theory::TheoryPreprocessor d_tpp; + /** Time spent in theory combination */ TimerStat d_combineTheoriesTime; @@ -488,7 +382,7 @@ class TheoryEngine { inline void addTheory(theory::TheoryId theoryId) { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); - d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId); + d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId); d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], @@ -542,11 +436,6 @@ class TheoryEngine { } private: - /** - * Helper for preprocess - */ - Node ppTheoryRewrite(TNode term); - /** * Queue of nodes for pre-registration. */ diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp new file mode 100644 index 000000000..7e5d1904d --- /dev/null +++ b/src/theory/theory_preprocessor.cpp @@ -0,0 +1,239 @@ +/********************* */ +/*! \file theory_preprocessor.cpp + ** \verbatim + ** Top contributors (to current version): + ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 The theory preprocessor + **/ + +#include "theory/theory_preprocessor.h" + +#include "theory/logic_info.h" +#include "theory/rewriter.h" +#include "theory/theory_engine.h" + +using namespace std; + +namespace CVC4 { +namespace theory { + +TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine, + RemoveTermFormulas& tfr) + : d_engine(engine), + d_logicInfo(engine.getLogicInfo()), + d_ppCache(), + d_tfr(tfr) +{ +} + +TheoryPreprocessor::~TheoryPreprocessor() {} + +void TheoryPreprocessor::clearCache() { d_ppCache.clear(); } + +void TheoryPreprocessor::preprocess(TNode node, + preprocessing::AssertionPipeline& lemmas, + bool doTheoryPreprocess) +{ + // Run theory preprocessing, maybe + Node ppNode = doTheoryPreprocess ? theoryPreprocess(node) : Node(node); + + // Remove the ITEs + Trace("te-tform-rm") << "Remove term formulas from " << ppNode << std::endl; + lemmas.push_back(ppNode); + lemmas.updateRealAssertionsEnd(); + d_tfr.run(lemmas.ref(), lemmas.getIteSkolemMap()); + Trace("te-tform-rm") << "..done " << lemmas[0] << std::endl; + + if (Debug.isOn("lemma-ites")) + { + Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl; + Debug("lemma-ites") << " + now have the following " << lemmas.size() + << " lemma(s):" << endl; + for (std::vector::const_iterator i = lemmas.begin(); + i != lemmas.end(); + ++i) + { + Debug("lemma-ites") << " + " << *i << endl; + } + Debug("lemma-ites") << endl; + } + + // now, rewrite the lemmas + Node retLemma; + for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i) + { + Node rewritten = Rewriter::rewrite(lemmas[i]); + lemmas.replace(i, rewritten); + } +} + +struct preprocess_stack_element +{ + TNode node; + bool children_added; + preprocess_stack_element(TNode n) : node(n), children_added(false) {} +}; + +Node TheoryPreprocessor::theoryPreprocess(TNode assertion) +{ + Trace("theory::preprocess") + << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl; + // spendResource(); + + // Do a topological sort of the subexpressions and substitute them + vector toVisit; + toVisit.push_back(assertion); + + while (!toVisit.empty()) + { + // The current node we are processing + preprocess_stack_element& stackHead = toVisit.back(); + TNode current = stackHead.node; + + Debug("theory::internal") + << "TheoryPreprocessor::theoryPreprocess(" << assertion + << "): processing " << current << endl; + + // If node already in the cache we're done, pop from the stack + NodeMap::iterator find = d_ppCache.find(current); + if (find != d_ppCache.end()) + { + toVisit.pop_back(); + continue; + } + + if (!d_logicInfo.isTheoryEnabled(Theory::theoryOf(current)) + && Theory::theoryOf(current) != THEORY_SAT_SOLVER) + { + stringstream ss; + ss << "The logic was specified as " << d_logicInfo.getLogicString() + << ", which doesn't include " << Theory::theoryOf(current) + << ", but got a preprocessing-time fact for that theory." << endl + << "The fact:" << endl + << current; + throw LogicException(ss.str()); + } + + // If this is an atom, we preprocess its terms with the theory ppRewriter + if (Theory::theoryOf(current) != THEORY_BOOL) + { + Node ppRewritten = ppTheoryRewrite(current); + d_ppCache[current] = ppRewritten; + Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]); + continue; + } + + // Not yet substituted, so process + if (stackHead.children_added) + { + // Children have been processed, so substitute + NodeBuilder<> builder(current.getKind()); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) + { + builder << current.getOperator(); + } + for (unsigned i = 0; i < current.getNumChildren(); ++i) + { + Assert(d_ppCache.find(current[i]) != d_ppCache.end()); + builder << d_ppCache[current[i]]; + } + // Mark the substitution and continue + Node result = builder; + if (result != current) + { + result = Rewriter::rewrite(result); + } + Debug("theory::internal") + << "TheoryPreprocessor::theoryPreprocess(" << assertion + << "): setting " << current << " -> " << result << endl; + d_ppCache[current] = result; + toVisit.pop_back(); + } + else + { + // Mark that we have added the children if any + if (current.getNumChildren() > 0) + { + stackHead.children_added = true; + // We need to add the children + for (TNode::iterator child_it = current.begin(); + child_it != current.end(); + ++child_it) + { + TNode childNode = *child_it; + NodeMap::iterator childFind = d_ppCache.find(childNode); + if (childFind == d_ppCache.end()) + { + toVisit.push_back(childNode); + } + } + } + else + { + // No children, so we're done + Debug("substitution::internal") + << "SubstitutionMap::internalSubstitute(" << assertion + << "): setting " << current << " -> " << current << endl; + d_ppCache[current] = current; + toVisit.pop_back(); + } + } + } + + // Return the substituted version + return d_ppCache[assertion]; +} + +// Recursively traverse a term and call the theory rewriter on its sub-terms +Node TheoryPreprocessor::ppTheoryRewrite(TNode term) +{ + NodeMap::iterator find = d_ppCache.find(term); + if (find != d_ppCache.end()) + { + return (*find).second; + } + unsigned nc = term.getNumChildren(); + if (nc == 0) + { + return d_engine.theoryOf(term)->ppRewrite(term); + } + Trace("theory-pp") << "ppTheoryRewrite { " << term << endl; + + Node newTerm; + // do not rewrite inside quantifiers + if (term.isClosure()) + { + newTerm = Rewriter::rewrite(term); + } + else + { + NodeBuilder<> newNode(term.getKind()); + if (term.getMetaKind() == kind::metakind::PARAMETERIZED) + { + newNode << term.getOperator(); + } + unsigned i; + for (i = 0; i < nc; ++i) + { + newNode << ppTheoryRewrite(term[i]); + } + newTerm = Rewriter::rewrite(Node(newNode)); + } + Node newTerm2 = d_engine.theoryOf(newTerm)->ppRewrite(newTerm); + if (newTerm != newTerm2) + { + newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2)); + } + d_ppCache[term] = newTerm; + Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl; + return newTerm; +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h new file mode 100644 index 000000000..f6caa10ec --- /dev/null +++ b/src/theory/theory_preprocessor.h @@ -0,0 +1,81 @@ +/********************* */ +/*! \file theory_preprocessor.h + ** \verbatim + ** Top contributors (to current version): + ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 The theory preprocessor. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__THEORY_PREPROCESSOR_H +#define CVC4__THEORY__THEORY_PREPROCESSOR_H + +#include + +#include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" + +namespace CVC4 { + +class LogicInfo; +class TheoryEngine; +class RemoveTermFormulas; +class LazyCDProof; + +namespace theory { + +/** + * The preprocessor used in TheoryEngine. + */ +class TheoryPreprocessor +{ + typedef std::unordered_map NodeMap; + + public: + /** Constructs a theory preprocessor */ + TheoryPreprocessor(TheoryEngine& engine, RemoveTermFormulas& tfr); + /** Destroys a theory preprocessor */ + ~TheoryPreprocessor(); + /** Clear the cache of this class */ + void clearCache(); + /** + * Preprocesses node and stores it along with lemmas generated by + * preprocessing into the assertion pipeline lemmas. The (optional) argument + * lcp is the proof that stores a proof of all top-level formulas in lemmas, + * assuming that lcp initially contains a proof of node. The flag + * doTheoryPreprocess is whether we should run theory-specific preprocessing. + */ + void preprocess(TNode node, + preprocessing::AssertionPipeline& lemmas, + bool doTheoryPreprocess); + /** + * Runs theory specific preprocessing on the non-Boolean parts of + * the formula. This is only called on input assertions, after ITEs + * have been removed. + */ + Node theoryPreprocess(TNode node); + + private: + /** Reference to owning theory engine */ + TheoryEngine& d_engine; + /** Logic info of theory engine */ + const LogicInfo& d_logicInfo; + /** Cache for theory-preprocessing of assertions */ + NodeMap d_ppCache; + /** The term formula remover */ + RemoveTermFormulas& d_tfr; + /** Helper for theoryPreprocess */ + Node ppTheoryRewrite(TNode term); +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__THEORY_PREPROCESSOR_H */ -- 2.30.2