}
}
}
+
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++ ){
}
}
}
-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;
}
}
+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){
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();
}
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()) {
}
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()) {
}
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());
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();
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 =
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;
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 );
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 ){
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;
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() );
}
}
}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;
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 ){
}
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];
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 );
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;
}
}
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() ){
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{
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;
}
}
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;
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;
}
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;
}
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;
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);
// 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 );
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 );
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() );
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 ){
/** 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
* 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
/** 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
* 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;
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(){}
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)
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 */
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;
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 ){}
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;
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) {}
};
/** 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 );
};
projects / cvc5.git / commitdiff