diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-09 16:54:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-09 16:54:58 -0500 |
commit | 9168f325706e61bb12fec71cd375647e2102f8d3 (patch) | |
tree | aa5129a48322e43ae0f5faa9ade2decbd7091df0 /src/theory/quantifiers/sygus/sygus_pbe.cpp | |
parent | 90ffa8b4eb26af9060e57be7fe5d6008717d3ce6 (diff) |
Support for basic actively-generated enumerators (#2606)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 26 |
1 files changed, 5 insertions, 21 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 8050e97f8..ac8b56ee4 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -179,7 +179,7 @@ bool SygusPbe::initialize(Node n, return false; } } - bool isVarAgnostic = options::sygusEnumVarAgnostic(); + bool isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; for (const Node& c : candidates) { Assert(d_examples.find(c) != d_examples.end()); @@ -203,9 +203,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, isVarAgnostic); - Node g = d_tds->getActiveGuardForEnumerator(e); - d_enum_to_active_guard[e] = g; + d_tds->registerEnumerator(e, c, d_parent, true, false, isActiveGen); d_enum_to_candidate[e] = c; TNode te = e; // initialize static symmetry breaking lemmas for it @@ -397,27 +395,13 @@ Node SygusPbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i) void SygusPbe::getTermList(const std::vector<Node>& candidates, std::vector<Node>& terms) { - Valuation& valuation = d_qe->getValuation(); for( unsigned i=0; i<candidates.size(); i++ ){ Node v = candidates[i]; std::map<Node, std::vector<Node> >::iterator it = d_candidate_to_enum.find(v); if (it != d_candidate_to_enum.end()) { - for (unsigned j = 0; j < it->second.size(); j++) - { - Node e = it->second[j]; - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - Node g = d_enum_to_active_guard[e]; - // Get whether the active guard for this enumerator is true, - // if so, then there may exist more values for it, and hence we add it - // to terms. - Node gstatus = valuation.getSatValue(g); - if (!gstatus.isNull() && gstatus.getConst<bool>()) - { - terms.push_back(e); - } - } + terms.insert(terms.end(), it->second.begin(), it->second.end()); } } } @@ -491,8 +475,8 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, if (!enum_lems.empty()) { // the lemmas must be guarded by the active guard of the enumerator - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - Node g = d_enum_to_active_guard[e]; + Node g = d_tds->getActiveGuardForEnumerator(e); + Assert(!g.isNull()); for (unsigned j = 0, size = enum_lems.size(); j < size; j++) { enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); |