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 \
namespace CVC4 {
-Node simpleNegate( Node n ){
- if( n.getKind()==OR || n.getKind()==AND ){
- std::vector< Node > children;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- children.push_back( simpleNegate( n[i] ) );
- }
- return NodeManager::currentNM()->mkNode( 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 ) {
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{
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() ){
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 );
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; i<prog_app.getNumChildren(); i++ ){
if( varList[i-1].getType().isBoolean() ){
//TODO force boolean term conversion mode
}else{
vars.push_back( prog_app[i] );
}
- subs.push_back( varList[i-1] );
- d_varlist.push_back( varList[i-1] );
+ d_varList.push_back( varList[i-1] );
+ d_sol->d_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; i<to_erase.size(); i++ ){
- Trace("cegqi-si-rcons-stats") << "......reconstructed all terms for type " << to_erase[i] << std::endl;
- d_rcons_to_process.erase( to_erase[i] );
- }
- index++;
- if( index%100==0 ){
- Trace("cegqi-si-rcons-stats") << "Tried " << index << " for each type." << std::endl;
- }
- if( success ){
- if( incomplete.empty() ){
- reconstructed = 1;
- Trace("cegqi-si-debug-sol") << "Reconstructing sygus solution..." << std::endl;
- d_sygus_solution = getReconstructedSolution( d_qe->getTermDatabaseSygus(), 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;
}
}
-bool CegConjectureSingleInv::debugSolution( Node sol ) {
- if( sol.getKind()==SKOLEM ){
- return false;
- }else{
- for( unsigned i=0; i<sol.getNumChildren(); i++ ){
- if( !debugSolution( sol[i] ) ){
- return false;
- }
- }
- return true;
- }
-
-}
-
-void CegConjectureSingleInv::debugTermSize( Node sol, int& t_size, int& num_ite ) {
- t_size++;
- if( sol.getKind()==ITE ){
- num_ite++;
- }
- for( unsigned i=0; i<sol.getNumChildren(); i++ ){
- debugTermSize( sol[i], t_size, num_ite );
- }
-}
-
-Node CegConjectureSingleInv::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("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<n_ite[0].getNumChildren(); i++ ){
- Node cond = n_ite[0][i];
- if( n_ite[0].getKind()==OR ){
- cond = simpleNegate( cond );
- }
- curr_conj.push_back( cond );
- }
- }else{
- Node neg = n_ite[0].negate();
- if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){
- isAnd = false;
- curr_conj.push_back( neg );
- }else{
- isAnd = true;
- curr_conj.push_back( n_ite[0] );
- }
- }
- // take intersection with current conditions
- std::vector< Node > 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; i<curr_conj.size(); i++ ){
- if( std::find( conj.begin(), conj.end(), curr_conj[i] )!=conj.end() ){
- new_conj.push_back( curr_conj[i] );
- }
- }
- Trace("cegqi-pull-ite") << "Pull ITE " << n_ite << ", #conj = " << conj.size() << " intersect " << curr_conj.size() << " = " << new_conj.size() << std::endl;
- }
- //cannot go further
- if( new_conj.empty() ){
- return false;
- }
- //it is an intersection with current
- conj.clear();
- conj.insert( conj.end(), new_conj.begin(), new_conj.end() );
- //recurse if possible
- Node trec = n_ite[ isAnd ? 2 : 1 ];
- Node tval = n_ite[ isAnd ? 1 : 2 ];
- bool success = false;
- if( trec.getKind()==ITE ){
- prev_conj.insert( prev_conj.end(), conj.begin(), conj.end() );
- success = pullITECondition( root, trec, conj, t, rem, depth+1 );
- }
- if( !success && depth>0 ){
- t = trec;
- rem = trec;
- success = true;
- if( trec.getKind()==ITE ){
- //restore previous state
- conj.clear();
- conj.insert( conj.end(), prev_conj.begin(), prev_conj.end() );
- }
- }
- if( success ){
- //make remainder : strip out conditions in conj
- Assert( !conj.empty() );
- std::vector< Node > cond_c;
- for( unsigned i=0; i<curr_conj.size(); i++ ){
- if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){
- cond_c.push_back( curr_conj[i] );
- }
- }
- if( cond_c.empty() ){
- rem = isAnd ? tval : rem;
- }else{
- Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c );
- rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval );
- }
- return true;
- }else{
- return false;
- }
-}
-
-Node CegConjectureSingleInv::flattenITEs( Node n, bool rec ) {
- Assert( !n.isNull() );
- if( n.getKind()==ITE ){
- Trace("csi-simp-debug") << "Flatten ITE : " << n << std::endl;
- Node ret;
- Node n0 = rec ? flattenITEs( n[0] ) : n[0];
- Node n1 = rec ? flattenITEs( n[1] ) : n[1];
- Node n2 = rec ? flattenITEs( n[2] ) : n[2];
- Assert( !n0.isNull() );
- Assert( !n1.isNull() );
- Assert( !n2.isNull() );
- if( n0.getKind()==NOT ){
- ret = NodeManager::currentNM()->mkNode( ITE, n0[0], n2, n1 );
- }else if( n0.getKind()==AND || n0.getKind()==OR ){
- std::vector< Node > children;
- for( unsigned i=1; i<n0.getNumChildren(); i++ ){
- children.push_back( n0[i] );
- }
- Node rem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( 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; i<n.getNumChildren(); i++ ){
- Node nc = flattenITEs( n[i] );
- children.push_back( nc );
- childChanged = childChanged || nc!=n[i];
- }
- if( !childChanged ){
- return n;
- }else{
- return NodeManager::currentNM()->mkNode( 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<n.getNumChildren(); i++ ){
- if( !getAssign( pol, n[i], assign, new_assign, vars, new_vars, new_subs, args ) ){
- return false;
- }
- }
- }else if( n.getKind()==NOT ){
- return getAssign( !pol, n[0], assign, new_assign, vars, new_vars, new_subs, args );
- }else if( pol && ( n.getKind()==IFF || n.getKind()==EQUAL ) ){
- getAssignEquality( n, vars, new_vars, new_subs, args );
- }
- }
- return true;
-}
-
-bool CegConjectureSingleInv::getAssignEquality( Node eq, std::vector< Node >& 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; i<new_assign.size(); i++ ){
- assign.erase( new_assign[i] );
- }
- }
- if( children.size()==1 || ( children.size()==2 && children[0]==children[1] ) ){
- return children[0];
- }else{
- Assert( children.size()==2 );
- Node ncond = simplifySolution( sol[0], assign, vars, subs, args, 0 );
- return NodeManager::currentNM()->mkNode( 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<sol.getNumChildren(); i++ ){
- bool do_exc = false;
- Node c = sol[i];
- 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, 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<ret.getNumChildren(); i++ ){
- children.push_back( ret[i] );
- }
- }else{
- children.push_back( ret );
- }
- }
- }else{
- //recurse on children
- for( unsigned i=0; i<inc.size(); i++ ){
- Node retc = simplifySolution( inc[i], assign, vars, subs, args, 0 );
- if( retc.isConst() ){
- if( retc==bc ){
- return bc;
- }
- }else{
- children.push_back( retc );
- }
- }
- }
- // now, remove all equalities that are implied
- std::vector< Node > final_children;
- for( unsigned i=0; i<children.size(); i++ ){
- bool red = false;
- Node atom = children[i].getKind()==NOT ? children[i][0] : children[i];
- bool pol = children[i].getKind()!=NOT;
- if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
- if( pol!=( sol.getKind()==AND ) ){
- std::vector< Node > 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; j<children.size(); j++ ){
- if( j!=i && ( j>i || 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; i<sol.getNumChildren(); i++ ){
- Node nc = simplifySolution( sol[i], assign, vars, subs, args, 0 );
- childChanged = childChanged || nc!=sol[i];
- children.push_back( nc );
- }
- if( childChanged ){
- return NodeManager::currentNM()->mkNode( 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; i<dt.getNumConstructors(); i++ ){
- Node g = tds->getGenericBase( 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<dt[i].getNumArgs(); j++ ){
- if( sigma[j].isNull() ){
- msuccess = false;
- break;
- }
- }
- if( msuccess ){
- std::map< TypeNode, int > 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; i<t.getNumChildren(); i++ ){
- TypeNode cstn = tds->getArgType( 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; i<t.getNumChildren(); i++ ){
- rem_children.push_back( t[i] );
- }
- Node t2 = NodeManager::currentNM()->mkNode( 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; i<rcons_child.size(); i++ ){
- setNeedsReconstruction( rcons_child[i], rcons_child_tn[i], ret, stn );
- }
- status = !rcons_set || !d_rcons_graph[0][ret][stn].empty() ? 1 : 0;
- if( rcons_set ){
- d_reconstructed[ret][stn] = rcons;
- d_reconstructed_op[ret][stn] = rcons_op;
- }
- d_rcons_processed[orig_t][stn] = ret;
- d_rcons_processed_status[orig_t][stn] = status;
- Trace("cegqi-si-rcons-debug") << "....return " << ret << " for " << orig_t << " in sygus type " << dt.getName() << ", status = " << status;
- Trace("cegqi-si-rcons-debug") << ", rcons=" << rcons << ", rcons op : " << rcons_op << std::endl;
- return ret;
- }else{
- status = d_rcons_processed_status[t][stn];
- return it->second;
- }
-}
-
-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<to_set.size(); i++ ){
- setReconstructed( to_set[i], to_set_tn[i] );
- }
-}
-
-Node CegConjectureSingleInv::getReconstructedSolution( TermDbSygus * tds, TypeNode stn, Node t ) {
- std::map< TypeNode, Node >::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; i<t.getNumChildren(); i++ ){
- TypeNode stnc = tds->getArgType( 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
#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 {
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 );
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
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
//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 );
};
}
--- /dev/null
+/********************* */
+/*! \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<sol.getNumChildren(); i++ ){
+ if( !debugSolution( sol[i] ) ){
+ return false;
+ }
+ }
+ return true;
+ }
+
+}
+
+void CegConjectureSingleInvSol::debugTermSize( Node sol, int& t_size, int& num_ite ) {
+ std::map< Node, int >::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; i<sol.getNumChildren(); i++ ){
+ debugTermSize( sol[i], t_size, num_ite );
+ }
+ d_dterm_size[sol] = t_size-prev;
+ d_dterm_ite_size[sol] = num_ite-prev_ite;
+ }else{
+ t_size += it->second;
+ 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<n_ite[0].getNumChildren(); i++ ){
+ Node cond = n_ite[0][i];
+ if( n_ite[0].getKind()==OR ){
+ cond = TermDb::simpleNegate( cond );
+ }
+ curr_conj.push_back( cond );
+ }
+ }else{
+ Node neg = n_ite[0].negate();
+ if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){
+ isAnd = false;
+ curr_conj.push_back( neg );
+ }else{
+ isAnd = true;
+ curr_conj.push_back( n_ite[0] );
+ }
+ }
+ // take intersection with current conditions
+ std::vector< Node > 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; i<curr_conj.size(); i++ ){
+ if( std::find( conj.begin(), conj.end(), curr_conj[i] )!=conj.end() ){
+ new_conj.push_back( curr_conj[i] );
+ }
+ }
+ Trace("csi-sol-debug") << "Pull ITE " << n_ite << ", #conj = " << conj.size() << " intersect " << curr_conj.size() << " = " << new_conj.size() << std::endl;
+ }
+ //cannot go further
+ if( new_conj.empty() ){
+ return false;
+ }
+ //it is an intersection with current
+ conj.clear();
+ conj.insert( conj.end(), new_conj.begin(), new_conj.end() );
+ //recurse if possible
+ Node trec = n_ite[ isAnd ? 2 : 1 ];
+ Node tval = n_ite[ isAnd ? 1 : 2 ];
+ bool success = false;
+ if( trec.getKind()==ITE ){
+ prev_conj.insert( prev_conj.end(), conj.begin(), conj.end() );
+ success = pullITECondition( root, trec, conj, t, rem, depth+1 );
+ }
+ if( !success && depth>0 ){
+ t = trec;
+ rem = trec;
+ success = true;
+ if( trec.getKind()==ITE ){
+ //restore previous state
+ conj.clear();
+ conj.insert( conj.end(), prev_conj.begin(), prev_conj.end() );
+ }
+ }
+ if( success ){
+ //make remainder : strip out conditions in conj
+ Assert( !conj.empty() );
+ std::vector< Node > cond_c;
+ for( unsigned i=0; i<curr_conj.size(); i++ ){
+ if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){
+ cond_c.push_back( curr_conj[i] );
+ }
+ }
+ if( cond_c.empty() ){
+ rem = isAnd ? tval : rem;
+ }else{
+ Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c );
+ rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval );
+ }
+ return true;
+ }else{
+ return false;
+ }
+}
+
+Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) {
+ Assert( !n.isNull() );
+ if( n.getKind()==ITE ){
+ Trace("csi-sol-debug") << "Flatten ITE." << std::endl;
+ Node ret;
+ Node n0 = rec ? flattenITEs( n[0] ) : n[0];
+ Node n1 = rec ? flattenITEs( n[1] ) : n[1];
+ Node n2 = rec ? flattenITEs( n[2] ) : n[2];
+ Assert( !n0.isNull() );
+ Assert( !n1.isNull() );
+ Assert( !n2.isNull() );
+ if( n0.getKind()==NOT ){
+ ret = NodeManager::currentNM()->mkNode( ITE, n0[0], n2, n1 );
+ }else if( n0.getKind()==AND || n0.getKind()==OR ){
+ std::vector< Node > children;
+ for( unsigned i=1; i<n0.getNumChildren(); i++ ){
+ children.push_back( n0[i] );
+ }
+ Node rem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( 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; i<n.getNumChildren(); i++ ){
+ Node nc = flattenITEs( n[i] );
+ children.push_back( nc );
+ childChanged = childChanged || nc!=n[i];
+ }
+ if( !childChanged ){
+ return n;
+ }else{
+ return NodeManager::currentNM()->mkNode( 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<n.getNumChildren(); i++ ){
+ if( !getAssign( pol, n[i], assign, new_assign, vars, new_vars, new_subs ) ){
+ return false;
+ }
+ }
+ }else if( n.getKind()==NOT ){
+ return getAssign( !pol, n[0], assign, new_assign, vars, new_vars, new_subs );
+ }else if( pol && ( n.getKind()==IFF || n.getKind()==EQUAL ) ){
+ getAssignEquality( n, vars, new_vars, new_subs );
+ }
+ }
+ return true;
+}
+
+bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& 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; i<dt[karg].getNumArgs(); i++ ){
+ stnc[i] = d_qe->getTermDatabaseSygus()->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; i<new_assign.size(); i++ ){
+ assign.erase( new_assign[i] );
+ }
+ }
+ if( children.size()==1 || ( children.size()==2 && children[0]==children[1] ) ){
+ return children[0];
+ }else{
+ Assert( children.size()==2 );
+ Node ncond = simplifySolutionNode( sol[0], stnc[0], assign, vars, subs, 0 );
+ Node ret = NodeManager::currentNM()->mkNode( 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<sol.getNumChildren(); i++ ){
+ bool do_exc = false;
+ Node c;
+ std::map< Node, bool >::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<ret.getNumChildren(); i++ ){
+ children.push_back( ret[i] );
+ }
+ }else{
+ children.push_back( ret );
+ }
+ }
+ }
+ }else{
+ //recurse on children
+ for( unsigned i=0; i<inc.size(); i++ ){
+ Node retc = simplifySolutionNode( inc[i], TypeNode::null(), assign, vars, subs, 0 );
+ if( retc.isConst() ){
+ if( retc==bc ){
+ return bc;
+ }
+ }else{
+ children.push_back( retc );
+ }
+ }
+ }
+ // now, remove all equalities that are implied
+ std::vector< Node > final_children;
+ for( unsigned i=0; i<children.size(); i++ ){
+ bool red = false;
+ Node atom = children[i].getKind()==NOT ? children[i][0] : children[i];
+ bool pol = children[i].getKind()!=NOT;
+ if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
+ if( pol!=( sol.getKind()==AND ) ){
+ std::vector< Node > 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; j<children.size(); j++ ){
+ if( j!=i && ( j>i || 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; i<sol.getNumChildren(); i++ ){
+ Node nc = simplifySolutionNode( sol[i], stnc[i], assign, vars, subs, 0 );
+ childChanged = childChanged || nc!=sol[i];
+ children.push_back( nc );
+ }
+ if( childChanged ){
+ return NodeManager::currentNM()->mkNode( 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<to_erase.size(); i++ ){
+ active.erase( to_erase[i] );
+ }
+ index++;
+ if( index%100==0 ){
+ Trace("csi-rcons-stats") << "Tried " << index << " for each type." << std::endl;
+ }
+ }while( !active.empty() );
+
+ //if solution is null, we ran out of elements, return the original solution
+ return sol;
+ }
+}
+
+int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, int& status ) {
+ std::map< Node, int >::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; i<min_t.getNumChildren(); i++ ){
+ rem_children.push_back( min_t[i] );
+ }
+ Node t2 = NodeManager::currentNM()->mkNode( 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<min_t.getNumChildren(); i++ ){
+ tchildren.push_back( min_t[i] );
+ }
+ }
+ //recurse on the children
+ if( tchildren.size()==dt[karg].getNumArgs() ){
+ Trace("csi-rcons-debug") << "Type for " << id << " has kind " << min_t.getKind() << ", recurse." << std::endl;
+ status = 0;
+ Node cons = Node::fromExpr( dt[karg].getConstructor() );
+ if( !collectReconstructNodes( id, tchildren, dt[karg], d_reconstruct_op[id][cons], status ) ){
+ Trace("csi-rcons-debug") << "...failure for " << id << " " << dt[karg].getName() << std::endl;
+ d_reconstruct_op[id].erase( cons );
+ status = 1;
+ }
+ }else{
+ Trace("csi-rcons-debug") << "Type for " << id << " has kind " << min_t.getKind() << ", but argument # mismatch." << std::endl;
+ }
+ }
+ }
+ if( status!=0 ){
+ Trace("csi-rcons-debug") << "Try matching for " << id << "." << std::endl;
+ //try other options
+ //match against other constructors
+ bool success;
+ int c_index = 0;
+ do{
+ success = false;
+ int index_found;
+ std::vector< Node > 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<args.size(); i++ ){
+ Trace("csi-rcons-debug") << " " << args[i] << std::endl;
+ }
+ if( !collectReconstructNodes( id, args, dt[index_found], d_reconstruct_op[id][cons], status ) ){
+ d_reconstruct_op[id].erase( cons );
+ status = 1;
+ }else{
+ c_index = index_found+1;
+ }
+ }
+ }while( success && status!=0 );
+
+ if( status!=0 ){
+ // construct an equivalence class of terms that are equivalent to t
+ if( d_rep[id]==id ){
+ Trace("csi-rcons-debug") << "Try rewriting for " << id << "." << std::endl;
+ //get equivalence class of term
+ std::vector< Node > 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<equiv.size(); i++ ){
+ Trace("csi-rcons-debug") << " " << equiv[i] << std::endl;
+ if( d_rcons_to_id[stn].find( equiv[i] )==d_rcons_to_id[stn].end() ){
+ int eq_id = allocate( equiv[i], stn );
+ d_eqc.erase( eq_id );
+ d_rep[eq_id] = id;
+ d_eqc[id].push_back( eq_id );
+ equiv_ids.push_back( eq_id );
+ }else{
+ equiv_ids.push_back( -1 );
+ }
+ }
+ // now, try each of them
+ for( unsigned i=0; i<equiv.size(); i++ ){
+ if( equiv_ids[i]!=-1 ){
+ collectReconstructNodes( equiv[i], stn, status );
+ //if one succeeds
+ if( status==0 ){
+ Node rsol = getReconstructedSolution( equiv_ids[i] );
+ Assert( !rsol.isNull() );
+ //set all members of the equivalence class that this is the reconstructed solution
+ setReconstructed( id, rsol );
+ break;
+ }
+ }
+ }
+ }else{
+ Trace("csi-rcons-debug") << "Do not try rewriting for " << id << ", rep = " << d_rep[id] << std::endl;
+ }
+ }
+ }
+ if( status!=0 ){
+ Trace("csi-rcons-debug") << "-> *** 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; i<ts.size(); i++ ){
+ TypeNode cstn = d_qe->getTermDatabaseSygus()->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; i<ids.size(); i++ ){
+ d_parents[ids[i]].push_back( pid );
+ }
+ return true;
+}
+
+ /*
+ //flatten ITEs if necessary TODO : carry assignment or move this elsewhere
+ 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("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; i<itt->second.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<d_eqc[rid].size(); i++ ){
+ int tid = d_eqc[rid][i];
+ if( tid!=id ){
+ Node eret = getReconstructedSolution( tid, false );
+ if( !eret.isNull() ){
+ setReconstructed( id, eret );
+ return eret;
+ }
+ }
+ }
+ }
+ d_tmp_fail.push_back( id );
+ return Node::null();
+ }
+ }
+}
+
+int CegConjectureSingleInvSol::allocate( Node n, TypeNode stn ) {
+ std::map< Node, int >::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_parents[rid].size(); j++ ){
+ if( getPathToRoot( d_parents[rid][j] ) ){
+ return true;
+ }
+ }
+ return false;
+ }
+ }
+}
+
+void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) {
+ //set all equivalent to this as reconstructed
+ int rid = d_rep[id];
+ for( unsigned i=0; i<d_eqc[rid].size(); i++ ){
+ d_reconstruct[d_eqc[rid][i]] = n;
+ }
+}
+
+}
--- /dev/null
+/********************* */
+/*! \file ce_guided_single_inv_sol.h
+ ** \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 reconstructing solutions for single invocation synthesis conjectures
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
+#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
+
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+
+class CegConjectureSingleInv;
+
+class CegConjectureSingleInvSol
+{
+ friend class CegConjectureSingleInv;
+private:
+ QuantifiersEngine * d_qe;
+ std::vector< Node > 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
}
}
+Node TermDb::simpleNegate( Node n ){
+ if( n.getKind()==OR || n.getKind()==AND ){
+ std::vector< Node > children;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ children.push_back( simpleNegate( n[i] ) );
+ }
+ return NodeManager::currentNM()->mkNode( 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() ){
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<dt.getNumConstructors(); i++ ){
+ if( (int)i!=index_exc ){
+ Node g = getGenericBase( st, dt, i );
+ gens.push_back( g );
+ kgens[g.getKind()].push_back( g );
+ Trace("sygus-db-debug") << "Check generic base : " << g << " from " << dt[i].getName() << std::endl;
+ if( g.getKind()==t.getKind() ){
+ Trace("sygus-db-debug") << "Possible match ? " << g << " " << t << " for " << dt[i].getName() << std::endl;
+ std::map< int, Node > sigma;
+ if( getMatch( g, t, sigma ) ){
+ //we found an exact match
+ bool msuccess = true;
+ for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+ if( sigma[j].isNull() ){
+ msuccess = false;
+ break;
+ }else{
+ args.push_back( sigma[j] );
+ }
+ }
+ if( msuccess ){
+ index_found = i;
+ return true;
+ }
+ //we found an exact match
+ //std::map< TypeNode, int > 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; i<it->second.size(); i++ ){
+ for( unsigned j=0; j<it->second.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() );
}
}
-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() ){
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{
}
return 1+sum;
}
-
}
bool TermDbSygus::isAssoc( Kind k ) {
}
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++ ){
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
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:
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
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 );
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 );
projects / cvc5.git / commitdiff