From 7f43bd304b3d6bede36a777ee85ab68fab35d742 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 25 Nov 2015 18:19:57 +0100 Subject: [PATCH] Infrastructure for partially single invocation properties. Bug fix for unconstrained functions in sygus solver. --- .../quantifiers/ce_guided_single_inv.cpp | 500 ++++++++++++++++-- src/theory/quantifiers/ce_guided_single_inv.h | 52 +- src/theory/quantifiers/options | 2 + src/theory/quantifiers/quant_util.cpp | 54 +- src/theory/quantifiers/quant_util.h | 2 +- src/theory/quantifiers/term_database.cpp | 65 +++ src/theory/quantifiers/term_database.h | 16 +- test/regress/regress0/sygus/Makefile.am | 3 +- test/regress/regress0/sygus/no-mention.sy | 15 + 9 files changed, 624 insertions(+), 85 deletions(-) create mode 100644 test/regress/regress0/sygus/no-mention.sy diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 19cf9b008..914c0614f 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -57,6 +57,12 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje d_cinst = new CegInstantiator( qe, cosi, false, false ); d_sol = new CegConjectureSingleInvSol( qe ); + + if( options::cegqiSingleInvPartial() ){ + d_sip = new SingleInvocationPartition; + }else{ + d_sip = NULL; + } } void CegConjectureSingleInv::getSingleInvLemma( Node guard, std::vector< Node >& lems ) { @@ -109,6 +115,88 @@ void CegConjectureSingleInv::initialize( Node q ) { } } } + if( options::cegqiSingleInvPartial() ){ + Node qq = q[1]; + if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){ + qq = q[1][0][1]; + }else{ + qq = TermDb::simpleNegate( qq ); + } + //remove the deep embedding + std::map< Node, Node > visited; + std::vector< TypeNode > types; + std::vector< Node > order_vars; + int type_valid = 0; + qq = removeDeepEmbedding( qq, progs, types, type_valid, visited ); + Trace("cegqi-si-debug") << "- Remove deep embedding, got : " << qq << ", type valid = " << type_valid << std::endl; + bool singleInvocation = true; + if( type_valid==0 ){ + //process the single invocation-ness of the property + d_sip->init( types ); + d_sip->process( qq ); + Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl; + d_sip->debugPrint( "cegqi-si" ); + //map from program to bound variables + for( unsigned j=0; j::iterator it_nsi = d_nsi_op_map.find( prog ); + if( it_nsi!=d_nsi_op_map.end() ){ + Node op = it_nsi->second; + std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( op ); + if( it_fov!=d_sip->d_func_fo_var.end() ){ + Node pv = it_fov->second; + d_single_inv_map[prog] = pv; + d_single_inv_map_to_prog[pv] = prog; + Assert( d_sip->d_func_inv.find( op )!=d_sip->d_func_inv.end() ); + Node inv = d_sip->d_func_inv[op]; + d_single_inv_app_map[prog] = inv; + Trace("cegqi-si") << " " << pv << ", " << inv << " is associated with program " << prog << std::endl; + d_prog_to_sol_index[prog] = order_vars.size(); + order_vars.push_back( pv ); + } + }else{ + //does not mention the function + } + } + //check if it is single invocation + if( !d_sip->d_conjuncts[1].empty() ){ + singleInvocation = false; + //TODO if we are doing invariant templates, then construct the template + }else{ + //we are fully single invocation + } + }else{ + Trace("cegqi-si") << "...property is not single invocation, involves functions with different argument sorts." << std::endl; + singleInvocation = false; + } + if( singleInvocation ){ + d_single_inv = d_sip->getSingleInvocation(); + d_single_inv = TermDb::simpleNegate( d_single_inv ); + if( !order_vars.empty() ){ + Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, order_vars ); + d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv ); + } + //now, introduce the skolems + for( unsigned i=0; id_si_vars.size(); i++ ){ + Node v = NodeManager::currentNM()->mkSkolem( "a", d_sip->d_si_vars[i].getType(), "single invocation arg" ); + d_single_inv_arg_sk.push_back( v ); + } + d_single_inv = d_single_inv.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() ); + Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv << std::endl; + if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){ + //just invoke the presolve now + d_cinst->presolve( d_single_inv ); + } + }else{ + Trace("cegqi-si") << "Formula is not single invocation." << std::endl; + if( options::cegqiSingleInvAbort() ){ + Notice() << "Property is not single invocation." << std::endl; + exit( 0 ); + } + } + return; + } + //collect information about conjunctions bool singleInvocation = false; bool invExtractPrePost = false; @@ -153,7 +241,7 @@ void CegConjectureSingleInv::initialize( Node q ) { } } if( singleInvocation || invExtractPrePost ){ - //no value in extracting pre/post if we are single invocation + //no value in extracting pre/post if we are (partially) single invocation if( singleInvocation ){ invExtractPrePost = false; } @@ -174,6 +262,7 @@ void CegConjectureSingleInv::initialize( Node q ) { Node pv = NodeManager::currentNM()->mkBoundVar( ss.str(), inv.getType() ); d_single_inv_map[prog] = pv; d_single_inv_map_to_prog[pv] = prog; + d_prog_to_sol_index[prog] = pbvs.size(); pbvs.push_back( pv ); Trace("cegqi-si-debug2") << "Make variable " << pv << " for " << prog << std::endl; for( unsigned k=1; k var for " << prog << " : " << d_single_inv_map[prog] << std::endl; + Trace("cegqi-si-debug2") << "subs : " << inv << " -> (var for " << prog << ") : " << d_single_inv_map[prog] << std::endl; } } if( singleInvocation ){ @@ -417,11 +506,9 @@ void CegConjectureSingleInv::initialize( Node q ) { } if( singleInvocation ){ - Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); - if( pbvl.isNull() ){ - d_single_inv = bd; - }else{ - d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + d_single_inv = conjuncts.empty() ? d_qe->getTermDatabase()->d_true : ( conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ) ); + if( !pbvl.isNull() ){ + d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv ); } Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; /* @@ -483,18 +570,14 @@ bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, if( hasPol ){ if( n.getKind()==NOT ){ return getVariableEliminationTerm( !pol, true, v, n[0], s, status ); - }else if( pol && n.getKind()==EQUAL ){ - for( unsigned r=0; r<2; r++ ){ - if( n[r]==v ){ - status = 1; - Node ss = n[r==0 ? 1 : 0]; - if( s.isNull() ){ - s = ss; - } - return ss==s; + }else if( pol && ( n.getKind()==EQUAL || n.getKind()==IFF ) ){ + Node ss = QuantArith::solveEqualityFor( n, v ); + if( !ss.isNull() ){ + if( s.isNull() ){ + s = ss; } + return ss==s; } - //did not match, now see if it contains v }else if( ( n.getKind()==OR && !pol ) || ( n.getKind()==AND && pol ) ){ for( unsigned i=0; i& progs, std::vector< TypeNode >& types, int& type_valid, + std::map< Node, Node >& visited ) { + std::map< Node, Node >::iterator itv = visited.find( n ); + if( itv!=visited.end() ){ + return itv->second; + }else{ + std::vector< Node > children; + bool childChanged = false; + for( unsigned i=0; i0 ); + if( std::find( progs.begin(), progs.end(), n[0] )!=progs.end() ){ + std::map< Node, Node >::iterator it = d_nsi_op_map.find( n[0] ); + Node op; + if( it==d_nsi_op_map.end() ){ + bool checkTypes = !types.empty(); + std::vector< TypeNode > argTypes; + for( unsigned j=1; j=types.size()+1 || tn!=types[j-1] ){ + type_valid = -1; + } + }else{ + types.push_back( tn ); + } + } + TypeNode ft = argTypes.empty() ? n.getType() : NodeManager::currentNM()->mkFunctionType( argTypes, n.getType() ); + std::stringstream ss2; + ss2 << "O_" << n[0]; + op = NodeManager::currentNM()->mkSkolem( ss2.str(), ft, "was created for non-single invocation reasoning" ); + d_nsi_op_map[n[0]] = op; + Trace("cegqi-si-debug2") << "Make operator " << op << " for " << n[0] << std::endl; + }else{ + op = it->second; + } + children[0] = d_nsi_op_map[n[0]]; + ret = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + } + } + if( ret.isNull() ){ + ret = n; + if( childChanged ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), n.getOperator() ); + } + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + } + visited[n] = ret; + return ret; + } +} + bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children, std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) { @@ -755,42 +898,81 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); Node varList = Node::fromExpr( dt.getSygusVarList() ); Node prog = d_quant[0][sol_index]; - Node prog_app = d_single_inv_app_map[prog]; - //get variables std::vector< Node > vars; - Trace("csi-sol") << "Get solution for " << prog << ", which is applied as " << prog_app << std::endl; - Assert( prog_app.getNumChildren()==varList.getNumChildren()+1 ); - d_varList.clear(); - d_sol->d_varList.clear(); - for( unsigned i=1; imkConst(BitVector(1u, 1u)); - vars.push_back( prog_app[i].eqNode( c ) ); + bool success = true; + if( options::cegqiSingleInvPartial() ){ + Trace("csi-sol") << "Get solution for " << prog << ", with skolems : "; + if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){ + success = false; }else{ - vars.push_back( prog_app[i] ); + sol_index = d_prog_to_sol_index[prog]; + d_varList.clear(); + d_sol->d_varList.clear(); + Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() ); + for( unsigned i=0; imkConst(BitVector(1u, 1u)); + vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) ); + }else{ + vars.push_back( d_single_inv_arg_sk[i] ); + } + d_varList.push_back( varList[i] ); + d_sol->d_varList.push_back( varList[i] ); + } + } + Trace("csi-sol") << std::endl; + }else{ + Node prog_app = d_single_inv_app_map[prog]; + //get variables + Trace("csi-sol") << "Get solution for " << prog << ", which is applied as " << prog_app << std::endl; + if( prog_app.isNull() ){ + Assert( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ); + success = false; + }else{ + Assert( d_prog_to_sol_index.find( prog )!=d_prog_to_sol_index.end() ); + Assert( prog_app.getNumChildren()==varList.getNumChildren()+1 ); + sol_index = d_prog_to_sol_index[prog]; + d_varList.clear(); + d_sol->d_varList.clear(); + for( unsigned i=1; imkConst(BitVector(1u, 1u)); + vars.push_back( prog_app[i].eqNode( c ) ); + }else{ + vars.push_back( prog_app[i] ); + } + d_varList.push_back( varList[i-1] ); + d_sol->d_varList.push_back( varList[i-1] ); + } } - d_varList.push_back( varList[i-1] ); - d_sol->d_varList.push_back( varList[i-1] ); } //construct the solution - Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl; - Assert( d_lemmas_produced.size()==d_inst.size() ); - std::vector< unsigned > indices; - for( unsigned i=0; i indices; + for( unsigned i=0; igetTermDatabase()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 ); + } //simplify the solution Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl; @@ -864,4 +1046,226 @@ void CegConjectureSingleInv::preregisterConjecture( Node q ) { d_orig_conjecture = q; } +void SingleInvocationPartition::init( std::vector< TypeNode >& typs ){ + Assert( d_arg_types.empty() ); + Assert( d_si_vars.empty() ); + d_arg_types.insert( d_arg_types.end(), typs.begin(), typs.end() ); + for( unsigned j=0; jmkBoundVar( d_arg_types[j] ); + d_si_vars.push_back( si_v ); + } +} + + +void SingleInvocationPartition::process( Node n ) { + Assert( d_si_vars.size()==d_arg_types.size() ); + Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl; + Trace("si-prt") << "Get conjuncts..." << std::endl; + std::vector< Node > conj; + if( collectConjuncts( n, true, conj ) ){ + Trace("si-prt") << "...success." << std::endl; + for( unsigned i=0; i si_terms; + std::vector< Node > si_subs; + Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl; + //do DER on conjunct + Node cr = TermDb::getQuantSimplify( conj[i] ); + Trace("si-prt-debug") << "...rewritten to " << cr << std::endl; + std::map< Node, bool > visited; + // functions to arguments + std::vector< Node > args; + std::vector< Node > terms; + std::vector< Node > subs; + bool singleInvocation = true; + if( processConjunct( cr, visited, args, terms, subs ) ){ + for( unsigned j=0; j subs_map; + std::map< Node, Node > subs_map_rev; + std::vector< Node > funcs; + //normalize the invocations + if( !terms.empty() ){ + cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + } + std::vector< Node > children; + children.push_back( cr ); + terms.clear(); + subs.clear(); + Trace("si-prt") << "...single invocation, with arguments: " << std::endl; + for( unsigned j=0; jmkNode( OR, children ); + cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl; + //now must check if it has other bound variables + std::vector< Node > bvs; + TermDb::getBoundVars( cr, bvs ); + if( bvs.size()>d_si_vars.size() ){ + Trace("si-prt") << "...not ground single invocation." << std::endl; + singleInvocation = false; + }else{ + Trace("si-prt") << "...ground single invocation : success." << std::endl; + } + }else{ + Trace("si-prt") << "...not single invocation." << std::endl; + singleInvocation = false; + } + Trace("si-prt") << "..... got si=" << singleInvocation << ", result : " << cr << std::endl; + d_conjuncts[2].push_back( cr ); + if( singleInvocation ){ + //replace with single invocation formulation + cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end() ); + Trace("si-prt") << "..... si version=" << cr << std::endl; + d_conjuncts[0].push_back( cr ); + }else{ + d_conjuncts[1].push_back( cr ); + } + } + }else{ + Trace("si-prt") << "...failed." << std::endl; + } +} + +bool SingleInvocationPartition::collectConjuncts( Node n, bool pol, std::vector< Node >& conj ) { + if( ( !pol && n.getKind()==OR ) || ( pol && n.getKind()==AND ) ){ + for( unsigned i=0; i& visited, std::vector< Node >& args, + std::vector< Node >& terms, std::vector< Node >& subs ) { + std::map< Node, bool >::iterator it = visited.find( n ); + if( it!=visited.end() ){ + return true; + }else{ + bool ret = true; + for( unsigned i=0; i::iterator it = d_funcs.find( f ); + if( it!=d_funcs.end() ){ + return it->second; + }else{ + TypeNode tn = f.getType(); + bool ret = false; + if( tn.getNumChildren()==d_arg_types.size()+1 ){ + ret = true; + std::vector< Node > children; + children.push_back( f ); + for( unsigned i=0; imkNode( APPLY_UF, children ); + std::stringstream ss; + ss << "F_" << f; + Node v = NodeManager::currentNM()->mkBoundVar( ss.str(), tn.getRangeType() ); + d_func_fo_var[f] = v; + d_func_vars.push_back( v ); + } + } + d_funcs[f] = ret; + return ret; + } +} + +Node SingleInvocationPartition::getConjunct( int index ) { + return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst( true ) : + ( d_conjuncts[index].size()==1 ? d_conjuncts[index][0] : NodeManager::currentNM()->mkNode( AND, d_conjuncts[index] ) ); +} + +void SingleInvocationPartition::debugPrint( const char * c ) { + Trace(c) << "Single invocation variables : "; + for( unsigned i=0; i::iterator it = d_funcs.begin(); it != d_funcs.end(); ++it ){ + Trace(c) << " " << it->first << " : "; + if( it->second ){ + Trace(c) << d_func_inv[it->first] << " " << d_func_fo_var[it->first] << std::endl; + }else{ + Trace(c) << "not incorporated." << std::endl; + } + } + for( unsigned i=0; i<3; i++ ){ + Trace(c) << ( i==0 ? "Single invocation" : ( i==1 ? "Non-single invocation" : "All" ) ); + Trace(c) << " conjuncts: " << std::endl; + for( unsigned j=0; j& curr_disj, bool pol ); Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ); + // partially single invocation + Node removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid, std::map< Node, Node >& visited ); //presolve void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ); void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); @@ -76,15 +80,16 @@ private: std::map< Node, Node > d_single_inv_app_map; //list of skolems for each argument of programs std::vector< Node > d_single_inv_arg_sk; - //list of skolems for each program + //list of variables/skolems for each program + std::vector< Node > d_single_inv_var; std::vector< Node > d_single_inv_sk; std::map< Node, int > d_single_inv_sk_index; - //list of skolems for each program - std::vector< Node > d_single_inv_var; + //program to solution index + std::map< Node, unsigned > d_prog_to_sol_index; //lemmas produced inst::InstMatchTrie d_inst_match_trie; inst::CDInstMatchTrie * d_c_inst_match_trie; - //original conjecture + //original conjecture Node d_orig_conjecture; // solution std::vector< Node > d_varList; @@ -108,12 +113,14 @@ public: CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ); // original conjecture Node d_quant; - // single invocation version of quant + // single invocation version of quantified formula Node d_single_inv; // transition relation version per program std::map< Node, Node > d_trans_pre; std::map< Node, Node > d_trans_post; std::map< Node, std::vector< Node > > d_prog_templ_vars; + //the non-single invocation portion of the quantified formula + std::map< Node, Node > d_nsi_op_map; public: //get the single invocation lemma(s) void getSingleInvLemma( Node guard, std::vector< Node >& lems ); @@ -135,6 +142,41 @@ public: void preregisterConjecture( Node q ); }; +// partitions any formulas given to it into single invocation/non-single invocation +// only processes functions having argument types exactly matching "d_arg_types", +// and all invocations are in the same order across all functions +class SingleInvocationPartition +{ +private: + bool collectConjuncts( Node n, bool pol, std::vector< Node >& conj ); + bool processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args, + std::vector< Node >& terms, std::vector< Node >& subs ); +public: + void init( std::vector< TypeNode >& typs ); + //inputs + void process( Node n ); + std::vector< TypeNode > d_arg_types; + + //outputs (everything is with bound var) + std::map< Node, bool > d_funcs; + std::map< Node, Node > d_func_inv; + std::map< Node, Node > d_func_fo_var; + std::vector< Node > d_func_vars; + std::vector< Node > d_si_vars; + // si, nsi, all + std::vector< Node > d_conjuncts[3]; + + bool isAntiSkolemizableType( Node f ); + + Node getConjunct( int index ); + Node getSingleInvocation() { return getConjunct( 0 ); } + Node getNonSingleInvocation() { return getConjunct( 1 ); } + Node getFullSpecification() { return getConjunct( 2 ); } + + void debugPrint( const char * c ); +}; + + } } } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index cdefcf8e9..be6f71c39 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -207,6 +207,8 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo if and how to apply fairness for cegqi option cegqiSingleInv --cegqi-si bool :default false :read-write process single invocation synthesis conjectures +option cegqiSingleInvPartial --cegqi-si-partial bool :default false + combined techniques for synthesis conjectures that are partially single invocation option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index d289e3938..fc1f052c3 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -75,7 +75,7 @@ bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) { 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, + 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{ @@ -155,6 +155,31 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Nod return ires; } +Node QuantArith::solveEqualityFor( Node lit, Node v ) { + Assert( lit.getKind()==EQUAL || lit.getKind()==IFF ); + //first look directly at sides + TypeNode tn = lit[0].getType(); + for( unsigned r=0; r<2; r++ ){ + if( lit[r]==v ){ + return lit[1-r]; + } + } + if( tn.isInteger() || tn.isReal() ){ + if( quantifiers::TermDb::containsTerm( lit, v ) ){ + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( lit, msum ) ){ + Node val, veqc; + if( QuantArith::isolate( v, msum, veqc, val, EQUAL )!=0 ){ + if( veqc.isNull() ){ + return val; + } + } + } + } + } + return Node::null(); +} + Node QuantArith::negate( Node t ) { Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t ); tt = Rewriter::rewrite( tt ); @@ -184,33 +209,6 @@ void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char Trace(c) << std::endl; } -bool QuantArith::solveEqualityFor( Node lit, Node v, Node & veq ) { - Assert( lit.getKind()==EQUAL || lit.getKind()==IFF ); - //first look directly at sides - TypeNode tn = lit[0].getType(); - for( unsigned r=0; r<2; r++ ){ - if( lit[r]==v ){ - Node olitr = lit[r==0 ? 1 : 0]; - veq = tn.isBoolean() ? lit[r].iffNode( olitr ) : lit[r].eqNode( olitr ); - return true; - } - } - if( tn.isInteger() || tn.isReal() ){ - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( lit, msum ) ){ - if( QuantArith::isolate( v, msum, veq, EQUAL ) ){ - if( veq[0]!=v ){ - Assert( veq[1]==v ); - veq = v.eqNode( veq[0] ); - } - return true; - } - } - } - return false; -} - - void QuantRelevance::registerQuantifier( Node f ){ //compute symbols in f diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index f65163415..566a09923 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -39,10 +39,10 @@ public: //return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false ); static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ); + static Node solveEqualityFor( Node lit, Node v ); static Node negate( Node t ); static Node offset( Node t, int i ); static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ); - static bool solveEqualityFor( Node lit, Node v, Node & veq ); }; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 79e62a6cd..724f16947 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -674,6 +674,47 @@ void TermDb::makeInstantiationConstantsFor( Node q ){ } } +void TermDb::getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==BOUND_VARIABLE ){ + if( std::find( vars.begin(), vars.end(), n )==vars.end() ) { + vars.push_back( n ); + } + } + for( unsigned i=0; i& visited ) { + std::map< Node, Node >::iterator it = visited.find( n ); + if( it!=visited.end() ){ + return it->second; + }else{ + Node ret = n; + if( n.getKind()==FORALL ){ + ret = getRemoveQuantifiers2( n[1], visited ); + }else if( n.getNumChildren()>0 ){ + std::vector< Node > children; + bool childrenChanged = false; + for( unsigned i=0; imkNode( n.getKind(), children ); + } + } + visited[n] = ret; + return ret; + } +} Node TermDb::getInstConstAttr( Node n ) { if (!n.hasAttribute(InstConstantAttribute()) ){ @@ -722,6 +763,30 @@ bool TermDb::hasBoundVarAttr( Node n ) { return !getBoundVarAttr(n).isNull(); } +void TermDb::getBoundVars( Node n, std::vector< Node >& vars ) { + std::map< Node, bool > visited; + return getBoundVars2( n, vars, visited ); +} + +//remove quantifiers +Node TermDb::getRemoveQuantifiers( Node n ) { + std::map< Node, Node > visited; + return getRemoveQuantifiers2( n, visited ); +} + +//quantified simplify +Node TermDb::getQuantSimplify( Node n ) { + std::vector< Node > bvs; + getBoundVars( n, bvs ); + if( bvs.empty() ) { + return Rewriter::rewrite( n ); + }else{ + Node q = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ), n ); + q = Rewriter::rewrite( q ); + return getRemoveQuantifiers( q ); + } +} + /** get the i^th instantiation constant of q */ Node TermDb::getInstantiationConstant( Node q, int i ) const { std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 8ce6aeaf0..86b0efbf3 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -267,7 +267,19 @@ public: static bool hasInstConstAttr( Node n ); static Node getBoundVarAttr( Node n ); static bool hasBoundVarAttr( Node n ); - + +private: + /** get bound vars */ + static void getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); + /** get bound vars */ + static Node getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ); +public: + //get the bound variables in this node + static void getBoundVars( Node n, std::vector< Node >& vars ); + //remove quantifiers + static Node getRemoveQuantifiers( Node n ); + //quantified simplify (treat free variables in n as quantified and run rewriter) + static Node getQuantSimplify( Node n ); //for skolem private: @@ -387,7 +399,7 @@ private: static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); //general utilities public: - /** simple check for contains term */ + /** simple check for whether n contains t as subterm */ static bool containsTerm( Node n, Node t ); /** simple check for contains term, true if contains at least one term in t */ static bool containsTerms( Node n, std::vector< Node >& t ); diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 71ca64aea..32caa4989 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -46,7 +46,8 @@ TESTS = commutative.sy \ dt-no-syntax.sy \ list-head-x.sy \ clock-inc-tuple.sy \ - dt-test-ns.sy + dt-test-ns.sy \ + no-mention.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/no-mention.sy b/test/regress/regress0/sygus/no-mention.sy new file mode 100644 index 000000000..05dfbced3 --- /dev/null +++ b/test/regress/regress0/sygus/no-mention.sy @@ -0,0 +1,15 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi --no-dump-synth +(set-logic LIA) + +(synth-fun p ((x Int) (y Int)) Int) +(synth-fun m ((x Int) (y Int)) Int) +(synth-fun n ((x Int)) Int) + +(declare-var x Int) +(declare-var y Int) + +(constraint (>= (m x y) x)) + +(check-synth) + -- 2.30.2