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/cegis_unif.cpp | |
parent | cc5ea0ed533e081ecccca57cf1c4efb63296f995 (diff) |
Change default sygus enumeration mode to auto (#2689)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index dbde79aae..18e313bf0 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -44,7 +44,12 @@ bool CegisUnif::processInitialize(Node n, std::map<Node, Node> pt_to_cond; // strategy lemmas for each strategy point std::map<Node, std::vector<Node>> strategy_lemmas; - // Initialize strategies for all functions-to-synhesize + // Initialize strategies for all functions-to-synthesize + // The role of non-unification enumerators is to be either the single solution + // or part of a solution involving multiple enumerators. + EnumeratorRole eroleNonUnif = candidates.size() == 1 + ? ROLE_ENUM_SINGLE_SOLUTION + : ROLE_ENUM_MULTI_SOLUTION; for (const Node& f : candidates) { // Init UNIF util for this candidate @@ -53,7 +58,7 @@ bool CegisUnif::processInitialize(Node n, if (!d_sygus_unif.usingUnif(f)) { Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl; - d_tds->registerEnumerator(f, f, d_parent); + d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif); d_non_unif_candidates.push_back(f); } else @@ -462,7 +467,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) exclude_cons, term_irrelevant); d_virtual_enum = nm->mkSkolem("_ve", vtn); - d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent); + d_tds->registerEnumerator( + d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED); } // if new_size is a power of two, then isPow2 returns log2(new_size)+1 // otherwise, this returns 0. In the case it returns 0, we don't care @@ -606,20 +612,17 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, } // register the enumerator si.d_enums[index].push_back(e); - bool mkActiveGuard = false; - bool isActiveGen = false; + EnumeratorRole erole = ROLE_ENUM_CONSTRAINED; // 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; - isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE; + erole = ROLE_ENUM_POOL; } 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, isActiveGen); + d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, false); } void CegisUnifEnumDecisionStrategy::registerEvalPts( |