From a9f4d3e2aed0c6d8d8b218c5f5d2bc95af2d45a6 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 31 Jul 2014 12:49:28 +0200 Subject: 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). --- src/theory/quantifiers/instantiation_engine.cpp | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) (limited to 'src/theory/quantifiers/instantiation_engine.cpp') 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) ){ -- cgit v1.2.3