From 2f930be0eb2d0ea7b8f96448dc2e353927a79b5c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 11 Feb 2015 13:10:11 +0100 Subject: [PATCH] Move si solution reconstruction to own file, make more robust. Other refactoring. --- src/Makefile.am | 2 + .../quantifiers/ce_guided_single_inv.cpp | 907 +-------------- src/theory/quantifiers/ce_guided_single_inv.h | 39 +- .../quantifiers/ce_guided_single_inv_sol.cpp | 1006 +++++++++++++++++ .../quantifiers/ce_guided_single_inv_sol.h | 92 ++ src/theory/quantifiers/term_database.cpp | 120 +- src/theory/quantifiers/term_database.h | 15 +- 7 files changed, 1259 insertions(+), 922 deletions(-) create mode 100644 src/theory/quantifiers/ce_guided_single_inv_sol.cpp create mode 100644 src/theory/quantifiers/ce_guided_single_inv_sol.h diff --git a/src/Makefile.am b/src/Makefile.am index 4ae3c16f8..60f3bc7c2 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -329,6 +329,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/ce_guided_instantiation.cpp \ theory/quantifiers/ce_guided_single_inv.h \ theory/quantifiers/ce_guided_single_inv.cpp \ + theory/quantifiers/ce_guided_single_inv_sol.h \ + theory/quantifiers/ce_guided_single_inv_sol.cpp \ theory/quantifiers/local_theory_ext.h \ theory/quantifiers/local_theory_ext.cpp \ theory/quantifiers/fun_def_process.h \ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 51cce2407..30eac03fb 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -32,21 +32,8 @@ using namespace std; namespace CVC4 { -Node simpleNegate( Node n ){ - if( n.getKind()==OR || n.getKind()==AND ){ - std::vector< Node > children; - for( unsigned i=0; imkNode( n.getKind()==OR ? AND : OR, children ); - }else{ - return n.negate(); - } -} - - -CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * d_qe, Node q, CegConjecture * p ) : d_qe( d_qe ), d_parent( p ), d_quant( q ){ - +CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p ) : d_qe( qe ), d_parent( p ), d_quant( q ){ + d_sol = new CegConjectureSingleInvSol( qe ); } Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { @@ -63,7 +50,7 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { d_single_inv_sk_index[k] = i; } Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); - inst = simpleNegate( inst ); + inst = TermDb::simpleNegate( inst ); Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); }else{ @@ -212,7 +199,7 @@ void CegConjectureSingleInv::initialize() { disj.push_back( cr ); } Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ); - curr = simpleNegate( curr ); + curr = TermDb::simpleNegate( curr ); Trace("cegqi-si") << " " << curr; conjuncts.push_back( curr ); if( !it->first.isNull() ){ @@ -414,7 +401,7 @@ bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Nod analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false ); }else{ if( pol ){ - n = simpleNegate( n ); + n = TermDb::simpleNegate( n ); } Trace("cegqi-si") << "Sygus conjunct : " << n << std::endl; children[p].push_back( n ); @@ -689,24 +676,25 @@ Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) { return d_inst[index][i]; }else{ Node cond = d_lemmas_produced[index]; - cond = simpleNegate( cond ); + cond = TermDb::simpleNegate( cond ); Node ite1 = d_inst[index][i]; Node ite2 = constructSolution( i, index+1 ); return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 ); } } -Node CegConjectureSingleInv::getSolution( unsigned i, TypeNode stn, int& reconstructed ){ +Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){ Assert( !d_lemmas_produced.empty() ); - Node s = constructSolution( i, 0 ); const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); Node varList = Node::fromExpr( dt.getSygusVarList() ); - Node prog = d_quant[0][i]; + Node prog = d_quant[0][sol_index]; Node prog_app = d_single_inv_app_map[prog]; + //get variables std::vector< Node > vars; - std::vector< Node > subs; - Trace("cegqi-si-debug-sol") << "Get solution for " << prog << ", which is applied as " << prog_app << std::endl; + 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; id_varList.push_back( varList[i-1] ); } - s = s.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + //construct the solution + Node s = constructSolution( sol_index, 0 ); + s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() ); d_orig_solution = s; - Trace("cegqi-si-debug-sol") << "Solution (pre-rewrite): " << d_orig_solution << std::endl; - s = pullITEs( s ); - //s = flattenITEs( s ); - //do standard rewriting - s = Rewriter::rewrite( s ); - std::map< Node, bool > sassign; - std::vector< Node > svars; - std::vector< Node > ssubs; - Trace("cegqi-si-debug-sol") << "Solution (pre-simplification): " << s << std::endl; - s = simplifySolution( s, sassign, svars, ssubs, subs, 0 ); - Trace("cegqi-si-debug-sol") << "Solution (post-simplification): " << s << std::endl; - s = Rewriter::rewrite( s ); - Trace("cegqi-si-debug-sol") << "Solution (post-rewrite): " << s << std::endl; + //simplify the solution + Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl; + s = d_sol->simplifySolution( s, stn ); + Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl; d_solution = s; + + //reconstruct the solution into sygus if necessary reconstructed = 0; if( options::cegqiSingleInvReconstruct() && !stn.isNull() ){ - int status; - d_templ_solution = collectReconstructNodes( d_qe->getTermDatabaseSygus(), d_solution, stn, status ); - if( status==1 ){ - setNeedsReconstruction( d_templ_solution, stn, Node::null(), TypeNode::null() ); - } - Trace("cegqi-si-debug-sol") << "Induced solution template is : " << d_templ_solution << std::endl; - std::vector< TypeNode > rcons_tn; - for( std::map< TypeNode, std::map< Node, bool > >::iterator it = d_rcons_to_process.begin(); it != d_rcons_to_process.end(); ++it ){ - TypeNode tn = it->first; - Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Trace("cegqi-si-rcons-stats") << it->second.size() << " terms to reconstruct of type " << dt.getName() << "." << std::endl; - Trace("cegqi-si-rcons") << it->second.size() << " terms to reconstruct of type " << dt.getName() << " : " << std::endl; - for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - Trace("cegqi-si-rcons") << " " << it2->first << std::endl; - } - Assert( !it->second.empty() ); - rcons_tn.push_back( it->first ); + d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed ); + if( reconstructed==1 ){ + Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl; } - bool success; - std::vector< TypeNode > incomplete; - unsigned index = 0; - do { - success = true; - std::vector< TypeNode > to_erase; - for( std::map< TypeNode, std::map< Node, bool > >::iterator it = d_rcons_to_process.begin(); it != d_rcons_to_process.end(); ++it ){ - TypeNode stn = it->first; - if( it->second.empty() ){ - to_erase.push_back( stn ); - }else{ - Node ns = d_qe->getTermDatabase()->getEnumerateTerm( stn, index ); - if( ns.isNull() ){ - to_erase.push_back( stn ); - incomplete.push_back( stn ); - }else{ - Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin( ns, stn ); - Node nr = Rewriter::rewrite( nb );//d_qe->getTermDatabaseSygus()->getNormalized( stn, nb, false, false ); - Trace("cegqi-si-rcons-debug2") << " - try " << ns << " -> " << nr << " for " << stn << " " << nr.getKind() << std::endl; - if( it->second.find( nr )!=it->second.end() ){ - Trace("cegqi-si-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl; - d_reconstructed[nr][stn] = ns; - d_reconstructed_op[nr][stn] = false; - Assert( d_rewrite_to_rcons.find( nr )!=d_rewrite_to_rcons.end() ); - Node nrr = d_rewrite_to_rcons[nr]; - setReconstructed( nrr, stn ); - }else{ - /* - // look if it has a kind of a term that we need to reconstruct TODO - Kind nrk = nr.getKind(); - std::map< Kind, std::map< Node, bool > >::iterator itk = d_rcons_kinds_to_process[stn].find( nrk ); - if( itk!=d_rcons_kinds_to_process[stn].end() ){ - Trace("cegqi-si-rcons") << "Term " << ns << " -> " << nr << " did not match, but has same operator " << nrk; - Trace("cegqi-si-rcons") << " as " << itk->second.size() << " waiting terms." << std::endl; - Assert( !itk->second.empty() ); - for( std::map< Node, bool >::iterator itkn = itk->second.begin(); itkn != itk->second.end(); ++itkn ){ - - } - } - */ - } - success = false; - } - } - } - for( unsigned i=0; igetTermDatabaseSygus(), stn, d_templ_solution ); - Trace("cegqi-si-debug-sol") << "Sygus solution is : " << d_sygus_solution << std::endl; - } - } - }while( !success ); } - if( Trace.isOn("cegqi-si-debug-sol") ){ + + + if( Trace.isOn("csi-sol") ){ //debug solution - if( !debugSolution( d_solution ) ){ - Trace("cegqi-si-debug-sol") << "WARNING : solution " << d_solution << " contains free constants." << std::endl; + if( !d_sol->debugSolution( d_solution ) ){ + Trace("csi-sol") << "WARNING : solution " << d_solution << " contains free constants." << std::endl; //exit( 47 ); }else{ //exit( 49 ); } } if( Trace.isOn("cegqi-stats") ){ - int t_size = 0; - int num_ite = 0; - debugTermSize( d_orig_solution, t_size, num_ite ); - //Trace("cegqi-stats") << "size " << t_size << " #ite " << num_ite << std::endl; - Trace("cegqi-stats") << t_size << " " << num_ite << " "; - t_size = 0; - num_ite = 0; - debugTermSize( d_solution, t_size, num_ite ); - //Trace("cegqi-stats") << "simplified size " << t_size << " #ite " << num_ite << std::endl; - Trace("cegqi-stats") << t_size << " " << num_ite << " "; - t_size = 0; - num_ite = 0; - debugTermSize( d_templ_solution, t_size, num_ite ); - //Trace("cegqi-stats") << "sygus size " << t_size << " #ite " << num_ite << std::endl; - Trace("cegqi-stats") << t_size << " " << num_ite << std::endl; + int tsize, itesize; + tsize = 0;itesize = 0; + d_sol->debugTermSize( d_orig_solution, tsize, itesize ); + Trace("cegqi-stats") << tsize << " " << itesize << " "; + tsize = 0;itesize = 0; + d_sol->debugTermSize( d_solution, tsize, itesize ); + Trace("cegqi-stats") << tsize << " " << itesize << " "; + if( !d_sygus_solution.isNull() ){ + tsize = 0;itesize = 0; + d_sol->debugTermSize( d_sygus_solution, tsize, itesize ); + Trace("cegqi-stats") << tsize << " - "; + }else{ + Trace("cegqi-stats") << "null "; + } + Trace("cegqi-stats") << std::endl; } if( reconstructed==1 ){ return d_sygus_solution; @@ -852,727 +760,4 @@ Node CegConjectureSingleInv::getSolution( unsigned i, TypeNode stn, int& reconst } } -bool CegConjectureSingleInv::debugSolution( Node sol ) { - if( sol.getKind()==SKOLEM ){ - return false; - }else{ - for( unsigned i=0; i conj; - Node t; - Node rem; - if( pullITECondition( s, s, conj, t, rem, 0 ) ){ - Assert( !conj.empty() ); - Node cond = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); - Trace("cegqi-si-debug-sol") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl; - t = pullITEs( t ); - rem = pullITEs( rem ); - s = NodeManager::currentNM()->mkNode( ITE, simpleNegate( cond ), t, rem ); - //Trace("cegqi-si-debug-sol") << "Now : " << s << std::endl; - success = true; - } - }while( success ); - } - return s; -} - -// pull condition common to all ITE conditions in path of size > 1 -bool CegConjectureSingleInv::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) { - Assert( n_ite.getKind()==ITE ); - std::vector< Node > curr_conj; - bool isAnd; - if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){ - isAnd = n_ite[0].getKind()==AND; - for( unsigned i=0; i new_conj; - std::vector< Node > prev_conj; - if( n_ite==root ){ - new_conj.insert( new_conj.end(), curr_conj.begin(), curr_conj.end() ); - Trace("cegqi-pull-ite") << "Pull ITE root " << n_ite << ", #conj = " << new_conj.size() << std::endl; - }else{ - for( unsigned i=0; imkNode( ITE, n0[0], n2, n1 ); - }else if( n0.getKind()==AND || n0.getKind()==OR ){ - std::vector< Node > children; - for( unsigned i=1; imkNode( n0.getKind(), children ); - if( n0.getKind()==AND ){ - ret = NodeManager::currentNM()->mkNode( ITE, rem, NodeManager::currentNM()->mkNode( ITE, n0[0], n1, n2 ), n2 ); - }else{ - ret = NodeManager::currentNM()->mkNode( ITE, rem, n1, NodeManager::currentNM()->mkNode( ITE, n0[0], n1, n2 ) ); - } - }else{ - if( n0.getKind()==ITE ){ - n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ), - NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) ); - }else if( n0.getKind()==IFF ){ - n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ), - NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) ); - }else{ - return NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 ); - } - ret = NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 ); - } - Assert( !ret.isNull() ); - return flattenITEs( ret, false ); - }else{ - if( n.getNumChildren()>0 ){ - std::vector< Node > children; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - bool childChanged = false; - for( unsigned i=0; imkNode( n.getKind(), children ); - } - }else{ - return n; - } - } -} - -// assign is from literals to booleans -// union_find is from args to values - -bool CegConjectureSingleInv::getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, std::vector< Node >& vars, - std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args ) { - std::map< Node, bool >::iterator ita = assign.find( n ); - if( ita!=assign.end() ){ - Trace("csi-simp-debug") << "---already assigned, lookup " << pol << " " << ita->second << std::endl; - return pol==ita->second; - }else if( n.isConst() ){ - return pol==(n==d_qe->getTermDatabase()->d_true); - }else{ - Trace("csi-simp-debug") << "---assign " << n << " " << pol << std::endl; - assign[n] = pol; - new_assign.push_back( n ); - if( ( pol && n.getKind()==AND ) || ( !pol && n.getKind()==OR ) ){ - for( unsigned i=0; i& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args ) { - Assert( eq.getKind()==IFF || eq.getKind()==EQUAL ); - //try to find valid argument - for( unsigned r=0; r<2; r++ ){ - if( std::find( args.begin(), args.end(), eq[r] )!=args.end() ){ - Assert( std::find( vars.begin(), vars.end(), eq[r] )==vars.end() ); - if( std::find( new_vars.begin(), new_vars.end(), eq[r] )==new_vars.end() ){ - Node eqro = eq[r==0 ? 1 : 0 ]; - if( !d_qe->getTermDatabase()->containsTerm( eqro, eq[r] ) ){ - Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl; - new_vars.push_back( eq[r] ); - new_subs.push_back( eqro ); - return true; - } - } - } - } - /* - TypeNode tn = eq[0].getType(); - if( tn.isInteger() || tn.isReal() ){ - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - - } - } - */ - return false; -} - -Node CegConjectureSingleInv::simplifySolution( Node sol, std::map< Node, bool >& assign, - std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status ) { - Assert( vars.size()==subs.size() ); - std::map< Node, bool >::iterator ita = assign.find( sol ); - if( ita!=assign.end() ){ - return NodeManager::currentNM()->mkConst( ita->second ); - }else{ - if( sol.getKind()==ITE ){ - Trace("csi-simp") << "Simplify ITE " << std::endl; - std::vector< Node > children; - for( unsigned r=1; r<=2; r++ ){ - std::vector< Node > new_assign; - std::vector< Node > new_vars; - std::vector< Node > new_subs; - if( getAssign( r==1, sol[0], assign, new_assign, vars, new_vars, new_subs, args ) ){ - Trace("csi-simp") << "- branch " << r << " led to " << new_assign.size() << " assignments, " << new_vars.size() << " equalities." << std::endl; - unsigned prev_size = vars.size(); - Node nc = sol[r]; - if( !new_vars.empty() ){ - nc = nc.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() ); - vars.insert( vars.end(), new_vars.begin(), new_vars.end() ); - subs.insert( subs.end(), new_subs.begin(), new_subs.end() ); - } - nc = simplifySolution( nc, assign, vars, subs, args, 0 ); - children.push_back( nc ); - //clean up substitution - if( !new_vars.empty() ){ - vars.resize( prev_size ); - subs.resize( prev_size ); - } - }else{ - Trace("csi-simp") << "- branch " << r << " of " << sol[0] << " is infeasible." << std::endl; - } - //clean up assignment - for( unsigned i=0; imkNode( ITE, ncond, children[0], children[1] ); - } - }else if( sol.getKind()==OR || sol.getKind()==AND ){ - Trace("csi-simp") << "Simplify " << sol.getKind() << std::endl; - //collect new equalities - std::map< Node, bool > atoms; - std::vector< Node > inc; - std::vector< Node > children; - std::vector< Node > new_vars; - std::vector< Node > new_subs; - Node bc = sol.getKind()==OR ? d_qe->getTermDatabase()->d_true : d_qe->getTermDatabase()->d_false; - for( unsigned i=0; i::iterator it = atoms.find( atom ); - if( it==atoms.end() ){ - atoms[atom] = pol; - if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){ - if( pol==( sol.getKind()==AND ) ){ - Trace("csi-simp") << " ...equality." << std::endl; - if( getAssignEquality( atom, vars, new_vars, new_subs, args ) ){ - children.push_back( sol[i] ); - do_exc = true; - } - } - } - }else{ - //repeated atom - if( it->second!=pol ){ - return NodeManager::currentNM()->mkConst( sol.getKind()==OR ); - }else{ - do_exc = true; - } - } - } - if( !do_exc ){ - inc.push_back( sol[i] ); - }else{ - Trace("csi-simp") << " ...exclude." << std::endl; - } - } - if( !new_vars.empty() ){ - if( !inc.empty() ){ - Node ret = inc.size()==1 ? sol[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc ); - Trace("csi-simp") << "Base return is : " << ret << std::endl; - // apply substitution - ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() ); - ret = Rewriter::rewrite( ret ); - Trace("csi-simp") << "After substitution : " << ret << std::endl; - unsigned prev_size = vars.size(); - vars.insert( vars.end(), new_vars.begin(), new_vars.end() ); - subs.insert( subs.end(), new_subs.begin(), new_subs.end() ); - ret = simplifySolution( ret, assign, vars, subs, args, 1 ); - //clean up substitution - if( !vars.empty() ){ - vars.resize( prev_size ); - subs.resize( prev_size ); - } - //Trace("csi-simp") << "After simplification : " << ret << std::endl; - if( ret.getKind()==sol.getKind() ){ - for( unsigned i=0; i final_children; - for( unsigned i=0; i tmp_vars; - std::vector< Node > tmp_subs; - if( getAssignEquality( atom, vars, tmp_vars, tmp_subs, args ) ){ - Trace("csi-simp-debug") << "Check if " << children[i] << " is redundant in " << sol << std::endl; - for( unsigned j=0; ji || std::find( final_children.begin(), final_children.end(), children[j] )!=final_children.end() ) ){ - Node sj = children[j].substitute( tmp_vars.begin(), tmp_vars.end(), tmp_subs.begin(), tmp_subs.end() ); - sj = Rewriter::rewrite( sj ); - if( sj==d_qe->getTermDatabase()->d_true ){ - Trace("csi-simp") << "--- " << children[i].negate() << " is implied by " << children[j].negate() << std::endl; - red = true; - break; - } - } - } - } - } - } - if( !red ){ - final_children.push_back( children[i] ); - } - } - - return final_children.size()==0 ? NodeManager::currentNM()->mkConst( sol.getKind()==AND ) : - ( final_children.size()==1 ? final_children[0] : NodeManager::currentNM()->mkNode( sol.getKind(), final_children ) ); - }else{ - //generic simplification - std::vector< Node > children; - if( sol.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( sol.getOperator() ); - } - bool childChanged = false; - for( unsigned i=0; imkNode( sol.getKind(), children ); - } - } - return sol; - } -} - -//TODO : accumulate assignment to literals as we traverse ITE -Node CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, int& status ) { - std::map< TypeNode, Node >::iterator it = d_rcons_processed[t].find( stn ); - if( it==d_rcons_processed[t].end() ){ - TypeNode tn = t.getType(); - Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) ); - const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); - Assert( dt.isSygus() ); - Trace("cegqi-si-rcons-debug") << "Check reconstruct " << t << " type " << tn << ", sygus type " << dt.getName() << ", kind " << t.getKind() << std::endl; - tds->registerSygusType( stn ); - Node ret; - std::vector< Node > children; - if( t.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( t.getOperator() ); - } - bool childChanged = false; - std::vector< Node > rcons_child; - std::vector< TypeNode > rcons_child_tn; - Node rcons; - bool rcons_op; - bool rcons_set = false; - Kind tk = t.getKind(); - int karg = tds->getKindArg( stn, tk ); - //preprocessing to fit syntax - Node orig_t = t; - if( t.getNumChildren()>0 ){ - // first, do standard minimizations - t = tds->minimizeBuiltinTerm( t ); - bool success = true; - while( karg==-1 && success ){ - success = false; - Node new_t; - Kind dk; - if( tds->isAntisymmetric( tk, dk ) ){ - if( tds->hasKind( stn, dk ) ){ - new_t = NodeManager::currentNM()->mkNode( dk, t[1], t[0] ); - } - } - if( new_t.isNull() ){ - for( unsigned i=0; igetGenericBase( stn, i ); - if( g.getKind()==t.getKind() ){ - Trace("cegqi-si-rcons-debug") << "Possible match ? " << g << " " << t << " for " << dt[i].getName() << std::endl; - std::map< int, Node > sigma; - if( tds->getMatch( g, t, sigma ) ){ - //we found an exact match - bool msuccess = true; - for( unsigned j=0; j var_count; - new_t = tds->mkGeneric( dt, i, var_count, sigma ); - Trace("cegqi-si-rcons-debug") << "Rewrote to : " << new_t << std::endl; - break; - } - } - } - } - //expand things that have compact representations (these will not be found by enumeration if they aren't already in the syntax) - if( new_t.isNull() ){ - if( t.getKind()==EQUAL && ( t[0].getType().isInteger() || t[0].getType().isReal() ) ){ - new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ), - NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) ); - }else if( t.getKind()==ITE ){ - new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), - NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) ); - }else if( t.getKind()==IFF ){ - new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), - NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) ); - }else if( ( t.getKind()==OR || t.getKind()==AND ) && tds->hasKind( stn, NOT ) ){ - new_t = simpleNegate( t ).negate(); - } - } - } - if( !new_t.isNull() ){ - t = new_t; - karg = tds->getKindArg( stn, t.getKind() ); - success = true; - Trace("cegqi-si-rcons-debug") << "Try rewriting to " << new_t << ", now karg=" << karg << std::endl; - } - } - } - if( karg!=-1 ){ - //flatten ITEs if necessary - if( t.getKind()==ITE ){ - TypeNode cstn = tds->getArgType( dt[karg], 0 ); - tds->registerSygusType( cstn ); - Node prev_t; - while( !tds->hasKind( cstn, t[0].getKind() ) && t!=prev_t ){ - prev_t = t; - Node exp_c = tds->expandBuiltinTerm( t[0] ); - if( !exp_c.isNull() ){ - t = NodeManager::currentNM()->mkNode( ITE, exp_c, t[1], t[2] ); - Trace("cegqi-si-rcons-debug") << "Pre expand to " << t << std::endl; - } - t = flattenITEs( t, false ); - if( t!=prev_t ){ - Trace("cegqi-si-rcons-debug") << "Flatten ITE to " << t << std::endl; - std::map< Node, bool > sassign; - std::vector< Node > svars; - std::vector< Node > ssubs; - t = simplifySolution( t, sassign, svars, ssubs, d_varlist, 0 ); - } - Assert( t.getKind()==ITE ); - } - } - if( t.getNumChildren()==dt[karg].getNumArgs() ){ - Trace("cegqi-si-rcons-debug") << " Type has kind " << t.getKind() << ", recurse." << std::endl; - for( unsigned i=0; igetArgType( dt[karg], i ); - int status; - Node tc = collectReconstructNodes( tds, t[i], cstn, status ); - if( status==1 ){ - rcons_child.push_back( tc ); - rcons_child_tn.push_back( cstn ); - } - children.push_back( tc ); - childChanged = childChanged || tc!=t[i]; - } - rcons = Node::fromExpr( dt[karg].getConstructor() ); - rcons_op = true; - rcons_set = true; - }else{ - Trace("cegqi-si-rcons-debug") << " Type has kind " << t.getKind() << ", but argument mismatch " << std::endl; - if( t.getNumChildren()>dt[karg].getNumArgs() && tds->isAssoc( t.getKind() ) && dt[karg].getNumArgs()==2 ){ - // make n-ary applications into binary ones - TypeNode cstn = tds->getArgType( dt[karg], 0 ); - int status; - Node t1 = collectReconstructNodes( tds, t[0], cstn, status ); - children.push_back( t1 ); - if( status==1 ){ - rcons_child.push_back( t1 ); - rcons_child_tn.push_back( cstn ); - } - std::vector< Node > rem_children; - for( unsigned i=1; imkNode( t.getKind(), rem_children ); - cstn = tds->getArgType( dt[karg], 1 ); - t2 = collectReconstructNodes( tds, t2, cstn, status ); - children.push_back( t2 ); - if( status==1 ){ - rcons_child.push_back( t2 ); - rcons_child_tn.push_back( cstn ); - } - childChanged = true; - rcons = Node::fromExpr( dt[karg].getConstructor() ); - rcons_op = true; - rcons_set = true; - } - } - } - if( !rcons_set ){ - int carg = tds->getOpArg( stn, t ); - if( carg==-1 ){ - if( t.isConst() ){ - ret = tds->builtinToSygusConst( t, stn ); - } - if( ret.isNull() ){ - Trace("cegqi-si-rcons") << "...Reconstruction needed for " << t << " sygus type " << dt.getName() << std::endl; - } - }else{ - rcons = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) ); - rcons_op = false; - rcons_set = true; - Trace("cegqi-si-rcons-debug") << " Type has constant." << std::endl; - } - } - if( ret.isNull() ){ - if( !childChanged ){ - ret = t; - }else{ - ret = NodeManager::currentNM()->mkNode( t.getKind(), children ); - } - } - // now, construct d_rcons_graph - for( unsigned i=0; isecond; - } -} - -void CegConjectureSingleInv::setNeedsReconstruction( Node t, TypeNode stn, Node parent, TypeNode pstn ) { - Trace("cegqi-si-rcons-debug") << "Set reconstruction for " << t << " " << stn << " " << parent << " " << pstn << std::endl; - d_rcons_graph[0][parent][pstn][t][stn] = true; - if( !parent.isNull() ){ - Node parentr = Rewriter::rewrite( parent ); - d_rewrite_to_rcons[parentr] = parent; - d_rcons_to_rewrite[parent] = parentr; - d_rcons_to_process[pstn][parentr] = true; - } - d_rcons_graph[1][t][stn][parent][pstn] = true; - Node tr = Rewriter::rewrite( t ); - d_rewrite_to_rcons[tr] = t; - d_rcons_to_rewrite[t] = tr; - d_rcons_to_process[stn][tr] = true; -} - -void CegConjectureSingleInv::setReconstructed( Node t, TypeNode stn ) { - Assert( !t.isNull() ); - if( Trace.isOn("cegqi-si-rcons-debug") ){ - const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); - Trace("cegqi-si-rcons-debug") << "set rcons : " << t << " in syntax " << dt.getName() << std::endl; - } - // clear all children, d_rcons_parents - std::vector< Node > to_set; - std::vector< TypeNode > to_set_tn; - for( unsigned r=0; r<2; r++){ - unsigned ro = r==0 ? 1 : 0; - for( std::map< Node, std::map< TypeNode, bool > >::iterator it = d_rcons_graph[r][t][stn].begin(); it != d_rcons_graph[r][t][stn].end(); ++it ){ - Node curr = it->first; - TypeNode stnc; - for( std::map< TypeNode, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - stnc = it2->first; - d_rcons_graph[ro][curr][stnc][t].erase( stn ); - if( d_rcons_graph[ro][curr][stnc][t].empty() ){ - d_rcons_graph[ro][curr][stnc].erase( t ); - }else{ - Trace("cegqi-si-rcons-debug") << " " << ( r==0 ? "child" : "parent" ) << " " << curr << " now has " << d_rcons_graph[ro][curr][stnc][t].size() << std::endl; - } - } - if( d_rcons_graph[ro][curr][stnc].empty() ){ - if( !curr.isNull() ){ - to_set.push_back( curr ); - to_set_tn.push_back( stnc ); - } - } - } - } - for( unsigned r=0; r<2; r++){ - d_rcons_graph[r].erase( t ); - } - d_rcons_to_process[stn].erase( d_rcons_to_rewrite[t] ); - for( unsigned i=0; i::iterator it = d_reconstructed[t].find( stn ); - if( it!=d_reconstructed[t].end() ){ - if( d_reconstructed_op[t][stn] ){ - Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) ); - const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); - Assert( dt.isSygus() ); - std::vector< Node > children; - children.push_back( it->second ); - int c = tds->getKindArg( stn, t.getKind() ); - Assert( c!=-1 ); - for( unsigned i=0; igetArgType( dt[c], i ); - Node nc = getReconstructedSolution( tds, stnc, t[i] ); - children.push_back( nc ); - } - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - }else{ - return it->second; - } - }else{ - Trace("cegqi-si-rcons-debug") << "*** error : missing reconstruction for " << t << std::endl; - Assert( false ); - return Node::null(); - } -} - - - } \ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 85ba25a0f..4a9ed76fe 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -20,6 +20,7 @@ #include "context/cdhashmap.h" #include "context/cdchunk_list.h" #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/ce_guided_single_inv_sol.h" namespace CVC4 { namespace theory { @@ -32,6 +33,7 @@ class CegConjectureSingleInv private: QuantifiersEngine * d_qe; CegConjecture * d_parent; + CegConjectureSingleInvSol * d_sol; bool analyzeSygusConjunct( Node n, Node p, 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 ); @@ -44,7 +46,6 @@ private: int classifyTerm( Node n, std::map< Node, int >& subs_from_model ); void collectProgVars( Node n, std::vector< Node >& vars ); Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ); - public: CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p ); // original conjecture @@ -67,10 +68,9 @@ public: std::vector< Node > d_lemmas_produced; std::vector< std::vector< Node > > d_inst; // solution - std::vector< Node > d_varlist; + std::vector< Node > d_varList; Node d_orig_solution; Node d_solution; - Node d_templ_solution; Node d_sygus_solution; public: //get the single invocation lemma @@ -80,38 +80,7 @@ public: //check void check( std::vector< Node >& lems ); //get solution - Node getSolution( unsigned i, TypeNode stn, int& reconstructed ); - - -//solution simplification -private: - bool debugSolution( Node sol ); - void debugTermSize( Node sol, int& t_size, int& num_ite ); - Node pullITEs( Node n ); - bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth ); - Node flattenITEs( Node n, bool rec = true ); - Node simplifySolution( Node sol, std::map< Node, bool >& assign, - std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status ); - bool getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, - std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args ); - bool getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args ); -//solution reconstruction -private: - std::map< Node, std::map< TypeNode, Node > > d_rcons_processed; - std::map< Node, std::map< TypeNode, int > > d_rcons_processed_status; - std::map< Node, std::map< TypeNode, Node > > d_reconstructed; - std::map< Node, std::map< TypeNode, bool > > d_reconstructed_op; - std::map< Node, std::map< TypeNode, std::map< Node, std::map< TypeNode, bool > > > > d_rcons_graph[2]; - std::map< TypeNode, std::map< Node, bool > > d_rcons_to_process; - std::map< Node, Node > d_rewrite_to_rcons; - std::map< Node, Node > d_rcons_to_rewrite; - // term t with sygus type st, returns inducted templated form of t - Node collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, int& status ); - // set reconstructed - void setNeedsReconstruction( Node t, TypeNode stn, Node parent, TypeNode pstn ); - void setReconstructed( Node tr, TypeNode stn ); - // get solution - Node getReconstructedSolution( TermDbSygus * tds, TypeNode stn, Node t ); + Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ); }; } diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp new file mode 100644 index 000000000..02c4c3a28 --- /dev/null +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -0,0 +1,1006 @@ +/********************* */ +/*! \file ce_guided_single_inv.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief utility for processing single invocation synthesis conjectures + ** + **/ + +#include "theory/quantifiers/ce_guided_single_inv_sol.h" +#include "theory/quantifiers/ce_guided_single_inv.h" +#include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/datatypes/datatypes_rewriter.h" +#include "util/datatype.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/trigger.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace std; + +namespace CVC4 { + +CegConjectureSingleInvSol::CegConjectureSingleInvSol( QuantifiersEngine * qe ) : d_qe( qe ){ + d_id_count = 0; +} + +bool CegConjectureSingleInvSol::debugSolution( Node sol ) { + if( sol.getKind()==SKOLEM ){ + return false; + }else{ + for( unsigned i=0; i::iterator it = d_dterm_size.find( sol ); + if( it==d_dterm_size.end() ){ + int prev = t_size; + int prev_ite = num_ite; + t_size++; + if( sol.getKind()==ITE ){ + num_ite++; + } + for( unsigned i=0; isecond; + num_ite += d_dterm_ite_size[sol]; + } +} + + +Node CegConjectureSingleInvSol::pullITEs( Node s ) { + if( s.getKind()==ITE ){ + bool success; + do { + success = false; + std::vector< Node > conj; + Node t; + Node rem; + if( pullITECondition( s, s, conj, t, rem, 0 ) ){ + Assert( !conj.empty() ); + Node cond = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); + Trace("csi-sol-debug") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl; + t = pullITEs( t ); + rem = pullITEs( rem ); + s = NodeManager::currentNM()->mkNode( ITE, TermDb::simpleNegate( cond ), t, rem ); + //Trace("csi-debug-sol") << "Now : " << s << std::endl; + success = true; + } + }while( success ); + } + return s; +} + +// pull condition common to all ITE conditions in path of size > 1 +bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) { + Assert( n_ite.getKind()==ITE ); + std::vector< Node > curr_conj; + bool isAnd; + if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){ + isAnd = n_ite[0].getKind()==AND; + for( unsigned i=0; i new_conj; + std::vector< Node > prev_conj; + if( n_ite==root ){ + new_conj.insert( new_conj.end(), curr_conj.begin(), curr_conj.end() ); + Trace("csi-sol-debug") << "Pull ITE root " << n_ite << ", #conj = " << new_conj.size() << std::endl; + }else{ + for( unsigned i=0; imkNode( ITE, n0[0], n2, n1 ); + }else if( n0.getKind()==AND || n0.getKind()==OR ){ + std::vector< Node > children; + for( unsigned i=1; imkNode( n0.getKind(), children ); + if( n0.getKind()==AND ){ + ret = NodeManager::currentNM()->mkNode( ITE, rem, NodeManager::currentNM()->mkNode( ITE, n0[0], n1, n2 ), n2 ); + }else{ + ret = NodeManager::currentNM()->mkNode( ITE, rem, n1, NodeManager::currentNM()->mkNode( ITE, n0[0], n1, n2 ) ); + } + }else{ + if( n0.getKind()==ITE ){ + n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ), + NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) ); + }else if( n0.getKind()==IFF ){ + n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ), + NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) ); + }else{ + return NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 ); + } + ret = NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 ); + } + Assert( !ret.isNull() ); + return flattenITEs( ret, false ); + }else{ + if( n.getNumChildren()>0 ){ + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; imkNode( n.getKind(), children ); + } + }else{ + return n; + } + } +} + +// assign is from literals to booleans +// union_find is from args to values + +bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, std::vector< Node >& vars, + std::vector< Node >& new_vars, std::vector< Node >& new_subs ) { + std::map< Node, bool >::iterator ita = assign.find( n ); + if( ita!=assign.end() ){ + Trace("csi-simp-debug") << "---already assigned, lookup " << pol << " " << ita->second << std::endl; + return pol==ita->second; + }else if( n.isConst() ){ + return pol==(n==d_qe->getTermDatabase()->d_true); + }else{ + Trace("csi-simp-debug") << "---assign " << n << " " << pol << std::endl; + assign[n] = pol; + new_assign.push_back( n ); + if( ( pol && n.getKind()==AND ) || ( !pol && n.getKind()==OR ) ){ + for( unsigned i=0; i& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ) { + Assert( eq.getKind()==IFF || eq.getKind()==EQUAL ); + //try to find valid argument + for( unsigned r=0; r<2; r++ ){ + if( std::find( d_varList.begin(), d_varList.end(), eq[r] )!=d_varList.end() ){ + Assert( std::find( vars.begin(), vars.end(), eq[r] )==vars.end() ); + if( std::find( new_vars.begin(), new_vars.end(), eq[r] )==new_vars.end() ){ + Node eqro = eq[r==0 ? 1 : 0 ]; + if( !d_qe->getTermDatabase()->containsTerm( eqro, eq[r] ) ){ + Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl; + new_vars.push_back( eq[r] ); + new_subs.push_back( eqro ); + return true; + } + } + } + } + /* + TypeNode tn = eq[0].getType(); + if( tn.isInteger() || tn.isReal() ){ + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + + } + } + */ + return false; +} + +Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ + int tsize, itesize; + if( Trace.isOn("csi-sol") ){ + tsize = 0;itesize = 0; + debugTermSize( sol, tsize, itesize ); + Trace("csi-sol") << tsize << " " << itesize << " rewrite..." << std::endl; + Trace("csi-sol-debug") << "sol : " << sol << "..." << std::endl; + } + Node sol0 = Rewriter::rewrite( sol ); + Trace("csi-sol") << "now : " << sol0 << std::endl; + + Node curr_sol = sol0; + Node prev_sol; + do{ + prev_sol = curr_sol; + //first, pull ITE conditions + if( Trace.isOn("csi-sol") ){ + tsize = 0;itesize = 0; + debugTermSize( curr_sol, tsize, itesize ); + Trace("csi-sol") << tsize << " " << itesize << " pull ITE..." << std::endl; + Trace("csi-sol-debug") << "sol : " << curr_sol << "..." << std::endl; + } + Node sol1 = pullITEs( curr_sol ); + Trace("csi-sol") << "now : " << sol1 << std::endl; + //do standard rewriting + if( sol1!=curr_sol ){ + if( Trace.isOn("csi-sol") ){ + tsize = 0;itesize = 0; + debugTermSize( sol1, tsize, itesize ); + Trace("csi-sol") << tsize << " " << itesize << " rewrite..." << std::endl; + Trace("csi-sol-debug") << "sol : " << sol1 << "..." << std::endl; + } + Node sol2 = Rewriter::rewrite( sol1 ); + Trace("csi-sol") << "now : " << sol2 << std::endl; + curr_sol = sol2; + } + //now do branch analysis + if( Trace.isOn("csi-sol") ){ + tsize = 0;itesize = 0; + debugTermSize( curr_sol, tsize, itesize ); + Trace("csi-sol") << tsize << " " << itesize << " simplify solution..." << std::endl; + Trace("csi-sol-debug") << "sol : " << curr_sol << "..." << std::endl; + } + std::map< Node, bool > sassign; + std::vector< Node > svars; + std::vector< Node > ssubs; + Node sol3 = simplifySolutionNode( curr_sol, stn, sassign, svars, ssubs, 0 ); + Trace("csi-sol") << "now : " << sol3 << std::endl; + if( sol3!=curr_sol ){ + //do standard rewriting again + if( Trace.isOn("csi-sol" ) ){ + tsize = 0;itesize = 0; + debugTermSize( sol3, tsize, itesize ); + Trace("csi-sol") << tsize << " " << itesize << " rewrite..." << std::endl; + } + Node sol4 = Rewriter::rewrite( sol3 ); + Trace("csi-sol") << "now : " << sol4 << std::endl; + curr_sol = sol4; + } + }while( curr_sol!=prev_sol ); + + return curr_sol; +} + +Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, std::map< Node, bool >& assign, + std::vector< Node >& vars, std::vector< Node >& subs, int status ) { + + Assert( vars.size()==subs.size() ); + std::map< Node, bool >::iterator ita = assign.find( sol ); + if( ita!=assign.end() ){ + //it is currently assigned a boolean value + return NodeManager::currentNM()->mkConst( ita->second ); + }else{ + d_qe->getTermDatabaseSygus()->registerSygusType( stn ); + std::map< int, TypeNode > stnc; + if( !stn.isNull() ){ + int karg = d_qe->getTermDatabaseSygus()->getKindArg( stn, sol.getKind() ); + if( karg!=-1 ){ + const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); + if( dt[karg].getNumArgs()==sol.getNumChildren() ){ + for( unsigned i=0; igetTermDatabaseSygus()->getArgType( dt[karg], i ); + } + } + } + } + + if( sol.getKind()==ITE ){ + Trace("csi-simp") << "Simplify ITE " << std::endl; + std::vector< Node > children; + for( unsigned r=1; r<=2; r++ ){ + std::vector< Node > new_assign; + std::vector< Node > new_vars; + std::vector< Node > new_subs; + if( getAssign( r==1, sol[0], assign, new_assign, vars, new_vars, new_subs ) ){ + Trace("csi-simp") << "- branch " << r << " led to " << new_assign.size() << " assignments, " << new_vars.size() << " equalities." << std::endl; + unsigned prev_size = vars.size(); + Node nc = sol[r]; + if( !new_vars.empty() ){ + nc = nc.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() ); + vars.insert( vars.end(), new_vars.begin(), new_vars.end() ); + subs.insert( subs.end(), new_subs.begin(), new_subs.end() ); + } + nc = simplifySolutionNode( nc, stnc[r], assign, vars, subs, 0 ); + children.push_back( nc ); + //clean up substitution + if( !new_vars.empty() ){ + vars.resize( prev_size ); + subs.resize( prev_size ); + } + }else{ + Trace("csi-simp") << "- branch " << r << " of " << sol[0] << " is infeasible." << std::endl; + } + //clean up assignment + for( unsigned i=0; imkNode( ITE, ncond, children[0], children[1] ); + + //expand/flatten if necessary + Node orig_ret = ret; + if( !stnc[0].isNull() ){ + d_qe->getTermDatabaseSygus()->registerSygusType( stnc[0] ); + Node prev_ret; + while( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) && ret!=prev_ret ){ + prev_ret = ret; + Node exp_c = d_qe->getTermDatabaseSygus()->expandBuiltinTerm( ret[0] ); + if( !exp_c.isNull() ){ + Trace("csi-simp-debug") << "Pre expand to " << ret[0] << " to " << exp_c << std::endl; + ret = NodeManager::currentNM()->mkNode( ITE, exp_c, ret[1], ret[2] ); + } + if( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) ){ + Trace("csi-sol") << "Flatten based on " << ret[0] << "." << std::endl; + ret = flattenITEs( ret, false ); + } + } + } + return ret; + /* + if( orig_ret!=ret ){ + Trace("csi-simp") << "Try expanded ITE" << std::endl; + return ret;//simplifySolutionNode( ret, stn, assign, vars, subs, status ); + }else{ + return ret; + } + */ + } + }else if( sol.getKind()==OR || sol.getKind()==AND ){ + Trace("csi-simp") << "Simplify " << sol.getKind() << std::endl; + //collect new equalities + std::map< Node, bool > atoms; + std::vector< Node > inc; + std::vector< Node > children; + std::vector< Node > new_vars; + std::vector< Node > new_subs; + Node bc = sol.getKind()==OR ? d_qe->getTermDatabase()->d_true : d_qe->getTermDatabase()->d_false; + for( unsigned i=0; i::iterator ita = assign.find( sol[i] ); + if( ita==assign.end() ){ + c = sol[i]; + }else{ + c = NodeManager::currentNM()->mkConst( ita->second ); + } + Trace("csi-simp") << " - child " << i << " : " << c << std::endl; + if( c.isConst() ){ + if( c==bc ){ + Trace("csi-simp") << " ...singularity." << std::endl; + return bc; + }else{ + do_exc = true; + } + }else{ + Node atom = c.getKind()==NOT ? c[0] : c; + bool pol = c.getKind()!=NOT; + std::map< Node, bool >::iterator it = atoms.find( atom ); + if( it==atoms.end() ){ + atoms[atom] = pol; + if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){ + if( pol==( sol.getKind()==AND ) ){ + Trace("csi-simp") << " ...equality." << std::endl; + if( getAssignEquality( atom, vars, new_vars, new_subs ) ){ + children.push_back( sol[i] ); + do_exc = true; + } + } + } + }else{ + //repeated atom + if( it->second!=pol ){ + return NodeManager::currentNM()->mkConst( sol.getKind()==OR ); + }else{ + do_exc = true; + } + } + } + if( !do_exc ){ + inc.push_back( sol[i] ); + }else{ + Trace("csi-simp") << " ...exclude." << std::endl; + } + } + if( !new_vars.empty() ){ + if( !inc.empty() ){ + Node ret = inc.size()==1 ? sol[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc ); + Trace("csi-simp") << "Base return is : " << ret << std::endl; + // apply substitution + ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() ); + ret = Rewriter::rewrite( ret ); + Trace("csi-simp") << "After substitution : " << ret << std::endl; + unsigned prev_size = vars.size(); + vars.insert( vars.end(), new_vars.begin(), new_vars.end() ); + subs.insert( subs.end(), new_subs.begin(), new_subs.end() ); + ret = simplifySolutionNode( ret, TypeNode::null(), assign, vars, subs, 1 ); + //clean up substitution + if( !vars.empty() ){ + vars.resize( prev_size ); + subs.resize( prev_size ); + } + //Trace("csi-simp") << "After simplification : " << ret << std::endl; + if( ret.isConst() ){ + if( ret==bc ){ + return bc; + } + }else{ + if( ret.getKind()==sol.getKind() ){ + for( unsigned i=0; i final_children; + for( unsigned i=0; i tmp_vars; + std::vector< Node > tmp_subs; + if( getAssignEquality( atom, vars, tmp_vars, tmp_subs ) ){ + Trace("csi-simp-debug") << "Check if " << children[i] << " is redundant in " << sol << std::endl; + for( unsigned j=0; ji || std::find( final_children.begin(), final_children.end(), children[j] )!=final_children.end() ) ){ + Node sj = children[j].substitute( tmp_vars.begin(), tmp_vars.end(), tmp_subs.begin(), tmp_subs.end() ); + sj = Rewriter::rewrite( sj ); + if( sj==( sol.getKind()==AND ? d_qe->getTermDatabase()->d_false : d_qe->getTermDatabase()->d_true ) ){ + Trace("csi-simp") << "--- " << children[i].negate() << " is implied by " << children[j].negate() << std::endl; + red = true; + break; + } + } + } + if( !red ){ + Trace("csi-simp-debug") << "...is not." << std::endl; + } + } + } + } + if( !red ){ + final_children.push_back( children[i] ); + } + } + return final_children.size()==0 ? NodeManager::currentNM()->mkConst( sol.getKind()==AND ) : + ( final_children.size()==1 ? final_children[0] : NodeManager::currentNM()->mkNode( sol.getKind(), final_children ) ); + }else{ + //generic simplification + std::vector< Node > children; + if( sol.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( sol.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; imkNode( sol.getKind(), children ); + } + } + return sol; + } +} + + + + + + +Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int& reconstructed ) { + Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl; + int status; + d_root_id = collectReconstructNodes( sol, stn, status ); + if( status==0 ){ + Node ret = getReconstructedSolution( d_root_id ); + Trace("csi-rcons") << "Sygus solution is : " << ret << std::endl; + Assert( !ret.isNull() ); + reconstructed = 1; + return ret; + }else{ + //Trace("csi-debug-sol") << "Induced solution template is : " << d_templ_solution << std::endl; + if( Trace.isOn("csi-rcons") ){ + for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){ + TypeNode tn = it->first; + Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName() << " : " << std::endl; + for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + if( d_reconstruct.find( it2->second )==d_reconstruct.end() ){ + Trace("csi-rcons") << " " << it2->first << std::endl; + } + } + Assert( !it->second.empty() ); + } + } + unsigned index = 0; + std::map< TypeNode, bool > active; + for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){ + active[it->first] = true; + } + //enumerate for all types + do { + std::vector< TypeNode > to_erase; + for( std::map< TypeNode, bool >::iterator it = active.begin(); it != active.end(); ++it ){ + TypeNode stn = it->first; + Node ns = d_qe->getTermDatabase()->getEnumerateTerm( stn, index ); + if( ns.isNull() ){ + to_erase.push_back( stn ); + }else{ + Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin( ns, stn ); + Node nr = Rewriter::rewrite( nb );//d_qe->getTermDatabaseSygus()->getNormalized( stn, nb, false, false ); + Trace("csi-rcons-debug2") << " - try " << ns << " -> " << nr << " for " << stn << " " << nr.getKind() << std::endl; + std::map< Node, int >::iterator itt = d_rcons_to_id[stn].find( nr ); + if( itt!= d_rcons_to_id[stn].end() ){ + // if it is not already reconstructed + if( d_reconstruct.find( itt->second )==d_reconstruct.end() ){ + Trace("csi-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl; + bool do_check = getPathToRoot( itt->second ); + setReconstructed( itt->second, ns ); + if( do_check ){ + Trace("csi-rcons-debug") << "...path to root, try reconstruction." << std::endl; + d_tmp_fail.clear(); + Node ret = getReconstructedSolution( d_root_id ); + if( !ret.isNull() ){ + Trace("csi-rcons") << "Sygus solution (after enumeration) is : " << ret << std::endl; + reconstructed = 1; + return ret; + } + }else{ + Trace("csi-rcons-debug") << "...no path to root." << std::endl; + } + } + } + } + } + for( unsigned i=0; i::iterator itri = d_rcons_to_status[stn].find( t ); + if( itri!=d_rcons_to_status[stn].end() ){ + status = itri->second; + //Trace("csi-rcons-debug") << "-> (cached) " << status << " for " << d_rcons_to_id[stn][t] << std::endl; + return d_rcons_to_id[stn][t]; + }else{ + status = 1; + d_qe->getTermDatabaseSygus()->registerSygusType( stn ); + int id = allocate( t, stn ); + d_rcons_to_status[stn][t] = -1; + TypeNode tn = t.getType(); + Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) ); + const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); + Assert( dt.isSygus() ); + Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl; + int carg = -1; + int karg = -1; + // first, do standard minimizations + Node min_t = d_qe->getTermDatabaseSygus()->minimizeBuiltinTerm( t ); + Trace("csi-rcons-debug") << "Minimized term is : " << min_t << std::endl; + //check if op is in syntax sort + carg = d_qe->getTermDatabaseSygus()->getOpArg( stn, min_t ); + if( carg!=-1 ){ + Trace("csi-rcons-debug") << " Type has constant." << std::endl; + d_reconstruct[id] = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) ); + status = 0; + }else{ + //check if kind is in syntax sort + karg = d_qe->getTermDatabaseSygus()->getKindArg( stn, min_t.getKind() ); + if( karg!=-1 ){ + //collect the children of min_t + std::vector< Node > tchildren; + if( min_t.getNumChildren()>dt[karg].getNumArgs() && d_qe->getTermDatabaseSygus()->isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){ + tchildren.push_back( min_t[0] ); + std::vector< Node > rem_children; + for( unsigned i=1; imkNode( min_t.getKind(), rem_children ); + tchildren.push_back( t2 ); + Trace("csi-rcons-debug") << "...split n-ary to binary " << min_t[0] << " " << t2 << "." << std::endl; + }else{ + for( unsigned i=0; i args; + if( d_qe->getTermDatabaseSygus()->getMatch( min_t, stn, index_found, args, karg, c_index ) ){ + success = true; + status = 0; + Node cons = Node::fromExpr( dt[index_found].getConstructor() ); + Trace("csi-rcons-debug") << "Try alternative for " << id << ", matching " << dt[index_found].getName() << " with children : " << std::endl; + for( unsigned i=0; i equiv; + if( tn.isBoolean() ){ + Node curr = min_t; + Node new_t; + do{ + new_t = Node::null(); + if( curr.getKind()==EQUAL && ( curr[0].getType().isInteger() || curr[0].getType().isReal() ) ){ + new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ), + NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) ); + }else if( curr.getKind()==ITE ){ + new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), + NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) ); + }else if( curr.getKind()==IFF ){ + new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), + NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) ); + }else if( curr.getKind()==OR || curr.getKind()==AND ){ + new_t = TermDb::simpleNegate( curr ).negate(); + }else if( curr.getKind()==NOT ){ + new_t = TermDb::simpleNegate( curr[0] ); + }else{ + new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) ); + } + if( !new_t.isNull() ){ + if( new_t!=min_t && std::find( equiv.begin(), equiv.end(), new_t )==equiv.end() ){ + curr = new_t; + equiv.push_back( new_t ); + }else{ + new_t = Node::null(); + } + } + }while( !new_t.isNull() ); + } + //assign ids to terms + Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl; + std::vector< int > equiv_ids; + for( unsigned i=0; i *** reconstruction required for id " << id << std::endl; + }else{ + Trace("csi-rcons-debug") << "-> success for " << id << std::endl; + } + d_rcons_to_status[stn][t] = status; + return id; + } +} + +bool CegConjectureSingleInvSol::collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status ) { + for( unsigned i=0; igetTermDatabaseSygus()->getArgType( dtc, i ); + int cstatus; + int c_id = collectReconstructNodes( ts[i], cstn, cstatus ); + if( cstatus==-1 ){ + return false; + }else if( cstatus!=0 ){ + status = 1; + } + ids.push_back( c_id ); + } + for( unsigned i=0; igetArgType( dt[karg], 0 ); + tds->registerSygusType( cstn ); + Node prev_t; + while( !tds->hasKind( cstn, t[0].getKind() ) && t!=prev_t ){ + prev_t = t; + Node exp_c = tds->expandBuiltinTerm( t[0] ); + if( !exp_c.isNull() ){ + t = NodeManager::currentNM()->mkNode( ITE, exp_c, t[1], t[2] ); + Trace("csi-rcons-debug") << "Pre expand to " << t << std::endl; + } + t = flattenITEs( t, false ); + if( t!=prev_t ){ + Trace("csi-rcons-debug") << "Flatten ITE to " << t << std::endl; + std::map< Node, bool > sassign; + std::vector< Node > svars; + std::vector< Node > ssubs; + t = simplifySolutionNode( t, sassign, svars, ssubs, 0 ); + } + Assert( t.getKind()==ITE ); + } + } + */ + + +Node CegConjectureSingleInvSol::CegConjectureSingleInvSol::getReconstructedSolution( int id, bool mod_eq ) { + std::map< int, Node >::iterator it = d_reconstruct.find( id ); + if( it!=d_reconstruct.end() ){ + return it->second; + }else{ + if( std::find( d_tmp_fail.begin(), d_tmp_fail.end(), id )!=d_tmp_fail.end() ){ + return Node::null(); + }else{ + // try each child option + std::map< int, std::map< Node, std::vector< int > > >::iterator ito = d_reconstruct_op.find( id ); + if( ito!=d_reconstruct_op.end() ){ + for( std::map< Node, std::vector< int > >::iterator itt = ito->second.begin(); itt != ito->second.end(); ++itt ){ + std::vector< Node > children; + children.push_back( itt->first ); + bool success = true; + for( unsigned i=0; isecond.size(); i++ ){ + Node nc = getReconstructedSolution( itt->second[i] ); + if( nc.isNull() ){ + success = false; + break; + }else{ + children.push_back( nc ); + } + } + if( success ){ + Node ret = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + setReconstructed( id, ret ); + return ret; + } + } + } + // try terms in the equivalence class of this + if( mod_eq ){ + int rid = d_rep[id]; + for( unsigned i=0; i::iterator it = d_rcons_to_id[stn].find( n ); + if( it==d_rcons_to_id[stn].end() ){ + int ret = d_id_count; + Trace("csi-rcons-debug") << "id " << ret << " : " << n << std::endl; + d_id_node[d_id_count] = n; + d_id_type[d_id_count] = stn; + d_rep[d_id_count] = d_id_count; + d_eqc[d_id_count].push_back( d_id_count ); + d_rcons_to_id[stn][n] = d_id_count; + d_id_count++; + return ret; + }else{ + return it->second; + } +} + +bool CegConjectureSingleInvSol::getPathToRoot( int id ) { + if( id==d_root_id ){ + return true; + }else{ + std::map< int, Node >::iterator it = d_reconstruct.find( id ); + if( it!=d_reconstruct.end() ){ + return false; + }else{ + int rid = d_rep[id]; + for( unsigned j=0; j d_varList; + std::map< Node, int > d_dterm_size; + std::map< Node, int > d_dterm_ite_size; +//solution simplification +private: + bool debugSolution( Node sol ); + void debugTermSize( Node sol, int& t_size, int& num_ite ); + Node pullITEs( Node n ); + bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth ); + Node flattenITEs( Node n, bool rec = true ); + bool getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, + std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ); + bool getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ); + Node simplifySolutionNode( Node sol, TypeNode stn, std::map< Node, bool >& assign, + std::vector< Node >& vars, std::vector< Node >& subs, int status ); +public: + Node simplifySolution( Node sol, TypeNode stn ); +//solution reconstruction +private: + int d_id_count; + int d_root_id; + std::map< int, Node > d_id_node; + std::map< int, TypeNode > d_id_type; + std::map< TypeNode, std::map< Node, int > > d_rcons_to_id; + std::map< TypeNode, std::map< Node, int > > d_rcons_to_status; + + std::map< int, std::map< Node, std::vector< int > > > d_reconstruct_op; + std::map< int, Node > d_reconstruct; + std::map< int, std::vector< int > > d_parents; + + std::map< int, std::vector< int > > d_eqc; + std::map< int, int > d_rep; + + //cache when reconstructing solutions + std::vector< int > d_tmp_fail; + // get reconstructed solution + Node getReconstructedSolution( int id, bool mod_eq = true ); + + // allocate node with type + int allocate( Node n, TypeNode stn ); + // term t with sygus type st, returns inducted templated form of t + int collectReconstructNodes( Node t, TypeNode stn, int& status ); + bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status ); + bool getPathToRoot( int id ); + void setReconstructed( int id, Node n ); +public: + Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed ); +public: + CegConjectureSingleInvSol( QuantifiersEngine * qe ); +}; + + +} +} +} + +#endif diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cca2cb5e2..e3f73699b 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1145,6 +1145,18 @@ bool TermDb::containsTerm( Node n, Node t ) { } } +Node TermDb::simpleNegate( Node n ){ + if( n.getKind()==OR || n.getKind()==AND ){ + std::vector< Node > children; + for( unsigned i=0; imkNode( n.getKind()==OR ? AND : OR, children ); + }else{ + return n.negate(); + } +} + void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ @@ -1404,6 +1416,85 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect return false; } +bool TermDbSygus::getMatch( Node t, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc, int index_start ) { + Assert( datatypes::DatatypesRewriter::isTypeDatatype( st ) ); + const Datatype& dt = ((DatatypeType)(st).toType()).getDatatype(); + Assert( dt.isSygus() ); + std::map< Kind, std::vector< Node > > kgens; + std::vector< Node > gens; + for( unsigned i=index_start; i sigma; + if( getMatch( g, t, sigma ) ){ + //we found an exact match + bool msuccess = true; + for( unsigned j=0; j var_count; + //Node new_t = mkGeneric( dt, i, var_count, args ); + //Trace("sygus-db-debug") << "Rewrote to : " << new_t << std::endl; + //return new_t; + } + } + } + } + /* + //otherwise, try to modulate based on kinds + for( std::map< Kind, std::vector< Node > >::iterator it = kgens.begin(); it != kgens.end(); ++it ){ + if( it->second.size()>1 ){ + for( unsigned i=0; isecond.size(); i++ ){ + for( unsigned j=0; jsecond.size(); j++ ){ + if( i!=j ){ + std::map< int, Node > sigma; + if( getMatch( it->second[i], it->second[j], sigma ) ){ + if( sigma.size()==1 ){ + //Node mod_pat = sigma.begin().second; + //Trace("cegqi-si-rcons-debug") << "Modulated pattern " << mod_pat << " from " << it->second[i] << " and " << it->second[j] << std::endl; + } + } + } + } + } + } + } + */ + return false; +} + +Node TermDbSygus::getGenericBase( TypeNode tn, const Datatype& dt, int c ) { + std::map< int, Node >::iterator it = d_generic_base[tn].find( c ); + if( it==d_generic_base[tn].end() ){ + registerSygusType( tn ); + std::map< TypeNode, int > var_count; + std::map< int, Node > pre; + Node g = mkGeneric( dt, c, var_count, pre ); + Node gr = Rewriter::rewrite( g ); + gr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( gr.toExpr() ) ); + Trace("sygus-db") << "Sygus DB : Generic base " << dt[c].getName() << " : " << gr << std::endl; + d_generic_base[tn][c] = gr; + return gr; + }else{ + return it->second; + } +} + Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ) { Assert( c>=0 && c<(int)dt.getNumConstructors() ); Assert( dt.isSygus() ); @@ -1443,24 +1534,6 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int } } -Node TermDbSygus::getGenericBase( TypeNode tn, int c ) { - std::map< int, Node >::iterator it = d_generic_base[tn].find( c ); - if( it==d_generic_base[tn].end() ){ - Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Assert( dt.isSygus() ); - registerSygusType( tn ); - std::map< TypeNode, int > var_count; - std::map< int, Node > pre; - Node g = mkGeneric( dt, c, var_count, pre ); - Node gr = Rewriter::rewrite( g ); - d_generic_base[tn][c] = gr; - return gr; - }else{ - return it->second; - } -} - Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n ); if( it==d_sygus_to_builtin[tn].end() ){ @@ -1474,6 +1547,7 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { pre[j] = sygusToBuiltin( n[j], getArgType( dt[i], j ) ); } Node ret = mkGeneric( dt, i, var_count, pre ); + ret = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( ret.toExpr() ) ); d_sygus_to_builtin[tn][n] = ret; return ret; }else{ @@ -1571,7 +1645,6 @@ int TermDbSygus::getTermSize( Node n ){ } return 1+sum; } - } bool TermDbSygus::isAssoc( Kind k ) { @@ -1868,7 +1941,8 @@ TypeNode TermDbSygus::getArgType( const DatatypeConstructor& c, int i ) { } Node TermDbSygus::minimizeBuiltinTerm( Node n ) { - if( ( n.getKind()==EQUAL || n.getKind()==LEQ ) && ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){ + if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) && + ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){ bool changed = false; std::vector< Node > mon[2]; for( unsigned r=0; r<2; r++ ){ @@ -1908,12 +1982,12 @@ Node TermDbSygus::expandBuiltinTerm( Node t ){ if( t.getKind()==EQUAL && ( t[0].getType().isInteger() || t[0].getType().isReal() ) ){ return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ), NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) ); - }else if( t.getKind()==ITE ){ + }else if( t.getKind()==ITE && t.getType().isBoolean() ){ return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), - NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) ); + NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) ); }else if( t.getKind()==IFF ){ return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), - NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) ); + NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) ); } return Node::null(); } \ No newline at end of file diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 1e457f8ec..e4e34ce7f 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -317,8 +317,13 @@ public: int isInstanceOf( Node n1, Node n2 ); /** filter all nodes that have instances */ void filterInstances( std::vector< Node >& nodes ); + +//general utilities +public: /** simple check for contains term */ - bool containsTerm( Node n, Node t ); + static bool containsTerm( Node n, Node t ); + /** simple negate */ + static Node simpleNegate( Node n ); //for sygus private: @@ -374,8 +379,14 @@ public: TNode getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ); bool isVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); } int getVarNum( Node n ) { return d_fv_num[n]; } +private: + std::map< TypeNode, std::map< int, Node > > d_generic_base; + std::map< TypeNode, std::vector< Node > > d_generic_templ; + Node getGenericBase( TypeNode tn, const Datatype& dt, int c ); bool getMatch( Node p, Node n, std::map< int, Node >& s ); bool getMatch2( Node p, Node n, std::map< int, Node >& s, std::vector< int >& new_s ); +public: + bool getMatch( Node n, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc = -1, int index_start = 0 ); private: //information for sygus types std::map< TypeNode, TypeNode > d_register; //stores sygus type @@ -394,7 +405,6 @@ private: std::map< TypeNode, std::map< Node, Node > > d_normalized; std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin; std::map< TypeNode, std::map< Node, Node > > d_builtin_const_to_sygus; - std::map< TypeNode, std::map< int, Node > > d_generic_base; public: TermDbSygus(){} bool isRegistered( TypeNode tn ); @@ -432,7 +442,6 @@ public: Node getTypeMaxValue( TypeNode tn ); TypeNode getSygusType( Node v ); Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); - Node getGenericBase( TypeNode tn, int c ); Node sygusToBuiltin( Node n, TypeNode tn ); Node builtinToSygusConst( Node c, TypeNode tn ); Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ); -- 2.30.2