diff options
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 54 |
1 files changed, 28 insertions, 26 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 52ea7cc62..93505b494 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -19,7 +19,9 @@ #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/theory_engine.h" @@ -66,8 +68,8 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { Trace("cbqi-debug") << "Do cbqi for " << q << std::endl; //add cbqi lemma //get the counterexample literal - Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); - Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); + Node ceLit = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); + Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q ); if( !ceBody.isNull() ){ //add counterexample lemma Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); @@ -90,7 +92,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); if( itc!=qepr->d_consts.end() ){ Assert( !itc->second.empty() ); - Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ); + Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ); std::vector< Node > disj; for( unsigned j=0; j<itc->second.size(); j++ ){ disj.push_back( ic.eqNode( itc->second[j] ) ); @@ -111,7 +113,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { //compute dependencies between quantified formulas if( options::cbqiLitDepend() || options::cbqiInnermost() ){ std::vector< Node > ics; - TermDb::computeVarContains( q, ics ); + TermUtil::computeVarContains( q, ics ); d_parent_quant[q].clear(); d_children_quant[q].clear(); std::vector< Node > dep; @@ -121,7 +123,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { d_parent_quant[q].push_back( qi ); d_children_quant[qi].push_back( q ); Assert( hasAddedCbqiLemma( qi ) ); - Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi ); + Node qicel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( qi ); dep.push_back( qi ); dep.push_back( qicel ); } @@ -135,7 +137,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { //must register all sub-quantifiers of counterexample lemma, register their lemmas std::vector< Node > quants; - TermDb::computeQuantContains( lem, quants ); + TermUtil::computeQuantContains( lem, quants ); for( unsigned i=0; i<quants.size(); i++ ){ if( doCbqi( quants[i] ) ){ registerCbqiLemma( quants[i] ); @@ -143,7 +145,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) { if( options::cbqiNestedQE() ){ //record these as counterexample quantifiers QAttributes qa; - TermDb::computeQuantAttributes( quants[i], qa ); + QuantAttributes::computeQuantAttributes( quants[i], qa ); if( !qa.d_qid_num.isNull() ){ d_id_to_ce_quant[ qa.d_qid_num ] = quants[i]; d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num; @@ -171,7 +173,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { 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 ); + Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); bool value; if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; @@ -299,7 +301,7 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis Node ret = n; if( n.getKind()==FORALL ){ QAttributes qa; - TermDb::computeQuantAttributes( n, qa ); + QuantAttributes::computeQuantAttributes( n, qa ); if( qa.d_qid_num.isNull() ){ std::vector< Node > rc; rc.push_back( n[0] ); @@ -392,15 +394,15 @@ Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< No //should not contain quantifiers Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) ); } - Assert( d_quantEngine->getTermDatabase()->d_inst_constants[q].size()==inst_terms.size() ); + Assert( d_quantEngine->getTermUtil()->d_inst_constants[q].size()==inst_terms.size() ); //replace inst constants with instantiation - Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermDatabase()->d_inst_constants[q].begin(), - d_quantEngine->getTermDatabase()->d_inst_constants[q].end(), + Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(), + d_quantEngine->getTermUtil()->d_inst_constants[q].end(), inst_terms.begin(), inst_terms.end() ); if( doVts ){ //do virtual term substitution ret = Rewriter::rewrite( ret ); - ret = d_quantEngine->getTermDatabase()->rewriteVtsSymbols( ret ); + ret = d_quantEngine->getTermUtil()->rewriteVtsSymbols( ret ); } Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl; Trace("cbqi-nqe") << " " << n << std::endl; @@ -413,7 +415,7 @@ Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& vi Node ret = n; if( n.getKind()==FORALL ){ QAttributes qa; - TermDb::computeQuantAttributes( n, qa ); + QuantAttributes::computeQuantAttributes( n, qa ); if( !qa.d_qid_num.isNull() ){ //if it has an id, check whether we have done quantifier elimination for this id std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num ); @@ -478,7 +480,7 @@ void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){ if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()!=BOUND_VARIABLE && TermDb::hasBoundVarAttr( n ) ){ + if( n.getKind()!=BOUND_VARIABLE && TermUtil::hasBoundVarAttr( n ) ){ if( !inst::Trigger::isCbqiKind( n.getKind() ) ){ Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n << std::endl; return true; @@ -554,8 +556,8 @@ bool InstStrategyCbqi::doCbqi( Node q ){ std::map< Node, int >::iterator it = d_do_cbqi.find( q ); if( it==d_do_cbqi.end() ){ int ret = 2; - if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ - Assert( !d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) ); + if( !d_quantEngine->getQuantAttributes()->isQuantElim( q ) ){ + Assert( !d_quantEngine->getQuantAttributes()->isQuantElimPartial( q ) ); //if has an instantiation pattern, don't do it if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ @@ -564,7 +566,7 @@ bool InstStrategyCbqi::doCbqi( Node q ){ } } } - if( d_quantEngine->getTermDatabase()->isQAttrSygus( q ) ){ + if( d_quantEngine->getQuantAttributes()->isSygus( q ) ){ ret = 0; } if( ret!=0 ){ @@ -616,7 +618,7 @@ Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool } //then check self if( hasAddedCbqiLemma( q ) ){ - Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); + Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); bool value; if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl; @@ -699,14 +701,14 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const ); d_small_const = Rewriter::rewrite( d_small_const ); //heuristic for now, until we know how to do nested quantification - Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false ); + Node delta = d_quantEngine->getTermUtil()->getVtsDelta( true, false ); if( !delta.isNull() ){ Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl; Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const ); d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); } std::vector< Node > inf; - d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false ); + d_quantEngine->getTermUtil()->getVtsTerms( inf, true, false, false ); for( unsigned i=0; i<inf.size(); i++ ){ Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl; Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) ); @@ -719,14 +721,14 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { Assert( !d_curr_quant.isNull() ); //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 ) ){ + if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( 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{ //check if we need virtual term substitution (if used delta or infinity) - bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false ); + bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false ); if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){ ++(d_quantEngine->d_statistics.d_instantiations_cbqi); //d_added_inst.insert( d_curr_quant ); @@ -761,7 +763,7 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { } } //only legal if current quantified formula contains n - return TermDb::containsTerm( d_curr_quant, n ); + return TermUtil::containsTerm( d_curr_quant, n ); } }else{ return true; @@ -796,8 +798,8 @@ void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) { //must register with the instantiator //must explicitly remove ITEs so that we record dependencies std::vector< Node > ce_vars; - for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){ - ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) ); + for( unsigned i=0; i<d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ); i++ ){ + ce_vars.push_back( d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ) ); } std::vector< Node > lems; lems.push_back( lem ); |