diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-28 15:49:56 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-28 15:49:56 -0600 |
| commit | 64624a5ff72c132b87b885780ad9c39f06e3cdbc (patch) | |
| tree | d26f9e217f3f681bf2966e4f9fae89c9f9b0338e /src/theory/quantifiers/sygus/sygus_unif.h | |
| parent | c92e6e49040b3ca4c33fbedb8e2a30ac3318fb8d (diff) | |
Information gain heuristic for PBE (#2719)
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 |