diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-27 16:54:05 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-27 16:54:05 -0500 |
commit | 0baee856785df0f018fa2a007f62299c45fd8e5d (patch) | |
tree | 0d1f7d42620561ef94e52e37dec0adece27933d6 /src/theory/quantifiers/sygus/sygus_pbe.h | |
parent | d8c56098916be16ba80c79933c2e6fc7850024b7 (diff) |
Make sygus pbe use sygus unif utility (#1724)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.h')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.h | 608 |
1 files changed, 23 insertions, 585 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index dd98dd0aa..fb353a102 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -47,10 +47,10 @@ class CegConjecture; * 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. +* permits string concatenation. This is managed through the SygusUnif +* utilities, d_sygus_unif. * (3) It makes (possibly multiple) calls to -* TermDatabaseSygus::registerMeasuredTerm(...) based +* 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". @@ -58,14 +58,14 @@ class CegConjecture; * 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 +* 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 +* restrictions for it. The search may continue unless all enumerators become * inactive. * * (4) During search, the extension of quantifier-free datatypes procedure for @@ -73,7 +73,7 @@ class CegConjecture; * 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 +* 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 @@ -216,6 +216,21 @@ class CegConjecturePbe : public SygusModule * search space pruning. */ std::map< Node, bool > 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<Node, SygusUnif> 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<Node, std::vector<Node> > d_candidate_to_enum; + /** reverse map of above */ + std::map<Node, Node> d_enum_to_candidate; + /** map from enumerators to active guards */ + std::map<Node, Node> d_enum_to_active_guard; /** for each candidate variable (function-to-synthesize), input of I/O * examples */ std::map< Node, std::vector< std::vector< Node > > > d_examples; @@ -258,583 +273,6 @@ class CegConjecturePbe : public SygusModule std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie; //--------------------------------- end PBE search values - // -------------------------------- decision tree learning - /** Subsumption trie - * - * This class manages a set of terms for a PBE sygus enumerator. - * - * In PBE sygus, we are interested in, for each term t, the set of I/O examples - * that it satisfies, which can be represented by a vector of Booleans. - * For example, given conjecture: - * f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5 - * If solutions for f are of the form (lambda x. [term]), then: - * Term x satisfies 0001, - * Term x+1 satisfies 1100, - * Term 2 satisfies 0100. - * Above, term 2 is subsumed by term x+1, since the set of I/O examples that - * x+1 satisfies are a superset of those satisfied by 2. - */ - class SubsumeTrie - { - public: - SubsumeTrie() {} - /** - * Adds term t to the trie, removes all terms that are subsumed by t from the - * trie and adds them to subsumed. The set of I/O examples that t satisfies - * is given by (pol ? vals : !vals). - */ - Node addTerm(Node t, - const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed); - /** - * Adds term c to the trie, without calculating/updating based on - * subsumption. This is useful for using this class to store conditionals - * in ITE strategies, where any conditional whose set of vals is unique - * (as opposed to not subsumed) is useful. - */ - Node addCond(Node c, const std::vector<Node>& vals, bool pol); - /** - * Returns the set of terms that are subsumed by (pol ? vals : !vals). - */ - void getSubsumed(const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed); - /** - * Returns the set of terms that subsume (pol ? vals : !vals). This - * is for instance useful when determining whether there exists a term - * that satisfies all active examples in the decision tree learning - * algorithm. - */ - void getSubsumedBy(const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed_by); - /** - * Get the leaves of the trie, which we store in the map v. - * v[-1] stores the children that always evaluate to !pol, - * v[1] stores the children that always evaluate to pol, - * v[0] stores the children that both evaluate to true and false for at least - * one example. - */ - void getLeaves(const std::vector<Node>& vals, - bool pol, - std::map<int, std::vector<Node> >& v); - /** 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(Node t, - const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed, - bool spol, - unsigned index, - int status, - bool checkExistsOnly, - bool checkSubsume); - /** helper function for above functions */ - void getLeavesInternal(const std::vector<Node>& vals, - bool pol, - std::map<int, std::vector<Node> >& v, - unsigned index, - int status); - }; - // -------------------------------- end decision tree learning - - //------------------------------ representation of a enumeration strategy - /** - * This class stores information regarding an enumerator, including: - * - Information regarding the role of this enumerator (see EnumRole), its - * parent, whether it is templated, its slave enumerators, and so on, and - * - A database of values that have been enumerated for this 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. We make - * the first enumerator for each type a master enumerator, and any additional - * ones slaves of it. - */ - 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; } - /** get the role of this enumerator */ - EnumRole getRole() { return d_role; } - /** - * The candidate variable that this enumerator is for (see sygus_pbe.h). - */ - Node d_parent_candidate; - /** enumerator template - * - * If d_template non-null, enumerated values V are immediately transformed to - * d_template { d_template_arg -> V }. - */ - Node d_template; - Node d_template_arg; - /** - * The active guard of this enumerator (see - * TermDbSygus::d_enum_to_active_guard). - */ - Node d_active_guard; - /** - * Slave enumerators of this enumerator. These are other enumerators that - * have the same type, but a different role in the strategy tree. We - * generally - * only use one enumerator per type, and hence these slaves are notified when - * values are enumerated for this enumerator. - */ - std::vector<Node> d_enum_slave; - - //---------------------------enumerated values - /** - * Notify this class that the term v has been enumerated for this enumerator. - * Its evaluation under the set of examples in pbe are stored in results. - */ - void addEnumValue(CegConjecturePbe* pbe, - Node v, - std::vector<Node>& results); - /** - * Notify this class that slv is the complete solution to the synthesis - * conjecture. This occurs rarely, for instance, when during an ITE strategy - * we find that a single enumerated term covers all examples. - */ - void setSolved(Node slv); - /** Have we been notified that a complete solution exists? */ - bool isSolved() { return !d_enum_solved.isNull(); } - /** Get the complete solution to the synthesis conjecture. */ - Node getSolved() { return d_enum_solved; } - /** Values that have been enumerated for this enumerator */ - 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; - /** - * The set of values in d_enum_vals that have been "subsumed" by others - * (see SubsumeTrie for explanation of subsumed). - */ - std::vector<Node> d_enum_subsume; - /** Map from values to their index in d_enum_vals. */ - std::map<Node, unsigned> d_enum_val_to_index; - /** - * A subsumption trie containing the values in d_enum_vals. Depending on the - * role of this enumerator, values may either be added to d_term_trie with - * subsumption (if role=enum_io), or without (if role=enum_ite_condition or - * enum_concat_term). - */ - SubsumeTrie d_term_trie; - //---------------------------end enumerated values - 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; - class EnumTypeInfoStrat; - - /** 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 - /** Unification context - * - * This class maintains state information during calls to - * CegConjecturePbe::constructSolution, which implements unification-based - * approaches for construction solutions to synthesis conjectures. - */ - class UnifContext - { - public: - UnifContext(); - /** 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(); - /** 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; - - private: - /** true and false nodes */ - Node d_true; - Node d_false; - }; - - /** 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 - - /** 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 for these - * children 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) } - * where * is application of substitution. - */ - 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; - /** Returns true if argument is valid strategy in context x */ - bool isValid(CegConjecturePbe* pbe, UnifContext& x); - }; }; }/* namespace CVC4::theory::quantifiers */ |