diff options
| -rw-r--r-- | src/theory/quantifiers/ce_guided_pbe.cpp | 104 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_pbe.h | 397 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/strings-concat-3-args.sy | 18 |
4 files changed, 343 insertions, 179 deletions
diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp index ac09a31d0..e4bf43963 100644 --- a/src/theory/quantifiers/ce_guided_pbe.cpp +++ b/src/theory/quantifiers/ce_guided_pbe.cpp @@ -35,6 +35,7 @@ void indent( const char * c, int ind ) { } } } + void print_val( const char * c, std::vector< Node >& vals, bool pol = true ){ if( Trace.isOn(c) ){ for( unsigned i=0; i<vals.size(); i++ ){ @@ -43,15 +44,8 @@ void print_val( const char * c, std::vector< Node >& vals, bool pol = true ){ } } } -void 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 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; @@ -61,6 +55,15 @@ void 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; + } +} + CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) : d_qe(qe), d_parent(p){ @@ -250,7 +253,7 @@ Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b, bool CegConjecturePbe::hasExamples(Node e) { if (isPbe()) { - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, bool>::iterator itx = d_examples_invalid.find(e); if (itx == d_examples_invalid.end()) { return d_examples.find(e) != d_examples.end(); @@ -260,7 +263,7 @@ bool CegConjecturePbe::hasExamples(Node e) { } unsigned CegConjecturePbe::getNumExamples(Node e) { - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, std::vector<std::vector<Node> > >::iterator it = d_examples.find(e); if (it != d_examples.end()) { @@ -271,7 +274,7 @@ unsigned CegConjecturePbe::getNumExamples(Node e) { } void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) { - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, std::vector<std::vector<Node> > >::iterator it = d_examples.find(e); if (it != d_examples.end()) { @@ -283,7 +286,7 @@ void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) { } Node CegConjecturePbe::getExampleOut(Node e, unsigned i) { - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e); if (it != d_examples_out.end()) { Assert(i < it->second.size()); @@ -297,7 +300,7 @@ Node CegConjecturePbe::getExampleOut(Node e, unsigned i) { Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) { Assert(isPbe()); Assert(!e.isNull()); - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, bool>::iterator itx = d_examples_invalid.find(e); if (itx == d_examples_invalid.end()) { unsigned nex = d_examples[e].size(); @@ -310,7 +313,7 @@ Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) { Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i) { - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, bool>::iterator itx = d_examples_invalid.find(e); if (itx == d_examples_invalid.end()) { std::map<Node, std::vector<std::vector<Node> > >::iterator it = @@ -323,7 +326,7 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, return Rewriter::rewrite(bn); } -Node CegConjecturePbe::getCandidateForEnumerator(Node e) { +Node CegConjecturePbe::getSynthFunctionForEnumerator(Node e) { std::map<Node, Node>::const_iterator it = d_enum_to_candidate.find(e); if (it != d_enum_to_candidate.end()) { return it->second; @@ -340,8 +343,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].d_parent_candidate = c; - d_einfo[et].d_role = 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 ); @@ -387,9 +389,9 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu 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) for( unsigned r=0; r<2; r++ ){ for( unsigned j=0; j<dt.getNumConstructors(); j++ ){ - bool success = false; Node cop = Node::fromExpr( dt[j].getConstructor() ); Node op = Node::fromExpr( dt[j].getSygusOp() ); if( r==0 ){ @@ -397,7 +399,6 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu if( op.getKind() == kind::BUILTIN ){ Kind sk = NodeManager::operatorToKind( op ); if( sk==kind::ITE ){ - Trace("sygus-unif") << "...type " << dt.getName() << " has ITE, enumerate child types..." << std::endl; // we can do unification Assert( dt[j].getNumArgs()==3 ); cop_to_strat[cop] = strat_ITE; @@ -405,9 +406,11 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu if( dt[j].getNumArgs()==2 ) { cop_to_strat[cop] = strat_CONCAT; } - Trace("sygus-unif") << "...type " << dt.getName() << " has CONCAT, child types successful = " << success << std::endl; } if( cop_to_strat.find( cop )!=cop_to_strat.end() ){ + Trace("sygus-unif") << "...type " << dt.getName() << " has strategy "; + print_strat("sygus-unif",cop_to_strat[cop]); + Trace("sygus-unif") << "..." << std::endl; // add child types for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){ TypeNode ct = TypeNode::fromType( dt[j][k].getRangeType() ); @@ -417,7 +420,7 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu } } }else if( cop_to_strat.find( cop )==cop_to_strat.end() ){ - // could be a defined function (this is a hack for ICFP benchmarks) + // could be a defined function (this handles the ICFP benchmarks) std::vector< Node > utchildren; utchildren.push_back( cop ); std::vector< Node > sks; @@ -449,7 +452,7 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu cop_to_strat[cop] = strat_ITE; } }else if( eut.getKind()==kind::STRING_CONCAT ){ - if( dt[j].getNumArgs()>=eut.getNumChildren() ){ + if( dt[j].getNumArgs()>=eut.getNumChildren() && eut.getNumChildren()==2 ){ cop_to_strat[cop] = strat_CONCAT; } }else if( eut.getKind()==kind::APPLY_UF ){ @@ -505,7 +508,8 @@ 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 "; - Trace("sygus-unif") << cop_to_strat[cop] << ", enumerate child types..." << std::endl; + print_strat("sygus-unif",cop_to_strat[cop]); + Trace("sygus-unif") << "..." << std::endl; for( unsigned k=0; k<eut.getNumChildren(); k++ ){ Assert( templ_injection.find( k )!=templ_injection.end() ); unsigned sk_index = templ_injection[k]; @@ -602,7 +606,7 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu Assert( !et.isNull() ); d_cinfo[e].d_tinfo[tn].d_strat[cop].d_cenum.push_back( et ); // need to make this take into account template - //Assert( et.getType()==e.getType() || d_einfo[et].d_role!=enum_io ); + //Assert( et.getType()==e.getType() || d_einfo[et].getRole()!=enum_io ); } Trace("sygus-unif") << "Initialized strategy "; print_strat( "sygus-unif", strat ); @@ -655,7 +659,7 @@ void CegConjecturePbe::staticLearnRedundantOps( Node c, std::vector< Node >& 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.d_role ); + print_role( "sygus-unif", itns->second.getRole() ); Trace("sygus-unif") << std::endl; } } @@ -679,7 +683,7 @@ void CegConjecturePbe::staticLearnRedundantOps( Node c, Node e, std::map< Node, indent("sygus-unif", ind); Trace("sygus-unif") << e << " : role : "; - print_role("sygus-unif", itn->second.d_role); + print_role("sygus-unif", itn->second.getRole()); Trace("sygus-unif") << " : "; if( itn->second.isTemplated() ){ @@ -847,7 +851,7 @@ 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.d_role==enum_io ){ + if( itv->second.getRole()==enum_io ){ Trace("sygus-pbe-enum") << " IO-Eval of "; //prevIsCover = itv->second.isFeasible(); }else{ @@ -870,7 +874,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& Assert( res.isConst() ); } Node resb; - if( itv->second.d_role==enum_io ){ + if( itv->second.getRole()==enum_io ){ Node out = itxo->second[j]; Assert( out.isConst() ); resb = res==out ? d_true : d_false; @@ -888,7 +892,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& } } bool keep = false; - if( itv->second.d_role==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; @@ -950,7 +954,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& itv->second.addEnumValue( this, v, results ); /* if( Trace.isOn("sygus-pbe-enum") ){ - if( itv->second.d_role==enum_io ){ + 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; } @@ -1038,7 +1042,7 @@ 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.d_role==enum_concat_term ){ + if( ei.getRole()==enum_concat_term ){ if( Trace.isOn("sygus-pbe-cterm-debug") ){ Trace("sygus-pbe-enum") << std::endl; } @@ -1091,7 +1095,7 @@ void CegConjecturePbe::EnumInfo::addEnumValue( CegConjecturePbe * pbe, Node v, s d_enum_vals.push_back( v ); d_enum_vals_res.push_back( results ); /* - if( d_role==enum_io ){ + if( getRole()==enum_io ){ // compute if( d_enum_total.empty() ){ d_enum_total = results; @@ -1460,12 +1464,12 @@ 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.d_role==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.d_role==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); @@ -1481,7 +1485,7 @@ 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.d_role==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 ); @@ -1518,7 +1522,7 @@ 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.d_role==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 ); @@ -1552,31 +1556,33 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in int incr_type = 0; std::map< Node, std::vector< unsigned > > incr; - // construct the child order + // construct the child order based on heuristics std::vector< unsigned > corder; + std::unordered_set< unsigned > 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. 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].d_role==enum_concat_term ); + Assert( d_einfo[ce].getRole()==enum_concat_term ); corder.push_back( sc ); - unsigned inc = r==0 ? 1 : -1; - unsigned scc = sc + inc; - while( scc>=0 && scc<itts->second.d_cenum.size() ){ - corder.push_back( scc ); - scc = scc + inc; - } + cused.insert( sc ); break; } } - }else{ - for( unsigned sc=0; sc<itts->second.d_cenum.size(); sc++ ){ + } + // fill remaining children for which there is no preference + for( unsigned sc=0; sc<itts->second.d_cenum.size(); sc++ ){ + if( cused.find( sc )==cused.end() ){ corder.push_back( sc ); } - } + } Assert( corder.size()==itts->second.d_cenum.size() ); @@ -1703,7 +1709,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.d_role==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 2f6f591ba..e4c252194 100644 --- a/src/theory/quantifiers/ce_guided_pbe.h +++ b/src/theory/quantifiers/ce_guided_pbe.h @@ -31,21 +31,142 @@ class CegEntailmentInfer; /** CegConjecturePbe * -* This class implements optimizations that target Programming-By-Examples (PBE) -* synthesis conjectures. -* [EX#1] An example of a PBE synthesis conjecture is: +* This class implements optimizations that target synthesis conjectures +* that are in Programming-By-Examples (PBE) form. * -* exists f. forall x. ( x = 0 => f( x ) = 2 ) ^ ( x = 5 => f( x ) = 7 ) ^ ( x = -* 6 => f( x ) = 8 ) +* [EX#1] An example of a synthesis conjecture in PBE form is : +* 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. +* +* Internally, this class does the following for SyGuS inputs: +* +* (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 +* 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 +* 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, +* 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. +* +* An enumerator is initially "active" but may become inactive if the enumeration +* 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(...). +* 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 +* specify incremental problems in SyguS. +* */ class CegConjecturePbe { +public: + CegConjecturePbe( QuantifiersEngine * qe, CegConjecture * p ); + ~CegConjecturePbe(); + + /** initialize this class */ + void initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas ); + /** get candidate list + * 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 + * 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(...). + */ + bool constructCandidates( std::vector< Node >& enums, std::vector< Node >& enum_values, + std::vector< Node >& candidates, std::vector< Node >& candidate_values, + std::vector< Node >& 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 */ + unsigned getNumExamples(Node e); + /** get the input arguments for i^th I/O example for e, which is added to the + * vector ex */ + void getExample(Node e, unsigned i, std::vector<Node>& 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 + * 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. + * - 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 + * 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: + /** quantifiers engine associated with this class */ QuantifiersEngine* d_qe; + /** sygus term database of d_qe */ quantifiers::TermDbSygus * d_tds; + /** true and false nodes */ + Node d_true; + Node d_false; + /** parent conjecture + * This is the data structure that contains global information about the conjecture. + */ CegConjecture* d_parent; - + /** is this a PBE conjecture for any function? */ + bool d_is_pbe; /** for each candidate variable f (a function-to-synthesize), whether the * conjecture is purely PBE for that variable * In other words, all occurrences of f are guarded by equalities that @@ -56,7 +177,12 @@ private: * conjecture is purely PBE for that variable. * An example of a conjecture for which d_examples_invalid is false but * d_examples_out_invalid is true is: - * exists f. forall x. ( x = 0 => f( x ) > 2 ) + * 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). + * However, the domain of f in both cases is finite, which can be used for + * search space pruning. */ std::map< Node, bool > d_examples_out_invalid; /** for each candidate variable (function-to-synthesize), input of I/O @@ -65,8 +191,9 @@ 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 @@ -74,58 +201,16 @@ private: * approaches (e.g. decision tree construction). */ std::map<Node, Node> d_enum_to_candidate; - + /** 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 ); - bool d_is_pbe; -public: - Node d_true; - Node d_false; - enum { - enum_io, - enum_ite_condition, - enum_concat_term, - enum_any, - }; - enum { - strat_ITE, - strat_CONCAT, - strat_ID, - }; -public: - CegConjecturePbe( QuantifiersEngine * qe, CegConjecture * p ); - ~CegConjecturePbe(); - - void initialize( Node n, std::vector< Node >& candidates, std::vector< Node >& lemmas ); - bool getPbeExamples( Node v, std::vector< std::vector< Node > >& exs, - std::vector< Node >& exos, std::vector< Node >& exts); - /** is PBE enabled for any enumerator? */ - bool isPbe() { return d_is_pbe; } - /** get candidate for enumerator */ - Node getCandidateForEnumerator(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 */ - unsigned getNumExamples(Node e); - /** get the input arguments for i^th I/O example for e, which is added to the - * vector ex */ - void getExample(Node e, unsigned i, std::vector<Node>& ex); - /** get the output value of the i^th I/O example for enumerator e */ - Node getExampleOut(Node e, unsigned i); - int getExampleId(Node n); - /** add the search val, returns an equivalent value (possibly the same) */ - Node addSearchVal(TypeNode tn, Node e, Node bvr); - /** evaluate builtin */ - Node evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i); - - private: + + //--------------------------------- PBE search values /** this class is an index of candidate solutions for PBE synthesis */ class PbeTrie { - private: - Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector<Node>& ex, - CegConjecturePbe* cpbe, unsigned index, - unsigned ntotal); - - public: + public: PbeTrie() {} ~PbeTrie() {} Node d_lazy_child; @@ -133,25 +218,22 @@ public: void clear() { d_children.clear(); } Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe, unsigned index, unsigned ntotal); + private: + Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector<Node>& ex, + CegConjecturePbe* cpbe, unsigned index, + unsigned ntotal); }; - /** trie of candidate solutions tried, for each (enumerator, type), - * where type is a type in the grammar of the space of solutions for a subterm - * of e - */ + /** trie of candidate solutions tried + * This stores information for each (enumerator, type), + * where type is a type in the grammar of the space of solutions for a subterm + * of e. This is used for symmetry breaking in quantifier-free reasoning + * about SyGuS datatypes. + */ std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie; - - private: // for 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 ); - - /** register candidate conditional */ - bool inferTemplate( unsigned k, Node n, std::map< Node, unsigned >& templ_var_index, std::map< unsigned, unsigned >& templ_injection ); - /** get guard status */ - int getGuardStatus( Node g ); -public: + //--------------------------------- end PBE search values + + // -------------------------------- decision tree learning + //index filter class IndexFilter { public: IndexFilter(){} @@ -161,17 +243,11 @@ public: unsigned next( unsigned i ); void clear() { d_next.clear(); } bool isEq( std::vector< Node >& vs, Node v ); - }; -private: + }; // subsumption trie class SubsumeTrie { - private: - 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 ); public: SubsumeTrie(){} - Node d_term; - std::map< Node, SubsumeTrie > d_children; // adds term to the trie, removes based on subsumption Node addTerm( CegConjecturePbe * pbe, Node t, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f = NULL ); // adds condition to the trie (does not do subsumption) @@ -180,37 +256,74 @@ private: void getSubsumed( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed, IndexFilter * f = NULL ); // returns the set of terms that are supersets of vals void getSubsumedBy( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::vector< Node >& subsumed_by, IndexFilter * f = NULL ); - private: - void getLeavesInternal( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f, - unsigned index, int status ); - public: // v[-1,1,0] -> children always false, always true, both void getLeaves( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol, std::map< int, std::vector< Node > >& v, IndexFilter * f = NULL ); - public: + /** is this trie empty? */ bool isEmpty() { return d_term.isNull() && d_children.empty(); } + /** clear this trie */ void clear() { d_term = Node::null(); d_children.clear(); } + private: + /** the term at this node */ + Node d_term; + /** the children nodes of this trie */ + std::map< Node, SubsumeTrie > 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 ); + /** 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 ); }; - + // -------------------------------- end decision tree learning + + //------------------------------ representation of a enumeration strategy + + /** roles for enumerators */ + enum { + enum_io, + enum_ite_condition, + enum_concat_term, + enum_any, + }; + /** print the role with Trace c. */ + static void print_role( const char * c, unsigned r ); + /** strategies for SyGuS datatype types */ + enum { + strat_ITE, + strat_CONCAT, + strat_ID, + }; + /** print the strategy with Trace c. */ + static void print_strat( const char * c, unsigned s ); + + /** information about an enumerator */ class EnumInfo { - private: - /** an OR of all in d_enum_res */ - //std::vector< Node > d_enum_total; - //bool d_enum_total_true; - Node d_enum_solved; public: EnumInfo() : d_role( enum_io ){} - Node d_parent_candidate; + /** 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 ){ + 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 ); + 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; Node d_template_arg; - // TODO : make private - unsigned d_role; - Node d_active_guard; std::vector< Node > d_enum_slave; /** values we have enumerated */ @@ -222,16 +335,18 @@ private: std::vector< Node > d_enum_subsume; std::map< Node, unsigned > d_enum_val_to_index; SubsumeTrie d_term_trie; - public: - bool isTemplated() { return !d_template.isNull(); } - void addEnumValue( CegConjecturePbe * pbe, Node v, std::vector< Node >& results ); - void setSolved( Node slv ); - bool isSolved() { return !d_enum_solved.isNull(); } - Node getSolved() { return d_enum_solved; } + 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; -private: + + class CandidateInfo; + /** represents a strategy for a SyGuS datatype type */ class EnumTypeInfoStrat { public: unsigned d_this; @@ -239,6 +354,9 @@ private: std::vector< TypeNode > d_csol_cts; std::vector< Node > d_cenum; }; + + + /** stores enumerators and strategies for a SyGuS datatype type */ class EnumTypeInfo { public: EnumTypeInfo() : d_parent( NULL ){} @@ -250,14 +368,23 @@ private: std::map< Node, EnumTypeInfoStrat > d_strat; bool isSolved( CegConjecturePbe * pbe ); }; + + + /** stores strategy and enumeration information for a function-to-synthesize */ class CandidateInfo { public: CandidateInfo() : d_check_sol( false ), d_cond_count( 0 ){} Node d_this_candidate; + /** root SyGuS datatype for the function-to-synthesize, + * which encodes the overall syntactic restrictions on the space + * of solutions. + */ TypeNode 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; - // role -> sygus type -> enumerator + /** maps sygus datatypes to their enumerator */ std::map< TypeNode, Node > d_search_enum; bool d_check_sol; unsigned d_cond_count; @@ -267,25 +394,27 @@ private: Node getRootEnumerator(); bool isNonTrivial(); }; - // candidate -> sygus type -> info + /** 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 ); -private: - // filtering verion - /* - class FilterSubsumeTrie { - public: - SubsumeTrie d_trie; - IndexFilter d_filter; - Node addTerm( Node t, std::vector< bool >& vals, std::vector< Node >& subsumed, bool checkExistsOnly = false ){ - return d_trie.addTerm( t, vals, subsumed, &d_filter, d_filter.start(), checkExistsOnly ); - } - }; - */ + //------------------------------ 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 ); + + /** 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 + + + //------------------------------ constructing solutions class UnifContext { public: UnifContext() : d_has_string_pos(0) {} @@ -319,25 +448,35 @@ private: }; /** construct solution */ Node constructSolution( Node c ); + /** helper function for construct solution. + * Construct a solution based on enumerator e for function-to-synthesize c, + * 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. */ Node constructBestSolvedTerm( std::vector< Node >& solved, UnifContext& x ); + /** 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 */ Node constructBestSolvedConditional( std::vector< Node >& solved, UnifContext& x ); + /** 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. + * total_inc[x] is the sum of incr[x] for each x in strs. + */ Node constructBestStringToConcat( std::vector< Node > strs, std::map< Node, unsigned > total_inc, std::map< Node, std::vector< unsigned > > incr, UnifContext& x ); - void getStringIncrement( bool isPrefix, Node c, Node v, - std::map< Node, unsigned > total_inc, - std::map< Node, std::vector< unsigned > > incr ); -public: - void registerCandidates( std::vector< Node >& candidates ); - void getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ); - // lems and candidate values are outputs - bool constructCandidates( std::vector< Node >& enums, std::vector< Node >& enum_values, - std::vector< Node >& candidates, std::vector< Node >& candidate_values, - std::vector< Node >& lems ); + //------------------------------ end constructing solutions + + /** 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 ); }; diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index a297cee81..6dfcb922a 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -65,7 +65,8 @@ TESTS = commutative.sy \ parse-bv-let.sy \ cegar1.sy \ triv-type-mismatch-si.sy \ - nia-max-square-ns.sy + nia-max-square-ns.sy \ + strings-concat-3-args.sy # sygus tests currently taking too long for make regress diff --git a/test/regress/regress0/sygus/strings-concat-3-args.sy b/test/regress/regress0/sygus/strings-concat-3-args.sy new file mode 100644 index 000000000..3c93c51d3 --- /dev/null +++ b/test/regress/regress0/sygus/strings-concat-3-args.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth +(set-logic SLIA) +(synth-fun f ((x String)) String +((Start String (ntString)) + +(ntString String (x "" (str.++ ntStringConst ntString ntString))) + +(ntStringConst String ("a" "b" " ")) + +)) + +; can be solved with concat PBE strategy, although we currently are not (issue #1259) +; regardless, this is small enough to solve quickly +(constraint (= (f "def") "ab def")) + +(check-synth) + |