diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/theory_engine.h | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 48 |
1 files changed, 45 insertions, 3 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ed95149b3..ff7648843 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -72,6 +72,10 @@ struct NodeTheoryPairHashFunction { } };/* struct NodeTheoryPairHashFunction */ +namespace theory { + class Instantiator; +}/* CVC4::theory namespace */ + /** * This is essentially an abstraction for a collection of theories. A * TheoryEngine provides services to a PropEngine, making various @@ -115,6 +119,11 @@ class TheoryEngine { */ SharedTermsDatabase d_sharedTerms; + /** + * The quantifiers engine + */ + theory::QuantifiersEngine* d_quantEngine; + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; @@ -151,18 +160,22 @@ class TheoryEngine { public: - IntStat conflicts, propagations, lemmas, propagationsAsDecisions; + IntStat conflicts, propagations, lemmas, propagationsAsDecisions, requirePhase, flipDecision; Statistics(theory::TheoryId theory): conflicts(mkName("theory<", theory, ">::conflicts"), 0), propagations(mkName("theory<", theory, ">::propagations"), 0), lemmas(mkName("theory<", theory, ">::lemmas"), 0), - propagationsAsDecisions(mkName("theory<", theory, ">::propagationsAsDecisions"), 0) + propagationsAsDecisions(mkName("theory<", theory, ">::propagationsAsDecisions"), 0), + requirePhase(mkName("theory<", theory, ">::requirePhase"), 0), + flipDecision(mkName("theory<", theory, ">::flipDecision"), 0) { StatisticsRegistry::registerStat(&conflicts); StatisticsRegistry::registerStat(&propagations); StatisticsRegistry::registerStat(&lemmas); StatisticsRegistry::registerStat(&propagationsAsDecisions); + StatisticsRegistry::registerStat(&requirePhase); + StatisticsRegistry::registerStat(&flipDecision); } ~Statistics() { @@ -170,6 +183,8 @@ class TheoryEngine { StatisticsRegistry::unregisterStat(&propagations); StatisticsRegistry::unregisterStat(&lemmas); StatisticsRegistry::unregisterStat(&propagationsAsDecisions); + StatisticsRegistry::unregisterStat(&requirePhase); + StatisticsRegistry::unregisterStat(&flipDecision); } };/* class TheoryEngine::Statistics */ @@ -234,6 +249,21 @@ class TheoryEngine { return d_engine->lemma(lemma, false, removable); } + void requirePhase(TNode n, bool phase) + throw(theory::Interrupted, AssertionException) { + Debug("theory") << "EngineOutputChannel::requirePhase(" + << n << ", " << phase << ")" << std::endl; + ++ d_statistics.requirePhase; + d_engine->d_propEngine->requirePhase(n, phase); + } + + bool flipDecision() + throw(theory::Interrupted, AssertionException) { + Debug("theory") << "EngineOutputChannel::flipDecision()" << std::endl; + ++ d_statistics.flipDecision; + return d_engine->d_propEngine->flipDecision(); + } + void setIncomplete() throw(AssertionException) { d_engine->setIncomplete(d_theory); } @@ -380,7 +410,7 @@ public: inline void addTheory(theory::TheoryId theoryId) { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId); - d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo); + d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo, getQuantifiersEngine()); } inline void setPropEngine(prop::PropEngine* propEngine) { @@ -400,6 +430,13 @@ public: return d_propEngine; } + /** + * Get a pointer to the underlying quantifiers engine. + */ + theory::QuantifiersEngine* getQuantifiersEngine() const { + return d_quantEngine; + } + private: /** @@ -610,6 +647,11 @@ public: return d_theoryTable[theoryId]; } + /** Get the theory for id */ + theory::Theory* getTheory(int id) { + return d_theoryTable[id]; + } + /** * Returns the equality status of the two terms, from the theory * that owns the domain type. The types of a and b must be the same. |