more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code

1 files changed, 2 insertions, 231 deletions

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index a0db1336f..426adc02d 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -20,81 +20,19 @@
 #include "util/hash.h"
 
 #include <ext/hash_set>
-#include <iostream>
 #include <map>
 
 #include "context/cdlist.h"
-#include "theory/quantifiers/candidate_generator.h"
-
-//#define USE_EFFICIENT_E_MATCHING
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace theory {
 
-/** Attribute true for nodes that should not be used for matching */
-struct NoMatchAttributeId {};
-/** use the special for boolean flag */
-typedef expr::Attribute< NoMatchAttributeId,
-                         bool,
-                         expr::attr::NullCleanupStrategy,
-                         true // context dependent
-                       > NoMatchAttribute;
-
-// attribute for "contains instantiation constants from"
-struct InstConstantAttributeId {};
-typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
-
-struct InstLevelAttributeId {};
-typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
-
-struct InstVarNumAttributeId {};
-typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
-
-// Attribute that tell if a node have been asserted in this branch
-struct AvailableInTermDbId {};
-/** use the special for boolean flag */
-typedef expr::Attribute<AvailableInTermDbId,
-                        bool,
-                        expr::attr::NullCleanupStrategy,
-                        true  // context dependent
-                        > AvailableInTermDb;
-
-
 class QuantifiersEngine;
-namespace quantifiers{
-  class TermArgTrie;
-}
-
-namespace uf{
-  class InstantiatorTheoryUf;
-  class TheoryUF;
-}/* CVC4::theory::uf namespace */
+class EqualityQuery;
 
 namespace inst {
 
-class EqualityQuery {
-public:
-  EqualityQuery(){}
-  virtual ~EqualityQuery(){};
-  /** contains term */
-  virtual bool hasTerm( Node a ) = 0;
-  /** get the representative of the equivalence class of a */
-  virtual Node getRepresentative( Node a ) = 0;
-  /** returns true if a and b are equal in the current context */
-  virtual bool areEqual( Node a, Node b ) = 0;
-  /** returns true is a and b are disequal in the current context */
-  virtual bool areDisequal( Node a, Node b ) = 0;
-  /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
-      If cbqi is active, this will return a term in the equivalence class of "a" that does
-      not contain instantiation constants, if such a term exists.
-   */
-  virtual Node getInternalRepresentative( Node a ) = 0;
-  /** get the equality engine associated with this query */
-  virtual eq::EqualityEngine* getEngine() = 0;
-  /** get the equivalence class of a */
-  virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
-};/* class EqualityQuery */
-
 /** basic class defining an instantiation */
 class InstMatch {
   /* map from variable to ground terms */
@@ -230,176 +168,9 @@ public:
   }
 };/* class InstMatchTrieOrdered */
 
-/** base class for producing InstMatch objects */
-class IMGenerator {
-public:
-  /** reset instantiation round (call this at beginning of instantiation round) */
-  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
-  /** get the next match.  must call reset( eqc ) before this function. */
-  virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
-  /** return true if whatever Node is substituted for the variables the
-      given Node can't match the pattern */
-  virtual bool nonunifiable( TNode t, const std::vector<Node> & vars) = 0;
-  /** add instantiations directly */
-  virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
-  /** add ground term t, called when t is added to term db */
-  virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;
-};/* class IMGenerator */
-
-
-class InstMatchGenerator : public IMGenerator {
-private:
-  /** candidate generator */
-  CandidateGenerator* d_cg;
-  /** policy to use for matching */
-  int d_matchPolicy;
-  /** children generators */
-  std::vector< InstMatchGenerator* > d_children;
-  std::vector< int > d_children_index;
-  /** partial vector */
-  std::vector< InstMatch > d_partial;
-  /** eq class */
-  Node d_eq_class;
-  /** for arithmetic matching */
-  std::map< Node, Node > d_arith_coeffs;
-  /** initialize pattern */
-  void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe );
-  void initializePattern( Node pat, QuantifiersEngine* qe );
-public:
-  enum {
-    //options for producing matches
-    MATCH_GEN_DEFAULT = 0,
-    MATCH_GEN_EFFICIENT_E_MATCH,   //generate matches via Efficient E-matching for SMT solvers
-    //others (internally used)
-    MATCH_GEN_INTERNAL_ARITHMETIC,
-    MATCH_GEN_INTERNAL_ERROR,
-  };
-private:
-  /** get the next match.  must call d_cg->reset( ... ) before using.
-      only valid for use where !d_match_pattern.isNull().
-  */
-  bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );
-  /** for arithmetic */
-  bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
-public:
-  /** get the match against ground term or formula t.
-      d_match_pattern and t should have the same shape.
-      only valid for use where !d_match_pattern.isNull().
-  */
-  bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );
-
-  /** constructors */
-  InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );
-  InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
-  /** destructor */
-  ~InstMatchGenerator(){}
-  /** The pattern we are producing matches for.
-      If null, this is a multi trigger that is merging matches from d_children.
-  */
-  Node d_pattern;
-  /** match pattern */
-  Node d_match_pattern;
-public:
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  void resetInstantiationRound( QuantifiersEngine* qe );
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  void reset( Node eqc, QuantifiersEngine* qe );
-  /** get the next match.  must call reset( eqc ) before this function. */
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
-  /** return true if whatever Node is substituted for the variables the
-      given Node can't match the pattern */
-  bool nonunifiable( TNode t, const std::vector<Node> & vars);
-  /** add instantiations */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t */
-  int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGenerator */
-
-/** smart multi-trigger implementation */
-class InstMatchGeneratorMulti : public IMGenerator {
-private:
-  /** indexed trie */
-  typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
-  /** process new match */
-  void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
-  /** process new instantiations */
-  void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
-                                 std::vector< IndexedTrie >& unique_var_tries,
-                                 int trieIndex, int childIndex, int endChildIndex, bool modEq );
-  /** process new instantiations 2 */
-  void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
-                                  std::vector< IndexedTrie >& unique_var_tries,
-                                  int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
-private:
-  /** var contains (variable indices) for each pattern node */
-  std::map< Node, std::vector< int > > d_var_contains;
-  /** variable indices contained to pattern nodes */
-  std::map< int, std::vector< Node > > d_var_to_node;
-  /** quantifier to use */
-  Node d_f;
-  /** policy to use for matching */
-  int d_matchPolicy;
-  /** children generators */
-  std::vector< InstMatchGenerator* > d_children;
-  /** inst match tries for each child */
-  std::vector< InstMatchTrieOrdered > d_children_trie;
-  /** calculate matches */
-  void calculateMatches( QuantifiersEngine* qe );
-public:
-  /** constructors */
-  InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
-  /** destructor */
-  ~InstMatchGeneratorMulti(){}
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  void resetInstantiationRound( QuantifiersEngine* qe );
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  void reset( Node eqc, QuantifiersEngine* qe );
-  /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
-  /** return true if whatever Node is substituted for the variables the
-      given Node can't match the pattern */
-  bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
-  /** add instantiations */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t */
-  int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGeneratorMulti */
-
-/** smart (single)-trigger implementation */
-class InstMatchGeneratorSimple : public IMGenerator {
-private:
-  /** quantifier for match term */
-  Node d_f;
-  /** match term */
-  Node d_match_pattern;
-  /** add instantiations */
-  void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
-public:
-  /** constructors */
-  InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){}
-  /** destructor */
-  ~InstMatchGeneratorSimple(){}
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  void resetInstantiationRound( QuantifiersEngine* qe ) {}
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  void reset( Node eqc, QuantifiersEngine* qe ) {}
-  /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
-  /** return true if whatever Node is substituted for the variables the
-      given Node can't match the pattern */
-  bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
-  /** add instantiations */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t, possibly add instantiations */
-  int addTerm( Node f, Node t, QuantifiersEngine* qe );
-};/* class InstMatchGeneratorSimple */
-
 }/* CVC4::theory::inst namespace */
 
 typedef CVC4::theory::inst::InstMatch InstMatch;
-typedef CVC4::theory::inst::EqualityQuery EqualityQuery;
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */