From 4f5c9dbbd0125294500cf5788cb131b355979fb6 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 26 Feb 2015 15:16:15 +0100 Subject: [PATCH] Robust strategy for single invocation LIA synthesis conjectures. Add regressions. --- .../quantifiers/ce_guided_instantiation.cpp | 7 +- .../quantifiers/ce_guided_single_inv.cpp | 509 ++++++++++-------- src/theory/quantifiers/ce_guided_single_inv.h | 23 +- src/theory/quantifiers/quant_util.cpp | 56 +- src/theory/quantifiers/quant_util.h | 1 + src/theory/quantifiers/term_database.cpp | 8 +- test/regress/regress0/sygus/Makefile.am | 8 +- test/regress/regress0/sygus/array_search_2.sy | 11 + test/regress/regress0/sygus/array_sum_2_5.sy | 9 + .../regress/regress0/sygus/{max.sl => max.sy} | 2 +- test/regress/regress0/sygus/parity-AIG-d0.sy | 30 ++ test/regress/regress0/sygus/twolets1.sy | 40 ++ 12 files changed, 467 insertions(+), 237 deletions(-) create mode 100644 test/regress/regress0/sygus/array_search_2.sy create mode 100644 test/regress/regress0/sygus/array_sum_2_5.sy rename test/regress/regress0/sygus/{max.sl => max.sy} (97%) create mode 100644 test/regress/regress0/sygus/parity-AIG-d0.sy create mode 100644 test/regress/regress0/sygus/twolets1.sy 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::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; jaddInstMatch( 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 " << 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 "; - 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 > 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 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; jmkNode( 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() ); - 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& 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& 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& 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(); + 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().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().isZero() ){ + mon[r].push_back( n[r] ); + } } } } diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index b5ea8b476..ef65ead1f 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -23,11 +23,15 @@ TESTS = hd-01-d1-prog.sy \ commutative.sy \ constant.sy \ multi-fun-polynomial2.sy \ - unbdd_inv_gen_winf1.sy + unbdd_inv_gen_winf1.sy \ + max.sy \ + array_sum_2_5.sy \ + parity-AIG-d0.sy \ + twolets1.sy \ + array_search_2.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ - max.sl \ max.smt2 \ sygus-uf.sl diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy new file mode 100644 index 000000000..5d8cd8752 --- /dev/null +++ b/test/regress/regress0/sygus/array_search_2.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) +(declare-var x1 Int) +(declare-var x2 Int) +(declare-var k Int) +(constraint (=> (< x1 x2) (=> (< k x1) (= (findIdx x1 x2 k) 0)))) +(constraint (=> (< x1 x2) (=> (> k x2) (= (findIdx x1 x2 k) 2)))) +(constraint (=> (< x1 x2) (=> (and (> k x1) (< k x2)) (= (findIdx x1 x2 k) 1)))) +(check-synth) diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy new file mode 100644 index 000000000..48b5c8a4d --- /dev/null +++ b/test/regress/regress0/sygus/array_sum_2_5.sy @@ -0,0 +1,9 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) +(declare-var x1 Int) +(declare-var x2 Int) +(constraint (=> (> (+ x1 x2) 5) (= (findSum x1 x2 ) (+ x1 x2)))) +(constraint (=> (<= (+ x1 x2) 5) (= (findSum x1 x2 ) 0))) +(check-synth) diff --git a/test/regress/regress0/sygus/max.sl b/test/regress/regress0/sygus/max.sy similarity index 97% rename from test/regress/regress0/sygus/max.sl rename to test/regress/regress0/sygus/max.sy index fdd925196..4fc515353 100644 --- a/test/regress/regress0/sygus/max.sl +++ b/test/regress/regress0/sygus/max.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi-si (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy new file mode 100644 index 000000000..c4fbd1c17 --- /dev/null +++ b/test/regress/regress0/sygus/parity-AIG-d0.sy @@ -0,0 +1,30 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic BV) + +(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + (xor (not (xor a b)) (not (xor c d)))) + +(synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + ((Start Bool ((and Start Start) (not Start) a b c d)))) + +(declare-var a Bool) +(declare-var b Bool) +(declare-var c Bool) +(declare-var d Bool) + +(constraint + (= (parity a b c d) + (and (AIG a b c d) + (not (and (and (not (and a b)) (not (and (not a) (not b)))) + (and (not (and (not c) (not d))) (not (and c d)))))))) + + +(check-synth) + +; Solution: +;(define-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool +;(not +; (and +; (and (not (and (not a) b)) (not (and d (not c)))) +; (and (not (and (not b) a)) (not (and (not d) c)))))) \ No newline at end of file diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy new file mode 100644 index 000000000..24b0f2c09 --- /dev/null +++ b/test/regress/regress0/sygus/twolets1.sy @@ -0,0 +1,40 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) + +;; f1 is x plus 2 ;; f2 is 2x plus 5 + +(define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z)) + +(synth-fun f1 ((x Int)) Int + ( + (Start Int ( + (let0 Intx CInt CInt) + ) + ) + (Intx Int (x)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) + +(synth-fun f2 ((x Int)) Int + ( + (Start Int (x + (let0 Intx Start CInt) + ) + ) + (Intx Int (x)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) +) + + +(declare-var x Int) + +(constraint (= (+ (f1 x)(f2 x)) (+ (+ x x) (+ x 8)))) +(constraint (= (- (f2 x)(f1 x)) (+ x 2))) + +(check-synth) + -- 2.30.2