diff options
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 127 |
1 files changed, 8 insertions, 119 deletions
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; @@ -217,11 +220,6 @@ class TheoryEngine { 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. */ @@ -234,115 +232,10 @@ class TheoryEngine { */ 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. @@ -450,11 +343,12 @@ class TheoryEngine { /** 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; @@ -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], @@ -543,11 +437,6 @@ class TheoryEngine { private: /** - * Helper for preprocess - */ - Node ppTheoryRewrite(TNode term); - - /** * Queue of nodes for pre-registration. */ std::queue<TNode> d_preregisterQueue; |