diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-02 17:50:31 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-02 17:50:31 -0500 |
commit | bc6cb232c11d65f763844c2c9274444446aee26e (patch) | |
tree | 141c067f887de219d8127a419ea2dd6b0958018d /src/theory/quantifiers/sygus/sygus_unif.h | |
parent | 065adbb66136022236efb73af740ff6b2c0f178a (diff) |
Make sygus unif utility use sygus unif strategies (#1732)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.h')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 247 |
1 files changed, 26 insertions, 221 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 9bb321a09..4e7806bf0 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -265,11 +265,11 @@ class SubsumeTrie * * This class maintains: * (1) A "strategy tree" based on the syntactic restrictions for f that is - * constructed during initialize, + * constructed during initialize (d_strategy), * (2) A set of input/output examples that are the specification for f. This * can be updated via calls to resetExmaples/addExamples, - * (3) A set of terms that have been enumerated for enumerators. This can be - * updated via calls to notifyEnumeration. + * (3) A set of terms that have been enumerated for enumerators (d_ecache). This + * can be updated via calls to notifyEnumeration. * * Based on the above, solutions can be constructed via calls to * constructSolution. @@ -353,72 +353,25 @@ class SygusUnif bool pol = true); //-----------------------end debug printing - //------------------------------ 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. + * a database of values that have been enumerated for this enumerator. */ - class EnumInfo + class EnumCache { 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(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; } - /** 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; - /** - * 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 + EnumCache() {} /** * 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(SygusUnif* pbe, Node v, std::vector<Node>& results); + void addEnumValue(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); + void setSolved(Node slv) { d_enum_solved = 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. */ @@ -444,174 +397,61 @@ class SygusUnif * 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; + std::map<Node, EnumCache> d_ecache; - 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 + /** + * Whether we will try to construct solution on the next call to + * constructSolution. This flag is set to true when we successfully + * register a new value for an enumerator. */ - 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 d_check_sol; + /** The number of values we have enumerated for all enumerators. */ + unsigned d_cond_count; + /** The solution for the function of this class, if one has been found */ + Node d_solution; /** the candidate for this class */ Node d_candidate; /** maps a function-to-synthesize to the above information */ - CandidateInfo d_cinfo; + SygusUnifStrategy d_strategy; - //------------------------------ representation of an enumeration strategy /** domain-specific enumerator exclusion techniques * - * Returns true if the value v for x can be excluded based on a + * Returns true if the value v for e can be excluded based on a * domain-specific exclusion technique like the ones below. * * results : the values of v under the input examples, - * 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 x, + bool getExplanationForEnumeratorExclude(Node e, 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 + /** returns true if we can exlude values of e based on negative str.contains * - * Values v for x may be excluded if we realize that the value of v under the + * Values v for e 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 + * This function depends on whether e 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); + bool useStrContainsEnumeratorExclude(Node e); /** 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 of this class. - */ - void collectEnumeratorTypes(TypeNode tn, NodeRole nrole); - /** register enumerator - * - * This registers that et is an enumerator 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, - 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 of this class, and stores these - * into lemmas. - */ - void staticLearnRedundantOps(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 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 /** helper function for construct solution. * * Construct a solution based on enumerator e for function-to-synthesize of @@ -644,41 +484,6 @@ class SygusUnif 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( d_cenum[1], ... ) = t1, - * ..., - * constructSolution( 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(SygusUnif* pbe, UnifContext& x); - }; }; } /* CVC4::theory::quantifiers namespace */ |