more cleanup of quantifiers code

1 files changed, 16 insertions, 119 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d0c5832ff..62e5d983e 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -21,6 +21,7 @@
 #include "util/hash.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/rewriterules/rr_inst_match.h"
+#include "theory/quantifiers/quant_util.h"
 
 #include "util/statistics_registry.h"
 
@@ -36,57 +37,6 @@ namespace theory {
 
 class QuantifiersEngine;
 
-class InstStrategy {
-public:
-  enum Status {
-    STATUS_UNFINISHED,
-    STATUS_UNKNOWN,
-    STATUS_SAT,
-  };/* enum Status */
-protected:
-  /** reference to the instantiation engine */
-  QuantifiersEngine* d_quantEngine;
-protected:
-  /** giving priorities */
-  std::vector< InstStrategy* > d_priority_over;
-  /** do not instantiate list */
-  std::vector< Node > d_no_instantiate;
-  std::vector< Node > d_no_instantiate_temp;
-  /** reset instantiation */
-  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
-  /** process method */
-  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
-public:
-  InstStrategy( QuantifiersEngine* ie ) : d_quantEngine( ie ){}
-  virtual ~InstStrategy(){}
-
-  /** reset instantiation */
-  void resetInstantiationRound( Theory::Effort effort );
-  /** do instantiation round method */
-  int doInstantiation( Node f, Theory::Effort effort, int e );
-  /** 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"); }
-public:
-  /** set priority */
-  void setPriorityOver( InstStrategy* is ) { d_priority_over.push_back( is ); }
-  /** set no instantiate */
-  void setNoInstantiate( Node n ) { d_no_instantiate.push_back( n ); }
-  /** should instantiate */
-  bool shouldInstantiate( Node n ) {
-    return std::find( d_no_instantiate_temp.begin(), d_no_instantiate_temp.end(), n )==d_no_instantiate_temp.end();
-  }
-};/* class InstStrategy */
-
 class QuantifiersModule {
 protected:
   QuantifiersEngine* d_quantEngine;
@@ -129,13 +79,13 @@ private:
   quantifiers::ModelEngine* d_model_engine;
   /** equality query class */
   EqualityQuery* d_eq_query;
-public:
+  /** for computing relevance of quantifiers */
+  QuantRelevance d_quant_rel;
+  /** phase requirements for each quantifier for each instantiation literal */
+  std::map< Node, QuantPhaseReq* > d_phase_reqs;
+private:
   /** list of all quantifiers (pre-rewrite) */
   std::vector< Node > d_quants;
-  /** list of all quantifiers (post-rewrite) */
-  std::vector< Node > d_r_quants;
-  /** map from quantifiers to whether they are active */
-  BoolMap d_active;
   /** lemmas produced */
   std::map< Node, bool > d_lemmas_produced;
   /** lemmas waiting */
@@ -150,30 +100,8 @@ public:
   quantifiers::TermDb* d_term_db;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
-  /** has the model been set? */
-  bool d_model_set;
-  /** has resetInstantiationRound() been called on this check(...) */
-  bool d_resetInstRound;
-  /** universal quantifiers that have been rewritten */
-  std::map< Node, std::vector< Node > > d_quant_rewritten;
-  /** map from rewritten universal quantifiers to the quantifier they are the consequence of */
-  std::map< Node, Node > d_rewritten_quant;
 private:
-  /** for computing relavance */
-  /** map from quantifiers to symbols they contain */
-  std::map< Node, std::vector< Node > > d_syms;
-  /** map from symbols to quantifiers */
-  std::map< Node, std::vector< Node > > d_syms_quants;
-  /** relevance for quantifiers and symbols */
-  std::map< Node, int > d_relevance;
-  /** compute symbols */
-  void computeSymbols( Node n, std::vector< Node >& syms );
-private:
-  /** helper functions compute phase requirements */
-  static void computePhaseReqs2( Node n, bool polarity, std::map< Node, int >& phaseReqs );
-
   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
-
 public:
   QuantifiersEngine(context::Context* c, TheoryEngine* te);
   ~QuantifiersEngine();
@@ -184,9 +112,7 @@ public:
   /** get equality query object for the given type. The default is the
       generic one */
   inst::EqualityQuery* getEqualityQuery(TypeNode t);
-  inst::EqualityQuery* getEqualityQuery() {
-    return d_eq_query;
-  }
+  inst::EqualityQuery* getEqualityQuery() { return d_eq_query; }
   /** get equality query object for the given type. The default is the
       one of UF */
   rrinst::CandidateGenerator* getRRCanGenClasses(TypeNode t);
@@ -204,14 +130,20 @@ public:
   OutputChannel& getOutputChannel();
   /** get default valuation for the quantifiers engine */
   Valuation& getValuation();
+  /** get quantifier relevance */
+  QuantRelevance* getQuantifierRelevance() { return &d_quant_rel; }
+  /** get phase requirement information */
+  QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
+  /** get phase requirement terms */
+  void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
 public:
   /** check at level */
   void check( Theory::Effort e );
-  /** register (non-rewritten) quantifier */
+  /** register quantifier */
   void registerQuantifier( Node f );
-  /** register (non-rewritten) quantifier */
+  /** register quantifier */
   void registerPattern( std::vector<Node> & pattern);
-  /** assert (universal) quantifier */
+  /** assert universal quantifier */
   void assertNode( Node f );
   /** propagate */
   void propagate( Theory::Effort level );
@@ -253,33 +185,6 @@ public:
   int getNumQuantifiers() { return (int)d_quants.size(); }
   /** get quantifier */
   Node getQuantifier( int i ) { return d_quants[i]; }
-  /** set active */
-  void setActive( Node n, bool val ) { d_active[n] = val; }
-  /** get active */
-  bool getActive( Node n ) { return d_active.find( n )!=d_active.end() && d_active[n]; }
-public:
-  /** phase requirements for each quantifier for each instantiation literal */
-  std::map< Node, std::map< Node, bool > > d_phase_reqs;
-  std::map< Node, std::map< Node, bool > > d_phase_reqs_equality;
-  std::map< Node, std::map< Node, Node > > d_phase_reqs_equality_term;
-public:
-  /** is phase required */
-  bool isPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )!=d_phase_reqs[f].end(); }
-  /** get phase requirement */
-  bool getPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )==d_phase_reqs[f].end() ? false : d_phase_reqs[f][ lit ]; }
-  /** get term req terms */
-  void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
-  /** helper functions compute phase requirements */
-  static void computePhaseReqs( Node n, bool polarity, std::map< Node, bool >& phaseReqs );
-  /** compute phase requirements */
-  void generatePhaseReqs( Node f, Node n );
-public:
-  /** has owner */
-  bool hasOwner( Node f ) { return d_owner.find( f )!=d_owner.end(); }
-  /** get owner */
-  Theory* getOwner( Node f ) { return d_owner[f]; }
-  /** set owner */
-  void setOwner( Node f, Theory* t ) { d_owner[f] = t; }
 public:
   /** get model */
   quantifiers::FirstOrderModel* getModel() { return d_model; }
@@ -287,14 +192,6 @@ public:
   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
   /** add term to database */
   void addTermToDatabase( Node n, bool withinQuant = false );
-private:
-  /** set relevance */
-  void setRelevance( Node s, int r );
-public:
-  /** get relevance */
-  int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; }
-  /** get number of quantifiers for symbol s */
-  int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); }
 public:
   /** statistics class */
   class Statistics {