diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-04 18:06:29 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-04 16:06:29 -0800 |
commit | f0d1016c0c9b5335a4c2f564ac1a115fe0a74329 (patch) | |
tree | 8d2f50f303584aee5cf51423ac91830bde0eca9c /src/theory/quantifiers/sygus/synth_conjecture.cpp | |
parent | c5d84115b1e54411a5816002d4615408e72a57fb (diff) |
Implement option to turn off symmetry breaking for basic enumerators (#2686)
Improves the existing implementation for sygus-active-gen=basic.
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 21079aedc..e668b2206 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -705,17 +705,17 @@ class EnumValGeneratorBasic : public EnumValGenerator } Node next = *d_te; ++d_te; - Node nextb = d_tds->sygusToBuiltin(next); if (options::sygusSymBreakDynamic()) { + Node nextb = d_tds->sygusToBuiltin(next); nextb = d_tds->getExtRewriter()->extendedRewrite(nextb); - } - if (d_cache.find(nextb) == d_cache.end()) - { + if (d_cache.find(nextb) != d_cache.end()) + { + return getNext(); + } d_cache.insert(nextb); - return next; } - return getNext(); + return next; } private: |