diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-12 15:43:36 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-12 15:43:36 -0600 |
| commit | 87602bc6d010eea33b8db93e80a79dcf99d230b5 (patch) | |
| tree | ba87d683d8cdb51097be211e6c51ec59a7c8658e /src/theory/quantifiers/sygus/cegis.cpp | |
| parent | e8064b85ded3b5508a0b7063737dee2fc8834105 (diff) | |
Make CEGIS sampling robust to non-vanilla CEGIS (#3559)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 7a9a9ca21..a4dc241b8 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -309,8 +309,9 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, { // if we didn't add a lemma, trying sampling to add a refinement lemma // that immediately refutes the candidate we just constructed - if (sampleAddRefinementLemma(enums, enum_values, lems)) + if (sampleAddRefinementLemma(candidates, candidate_values, lems)) { + candidate_values.clear(); // restart (should be guaranteed to add evaluation lemmas on this call) return constructCandidates( enums, enum_values, candidates, candidate_values, lems); |