New module for generating candidate equality conjectures used in inductive proofs. Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness. Refactoring of term database. QcfEngine now uses central data structure for term indexing. Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check).

1 files changed, 11 insertions, 3 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 3dd4423de..2167c7c7d 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -53,7 +53,13 @@ void InstantiationEngine::finishInit(){
     }else{
       d_isup = NULL;
     }
-    d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, 3 );
+    int tstrt = Trigger::TS_ALL;
+    if( options::triggerSelMode()==TRIGGER_SEL_MIN ){
+      tstrt = Trigger::TS_MIN_TRIGGER;
+    }else if( options::triggerSelMode()==TRIGGER_SEL_MAX ){
+      tstrt = Trigger::TS_MAX_TRIGGER;
+    }
+    d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, tstrt, 3 );
     d_i_ag->setGenerateAdditional( true );
     addInstStrategy( d_i_ag );
     //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
@@ -214,9 +220,12 @@ void InstantiationEngine::check( Theory::Effort e ){
                          << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      //it is not active if we have found the skolemized negation is unsat
+      //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
       if( TermDb::isRewriteRule( n ) ){
         d_quant_active[n] = false;
+      }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){
+        d_quant_active[n] = false;
+      //it is not active if we have found the skolemized negation is unsat
       }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){
         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n );
         bool active, value;
@@ -248,7 +257,6 @@ void InstantiationEngine::check( Theory::Effort e ){
           Debug("quantifiers") << ", ce is asserted";
         }
         Debug("quantifiers") << std::endl;
-      //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
       }else{
         d_quant_active[n] = true;
         if( !TermDb::hasInstConstAttr(n) ){