(Refactor) Instantiate utility (#1387)

1 files changed, 30 insertions, 75 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 37691488e..6c7820cef 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -40,18 +40,6 @@ namespace theory {
 
 class QuantifiersEngine;
 
-class InstantiationNotify {
-public:
-  InstantiationNotify(){}
-  virtual ~InstantiationNotify() {}
-  virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
-                                   Node q,
-                                   Node lem,
-                                   std::vector<Node>& terms,
-                                   Node body) = 0;
-  virtual void filterInstantiations() = 0;
-};
-
 namespace quantifiers {
   //TODO: organize this more/review this, github issue #1163
   //TODO: include these instead of doing forward declarations? #1307
@@ -59,6 +47,7 @@ namespace quantifiers {
   class TermDb;
   class TermDbSygus;
   class TermUtil;
+  class Instantiate;
   class Skolemize;
   class TermEnumeration;
   class FirstOrderModel;
@@ -97,6 +86,7 @@ namespace inst {
 
 
 class QuantifiersEngine {
+  // TODO: remove these github issue #1163
   friend class quantifiers::InstantiationEngine;
   friend class quantifiers::InstStrategyCbqi;
   friend class quantifiers::InstStrategyCegqi;
@@ -115,8 +105,6 @@ private:
   std::vector< QuantifiersUtil* > d_util;
   /** vector of modules for quantifiers */
   std::vector< QuantifiersModule* > d_modules;
-  /** instantiation notify */
-  std::vector< InstantiationNotify* > d_inst_notify;
   /** equality query class */
   quantifiers::EqualityQueryQuantifiersEngine* d_eq_query;
   /** equality inference class */
@@ -141,6 +129,8 @@ private:
   quantifiers::TermUtil* d_term_util;
   /** quantifiers attributes */
   std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
+  /** instantiate utility */
+  std::unique_ptr<quantifiers::Instantiate> d_instantiate;
   /** skolemize utility */
   std::unique_ptr<quantifiers::Skolemize> d_skolemize;
   /** term enumeration utility */
@@ -199,19 +189,10 @@ private:
   std::vector< Node > d_lemmas_waiting;
   /** phase requirements waiting */
   std::map< Node, bool > d_phase_req_waiting;
-  /** list of all instantiations produced for each quantifier */
-  std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
-  std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
-  /** recorded instantiations */
-  std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst;
   /** all triggers will be stored in this trie */
   inst::TriggerTrie* d_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
-  /** statistics for debugging */
-  std::map< Node, int > d_total_inst_debug;
-  std::map< Node, int > d_temp_inst_debug;
-  int d_total_inst_count_debug;
   /** inst round counters TODO: make context-dependent? */
   context::CDO< int > d_ierCounter_c;
   int d_ierCounter;
@@ -319,37 +300,15 @@ public:
 private:
   /** reduceQuantifier, return true if reduced */
   bool reduceQuantifier( Node q );
-  /** compute term vector */
-  void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
-  /** record instantiation, return true if it was non-duplicate */
-  bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool addedLem = true );
-  /** remove instantiation */
-  bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
-  /** set instantiation level attr */
-  static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
   /** flush lemmas */
   void flushLemmas();
 public:
-  /** get instantiation */
-  Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
-  /** get instantiation */
-  Node getInstantiation( Node q, InstMatch& m, bool doVts = false );
-  /** get instantiation */
-  Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false );
-  /** do substitution */
-  Node getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited );
   /** add lemma lem */
   bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
   /** remove pending lemma */
   bool removeLemma( Node lem );
   /** add require phase */
   void addRequirePhase( Node lit, bool req );
-  /** do instantiation specified by m */
-  bool addInstantiation( Node q, InstMatch& m, bool mkRep = false, bool modEq = false, bool doVts = false );
-  /** add instantiation */
-  bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = false, bool modEq = false, bool doVts = false );
-  /** remove pending instantiation */
-  bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms );
   /** split on node n */
   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
   /** add split equality */
@@ -364,14 +323,14 @@ public:
   bool inConflict() { return d_conflict; }
   /** set conflict */
   void setConflict();
+  /** get current q effort */
+  QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
   /** get number of waiting lemmas */
   unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
   /** get needs check */
   bool getInstWhenNeedsCheck( Theory::Effort e );
   /** get user pat mode */
   quantifiers::UserPatMode getInstUserPatMode();
-  /** set instantiation level attr */
-  static void setInstantiationLevelAttr( Node n, uint64_t level );
 public:
   /** get model */
   quantifiers::FirstOrderModel* getModel() { return d_model; }
@@ -385,6 +344,8 @@ public:
   quantifiers::QuantAttributes* getQuantAttributes() {
     return d_quant_attr.get();
   }
+  /** get instantiate utility */
+  quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); }
   /** get skolemize utility */
   quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); }
   /** get term enumeration utility */
@@ -405,42 +366,41 @@ public:
   eq::EqualityEngine* getMasterEqualityEngine();
   /** get the active equality engine */
   eq::EqualityEngine* getActiveEqualityEngine();
+  /** use model equality engine */
+  bool usingModelEqualityEngine() const { return d_useModelEe; }
   /** debug print equality engine */
   void debugPrintEqualityEngine( const char * c );
   /** get internal representative */
   Node getInternalRepresentative( Node a, Node q, int index );
-  /** get term for type
-   *
-   * This returns an arbitrary term for type tn.
-   * This term is chosen heuristically to be the best
-   * term for instantiation. Currently, this
-   * heuristic enumerates the first term of the
-   * type if the type is closed enumerable, otherwise
-   * an existing ground term from the term database if
-   * one exists, or otherwise a fresh variable.
-   */
-  Node getTermForType(TypeNode tn);
 
  public:
+  //----------user interface for instantiations (see quantifiers/instantiate.h)
   /** print instantiations */
-  void printInstantiations( std::ostream& out );
+  void printInstantiations(std::ostream& out);
   /** print solution for synthesis conjectures */
-  void printSynthSolution( std::ostream& out );
+  void printSynthSolution(std::ostream& out);
   /** get list of quantified formulas that were instantiated */
-  void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
+  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
   /** get instantiations */
-  void getInstantiations( Node q, std::vector< Node >& insts );
-  void getInstantiations( std::map< Node, std::vector< Node > >& insts );
+  void getInstantiations(Node q, std::vector<Node>& insts);
+  void getInstantiations(std::map<Node, std::vector<Node> >& insts);
   /** get instantiation term vectors */
-  void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
-  void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
+  void getInstantiationTermVectors(Node q,
+                                   std::vector<std::vector<Node> >& tvecs);
+  void getInstantiationTermVectors(
+      std::map<Node, std::vector<std::vector<Node> > >& insts);
   /** get instantiated conjunction */
-  Node getInstantiatedConjunction( Node q );
+  Node getInstantiatedConjunction(Node q);
   /** get unsat core lemmas */
-  bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas );
-  bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp );
-  /** get inst for lemmas */
-  void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ); 
+  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
+  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
+                          std::map<Node, Node>& weak_imp);
+  /** get explanation for instantiation lemmas */
+  void getExplanationForInstLemmas(const std::vector<Node>& lems,
+                                   std::map<Node, Node>& quant,
+                                   std::map<Node, std::vector<Node> >& tvec);
+  //----------end user interface for instantiations
+
   /** statistics class */
   class Statistics {
   public:
@@ -450,11 +410,6 @@ public:
     IntStat d_num_quant;
     IntStat d_instantiation_rounds;
     IntStat d_instantiation_rounds_lc;
-    IntStat d_instantiations;
-    IntStat d_inst_duplicate;
-    IntStat d_inst_duplicate_eq;
-    IntStat d_inst_duplicate_ent;
-    IntStat d_inst_duplicate_model_true;
     IntStat d_triggers;
     IntStat d_simple_triggers;
     IntStat d_multi_triggers;