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

7 files changed, 151 insertions, 11 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
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c04920ab8..08bdd496b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -35,9 +35,10 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
-QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te):
+QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
 d_te( te ),
-d_quant_rel( false ){ //currently do not care about relevance
+d_quant_rel( false ),
+d_lemmas_produced_c(u){
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( this );
   d_tr_trie = new inst::TriggerTrie;
@@ -92,6 +93,10 @@ context::Context* QuantifiersEngine::getSatContext(){
   return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
 }
 
+context::Context* QuantifiersEngine::getUserContext(){
+  return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
+}
+
 OutputChannel& QuantifiersEngine::getOutputChannel(){
   return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
 }
@@ -309,7 +314,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
 
 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
   if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
-    if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
+    if( d_inst_match_trie[f]->existsInstMatch( this, f, m, modEq, modInst ) ){
       return true;
     }
   }
@@ -323,9 +328,9 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
 bool QuantifiersEngine::addLemma( Node lem ){
   Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
   lem = Rewriter::rewrite(lem);
-  if( d_lemmas_produced.find( lem )==d_lemmas_produced.end() ){
+  if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
     //d_curr_out->lemma( lem );
-    d_lemmas_produced[ lem ] = true;
+    d_lemmas_produced_c[ lem ] = true;
     d_lemmas_waiting.push_back( lem );
     Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
     return true;
@@ -355,11 +360,21 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool
     }
   }
   //check for duplication modulo equality
-  if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){
+  inst::CDInstMatchTrie* imt;
+  std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_inst_match_trie.find( f );
+  if( it!=d_inst_match_trie.end() ){
+    imt = it->second;
+  }else{
+    imt = new CDInstMatchTrie( getUserContext() );
+    d_inst_match_trie[f] = imt;
+  }
+  Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+  if( !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
     Trace("inst-add-debug") << " -> Already exists." << std::endl;
     ++(d_statistics.d_inst_duplicate);
     return false;
   }
+  Trace("inst-add-debug") << "compute terms" << std::endl;
   //compute the vector of terms for the instantiation
   std::vector< Node > terms;
   for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 8169c78fb..29381a309 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -104,12 +104,13 @@ private:
   std::vector< Node > d_quants;
   /** list of all lemmas produced */
   std::map< Node, bool > d_lemmas_produced;
+  BoolMap d_lemmas_produced_c;
   /** lemmas waiting */
   std::vector< Node > d_lemmas_waiting;
   /** has added lemma this round */
   bool d_hasAddedLemma;
   /** list of all instantiations produced for each quantifier */
-  std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
+  std::map< Node, inst::CDInstMatchTrie* > d_inst_match_trie;
   /** term database */
   quantifiers::TermDb* d_term_db;
   /** all triggers will be stored in this trie */
@@ -121,7 +122,7 @@ private:
 private:
   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
 public:
-  QuantifiersEngine(context::Context* c, TheoryEngine* te);
+  QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
   ~QuantifiersEngine();
   /** get instantiator for id */
   //Instantiator* getInstantiator( theory::TheoryId id );
@@ -136,6 +137,8 @@ public:
   quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
   /** get default sat context for quantifiers engine */
   context::Context* getSatContext();
+  /** get default sat context for quantifiers engine */
+  context::Context* getUserContext();
   /** get default output channel for the quantifiers engine */
   OutputChannel& getOutputChannel();
   /** get default valuation for the quantifiers engine */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a23480eeb..35ed63bed 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -127,7 +127,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   }
 
   // initialize the quantifiers engine
-  d_quantEngine = new QuantifiersEngine(context, this);
+  d_quantEngine = new QuantifiersEngine(context, userContext, this);
 
   // build model information if applicable
   d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);