made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486

4 files changed, 124 insertions, 2 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 1a48ec161..dcd7a1b79 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -217,6 +217,88 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, b
 }
 
 
+
+/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
+void CDInstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio ){
+  if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
+    int i_index = imtio ? imtio->d_order[index] : index;
+    Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
+    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+    if( it!=d_data.end() ){
+      it->second->addInstMatch2( qe, f, m, c, index+1, imtio );
+    }else{
+      CDInstMatchTrie* imt = new CDInstMatchTrie( c );
+      d_data[n] = imt;
+      imt->d_valid = true;
+      imt->addInstMatch2( qe, f, m, c, index+1, imtio );
+    }
+  }
+}
+
+/** exists match */
+bool CDInstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){
+  if( !d_valid ){
+    return false;
+  }else if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
+    return true;
+  }else{
+    int i_index = imtio ? imtio->d_order[index] : index;
+    Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
+    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+    if( it!=d_data.end() ){
+      if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
+        return true;
+      }
+    }
+    //check if m is an instance of another instantiation if modInst is true
+    if( modInst ){
+      if( !n.isNull() ){
+        Node nl;
+        it = d_data.find( nl );
+        if( it!=d_data.end() ){
+          if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
+            return true;
+          }
+        }
+      }
+    }
+    if( modEq ){
+      //check modulo equality if any other instantiation match exists
+      if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+        eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
+                                 qe->getEqualityQuery()->getEngine() );
+        while( !eqc.isFinished() ){
+          Node en = (*eqc);
+          if( en!=n ){
+            std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
+            if( itc!=d_data.end() ){
+              if( itc->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
+                return true;
+              }
+            }
+          }
+          ++eqc;
+        }
+      }
+    }
+    return false;
+  }
+}
+
+bool CDInstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
+  return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio );
+}
+
+bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, Context* c, bool modEq, bool modInst, ImtIndexOrder* imtio ){
+  if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){
+    addInstMatch2( qe, f, m, c, 0, imtio );
+    return true;
+  }else{
+    return false;
+  }
+}
+
+
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index c8f843c90..8b2d9726b 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -18,6 +18,7 @@
 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
 
 #include "util/hash.h"
+#include "context/cdo.h"
 
 #include <ext/hash_set>
 #include <map>
@@ -141,6 +142,42 @@ public:
                      bool modInst = false, ImtIndexOrder* imtio = NULL );
 };/* class InstMatchTrie */
 
+
+/** trie for InstMatch objects */
+class CDInstMatchTrie {
+public:
+  class ImtIndexOrder {
+  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, context::Context* c, 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, 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, bool modEq = false,
+                        bool modInst = false, ImtIndexOrder* imtio = NULL );
+  /** 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, ImtIndexOrder* imtio = NULL );
+};/* class CDInstMatchTrie */
+
 class InstMatchTrieOrdered{
 private:
   InstMatchTrie::ImtIndexOrder* d_imtio;
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 653016d1c..53977ee4f 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -48,8 +48,8 @@ void InstantiationEngine::finishInit(){
     }else{
       d_isup = NULL;
     }
-    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL,
-                                                                         InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 );
+    int rlv = options::relevantTriggers() ? InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT : InstStrategyAutoGenTriggers::RELEVANCE_NONE;
+    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, rlv, 3 );
     i_ag->setGenerateAdditional( true );
     addInstStrategy( i_ag );
     //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 24d0c4047..bc45e6051 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -44,6 +44,9 @@ option macrosQuant --macros-quant bool :default false
 # Whether to use smart triggers
 option smartTriggers /--disable-smart-triggers bool :default true
  disable smart triggers
+# Whether to use relevent triggers
+option relevantTriggers /--relevant-triggers bool :default true
+ prefer triggers that are more relevant based on SInE style method
 
 # Whether to consider terms in the bodies of quantifiers for matching
 option registerQuantBodyTerms --register-quant-body-terms bool :default false