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/sygus_pbe.cpp | |
| parent | cc5ea0ed533e081ecccca57cf1c4efb63296f995 (diff) | |
Change default sygus enumeration mode to auto (#2689)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index b49c29c53..f91dd5d30 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -179,7 +179,6 @@ bool SygusPbe::initialize(Node n, return false; } } - bool isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; for (const Node& c : candidates) { Assert(d_examples.find(c) != d_examples.end()); @@ -203,7 +202,7 @@ bool SygusPbe::initialize(Node n, for (const Node& e : d_candidate_to_enum[c]) { TypeNode etn = e.getType(); - d_tds->registerEnumerator(e, c, d_parent, true, false, isActiveGen); + d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL, false); d_enum_to_candidate[e] = c; TNode te = e; // initialize static symmetry breaking lemmas for it |