From ef4bac5d6082c21afc43c896552290d3026ede75 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 Aug 2019 14:34:38 -0500 Subject: [PATCH] Remove simplification specialized for sygus si solution reconstruction (#3147) --- .../sygus/ce_guided_single_inv.cpp | 4 +- .../sygus/ce_guided_single_inv_sol.cpp | 561 ------------------ .../sygus/ce_guided_single_inv_sol.h | 14 - test/regress/CMakeLists.txt | 7 +- 4 files changed, 6 insertions(+), 580 deletions(-) diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 3fbb4eaee..e4f16de65 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -614,9 +614,9 @@ Node CegSingleInv::getSolution(unsigned sol_index, } d_orig_solution = s; - //simplify the solution + //simplify the solution using the extended rewriter Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl; - s = d_sol->simplifySolution( s, stn ); + s = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s); Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl; return reconstructToSyntax( s, stn, reconstructed, rconsSygus ); } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 074971622..b74caf49a 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -83,567 +83,6 @@ void CegSingleInvSol::debugTermSize(Node sol, int& t_size, int& num_ite) } } -Node CegSingleInvSol::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 ); - Trace("csi-pull-ite") << "PI: Rewrite : " << s << std::endl; - Node prev = s; - s = NodeManager::currentNM()->mkNode( ITE, TermUtil::simpleNegate( cond ), t, rem ); - Trace("csi-pull-ite") << "PI: Rewrite Now : " << s << std::endl; - Trace("csi-pull-ite") << "(= " << prev << " " << s << ")" << std::endl; - success = true; - } - }while( success ); - } - return s; -} - -// pull condition common to all ITE conditions in path of size > 1 -bool CegSingleInvSol::pullITECondition(Node root, - Node n_ite, - std::vector& conj, - Node& t, - Node& rem, - int depth) -{ - Assert( n_ite.getKind()==ITE ); - std::vector< Node > curr_conj; - std::vector< Node > orig_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()==EQUAL && n0[0].getType().isBoolean() ){ - 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 CegSingleInvSol::getAssign(bool pol, - Node n, - std::map& assign, - std::vector& new_assign, - std::vector& vars, - std::vector& new_vars, - std::vector& 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->getTermUtil()->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& new_vars, - std::vector& new_subs) -{ - Assert( 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 (!expr::hasSubterm(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; - } - } - } - } - return false; -} - -Node CegSingleInvSol::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 CegSingleInvSol::simplifySolutionNode(Node sol, - TypeNode stn, - std::map& assign, - std::vector& vars, - std::vector& 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()->getKindConsNum( 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-simp-debug") << "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->getTermUtil()->d_true : d_qe->getTermUtil()->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()==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 ? inc[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->getTermUtil()->d_false : d_qe->getTermUtil()->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; - } -} - void CegSingleInvSol::preregisterConjecture(Node q) { Trace("csi-sol") << "Preregister conjecture : " << q << std::endl; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h index 40117af6c..6a00bc467 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h @@ -45,23 +45,9 @@ class CegSingleInvSol 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: CegSingleInvSol(QuantifiersEngine* qe); - /** simplify solution - * - * Returns the simplified version of node sol whose syntax is restricted by - * the grammar corresponding to sygus datatype stn. - */ - Node simplifySolution( Node sol, TypeNode stn ); /** reconstruct solution * * Returns (if possible) a node that is equivalent to sol those syntax diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 19e5fa899..9a1e5d6dc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1635,9 +1635,7 @@ set(regress_1_tests regress1/sygus-abduct-test-user.smt2 regress1/sygus/VC22_a.sy regress1/sygus/abv.sy - regress1/sygus/array_search_2.sy regress1/sygus/array_search_5-Q-easy.sy - regress1/sygus/array_sum_2_5.sy regress1/sygus/bvudiv-by-2.sy regress1/sygus/car_3.lus.sy regress1/sygus/cegar1.sy @@ -1652,7 +1650,6 @@ set(regress_1_tests regress1/sygus/constant-ite-bv.sy regress1/sygus/constant.sy regress1/sygus/crci-ssb-unk.sy - regress1/sygus/crcy-si-rcons.sy regress1/sygus/crcy-si.sy regress1/sygus/cube-nia.sy regress1/sygus/double.sy @@ -2176,6 +2173,10 @@ set(regression_disabled_tests regress1/sygus/Base16_1.sy regress1/sygus/enum-test.sy regress1/sygus/inv_gen_fig8.sy + # rely on heuristic solution reconstruction TODO #3146 revisit + regress1/sygus/array_search_2.sy + regress1/sygus/array_sum_2_5.sy + regress1/sygus/crcy-si-rcons.sy regress2/arith/arith-int-098.cvc regress2/arith/miplib-opt1217--27.smt2 regress2/arith/miplib-pp08a-3000.smt2 -- 2.30.2