/********************* */ /*! \file inst_strategy_cbqi.cpp ** \verbatim ** Original author: Andrew Reynolds ** Major contributors: Morgan Deters ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** ** \brief Implementation of counterexample-guided quantifier instantiation strategies **/ #include "theory/quantifiers/inst_strategy_cbqi.h" #include "options/quantifiers_options.h" #include "smt/ite_removal.h" #include "theory/arith/partial_model.h" #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" using namespace std; using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; 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() ) { } InstStrategyCbqi::~InstStrategyCbqi() throw(){} bool InstStrategyCbqi::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) { for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ return QuantifiersEngine::QEFFORT_STANDARD; } } return QuantifiersEngine::QEFFORT_NONE; } void InstStrategyCbqi::reset_round( Theory::Effort effort ) { d_cbqi_set_quant_inactive = false; d_incomplete_check = false; //check if any cbqi lemma has not been added yet for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( doCbqi( q ) ){ if( !hasAddedCbqiLemma( q ) ){ d_added_cbqi_lemma.insert( q ); Trace("cbqi") << "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 ); if( !ceBody.isNull() ){ //add counterexample lemma Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); //require any decision on cel to be phase=true d_quantEngine->addRequirePhase( ceLit, true ); Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; //add counterexample lemma lem = Rewriter::rewrite( lem ); Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; registerCounterexampleLemma( q, lem ); } //set inactive the quantified formulas whose CE literals are asserted false }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); bool value; if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; if( !value ){ if( d_quantEngine->getValuation().isDecision( cel ) ){ Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; }else{ d_quantEngine->getModel()->setQuantifierActive( q, false ); d_cbqi_set_quant_inactive = true; } } }else{ Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; } } } } processResetInstantiationRound( effort ); } void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ double clSet = 0; if( Trace.isOn("cbqi-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl; } unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); for( int ee=0; ee<=1; ee++ ){ for( int 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->getNumLemmasWaiting()>lastWaiting ){ break; } } if( Trace.isOn("cbqi-engine") ){ if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; } double clSet2 = double(clock())/double(CLOCKS_PER_SEC); Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl; } } } bool InstStrategyCbqi::checkComplete() { if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ return false; }else{ return true; } } void InstStrategyCbqi::preRegisterQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ if( !options::cbqiAll() && !options::cbqiSplx() ){ //take full ownership of the quantified formula d_quantEngine->setOwner( q, this ); } } } void InstStrategyCbqi::registerQuantifier( Node q ) { } void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; d_quantEngine->addLemma( lem, false ); } 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( !inst::Trigger::isCbqiKind( n.getKind() ) ){ Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n << std::endl; return true; }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){ Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl; return true; }else if( n.getKind()==FORALL ){ return hasNonCbqiOperator( n[1], visited ); }else{ for( unsigned i=0; i::iterator it = d_do_cbqi.find( q ); if( it==d_do_cbqi.end() ){ bool ret = false; if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ ret = true; }else{ //if has an instantiation pattern, don't do it if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ ret = false; }else{ if( options::cbqiAll() ){ ret = true; }else{ //if quantifier has a non-arithmetic variable, then do not use cbqi //if quantifier has an APPLY_UF term, then do not use cbqi //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); std::map< Node, bool > visited; ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( q[1], visited ); } } } Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl; d_do_cbqi[q] = ret; return ret; }else{ return it->second; } } Node InstStrategyCbqi::getNextDecisionRequest(){ // all counterexample literals that are not asserted for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( hasAddedCbqiLemma( q ) ){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); bool value; if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ Trace("cbqi-debug2") << "CBQI: get next decision " << cel << std::endl; return cel; } } } return Node::null(); } //old implementation InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : InstStrategyCbqi( ie ), d_th( th ), d_counter( 0 ){ d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) ); d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); } void getInstantiationConstants( Node n, std::vector< Node >& ics ){ if( n.getKind()==INST_CONSTANT ){ if( std::find( ics.begin(), ics.end(), n )==ics.end() ){ ics.push_back( n ); } }else{ for( unsigned i=0; id_internal->d_partialModel; ArithVariables::var_iterator vi, vend; for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ ArithVar x = *vi; Node n = avnm.asNode(x); //collect instantiation constants std::vector< Node > ics; getInstantiationConstants( n, ics ); for( unsigned i=0; i t(kind::PLUS); if( n.getKind()==PLUS ){ for( int j=0; j<(int)n.getNumChildren(); j++ ){ addTermToRow( ics[i], x, n[j], t ); } }else{ addTermToRow( ics[i], x, n, t ); } d_instRows[ics[i]].push_back( x ); //this theory has constraints from f Node f = TermDb::getInstConstAttr(ics[i]); Debug("quant-arith") << "Has constraints from " << f << std::endl; //set that we should process it d_quantActive[ f ] = true; //set tableaux term if( t.getNumChildren()==0 ){ d_tableaux_term[ics[i]][x] = d_zero; }else if( t.getNumChildren()==1 ){ d_tableaux_term[ics[i]][x] = t.getChild( 0 ); }else{ d_tableaux_term[ics[i]][x] = t; } } } //print debug Debug("quant-arith-debug") << std::endl; debugPrint( "quant-arith-debug" ); d_counter++; } void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){ if( n.getKind()==MULT ){ if( TermDb::hasInstConstAttr(n[1]) && n[0].getKind()==CONST_RATIONAL ){ if( n[1]==i ){ d_ceTableaux[i][x][ n[1] ] = n[0]; }else{ d_tableaux_ce_term[i][x][ n[1] ] = n[0]; } }else{ d_tableaux[i][x][ n[1] ] = n[0]; t << n; } }else{ if( TermDb::hasInstConstAttr(n) ){ if( n==i ){ d_ceTableaux[i][x][ n ] = Node::null(); }else{ d_tableaux_ce_term[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); } }else{ d_tableaux[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) ); t << n; } } } void InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ if( e==0 ){ if( d_quantActive.find( f )!=d_quantActive.end() ){ //the point instantiation InstMatch m_point( f ); bool m_point_valid = true; int lem = 0; //scan over all instantiation rows for( int i=0; igetTermDatabase()->getNumInstantiationConstants( f ); i++ ){ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl; for( int j=0; j<(int)d_instRows[ic].size(); j++ ){ ArithVar x = d_instRows[ic][j]; if( !d_ceTableaux[ic][x].empty() ){ if( Debug.isOn("quant-arith-simplex") ){ Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl; Debug("quant-arith-simplex") << " "; for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){ if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } Debug("quant-arith-simplex") << it->first << " * " << it->second; } Debug("quant-arith-simplex") << " = "; Node v = getTableauxValue( x, false ); Debug("quant-arith-simplex") << v << std::endl; Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl; Debug("quant-arith-simplex") << " ce-term : "; for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){ if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; } Debug("quant-arith-simplex") << it->first << " * " << it->second; } Debug("quant-arith-simplex") << std::endl; } //instantiation row will be A*e + B*t = beta, // where e is a vector of terms , and t is vector of ground terms. // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant // We will construct the term ( beta - B*t)/coeff to use for e_i. InstMatch m( f ); for( unsigned k=0; kfirst; //if it is integer, we need to find variable with coefficent +/- 1 if( var.getType().isInteger() ){ std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){ ++it; if( it==d_ceTableaux[ic][x].end() ){ var = Node::null(); }else{ var = it->first; } } //Otherwise, try one that divides all ground term coefficients? // Might be futile, if rewrite ensures gcd of coeffs is 1. } if( !var.isNull() ){ //add to point instantiation if applicable if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){ Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl; Node v = getTableauxValue( x, false ); if( !var.getType().isInteger() || v.getType().isInteger() ){ m_point.setValue( i, v ); }else{ m_point_valid = false; } } Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl; if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){ lem++; } }else{ Debug("quant-arith-simplex") << "Could not find var." << std::endl; } } } } if( lem==0 && m_point_valid ){ if( d_quantEngine->addInstantiation( f, m_point ) ){ Debug("quant-arith-simplex") << "...added point instantiation." << std::endl; } } } } } void InstStrategySimplex::debugPrint( const char* c ){ ArithVariables& avnm = d_th->d_internal->d_partialModel; ArithVariables::var_iterator vi, vend; for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ ArithVar x = *vi; Node n = avnm.asNode(x); //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){ Debug(c) << x << " : " << n << ", bounds = "; if( d_th->d_internal->d_partialModel.hasLowerBound( x ) ){ Debug(c) << d_th->d_internal->d_partialModel.getLowerBound( x ); }else{ Debug(c) << "-infty"; } Debug(c) << " <= "; Debug(c) << d_th->d_internal->d_partialModel.getAssignment( x ); Debug(c) << " <= "; if( d_th->d_internal->d_partialModel.hasUpperBound( x ) ){ Debug(c) << d_th->d_internal->d_partialModel.getUpperBound( x ); }else{ Debug(c) << "+infty"; } Debug(c) << std::endl; //Debug(c) << " Term = " << d_tableaux_term[x] << std::endl; //Debug(c) << " "; //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){ // Debug(c) << "( " << it2->first << ", " << it2->second << " ) "; //} //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){ // Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) "; //} //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){ // Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) "; //} //Debug(c) << std::endl; //} } Debug(c) << std::endl; for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); Debug(c) << f << std::endl; Debug(c) << " Inst constants: "; for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ if( i>0 ){ Debug( c ) << ", "; } Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ); } Debug(c) << std::endl; for( int j=0; jgetTermDatabase()->getNumInstantiationConstants( f ); j++ ){ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); Debug(c) << " Instantiation rows for " << ic << " : "; for( int i=0; i<(int)d_instRows[ic].size(); i++ ){ if( i>0 ){ Debug(c) << ", "; } Debug(c) << d_instRows[ic][i]; } Debug(c) << std::endl; } } } //say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta, // where var is an instantiation constant from f, // t[e] is a vector of terms containing instantiation constants from f, // and term is a ground term (c1*t1 + ... + cn*tn). // We construct the term ( beta - term )/coeff to use as an instantiation for var. bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var ){ //first try +delta if( doInstantiation2( f, ic, term, x, m, var ) ){ ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith); return true; }else{ #ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA //otherwise try -delta if( doInstantiation2( f, ic, term, x, m, var, true ) ){ ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith); return true; }else{ return false; } #else return false; #endif } } bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){ // make term ( beta - term )/coeff bool vIsInteger = var.getType().isInteger(); Node beta = getTableauxValue( x, minus_delta ); if( !vIsInteger || beta.getType().isInteger() ){ Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term ); if( !d_ceTableaux[ic][x][var].isNull() ){ if( vIsInteger ){ Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) ); instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal ); }else{ Assert( d_ceTableaux[ic][x][var].getKind()==CONST_RATIONAL ); Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst() ); instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal ); } } instVal = Rewriter::rewrite( instVal ); //use as instantiation value for var int vn = var.getAttribute(InstVarNumAttribute()); m.setValue( vn, instVal ); Debug("quant-arith") << "Add instantiation " << m << std::endl; return d_quantEngine->addInstantiation( f, m ); }else{ return false; } } /* Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){ if( d_th->d_internal->d_partialModel.hasArithVar(n) ){ ArithVar v = d_th->d_internal->d_partialModel.asArithVar( n ); return getTableauxValue( v, minus_delta ); }else{ return NodeManager::currentNM()->mkConst( Rational(0) ); } } */ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ const Rational& delta = d_th->d_internal->d_partialModel.getDelta(); DeltaRational drv = d_th->d_internal->d_partialModel.getAssignment( v ); Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta ); return mkRationalNode(qmodel); } //new implementation bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs ) { return d_out->addInstantiation( subs ); } bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) { return d_out->isEligibleForInstantiation( n ); } bool CegqiOutputInstStrategy::addLemma( Node lem ) { return d_out->addLemma( lem ); } InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategyCbqi( qe ) { d_out = new CegqiOutputInstStrategy( this ); d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); } InstStrategyCegqi::~InstStrategyCegqi() throw () { delete d_out; for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(), iend = d_cinst.end(); i != iend; ++i) { CegInstantiator * instantiator = (*i).second; delete instantiator; } d_cinst.clear(); } void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { d_check_vts_lemma_lc = false; } void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { if( e==0 ){ 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 ); //heuristic for now, until we know how to do nested quantification Node delta = d_quantEngine->getTermDatabase()->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 ); for( unsigned i=0; imkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst() ) ); d_quantEngine->getOutputChannel().lemma( inf_lem_lb ); } } } } bool InstStrategyCegqi::addInstantiation( 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 ) ){ 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 ); 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; } } } bool InstStrategyCegqi::addLemma( Node lem ) { return d_quantEngine->addLemma( lem ); } bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){ if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){ return true; }else{ //only legal if current quantified formula contains n return TermDb::containsTerm( d_curr_quant, n ); } }else{ return true; } } CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q ); if( it==d_cinst.end() ){ CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true ); d_cinst[q] = cinst; return cinst; }else{ return it->second; } } void InstStrategyCegqi::registerQuantifier( Node q ) { if( options::cbqiPreRegInst() ){ //just get the instantiator getInstantiator( q ); } } 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( int i=0; igetTermDatabase()->getNumInstantiationConstants( q ); i++ ){ ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) ); } std::vector< Node > lems; lems.push_back( lem ); CegInstantiator * cinst = getInstantiator( q ); cinst->registerCounterexampleLemma( lems, ce_vars ); for( unsigned i=0; iaddLemma( lems[i], false ); } } void InstStrategyCegqi::presolve() { if( options::cbqiPreRegInst() ){ for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){ it->second->presolve( it->first ); } } }