diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-16 18:22:35 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-16 18:22:35 -0500 |
commit | 13e248f4087347721c731c1f21a6f8b66dc52ed1 (patch) | |
tree | 496583cbb77635a9ef90780f6aaeb6a32c6d3bb7 /src/theory/quantifiers/sygus/sygus_unif.h | |
parent | e2b8d90e1ea596a960de9ddb75094e7f6d7856e8 (diff) |
Improve the separation resolution scheme in cegis unif (#1931)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.h')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 1c7972978..a19f8e41b 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -80,8 +80,12 @@ class SygusUnif * based on the current set of enumerated values. Returns null if it cannot * for some function (for example, if the set of enumerated values is * insufficient, or if a non-deterministic strategy aborts). + * + * This call may add lemmas to lemmas that should be sent out on an output + * channel by the caller. */ - virtual bool constructSolution(std::vector<Node>& sols); + virtual bool constructSolution(std::vector<Node>& sols, + std::vector<Node>& lemmas); protected: /** reference to quantifier engine */ @@ -150,7 +154,8 @@ class SygusUnif * * ind is the term depth of the context (for debugging). */ - virtual Node constructSol(Node f, Node e, NodeRole nrole, int ind) = 0; + 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); |