More optimizations of quantifier instantiation data structures.

1 files changed, 25 insertions, 43 deletions

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index eb7f50095..c366c4a09 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -36,16 +36,14 @@ namespace inst {
 
 /** basic class defining an instantiation */
 class InstMatch {
+public:
   /* map from variable to ground terms */
-  std::map< Node, Node > d_map;
+  std::vector< Node > d_vals;
 public:
-  InstMatch();
+  InstMatch(){}
+  InstMatch( Node f );
   InstMatch( InstMatch* m );
 
-  /** set the match of v to m */
-  bool setMatch( EqualityQuery* q, TNode v, TNode m );
-  /* This version tell if the variable has been set */
-  bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & st);
   /** fill all unfilled values with m */
   bool add( InstMatch& m );
   /** if compatible, fill all unfilled values with m and return true
@@ -54,56 +52,36 @@ public:
   /** debug print method */
   void debugPrint( const char* c );
   /** is complete? */
-  bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
+  bool isComplete();
   /** make complete */
   void makeComplete( Node f, QuantifiersEngine* qe );
-  /** make internal representative */
-  //void makeInternalRepresentative( QuantifiersEngine* qe );
   /** make representative */
   void makeRepresentative( QuantifiersEngine* qe );
-  /** get value */
-  Node getValue( Node var ) const;
+  /** empty */
+  bool empty();
   /** clear */
-  void clear(){ d_map.clear(); }
-  /** is_empty */
-  bool empty(){ return d_map.empty(); }
+  void clear();
   /** to stream */
   inline void toStream(std::ostream& out) const {
     out << "INST_MATCH( ";
-    for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){
-      if( it != d_map.begin() ){ out << ", "; }
-      out << it->first << " -> " << it->second;
+    bool printed = false;
+    for( unsigned i=0; i<d_vals.size(); i++ ){
+      if( !d_vals[i].isNull() ){
+        if( printed ){ out << ", "; }
+        out << i << " -> " << d_vals[i];
+        printed = true;
+      }
     }
     out << " )";
   }
-
-
-  //for rewrite rules
-
   /** apply rewrite */
   void applyRewrite();
-  /** erase */
-  template<class Iterator>
-  void erase(Iterator begin, Iterator end){
-    for(Iterator i = begin; i != end; ++i){
-      d_map.erase(*i);
-    };
-  }
-  void erase(Node node){ d_map.erase(node); }
   /** get */
-  Node get( TNode var ) { return d_map[var]; }
-  Node get( QuantifiersEngine* qe, Node f, int i );
+  Node get( int i );
   /** set */
-  void set(TNode var, TNode n);
-  void set( QuantifiersEngine* qe, Node f, int i, TNode n );
-  /** size */
-  size_t size(){ return d_map.size(); }
-  /* iterator */
-  std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
-  std::map< Node, Node >::iterator end(){ return d_map.end(); };
-  std::map< Node, Node >::iterator find(Node var){ return d_map.find(var); };
-  /* Node used for matching the trigger only for mono-trigger (just for
-     efficiency because I need only that) */
+  void setValue( int i, TNode n );
+  bool set( QuantifiersEngine* qe, int i, TNode n );
+  /* Node used for matching the trigger */
   Node d_matched;
 };/* class InstMatch */
 
@@ -143,7 +121,9 @@ public:
       return true if successful
   */
   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                     bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
+                     bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
+    return addInstMatch( qe, f, m.d_vals, modEq, modInst, imtio, onlyExist, index );
+  }
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
                      bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
 };/* class InstMatchTrie */
@@ -176,7 +156,9 @@ public:
       return true if successful
   */
   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
-                     bool modInst = false, int index = 0, bool onlyExist = false );
+                     bool modInst = false, int index = 0, bool onlyExist = false ) {
+    return addInstMatch( qe, f, m.d_vals, c, modEq, modInst, index, onlyExist );
+  }
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
                      bool modInst = false, int index = 0, bool onlyExist = false );
 };/* class CDInstMatchTrie */