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.
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
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
--- /dev/null
+/********************* */
+/*! \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> 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
--- /dev/null
+/********************* */
+/*! \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<Proof> 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 */
}
}
-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> 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() ) {
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),
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(),
}
}
- d_ppCache.clear();
+ d_tpp.clearCache();
}
theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
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<preprocess_stack_element> 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(
<< 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<Node>::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
// 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());
}
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 */
#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"
#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"
/** 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;
typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
typedef std::unordered_map<TNode, Node, TNodeHashFunction> 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.
*/
context::CDHashSet<Node, NodeHashFunction> 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<Proof> 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.
/** Enusre that the given atoms are send to the given theory */
void ensureLemmaAtoms(const std::vector<TNode>& 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;
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],
}
private:
- /**
- * Helper for preprocess
- */
- Node ppTheoryRewrite(TNode term);
-
/**
* Queue of nodes for pre-registration.
*/
--- /dev/null
+/********************* */
+/*! \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<Node>::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<preprocess_stack_element> 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
--- /dev/null
+/********************* */
+/*! \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 <unordered_map>
+
+#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<Node, Node, NodeHashFunction> 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 */
projects / cvc5.git / commitdiff