diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 29 |
1 files changed, 4 insertions, 25 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 9367444ac..dbde79aae 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -86,7 +86,6 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates, // Non-unif candidate are themselves the enumerators enums.insert( enums.end(), d_non_unif_candidates.begin(), d_non_unif_candidates.end()); - Valuation& valuation = d_qe->getValuation(); for (const Node& c : d_unif_candidates) { // Collect heads of candidates @@ -104,19 +103,6 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates, std::vector<Node> uenums; // get the current unification enumerators d_u_enum_manager.getEnumeratorsForStrategyPt(e, uenums, index); - if (index == 1 && options::sygusUnifCondIndependent()) - { - Assert(uenums.size() == 1); - Node eu = uenums[0]; - Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); - // If active guard for this enumerator is not true, there are no more - // values for it, and hence we ignore it - Node gstatus = valuation.getSatValue(g); - if (gstatus.isNull() || !gstatus.getConst<bool>()) - { - continue; - } - } // get the model value of each enumerator enums.insert(enums.end(), uenums.begin(), uenums.end()); } @@ -264,7 +250,7 @@ void CegisUnif::setConditions( Assert(!itv->second.empty()); if (d_tds->isPassiveEnumerator(eu)) { - Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); + Node g = d_tds->getActiveGuardForEnumerator(eu); Node exp_exc = d_tds->getExplain() ->getExplanationForEquality(eu, itv->second[0]) .negate(); @@ -563,7 +549,6 @@ void CegisUnifEnumDecisionStrategy::initialize( { Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type); setUpEnumerator(ceu, ci.second, 1); - d_enum_to_active_guard[ceu] = d_tds->getActiveGuardForEnumerator(ceu); } } } @@ -592,12 +577,6 @@ void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt( } } -Node CegisUnifEnumDecisionStrategy::getActiveGuardForEnumerator(Node e) -{ - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - return d_enum_to_active_guard[e]; -} - void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index) @@ -628,19 +607,19 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, // register the enumerator si.d_enums[index].push_back(e); bool mkActiveGuard = false; - bool isVarAgnostic = false; + bool isActiveGen = 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(); + isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; } Trace("cegis-unif-enum") << "* Registering new enumerator " << e << " to strategy point " << si.d_pt << "\n"; d_tds->registerEnumerator( - e, si.d_pt, d_parent, mkActiveGuard, false, isVarAgnostic); + e, si.d_pt, d_parent, mkActiveGuard, false, isActiveGen); } void CegisUnifEnumDecisionStrategy::registerEvalPts( |