Promote InstStrategyCbqi to quantifier module. Cleanup unused code.

1 files changed, 17 insertions, 9 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index adbb2a5e4..6619860e0 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -33,11 +33,12 @@ namespace arith {
 
 namespace quantifiers {
 
-class InstStrategyCbqi : public InstStrategy {
+class InstStrategyCbqi : public QuantifiersModule {
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 protected:
   bool d_cbqi_set_quant_inactive;
   /** whether we have added cbqi lemma */
-  std::map< Node, bool > d_added_cbqi_lemma;
+  NodeSet d_added_cbqi_lemma;
   /** whether to do cbqi for this quantified formula */
   std::map< Node, bool > d_do_cbqi;  
   /** register ce lemma */
@@ -47,17 +48,24 @@ protected:
   /** helper functions */
   bool hasNonCbqiVariable( Node q );
   bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
+  /** process functions */
+  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
+  virtual void process( Node q, Theory::Effort effort, int e ) = 0;
 public:
   InstStrategyCbqi( QuantifiersEngine * qe );
   ~InstStrategyCbqi() throw() {}
+  /** whether to do CBQI for quantifier q */
+  bool doCbqi( Node q );
   /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
+  bool needsCheck( Theory::Effort e );
+  unsigned needsModel( Theory::Effort e );
+  void reset_round( Theory::Effort e );
+  void check( Theory::Effort e, unsigned quant_e );
+  bool checkComplete();
+  void preRegisterQuantifier( Node q );
+  void registerQuantifier( Node q );
   /** get next decision request */
   Node getNextDecisionRequest();
-  //set quant inactive
-  bool setQuantifierInactive() { return d_cbqi_set_quant_inactive; }
-  /** whether to do CBQI for quantifier q */
-  bool doCbqi( Node q );
 };
 
 
@@ -95,7 +103,7 @@ private:
   Node d_negOne;
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
+  void process( Node f, Theory::Effort effort, int e );
 public:
   InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
   ~InstStrategySimplex() throw() {}
@@ -126,7 +134,7 @@ protected:
   bool d_check_vts_lemma_lc;
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
+  void process( Node f, Theory::Effort effort, int e );
   /** register ce lemma */
   void registerCounterexampleLemma( Node q, Node lem );
 public: