From: ajreynol Date: Thu, 25 Aug 2016 18:50:45 +0000 (-0500) Subject: Options for counterexample guided instantiation. X-Git-Tag: cvc5-1.0.0~6028^2~77 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dce53c4de6dd7482d9784388cc61753352f241d8;p=cvc5.git Options for counterexample guided instantiation. --- diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 85355c037..cb4f292c1 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -301,6 +301,10 @@ option cbqiMidpoint --cbqi-midpoint bool :default false choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation option cbqiNopt --cbqi-nopt bool :default true non-optimal bounds for counterexample-based quantifier instantiation +option cbqiLitDepend --cbqi-lit-dep bool :default false + dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation +option cbqiInnermost --cbqi-innermost bool :default false + only process innermost quantified formulas in counterexample-based quantifier instantiation ### local theory extensions options diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 0fe4b98c7..e4d12904e 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -504,7 +504,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: } if( options::cbqiModel() ){ if( pvtn.isInteger() || pvtn.isReal() ){ - bool use_inf = d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ) && !options::cbqiMidpoint(); + bool use_inf = d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); bool upper_first = false; if( options::cbqiMinBounds() ){ upper_first = mbp_bounds[1].size()getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); @@ -80,9 +81,34 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { lem = Rewriter::rewrite( lem ); Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; registerCounterexampleLemma( q, lem ); + + //compute dependencies between quantified formulas + if( options::cbqiLitDepend() || options::cbqiInnermost() ){ + std::vector< Node > ics; + TermDb::computeVarContains( q, ics ); + d_parent_quant[q].clear(); + d_children_quant[q].clear(); + std::vector< Node > dep; + for( unsigned i=0; igetTermDatabase()->getCounterexampleLiteral( qi ); + dep.push_back( qi ); + dep.push_back( qicel ); + } + } + if( !dep.empty() ){ + Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) ); + Trace("cbqi") << "Counterexample dependency lemma : " << dep_lemma << std::endl; + d_quantEngine->getOutputChannel().lemma( dep_lemma ); + } + } } //set inactive the quantified formulas whose CE literals are asserted false }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ + d_active_quant[q] = true; Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); bool value; @@ -94,6 +120,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { }else{ d_quantEngine->getModel()->setQuantifierActive( q, false ); d_cbqi_set_quant_inactive = true; + d_active_quant.erase( q ); } } }else{ @@ -102,6 +129,34 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { } } } + + //refinement: only consider innermost active quantified formulas + if( options::cbqiInnermost() ){ + if( !d_children_quant.empty() && !d_active_quant.empty() ){ + Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl; + std::vector< Node > ninner; + for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ + std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first ); + if( itc!=d_children_quant.end() ){ + for( unsigned j=0; jsecond.size(); j++ ){ + if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){ + Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl; + ninner.push_back( it->first ); + break; + } + } + } + } + Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl; + for( unsigned i=0; igetNumLemmasWaiting(); for( int ee=0; ee<=1; ee++ ){ - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ - process( q, e, ee ); - if( d_quantEngine->inConflict() ){ - break; - } + //for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + // if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ + Node q = it->first; + process( q, e, ee ); + if( d_quantEngine->inConflict() ){ + break; } } if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 8ed59778b..20d872c36 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -39,6 +39,10 @@ protected: bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; + /** parent guards */ + std::map< Node, std::vector< Node > > d_parent_quant; + std::map< Node, std::vector< Node > > d_children_quant; + std::map< Node, bool > d_active_quant; /** whether we have instantiated quantified formulas */ //NodeSet d_added_inst; /** whether to do cbqi for this quantified formula */