diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-25 10:10:47 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-25 10:10:47 -0600 |
commit | a1135ca591276f6d02b3632bc77a3934ded2d2af (patch) | |
tree | fa45a24bc072970abd71f59967a4dd759d2be0d2 /src/theory/quantifiers/inst_strategy_cbqi.cpp | |
parent | bab37658aa27ee455e3928c66db49c1bb3224e3b (diff) |
Minor improvement to partial qe. Add options for representative selection in FMF.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 42 |
1 files changed, 23 insertions, 19 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index e6c9b9e6b..faad18c28 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -34,7 +34,9 @@ using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) - : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), d_added_inst( qe->getUserContext() ) { + : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ) +//, d_added_inst( qe->getUserContext() ) +{ } InstStrategyCbqi::~InstStrategyCbqi() throw(){} @@ -97,14 +99,6 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { }else{ Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; } - //if doing partial quantifier elimination, do not process this if already processed once - if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) ){ - if( d_added_inst.find( q )!=d_added_inst.end() ){ - d_quantEngine->getModel()->setQuantifierActive( q, false ); - d_cbqi_set_quant_inactive = true; - d_incomplete_check = true; - } - } } } } @@ -597,21 +591,23 @@ InstStrategyCegqi::~InstStrategyCegqi() throw () { } void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { - d_check_vts_lemma_lc = true; + d_check_vts_lemma_lc = false; } -void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { +void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { if( e==0 ){ - CegInstantiator * cinst = getInstantiator( f ); - Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; - d_curr_quant = f; + CegInstantiator * cinst = getInstantiator( q ); + Trace("inst-alg") << "-> Run cegqi for " << q << std::endl; + d_curr_quant = q; if( !cinst->check() ){ d_incomplete_check = true; + d_check_vts_lemma_lc = true; } d_curr_quant = Node::null(); }else if( e==1 ){ //minimize the free delta heuristically on demand if( d_check_vts_lemma_lc ){ + Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl; d_check_vts_lemma_lc = false; d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const ); d_small_const = Rewriter::rewrite( d_small_const ); @@ -635,13 +631,21 @@ void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) { Assert( !d_curr_quant.isNull() ); - //check if we need virtual term substitution (if used delta or infinity) - bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false ); - if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){ - d_added_inst.insert( d_curr_quant ); + //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma + if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){ + d_cbqi_set_quant_inactive = true; + d_incomplete_check = true; + d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false ); return true; }else{ - return false; + //check if we need virtual term substitution (if used delta or infinity) + bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false ); + if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){ + //d_added_inst.insert( d_curr_quant ); + return true; + }else{ + return false; + } } } |