diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-12-01 15:13:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-12-01 15:13:58 +0000 |
commit | e820acb9e220389e9a7e23bcffd97f1d0354f612 (patch) | |
tree | 2c968d847c87ec363cf6add1ac3cf8cfbf4902a1 /src/theory/theory.h | |
parent | ec29471e427bf25034a93c182b424730d439a90a (diff) |
remove instantiator framework
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 82 |
1 files changed, 0 insertions, 82 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 1f55a4b90..f317d4b92 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -46,7 +46,6 @@ class TheoryEngine; namespace theory { -class Instantiator; class QuantifiersEngine; class TheoryModel; @@ -192,12 +191,6 @@ private: */ 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; @@ -208,12 +201,6 @@ 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: /** @@ -261,7 +248,6 @@ protected: , 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) @@ -487,20 +473,6 @@ public: } /** - * 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) { } @@ -821,55 +793,6 @@ namespace eq{ } -/** instantiator class */ -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; - /** reset instantiation round */ - virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; - /** process quantifier */ - virtual int process( Node f, Theory::Effort effort, int e ) = 0; -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 ){} - /** identify */ - virtual std::string identify() const { return std::string("Unknown"); } - /** print debug information */ - virtual void debugPrint( const char* c ) {} -public: - /** reset instantiation round */ - void resetInstantiationRound( Theory::Effort effort ); - /** do instantiation method*/ - int doInstantiation( Node f, Theory::Effort effort, int e ); -public: - /** general queries about equality */ - virtual bool hasTerm( Node a ) { return false; } - virtual bool areEqual( Node a, Node b ) { return false; } - virtual bool areDisequal( Node a, Node b ) { return false; } - virtual Node getRepresentative( Node a ) { return a; } - virtual eq::EqualityEngine* getEqualityEngine() { return NULL; } - virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) {} -public: - /** A Creator of CandidateGenerator for classes (one element in each - equivalence class) and class (every element of one equivalence - class) */ - virtual rrinst::CandidateGenerator* getRRCanGenClasses(){ return NULL; }; - virtual rrinst::CandidateGenerator* getRRCanGenClass(){ return NULL; }; -};/* class Instantiator */ - inline Assertion Theory::get() { Assert( !done(), "Theory::get() called with assertion queue empty!" ); @@ -883,11 +806,6 @@ inline Assertion Theory::get() { 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; } |