More optimization of QCF. Fixed InstMatchTrie for caching instantiations. Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.

1 files changed, 40 insertions, 7 deletions

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 72447fd66..2cf33bc8e 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -119,11 +119,6 @@ public:
   public:
     std::vector< int > d_order;
   };/* class InstMatchTrie ImtIndexOrder */
-private:
-  /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
-  void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio );
-  /** exists match */
-  bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
 public:
   /** the data */
   std::map< Node, InstMatchTrie > d_data;
@@ -136,16 +131,20 @@ public:
         modInst is if we return true if m is an instance of a match that exists
    */
   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                        bool modInst = false, ImtIndexOrder* imtio = NULL );
+                        bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
+    return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
+  }
   /** add match m for quantifier f, take into account equalities if modEq = true,
       if imtio is non-null, this is the order to add to trie
       return true if successful
   */
   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                     bool modInst = false, ImtIndexOrder* imtio = NULL );
+                     bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
 };/* class InstMatchTrie */
 
 
+#if 0
+
 /** trie for InstMatch objects */
 class CDInstMatchTrie {
 public:
@@ -181,6 +180,37 @@ public:
                      bool modInst = false, ImtIndexOrder* imtio = NULL );
 };/* class CDInstMatchTrie */
 
+#else
+
+
+/** trie for InstMatch objects */
+class CDInstMatchTrie {
+public:
+  /** the data */
+  std::map< Node, CDInstMatchTrie* > d_data;
+  /** is valid */
+  context::CDO< bool > d_valid;
+public:
+  CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
+  ~CDInstMatchTrie(){}
+public:
+  /** return true if m exists in this trie
+        modEq is if we check modulo equality
+        modInst is if we return true if m is an instance of a match that exists
+   */
+  bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
+                        bool modInst = false, int index = 0 ) {
+    return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
+  }
+  /** add match m for quantifier f, take into account equalities if modEq = true,
+      if imtio is non-null, this is the order to add to trie
+      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 );
+};/* class CDInstMatchTrie */
+
+
 class InstMatchTrieOrdered{
 private:
   InstMatchTrie::ImtIndexOrder* d_imtio;
@@ -202,6 +232,9 @@ public:
   }
 };/* class InstMatchTrieOrdered */
 
+#endif
+
+
 }/* CVC4::theory::inst namespace */
 
 typedef CVC4::theory::inst::InstMatch InstMatch;