summaryrefslogtreecommitdiff
path: root/src/theory/theory.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r--src/theory/theory.h185
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback