diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-02 14:44:04 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-02 14:44:04 -0600 |
commit | c8d0db7ee9c48fadd19227d472f60ff0089c34da (patch) | |
tree | ad8b35763f65e53f96cb9574f3392fd870c0c1e0 /src/theory/quantifiers/sygus/cegis.cpp | |
parent | 356319744514261f06afced5ee975d49abe83eb4 (diff) |
Simplify sygus wrt miniscoping (#1634)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index a571c85fb..b778b90be 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -150,9 +150,19 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, return true; } -void Cegis::registerRefinementLemma(Node lem) +void Cegis::registerRefinementLemma(const std::vector<Node>& vars, + Node lem, + std::vector<Node>& lems) { d_refinement_lemmas.push_back(lem); + // Make the refinement lemma and add it to lems. + // This lemma is guarded by the parent's guard, which has the semantics + // "this conjecture has a solution", hence this lemma states: + // if the parent conjecture has a solution, it satisfies the specification + // for the given concrete point. + Node rlem = + NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem); + lems.push_back(rlem); } void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, |