diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-29 10:29:02 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-29 10:29:02 -0500 |
commit | 48767f17e63ea1df001d670429e89d64214ffe11 (patch) | |
tree | 449e2828a47ef24d95f255c83e3879a6c750209e /src/theory/quantifiers/sygus/sygus_unif.h | |
parent | 0baee856785df0f018fa2a007f62299c45fd8e5d (diff) |
Simplify sygus unif so that it is one-to-one with functions to synthesize (#1726)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.h')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 50 |
1 files changed, 26 insertions, 24 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index d46fb9c86..518a730a5 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -101,8 +101,11 @@ class UnifContext { public: UnifContext(); - /** this intiializes this context for function-to-synthesize c */ - void initialize(SygusUnif* pbe, Node c); + /** + * This intiializes this context based on information in pbe regarding the + * kinds of examples it contains. + */ + void initialize(SygusUnif* pbe); //----------for ITE strategy /** the value of the context conditional @@ -408,9 +411,9 @@ class SygusUnif Node d_true; Node d_false; /** input of I/O examples */ - std::map<Node, std::vector<std::vector<Node> > > d_examples; + std::vector<std::vector<Node> > d_examples; /** output of I/O examples */ - std::map<Node, std::vector<Node> > d_examples_out; + std::vector<Node> d_examples_out; //------------------------------ representation of a enumeration strategy /** @@ -582,7 +585,7 @@ class SygusUnif /** the candidate for this class */ Node d_candidate; /** maps a function-to-synthesize to the above information */ - std::map<Node, CandidateInfo> d_cinfo; + CandidateInfo d_cinfo; //------------------------------ representation of an enumeration strategy /** domain-specific enumerator exclusion techniques @@ -590,14 +593,12 @@ class SygusUnif * 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, + * 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 c, - Node x, + bool getExplanationForEnumeratorExclude(Node x, Node v, std::vector<Node>& results, EnumInfo& ei, @@ -622,21 +623,23 @@ class SygusUnif /** 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. + * role of nrole, for solutions to function-to-synthesize of this class. */ - void collectEnumeratorTypes(Node c, TypeNode tn, NodeRole nrole); + void collectEnumeratorTypes(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. + * 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, Node c, TypeNode tn, EnumRole enum_role, bool inSearch); + void registerEnumerator(Node et, + TypeNode tn, + EnumRole enum_role, + bool inSearch); /** infer template */ bool inferTemplate(unsigned k, Node n, @@ -645,9 +648,10 @@ class SygusUnif /** 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. + * strategy for the function-to-synthesize of this class, and stores these + * into lemmas. */ - void staticLearnRedundantOps(Node c, std::vector<Node>& 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 @@ -662,7 +666,6 @@ class SygusUnif * conditional of an strat_ITE strategy). */ void staticLearnRedundantOps( - Node c, Node e, NodeRole nrole, std::map<Node, std::map<NodeRole, bool> >& visited, @@ -673,13 +676,12 @@ class SygusUnif /** helper function for construct solution. * - * Construct a solution based on enumerator e for function-to-synthesize c - * with node role nrole in context x. + * Construct a solution based on enumerator e for function-to-synthesize of + * this class 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); + Node constructSolution(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); @@ -712,9 +714,9 @@ class SygusUnif * 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( d_cenum[1], ... ) = t1, * ..., - * constructSolution( c, d_cenum[n], ... ) = tn, + * 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. |