diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.h')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 614a29d1c..67e798854 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -156,18 +156,20 @@ class SygusUnif */ virtual Node constructSol( Node f, Node e, NodeRole nrole, int ind, std::vector<Node>& lemmas) = 0; - /** Heuristically choose the best solved term from solved in context x, - * currently return the first. */ - virtual Node constructBestSolvedTerm(const std::vector<Node>& solved); - /** Heuristically choose the best solved string term from solved in context - * x, currently return the first. */ - virtual Node constructBestStringSolvedTerm(const std::vector<Node>& solved); - /** Heuristically choose the best solved conditional term from solved in - * context x, currently random */ - virtual Node constructBestSolvedConditional(const std::vector<Node>& solved); - /** Heuristically choose the best conditional term from conds in context x, - * currently random */ - virtual Node constructBestConditional(const std::vector<Node>& conds); + /** + * Heuristically choose the best solved term for enumerator e, + * currently return the first by default. A solved term is one that + * suffices to form part of the solution for the given context. For example, + * x is a solved term in the context "ite(x>0, _, 0)" for PBE problem + * with I/O pairs { 1 -> 1, 4 -> 4, -1 -> 0 }. + */ + virtual Node constructBestSolvedTerm(Node e, const std::vector<Node>& solved); + /** + * Heuristically choose the best conditional term from conds for condition + * enumerator ce, random by default. + */ + virtual Node constructBestConditional(Node ce, + const std::vector<Node>& conds); /** 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 |