drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine

1 files changed, 0 insertions, 53 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 4d535a8af..1f55a4b90 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -820,40 +820,6 @@ namespace eq{
   class EqualityEngine;
 }
 
-/** instantiation strategy class */
-class InstStrategy {
-public:
-  enum Status {
-    STATUS_UNFINISHED,
-    STATUS_UNKNOWN,
-    STATUS_SAT,
-  };/* enum Status */
-protected:
-  /** reference to the instantiation engine */
-  QuantifiersEngine* d_quantEngine;
-
-
-public:
-  InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
-  virtual ~InstStrategy(){}
-
-  /** reset instantiation */
-  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
-  /** process method, returns a status */
-  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
-  /** update status */
-  static void updateStatus( int& currStatus, int addStatus ){
-    if( addStatus==STATUS_UNFINISHED ){
-      currStatus = STATUS_UNFINISHED;
-    }else if( addStatus==STATUS_UNKNOWN ){
-      if( currStatus==STATUS_SAT ){
-        currStatus = STATUS_UNKNOWN;
-      }
-    }
-  }
-  /** identify */
-  virtual std::string identify() const { return std::string("Unknown"); }
-};/* class InstStrategy */
 
 /** instantiator class */
 class Instantiator {
@@ -863,21 +829,6 @@ protected:
   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_quantActive;
-  /** 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 */
@@ -899,10 +850,6 @@ public:
   /** print debug information */
   virtual void debugPrint( const char* c ) {}
 public:
-  /** set has constraints from quantifier f */
-  void setQuantifierActive( Node f ) { d_quantActive[f] = true; }
-  /** has constraints from */
-  bool getQuantifierActive( Node f ) { return d_quantActive.find(f) != d_quantActive.end() && d_quantActive[f]; }
   /** reset instantiation round */
   void resetInstantiationRound( Theory::Effort effort );
   /** do instantiation method*/