Accept user-provided triggers with variable terms. Flush lemmas before quantifiers...

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index c775bb55802bbb9e55581c2de9e9c3167ffc45da..0b8e0e4629d5a70be89e857a5ae7310c530361cb 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -700,7 +700,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
         d_tg_alloc[0].reset( this, TypeNode::null() );\r
         while( d_tg_alloc[0].getNextTerm( this, depth ) ){\r
           Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth );\r
-          if( d_tg_alloc[0].getDepth( this )==depth ){\r
+          //if( d_tg_alloc[0].getDepth( this )==depth ){\r
+          if( (int)d_tg_gdepth==d_tg_gdepth_limit ){\r
             //construct term\r
             Node nn = d_tg_alloc[0].getTerm( this );\r
             if( getUniversalRepresentative( nn )==nn ){\r

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index df7f06aff4387c25f49dd0c224cd238ff1288ea2..ef1997d4c5f086aa5f980d59c0cd8775f1f5838c 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -68,12 +68,12 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
     for( int i=0; i<(int)d_user_gen[f].size(); i++ ){
       bool processTrigger = true;
       if( processTrigger ){
-        //if( d_user_gen[f][i]->isMultiTrigger() )
-          Trace("process-trigger") << "  Process (user) " << (*d_user_gen[f][i]) << "..." << std::endl;
+        Trace("process-trigger") << "  Process (user) ";
+        d_user_gen[f][i]->debugPrint("process-trigger");
+        Trace("process-trigger") << "..." << std::endl;
         InstMatch baseMatch( f );
         int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
-        //if( d_user_gen[f][i]->isMultiTrigger() )
-          Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
+        Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
         d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;
         if( d_user_gen[f][i]->isMultiTrigger() ){
           d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
@@ -89,17 +89,22 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
 
 void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
   //add to generators
+  bool usable = true;
   std::vector< Node > nodes;
   for( int i=0; i<(int)pat.getNumChildren(); i++ ){
     nodes.push_back( pat[i] );
+    if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], f ) ){
+      Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl;
+      usable = false;
+      break;
+    }
   }
-  if( Trigger::isUsableTrigger( nodes, f ) ){
+  if( usable ){
     //extend to literal matching
     d_quantEngine->getPhaseReqTerms( f, nodes );
     //check match option
     int matchOption = 0;
-    d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,
-                                                 options::smartTriggers() ) );
+    d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) );
   }
 }
 
@@ -156,14 +161,12 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
           bool processTrigger = itt->second;
           if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){
             d_processed_trigger[f][tr] = true;
-            //if( tr->isMultiTrigger() )
-              Trace("process-trigger") << "  Process ";
-              tr->debugPrint("process-trigger");
-              Trace("process-trigger") << "..." << std::endl;
+            Trace("process-trigger") << "  Process ";
+            tr->debugPrint("process-trigger");
+            Trace("process-trigger") << "..." << std::endl;
             InstMatch baseMatch( f );
             int numInst = tr->addInstantiations( baseMatch );
-            //if( tr->isMultiTrigger() )
-              Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
+            Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
             if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
               d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;
             }else{

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 4a99852d102bc9428ce4ef5033057df8d6dc652e..11ec0210d5ab334b6880e92b72661fd17ae751ce 100644 (file)
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -210,15 +210,6 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOpt
   return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );
 }
 
-bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
-  for( int i=0; i<(int)nodes.size(); i++ ){
-    if( !isUsableTrigger( nodes[i], f ) ){
-      return false;
-    }
-  }
-  return true;
-}
-
 bool Trigger::isUsable( Node n, Node f ){
   if( quantifiers::TermDb::getInstConstAttr(n)==f ){
     if( isAtomicTrigger( n ) ){
@@ -234,7 +225,7 @@ bool Trigger::isUsable( Node n, Node f ){
       std::map< Node, Node > coeffs;
       if( isBooleanTermTrigger( n ) ){
         return true;
-      }    
+      }
     }
     return false;
   }else{

diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 1a3ae3fcd8d0c0268a81c545fe5e367d062ae0b8..74a87591f9aea29c6107098f0080e75975124ac5 100644 (file)
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -105,7 +105,6 @@ public:
   static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst = false );
 public:
   /** is usable trigger */
-  static bool isUsableTrigger( std::vector< Node >& nodes, Node f );
   static bool isUsableTrigger( Node n, Node f );
   static bool isAtomicTrigger( Node n );
   static bool isAtomicTriggerKind( Kind k );

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a00592e8b9e17e3ef67afdbc50aec835432c6a6e..4c29c8f9ab7283a33c1174d1325e0c2cf1ce297a 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -195,6 +195,13 @@ void QuantifiersEngine::check( Theory::Effort e ){
     //reset relevant information
     d_conflict = false;
     d_hasAddedLemma = false;
+
+    //flush previous lemmas (for instance, if was interupted)
+    flushLemmas();
+    if( d_hasAddedLemma ){
+      return;
+    }
+
     d_term_db->reset( e );
     d_eq_query->reset();
     if( d_rel_dom ){