From 2b16150a3cad033fec971839897a4aa28b002edb Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 15 Sep 2016 18:44:04 -0500 Subject: [PATCH] Further refactor cbqi. --- src/theory/quantifiers/ceg_instantiator.cpp | 249 +++++++++----------- src/theory/quantifiers/ceg_instantiator.h | 137 +++++++---- 2 files changed, 208 insertions(+), 178 deletions(-) diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 6eb91cbdf..358ba7381 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -75,26 +75,62 @@ bool CegInstantiator::isEligible( Node n ) { return d_inelig.find( n )==d_inelig.end(); } -bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ){ +void CegInstantiator::registerInstantiationVariable( Node v, unsigned index ) { + if( d_instantiator.find( v )==d_instantiator.end() ){ + //TODO + } + d_curr_subs_proc[v].clear(); + d_curr_index[v] = index; +} + +void CegInstantiator::unregisterInstantiationVariable( Node v ) { + d_curr_subs_proc.erase( v ); + d_curr_index.erase( v ); +} + +bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ){ if( i==d_vars.size() ){ //solved for all variables, now construct instantiation - if( !sf.d_has_coeff.empty() ){ - return doAddInstantiationCoeff( sf, 0, cons ); + bool needsPostprocess = !sf.d_has_coeff.empty(); + if( needsPostprocess ){ + SolvedForm sf_tmp; + sf_tmp.copy( sf ); + bool postProcessSuccess = true; + if( !processInstantiationCoeff( sf_tmp ) ){ + postProcessSuccess = false; + } + if( postProcessSuccess ){ + return doAddInstantiation( sf_tmp.d_subs, sf_tmp.d_vars ); + }else{ + return false; + } }else{ - return doAddInstantiation( sf.d_subs, sf.d_vars, cons ); + return doAddInstantiation( sf.d_subs, sf.d_vars ); } }else{ - std::map< Node, std::map< Node, bool > > subs_proc; //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; bool is_cv = false; Node pv; - if( curr_var.empty() ){ + if( d_stack_vars.empty() ){ pv = d_vars[i]; }else{ - pv = curr_var.back(); + pv = d_stack_vars.back(); is_cv = true; + d_stack_vars.pop_back(); + } + registerInstantiationVariable( pv, i ); + /* + //get the instantiator object + std::map< Node, Instantiator * >::iterator itin = d_instantiator.find( pv ); + Instantiator * vinst = NULL; + if( itin!=d_instantiator.end() ){ + vinst = itin->second; + } + if( vinst!=NULL ){ + d_active_instantiators[vinst] = true; } + */ + TypeNode pvtn = pv.getType(); TypeNode pvtnb = pvtn.getBaseType(); Node pvr = pv; @@ -115,6 +151,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl; std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr ); if( it_eqc!=d_curr_eqc.end() ){ + //std::vector< Node > eq_candidates; Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl; for( unsigned k=0; ksecond.size(); k++ ){ Node n = it_eqc->second[k]; @@ -138,7 +175,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i } if( proc ){ //try the substitution - if( tryDoAddInstantiationInc( ns, pv, pv_coeff, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + if( tryDoAddInstantiationInc( pv, ns, pv_coeff, 0, sf, effort ) ){ return true; } } @@ -152,27 +189,24 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i Node n = it_eqc->second[k]; if( n.getKind()==APPLY_CONSTRUCTOR ){ Trace("cbqi-inst-debug") << "... " << i << "...try based on constructor term " << n << std::endl; - cons[pv] = n.getOperator(); + std::vector< Node > children; + children.push_back( n.getOperator() ); const Datatype& dt = ((DatatypeType)(pvtn).toType()).getDatatype(); unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() ); - if( is_cv ){ - curr_var.pop_back(); - } //now must solve for selectors applied to pv for( unsigned j=0; jmkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) ); + Node c = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ); + pushStackVariable( c ); + children.push_back( c ); } - if( doAddInstantiation( sf, theta, i, effort, cons, curr_var ) ){ + Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); + if( tryDoAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ return true; }else{ //cleanup - cons.erase( pv ); - Assert( curr_var.size()>=dt[cindex].getNumArgs() ); + Assert( d_stack_vars.size()>=dt[cindex].getNumArgs() ); for( unsigned j=0; j msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - if( Trace.isOn("cbqi-inst-debug") ){ - Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); - Trace("cbqi-inst-debug") << "isolate for " << pv << " : " << pv.getType() << "..." << std::endl; - } - Node veq; - if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ - Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl; - Node veq_c; - if( veq[0]!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } - } - Node val = veq[1]; - if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ - subs_proc[val][veq_c] = true; - if( doAddInstantiationInc( val, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var ) ){ - return true; - } - } + if( tryDoAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ + return true; } } - */ }else if( pvtnb.isDatatype() ){ val = solve_dt( pv, lhs[j], ns, lhs[j], ns ); if( !val.isNull() ){ - success = true; - } - } - if( success ){ - if( tryDoAddInstantiationInc( val, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ - return true; + if( tryDoAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){ + return true; + } } } } @@ -448,7 +449,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i mbp_lit[index].push_back( lit ); }else{ //try this bound - if( tryDoAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + if( tryDoAddInstantiationInc( pv, uval, veq_c, uires>0 ? 1 : -1, sf, effort ) ){ return true; } } @@ -475,11 +476,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], bv::utils::mkConst(pvtn.getConst(), 1) ); } - if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ - subs_proc[uval][veq_c] = true; - if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var ) ){ - return true; - } + if( tryDoAddInstantiationInc( pv, uval, veq_c, 0, sf, effort ) ){ + return true; } } } @@ -514,7 +512,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i val = NodeManager::currentNM()->mkNode( UMINUS, val ); val = Rewriter::rewrite( val ); } - if( tryDoAddInstantiationInc( val, pv, Node::null(), 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + if( tryDoAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ return true; } } @@ -605,10 +603,10 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict if( !options::cbqiMidpoint() || pvtn.isInteger() || mbp_vts_coeff[rr][1][best].isNull() ){ Node val = mbp_bounds[rr][best]; - val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta, + val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta, mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] ); if( !val.isNull() ){ - if( tryDoAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + if( tryDoAddInstantiationInc( pv, val, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, effort ) ){ return true; } } @@ -620,9 +618,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){ Node val = d_zero; Node c; //null (one) coefficient - val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), Node::null() ); + val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, sf.d_theta, Node::null(), Node::null() ); if( !val.isNull() ){ - if( tryDoAddInstantiationInc( val, pv, c, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + if( tryDoAddInstantiationInc( pv, val, c, 0, sf, effort ) ){ return true; } } @@ -637,7 +635,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i bothBounds = false; }else{ vals[rr] = mbp_bounds[rr][best]; - vals[rr] = getModelBasedProjectionValue( pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], theta, + vals[rr] = getModelBasedProjectionValue( pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.d_theta, mbp_vts_coeff[rr][0][best], Node::null() ); } Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl; @@ -663,7 +661,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i } Trace("cbqi-bound") << "Midpoint value : " << val << std::endl; if( !val.isNull() ){ - if( tryDoAddInstantiationInc( val, pv, Node::null(), 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + if( tryDoAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){ return true; } } @@ -678,10 +676,10 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i int rr = upper_first ? (1-r) : r; for( unsigned j=0; j0 || pvtn.isBoolean() || pvtn.isBitVector() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){ + if( ( effort>0 || pvtn.isBoolean() || pvtn.isBitVector() || is_cv ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){ #ifdef CVC4_ASSERTIONS if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){ @@ -711,29 +709,43 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i //we only resort to values in the case of booleans Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); #endif - if( tryDoAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, theta, i, new_effort, cons, curr_var, subs_proc ) ){ + if( tryDoAddInstantiationInc( pv, mv, pv_coeff_m, 0, sf, new_effort ) ){ return true; } } Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; + if( is_cv ){ + d_stack_vars.push_back( pv ); + } + /* + if( vinst!=NULL ){ + d_active_instantiators.erase( vinst ); + } + */ + unregisterInstantiationVariable( pv ); return false; } } +void CegInstantiator::pushStackVariable( Node v ) { + d_stack_vars.push_back( v ); +} + +void CegInstantiator::popStackVariable() { + d_stack_vars.pop_back(); +} + //cached version -bool CegInstantiator::tryDoAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var, - std::map< Node, std::map< Node, bool > >& subs_proc ) { - if( subs_proc[n].find( pv_coeff )==subs_proc[n].end() ){ - subs_proc[n][pv_coeff] = true; - return doAddInstantiationInc( n, pv, pv_coeff, bt, sf, theta, i, effort, cons, curr_var ); +bool CegInstantiator::tryDoAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ) { + if( d_curr_subs_proc[pv][n].find( pv_coeff )==d_curr_subs_proc[pv][n].end() ){ + d_curr_subs_proc[pv][n][pv_coeff] = true; + return doAddInstantiationInc( pv, n, pv_coeff, bt, sf, effort ); }else{ return false; } } -bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ) { +bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ) { if( Trace.isOn("cbqi-inst") ){ for( unsigned j=0; j& cons ) { - if( j==sf.d_has_coeff.size() ){ - return doAddInstantiation( sf.d_subs, sf.d_vars, cons ); - }else{ +bool CegInstantiator::processInstantiationCoeff( SolvedForm& sf ) { + for( unsigned j=0; j " << sf.d_subs[index] << std::endl; - if( doAddInstantiationCoeff( sf, j+1, cons ) ){ - return true; - } + }else{ + Trace("cbqi-inst-debug") << "...failed." << std::endl; + return false; } + }else{ + Trace("cbqi-inst-debug") << "...failed." << std::endl; + return false; } - sf.d_subs[index] = prev; - Trace("cbqi-inst-debug") << "...failed." << std::endl; - return false; } + return true; } -bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) { +bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ) { if( vars.size()>d_vars.size() ){ Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; std::map< Node, Node > subs_map; @@ -913,7 +918,9 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector } subs.clear(); for( unsigned i=0; i::iterator it = subs_map.find( d_vars[i] ); + Assert( it!=subs_map.end() ); + Node n = it->second; Trace("cbqi-inst-debug") << " " << d_vars[i] << " -> " << n << std::endl; subs.push_back( n ); } @@ -933,26 +940,6 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector return ret; } -Node CegInstantiator::constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ) { - std::map< Node, Node >::iterator it = subs_map.find( n ); - if( it!=subs_map.end() ){ - return it->second; - }else{ - it = cons.find( n ); - Assert( it!=cons.end() ); - std::vector< Node > children; - children.push_back( it->second ); - const Datatype& dt = Datatype::datatypeOf( it->second.toExpr() ); - unsigned cindex = Datatype::indexOf( it->second.toExpr() ); - for( unsigned i=0; imkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), n ); - Node nc = constructInstantiation( nn, subs_map, cons ); - children.push_back( nc ); - } - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - } -} - Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff ) { Assert( d_prog_var.find( n )!=d_prog_var.end() ); @@ -1125,11 +1112,9 @@ bool CegInstantiator::check() { processAssertions(); for( unsigned r=0; r<2; r++ ){ SolvedForm sf; - Node theta; - std::map< Node, Node > cons; - std::vector< Node > curr_var; + d_stack_vars.clear(); //try to add an instantiation - if( doAddInstantiation( sf, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ + if( doAddInstantiation( sf, 0, r==0 ? 0 : 2 ) ){ return true; } } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 5b8942027..c2670d74e 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -40,6 +40,44 @@ public: class Instantiator; + +//solved form, involves substitution with coefficients +class SolvedForm { +public: + std::vector< Node > d_vars; + std::vector< Node > d_subs; + std::vector< Node > d_coeff; + std::vector< int > d_btyp; + std::vector< Node > d_has_coeff; + Node d_theta; + void copy( SolvedForm& sf ){ + d_vars.insert( d_vars.end(), sf.d_vars.begin(), sf.d_vars.end() ); + d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() ); + d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() ); + d_btyp.insert( d_btyp.end(), sf.d_btyp.begin(), sf.d_btyp.end() ); + d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() ); + d_theta = sf.d_theta; + } + void push_back( Node pv, Node n, Node pv_coeff, int bt ){ + d_vars.push_back( pv ); + d_subs.push_back( n ); + d_coeff.push_back( pv_coeff ); + d_btyp.push_back( bt ); + if( !pv_coeff.isNull() ){ + d_has_coeff.push_back( pv ); + } + } + void pop_back( Node pv, Node n, Node pv_coeff, int bt ){ + d_vars.pop_back(); + d_subs.pop_back(); + d_coeff.pop_back(); + d_btyp.pop_back(); + if( !pv_coeff.isNull() ){ + d_has_coeff.pop_back(); + } + } +}; + class CegInstantiator { private: QuantifiersEngine * d_qe; @@ -69,6 +107,19 @@ private: //atoms of the CE lemma bool d_is_nested_quant; std::vector< Node > d_ce_atoms; +private: + //map from variables to their instantiators + std::map< Node, Instantiator * > d_instantiator; + //cache of current substitutions tried between register/unregister + std::map< Node, std::map< Node, std::map< Node, bool > > > d_curr_subs_proc; + std::map< Node, unsigned > d_curr_index; + //stack of temporary variables we are solving (e.g. subfields of datatypes) + std::vector< Node > d_stack_vars; + //used instantiators + std::map< Instantiator *, bool > d_active_instantiators; + //register variable + void registerInstantiationVariable( Node v, unsigned index ); + void unregisterInstantiationVariable( Node v ); private: //collect atoms void collectCeAtoms( Node n, std::map< Node, bool >& visited ); @@ -76,54 +127,20 @@ private: void computeProgVars( Node n ); // is eligible bool isEligible( Node n ); - //solved form, involves substitution with coefficients - class SolvedForm { - public: - std::vector< Node > d_vars; - std::vector< Node > d_subs; - std::vector< Node > d_coeff; - std::vector< int > d_btyp; - std::vector< Node > d_has_coeff; - void copy( SolvedForm& sf ){ - d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() ); - d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() ); - d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() ); - } - void push_back( Node pv, Node n, Node pv_coeff, int bt ){ - d_vars.push_back( pv ); - d_subs.push_back( n ); - d_coeff.push_back( pv_coeff ); - d_btyp.push_back( bt ); - if( !pv_coeff.isNull() ){ - d_has_coeff.push_back( pv ); - } - } - void pop_back( Node pv, Node n, Node pv_coeff, int bt ){ - d_vars.pop_back(); - d_subs.pop_back(); - d_coeff.pop_back(); - d_btyp.pop_back(); - if( !pv_coeff.isNull() ){ - d_has_coeff.pop_back(); - } - } - }; // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool doAddInstantiation( SolvedForm& sf, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool tryDoAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var, - std::map< Node, std::map< Node, bool > >& subs_proc ); - bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool doAddInstantiationCoeff( SolvedForm& sf, unsigned j, std::map< Node, Node >& cons ); - bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ); - Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ); + bool doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ); + bool doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ); + bool processInstantiationCoeff( SolvedForm& sf ); + bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ); Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) { return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff ); } Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ); + //TODO: move to public + void pushStackVariable( Node v ); + void popStackVariable(); + bool tryDoAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ); Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ); void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); @@ -143,14 +160,42 @@ public: }; -/* + // an instantiator for individual variables -class InstantiatorVar { +// will make calls into CegInstantiator::doAddInstantiationInc +class Instantiator { +public: + virtual void reset( unsigned effort ) {} + + virtual bool processEqualTerm( SolvedForm& sf, Node pv, Node n, unsigned effort ) { return false; } + virtual bool processEqualTerms( SolvedForm& sf, Node pv, std::vector< Node >& term, unsigned effort ) { return false; } + + virtual bool processEquality( SolvedForm& sf, Node pv, Node lhs, Node rhs, unsigned effort ) { return false; } + virtual bool processEqualities( SolvedForm& sf, Node pv, std::vector< Node >& lhss, std::vector< Node >& rhss, unsigned effort ) { return false; } + + virtual bool processAssertion( SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; } + virtual bool processAssertions( SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { return false; } + + virtual bool allowModelValue( SolvedForm& sf, Node pv, unsigned effort ) { return true; } + + virtual bool needsPostProcessInstantiation( SolvedForm& sf, unsigned effort ) { return false; } + virtual bool postProcessInstantiation( SolvedForm& sf, unsigned effort ) { return true; } +}; + +class ArithInstantiator : public Instantiator { +public: + +}; + +class DtInstantiator : public Instantiator { +public: + +}; + +class EprInstantiator : public Instantiator { public: - void postProcessInstantiation( SolvedForm& sf ); }; -*/ /* class MbpBound { -- 2.30.2