diff options
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 185 |
1 files changed, 158 insertions, 27 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 020a2b194..8c830f8a2 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -46,6 +46,10 @@ class TheoryEngine; namespace theory { +class Instantiator; +class InstStrategy; +class QuantifiersEngine; + /** * Information about an assertion for the theories. */ @@ -72,7 +76,8 @@ struct Assertion { operator Node () const { return assertion; } -}; + +};/* struct Assertion */ /** * A (oredered) pair of terms a theory cares about. @@ -84,7 +89,7 @@ struct CarePair { public: - CarePair(TNode a, TNode b, TheoryId theory) + CarePair(TNode a, TNode b, TheoryId theory) : a(a < b ? a : b), b(a < b ? b : a), theory(theory) {} bool operator == (const CarePair& other) const { @@ -99,7 +104,7 @@ public: return b < other.b; } -}; +};/* struct CarePair */ /** * A set of care pairs. @@ -172,6 +177,18 @@ private: */ CareGraph* d_careGraph; + /** + * Reference to the quantifiers engine (or NULL, if quantifiers are + * not supported or not enabled). + */ + QuantifiersEngine* d_quantEngine; + + /** + * The instantiator for this theory, or NULL if quantifiers are not + * supported or not enabled. + */ + Instantiator* d_inst; + // === STATISTICS === /** time spent in theory combination */ TimerStat d_computeCareGraphTime; @@ -182,6 +199,12 @@ private: return ss.str(); } + /** + * Construct and return the instantiator for the given theory. + * If there is no instantiator class, NULL is returned. + */ + theory::Instantiator* makeInstantiator(context::Context* c, theory::QuantifiersEngine* qe); + protected: /** @@ -208,7 +231,7 @@ protected: * Construct a Theory. */ Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, - OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) throw() + OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) throw() : d_id(id) , d_satContext(satContext) , d_userContext(userContext) @@ -217,6 +240,8 @@ protected: , d_factsHead(satContext, 0) , d_sharedTermsIndex(satContext, 0) , d_careGraph(0) + , d_quantEngine(qe) + , d_inst(makeInstantiator(satContext, qe)) , d_computeCareGraphTime(statName(id, "computeCareGraphTime")) , d_sharedTerms(satContext) , d_out(&out) @@ -252,19 +277,7 @@ protected: * * @return the next assertion in the assertFact() queue */ - Assertion get() { - Assert( !done(), "Theory`() called with assertion queue empty!" ); - - // Get the assertion - Assertion fact = d_facts[d_factsHead]; - d_factsHead = d_factsHead + 1; - Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl; - if(Dump.isOn("state")) { - Dump("state") << AssertCommand(fact.assertion.toExpr()); - } - - return fact; - } + inline Assertion get(); const LogicInfo& getLogicInfo() const { return d_logicInfo; @@ -348,13 +361,9 @@ public: } /** - * Destructs a Theory. This implementation does nothing, but we - * need a virtual destructor for safety in case subclasses have a - * destructor. + * Destructs a Theory. */ - virtual ~Theory() { - StatisticsRegistry::unregisterStat(&d_computeCareGraphTime); - } + virtual ~Theory(); /** * Subclasses of Theory may add additional efforts. DO NOT CHECK @@ -376,7 +385,11 @@ public: * Combination effort means that the individual theories are already satisfied, and * it is time to put some effort into propagation of shared term equalities */ - EFFORT_COMBINATION = 150 + EFFORT_COMBINATION = 150, + /** + * Last call effort, reserved for quantifiers. + */ + EFFORT_LAST_CALL = 200 };/* enum Effort */ static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION @@ -385,7 +398,7 @@ public: { return e >= EFFORT_STANDARD && e < EFFORT_FULL; } static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION { return e == EFFORT_FULL; } - static inline bool combination(Effort e) CVC4_CONST_FUNCTION + static inline bool combination(Effort e) CVC4_CONST_FUNCTION { return e == EFFORT_COMBINATION; } /** @@ -424,6 +437,41 @@ public: } /** + * Get the valuation associated to this theory. + */ + Valuation& getValuation() { + return d_valuation; + } + + /** + * Get the quantifiers engine associated to this theory. + */ + QuantifiersEngine* getQuantifiersEngine() { + return d_quantEngine; + } + + /** + * Get the quantifiers engine associated to this theory (const version). + */ + const QuantifiersEngine* getQuantifiersEngine() const { + return d_quantEngine; + } + + /** + * Get the theory instantiator. + */ + Instantiator* getInstantiator() { + return d_inst; + } + + /** + * Get the theory instantiator (const version). + */ + const Instantiator* getInstantiator() const { + return d_inst; + } + + /** * Pre-register a term. Done one time for a Node, ever. */ virtual void preRegisterTerm(TNode) { } @@ -455,7 +503,7 @@ public: } /** - * Return the status of two terms in the current context. Should be implemented in + * Return the status of two terms in the current context. Should be implemented in * sub-theories to enable more efficient theory-combination. */ virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } @@ -573,6 +621,11 @@ public: virtual Node ppRewrite(TNode atom) { return atom; } /** + * Don't preprocess subterm of this term + */ + virtual bool ppDontRewriteSubterm(TNode atom) { return false; } + + /** * A Theory is called with presolve exactly one time per user * check-sat. presolve() is called after preregistration, * rewriting, and Boolean propagation, (other theories' @@ -664,7 +717,7 @@ public: static inline Set setIntersection(Set a, Set b) { return a & b; - } + } static inline Set setUnion(Set a, Set b) { return a | b; @@ -735,6 +788,84 @@ public: std::ostream& operator<<(std::ostream& os, Theory::Effort level); +class Instantiator { + friend class QuantifiersEngine; +protected: + /** reference to the quantifiers engine */ + QuantifiersEngine* d_quantEngine; + /** reference to the theory that it looks at */ + Theory* d_th; + /** instantiation strategies */ + std::vector< InstStrategy* > d_instStrategies; + /** instantiation strategies active */ + std::map< InstStrategy*, bool > d_instStrategyActive; + /** has constraints from quantifier */ + std::map< Node, bool > d_hasConstraints; + /** is instantiation strategy active */ + bool isActiveStrategy( InstStrategy* is ) { + return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is]; + } + /** add inst strategy */ + void addInstStrategy( InstStrategy* is ){ + d_instStrategies.push_back( is ); + d_instStrategyActive[is] = true; + } + /** reset instantiation round */ + virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; + /** process quantifier */ + virtual int process( Node f, Theory::Effort effort, int e, int limitInst = 0 ) = 0; +public: + /** set has constraints from quantifier f */ + void setHasConstraintsFrom( Node f ); + /** has constraints from */ + bool hasConstraintsFrom( Node f ); + /** is full owner of quantifier f? */ + bool isOwnerOf( Node f ); +public: + Instantiator(context::Context* c, QuantifiersEngine* qe, Theory* th); + virtual ~Instantiator(); + + /** get quantifiers engine */ + QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } + /** get corresponding theory for this instantiator */ + Theory* getTheory() { return d_th; } + /** Pre-register a term. */ + virtual void preRegisterTerm( Node t ) { } + /** assertNode function, assertion was asserted to theory */ + virtual void assertNode( Node assertion ){} + /** reset instantiation round */ + void resetInstantiationRound( Theory::Effort effort ); + /** do instantiation method*/ + int doInstantiation( Node f, Theory::Effort effort, int e, int limitInst = 0 ); + /** identify */ + virtual std::string identify() const { return std::string("Unknown"); } + /** print debug information */ + virtual void debugPrint( const char* c ) {} + /** get status */ + //int getStatus() { return d_status; } +};/* class Instantiator */ + +inline Assertion Theory::get() { + Assert( !done(), "Theory::get() called with assertion queue empty!" ); + + // Get the assertion + Assertion fact = d_facts[d_factsHead]; + d_factsHead = d_factsHead + 1; + + Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl; + + if(Dump.isOn("state")) { + Dump("state") << AssertCommand(fact.assertion.toExpr()); + } + + // if quantifiers are turned on and we have an instantiator, notify it + if(getLogicInfo().isQuantified() && getInstantiator() != NULL) { + getInstantiator()->assertNode(fact); + } + + return fact; +} + }/* CVC4::theory namespace */ inline std::ostream& operator<<(std::ostream& out, |