From a1135ca591276f6d02b3632bc77a3934ded2d2af Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 25 Feb 2016 10:10:47 -0600 Subject: Minor improvement to partial qe. Add options for representative selection in FMF. --- src/theory/quantifiers/inst_strategy_cbqi.cpp | 42 +++++++++++++++------------ src/theory/quantifiers/inst_strategy_cbqi.h | 2 +- src/theory/quantifiers/term_database.cpp | 15 ++++++++++ src/theory/quantifiers/term_database.h | 5 ++++ 4 files changed, 44 insertions(+), 20 deletions(-) (limited to 'src/theory/quantifiers') 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; + } } } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 8de844eb8..fd8afb149 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -40,7 +40,7 @@ protected: /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; /** whether we have instantiated quantified formulas */ - NodeSet d_added_inst; + //NodeSet d_added_inst; /** whether to do cbqi for this quantified formula */ std::map< Node, bool > d_do_cbqi; /** register ce lemma */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cb23b8bb7..be0f60654 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1680,6 +1680,21 @@ bool TermDb::containsTerms( Node n, std::vector< Node >& t ) { } } +int TermDb::getTermDepth( Node n ) { + if (!n.hasAttribute(TermDepthAttribute()) ){ + int maxDepth = -1; + for( unsigned i=0; imaxDepth ){ + maxDepth = depth; + } + } + TermDepthAttribute tda; + n.setAttribute(tda,1+maxDepth); + } + return n.getAttribute(TermDepthAttribute()); +} + bool TermDb::containsUninterpretedConstant( Node n ) { std::map< Node, bool > visited; return containsUninterpretedConstant2( n, visited ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 5560098c9..b1cfcf2ae 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -68,6 +68,9 @@ typedef expr::Attribute InstLevelAttribute; struct InstVarNumAttributeId {}; typedef expr::Attribute InstVarNumAttribute; +struct TermDepthAttributeId {}; +typedef expr::Attribute TermDepthAttribute; + struct ModelBasisAttributeId {}; typedef expr::Attribute ModelBasisAttribute; //for APPLY_UF terms, 1 : term has direct child with model basis attribute, @@ -436,6 +439,8 @@ public: static bool containsTerms( Node n, std::vector< Node >& t ); /** contains uninterpreted constant */ static bool containsUninterpretedConstant( Node n ); + /** get the term depth of n */ + static int getTermDepth( Node n ); /** simple negate */ static Node simpleNegate( Node n ); /** is assoc */ -- cgit v1.2.3