diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-04 15:25:16 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-04 15:25:16 +0100 |
commit | 42f269065fbb9204627a2ce483b27d3bc6fd91f4 (patch) | |
tree | 4e15f3844e8303c9f3bbdbc06c9673c27b39d870 | |
parent | 97e30c1089e42b668a914472b986f2d986190fc6 (diff) |
Work on solution reconstruction for single inv. Fix compiler error found by Tim regarding Trace.isOn
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 112 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 30 | ||||
-rw-r--r-- | 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; i<d_conj->d_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; i<to_erase.size(); i++ ){ + Trace("cegqi-si-rcons") << "......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-debug") << "Tried " << index << " for each type." << std::endl; + } + if( success ){ + reconstructed = 1; + } }while( !success ); - */ + }else{ + reconstructed = 0; } if( Trace.isOn("cegqi-si-debug-sol") ){ //debug solution @@ -900,6 +917,60 @@ bool CegConjectureSingleInv::pullITECondition( Node root, Node n_ite, std::vecto } } +Node CegConjectureSingleInv::flattenITEs( Node n, bool rec ) { + 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]; + 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 ); + 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; 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 @@ -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<t.getNumChildren(); i++ ){ collectReconstructNodes( tds, t[i], stn, parent, pstn, ignoreBoolean ); } @@ -1140,6 +1211,7 @@ void CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t, collectReconstructNodes( tds, t[i], stnc, t, stn, ignB ); } d_reconstructed[t][stn] = Node::fromExpr( dt[arg].getSygusOp() ); + d_reconstructed_op[t][stn] = true; processed = true; }else{ Trace("cegqi-si-rcons-debug") << " Type has kind " << t.getKind() << ", but argument mismatch, with parent " << parent << std::endl; @@ -1150,6 +1222,7 @@ void CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t, Trace("cegqi-si-rcons") << "...Reconstruction needed for " << t << " sygus type " << dt.getName() << " with parent " << parent << std::endl; }else{ d_reconstructed[t][stn] = Node::fromExpr( dt[carg].getSygusOp() ); + d_reconstructed_op[t][stn] = false; processed = true; Trace("cegqi-si-rcons-debug") << " Type has constant." << std::endl; } @@ -1178,9 +1251,11 @@ void CegConjectureSingleInv::setReconstructed( Node t, TypeNode stn ) { TypeNode stnc; for( std::map< TypeNode, bool >::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; i<t.getNumChildren(); i++ ){ + Node nc = getReconstructedSolution( stn, t[i] ); + children.push_back( nc ); + } + return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + }else{ + return it->second; + } + }else{ + Trace("cegqi-si-rcons-debug") << "*** error : missing reconstruction for " << t << std::endl; + Assert( false ); + return Node::null(); + } +} + }
\ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 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; j<n.getNumChildren(); j++ ){ + pre[j] = sygusToBuiltin( n[j], getArgType( dt[i], j ) ); + } + Node ret = mkGeneric( dt, i, var_count, pre ); + d_sygus_to_builtin[tn][n] = ret; + return ret; + }else{ + return it->second; + } +} + 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 ); }; |