diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-26 15:16:15 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-26 15:16:23 +0100 |
commit | 4f5c9dbbd0125294500cf5788cb131b355979fb6 (patch) | |
tree | fd07a862b4ad35111d56bdfa84f17f8c44d45e6c /src | |
parent | 92e4099d9d2b313a521d2a015e604645e24617f4 (diff) |
Robust strategy for single invocation LIA synthesis conjectures. Add regressions.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 509 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 23 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 56 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 8 |
6 files changed, 370 insertions, 234 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index e291dce9d..bcad52087 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -31,7 +31,7 @@ namespace CVC4 { CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){ d_refine_count = 0; - d_ceg_si = NULL; + d_ceg_si = new CegConjectureSingleInv( this ); } void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { @@ -60,8 +60,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } d_syntax_guided = true; if( options::cegqiSingleInv() ){ - d_ceg_si = new CegConjectureSingleInv( qe, q, this ); - d_ceg_si->initialize(); + d_ceg_si->initialize( qe, q ); } }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){ d_syntax_guided = false; @@ -131,7 +130,7 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { } CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ - d_conj = new CegConjecture( d_quantEngine->getSatContext() ); + d_conj = new CegConjecture( qe->getSatContext() ); d_last_inst_si = false; } diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index f9c8e42fd..1a1169578 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -32,8 +32,9 @@ using namespace std; namespace CVC4 { -CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p ) : d_qe( qe ), d_parent( p ), d_quant( q ){ - d_sol = new CegConjectureSingleInvSol( qe ); +CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){ + d_sol = NULL; + d_c_inst_match_trie = NULL; } Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { @@ -58,8 +59,15 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { } } -void CegConjectureSingleInv::initialize() { - Node q = d_quant; +void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { + //initialize data + d_sol = new CegConjectureSingleInvSol( qe ); + d_qe = qe; + d_quant = q; + if( options::incrementalSolving() ){ + d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() ); + } + //process Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl; // conj -> conj* std::map< Node, std::vector< Node > > children; @@ -405,176 +413,306 @@ bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vect } -void CegConjectureSingleInv::check( std::vector< Node >& lems ) { - if( !d_single_inv.isNull() ) { + +void CegConjectureSingleInv::computeProgVars( Node n ){ + if( d_prog_var.find( n )==d_prog_var.end() ){ + d_prog_var[n].clear(); + if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){ + d_prog_var[n][n] = true; + }else if( n.getKind()==SKOLEM && std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )==d_single_inv_arg_sk.end() ){ + d_inelig[n] = true; + return; + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + computeProgVars( n[i] ); + if( d_inelig.find( n[i] )!=d_inelig.end() ){ + d_inelig[n] = true; + return; + } + for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){ + d_prog_var[n][it->first] = true; + } + } + } +} + +bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned i, std::vector< Node >& lems ){ + if( i==d_single_inv_sk.size() ){ + for( unsigned j=0; j<has_coeff.size(); j++ ){ + //unsigned index = std::find( vars.begin(), vars.end(), has_coeff[j] )-vars.begin(); + //Assert( !coeff[index].isNull() ); + //must normalize TODO + return false; + } + + //check if we have already added this instantiation + bool alreadyExists; + if( options::incrementalSolving() ){ + alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() ); + }else{ + alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs ); + } + if( alreadyExists ){ + return false; + }else{ + Trace("cegqi-engine") << " * single invocation: " << std::endl; + for( unsigned j=0; j<vars.size(); j++ ){ + Node v = d_single_inv_map_to_prog[d_single_inv[0][j]]; + Trace("cegqi-engine") << " * " << v; + Trace("cegqi-engine") << " (" << vars[j] << ")"; + Trace("cegqi-engine") << " -> " << subs[j] << std::endl; + } + Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); + lem = Rewriter::rewrite( lem ); + Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; + if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){ + lems.push_back( lem ); + d_lemmas_produced.push_back( lem ); + d_inst.push_back( std::vector< Node >() ); + d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() ); + } + return true; + } + }else{ eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); - Trace("cegqi-engine") << " * single invocation: " << std::endl; - std::vector< Node > subs; - std::map< Node, int > subs_from_model; - std::vector< Node > waiting_to_slv; - for( unsigned i=0; i<d_single_inv_sk.size(); i++ ){ - Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; - Node pv = d_single_inv_sk[i]; - Trace("cegqi-engine") << " * " << v; - Trace("cegqi-engine") << " (" << pv << ")"; - Trace("cegqi-engine") << " -> "; - Node slv; - if( ee->hasTerm( pv ) ){ - Node r = ee->getRepresentative( pv ); - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - bool isWaitingSlv = false; - while( !eqc_i.isFinished() ){ - Node n = *eqc_i; - if( n!=pv ){ - if( slv.isNull() || isWaitingSlv ){ - std::vector< Node > vars; - collectProgVars( n, vars ); - if( slv.isNull() || vars.empty() ){ - // n cannot contain pv - bool isLoop = std::find( vars.begin(), vars.end(), pv )!=vars.end(); - if( !isLoop ){ - for( unsigned j=0; j<vars.size(); j++ ){ - if( std::find( waiting_to_slv.begin(), waiting_to_slv.end(), vars[j] )!=waiting_to_slv.end() ){ - isLoop = true; - break; - } - } - if( !isLoop ){ - slv = n; - isWaitingSlv = !vars.empty(); - } - } + std::map< Node, std::map< Node, bool > > subs_proc; + Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; + Node pv = d_single_inv_sk[i]; + Node pvr; + Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) + + //[1] easy case : pv is in the equivalence class as another term not containing pv + if( ee->hasTerm( pv ) ){ + pvr = ee->getRepresentative( pv ); + eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + if( n!=pv ){ + Trace("cegqi-si-inst-debug") << i << "...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() ){ + Node ns; + bool proc = false; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( n, subs, vars, coeff, has_coeff, 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(); } + }else{ + ns = n; + proc = true; } - } - ++eqc_i; - } - if( isWaitingSlv ){ - Trace("cegqi-engine-debug") << "waiting:"; - waiting_to_slv.push_back( pv ); - } - }else{ - Trace("cegqi-engine-debug") << "N/A:"; - } - if( slv.isNull() ){ - //get model value - Node mv = d_qe->getModel()->getValue( pv ); - subs.push_back( mv ); - subs_from_model[pv] = i; - if( Trace.isOn("cegqi-engine") || Trace.isOn("cegqi-engine-debug") ){ - Trace("cegqi-engine") << "M:" << mv; - } - }else{ - subs.push_back( slv ); - Trace("cegqi-engine") << slv; - } - Trace("cegqi-engine") << std::endl; - } - for( int i=(int)(waiting_to_slv.size()-1); i>=0; --i ){ - int index = d_single_inv_sk_index[waiting_to_slv[i]]; - Trace("cegqi-engine-debug") << "Go back and solve " << d_single_inv_sk[index] << std::endl; - Trace("cegqi-engine-debug") << "Substitute " << subs[index] << " to "; - subs[index] = applyProgVarSubstitution( subs[index], subs_from_model, subs ); - Trace("cegqi-engine-debug") << subs[index] << std::endl; - } - //try to improve substitutions : look for terms that contain terms in question - bool success; - do{ - success = false; - if( !subs_from_model.empty() ){ - std::map< int, std::vector< Node > > cls_terms; - std::map< Node, std::vector< int > > vars; - std::map< Node, std::map< int, std::vector< Node > > > node_eqc; - std::map< Node, Node > node_rep; - int vn_max = -1; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - Node r = *eqcs_i; - TypeNode rtn = r.getType(); - if( rtn.isInteger() || rtn.isReal() ){ - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( !eqc_i.isFinished() ){ - Node n = *eqc_i; - if( classifyTerm( n, subs_from_model, vars[n] ) ){ - Trace("cegqi-si-debug") << "Term " << n << " in eqc " << r << " with " << vars[n].size() << " unset variables." << std::endl; - int vs = (int)vars[n].size(); - cls_terms[vs].push_back( n ); - node_eqc[r][vs].push_back( n ); - node_rep[n] = r; - vn_max = vs>vn_max ? vs : vn_max; + if( proc ){ + //try the substitution + subs_proc[ns][pv_coeff] = true; + if( addInstantiationInc( ns, pv, pv_coeff, subs, vars, coeff, has_coeff, i, lems ) ){ + return true; } - ++eqc_i; } } - ++eqcs_i; } - // will try processed, then unprocessed - for( unsigned p=0; p<2; p++ ){ - Trace("cegqi-si-debug") << "Try " << ( p==0 ? "un" : "" ) << "processed equalities..." << std::endl; - //prefer smallest # variables first on LHS - for( int vn = 1; vn<=vn_max; vn++ ){ - Trace("cegqi-si-debug") << " Having " << vn << " variables on LHS..." << std::endl; - for( unsigned i=0; i<cls_terms[vn].size(); i++ ){ - Node lhs = cls_terms[vn][i]; - Node r = node_rep[lhs]; - //prefer smallest # variables on RHS - for( int vnc = 0; vnc<=vn_max; vnc++ ){ - Trace("cegqi-si-debug") << " Having " << vnc << " variables on RHS..." << std::endl; - for( unsigned j=0; j<node_eqc[r][vnc].size(); j++ ){ - Node rhs = node_eqc[r][vnc][j]; - if( lhs!=rhs ){ - Trace("cegqi-si-debug") << " try " << lhs << " " << rhs << std::endl; - //for each variable in LHS - for( unsigned k=0; k<vars[lhs].size(); k++ ){ - int v = vars[lhs][k]; - Trace("cegqi-si-debug") << " variable " << v << std::endl; - Assert( (int)vars[lhs].size()==vn ); - //check if already processed - bool proc = d_eq_processed[lhs][rhs].find( v )!=d_eq_processed[lhs][rhs].end(); - if( proc==(p==1) ){ - if( solveEquality( lhs, rhs, v, subs_from_model, subs ) ){ - Trace("cegqi-si-debug") << "Success, set " << lhs << " " << rhs << " " << v << std::endl; - d_eq_processed[lhs][rhs][v] = true; - success = true; - break; + ++eqc_i; + } + } + + //[2] : we can solve an equality for pv + ///iterate over equivalence classes to find cases where we can solve for the variable + if( pv.getType().isInteger() || pv.getType().isReal() ){ + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + Node r = *eqcs_i; + TypeNode rtn = r.getType(); + if( rtn.isInteger() || rtn.isReal() ){ + std::vector< Node > lhs; + std::vector< bool > lhs_v; + std::vector< Node > lhs_coeff; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + computeProgVars( n ); + //must be an eligible term + if( d_inelig.find( n )==d_inelig.end() ){ + Node ns; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff ); + if( !ns.isNull() ){ + computeProgVars( ns ); + } + }else{ + ns = n; + pv_coeff = Node::null(); + } + if( !ns.isNull() ){ + bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); + for( unsigned j=0; j<lhs.size(); j++ ){ + //if this term or the another has pv in it, try to solve for it + if( hasVar || lhs_v[j] ){ + Trace("cegqi-si-inst-debug") << i << "...try based on equality " << lhs[j] << " " << ns << std::endl; + Node eq_lhs = lhs[j]; + Node eq_rhs = ns; + //make the same coefficient + if( pv_coeff!=lhs_coeff[j] ){ + if( !pv_coeff.isNull() ){ + Trace("cegqi-si-inst-debug") << "...mult lhs by " << pv_coeff << std::endl; + eq_lhs = NodeManager::currentNM()->mkNode( MULT, pv_coeff, eq_lhs ); + eq_lhs = Rewriter::rewrite( eq_lhs ); + } + if( !lhs_coeff[j].isNull() ){ + Trace("cegqi-si-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; + eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); + eq_rhs = Rewriter::rewrite( eq_rhs ); + } + } + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + if( Trace.isOn("cegqi-si-inst-debug") ){ + Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); + Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; + } + Node veq; + if( QuantArith::isolateEqCoeff( pv, msum, veq ) ){ + Trace("cegqi-si-inst-debug") << "...isolated equality " << veq << "." << std::endl; + Node veq_c; + if( veq[0]!=v ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==v ); + } + } + if( veq_c.isNull() ){ //TODO + computeProgVars( veq[1] ); + subs_proc[veq[1]][veq_c] = true; + if( addInstantiationInc( veq[1], pv, veq_c, subs, vars, coeff, has_coeff, i, lems ) ){ + return true; + } } } } - if( success ){ break; } } } - if( success ){ break; } + lhs.push_back( ns ); + lhs_v.push_back( hasVar ); + lhs_coeff.push_back( pv_coeff ); } - if( success ){ break; } } - if( success ){ break; } + ++eqc_i; } - if( success ){ break; } } + ++eqcs_i; } - }while( !subs_from_model.empty() && success ); + } - if( Trace.isOn("cegqi-si-warn") ){ - if( !subs_from_model.empty() ){ - Trace("cegqi-si-warn") << "Warning : could not find values for : " << std::endl; - for( std::map< Node, int >::iterator it = subs_from_model.begin(); it != subs_from_model.end(); ++it ){ - Trace("cegqi-si-warn") << " " << it->first << std::endl; - } + //[3] directly look at assertions + //TODO + + + //[4] resort to using value in model + Node mv = d_qe->getModel()->getValue( pv ); + Trace("cegqi-si-inst-debug") << i << "...try model value " << mv << std::endl; + return addInstantiationInc( mv, pv, pv_coeff, subs, vars, coeff, has_coeff, i, lems ); + } +} + + +bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned i, std::vector< Node >& lems ) { + //substitute into previous substitutions, when applicable + std::map< int, Node > prev; + for( unsigned j=0; j<subs.size(); j++ ){ + Assert( d_prog_var.find( subs[j] )!=d_prog_var.end() ); + if( d_prog_var[subs[j]].find( pv )!=d_prog_var[subs[j]].end() ){ + prev[j] = subs[j]; + TNode tv = pv; + TNode ts = n; + subs[j] = subs[j].substitute( tv, ts ); + if( subs[j]!=prev[j] ){ + subs[j] = Rewriter::rewrite( subs[j] ); } } - - Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); - lem = Rewriter::rewrite( lem ); - Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; - if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){ - lems.push_back( lem ); - d_lemmas_produced.push_back( lem ); - d_inst.push_back( std::vector< Node >() ); - d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() ); + } + subs.push_back( n ); + vars.push_back( pv ); + coeff.push_back( pv_coeff ); + if( !pv_coeff.isNull() ){ + has_coeff.push_back( pv ); + } + Trace("cegqi-si-inst-debug") << i << ": "; + if( !pv_coeff.isNull() ){ + Trace("cegqi-si-inst-debug") << "*" << pv_coeff; + } + Trace("cegqi-si-inst-debug") << pv << " -> " << n << std::endl; + if( addInstantiation( subs, vars, coeff, has_coeff, i+1, lems ) ){ + return true; + }else{ + subs.pop_back(); + vars.pop_back(); + coeff.pop_back(); + if( !pv_coeff.isNull() ){ + has_coeff.pop_back(); + } + //revert substitution + for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); it++ ){ + subs[it->first] = it->second; + } + return false; + } +} + +Node CegConjectureSingleInv::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 ) { + Assert( d_prog_var.find( n )!=d_prog_var.end() ); + bool req_coeff = false; + if( !has_coeff.empty() ){ + for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){ + if( std::find( has_coeff.begin(), has_coeff.end(), it->first )!=has_coeff.end() ){ + req_coeff = true; + break; + } + } + } + if( !req_coeff ){ + Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + if( n!=nret ){ + Rewriter::rewrite( nret ); + } + return nret; + }else{ + if( try_coeff ){ + //must convert to monomial representation + std::map< Node, Node > msum; + if( QuantArith::getMonomialSum( n, msum ) ){ + //TODO + + } } + // failed to apply the substitution + return Node::null(); } } +void CegConjectureSingleInv::check( std::vector< Node >& lems ) { + if( !d_single_inv.isNull() ) { + std::vector< Node > subs; + std::vector< Node > vars; + std::vector< Node > coeff; + std::vector< Node > has_coeff; + //try to add an instantiation + if( !addInstantiation( subs, vars, coeff, has_coeff, 0, lems ) ){ + Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + } + } +} + +/* bool CegConjectureSingleInv::solveEquality( Node lhs, Node rhs, int v, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) { Trace("cegqi-si-debug") << "Can possibly set " << d_single_inv_sk[v] << " based on " << lhs << " = " << rhs << std::endl; subs_from_model.erase( d_single_inv_sk[v] ); @@ -606,75 +744,7 @@ bool CegConjectureSingleInv::solveEquality( Node lhs, Node rhs, int v, std::map< subs[v] = prev_subs_v; return false; } - -Node CegConjectureSingleInv::applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) { - std::vector< Node > vars; - collectProgVars( n, vars ); - if( !vars.empty() ){ - std::vector< Node > ssubs; - //get substitution - for( unsigned i=0; i<vars.size(); i++ ){ - Assert( d_single_inv_sk_index.find( vars[i] )!=d_single_inv_sk_index.end() ); - int index = d_single_inv_sk_index[vars[i]]; - ssubs.push_back( subs[index] ); - //it is now constrained - if( subs_from_model.find( vars[i] )!=subs_from_model.end() ){ - subs_from_model.erase( vars[i] ); - } - } - n = n.substitute( vars.begin(), vars.end(), ssubs.begin(), ssubs.end() ); - n = Rewriter::rewrite( n ); - return n; - }else{ - return n; - } -} - -bool CegConjectureSingleInv::classifyTerm( Node n, std::map< Node, int >& subs_from_model, std::vector< int >& vars ) { - if( n.getKind()==SKOLEM ){ - std::map< Node, int >::iterator it = subs_from_model.find( n ); - if( it!=subs_from_model.end() ){ - if( std::find( vars.begin(), vars.end(), it->second )==vars.end() ){ - vars.push_back( it->second ); - } - return true; - }else{ - // if it is symbolic argument, we are also fine - if( std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end() ){ - return true; - }else{ - //if it is another program, we are also fine - if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){ - return true; - }else{ - return false; - } - } - } - }else{ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( !classifyTerm( n[i], subs_from_model, vars ) ){ - return false; - } - } - return true; - } -} - -void CegConjectureSingleInv::collectProgVars( Node n, std::vector< Node >& vars ) { - if( n.getKind()==SKOLEM ){ - if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){ - if( std::find( vars.begin(), vars.end(), n )==vars.end() ){ - vars.push_back( n ); - } - } - }else{ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - collectProgVars( n[i], vars ); - } - } -} - +*/ Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) { Assert( index<d_inst.size() ); @@ -691,6 +761,7 @@ Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) { } Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){ + Assert( d_sol!=NULL ); Assert( !d_lemmas_produced.empty() ); const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); Node varList = Node::fromExpr( dt.getSygusVarList() ); diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index a1f9d5a1f..f8edfacf0 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -43,14 +43,8 @@ private: bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status ); Node constructSolution( unsigned i, unsigned index ); - bool classifyTerm( Node n, std::map< Node, int >& subs_from_model, std::vector< int >& vars ); - void collectProgVars( Node n, std::vector< Node >& vars ); - Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ); - //equalities processed - std::map< Node, std::map< Node, std::map< int, bool > > > d_eq_processed; - bool solveEquality( Node lhs, Node rhs, int v, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ); public: - CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p ); + CegConjectureSingleInv( CegConjecture * p ); // original conjecture Node d_quant; // single invocation version of quant @@ -70,16 +64,29 @@ public: //lemmas produced std::vector< Node > d_lemmas_produced; std::vector< std::vector< Node > > d_inst; + inst::InstMatchTrie d_inst_match_trie; + inst::CDInstMatchTrie * d_c_inst_match_trie; // solution std::vector< Node > d_varList; Node d_orig_solution; Node d_solution; Node d_sygus_solution; + //program variable contains cache + std::map< Node, std::map< Node, bool > > d_prog_var; + std::map< Node, bool > d_inelig; + + void computeProgVars( Node n ); + bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned i, std::vector< Node >& lems ); + bool addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned i, std::vector< Node >& lems ); + 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 ); public: //get the single invocation lemma Node getSingleInvLemma( Node guard ); //initialize - void initialize(); + void initialize( QuantifiersEngine * qe, Node q ); //check void check( std::vector< Node >& lems ); //get solution diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index ccc4cfd15..1d3bf7c2a 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -68,6 +68,22 @@ bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) { msum[Node::null()] = negate( lit[1] ); } return true; + }else{ + //subtract the other side + std::map< Node, Node > msum2; + if( getMonomialSum( lit[1], msum2 ) ){ + for( std::map< Node, Node >::iterator it = msum2.begin(); it != msum2.end(); ++it ){ + std::map< Node, Node >::iterator it2 = msum.find( it->first ); + if( it2!=msum.end() ){ + Node r = NodeManager::currentNM()->mkNode( MINUS, it2->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it2->second, + it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second ); + msum[it->first] = Rewriter::rewrite( r ); + }else{ + msum[it->first] = negate( it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second ); + } + } + return true; + } } } } @@ -100,7 +116,7 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind if( r.isOne() ){ veq = negate(veq); }else{ - //TODO : lcd computation + //TODO : gcd computation return false; } } @@ -114,6 +130,44 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind } } +bool QuantArith::isolateEqCoeff( Node v, std::map< Node, Node >& msum, Node & veq ) { + std::map< Node, Node >::iterator itv = msum.find( v ); + if( itv!=msum.end() ){ + std::vector< Node > children; + Rational r = itv->second.isNull() ? Rational(1) : itv->second.getConst<Rational>(); + if ( r.sgn()!=0 ){ + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( it->first!=v ){ + Node m; + if( !it->first.isNull() ){ + if ( !it->second.isNull() ){ + m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first ); + }else{ + m = it->first; + } + }else{ + m = it->second; + } + children.push_back(m); + } + } + veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : + (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); + if( r.sgn()==1 ){ + veq = negate(veq); + } + veq = Rewriter::rewrite( veq ); + Node vc = v; + if( !r.isOne() && !r.isNegativeOne() ){ + vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc ); + } + veq = NodeManager::currentNM()->mkNode( EQUAL, vc, veq ); + return true; + } + } + return false; +} + Node QuantArith::negate( Node t ) { Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t ); tt = Rewriter::rewrite( tt ); diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index f0dfb1ed6..eebf87dc0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -37,6 +37,7 @@ public: static bool getMonomialSum( Node n, std::map< Node, Node >& msum ); static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum ); static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ); + static bool isolateEqCoeff( Node v, std::map< Node, Node >& msum, Node & veq ); static Node negate( Node t ); static Node offset( Node t, int i ); static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 08c8a7e3e..2e2007c0a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1957,7 +1957,9 @@ Node TermDbSygus::minimizeBuiltinTerm( Node n ) { mon[ro].push_back( nc ); changed = true; }else{ - mon[r].push_back( n[r][i] ); + if( !n[r][i].isConst() || !n[r][i].getConst<Rational>().isZero() ){ + mon[r].push_back( n[r][i] ); + } } } }else{ @@ -1965,7 +1967,9 @@ Node TermDbSygus::minimizeBuiltinTerm( Node n ) { mon[ro].push_back( nc ); changed = true; }else{ - mon[r].push_back( n[r] ); + if( !n[r].isConst() || !n[r].getConst<Rational>().isZero() ){ + mon[r].push_back( n[r] ); + } } } } |