diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-31 16:25:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-31 16:25:37 -0500 |
| commit | f59097bfc7f89a30b2d857b0b43eb9130e85f45e (patch) | |
| tree | d71d10bb69f23c99e607b897a9a691ab49ade9fa /src/theory/quantifiers/sygus/sygus_pbe.cpp | |
| parent | 6a89ff6d106a012442f0ab3b212dc3d26a758da3 (diff) | |
Add optimized sygus enumeration (#2677)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index ac8b56ee4..b49c29c53 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -356,10 +356,10 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr) { Assert(isPbe()); Assert(!e.isNull()); - if (!d_tds->isPassiveEnumerator(e)) + if (d_tds->isVariableAgnosticEnumerator(e)) { - // we cannot apply conjecture-specific symmetry breaking on enumerators that - // are not passive + // we cannot apply conjecture-specific symmetry breaking on variable + // agnostic enumerators return Node::null(); } Node ee = d_tds->getSynthFunForEnumerator(e); |