summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp7
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.cpp509
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.h23
-rw-r--r--src/theory/quantifiers/quant_util.cpp56
-rw-r--r--src/theory/quantifiers/quant_util.h1
-rw-r--r--src/theory/quantifiers/term_database.cpp8
-rw-r--r--test/regress/regress0/sygus/Makefile.am8
-rw-r--r--test/regress/regress0/sygus/array_search_2.sy11
-rw-r--r--test/regress/regress0/sygus/array_sum_2_5.sy9
-rw-r--r--test/regress/regress0/sygus/max.sy (renamed from test/regress/regress0/sygus/max.sl)2
-rw-r--r--test/regress/regress0/sygus/parity-AIG-d0.sy30
-rw-r--r--test/regress/regress0/sygus/twolets1.sy40
12 files changed, 467 insertions, 237 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] );
+ }
}
}
}
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
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)
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback