diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.h | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 00cc5af72..c32a1390c 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -90,6 +90,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf void registerEvalPts(const std::vector<Node>& eis, Node e); /** Retrieves active guard for enumerator */ Node getActiveGuardForEnumerator(Node e); + private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; @@ -223,7 +224,7 @@ class CegisUnif : public Cegis * example would actually correspond to * eval(d, 0) != c1 v eval(d, c1) != c2 v eval(d, c2) > 1 * in which d is the deep embedding of the function-to-synthesize f - */ + */ void registerRefinementLemma(const std::vector<Node>& vars, Node lem, std::vector<Node>& lems) override; @@ -261,6 +262,35 @@ class CegisUnif : public Cegis std::vector<Node>& candidate_values, bool satisfiedRl, std::vector<Node>& lems) override; + /** communicate condition values to solution building utility + * + * for each unification candidate and for each strategy point associated with + * it, set in d_sygus_unif the condition values (unif_cvalues) for respective + * condition enumerators (unif_cenums) + */ + void setConditions(const std::map<Node, std::vector<Node>>& unif_cenums, + const std::map<Node, std::vector<Node>>& unif_cvalues, + std::vector<Node>& lems); + /** set values of condition enumerators based on current enumerator assignment + * + * enums and enum_values are the enumerators registered in getTermList and + * their values retrieved by the parent SynthConjecture module, respectively. + * + * unif_cenums and unif_cvalues associate the conditional enumerators of each + * strategy point of each unification candidate with their respective model + * values + * + * This function also generates inter-enumerator symmetry breaking for return + * values, such that their model values are ordered by size + * + * returns true if no symmetry breaking lemmas were generated for the return + * value enumerators, false otherwise + */ + bool getEnumValues(const std::vector<Node>& enums, + const std::vector<Node>& enum_values, + std::map<Node, std::vector<Node>>& unif_cenums, + std::map<Node, std::vector<Node>>& unif_cvalues, + std::vector<Node>& lems); /** * Sygus unif utility. This class implements the core algorithm (e.g. decision * tree learning) that this module relies upon. |