From 1cb5f852ba17c13cc39a9c75e5bc0019c80223e8 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 15 Sep 2016 16:10:20 -0500 Subject: [PATCH] Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in EPR mode. --- src/options/quantifiers_options | 8 +- src/smt/smt_engine.cpp | 10 +- src/theory/quantifiers/ceg_instantiator.cpp | 200 +++++++----------- src/theory/quantifiers/ceg_instantiator.h | 64 ++++-- .../quantifiers/inst_match_generator.cpp | 47 ---- src/theory/quantifiers/inst_match_generator.h | 8 - src/theory/quantifiers/term_database.cpp | 11 - src/theory/quantifiers/trigger.cpp | 10 - src/theory/quantifiers/trigger.h | 2 - src/theory/quantifiers_engine.cpp | 5 +- 10 files changed, 123 insertions(+), 242 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 04b918afc..9e704691a 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -47,7 +47,7 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal option preSkolemQuant --pre-skolem-quant bool :read-write :default false apply skolemization eagerly to bodies of quantified formulas option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true - apply skolemization to nested quantified formulass + apply skolemization to nested quantified formulas option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true apply skolemization to quantified formulas aggressively option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false @@ -118,10 +118,6 @@ option quantRepMode --quant-rep-mode=MODE CVC4::theory::quantifiers::QuantRepMo option instRelevantCond --inst-rlv-cond bool :default false add relevancy conditions for instantiations - -option eagerInstQuant --eager-inst-quant bool :default false - apply quantifier instantiation eagerly - option fullSaturateQuant --full-saturate-quant bool :default false :read-write when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown option fullSaturateQuantRd --full-saturate-quant-rd bool :default true @@ -293,8 +289,6 @@ option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false preregister ground instantiations in counterexample-based quantifier instantiation option cbqiMinBounds --cbqi-min-bounds bool :default false use minimally constrained lower/upper bound for counterexample-based quantifier instantiation -option cbqiSymLia --cbqi-sym-lia bool :default false - use symbolic integer division in substitutions for counterexample-based quantifier instantiation option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false round up integer lower bounds in substitutions for counterexample-based quantifier instantiation option cbqiMidpoint --cbqi-midpoint bool :default false diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b7997a204..19bc85e3e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1748,6 +1748,12 @@ void SmtEngine::setDefaults() { options::finiteModelFind.set( true ); } } + //EPR + if( options::quantEpr() ){ + if( !options::preSkolemQuant.wasSetByUser() ){ + options::preSkolemQuant.set( true ); + } + } //now, have determined whether finite model find is on/off //apply finite model finding options @@ -1840,9 +1846,7 @@ void SmtEngine::setDefaults() { } if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){ //only instantiation should happen at last call when model is avaiable - if( !options::instWhenMode.wasSetByUser() ){ - options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); - } + options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } } diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index d31851ec4..6eb91cbdf 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -69,22 +69,20 @@ void CegInstantiator::computeProgVars( Node n ){ } } -bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, +bool CegInstantiator::isEligible( Node n ) { + //compute d_subs_fv, which program variables are contained in n, and determines if eligible + computeProgVars( 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 ){ if( i==d_vars.size() ){ //solved for all variables, now construct instantiation if( !sf.d_has_coeff.empty() ){ - if( options::cbqiSymLia() ){ - //use symbolic solved forms - SolvedForm csf; - csf.copy( ssf ); - return doAddInstantiationCoeff( csf, vars, btyp, 0, cons ); - }else{ - return doAddInstantiationCoeff( sf, vars, btyp, 0, cons ); - } + return doAddInstantiationCoeff( sf, 0, cons ); }else{ - return doAddInstantiation( sf.d_subs, vars, cons ); + return doAddInstantiation( sf.d_subs, sf.d_vars, cons ); } }else{ std::map< Node, std::map< Node, bool > > subs_proc; @@ -122,19 +120,17 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: Node n = it_eqc->second[k]; if( n!=pv ){ Trace("cbqi-inst-debug") << "...try based on equal term " << n << std::endl; - //compute d_subs_fv, which program variables are contained in n - computeProgVars( n ); //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ + if( isEligible( n ) ){ Node ns; Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) bool proc = false; if( !d_prog_var[n].empty() ){ - ns = applySubstitution( pvtn, n, sf, vars, pv_coeff, false ); + ns = applySubstitution( pvtn, n, sf, pv_coeff, false ); if( !ns.isNull() ){ computeProgVars( ns ); //substituted version must be new and cannot contain pv - proc = subs_proc[pv_coeff].find( ns )==subs_proc[pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end(); + proc = d_prog_var[ns].find( pv )==d_prog_var[ns].end(); } }else{ ns = n; @@ -142,8 +138,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: } if( proc ){ //try the substitution - subs_proc[ns][pv_coeff] = true; - if( doAddInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( tryDoAddInstantiationInc( ns, pv, pv_coeff, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ return true; } } @@ -167,7 +162,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: for( unsigned j=0; jmkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) ); } - if( doAddInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiation( sf, theta, i, effort, cons, curr_var ) ){ return true; }else{ //cleanup @@ -201,14 +196,12 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: for( unsigned kk=0; kksecond.size(); kk++ ){ Node n = it_reqc->second[kk]; Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; - //compute the variables in n - computeProgVars( n ); //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ + if( isEligible( n ) ){ Node ns; Node pv_coeff; if( !d_prog_var[n].empty() ){ - ns = applySubstitution( pvtn, n, sf, vars, pv_coeff ); + ns = applySubstitution( pvtn, n, sf, pv_coeff ); if( !ns.isNull() ){ computeProgVars( ns ); } @@ -274,7 +267,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: 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, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -288,11 +281,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: } } if( success ){ - 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, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } + if( tryDoAddInstantiationInc( val, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + return true; } } } @@ -343,14 +333,12 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: atom_lhs = Rewriter::rewrite( atom_lhs ); atom_rhs = d_zero; } - - computeProgVars( atom_lhs ); //must be an eligible term - if( d_inelig.find( atom_lhs )==d_inelig.end() ){ + if( isEligible( atom_lhs ) ){ //apply substitution to LHS of atom if( !d_prog_var[atom_lhs].empty() ){ Node atom_lhs_coeff; - atom_lhs = applySubstitution( pvtn, atom_lhs, sf, vars, atom_lhs_coeff ); + atom_lhs = applySubstitution( pvtn, atom_lhs, sf, atom_lhs_coeff ); if( !atom_lhs.isNull() ){ computeProgVars( atom_lhs ); if( !atom_lhs_coeff.isNull() ){ @@ -460,11 +448,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: mbp_lit[index].push_back( lit ); }else{ //try this bound - if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ - subs_proc[uval][veq_c] = true; - if( doAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } + if( tryDoAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + return true; } } } @@ -492,7 +477,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: } 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, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -529,7 +514,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: val = NodeManager::currentNM()->mkNode( UMINUS, val ); val = Rewriter::rewrite( val ); } - if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( tryDoAddInstantiationInc( val, pv, Node::null(), 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ return true; } } @@ -623,11 +608,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta, mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] ); if( !val.isNull() ){ - if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){ - subs_proc[val][mbp_coeff[rr][best]] = true; - if( doAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } + if( tryDoAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + return true; } } } @@ -640,11 +622,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: Node c; //null (one) coefficient val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), Node::null() ); if( !val.isNull() ){ - if( subs_proc[val].find( c )==subs_proc[val].end() ){ - subs_proc[val][c] = true; - if( doAddInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } + if( tryDoAddInstantiationInc( val, pv, c, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + return true; } } } @@ -684,11 +663,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: } Trace("cbqi-bound") << "Midpoint value : " << val << std::endl; if( !val.isNull() ){ - if( subs_proc[val].find( Node::null() )==subs_proc[val].end() ){ - subs_proc[val][Node::null()] = true; - if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } + if( tryDoAddInstantiationInc( val, pv, Node::null(), 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + return true; } } } @@ -705,11 +681,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: Node val = getModelBasedProjectionValue( pv, mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta, mbp_vts_coeff[rr][0][j], mbp_vts_coeff[rr][1][j] ); if( !val.isNull() ){ - if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){ - subs_proc[val][mbp_coeff[rr][j]] = true; - if( doAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ - return true; - } + if( tryDoAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){ + return true; } } } @@ -738,7 +711,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: //we only resort to values in the case of booleans Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); #endif - if( doAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){ + if( tryDoAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, theta, i, new_effort, cons, curr_var, subs_proc ) ){ return true; } } @@ -747,9 +720,19 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: } } +//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 ); + }else{ + return false; + } +} -bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, +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 ) { if( Trace.isOn("cbqi-inst") ){ for( unsigned j=0; jmkNode( MULT, sf.d_coeff[j], a_pv_coeff ) ); @@ -819,19 +802,10 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int }else{ Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl; } - if( options::cbqiSymLia() && pv_coeff.isNull() ){ - //apply simple substitutions also to sym_subs - prev_sym_subs[j] = ssf.d_subs[j]; - ssf.d_subs[j] = ssf.d_subs[j].substitute( a_var.begin(), a_var.end(), a_subs.begin(), a_subs.end() ); - ssf.d_subs[j] = Rewriter::rewrite( ssf.d_subs[j] ); - } } if( success ){ Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl; - vars.push_back( pv ); - btyp.push_back( bt ); - sf.push_back( pv, n, pv_coeff ); - ssf.push_back( pv, n, pv_coeff ); + sf.push_back( pv, n, pv_coeff, bt ); Node new_theta = theta; if( !pv_coeff.isNull() ){ if( new_theta.isNull() ){ @@ -848,16 +822,13 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int is_cv = true; } Trace("cbqi-inst-debug2") << "Recurse..." << std::endl; - success = doAddInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var ); + success = doAddInstantiation( sf, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var ); if( !success ){ Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl; if( is_cv ){ curr_var.push_back( pv ); } - sf.pop_back( pv, n, pv_coeff ); - ssf.pop_back( pv, n, pv_coeff ); - vars.pop_back(); - btyp.pop_back(); + sf.pop_back( pv, n, pv_coeff, bt ); } } if( success ){ @@ -874,29 +845,23 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int for( unsigned i=0; i::iterator it = prev_sym_subs.begin(); it != prev_sym_subs.end(); it++ ){ - ssf.d_subs[it->first] = it->second; - } return false; } } -bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp, - unsigned j, std::map< Node, Node >& cons ) { - - +bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, unsigned j, std::map< Node, Node >& cons ) { if( j==sf.d_has_coeff.size() ){ - return doAddInstantiation( sf.d_subs, vars, cons ); + return doAddInstantiation( sf.d_subs, sf.d_vars, cons ); }else{ - Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() ); - unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin(); + Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), sf.d_has_coeff[j] )!=sf.d_vars.end() ); + unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), sf.d_has_coeff[j] )-sf.d_vars.begin(); Node prev = sf.d_subs[index]; Assert( !sf.d_coeff[index].isNull() ); - Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << vars[index] << " = " << sf.d_subs[index] << std::endl; - Assert( vars[index].getType().isInteger() ); + Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl; + Assert( sf.d_vars[index].getType().isInteger() ); //must ensure that divisibility constraints are met //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful - Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], vars[index] ); + Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], sf.d_vars[index] ); Node eq_rhs = sf.d_subs[index]; Node eq = eq_lhs.eqNode( eq_rhs ); eq = Rewriter::rewrite( eq ); @@ -904,20 +869,20 @@ bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( eq, msum ) ){ Node veq; - if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){ + if( QuantArith::isolate( sf.d_vars[index], msum, veq, EQUAL, true )!=0 ){ Node veq_c; - if( veq[0]!=vars[index] ){ + if( veq[0]!=sf.d_vars[index] ){ Node veq_v; if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==vars[index] ); + Assert( veq_v==sf.d_vars[index] ); } } sf.d_subs[index] = veq[1]; if( !veq_c.isNull() ){ sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c ); - Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl; + Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_btyp[index] << std::endl; //intger division rounding up if from a lower bound - if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){ + if( sf.d_btyp[index]==1 && options::cbqiRoundUpLowerLia() ){ sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index], NodeManager::currentNM()->mkNode( ITE, NodeManager::currentNM()->mkNode( EQUAL, @@ -927,24 +892,8 @@ bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node ); } } - Trace("cbqi-inst-debug") << "...normalize integers : " << vars[index] << " -> " << sf.d_subs[index] << std::endl; - if( options::cbqiSymLia() ){ - //must apply substitution to previous subs - std::vector< Node > curr_var; - std::vector< Node > curr_subs; - curr_var.push_back( vars[index] ); - curr_subs.push_back( sf.d_subs[index] ); - for( unsigned k=0; k " << prevs << " to "; - sf.d_subs[k] = Rewriter::rewrite( sf.d_subs[k] ); - Trace("cbqi-inst-debug2") << sf.d_subs[k] << std::endl; - } - } - } - if( doAddInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){ + Trace("cbqi-inst-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl; + if( doAddInstantiationCoeff( sf, j+1, cons ) ){ return true; } } @@ -1176,14 +1125,11 @@ bool CegInstantiator::check() { processAssertions(); for( unsigned r=0; r<2; r++ ){ SolvedForm sf; - SolvedForm ssf; - std::vector< Node > vars; - std::vector< int > btyp; Node theta; std::map< Node, Node > cons; std::vector< Node > curr_var; //try to add an instantiation - if( doAddInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ + if( doAddInstantiation( sf, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ return true; } } @@ -1236,16 +1182,16 @@ void CegInstantiator::presolve( Node q ) { //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing //only if no nested quantifiers if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){ - std::vector< Node > vars; + std::vector< Node > ps_vars; std::map< Node, std::vector< Node > > teq; for( unsigned i=0; i terms; std::vector< Node > conj; - getPresolveEqConjuncts( vars, terms, teq, q, conj ); + getPresolveEqConjuncts( ps_vars, terms, teq, q, conj ); if( !conj.empty() ){ Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); @@ -1410,10 +1356,8 @@ void CegInstantiator::processAssertions() { std::vector< Node > akeep; for( unsigned i=0; isecond.size(); i++ ){ Node n = it->second[i]; - //compute the variables in assertion - computeProgVars( n ); //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ + if( isEligible( n ) ){ //must contain at least one variable if( !d_prog_var[n].empty() ){ Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl; diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 3d7bbcb55..5b8942027 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -38,6 +38,8 @@ public: virtual bool addLemma( Node lem ) = 0; }; +class Instantiator; + class CegInstantiator { private: QuantifiersEngine * d_qe; @@ -72,55 +74,53 @@ private: void collectCeAtoms( Node n, std::map< Node, bool >& visited ); //for adding instantiations during check 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 ){ + 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 ){ + 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 MbpBound { - public: - Node d_bound; - Node d_coeff; - Node d_vts_coeff[2]; - Node d_lit; - }; - */ // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool doAddInstantiationCoeff( SolvedForm& sf, - std::vector< Node >& vars, std::vector< int >& btyp, - unsigned j, std::map< Node, Node >& cons ); + 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 ); - Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) { - return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff ); + 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 ); @@ -142,6 +142,26 @@ public: void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); }; + +/* +// an instantiator for individual variables +class InstantiatorVar { +public: + + void postProcessInstantiation( SolvedForm& sf ); +}; +*/ + +/* +class MbpBound { +public: + Node d_bound; + Node d_coeff; + Node d_vts_coeff[2]; + Node d_lit; +}; +*/ + } } } diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index b3df9ca5d..ceae3e4c8 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -388,23 +388,6 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif return addedLemmas; } -int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){ - Assert( options::eagerInstQuant() ); - if( !d_match_pattern.isNull() ){ - InstMatch m( f ); - if( getMatch( f, t, m, qe ) ){ - if( qe->addInstantiation( f, m ) ){ - return 1; - } - } - }else{ - for( unsigned i=0; iaddTerm( f, t, qe ); - } - } - return 0; -} - InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ) { std::vector< Node > pats; @@ -716,22 +699,6 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, } } -int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){ - Assert( options::eagerInstQuant() ); - int addedLemmas = 0; - for( int i=0; i<(int)d_children.size(); i++ ){ - Node t_op = qe->getTermDatabase()->getMatchOperator( t ); - if( ((InstMatchGenerator*)d_children[i])->d_match_pattern_op==t_op ){ - InstMatch m( q ); - //if it produces a match, then process it with the rest - if( ((InstMatchGenerator*)d_children[i])->getMatch( q, t, m, qe ) ){ - processNewMatch( qe, m, i, addedLemmas ); - } - } - } - return addedLemmas; -} - InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ) : d_f( q ), d_match_pattern( pat ) { if( d_match_pattern.getKind()==NOT ){ d_match_pattern = d_match_pattern[0]; @@ -841,20 +808,6 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin } } -int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){ - //for eager instantiation only - Assert( options::eagerInstQuant() ); - InstMatch m( q ); - for( unsigned i=0; igetEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){ - return 0; - } - } - return qe->addInstantiation( q, m ) ? 1 : 0; -} - int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) { Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern ); unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f ); diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 65c5a1427..c238e3c4e 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -42,8 +42,6 @@ public: virtual bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) = 0; /** add instantiations directly */ virtual int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0; - /** add ground term t, called when t is added to term db */ - virtual int addTerm( Node q, Node t, QuantifiersEngine* qe ) { return 0; } /** set active add */ virtual void setActiveAdd( bool val ) {} /** get active score */ @@ -113,8 +111,6 @@ public: bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ); /** add instantiations */ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t */ - int addTerm( Node q, Node t, QuantifiersEngine* qe ); bool d_active_add; void setActiveAdd( bool val ); @@ -205,8 +201,6 @@ public: bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; } /** add instantiations */ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t */ - int addTerm( Node q, Node t, QuantifiersEngine* qe ); };/* class InstMatchGeneratorMulti */ /** smart (single)-trigger implementation */ @@ -240,8 +234,6 @@ public: bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; } /** add instantiations */ int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t, possibly add instantiations */ - int addTerm( Node q, Node t, QuantifiersEngine* qe ); /** get active score */ int getActiveScore( QuantifiersEngine * qe ); };/* class InstMatchGeneratorSimple */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a34ad116a..dee4952bd 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -175,17 +175,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi if( d_sygus_tdb ){ d_sygus_tdb->registerEvalTerm( n ); } - - if( options::eagerInstQuant() ){ - for( unsigned i=0; iaddTerm( n ); - } - } - } - } } }else{ setTermInactive( n ); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index d0bcd3a69..3017238ca 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -76,12 +76,6 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes ) ++(qe->d_statistics.d_multi_triggers); } //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; - if( options::eagerInstQuant() ){ - for( int i=0; i<(int)d_nodes.size(); i++ ){ - Node op = qe->getTermDatabase()->getMatchOperator( d_nodes[i] ); - qe->getTermDatabase()->registerTrigger( this, op ); - } - } Trace("trigger-debug") << "Finished making trigger." << std::endl; } @@ -107,10 +101,6 @@ bool Trigger::getMatch( Node f, Node t, InstMatch& m ){ return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine ); } -int Trigger::addTerm( Node t ){ - return d_mg->addTerm( d_f, t, d_quantEngine ); -} - Node Trigger::getInstPattern(){ return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes ); } diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 6d7bf1f4d..631627331 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -72,8 +72,6 @@ class Trigger { Currently the trigger should not be a multi-trigger. */ bool getMatch( Node f, Node t, InstMatch& m); - /** add ground term t, called when t is added to the TermDb */ - int addTerm( Node t ); /** return whether this is a multi-trigger */ bool isMultiTrigger() { return d_nodes.size()>1; } /** get inst pattern list */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index fbfdb856e..ec20d1ede 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -794,10 +794,7 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within if( !d_presolve || !options::incrementalSolving() ){ std::set< Node > added; getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure ); - //maybe have triggered instantiations if we are doing eager instantiation - if( options::eagerInstQuant() ){ - flushLemmas(); - } + //added contains also the Node that just have been asserted in this branch if( d_quant_rel ){ for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ -- 2.30.2