From: Andrew Reynolds Date: Sat, 28 Oct 2017 18:01:49 +0000 (-0500) Subject: Sygus process conjecture (#1286) X-Git-Tag: cvc5-1.0.0~5524 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=49912baa48d87e6d8c38f9bc3e1739b8fbe4e8b3;p=cvc5.git Sygus process conjecture (#1286) * Initial infrastructure for static preprocessing for sygus conjectures. * Initial infrastructure. * Minor change in terminology, move enumerator to synth-fun mapping to sygus term database, minor fix and add documentation to NegContainsInvarianceTest. * Clang format * Fixing comments, more initial infrastructure. * More * Minor * New clang format. * Address review. --- diff --git a/src/Makefile.am b/src/Makefile.am index b05a3503c..0bcd35215 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -420,6 +420,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/rewrite_engine.h \ theory/quantifiers/sygus_grammar_cons.cpp \ theory/quantifiers/sygus_grammar_cons.h \ + theory/quantifiers/sygus_process_conj.cpp \ + theory/quantifiers/sygus_process_conj.h \ theory/quantifiers/symmetry_breaking.cpp \ theory/quantifiers/symmetry_breaking.h \ theory/quantifiers/term_database.cpp \ diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 4999114eb..f27a852d9 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -262,7 +262,7 @@ void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) { registerSizeTerm( n, lemmas ); if( d_register_st[n] ){ d_term_to_anchor[n] = n; - d_term_to_anchor_conj[n] = d_tds->getConjectureFor(n); + d_term_to_anchor_conj[n] = d_tds->getConjectureForEnumerator(n); // this assertion fails if we have a sygus term in the search that is unmeasured Assert(d_term_to_anchor_conj[n] != NULL); d = 0; @@ -361,29 +361,54 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: Trace("sygus-sb-fair-debug") << "Tester " << exp << " is for depth " << d << " term in search size " << ssz << std::endl; //Assert( d<=ssz ); if( options::sygusSymBreakLazy() ){ + // dynamic symmetry breaking addSymBreakLemmasFor( ntn, n, d, lemmas ); } - - // process simple symmetry breaking + unsigned max_depth = ssz>=d ? ssz-d : 0; unsigned min_depth = d_simple_proc[exp]; if( min_depth<=max_depth ){ TNode x = getFreeVar( ntn ); - Node rlv = getRelevancyCondition( n ); - for( unsigned d=0; d<=max_depth; d++ ){ - Node simple_sb_pred = getSimpleSymBreakPred( ntn, tindex, d ); - if( !simple_sb_pred.isNull() ){ - simple_sb_pred = simple_sb_pred.substitute( x, n ); - if( !rlv.isNull() ){ - simple_sb_pred = NodeManager::currentNM()->mkNode( kind::OR, rlv.negate(), simple_sb_pred ); + std::vector sb_lemmas; + for (unsigned ds = 0; ds <= max_depth; ds++) + { + // static conjecture-independent symmetry breaking + Node ipred = getSimpleSymBreakPred(ntn, tindex, ds); + if (!ipred.isNull()) + { + sb_lemmas.push_back(ipred); + } + // static conjecture-dependent symmetry breaking + std::map::iterator itc = + d_term_to_anchor_conj.find(n); + if (itc != d_term_to_anchor_conj.end()) + { + quantifiers::CegConjecture* conj = itc->second; + Assert(conj != NULL); + Node dpred = conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds); + if (!dpred.isNull()) + { + sb_lemmas.push_back(dpred); } - lemmas.push_back( simple_sb_pred ); } } + + // add the above symmetry breaking predicates to lemmas + Node rlv = getRelevancyCondition(n); + for (unsigned i = 0; i < sb_lemmas.size(); i++) + { + Node pred = sb_lemmas[i].substitute(x, n); + if (!rlv.isNull()) + { + pred = NodeManager::currentNM()->mkNode(kind::OR, rlv.negate(), pred); + } + lemmas.push_back(pred); + } } d_simple_proc[exp] = max_depth + 1; - - // add back testers for the children if they exist + + // now activate the children those testers were previously asserted in this + // context and are awaiting activation, if they exist. if( options::sygusSymBreakLazy() ){ for( unsigned j=0; jmkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( ntn.toType(), j ) ), n ); @@ -1054,9 +1079,10 @@ void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) { if( e.getType().isDatatype() ){ const Datatype& dt = ((DatatypeType)(e.getType()).toType()).getDatatype(); if( dt.isSygus() ){ - if (d_tds->isMeasuredTerm(e)) { + if (d_tds->isEnumerator(e)) + { d_register_st[e] = true; - Node ag = d_tds->getActiveGuardForMeasureTerm( e ); + Node ag = d_tds->getActiveGuardForEnumerator(e); if( !ag.isNull() ){ d_anchor_to_active_guard[e] = ag; } @@ -1157,10 +1183,11 @@ unsigned SygusSymBreakNew::getSearchSizeForAnchor( Node a ) { Trace("sygus-sb-debug2") << "get search size for anchor : " << a << std::endl; std::map< Node, Node >::iterator it = d_anchor_to_measure_term.find( a ); Assert( it!=d_anchor_to_measure_term.end() ); - return getSearchSizeForMeasureTerm( it->second ); + return getSearchSizeForMeasureTerm(it->second); } -unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm( Node m ) { +unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm(Node m) +{ Trace("sygus-sb-debug2") << "get search size for measure : " << m << std::endl; std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m ); Assert( its!=d_szinfo.end() ); @@ -1243,7 +1270,7 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { } //register any measured terms that we haven't encountered yet (should only be invoked on first call to check std::vector< Node > mts; - d_tds->getMeasuredTerms( mts ); + d_tds->getEnumerators(mts); for( unsigned i=0; i& top_level, std::map< Node, unsigned >& tdepth, std::vector< Node >& lemmas ); bool debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas ); diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index a380dcbf2..7fcc3f2af 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -48,12 +48,14 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe) d_refine_count = 0; d_ceg_si = new CegConjectureSingleInv(qe, this); d_ceg_pbe = new CegConjecturePbe(qe, this); + d_ceg_proc = new CegConjectureProcess(qe); d_ceg_gc = new CegGrammarConstructor(qe); } CegConjecture::~CegConjecture() { delete d_ceg_si; delete d_ceg_pbe; + delete d_ceg_proc; delete d_ceg_gc; } @@ -63,12 +65,16 @@ void CegConjecture::assign( Node q ) { Trace("cegqi") << "CegConjecture : assign : " << q << std::endl; d_quant = q; + // simplify the quantified formula based on the process utility + d_simp_quant = d_ceg_proc->simplify(d_quant); + std::map< Node, Node > templates; std::map< Node, Node > templates_arg; //register with single invocation if applicable - if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){ - d_ceg_si->initialize( d_quant ); - q = d_ceg_si->getSimplifiedConjecture(); + if (d_qe->getQuantAttributes()->isSygus(q)) + { + d_ceg_si->initialize(d_simp_quant); + d_simp_quant = d_ceg_si->getSimplifiedConjecture(); // carry the templates for( unsigned i=0; iprocess( q, templates, templates_arg ); + d_embed_quant = d_ceg_gc->process(d_simp_quant, templates, templates_arg); Trace("cegqi") << "CegConjecture : converted to embedding : " << d_embed_quant << std::endl; // we now finalize the single invocation module, based on the syntax restrictions - if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){ + if (d_qe->getQuantAttributes()->isSygus(q)) + { d_ceg_si->finishInit( d_ceg_gc->isSyntaxRestricted(), d_ceg_gc->hasSyntaxITE() ); } @@ -99,22 +106,25 @@ void CegConjecture::assign( Node q ) { Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl; //construct base instantiation d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( d_embed_quant, vars, d_candidates ) ); - - // register this term with sygus database + Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; + + // register this term with sygus database and other utilities that impact + // the enumerative sygus search std::vector< Node > guarded_lemmas; if( !isSingleInvocation() ){ + d_ceg_proc->initialize(d_base_inst, d_candidates); if( options::sygusPbe() ){ - d_ceg_pbe->initialize( d_base_inst, d_candidates, guarded_lemmas ); + d_ceg_pbe->initialize(d_base_inst, d_candidates, guarded_lemmas); } else { for (unsigned i = 0; i < d_candidates.size(); i++) { Node e = d_candidates[i]; - d_qe->getTermDatabaseSygus()->registerMeasuredTerm(e, this); + d_qe->getTermDatabaseSygus()->registerEnumerator(e, e, this); } } } - - Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; - if( d_qe->getQuantAttributes()->isSygus( d_quant ) ){ + + if (d_qe->getQuantAttributes()->isSygus(q)) + { collectDisjuncts( d_base_inst, d_base_disj ); Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; //store the inner variables for each disjunct @@ -130,7 +140,9 @@ void CegConjecture::assign( Node q ) { } } d_syntax_guided = true; - }else if( d_qe->getQuantAttributes()->isSynthesis( d_quant ) ){ + } + else if (d_qe->getQuantAttributes()->isSynthesis(q)) + { d_syntax_guided = false; }else{ Assert( false ); @@ -612,6 +624,33 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation } } +Node CegConjecture::getSymmetryBreakingPredicate( + Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth) +{ + std::vector sb_lemmas; + + // based on simple preprocessing + Node ppred = + d_ceg_proc->getSymmetryBreakingPredicate(x, e, tn, tindex, depth); + if (!ppred.isNull()) + { + sb_lemmas.push_back(ppred); + } + + // other static conjecture-dependent symmetry breaking goes here + + if (!sb_lemmas.empty()) + { + return sb_lemmas.size() == 1 + ? sb_lemmas[0] + : NodeManager::currentNM()->mkNode(kind::AND, sb_lemmas); + } + else + { + return Node::null(); + } +} + }/* namespace CVC4::theory::quantifiers */ }/* namespace CVC4::theory */ }/* namespace CVC4 */ diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h index dfd9c1623..b725449b4 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.h +++ b/src/theory/quantifiers/ce_guided_conjecture.h @@ -18,9 +18,10 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H -#include "theory/quantifiers/ce_guided_single_inv.h" #include "theory/quantifiers/ce_guided_pbe.h" +#include "theory/quantifiers/ce_guided_single_inv.h" #include "theory/quantifiers/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus_process_conj.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -31,10 +32,8 @@ namespace quantifiers { * This class implements approaches for a synthesis conecjture, given by data * member d_quant. * This includes both approaches for synthesis in Reynolds et al CAV 2015. It - * determines - * which approach and optimizations are applicable to the conjecture, and has - * interfaces for - * implementing them. + * determines which approach and optimizations are applicable to the + * conjecture, and has interfaces for implementing them. */ class CegConjecture { public: @@ -46,7 +45,10 @@ public: Node getEmbeddedConjecture() { return d_embed_quant; } /** get next decision request */ Node getNextDecisionRequest( unsigned& priority ); - /** increment the number of times we have successfully done candidate refinement */ + + //-------------------------------for counterexample-guided check/refine + /** increment the number of times we have successfully done candidate + * refinement */ void incrementRefineCount() { d_refine_count++; } /** whether the conjecture is waiting for a call to doCheck below */ bool needsCheck( std::vector< Node >& lem ); @@ -73,6 +75,8 @@ public: /** Print the synthesis solution * singleInvocation is whether the solution was found by single invocation techniques. */ + //-------------------------------end for counterexample-guided check/refine + void printSynthSolution( std::ostream& out, bool singleInvocation ); /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */ Node getGuard(); @@ -96,14 +100,21 @@ public: void getModelValues( std::vector< Node >& n, std::vector< Node >& v ); /** get model value for term n */ Node getModelValue( Node n ); + + //-----------------------------------refinement lemmas /** get number of refinement lemmas we have added so far */ unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); } /** get refinement lemma */ Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; } /** get refinement lemma */ Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; } + //-----------------------------------end refinement lemmas + /** get program by examples utility */ CegConjecturePbe* getPbe() { return d_ceg_pbe; } + /** get the symmetry breaking predicate for type */ + Node getSymmetryBreakingPredicate( + Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth); /** print out debug information about this conjecture */ void debugPrint( const char * c ); private: @@ -113,11 +124,18 @@ private: CegConjectureSingleInv * d_ceg_si; /** program by examples utility */ CegConjecturePbe * d_ceg_pbe; + /** utility for static preprocessing and analysis of conjectures */ + CegConjectureProcess* d_ceg_proc; /** grammar utility */ CegGrammarConstructor * d_ceg_gc; - /** list of constants for quantified formula */ + /** list of constants for quantified formula + * The Skolems for the negation of d_embed_quant. + */ std::vector< Node > d_candidates; - /** base instantiation */ + /** base instantiation + * If d_embed_quant is forall d. exists y. P( d, y ), then + * this is the formula P( candidates, y ). + */ Node d_base_inst; /** expand base inst to disjuncts */ std::vector< Node > d_base_disj; @@ -126,12 +144,18 @@ private: std::vector< std::vector< Node > > d_inner_vars_disj; /** current extential quantifeirs whose couterexamples we must refine */ std::vector< std::vector< Node > > d_ce_sk; + + //-----------------------------------refinement lemmas /** refinement lemmas */ std::vector< Node > d_refinement_lemmas; std::vector< Node > d_refinement_lemmas_base; + //-----------------------------------end refinement lemmas + /** quantified formula asserted */ Node d_quant; - /** quantified formula (after processing) */ + /** quantified formula (after simplification) */ + Node d_simp_quant; + /** quantified formula (after simplification, conversion to deep embedding) */ Node d_embed_quant; /** candidate information */ class CandidateInfo { diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp index e4bf43963..cadfbbe86 100644 --- a/src/theory/quantifiers/ce_guided_pbe.cpp +++ b/src/theory/quantifiers/ce_guided_pbe.cpp @@ -45,7 +45,8 @@ void print_val( const char * c, std::vector< Node >& vals, bool pol = true ){ } } -void CegConjecturePbe::print_role( const char * c, unsigned r ){ +void CegConjecturePbe::print_role(const char* c, unsigned r) +{ switch(r){ case CegConjecturePbe::enum_io:Trace(c) << "IO";break; case CegConjecturePbe::enum_ite_condition:Trace(c) << "CONDITION";break; @@ -55,12 +56,14 @@ void CegConjecturePbe::print_role( const char * c, unsigned r ){ } } -void CegConjecturePbe::print_strat( const char * c, unsigned s ){ - switch(s){ - case CegConjecturePbe::strat_ITE:Trace(c) << "ITE";break; - case CegConjecturePbe::strat_CONCAT:Trace(c) << "CONCAT";break; - case CegConjecturePbe::strat_ID:Trace(c) << "ID";break; - default:Trace(c) << "strat_" << s;break; +void CegConjecturePbe::print_strat(const char* c, unsigned s) +{ + switch (s) + { + case CegConjecturePbe::strat_ITE: Trace(c) << "ITE"; break; + case CegConjecturePbe::strat_CONCAT: Trace(c) << "CONCAT"; break; + case CegConjecturePbe::strat_ID: Trace(c) << "ID"; break; + default: Trace(c) << "strat_" << s; break; } } @@ -144,7 +147,10 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, } } -void CegConjecturePbe::initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas ) { +void CegConjecturePbe::initialize(Node n, + std::vector& candidates, + std::vector& lemmas) +{ Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl; for( unsigned i=0; i& candidates, std: if( !d_is_pbe ){ Trace("sygus-unif") << "Do not do PBE optimizations, register..." << std::endl; for( unsigned i=0; igetTermDatabaseSygus()->registerMeasuredTerm(candidates[i], - d_parent); + d_qe->getTermDatabaseSygus()->registerEnumerator( + candidates[i], candidates[i], d_parent); } } } @@ -211,7 +217,6 @@ void CegConjecturePbe::initialize( Node n, std::vector< Node >& candidates, std: Node CegConjecturePbe::PbeTrie::addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe, unsigned index, unsigned ntotal) { - Assert(cpbe->getNumExamples(e) == ntotal); if (index == ntotal) { // lazy child holds the leaf data if (d_lazy_child.isNull()) { @@ -253,7 +258,8 @@ Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b, bool CegConjecturePbe::hasExamples(Node e) { if (isPbe()) { - e = getSynthFunctionForEnumerator(e); + e = d_tds->getSynthFunForEnumerator(e); + Assert(!e.isNull()); std::map::iterator itx = d_examples_invalid.find(e); if (itx == d_examples_invalid.end()) { return d_examples.find(e) != d_examples.end(); @@ -263,7 +269,8 @@ bool CegConjecturePbe::hasExamples(Node e) { } unsigned CegConjecturePbe::getNumExamples(Node e) { - e = getSynthFunctionForEnumerator(e); + e = d_tds->getSynthFunForEnumerator(e); + Assert(!e.isNull()); std::map > >::iterator it = d_examples.find(e); if (it != d_examples.end()) { @@ -274,7 +281,8 @@ unsigned CegConjecturePbe::getNumExamples(Node e) { } void CegConjecturePbe::getExample(Node e, unsigned i, std::vector& ex) { - e = getSynthFunctionForEnumerator(e); + e = d_tds->getSynthFunForEnumerator(e); + Assert(!e.isNull()); std::map > >::iterator it = d_examples.find(e); if (it != d_examples.end()) { @@ -286,7 +294,8 @@ void CegConjecturePbe::getExample(Node e, unsigned i, std::vector& ex) { } Node CegConjecturePbe::getExampleOut(Node e, unsigned i) { - e = getSynthFunctionForEnumerator(e); + e = d_tds->getSynthFunForEnumerator(e); + Assert(!e.isNull()); std::map >::iterator it = d_examples_out.find(e); if (it != d_examples_out.end()) { Assert(i < it->second.size()); @@ -300,7 +309,8 @@ Node CegConjecturePbe::getExampleOut(Node e, unsigned i) { Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) { Assert(isPbe()); Assert(!e.isNull()); - e = getSynthFunctionForEnumerator(e); + e = d_tds->getSynthFunForEnumerator(e); + Assert(!e.isNull()); std::map::iterator itx = d_examples_invalid.find(e); if (itx == d_examples_invalid.end()) { unsigned nex = d_examples[e].size(); @@ -313,7 +323,8 @@ Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) { Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i) { - e = getSynthFunctionForEnumerator(e); + e = d_tds->getSynthFunForEnumerator(e); + Assert(!e.isNull()); std::map::iterator itx = d_examples_invalid.find(e); if (itx == d_examples_invalid.end()) { std::map > >::iterator it = @@ -326,15 +337,6 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, return Rewriter::rewrite(bn); } -Node CegConjecturePbe::getSynthFunctionForEnumerator(Node e) { - std::map::const_iterator it = d_enum_to_candidate.find(e); - if (it != d_enum_to_candidate.end()) { - return it->second; - } else { - return e; - } -} - // ----------------------------- establishing enumeration types @@ -343,7 +345,7 @@ void CegConjecturePbe::registerEnumerator( Node et, Node c, TypeNode tn, unsigne Trace("sygus-unif-debug") << ", role = "; print_role( "sygus-unif-debug", enum_role ); Trace("sygus-unif-debug") << ", in search = " << inSearch << std::endl; - d_einfo[et].initialize( c, enum_role ); + d_einfo[et].initialize(c, enum_role); // if we are actually enumerating this (could be a compound node in the strategy) if( inSearch ){ std::map< TypeNode, Node >::iterator itn = d_cinfo[c].d_search_enum.find( tn ); @@ -353,9 +355,9 @@ void CegConjecturePbe::registerEnumerator( Node et, Node c, TypeNode tn, unsigne d_cinfo[c].d_esym_list.push_back( et ); d_einfo[et].d_enum_slave.push_back( et ); //register measured term with database - d_enum_to_candidate[et] = c; - d_qe->getTermDatabaseSygus()->registerMeasuredTerm(et, d_parent, true); - d_einfo[et].d_active_guard = d_qe->getTermDatabaseSygus()->getActiveGuardForMeasureTerm( et ); + d_qe->getTermDatabaseSygus()->registerEnumerator(et, c, d_parent, true); + d_einfo[et].d_active_guard = + d_qe->getTermDatabaseSygus()->getActiveGuardForEnumerator(et); }else{ Trace("sygus-unif-debug") << "Make " << et << " a slave of " << itn->second << std::endl; d_einfo[itn->second].d_enum_slave.push_back( et ); @@ -388,8 +390,9 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu std::map< Node, std::map< unsigned, Node > > cop_to_child_templ_arg; std::map< Node, unsigned > cop_to_strat; std::map< Node, unsigned > cop_to_cindex; - - // look at builtin operartors first (when r=0), then defined operators (when r=1) + + // look at builtin operartors first (when r=0), then defined operators + // (when r=1) for( unsigned r=0; r<2; r++ ){ for( unsigned j=0; j=eut.getNumChildren() && eut.getNumChildren()==2 ){ + if (dt[j].getNumArgs() >= eut.getNumChildren() + && eut.getNumChildren() == 2) + { cop_to_strat[cop] = strat_CONCAT; } }else if( eut.getKind()==kind::APPLY_UF ){ @@ -508,7 +514,7 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu } if( cop_to_strat.find( cop )!=cop_to_strat.end() ){ Trace("sygus-unif") << "...type " << dt.getName() << " has defined constructor matching strategy "; - print_strat("sygus-unif",cop_to_strat[cop]); + print_strat("sygus-unif", cop_to_strat[cop]); Trace("sygus-unif") << "..." << std::endl; for( unsigned k=0; k& lem std::map< Node, EnumInfo >::iterator itns = d_einfo.find( es ); Assert( itns!=d_einfo.end() ); Trace("sygus-unif") << " " << es << ", role = "; - print_role( "sygus-unif", itns->second.getRole() ); + print_role("sygus-unif", itns->second.getRole()); Trace("sygus-unif") << std::endl; } } @@ -851,7 +855,8 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& Assert( itv!=d_einfo.end() ); Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl; //bool prevIsCover = false; - if( itv->second.getRole()==enum_io ){ + if (itv->second.getRole() == enum_io) + { Trace("sygus-pbe-enum") << " IO-Eval of "; //prevIsCover = itv->second.isFeasible(); }else{ @@ -874,7 +879,8 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& Assert( res.isConst() ); } Node resb; - if( itv->second.getRole()==enum_io ){ + if (itv->second.getRole() == enum_io) + { Node out = itxo->second[j]; Assert( out.isConst() ); resb = res==out ? d_true : d_false; @@ -892,7 +898,8 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& } } bool keep = false; - if( itv->second.getRole()==enum_io ){ + if (itv->second.getRole() == enum_io) + { if( cond_vals.find( d_true )!=cond_vals.end() || cond_vals.empty() ){ // latter is the degenerate case of no examples //check subsumbed/subsuming std::vector< Node > subsume; @@ -956,7 +963,8 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& if( Trace.isOn("sygus-pbe-enum") ){ if( itv->second.getRole()==enum_io ){ if( !prevIsCover && itv->second.isFeasible() ){ - Trace("sygus-pbe-enum") << "...PBE : success : Evaluation of " << xs << " now covers all examples." << std::endl; + Trace("sygus-pbe-enum") << "...PBE : success : Evaluation of " + << xs << " now covers all examples." << std::endl; } } } @@ -980,30 +988,76 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& } } - - +/** NegContainsSygusInvarianceTest +* +* This class is used to construct a minimal shape of a term that cannot +* be contained in at least one output of an I/O pair. +* +* Say our PBE conjecture is: +* +* exists f. +* f( "abc" ) = "abc abc" ^ +* f( "de" ) = "de de" +* +* Then, this class is used when there is a candidate solution t[x1] such that +* either +* contains( "abc abc", t["abc"] ) ---> false or +* contains( "de de", t["de"] ) ---> false +* +* In particular it is used to determine whether certain generalizations of t[x1] +* are still sufficient to falsify one of the above containments. +* +* For example: +* +* str.++( x1, "d" ) can be minimized to str.++( _, "d" ) +* ...since contains( "abc abc", str.++( y, "d" ) ) ---> false, +* for any y. +* str.replace( "de", x1, "b" ) can be minimized to str.replace( "de", x1, _ ) +* ...since contains( "abc abc", str.replace( "de", "abc", y ) ) ---> false, +* for any y. +* +* It is an instance of quantifiers::SygusInvarianceTest, which +* traverses the AST of a given term, replaces each subterm by a +* fresh variable y and checks whether an invariance test (such as +* the one specified by this class) holds. +* +*/ class NegContainsSygusInvarianceTest : public quantifiers::SygusInvarianceTest { public: NegContainsSygusInvarianceTest(){} ~NegContainsSygusInvarianceTest(){} - Node d_ar; - std::vector< Node > d_exo; - std::vector< unsigned > d_neg_con_indices; - quantifiers::CegConjecturePbe* d_cpbe; - - void init(quantifiers::CegConjecturePbe* cpbe, Node ar, - std::vector& exo, std::vector& ncind) { - if (cpbe->hasExamples(ar)) { - Assert(cpbe->getNumExamples(ar) == exo.size()); - d_ar = ar; + /** initialize this invariance test + * cpbe is the conjecture utility. + * e is the enumerator which we are reasoning about (associated with a synth + * fun). + * exo is the list of outputs of the PBE conjecture. + * ncind is the set of possible indices of the PBE conjecture to check + * invariance of non-containment. + * For example, in the above example, when t[x1] = "ab", then this + * has the index 1 since contains("de de", "ab") ---> false but not + * the index 0 since contains("abc abc","ab") ---> true. + */ + void init(quantifiers::CegConjecturePbe* cpbe, + Node e, + std::vector& exo, + std::vector& ncind) + { + if (cpbe->hasExamples(e)) + { + Assert(cpbe->getNumExamples(e) == exo.size()); + d_enum = e; d_exo.insert( d_exo.end(), exo.begin(), exo.end() ); d_neg_con_indices.insert( d_neg_con_indices.end(), ncind.begin(), ncind.end() ); d_cpbe = cpbe; } } -protected: + + protected: + /** checks whether contains( out_i, nvn[in_i] ) --> false for some I/O pair i. + */ bool invariant( quantifiers::TermDbSygus * tds, Node nvn, Node x ){ - if( !d_ar.isNull() ){ + if (!d_enum.isNull()) + { TypeNode tn = nvn.getType(); Node nbv = tds->sygusToBuiltin( nvn, tn ); Node nbvr = tds->extendedRewrite( nbv ); @@ -1011,7 +1065,7 @@ protected: for( unsigned i=0; ievaluateBuiltin(tn, nbvr, d_ar, ii); + Node nbvre = d_cpbe->evaluateBuiltin(tn, nbvr, d_enum, ii); Node out = d_exo[ii]; Node cont = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, out, nbvre ); Node contr = Rewriter::rewrite( cont ); @@ -1021,7 +1075,7 @@ protected: Trace("sygus-pbe-cterm") << nbv << " for any " << tds->sygusToBuiltin( x ) << " since " << std::endl; Trace("sygus-pbe-cterm") << " PBE-cterm : for input example : "; std::vector< Node > ex; - d_cpbe->getExample(d_ar, ii, ex); + d_cpbe->getExample(d_enum, ii, ex); for( unsigned j=0; j d_exo; + /** The set of I/O pair indices i such that + * contains( out_i, nvn[in_i] ) ---> false + */ + std::vector d_neg_con_indices; + /** reference to the PBE utility */ + quantifiers::CegConjecturePbe* d_cpbe; }; @@ -1042,7 +1108,8 @@ bool CegConjecturePbe::getExplanationForEnumeratorExclude( Node c, Node x, Node if( ei.d_enum_slave.size()==1 ){ // this check whether the example evaluates to something that is larger than the output // if so, then this term is never useful when using a concatenation strategy - if( ei.getRole()==enum_concat_term ){ + if (ei.getRole() == enum_concat_term) + { if( Trace.isOn("sygus-pbe-cterm-debug") ){ Trace("sygus-pbe-enum") << std::endl; } @@ -1078,7 +1145,7 @@ bool CegConjecturePbe::getExplanationForEnumeratorExclude( Node c, Node x, Node if( !cmp_indices.empty() ){ //set up the inclusion set NegContainsSygusInvarianceTest ncset; - ncset.init(this, c, itxo->second, cmp_indices); + ncset.init(this, x, itxo->second, cmp_indices); d_tds->getExplanationFor( x, v, exp, ncset ); Trace("sygus-pbe-cterm") << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin( v ) << " due to negative containment." << std::endl; return true; @@ -1096,7 +1163,7 @@ void CegConjecturePbe::EnumInfo::addEnumValue( CegConjecturePbe * pbe, Node v, s d_enum_vals_res.push_back( results ); /* if( getRole()==enum_io ){ - // compute + // compute if( d_enum_total.empty() ){ d_enum_total = results; }else if( !d_enum_total_true ){ @@ -1464,12 +1531,16 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e ); Assert( itn!=d_einfo.end() ); Node ret_dt; - if( itn->second.getRole()==enum_any ){ + if (itn->second.getRole() == enum_any) + { indent("sygus-pbe-dt", ind); ret_dt = constructBestSolvedTerm( itn->second.d_enum_vals, x ); Trace("sygus-pbe-dt") << "return PBE: success : use any " << d_tds->sygusToBuiltin( ret_dt ) << std::endl; Assert( !ret_dt.isNull() ); - }else if( itn->second.getRole()==enum_io && !x.isReturnValueModified() && itn->second.isSolved() ){ + } + else if (itn->second.getRole() == enum_io && !x.isReturnValueModified() + && itn->second.isSolved()) + { // this type has a complete solution ret_dt = itn->second.getSolved(); indent("sygus-pbe-dt", ind); @@ -1485,7 +1556,8 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in // get the term enumerator for this type bool success = true; std::map< Node, EnumInfo >::iterator itet; - if( itn->second.getRole()==enum_concat_term ){ + if (itn->second.getRole() == enum_concat_term) + { itet = itn; }else{ std::map< unsigned, Node >::iterator itnt = itt->second.d_enum.find( enum_concat_term ); @@ -1522,7 +1594,9 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in Trace("sygus-pbe-dt-debug") << " ...not currently string solved." << std::endl; } } - }else if( itn->second.getRole()==enum_io && !x.isReturnValueModified() ){ + } + else if (itn->second.getRole() == enum_io && !x.isReturnValueModified()) + { // it has an enumerated value that is conditionally correct under the current assumptions std::vector< Node > subsumed_by; itn->second.d_term_trie.getSubsumedBy( this, x.d_vals, true, subsumed_by ); @@ -1555,31 +1629,36 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in Node incr_val; int incr_type = 0; std::map< Node, std::vector< unsigned > > incr; - + // construct the child order based on heuristics std::vector< unsigned > corder; - std::unordered_set< unsigned > cused; + std::unordered_set cused; if( strat==strat_CONCAT ){ for( unsigned r=0; r<2; r++ ){ // Concatenate strategy can only be applied from the endpoints. - // This chooses the appropriate endpoint for which we stay within the same SyGuS type. - // In other words, if we are synthesizing based on a production rule ( T -> str.++( T1, ..., Tn ) ), then we - // prefer recursing on the 1st argument of the concat if T1 = T, and the last argument if Tn = T. + // This chooses the appropriate endpoint for which we stay within + // the same SyGuS type. + // In other words, if we are synthesizing based on a production + // rule ( T -> str.++( T1, ..., Tn ) ), then we + // prefer recursing on the 1st argument of the concat if T1 = T, + // and the last argument if Tn = T. unsigned sc = r==0 ? 0 : itts->second.d_cenum.size()-1; Node ce = itts->second.d_cenum[sc]; if( ce.getType()==etn ){ // prefer simple recursion (self type) Assert( d_einfo.find( ce )!=d_einfo.end() ); - Assert( d_einfo[ce].getRole()==enum_concat_term ); + Assert(d_einfo[ce].getRole() == enum_concat_term); corder.push_back( sc ); - cused.insert( sc ); + cused.insert(sc); break; } } } // fill remaining children for which there is no preference - for( unsigned sc=0; scsecond.d_cenum.size(); sc++ ){ - if( cused.find( sc )==cused.end() ){ + for (unsigned sc = 0; sc < itts->second.d_cenum.size(); sc++) + { + if (cused.find(sc) == cused.end()) + { corder.push_back( sc ); } } @@ -1709,7 +1788,7 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in std::map< Node, EnumInfo >::iterator itsc = d_einfo.find( ce ); Assert( itsc!=d_einfo.end() ); // ensured by the child order we set above - Assert( itsc->second.getRole()==enum_concat_term ); + Assert(itsc->second.getRole() == enum_concat_term); // check if each return value is a prefix/suffix of all open examples incr_type = sc==0 ? -1 : 1; if( x.d_has_string_pos==0 || x.d_has_string_pos==incr_type ){ diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h index e4c252194..ca0190dc0 100644 --- a/src/theory/quantifiers/ce_guided_pbe.h +++ b/src/theory/quantifiers/ce_guided_pbe.h @@ -35,7 +35,7 @@ class CegEntailmentInfer; * that are in Programming-By-Examples (PBE) form. * * [EX#1] An example of a synthesis conjecture in PBE form is : -* exists f. forall x. +* exists f. forall x. * ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = 6 => f( x ) = 8 ) * * We say that the above conjecture has I/O examples (0)->2, (5)->7, (6)->8. @@ -45,79 +45,104 @@ class CegEntailmentInfer; * (1) Infers whether the input conjecture is in PBE form or not. * (2) Based on this information and on the syntactic restrictions, it * devises a strategy for enumerating terms and construction solutions, -* which is inspired by Alur et al. "Scaling Enumerative Program Synthesis -* via Divide and Conquer" TACAS 2017. In particular, it may consider strategies -* for constructing decision trees when the grammar permits ITEs and a -* strategy for divide-and-conquer string synthesis when the grammar permits -* string concatenation. This is stored in a set of data structures within -* d_cinfo. -* (3) It makes (possibly multiple) calls to +* which is inspired by Alur et al. "Scaling Enumerative Program Synthesis +* via Divide and Conquer" TACAS 2017. In particular, it may consider +* strategies for constructing decision trees when the grammar permits ITEs +* and a strategy for divide-and-conquer string synthesis when the grammar +* permits string concatenation. This is stored in a set of data structures +* within d_cinfo. +* (3) It makes (possibly multiple) calls to * TermDatabaseSygus::registerMeasuredTerm(...) based * on the strategy, which inform the rest of the system to enumerate values -* of particular types in the grammar through use of fresh variables which +* of particular types in the grammar through use of fresh variables which * we call "enumerators". * * Points (1)-(3) happen within a call to CegConjecturePbe::initialize(...). * -* Notice that each enumerator is associated with a single function-to-synthesize, +* Notice that each enumerator is associated with a single +* function-to-synthesize, * but a function-to-sythesize may be mapped to multiple enumerators. * Some public functions of this class expect an enumerator as input, which we -* map to a function-to-synthesize via getSynthFunctionForEnumerator. +* map to a function-to-synthesize via TermDatabaseSygus::getSynthFunFor(e). * * An enumerator is initially "active" but may become inactive if the enumeration -* exhausts all possible values in the datatype corresponding to syntactic restrictions +* exhausts all possible values in the datatype corresponding to syntactic +* restrictions * for it. The search may continue unless all enumerators become inactive. * -* (4) During search, the extension of quantifier-free datatypes procedure for SyGuS -* datatypes may ask this class whether current candidates can be discarded based on -* inferring when two candidate solutions are equivalent up to examples. -* For example, the candidate solutions: -* f = \x ite( x<0, x+1, x ) and f = \x x -* are equivalent up to examples on the above conjecture, since they have the same -* value on the points x = 0,5,6. Hence, we need only consider one of them. -* The interface for querying this is CegConjecturePbe::addSearchVal(...). +* (4) During search, the extension of quantifier-free datatypes procedure for +* SyGuS datatypes may ask this class whether current candidates can be +* discarded based on +* inferring when two candidate solutions are equivalent up to examples. +* For example, the candidate solutions: +* f = \x ite( x<0, x+1, x ) and f = \x x +* are equivalent up to examples on the above conjecture, since they have the +* same value on the points x = 0,5,6. Hence, we need only consider one of +* them. The interface for querying this is +* CegConjecturePbe::addSearchVal(...). * For details, see Reynolds et al. SYNT 2017. -* -* (5) When the extension of quantifier-free datatypes procedure for SyGuS datatypes -* terminates with a model, the parent of this class calls -* CegConjecturePbe::getCandidateList(...), where this class returns the list of -* active enumerators. -* (6) The parent class subsequently calls CegConjecturePbe::constructValues(...), which -* informs this class that new values have been enumerated for active enumerators, -* as indicated by the current model. This call also requests that based on these -* newly enumerated values, whether this class is now able to construct a solution -* based on the high-level strategy (stored in d_c_info). * -* This class is not designed to work in incremental mode, since there is no way to +* (5) When the extension of quantifier-free datatypes procedure for SyGuS +* datatypes terminates with a model, the parent of this class calls +* CegConjecturePbe::getCandidateList(...), where this class returns the list +* of active enumerators. +* (6) The parent class subsequently calls +* CegConjecturePbe::constructValues(...), which +* informs this class that new values have been enumerated for active +* enumerators, as indicated by the current model. This call also requests +* that based on these +* newly enumerated values, whether this class is now able to construct a +* solution based on the high-level strategy (stored in d_c_info). +* +* This class is not designed to work in incremental mode, since there is no way +* to * specify incremental problems in SyguS. * */ class CegConjecturePbe { -public: - CegConjecturePbe( QuantifiersEngine * qe, CegConjecture * p ); + public: + CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p); ~CegConjecturePbe(); - - /** initialize this class */ - void initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas ); + + /** initialize this class + * + * n is the "base instantiation" of the deep-embedding version of + * the synthesis conjecture under "candidates". + * (see CegConjecture::d_base_inst) + * + * This function may add lemmas to the vector lemmas corresponding + * to initial lemmas regarding static analysis of enumerators it + * introduced. For example, we may say that the top-level symbol + * of an enumerator is not ITE if it is being used to construct + * return values for decision trees. + */ + void initialize(Node n, + std::vector& candidates, + std::vector& lemmas); /** get candidate list - * Adds all active enumerators associated with functions-to-synthesize in candidates to clist. + * Adds all active enumerators associated with functions-to-synthesize in + * candidates to clist. */ - void getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ); - /** construct candidates - * (1) Indicates that the list of enumerators in "enums" currently have model values "enum_values". - * (2) Asks whether based on these new enumerated values, we can construct a solution for - * the functions-to-synthesize in "candidates". If so, this function returns "true" and + void getCandidateList(std::vector& candidates, + std::vector& clist); + /** construct candidates + * (1) Indicates that the list of enumerators in "enums" currently have model + * values "enum_values". + * (2) Asks whether based on these new enumerated values, we can construct a + * solution for + * the functions-to-synthesize in "candidates". If so, this function + * returns "true" and * adds solutions for candidates into "candidate_values". - * During this class, this class may add auxiliary lemmas to "lems", which the caller - * should send on the output channel via lemma(...). + * During this class, this class may add auxiliary lemmas to "lems", which the + * caller should send on the output channel via lemma(...). */ - bool constructCandidates( std::vector< Node >& enums, std::vector< Node >& enum_values, - std::vector< Node >& candidates, std::vector< Node >& candidate_values, - std::vector< Node >& lems ); + bool constructCandidates(std::vector& enums, + std::vector& enum_values, + std::vector& candidates, + std::vector& candidate_values, + std::vector& lems); /** is PBE enabled for any enumerator? */ bool isPbe() { return d_is_pbe; } - /** get candidate for enumerator */ - Node getSynthFunctionForEnumerator(Node e); /** is the enumerator e associated with I/O example pairs? */ bool hasExamples(Node e); /** get number of I/O example pairs for enumerator e */ @@ -127,33 +152,38 @@ public: void getExample(Node e, unsigned i, std::vector& ex); /** get the output value of the i^th I/O example for enumerator e */ Node getExampleOut(Node e, unsigned i); - + /** add the search val - * This function is called by the extension of quantifier-free datatypes procedure - * for SyGuS datatypes when we are considering a value of enumerator e of sygus - * type tn whose analog in the signature of builtin theory is bvr. - * - * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) and + * This function is called by the extension of quantifier-free datatypes + * procedure for SyGuS datatypes when we are considering a value of + * enumerator e of sygus type tn whose analog in the signature of builtin + * theory is bvr. + * + * For example, bvr = x + 1 when e is the datatype value Plus( x(), One() ) and * tn is a sygus datatype that encodes a subsignature of the integers. * * This returns either: - * - A SyGuS term whose analog is equivalent to bvr up to examples, in the above example, - * it may return a term t of the form Plus( One(), x() ), such that this function was - * previously called with t as input. + * - A SyGuS term whose analog is equivalent to bvr up to examples, in the + * above example, + * it may return a term t of the form Plus( One(), x() ), such that this + * function was previously called with t as input. * - e, indicating that no previous terms are equivalent to e up to examples. */ Node addSearchVal(TypeNode tn, Node e, Node bvr); /** evaluate builtin - * This returns the evaluation of bn on the i^th example for the function-to-synthesis - * associated with enumerator e. If there are not at least i examples, it returns - * the rewritten form of bn. - * For example, if bn = x+5, e is an enumerator for f in the above example [EX#1], then + * This returns the evaluation of bn on the i^th example for the + * function-to-synthesis + * associated with enumerator e. If there are not at least i examples, it + * returns the rewritten form of bn. + * For example, if bn = x+5, e is an enumerator for f in the above example + * [EX#1], then * evaluateBuiltin( tn, bn, e, 0 ) = 7 * evaluateBuiltin( tn, bn, e, 1 ) = 9 * evaluateBuiltin( tn, bn, e, 2 ) = 10 */ - Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i); -private: + Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i); + + private: /** quantifiers engine associated with this class */ QuantifiersEngine* d_qe; /** sygus term database of d_qe */ @@ -162,7 +192,8 @@ private: Node d_true; Node d_false; /** parent conjecture - * This is the data structure that contains global information about the conjecture. + * This is the data structure that contains global information about the + * conjecture. */ CegConjecture* d_parent; /** is this a PBE conjecture for any function? */ @@ -180,7 +211,8 @@ private: * exists f. forall x. ( x = 0 => f( x ) > 2 ) * another example is: * exists f. forall x. ( ( x = 0 => f( x ) = 2 ) V ( x = 3 => f( x ) = 3 ) ) - * since the formula is not a conjunction (the example values are not entailed). + * since the formula is not a conjunction (the example values are not + * entailed). * However, the domain of f in both cases is finite, which can be used for * search space pruning. */ @@ -191,26 +223,20 @@ private: /** for each candidate variable (function-to-synthesize), output of I/O * examples */ std::map< Node, std::vector< Node > > d_examples_out; - /** the list of example terms - * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 ) + /** the list of example terms + * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 ) */ std::map< Node, std::vector< Node > > d_examples_term; - /** map from enumerators to candidate varaibles (function-to-synthesize). An - * enumerator may not be equivalent - * to the candidate variable it maps so in synthesis-through-unification - * approaches (e.g. decision tree construction). - */ - std::map d_enum_to_candidate; - /** collect the PBE examples in n + /** collect the PBE examples in n * This is called on the input conjecture, and will populate the above vectors. * hasPol/pol denote the polarity of n in the conjecture. */ void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol ); - + //--------------------------------- PBE search values /** this class is an index of candidate solutions for PBE synthesis */ class PbeTrie { - public: + public: PbeTrie() {} ~PbeTrie() {} Node d_lazy_child; @@ -218,7 +244,8 @@ private: void clear() { d_children.clear(); } Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe, unsigned index, unsigned ntotal); - private: + + private: Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector& ex, CegConjecturePbe* cpbe, unsigned index, unsigned ntotal); @@ -231,9 +258,9 @@ private: */ std::map > d_pbe_trie; //--------------------------------- end PBE search values - + // -------------------------------- decision tree learning - //index filter + // index filter class IndexFilter { public: IndexFilter(){} @@ -243,7 +270,7 @@ private: unsigned next( unsigned i ); void clear() { d_next.clear(); } bool isEq( std::vector< Node >& vs, Node v ); - }; + }; // subsumption trie class SubsumeTrie { public: @@ -265,22 +292,37 @@ private: d_term = Node::null(); d_children.clear(); } - private: + + private: /** the term at this node */ Node d_term; /** the children nodes of this trie */ - std::map< Node, SubsumeTrie > d_children; + std::map d_children; /** helper function for above functions */ - Node addTermInternal( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, bool spol, IndexFilter * f, - unsigned index, int status, bool checkExistsOnly, bool checkSubsume ); + Node addTermInternal(CegConjecturePbe* pbe, + Node t, + std::vector& vals, + bool pol, + std::vector& subsumed, + bool spol, + IndexFilter* f, + unsigned index, + int status, + bool checkExistsOnly, + bool checkSubsume); /** helper function for above functions */ - void getLeavesInternal( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f, - unsigned index, int status ); + void getLeavesInternal(CegConjecturePbe* pbe, + std::vector& vals, + bool pol, + std::map >& v, + IndexFilter* f, + unsigned index, + int status); }; // -------------------------------- end decision tree learning - + //------------------------------ representation of a enumeration strategy - + /** roles for enumerators */ enum { enum_io, @@ -289,36 +331,39 @@ private: enum_any, }; /** print the role with Trace c. */ - static void print_role( const char * c, unsigned r ); + static void print_role(const char* c, unsigned r); /** strategies for SyGuS datatype types */ - enum { + enum + { strat_ITE, strat_CONCAT, strat_ID, - }; + }; /** print the strategy with Trace c. */ - static void print_strat( const char * c, unsigned s ); - + static void print_strat(const char* c, unsigned s); + /** information about an enumerator */ class EnumInfo { public: EnumInfo() : d_role( enum_io ){} - /** initialize this class - * c is the parent function-to-synthesize + /** initialize this class + * c is the parent function-to-synthesize * role is the "role" the enumerator plays in the high-level strategy, * which is one of enum_* above. */ - void initialize( Node c, unsigned role ){ + void initialize(Node c, unsigned role) + { d_parent_candidate = c; d_role = role; } bool isTemplated() { return !d_template.isNull(); } - void addEnumValue( CegConjecturePbe * pbe, Node v, std::vector< Node >& results ); - void setSolved( Node slv ); + void addEnumValue(CegConjecturePbe* pbe, + Node v, + std::vector& results); + void setSolved(Node slv); bool isSolved() { return !d_enum_solved.isNull(); } Node getSolved() { return d_enum_solved; } unsigned getRole() { return d_role; } - Node d_parent_candidate; // for template Node d_template; @@ -335,16 +380,17 @@ private: std::vector< Node > d_enum_subsume; std::map< Node, unsigned > d_enum_val_to_index; SubsumeTrie d_term_trie; - private: - /** whether an enumerated value for this conjecture has solved the entire conjecture */ + + private: + /** whether an enumerated value for this conjecture has solved the entire + * conjecture */ Node d_enum_solved; /** the role of this enumerator (one of enum_* above). */ unsigned d_role; }; /** maps enumerators to the information above */ std::map< Node, EnumInfo > d_einfo; - - + class CandidateInfo; /** represents a strategy for a SyGuS datatype type */ class EnumTypeInfoStrat { @@ -354,8 +400,7 @@ private: std::vector< TypeNode > d_csol_cts; std::vector< Node > d_cenum; }; - - + /** stores enumerators and strategies for a SyGuS datatype type */ class EnumTypeInfo { public: @@ -368,9 +413,9 @@ private: std::map< Node, EnumTypeInfoStrat > d_strat; bool isSolved( CegConjecturePbe * pbe ); }; - - - /** stores strategy and enumeration information for a function-to-synthesize */ + + /** stores strategy and enumeration information for a function-to-synthesize + */ class CandidateInfo { public: CandidateInfo() : d_check_sol( false ), d_cond_count( 0 ){} @@ -380,7 +425,8 @@ private: * of solutions. */ TypeNode d_root; - /** Information for each SyGuS datatype type occurring in a field of d_root */ + /** Information for each SyGuS datatype type occurring in a field of d_root + */ std::map< TypeNode, EnumTypeInfo > d_tinfo; /** list of all enumerators for the function-to-synthesize */ std::vector< Node > d_esym_list; @@ -396,24 +442,31 @@ private: }; /** maps a function-to-synthesize to the above information */ std::map< Node, CandidateInfo > d_cinfo; - + //------------------------------ representation of an enumeration strategy /** add enumerated value */ void addEnumeratedValue( Node x, Node v, std::vector< Node >& lems ); bool getExplanationForEnumeratorExclude( Node c, Node x, Node v, std::vector< Node >& results, EnumInfo& ei, std::vector< Node >& exp ); - + //------------------------------ strategy registration - void collectEnumeratorTypes( Node c, TypeNode tn, unsigned enum_role ); - void registerEnumerator( Node et, Node c, TypeNode tn, unsigned enum_role, bool inSearch ); - void staticLearnRedundantOps( Node c, std::vector< Node >& lemmas ); - void staticLearnRedundantOps( Node c, Node e, std::map< Node, bool >& visited, std::vector< Node >& redundant, - std::vector< Node >& lemmas, int ind ); + void collectEnumeratorTypes(Node c, TypeNode tn, unsigned enum_role); + void registerEnumerator( + Node et, Node c, TypeNode tn, unsigned enum_role, bool inSearch); + void staticLearnRedundantOps(Node c, std::vector& lemmas); + void staticLearnRedundantOps(Node c, + Node e, + std::map& visited, + std::vector& redundant, + std::vector& lemmas, + int ind); /** register candidate conditional */ - bool inferTemplate( unsigned k, Node n, std::map< Node, unsigned >& templ_var_index, std::map< unsigned, unsigned >& templ_injection ); - //------------------------------ end strategy registration - - + bool inferTemplate(unsigned k, + Node n, + std::map& templ_var_index, + std::map& templ_injection); + //------------------------------ end strategy registration + //------------------------------ constructing solutions class UnifContext { public: @@ -453,16 +506,22 @@ private: * in context x, where ind is the term depth of the context. */ Node constructSolution( Node c, Node e, UnifContext& x, int ind ); - /** Heuristically choose the best solved term from solved in context x, currently return the first. */ + /** Heuristically choose the best solved term from solved in context x, + * currently return the first. */ Node constructBestSolvedTerm( std::vector< Node >& solved, UnifContext& x ); - /** Heuristically choose the best solved string term from solved in context x, currently return the first. */ + /** Heuristically choose the best solved string term from solved in context + * x, currently return the first. */ Node constructBestStringSolvedTerm( std::vector< Node >& solved, UnifContext& x ); - /** heuristically choose the best solved conditional term from solved in context x, currently random */ + /** heuristically choose the best solved conditional term from solved in + * context x, currently random */ Node constructBestSolvedConditional( std::vector< Node >& solved, UnifContext& x ); - /** heuristically choose the best conditional term from conds in context x, currently random */ + /** heuristically choose the best conditional term from conds in context x, + * currently random */ Node constructBestConditional( std::vector< Node >& conds, UnifContext& x ); - /** heuristically choose the best string to concatenate from strs to the solution in context x, currently random - * incr stores the vector of indices that are incremented by this solution in example outputs. + /** heuristically choose the best string to concatenate from strs to the + * solution in context x, currently random + * incr stores the vector of indices that are incremented by this solution in + * example outputs. * total_inc[x] is the sum of incr[x] for each x in strs. */ Node constructBestStringToConcat( std::vector< Node > strs, @@ -470,13 +529,13 @@ private: std::map< Node, std::vector< unsigned > > incr, UnifContext& x ); //------------------------------ end constructing solutions - - /** get guard status + + /** get guard status * Returns 1 if g is asserted true in the SAT solver. * Returns -1 if g is asserted false in the SAT solver. * Returns 0 otherwise. */ - int getGuardStatus( Node g ); + int getGuardStatus(Node g); }; diff --git a/src/theory/quantifiers/sygus_process_conj.cpp b/src/theory/quantifiers/sygus_process_conj.cpp new file mode 100644 index 000000000..600c09a58 --- /dev/null +++ b/src/theory/quantifiers/sygus_process_conj.cpp @@ -0,0 +1,97 @@ +/********************* */ +/*! \file sygus_process_conj.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of techniqures for static preprocessing and analysis + ** of sygus conjectures. + **/ +#include "theory/quantifiers/sygus_process_conj.h" + +#include + +#include "expr/datatype.h" +#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" + +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) : d_qe(qe) {} +CegConjectureProcess::~CegConjectureProcess() {} +Node CegConjectureProcess::simplify(Node q) +{ + Trace("sygus-process") << "Simplify conjecture : " << q << std::endl; + + return q; +} + +void CegConjectureProcess::initialize(Node n, std::vector& candidates) +{ + if (Trace.isOn("sygus-process")) + { + Trace("sygus-process") << "Process conjecture : " << n + << " with candidates: " << std::endl; + for (unsigned i = 0; i < candidates.size(); i++) + { + Trace("sygus-process") << " " << candidates[i] << std::endl; + } + } + Node base; + if (n.getKind() == NOT && n[0].getKind() == FORALL) + { + base = n[0][1]; + } + else + { + base = n; + } + + std::vector conj; + if (base.getKind() == AND) + { + for (unsigned i = 0; i < base.getNumChildren(); i++) + { + conj.push_back(base[i]); + } + } + else + { + conj.push_back(base); + } + + // initialize the information for synth funs + for (unsigned i = 0; i < candidates.size(); i++) + { + Node e = candidates[i]; + // d_sf_info[e].d_arg_independent + } + + // process the conjunctions + for (unsigned i = 0; i < conj.size(); i++) + { + processConjunct(conj[i]); + } +} + +void CegConjectureProcess::processConjunct(Node c) {} +Node CegConjectureProcess::getSymmetryBreakingPredicate( + Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth) +{ + return Node::null(); +} + +void CegConjectureProcess::debugPrint(const char* c) {} +} /* namespace CVC4::theory::quantifiers */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus_process_conj.h b/src/theory/quantifiers/sygus_process_conj.h new file mode 100644 index 000000000..4637ae551 --- /dev/null +++ b/src/theory/quantifiers/sygus_process_conj.h @@ -0,0 +1,99 @@ +/********************* */ +/*! \file sygus_process_conj.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Techniqures for static preprocessing and analysis of + ** sygus conjectures. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PPROCESS_CONJ_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESSS_CONJ_H + +#include "expr/node.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** This structure stores information regarding conjecture-specific +* analysis of a function to synthesize. +*/ +struct CegSynthFunProcessInfo +{ + public: + CegSynthFunProcessInfo() {} + ~CegSynthFunProcessInfo() {} + /** the set of arguments that this synth-fun is independent of */ + std::map d_arg_independent; +}; + +/** Ceg Conjecture Process +* +* This class implements static techniques for preprocessing and analysis of +* sygus conjectures. +* +* It is used as a back-end to CegConjecture, which calls it using the following +* interface: +* (1) When a sygus conjecture is asserted, we call +* CegConjectureProcess::simplify( q ), +* where q is the sygus conjecture in original form. +* +* (2) After a sygus conjecture is simplified and converted to deep +* embedding form, we call CegConjectureProcess::initialize( n, candidates ). +* +* (3) During enumerative SyGuS search, calls may be made by +* the extension of the quantifier-free datatypes decision procedure for +* sygus to CegConjectureProcess::getSymmetryBreakingPredicate(...), which are +* used for pruning search space based on conjecture-specific analysis. +*/ +class CegConjectureProcess +{ + public: + CegConjectureProcess(QuantifiersEngine* qe); + ~CegConjectureProcess(); + /** simplify the synthesis conjecture q + * Returns a formula that is equivalent to q. + */ + Node simplify(Node q); + /** initialize + * + * n is the "base instantiation" of the deep-embedding version of + * the synthesis conjecture under "candidates". + * (see CegConjecture::d_base_inst) + */ + void initialize(Node n, std::vector& candidates); + /** get symmetry breaking predicate + * + * Returns a formula that restricts the enumerative search space (for a given + * depth) for a term x of sygus type tn whose top symbol is the tindex^{th} + * constructor, where x is a subterm of enumerator e. + */ + Node getSymmetryBreakingPredicate( + Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth); + /** print out debug information about this conjecture */ + void debugPrint(const char* c); + + private: + /** process conjunct */ + void processConjunct(Node c); + /** for each synth-fun, information that is specific to this conjecture */ + std::map d_sf_info; + /** reference to quantifier engine */ + QuantifiersEngine* d_qe; +}; + +} /* namespace CVC4::theory::quantifiers */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ + +#endif diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index a12397d8c..f298e9711 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -1368,11 +1368,15 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { } } -void TermDbSygus::registerMeasuredTerm(Node e, CegConjecture* conj, - bool mkActiveGuard) { +void TermDbSygus::registerEnumerator(Node e, + Node f, + CegConjecture* conj, + bool mkActiveGuard) +{ Assert(d_enum_to_conjecture.find(e) == d_enum_to_conjecture.end()); Trace("sygus-db") << "Register measured term : " << e << std::endl; d_enum_to_conjecture[e] = conj; + d_enum_to_synth_fun[e] = f; if( mkActiveGuard ){ // make the guard Node eg = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "eG", NodeManager::currentNM()->booleanType() ) ); @@ -1387,11 +1391,13 @@ void TermDbSygus::registerMeasuredTerm(Node e, CegConjecture* conj, } } -bool TermDbSygus::isMeasuredTerm(Node e) const { +bool TermDbSygus::isEnumerator(Node e) const +{ return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end(); } -CegConjecture* TermDbSygus::getConjectureFor(Node e) { +CegConjecture* TermDbSygus::getConjectureForEnumerator(Node e) +{ std::map::iterator itm = d_enum_to_conjecture.find(e); if (itm != d_enum_to_conjecture.end()) { return itm->second; @@ -1400,7 +1406,21 @@ CegConjecture* TermDbSygus::getConjectureFor(Node e) { } } -Node TermDbSygus::getActiveGuardForMeasureTerm( Node e ) { +Node TermDbSygus::getSynthFunForEnumerator(Node e) +{ + std::map::iterator itsf = d_enum_to_synth_fun.find(e); + if (itsf != d_enum_to_synth_fun.end()) + { + return itsf->second; + } + else + { + return Node::null(); + } +} + +Node TermDbSygus::getActiveGuardForEnumerator(Node e) +{ std::map::iterator itag = d_enum_to_active_guard.find(e); if (itag != d_enum_to_active_guard.end()) { return itag->second; @@ -1409,7 +1429,8 @@ Node TermDbSygus::getActiveGuardForMeasureTerm( Node e ) { } } -void TermDbSygus::getMeasuredTerms( std::vector< Node >& mts ) { +void TermDbSygus::getEnumerators(std::vector& mts) +{ for (std::map::iterator itm = d_enum_to_conjecture.begin(); itm != d_enum_to_conjecture.end(); ++itm) { diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h index 768047734..030963b58 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/term_database_sygus.h @@ -83,6 +83,9 @@ private: private: /** mapping from enumerator terms to the conjecture they are associated with */ std::map d_enum_to_conjecture; + /** mapping from enumerator terms to the function-to-synthesize they are + * associated with */ + std::map d_enum_to_synth_fun; /** mapping from enumerator terms to the guard they are associated with * The guard G for an enumerator e has the semantics * "if G is true, then there are more values of e to enumerate". @@ -129,21 +132,31 @@ public: /** register the sygus type */ void registerSygusType( TypeNode tn ); /** register a variable e that we will do enumerative search on - * conj is the conjecture that the enumeration for e is for. + * conj is the conjecture that the enumeration of e is for. + * f is the synth-fun that the enumeration of e is for. * mkActiveGuard is whether we want to make a active guard for e (see * d_enum_to_active_guard) + * + * Notice that enumerator e may not be equivalent + * to f in synthesis-through-unification approaches + * (e.g. decision tree construction for PBE synthesis). */ - void registerMeasuredTerm(Node e, CegConjecture* conj, - bool mkActiveGuard = false); - /** is e a measured term (enumerator)? */ - bool isMeasuredTerm(Node e) const; + void registerEnumerator(Node e, + Node f, + CegConjecture* conj, + bool mkActiveGuard = false); + /** is e an enumerator? */ + bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ - CegConjecture* getConjectureFor(Node e); + CegConjecture* getConjectureForEnumerator(Node e); + /** return the function-to-synthesize e is associated with */ + Node getSynthFunForEnumerator(Node e); /** get active guard for e */ - Node getActiveGuardForMeasureTerm( Node e ); - /** get all registered measure terms (enumerators) */ - void getMeasuredTerms( std::vector< Node >& mts ); -public: //general sygus utilities + Node getActiveGuardForEnumerator(Node e); + /** get all registered enumerators */ + void getEnumerators(std::vector& mts); + + public: // general sygus utilities bool isRegistered( TypeNode tn ); // get the minimum depth of type in its parent grammar unsigned getMinTypeDepth( TypeNode root_tn, TypeNode tn );