diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index d71139eef..fc26d72f6 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -600,10 +600,20 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, } // register the enumerator si.d_enums[index].push_back(e); + bool mkActiveGuard = false; + bool isVarAgnostic = false; + // if we are using a single independent enumerator for conditions, then we + // allocate an active guard, and are eligible to use variable-agnostic + // enumeration. + if (options::sygusUnifCondIndependent() && index == 1) + { + mkActiveGuard = true; + isVarAgnostic = options::sygusEnumVarAgnostic(); + } Trace("cegis-unif-enum") << "* Registering new enumerator " << e << " to strategy point " << si.d_pt << "\n"; d_tds->registerEnumerator( - e, si.d_pt, d_parent, options::sygusUnifCondIndependent() && index == 1); + e, si.d_pt, d_parent, mkActiveGuard, false, isVarAgnostic); } void CegisUnifEnumDecisionStrategy::registerEvalPts( |