diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-05 16:50:48 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-05 16:50:48 -0600 |
commit | 2ef5f132c1169cbeadd580638cbc35b6e454d6a5 (patch) | |
tree | e52fe812aafe511293e345c494f4a389eec0f855 /src/theory/quantifiers/sygus/synth_conjecture.cpp | |
parent | cc5ea0ed533e081ecccca57cf1c4efb63296f995 (diff) |
Change default sygus enumeration mode to auto (#2689)
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 03344d2e7..2bfde2d80 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -703,13 +703,13 @@ class EnumValGeneratorBasic : public EnumValGenerator */ bool increment() override { + ++d_te; if (d_te.isFinished()) { d_currTerm = Node::null(); return false; } d_currTerm = *d_te; - ++d_te; if (options::sygusSymBreakDynamic()) { Node nextb = d_tds->sygusToBuiltin(d_currTerm); @@ -773,15 +773,18 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) else { // Actively-generated enumerators are currently either variable agnostic - // or basic. + // or basic. The auto mode always prefers the optimized enumerator over + // the basic one. Assert(d_tds->isBasicEnumerator(e)); - if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM) + if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM_BASIC) { - d_evg[e].reset(new SygusEnumerator(d_tds, this)); + d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); } else { - d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); + Assert(options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM + || options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO); + d_evg[e].reset(new SygusEnumerator(d_tds, this)); } } Trace("sygus-active-gen") |