diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_pbe.h')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_pbe.h | 802 |
1 files changed, 0 insertions, 802 deletions
diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h deleted file mode 100644 index ce1f2bf5e..000000000 --- a/src/theory/quantifiers/ce_guided_pbe.h +++ /dev/null @@ -1,802 +0,0 @@ -/********************* */ -/*! \file ce_guided_pbe.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 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_engine.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -/** roles for enumerators - * - * This indicates the role of an enumerator that is allocated by approaches - * for synthesis-by-unification (see details below). - * io : the enumerator should enumerate values that are overall solutions - * for the function-to-synthesize, - * ite_condition : the enumerator should enumerate values that are useful - * in ite conditions in the ITE strategy, - * concat_term : the enumerator should enumerate values that are used as - * components of string concatenation solutions. - */ -enum EnumRole -{ - enum_invalid, - enum_io, - enum_ite_condition, - enum_concat_term, -}; -std::ostream& operator<<(std::ostream& os, EnumRole r); - -/** roles for strategy nodes - * - * This indicates the role of a strategy node, which is a subprocedure of - * CegConjecturePbe::constructSolution (see details below). - * equal : the node constructed must be equal to the overall solution for - * the function-to-synthesize, - * string_prefix/suffix : the node constructed must be a prefix/suffix - * of the function-to-synthesize, - * ite_condition : the node constructed must be a condition that makes some - * active input examples true and some input examples false. - */ -enum NodeRole -{ - role_invalid, - role_equal, - role_string_prefix, - role_string_suffix, - role_ite_condition, -}; -std::ostream& operator<<(std::ostream& os, NodeRole r); - -/** enumerator role for node role */ -EnumRole getEnumeratorRoleForNodeRole(NodeRole r); - -/** strategy types - * - * This indicates a strategy for synthesis-by-unification (see details below). - * ITE : strategy for constructing if-then-else solutions via decision - * tree learning techniques, - * CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation - * solutions via a divide and conquer approach, - * ID : identity strategy used for calling strategies on child type through - * an identity function. - */ -enum StrategyType -{ - strat_INVALID, - strat_ITE, - strat_CONCAT_PREFIX, - strat_CONCAT_SUFFIX, - strat_ID, -}; -std::ostream& operator<<(std::ostream& os, StrategyType st); - -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 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 -* 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_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 - * - * 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<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; } - /** 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; - /** A reference to the conjecture that owns this class. */ - 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 - * constraint its arguments to constants. - */ - std::map< Node, bool > 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< Node, bool > d_examples_out_invalid; - /** for each candidate variable (function-to-synthesize), input of I/O - * examples */ - std::map< Node, std::vector< std::vector< Node > > > d_examples; - /** 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 ) - */ - std::map< Node, std::vector< Node > > 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< Node, bool >& visited, bool hasPol, bool pol ); - - //--------------------------------- PBE search values - /** this class is an index of candidate solutions for PBE synthesis */ - class PbeTrie { - public: - PbeTrie() {} - ~PbeTrie() {} - Node d_lazy_child; - std::map<Node, PbeTrie> d_children; - 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 - * 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; - //--------------------------------- end PBE search values - - // -------------------------------- decision tree learning - // index filter - class IndexFilter { - public: - IndexFilter(){} - void mk( std::vector< Node >& vals, bool pol = true ); - std::map< unsigned, unsigned > d_next; - unsigned start(); - unsigned next( unsigned i ); - void clear() { d_next.clear(); } - bool isEq( std::vector< Node >& vs, Node v ); - }; - // subsumption trie - class SubsumeTrie { - public: - SubsumeTrie(){} - // 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) - Node addCond( CegConjecturePbe * pbe, Node c, std::vector< Node >& vals, bool pol, IndexFilter * f = NULL ); - // returns the set of terms that are subsets of vals - 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 ); - // 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 ); - /** 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 - - /** information about an enumerator - * - * We say an enumerator is a master enumerator if it is the variable that - * we use to enumerate values for its sort. Master enumerators may have - * (possibly multiple) slave enumerators, stored in d_enum_slave, - */ - class EnumInfo { - public: - EnumInfo() : d_role(enum_io), d_is_conditional(false) {} - /** 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, EnumRole role); - /** is this enumerator associated with a template? */ - bool isTemplated() { return !d_template.isNull(); } - /** set conditional - * - * This flag is set to true if this enumerator may not apply to all - * input/output examples. For example, if this enumerator is used - * as an output value beneath a conditional in an instance of strat_ITE, - * then this enumerator is conditional. - */ - void setConditional() { d_is_conditional = true; } - /** is conditional */ - bool isConditional() { return d_is_conditional; } - 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; } - EnumRole getRole() { return d_role; } - Node d_parent_candidate; - // for template - Node d_template; - Node d_template_arg; - - Node d_active_guard; - std::vector<Node> d_enum_slave; - /** values we have enumerated */ - std::vector<Node> d_enum_vals; - /** - * This either stores the values of f( I ) for inputs - * or the value of f( I ) = O if d_role==enum_io - */ - std::vector<std::vector<Node> > d_enum_vals_res; - 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. - */ - Node d_enum_solved; - /** the role of this enumerator (one of enum_* above). */ - EnumRole d_role; - /** is this enumerator conditional */ - bool d_is_conditional; - }; - /** maps enumerators to the information above */ - std::map< Node, EnumInfo > d_einfo; - - class CandidateInfo; - - /** represents a strategy for a SyGuS datatype type - * - * This represents a possible strategy to apply when processing a strategy - * node in constructSolution. When applying the strategy represented by this - * class, we may make recursive calls to the children of the strategy, - * given in d_cenum. If all recursive calls to constructSolution are - * successful, say: - * constructSolution( c, d_cenum[1], ... ) = t1, - * ..., - * constructSolution( c, d_cenum[n], ... ) = tn, - * Then, the solution returned by this strategy is - * d_sol_templ * { d_sol_templ_args -> (t1,...,tn) } - */ - class EnumTypeInfoStrat { - public: - /** the type of strategy this represents */ - StrategyType d_this; - /** the sygus datatype constructor that induced this strategy - * - * For example, this may be a sygus datatype whose sygus operator is ITE, - * if the strategy type above is strat_ITE. - */ - Node d_cons; - /** children of this strategy */ - std::vector<std::pair<Node, NodeRole> > d_cenum; - /** the arguments for the (templated) solution */ - std::vector<Node> d_sol_templ_args; - /** the template for the solution */ - Node d_sol_templ; - }; - - /** represents a node in the strategy graph - * - * It contains a list of possible strategies which are tried during calls - * to constructSolution. - */ - class StrategyNode - { - public: - StrategyNode() {} - ~StrategyNode(); - /** the set of strategies to try at this node in the strategy graph */ - std::vector<EnumTypeInfoStrat*> d_strats; - }; - - /** stores enumerators and strategies for a SyGuS datatype type */ - class EnumTypeInfo { - public: - EnumTypeInfo() : d_parent( NULL ){} - /** the parent candidate info (see below) */ - CandidateInfo * d_parent; - /** the type that this information is for */ - TypeNode d_this_type; - /** map from enum roles to enumerators for this type */ - std::map<EnumRole, Node> d_enum; - /** map from node roles to strategy nodes */ - std::map<NodeRole, StrategyNode> d_snodes; - }; - - /** 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; - /** - * The root sygus datatype for the function-to-synthesize, - * which encodes the overall syntactic restrictions on the space - * of solutions. - */ - TypeNode d_root; - /** Info for 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; - /** - * Maps sygus datatypes to their search enumerator. This is the (single) - * enumerator of that type that we enumerate values for. - */ - std::map< TypeNode, Node > d_search_enum; - bool d_check_sol; - unsigned d_cond_count; - Node d_solution; - void initialize( Node c ); - void initializeType( TypeNode tn ); - Node getRootEnumerator(); - bool isNonTrivial(); - }; - /** maps a function-to-synthesize to the above information */ - std::map< Node, CandidateInfo > d_cinfo; - - //------------------------------ representation of an enumeration strategy - /** add enumerated value - * - * We have enumerated the value v for x. This function adds x->v to the - * relevant data structures that are used for strategy-specific construction - * of solutions when necessary, and returns a set of lemmas, which are added - * to the input argument lems. These lemmas are used to rule out models where - * x = v, to force that a new value is enumerated for x. - */ - void addEnumeratedValue( Node x, Node v, std::vector< Node >& lems ); - /** domain-specific enumerator exclusion techniques - * - * Returns true if the value v for x can be excluded based on a - * domain-specific exclusion technique like the ones below. - * - * c : the candidate variable that x is enumerating for, - * results : the values of v under the input examples of c, - * ei : the enumerator information for x, - * exp : if this function returns true, then exp contains a (possibly - * generalize) explanation for why v can be excluded. - */ - bool getExplanationForEnumeratorExclude( Node c, Node x, Node v, std::vector< Node >& results, EnumInfo& ei, std::vector< Node >& exp ); - /** returns true if we can exlude values of x based on negative str.contains - * - * Values v for x may be excluded if we realize that the value of v under the - * substitution for some input example will never be contained in some output - * example. For details on this technique, see NegContainsSygusInvarianceTest - * in sygus_invariance.h. - * - * This function depends on whether x is being used to enumerate values - * for any node that is conditional in the strategy graph. For example, - * nodes that are children of ITE strategy nodes are conditional. If any node - * is conditional, then this function returns false. - */ - bool useStrContainsEnumeratorExclude(Node x, EnumInfo& ei); - /** cache for the above function */ - std::map<Node, bool> d_use_str_contains_eexc; - - //------------------------------ strategy registration - /** collect enumerator types - * - * This builds the strategy for enumerated values of type tn for the given - * role of nrole, for solutions to function-to-synthesize c. - */ - void collectEnumeratorTypes(Node c, TypeNode tn, NodeRole nrole); - /** register enumerator - * - * This registers that et is an enumerator for function-to-synthesize c - * of type tn, having enumerator role enum_role. - * - * inSearch is whether we will enumerate values based on this enumerator. - * A strategy node is represented by a (enumerator, node role) pair. Hence, - * we may use enumerators for which this flag is false to represent strategy - * nodes that have child strategies. - */ - void registerEnumerator( - Node et, Node c, TypeNode tn, EnumRole enum_role, bool inSearch); - /** infer template */ - bool inferTemplate(unsigned k, - Node n, - std::map<Node, unsigned>& templ_var_index, - std::map<unsigned, unsigned>& templ_injection); - /** static learn redundant operators - * - * This learns static lemmas for pruning enumerative space based on the - * strategy for the function-to-synthesize c, and stores these into lemmas. - */ - void staticLearnRedundantOps(Node c, std::vector<Node>& lemmas); - /** helper for static learn redundant operators - * - * (e, nrole) specify the strategy node in the graph we are currently - * analyzing, visited stores the nodes we have already visited. - * - * This method builds the mapping needs_cons, which maps (master) enumerators - * to a map from the constructors that it needs. - * - * ind is the depth in the strategy graph we are at (for debugging). - * - * isCond is whether the current enumerator is conditional (beneath a - * conditional of an strat_ITE strategy). - */ - void staticLearnRedundantOps( - Node c, - Node e, - NodeRole nrole, - std::map<Node, std::map<NodeRole, bool> >& visited, - std::map<Node, std::map<unsigned, bool> >& needs_cons, - int ind, - bool isCond); - //------------------------------ end strategy registration - - //------------------------------ constructing solutions - class UnifContext { - public: - UnifContext() : d_has_string_pos(role_invalid) {} - /** this intiializes this context for function-to-synthesize c */ - void initialize(CegConjecturePbe* pbe, Node c); - - //----------for ITE strategy - /** the value of the context conditional - * - * This stores a list of Boolean constants that is the same length of the - * number of input/output example pairs we are considering. For each i, - * if d_vals[i] = true, i/o pair #i is active according to this context - * if d_vals[i] = false, i/o pair #i is inactive according to this context - */ - std::vector<Node> d_vals; - /** update the examples - * - * if pol=true, this method updates d_vals to d_vals & vals - * if pol=false, this method updates d_vals to d_vals & ( ~vals ) - */ - bool updateContext(CegConjecturePbe* pbe, std::vector<Node>& vals, bool pol); - //----------end for ITE strategy - - //----------for CONCAT strategies - /** the position in the strings - * - * For each i/o example pair, this stores the length of the current solution - * for the input of the pair, where the solution for that input is a prefix - * or - * suffix of the output of the pair. For example, if our i/o pairs are: - * f( "abcd" ) = "abcdcd" - * f( "aa" ) = "aacd" - * If the solution we have currently constructed is str.++( x1, "c", ... ), - * then d_str_pos = ( 5, 3 ), where notice that - * str.++( "abc", "c" ) is a prefix of "abcdcd" and - * str.++( "aa", "c" ) is a prefix of "aacd". - */ - std::vector<unsigned> d_str_pos; - /** has string position - * - * Whether the solution positions indicate a prefix or suffix of the output - * examples. If this is role_invalid, then we have not updated the string - * position. - */ - NodeRole d_has_string_pos; - /** update the string examples - * - * This method updates d_str_pos to d_str_pos + pos. - */ - bool updateStringPosition(CegConjecturePbe* pbe, std::vector<unsigned>& pos); - /** get current strings - * - * This returns the prefix/suffix of the string constants stored in vals - * of size d_str_pos, and stores the result in ex_vals. For example, if vals - * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add - * "d" and "de" to ex_vals. - */ - void getCurrentStrings(CegConjecturePbe* pbe, - const std::vector<Node>& vals, - std::vector<String>& ex_vals); - /** get string increment - * - * If this method returns true, then inc and tot are updated such that - * for all active indices i, - * vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and - * inc[i] = str.len(vals[i]) - * for all inactive indices i, inc[i] = 0 - * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total - * number of characters incremented across all examples. - */ - bool getStringIncrement(CegConjecturePbe* pbe, - bool isPrefix, - const std::vector<String>& ex_vals, - const std::vector<Node>& vals, - std::vector<unsigned>& inc, - unsigned& tot); - /** returns true if ex_vals[i] = vals[i] for all active indices i. */ - bool isStringSolved(CegConjecturePbe* pbe, - const std::vector<String>& ex_vals, - const std::vector<Node>& vals); - //----------end for CONCAT strategies - - /** is return value modified? - * - * This returns true if we are currently in a state where the return value - * of the solution has been modified, e.g. by a previous node that solved - * for a prefix. - */ - bool isReturnValueModified(); - /** returns true if argument is valid strategy in this context */ - bool isValidStrategy(EnumTypeInfoStrat* etis); - /** visited role - * - * This is the current set of enumerator/node role pairs we are currently - * visiting. This set is cleared when the context is updated. - */ - std::map<Node, std::map<NodeRole, bool> > d_visit_role; - - /** unif context enumerator information */ - class UEnumInfo - { - public: - UEnumInfo() {} - /** map from conditions and branch positions to a solved node - * - * For example, if we have: - * f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 - * Then, valid entries in this map is: - * d_look_ahead_sols[x>0][1] = x+1 - * d_look_ahead_sols[x>0][2] = 1 - * For the first entry, notice that for all input examples such that x>0 - * evaluates to true, which are (1) and (3), we have that their output - * values for x+1 under the substitution that maps x to the input value, - * resulting in 2 and 4, are equal to the output value for the respective - * pairs. - */ - std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols; - }; - /** map from enumerators to the above info class */ - std::map< Node, UEnumInfo > d_uinfo; - }; - - /** construct solution - * - * This method tries to construct a solution for function-to-synthesize c - * based on the strategy stored for c in d_cinfo, which may include - * synthesis-by-unification approaches for ite and string concatenation terms. - * These approaches include the work of Alur et al. TACAS 2017. - * If it cannot construct a solution, it returns the null node. - */ - Node constructSolution( Node c ); - /** helper function for construct solution. - * - * Construct a solution based on enumerator e for function-to-synthesize c - * with node role nrole in context x. - * - * ind is the term depth of the context (for debugging). - */ - Node constructSolution( - Node c, Node e, NodeRole nrole, 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 ); - //------------------------------ end constructing solutions -}; - -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ - -#endif |