Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module. Refactor QuantifiersEngine registration and check.

1 files changed, 6 insertions, 8 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index eb4470eec..78609914f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -89,6 +89,7 @@ namespace quantifiers {
   class QModelBuilder;
   class ConjectureGenerator;
   class CegInstantiation;
+  class LtePartialInst;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -135,7 +136,7 @@ private:
   /** ceg instantiation */
   quantifiers::CegInstantiation * d_ceg_inst;
   /** lte partial instantiation */
-  QuantLtePartialInst * d_lte_part_inst;
+  quantifiers::LtePartialInst * d_lte_part_inst;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -144,7 +145,7 @@ public: //effort levels
   };
 private:
   /** list of all quantifiers seen */
-  std::vector< Node > d_quants;
+  std::map< Node, bool > d_quants;
   /** list of all lemmas produced */
   //std::map< Node, bool > d_lemmas_produced;
   BoolMap d_lemmas_produced_c;
@@ -217,6 +218,8 @@ public:  //modules
   quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
   /** ceg instantiation */
   quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
+  /** local theory ext partial inst */
+  quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
@@ -233,7 +236,7 @@ public:
   /** check at level */
   void check( Theory::Effort e );
   /** register quantifier */
-  void registerQuantifier( Node f );
+  bool registerQuantifier( Node f );
   /** register quantifier */
   void registerPattern( std::vector<Node> & pattern);
   /** assert universal quantifier */
@@ -283,11 +286,6 @@ public:
   /** set instantiation level attr */
   static void setInstantiationLevelAttr( Node n, uint64_t level );
 public:
-  /** get number of quantifiers */
-  int getNumQuantifiers() { return (int)d_quants.size(); }
-  /** get quantifier */
-  Node getQuantifier( int i ) { return d_quants[i]; }
-public:
   /** get model */
   quantifiers::FirstOrderModel* getModel() { return d_model; }
   /** get term database */