From e61a79df77924c66e8f6ff3141172bda49301475 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 26 Sep 2015 10:04:34 +0200 Subject: [PATCH] Better organization of quantifiers modules, promote full saturation to module. Add heuristics for cbqi LIA instantiation with coefficients. --- src/theory/quantifiers/inst_strategy_cbqi.cpp | 183 ++++++++------- src/theory/quantifiers/inst_strategy_cbqi.h | 54 +++-- .../quantifiers/inst_strategy_e_matching.cpp | 212 ++++++++++-------- .../quantifiers/inst_strategy_e_matching.h | 18 +- .../quantifiers/instantiation_engine.cpp | 29 +-- src/theory/quantifiers/instantiation_engine.h | 2 - src/theory/quantifiers/model_engine.cpp | 2 +- src/theory/quantifiers/options | 6 +- src/theory/quantifiers_engine.cpp | 81 ++++--- src/theory/quantifiers_engine.h | 6 + 10 files changed, 351 insertions(+), 242 deletions(-) diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 3a626cb92..8e6673fb9 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -67,12 +67,23 @@ void CegInstantiator::computeProgVars( Node n ){ } } -bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< int >& btyp, - std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort, +bool CegInstantiator::addInstantiation( 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 ){ if( i==d_vars.size() ){ - return addInstantiationCoeff( subs, vars, coeff, btyp, has_coeff, 0, cons ); + //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 addInstantiationCoeff( csf, vars, btyp, 0, cons ); + }else{ + return addInstantiationCoeff( sf, vars, btyp, 0, cons ); + } + }else{ + return addInstantiation( sf.d_subs, vars, cons ); + } }else{ std::map< Node, std::map< Node, bool > > subs_proc; //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; @@ -98,7 +109,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< //if in effort=2, we must choose at least one model value if( (i+1) >::iterator it_eqc = d_curr_eqc.find( pvr ); @@ -116,7 +127,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< 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( n, subs, vars, coeff, has_coeff, pv_coeff, false ); + ns = applySubstitution( n, sf, vars, pv_coeff, false ); if( !ns.isNull() ){ computeProgVars( ns ); //substituted version must be new and cannot contain pv @@ -129,7 +140,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< if( proc ){ //try the substitution subs_proc[ns][pv_coeff] = true; - if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){ + if( addInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -162,7 +173,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node ns; Node pv_coeff; if( !d_prog_var[n].empty() ){ - ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff ); + ns = applySubstitution( n, sf, vars, pv_coeff ); if( !ns.isNull() ){ computeProgVars( ns ); } @@ -216,7 +227,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node val = veq[1]; if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ subs_proc[val][veq_c] = true; - if( addInstantiationInc( val, pv, veq_c, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){ + if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -253,7 +264,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< for( unsigned j=0; jmkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) ); } - if( addInstantiation( subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){ + if( addInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; }else{ //cleanup @@ -316,7 +327,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< //apply substitution to LHS of atom if( !d_prog_var[atom_lhs].empty() ){ Node atom_lhs_coeff; - atom_lhs = applySubstitution( atom_lhs, subs, vars, coeff, has_coeff, atom_lhs_coeff ); + atom_lhs = applySubstitution( atom_lhs, sf, vars, atom_lhs_coeff ); if( !atom_lhs.isNull() ){ computeProgVars( atom_lhs ); if( !atom_lhs_coeff.isNull() ){ @@ -472,7 +483,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< //try this bound if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ subs_proc[uval][veq_c] = true; - if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){ + if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -509,7 +520,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< val = NodeManager::currentNM()->mkNode( UMINUS, val ); val = Rewriter::rewrite( val ); } - if( addInstantiationInc( val, pv, Node::null(), 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){ + if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -603,7 +614,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< 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( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){ + if( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -619,7 +630,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< if( !val.isNull() ){ if( subs_proc[val].find( c )==subs_proc[val].end() ){ subs_proc[val][c] = true; - if( addInstantiationInc( val, pv, c, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){ + if( addInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -639,7 +650,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< 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( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){ + if( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -662,7 +673,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< //we only resort to values in the case of booleans Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); #endif - if( addInstantiationInc( mv, pv, pv_coeff_m, 0, subs, vars, coeff, btyp, has_coeff, theta, i, new_effort, cons, curr_var ) ){ + if( addInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){ return true; } } @@ -672,15 +683,14 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } -bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< int >& btyp, - std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort, +bool CegInstantiator::addInstantiationInc( 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 ) { if( Trace.isOn("cbqi-inst") ){ - for( unsigned j=0; j a_subs; a_subs.push_back( n ); @@ -703,47 +713,51 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b bool success = true; std::map< int, Node > prev_subs; std::map< int, Node > prev_coeff; + std::map< int, Node > prev_sym_subs; std::vector< Node > new_has_coeff; - for( unsigned j=0; jmkNode( MULT, coeff[j], a_pv_coeff ) ); + sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) ); } } - if( subs[j]!=prev_subs[j] ){ - computeProgVars( subs[j] ); + if( sf.d_subs[j]!=prev_subs[j] ){ + computeProgVars( sf.d_subs[j] ); } }else{ - Trace("cbqi-inst-debug") << "...failed to apply substitution to " << subs[j] << std::endl; + Trace("cbqi-inst-debug") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl; success = false; break; } } + 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 ){ - subs.push_back( n ); vars.push_back( pv ); - coeff.push_back( pv_coeff ); btyp.push_back( bt ); - if( !pv_coeff.isNull() ){ - has_coeff.push_back( pv ); - } + sf.push_back( pv, n, pv_coeff ); + ssf.push_back( pv, n, pv_coeff ); Node new_theta = theta; if( !pv_coeff.isNull() ){ if( new_theta.isNull() ){ @@ -759,18 +773,15 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b curr_var.pop_back(); is_cv = true; } - success = addInstantiation( subs, vars, coeff, btyp, has_coeff, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var ); + success = addInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var ); if( !success ){ if( is_cv ){ curr_var.push_back( pv ); } - subs.pop_back(); + sf.pop_back( pv, n, pv_coeff ); + ssf.pop_back( pv, n, pv_coeff ); vars.pop_back(); - coeff.pop_back(); btyp.pop_back(); - if( !pv_coeff.isNull() ){ - has_coeff.pop_back(); - } } } if( success ){ @@ -778,33 +789,38 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b }else{ //revert substitution information for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ - subs[it->first] = it->second; + sf.d_subs[it->first] = it->second; } for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ - coeff[it->first] = it->second; + sf.d_coeff[it->first] = it->second; } 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::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< int >& btyp, std::vector< Node >& has_coeff, unsigned j, std::map< Node, Node >& cons ) { - if( j==has_coeff.size() ){ - return addInstantiation( subs, vars, cons ); +bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp, + unsigned j, std::map< Node, Node >& cons ) { + + + if( j==sf.d_has_coeff.size() ){ + return addInstantiation( sf.d_subs, vars, cons ); }else{ - Assert( std::find( vars.begin(), vars.end(), has_coeff[j] )!=vars.end() ); - unsigned index = std::find( vars.begin(), vars.end(), has_coeff[j] )-vars.begin(); - Node prev = subs[index]; - Assert( !coeff[index].isNull() ); - Trace("cbqi-inst-debug") << "Normalize substitution for " << coeff[index] << " * " << vars[index] << " = " << subs[index] << std::endl; + 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(); + 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() ); //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, coeff[index], vars[index] ); - Node eq_rhs = subs[index]; + Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], vars[index] ); + Node eq_rhs = sf.d_subs[index]; Node eq = eq_lhs.eqNode( eq_rhs ); eq = Rewriter::rewrite( eq ); Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; @@ -819,13 +835,13 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec Assert( veq_v==vars[index] ); } } - subs[index] = veq[1]; + sf.d_subs[index] = veq[1]; if( !veq_c.isNull() ){ - subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); + sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl; //intger division rounding up if from a lower bound - if( btyp[index]==1 ){ - subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], + if( 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, NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), @@ -834,13 +850,29 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec ); } } - Trace("cbqi-inst-debug") << "...normalize integers : " << subs[index] << std::endl; - if( addInstantiationCoeff( subs, vars, coeff, btyp, has_coeff, j+1, cons ) ){ + 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( addInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){ return true; } } } - subs[index] = prev; + sf.d_subs[index] = prev; Trace("cbqi-inst-debug") << "...failed." << std::endl; return false; } @@ -887,8 +919,8 @@ Node CegInstantiator::constructInstantiation( Node n, std::map< Node, Node >& su } } -Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) { +Node CegInstantiator::applySubstitution( 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() ); Assert( n==Rewriter::rewrite( n ) ); bool req_coeff = false; @@ -1030,16 +1062,15 @@ bool CegInstantiator::check() { } processAssertions(); for( unsigned r=0; r<2; r++ ){ - std::vector< Node > subs; + SolvedForm sf; + SolvedForm ssf; std::vector< Node > vars; - std::vector< Node > coeff; std::vector< int > btyp; - std::vector< Node > has_coeff; Node theta; std::map< Node, Node > cons; std::vector< Node > curr_var; //try to add an instantiation - if( addInstantiation( subs, vars, coeff, btyp, has_coeff, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ + if( addInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ return true; } } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 2074e0f4b..9b3b15dc5 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -68,24 +68,50 @@ private: private: //for adding instantiations during check void computeProgVars( Node n ); + //solved form, involves substitution with coefficients + class SolvedForm { + public: + std::vector< Node > d_subs; + std::vector< Node > d_coeff; + 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 ){ + d_subs.push_back( n ); + d_coeff.push_back( pv_coeff ); + if( !pv_coeff.isNull() ){ + d_has_coeff.push_back( pv ); + } + } + void pop_back( Node pv, Node n, Node pv_coeff ){ + d_subs.pop_back(); + d_coeff.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 addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< int >& btyp, - std::vector< Node >& has_coeff, Node theta, - unsigned i, unsigned effort, + bool addInstantiation( 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 addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< int >& btyp, - std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort, + bool addInstantiationInc( 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 addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< int >& btyp, - std::vector< Node >& has_coeff, unsigned j, std::map< Node, Node >& cons ); + bool addInstantiationCoeff( SolvedForm& sf, + std::vector< Node >& vars, std::vector< int >& btyp, + unsigned j, std::map< Node, Node >& cons ); bool addInstantiation( 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( Node n, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); - Node getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, + Node applySubstitution( Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) { + return applySubstitution( n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff ); + } + Node applySubstitution( 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 ); + Node getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ); void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); @@ -95,7 +121,7 @@ public: bool check(); //presolve for quantified formula void presolve( Node q ); - //register the counterexample lemma (stored in lems), modify vector + //register the counterexample lemma (stored in lems), modify vector void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); }; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 8958034df..a55dfda84 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -456,114 +456,146 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { } } */ +FullSaturation::FullSaturation( QuantifiersEngine* qe ) : QuantifiersModule( qe ){ -void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ +} + +void FullSaturation::reset_round( Theory::Effort e ) { } -int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ - if( e<5 ){ - return STATUS_UNFINISHED; - }else{ - //first, try from relevant domain - RelevantDomain * rd = d_quantEngine->getRelevantDomain(); - unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; - for( unsigned r=rstart; r<2; r++ ){ - if( rd || r>0 ){ +void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { + if( quant_e==QuantifiersEngine::QEFFORT_LAST_CALL ){ + double clSet = 0; + if( Trace.isOn("fs-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" << std::endl; + } + int addedLemmas = 0; + for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + if( process( q, e ) ){ + //added lemma + addedLemmas++; + } + } + } + if( Trace.isOn("fs-engine") ){ + Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("fs-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl; + } + } +} + +bool FullSaturation::process( Node f, Theory::Effort effort ){ + //first, try from relevant domain + RelevantDomain * rd = d_quantEngine->getRelevantDomain(); + unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; + for( unsigned r=rstart; r<2; r++ ){ + if( rd || r>0 ){ + if( r==0 ){ + Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; + }else{ + Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; + } + rd->compute(); + unsigned final_max_i = 0; + std::vector< unsigned > maxs; + for(unsigned i=0; i Relevant domain instantiate " << f << "..." << std::endl; + ts = rd->getRDomain( f, i )->d_terms.size(); }else{ - Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; + ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size(); } - rd->compute(); - unsigned final_max_i = 0; - std::vector< unsigned > maxs; - for(unsigned i=0; igetRDomain( f, i )->d_terms.size(); - }else{ - ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size(); - } - maxs.push_back( ts ); - Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl; - if( ts>final_max_i ){ - final_max_i = ts; - } + maxs.push_back( ts ); + Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl; + if( ts>final_max_i ){ + final_max_i = ts; } - Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl; + } + Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl; - unsigned max_i = 0; - bool success; - while( max_i<=final_max_i ){ - Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; - std::vector< unsigned > childIndex; - int index = 0; - do { - while( index>=0 && index<(int)f[0].getNumChildren() ){ - if( index==(int)childIndex.size() ){ - childIndex.push_back( -1 ); - }else{ - Assert( index==(int)(childIndex.size())-1 ); - unsigned nv = childIndex[index]+1; - if( options::cbqi() ){ - //skip inst constant nodes - while( nvgetTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ - nv++; - } - } - if( nv childIndex; + int index = 0; + do { + while( index>=0 && index<(int)f[0].getNumChildren() ){ + if( index==(int)childIndex.size() ){ + childIndex.push_back( -1 ); + }else{ + Assert( index==(int)(childIndex.size())-1 ); + unsigned nv = childIndex[index]+1; + if( options::cbqi() ){ + //skip inst constant nodes + while( nvgetTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ + nv++; } } - } - success = index>=0; - if( success ){ - Trace("inst-alg-rd") << "Try instantiation { "; - for( unsigned j=0; j terms; - for( unsigned i=0; igetRDomain( f, i )->d_terms[childIndex[i]] ); - }else{ - terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] ); - } - } - if( d_quantEngine->addInstantiation( f, terms, false ) ){ - Trace("inst-alg-rd") << "Success!" << std::endl; - ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); - return STATUS_UNKNOWN; + if( nv Guess instantiate " << f << "..." << std::endl; - d_guessed[f] = true; - InstMatch m( f ); - if( d_quantEngine->addInstantiation( f, m ) ){ - ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); - return STATUS_UNKNOWN; } + success = index>=0; + if( success ){ + Trace("inst-alg-rd") << "Try instantiation { "; + for( unsigned j=0; j terms; + for( unsigned i=0; igetRDomain( f, i )->d_terms[childIndex[i]] ); + }else{ + terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] ); + } + } + if( d_quantEngine->addInstantiation( f, terms, false ) ){ + Trace("inst-alg-rd") << "Success!" << std::endl; + ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); + return true; + }else{ + index--; + } + } + }while( success ); + max_i++; + } + } + if( r==0 ){ + //complete guess + if( d_guessed.find( f )==d_guessed.end() ){ + Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; + d_guessed[f] = true; + InstMatch m( f ); + if( d_quantEngine->addInstantiation( f, m ) ){ + ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); + return true; } } } - //term enumerator? } - return STATUS_UNKNOWN; + //term enumerator? + return false; +} + +void FullSaturation::registerQuantifier( Node q ) { + +} + +void FullSaturation::assertNode( Node n ) { + } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 02ddd233e..5163653cf 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -105,20 +105,22 @@ public: void addUserNoPattern( Node f, Node pat ); };/* class InstStrategyAutoGenTriggers */ -class InstStrategyFreeVariable : public InstStrategy{ +class FullSaturation : public QuantifiersModule { private: /** guessed instantiations */ std::map< Node, bool > d_guessed; /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e ); + bool process( Node f, Theory::Effort effort ); public: - InstStrategyFreeVariable( QuantifiersEngine* qe ) : - InstStrategy( qe ){} - ~InstStrategyFreeVariable(){} + FullSaturation( QuantifiersEngine* qe ); + ~FullSaturation(){} + void reset_round( Theory::Effort e ); + void check( Theory::Effort e, unsigned quant_e ); + void registerQuantifier( Node q ); + void assertNode( Node n ); /** identify */ - std::string identify() const { return std::string("FreeVariable"); } -};/* class InstStrategyFreeVariable */ + std::string identify() const { return std::string("FullSaturation"); } +};/* class FullSaturation */ } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 2d637e1a0..8f1ef42d8 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -31,14 +31,13 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){ +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){ } InstantiationEngine::~InstantiationEngine() { delete d_i_ag; delete d_isup; - delete d_i_fs; delete d_i_splx; delete d_i_cegqi; } @@ -57,13 +56,7 @@ void InstantiationEngine::finishInit(){ d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine ); d_instStrategies.push_back( d_i_ag ); } - - //full saturation : instantiate from relevant domain, then arbitrary terms - if( options::fullSaturateQuant() ){ - d_i_fs = new InstStrategyFreeVariable( d_quantEngine ); - d_instStrategies.push_back( d_i_fs ); - } - + //counterexample-based quantifier instantiation if( options::cbqi() ){ if( !options::cbqi2() ){ @@ -88,7 +81,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ if( options::cbqi() ){ //check if any cbqi lemma has not been added yet bool addedLemma = false; - for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){ d_added_cbqi_lemma[f] = true; @@ -136,7 +129,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } //if not, proceed to instantiation round //reset the instantiation strategies - for( size_t i=0; iprocessResetInstantiationRound( effort ); } @@ -158,8 +151,8 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ if( e_use>=0 ){ Trace("inst-engine-debug") << "inst-engine : " << q << std::endl; //check each instantiation strategy - for( size_t i=0; iidentify() << " " << e_use << std::endl; int quantStatus = is->process( q, effort, e_use ); Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl; @@ -200,7 +193,7 @@ void InstantiationEngine::reset_round( Theory::Effort e ) { d_cbqi_set_quant_inactive = false; if( options::cbqi() ){ //set inactive the quantified formulas whose CE literals are asserted false - for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + 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( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) && hasAddedCbqiLemma( q ) ){ @@ -236,12 +229,12 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ bool quantActive = false; d_quants.clear(); for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( d_quantEngine->hasOwnership( n, this ) && d_quantEngine->getModel()->isQuantifierActive( n ) ){ - if( !options::cbqi() || !TermDb::hasInstConstAttr(n) ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + if( !options::cbqi() || !TermDb::hasInstConstAttr(q) ){ quantActive = true; } - d_quants.push_back( n ); + d_quants.push_back( q ); } } Trace("inst-engine-debug") << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/"; diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index c789cd3b2..3b7a5f4f8 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -66,8 +66,6 @@ private: InstStrategyUserPatterns* d_isup; /** auto gen triggers; only kept for destructor cleanup */ InstStrategyAutoGenTriggers* d_i_ag; - /** full saturate */ - InstStrategyFreeVariable * d_i_fs; /** simplex (cbqi) */ InstStrategySimplex * d_i_splx; /** generic cegqi */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 752e88c5a..a3a18cf30 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -265,7 +265,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl; - if( !riter.d_incomplete || options::fmfFullSaturate() ){ + if( !riter.d_incomplete ){ int triedLemmas = 0; int addedLemmas = 0; while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index a31fbe6e7..cd5f90a37 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -131,8 +131,6 @@ option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false option fmfInstEngine --fmf-inst-engine bool :default false use instantiation engine in conjunction with finite model finding -option fmfFullSaturate --fmf-full-saturate bool :default false - instantiate with all known ground terms for infinite domain quantifiers when finite model finding option fmfInstGen --fmf-inst-gen bool :default true enable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false @@ -247,6 +245,10 @@ 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 ### local theory extensions options diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a2c6a9ddf..e5b5c4080 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -39,6 +39,7 @@ #include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/fun_def_engine.h" #include "theory/quantifiers/quant_equality_engine.h" +#include "theory/quantifiers/inst_strategy_e_matching.h" using namespace std; using namespace CVC4; @@ -186,7 +187,14 @@ d_presolve(u, true){ }else{ d_uee = NULL; } - + + //full saturation : instantiate from relevant domain, then arbitrary terms + if( options::fullSaturateQuant() ){ + d_fs = new quantifiers::FullSaturation( this ); + d_modules.push_back( d_fs ); + }else{ + d_fs = NULL; + } if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; @@ -228,6 +236,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_lte_part_inst; delete d_fun_def_engine; delete d_uee; + delete d_fs; for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) { delete (*i).second; } @@ -327,7 +336,16 @@ void QuantifiersEngine::check( Theory::Effort e ){ } d_hasAddedLemma = false; - + bool setIncomplete = false; + if( e==Theory::EFFORT_LAST_CALL ){ + //sources of incompleteness + if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){ + Trace("quant-engine-debug") << "Set incomplete due to LTE partial instantiation." << std::endl; + setIncomplete = true; + } + } + bool usedModelBuilder = false; + Trace("quant-engine-debug") << "Quantifiers Engine call to check, level = " << e << std::endl; if( needsCheck ){ Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; @@ -387,12 +405,13 @@ void QuantifiersEngine::check( Theory::Effort e ){ ++(d_statistics.d_instantiation_rounds); } Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl; - for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){ + for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){ bool success = true; //build the model if any module requested it if( needsModelE==quant_e ){ Assert( d_builder!=NULL ); Trace("quant-engine-debug") << "Build model..." << std::endl; + usedModelBuilder = true; d_builder->d_addedLemmas = 0; d_builder->buildModel( d_model, false ); //we are done if model building was unsuccessful @@ -412,10 +431,23 @@ void QuantifiersEngine::check( Theory::Effort e ){ //if we have added one, stop if( d_hasAddedLemma ){ break; - //otherwise, complete the model generation if necessary - }else if( quant_e==QEFFORT_MODEL && needsModelE<=quant_e && options::produceModels() && e==Theory::EFFORT_LAST_CALL ){ - Trace("quant-engine-debug") << "Build completed model..." << std::endl; - d_builder->buildModel( d_model, true ); + }else if( e==Theory::EFFORT_LAST_CALL && quant_e==QEFFORT_MODEL ){ + //if we have a chance not to set incomplete + if( !setIncomplete ){ + setIncomplete = true; + //check if we should set the incomplete flag + for( unsigned i=0; icheckComplete() ){ + Trace("quant-engine-debug") << "Do not set incomplete because " << qm[i]->identify().c_str() << " was complete." << std::endl; + setIncomplete = false; + break; + } + } + } + //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL + if( !setIncomplete ){ + break; + } } } Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl; @@ -432,34 +464,21 @@ void QuantifiersEngine::check( Theory::Effort e ){ }else{ Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl; } + //SAT case if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ - if( options::produceModels() && !d_model->isModelSet() ){ - //use default model builder when no module built the model - Trace("quant-engine-debug") << "Build the model..." << std::endl; - d_te->getModelBuilder()->buildModel( d_model, true ); - Trace("quant-engine-debug") << "Done building the model." << std::endl; - } - bool setInc = false; - if( needsCheck ){ - setInc = true; - for( unsigned i=0; icheckComplete() ){ - Trace("quant-engine-debug") << "Do not set incomplete because " << qm[i]->identify().c_str() << " was complete." << std::endl; - setInc = false; - } - } - }else{ - Trace("quant-engine-debug") << "Do not set incomplete because check wasn't necessary." << std::endl; - } - //check other sources of incompleteness - if( !setInc ){ - if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){ - Trace("quant-engine-debug") << "Set incomplete due to LTE partial instantiation." << std::endl; - setInc = true; + if( options::produceModels() ){ + if( usedModelBuilder ){ + Trace("quant-engine-debug") << "Build completed model..." << std::endl; + d_builder->buildModel( d_model, true ); + }else if( !d_model->isModelSet() ){ + //use default model builder when no module built the model + Trace("quant-engine-debug") << "Build the model..." << std::endl; + d_te->getModelBuilder()->buildModel( d_model, true ); + Trace("quant-engine-debug") << "Done building the model." << std::endl; } } - if( setInc ){ + if( setIncomplete ){ Trace("quant-engine-debug") << "Set incomplete flag." << std::endl; getOutputChannel().setIncomplete(); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 3cdd5bae7..4e3bba501 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -97,6 +97,7 @@ namespace quantifiers { class AlphaEquivalence; class FunDefEngine; class QuantEqualityEngine; + class FullSaturation; }/* CVC4::theory::quantifiers */ namespace inst { @@ -150,11 +151,14 @@ private: quantifiers::FunDefEngine * d_fun_def_engine; /** quantifiers equality engine */ quantifiers::QuantEqualityEngine * d_uee; + /** full saturation */ + quantifiers::FullSaturation * d_fs; public: //effort levels enum { QEFFORT_CONFLICT, QEFFORT_STANDARD, QEFFORT_MODEL, + QEFFORT_LAST_CALL, //none QEFFORT_NONE, }; @@ -244,6 +248,8 @@ public: //modules quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; } /** quantifiers equality engine */ quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; } + /** get full saturation */ + quantifiers::FullSaturation * getFullSaturation() { return d_fs; } private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; -- 2.30.2