diff options
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 63 |
1 files changed, 28 insertions, 35 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index d0218236d..40f72dafc 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -130,19 +130,19 @@ private: TheoryId d_id; /** - * The context for the Theory. + * The SAT search context for the Theory. */ - context::Context* d_context; + context::Context* d_satContext; /** - * The user context for the Theory. + * The user level assertion context for the Theory. */ context::UserContext* d_userContext; /** * Information about the logic we're operating within. */ - const LogicInfo* d_logicInfo; + const LogicInfo& d_logicInfo; /** * The assertFact() queue. @@ -205,19 +205,20 @@ protected: /** * Construct a Theory. */ - Theory(TheoryId id, context::Context* context, context::UserContext* userContext, - OutputChannel& out, Valuation valuation) throw() : - d_id(id), - d_context(context), - d_userContext(userContext), - d_facts(context), - d_factsHead(context, 0), - d_sharedTermsIndex(context, 0), - d_careGraph(0), - d_computeCareGraphTime(statName(id, "computeCareGraphTime")), - d_sharedTerms(context), - d_out(&out), - d_valuation(valuation) + Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, + OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) throw() + : d_id(id) + , d_satContext(satContext) + , d_userContext(userContext) + , d_logicInfo(logicInfo) + , d_facts(satContext) + , d_factsHead(satContext, 0) + , d_sharedTermsIndex(satContext, 0) + , d_careGraph(0) + , d_computeCareGraphTime(statName(id, "computeCareGraphTime")) + , d_sharedTerms(satContext) + , d_out(&out) + , d_valuation(valuation) { StatisticsRegistry::registerStat(&d_computeCareGraphTime); } @@ -264,7 +265,7 @@ protected: } const LogicInfo& getLogicInfo() const { - return *d_logicInfo; + return d_logicInfo; } /** @@ -393,10 +394,10 @@ public: } /** - * Get the context associated to this Theory. + * Get the SAT context associated to this Theory. */ - context::Context* getContext() const { - return d_context; + context::Context* getSatContext() const { + return d_satContext; } /** @@ -429,7 +430,7 @@ public: * Assert a fact in the current context. */ void assertFact(TNode assertion, bool isPreregistered) { - Trace("theory") << "Theory<" << getId() << ">::assertFact[" << d_context->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl; + Trace("theory") << "Theory<" << getId() << ">::assertFact[" << d_satContext->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl; d_facts.push_back(Assertion(assertion, isPreregistered)); } @@ -457,19 +458,6 @@ public: virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } /** - * This method is called by the shared term manager when a shared - * term lhs which this theory cares about (either because it - * received a previous addSharedTerm call with lhs or because it - * received a previous notifyEq call with lhs as the second - * argument) becomes equal to another shared term rhs. This call - * also serves as notice to the theory that the shared term manager - * now considers rhs the representative for this equivalence class - * of shared terms, so future notifications for this class will be - * based on rhs not lhs. - */ - virtual void notifyEq(TNode lhs, TNode rhs) { } - - /** * Check the current assignment's consistency. * * An implementation of check() is required to either: @@ -629,6 +617,11 @@ public: return set | (1 << theory); } + /** Add the theory to the set. If no set specified, just returns a singleton set */ + static inline Set setRemove(TheoryId theory, Set set = 0) { + return set ^ (1 << theory); + } + /** Check if the set contains the theory */ static inline bool setContains(TheoryId theory, Set set) { return set & (1 << theory); |