/********************* */ /*! \file sygus_pbe.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 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 utility for processing programming by examples synthesis conjectures **/ #include "cvc4_private.h" #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H #include "context/cdhashmap.h" #include "theory/quantifiers/sygus/sygus_module.h" #include "theory/quantifiers/sygus/sygus_unif_io.h" namespace CVC4 { namespace theory { namespace quantifiers { class CegConjecture; /** CegConjecturePbe * * This class implements optimizations that target synthesis conjectures * that are in Programming-By-Examples (PBE) form. * * [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 managed through the SygusUnif * utilities, d_sygus_unif. * (3) It makes (possibly multiple) calls to * TermDatabaseSygus::regstierEnumerator(...) 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 * 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 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_sygus_unif). * * This class is not designed to work in incremental mode, since there is no way * to specify incremental problems in SyguS. */ class CegConjecturePbe : public SygusModule { public: CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p); ~CegConjecturePbe(); /** initialize this class * * 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. */ bool initialize(Node n, const std::vector& candidates, std::vector& lemmas) override; /** get term list * * Adds all active enumerators associated with functions-to-synthesize in * candidates to terms. */ void getTermList(const std::vector& candidates, std::vector& terms) override; /** construct candidates * * This function attempts to use unification-based approaches for constructing * solutions for all functions-to-synthesize (indicated by candidates). These * approaches include decision tree learning and a divide-and-conquer * algorithm based on string concatenation. * * Calls to this function are such that terms is the list of active * enumerators (returned by getTermList), and term_values are their current * model values. This function registers { terms -> terms_values } in * the database of values that have been enumerated, which are in turn used * for constructing candidate solutions when possible. * * This function also excludes models where (terms = terms_values) by adding * blocking clauses to lems. For example, for grammar: * A -> A+A | x | 1 | 0 * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds: * ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 ) * to lems, where G is active guard of the enumerator d (see * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause * indicates that d should not be given the model value +( x, 1 ) anymore, * since { d -> +( x, 1 ) } has now been added to the database of this class. */ bool constructCandidates(const std::vector& terms, const std::vector& term_values, const std::vector& candidates, std::vector& candidate_values, std::vector& lems) override; /** is PBE enabled for any enumerator? */ bool isPbe() { return d_is_pbe; } /** 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& 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: /** true and false nodes */ Node d_true; Node d_false; /** 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 * constraint its arguments to constants. */ std::map d_examples_invalid; /** for each candidate variable (function-to-synthesize), whether the * 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 ) * 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 d_examples_out_invalid; /** * Map from candidates to sygus unif utility. This class implements * the core algorithm (e.g. decision tree learning) that this module relies * upon. */ std::map d_sygus_unif; /** * map from candidates to the list of enumerators that are being used to * build solutions for that candidate by the above utility. */ std::map > d_candidate_to_enum; /** reverse map of above */ std::map d_enum_to_candidate; /** map from enumerators to active guards */ std::map d_enum_to_active_guard; /** for each candidate variable (function-to-synthesize), input of I/O * examples */ std::map > > d_examples; /** for each candidate variable (function-to-synthesize), output of I/O * examples */ std::map > d_examples_out; /** the list of example terms * For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 ) */ std::map > d_examples_term; /** 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& visited, bool hasPol, bool pol); //--------------------------------- PBE search values /** * This class is an index of candidate solutions for PBE synthesis and their * (concrete) evaluation on the set of input examples. For example, if the * set of input examples for (x,y) is (0,1), (1,3), then: * term x is indexed by 0,1 * term x+y is indexed by 1,4 * term 0 is indexed by 0,0. */ class PbeTrie { public: PbeTrie() {} ~PbeTrie() {} /** the data for this node in the trie */ Node d_lazy_child; /** the children for this node in the trie */ std::map d_children; /** clear this trie */ void clear() { d_children.clear(); } /** * Add term b as a value enumerated for enumerator e to the trie. * * cpbe : reference to the parent pbe utility which stores the examples, * index : the index of the example we are processing, * ntotal : the total of the examples for enumerator e. */ Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe, unsigned index, unsigned ntotal); private: /** Helper function for above, called when we get the current example ex. */ Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector& ex, CegConjecturePbe* cpbe, unsigned index, unsigned ntotal); }; /** 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 > d_pbe_trie; //--------------------------------- end PBE search values }; } /* namespace CVC4::theory::quantifiers */ } /* namespace CVC4::theory */ } /* namespace CVC4 */ #endif