From 42f269065fbb9204627a2ce483b27d3bc6fd91f4 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 4 Feb 2015 15:25:16 +0100 Subject: [PATCH] Work on solution reconstruction for single inv. Fix compiler error found by Tim regarding Trace.isOn --- .../quantifiers/ce_guided_instantiation.cpp | 10 +- .../quantifiers/ce_guided_single_inv.cpp | 112 ++++++++++++++++-- src/theory/quantifiers/ce_guided_single_inv.h | 6 +- src/theory/quantifiers/term_database.cpp | 30 ++++- src/theory/quantifiers/term_database.h | 4 +- 5 files changed, 144 insertions(+), 18 deletions(-) diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 2044d612c..3475e9e97 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -477,7 +477,7 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le void CegInstantiation::printSynthSolution( std::ostream& out ) { if( d_conj ){ - if( !Trace.isOn("cegqi-stats") ){ + if( !(Trace.isOn("cegqi-stats")) ){ out << "Solution:" << std::endl; } for( unsigned i=0; id_candidates.size(); i++ ){ @@ -491,19 +491,21 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { Assert( dt.isSygus() ); //get the solution Node sol; + int status; if( d_last_inst_si ){ Assert( d_conj->d_ceg_si ); - sol = d_conj->d_ceg_si->getSolution( d_quantEngine, tn, i, Node::fromExpr( dt.getSygusVarList() ) ); + sol = d_conj->d_ceg_si->getSolution( d_quantEngine, i, tn, status ); }else{ if( !d_conj->d_candidate_inst[i].empty() ){ sol = d_conj->d_candidate_inst[i].back(); + status = 1; } } - if( !Trace.isOn("cegqi-stats") ){ + if( !(Trace.isOn("cegqi-stats")) ){ out << "(define-fun " << f << " "; out << dt.getSygusVarList() << " "; out << dt.getSygusType() << " "; - if( d_last_inst_si ){ + if( status==0 ){ out << sol; }else{ if( sol.isNull() ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index be20dd7c0..e22674414 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -679,9 +679,11 @@ Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) { } } -Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn, unsigned i, Node varList ){ +Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, 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() ); //TODO : not in grammar Node prog = d_quant[0][i]; Node prog_app = d_single_inv_app_map[prog]; @@ -697,6 +699,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn, 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 ); @@ -709,7 +712,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn, s = Rewriter::rewrite( s ); Trace("cegqi-si-debug-sol") << "Solution (post-rewrite): " << s << std::endl; d_solution = s; - if( options::cegqiSingleInvReconstruct() ){ + if( options::cegqiSingleInvReconstruct() && !stn.isNull() ){ collectReconstructNodes( qe->getTermDatabaseSygus(), d_solution, stn, Node::null(), TypeNode::null(), false ); 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 ){ @@ -723,7 +726,6 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn, Assert( !it->second.empty() ); rcons_tn.push_back( it->first ); } - /* bool success; unsigned index = 0; do { @@ -733,17 +735,32 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn, if( it->second.empty() ){ to_erase.push_back( it->first ); }else{ - Node n = qe->getTermDatabase()->getEnumerateType( it->first, index ); - + Node ns = qe->getTermDatabase()->getEnumerateTerm( it->first, index ); + Node nb = qe->getTermDatabaseSygus()->sygusToBuiltin( ns, it->first ); + Node nr = Rewriter::rewrite( nb );//qe->getTermDatabaseSygus()->getNormalized( it->first, nb, false, false ); + if( it->second.find( nr )!=it->second.end() ){ + Trace("cegqi-si-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl; + d_reconstructed[nr][it->first] = ns; + d_reconstructed_op[nr][it->first] = false; + setReconstructed( nr, it->first ); + } success = false; } } 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 ); + Node ret; + if( n0.getKind()==AND ){ + ret = NodeManager::currentNM()->mkNode( ITE, rem, NodeManager::currentNM()->mkNode( n0[0], n1, n2 ), n2 ); + }else{ + ret = NodeManager::currentNM()->mkNode( ITE, rem, n1, NodeManager::currentNM()->mkNode( 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 ); + } + return flattenITEs( ret, false ); + }else{ + if( n.getNumChildren()>0 ){ + std::vector< Node > children; + 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 @@ -1114,7 +1185,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol, void CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, Node parent, TypeNode pstn, bool ignoreBoolean ) { if( ignoreBoolean && t.getType().isBoolean() ){ - if( t.getKind()==OR || t.getKind()==AND || t.getKind()==IFF || t.getKind()==ITE ){ + if( t.getKind()==OR || t.getKind()==AND || t.getKind()==IFF || t.getKind()==ITE || t.getKind()==NOT ){ //FIXME for( unsigned i=0; i::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ stnc = it2->first; - d_rcons_graph[ro][it->first][stnc][t].erase( it2->first ); + d_rcons_graph[ro][it->first][stnc][t].erase( stn ); if( d_rcons_graph[ro][it->first][stnc][t].empty() ){ d_rcons_graph[ro][it->first][stnc].erase( t ); + }else{ + Trace("cegqi-si-rcons-debug") << " " << ( r==0 ? "child" : "parent" ) << " " << it->first << " now has " << d_rcons_graph[ro][it->first][stnc][t].size() << std::endl; } } if( d_rcons_graph[ro][it->first][stnc].empty() ){ @@ -1198,6 +1273,27 @@ void CegConjectureSingleInv::setReconstructed( Node t, TypeNode stn ) { } } +Node CegConjectureSingleInv::getReconstructedSolution( 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] ){ + std::vector< Node > children; + children.push_back( it->second ); + for( unsigned i=0; imkNode( APPLY_CONSTRUCTOR, children ); + }else{ + return it->second; + } + }else{ + Trace("cegqi-si-rcons-debug") << "*** error : missing reconstruction for " << t << std::endl; + Assert( false ); + return Node::null(); + } +} + } \ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index afd7167f2..7667ccf11 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -76,7 +76,7 @@ public: //check void check( QuantifiersEngine * qe, std::vector< Node >& lems ); //get solution - Node getSolution( QuantifiersEngine * qe, TypeNode stn, unsigned i, Node varList ); + Node getSolution( QuantifiersEngine * qe, unsigned i, TypeNode stn, int& reconstructed ); //solution simplification @@ -85,6 +85,7 @@ private: 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( QuantifiersEngine * qe, Node sol, std::map< Node, bool >& assign, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status ); bool getAssign( QuantifiersEngine * qe, bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, @@ -94,12 +95,15 @@ private: private: std::map< Node, std::vector< TypeNode > > d_rcons_processed; 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; // term t with sygus type st void collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, Node parent, TypeNode pstn, bool ignoreBoolean ); // set reconstructed void setReconstructed( Node t, TypeNode stn ); + // get solution + Node getReconstructedSolution( TypeNode stn, Node t ); }; } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 24d7cbb5c..c5a3cec4d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1400,6 +1400,26 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int } } +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() ){ + Assert( n.getKind()==APPLY_CONSTRUCTOR ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + unsigned i = Datatype::indexOf( n.getOperator().toExpr() ); + Assert( n.getNumChildren()==dt[i].getNumArgs() ); + std::map< TypeNode, int > var_count; + std::map< int, Node > pre; + for( unsigned j=0; jsecond; + } +} + Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ) { return n; if( n.getKind()==SKOLEM ){ @@ -1436,7 +1456,7 @@ Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_cou } } -Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm ) { +Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm, bool do_post_norm ) { if( do_pre_norm ){ std::map< TypeNode, int > var_count; std::map< Node, Node > subs; @@ -1446,9 +1466,11 @@ Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm ) { if( itn==d_normalized[t].end() ){ Node progr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( prog.toExpr() ) ); progr = Rewriter::rewrite( progr ); - std::map< TypeNode, int > var_count; - std::map< Node, Node > subs; - progr = getSygusNormalized( progr, var_count, subs ); + if( do_post_norm ){ + std::map< TypeNode, int > var_count; + std::map< Node, Node > subs; + progr = getSygusNormalized( progr, var_count, subs ); + } Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl; d_normalized[t][prog] = progr; return progr; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index ce3a52d1c..0f730929c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -388,6 +388,7 @@ private: std::map< TypeNode, std::map< Node, std::map< int, int > > > d_type_value_offset_status; //normalized map std::map< TypeNode, std::map< Node, Node > > d_normalized; + std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin; public: TermDbSygus(){} bool isRegistered( TypeNode tn ); @@ -425,8 +426,9 @@ public: Node getTypeMaxValue( TypeNode tn ); TypeNode getSygusType( Node v ); Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); + Node sygusToBuiltin( Node n, TypeNode tn ); Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ); - Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false ); + Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true ); int getTermSize( Node n ); }; -- 2.30.2