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.cpp | |
parent | cc5ea0ed533e081ecccca57cf1c4efb63296f995 (diff) |
Change default sygus enumeration mode to auto (#2689)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 24 |
1 files changed, 6 insertions, 18 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 79bec60ee..6aca71ca3 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -69,17 +69,10 @@ bool Cegis::processInitialize(Node n, { Trace("cegis") << "Initialize cegis..." << std::endl; unsigned csize = candidates.size(); - // We only can use actively-generated enumerators if there is only one - // function-to-synthesize. Otherwise, we would have to generate a "product" of - // two actively-generated enumerators. That is, given a conjecture with two - // functions-to-synthesize with enumerators e_f and e_g, if: - // e_f -> t1, ..., tn - // e_g -> s1, ..., sm - // This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj) - // for each i,j. We do not do this and revert to the default behavior of - // this module instead. - bool isActiveGen = - options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1; + // The role of enumerators is to be either the single solution or part of + // a solution involving multiple enumerators. + EnumeratorRole erole = + csize == 1 ? ROLE_ENUM_SINGLE_SOLUTION : ROLE_ENUM_MULTI_SOLUTION; // initialize an enumerator for each candidate for (unsigned i = 0; i < csize; i++) { @@ -98,13 +91,8 @@ bool Cegis::processInitialize(Node n, } } Trace("cegis") << std::endl; - // variable agnostic enumerators require an active guard - d_tds->registerEnumerator(candidates[i], - candidates[i], - d_parent, - isActiveGen, - do_repair_const, - isActiveGen); + d_tds->registerEnumerator( + candidates[i], candidates[i], d_parent, erole, do_repair_const); } return true; } |