diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index a4dc241b8..78ea5b22f 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -52,7 +52,7 @@ bool Cegis::initialize(Node conj, } // assign the cegis sampler if applicable - if (options::cegisSample() != CEGIS_SAMPLE_NONE) + if (options::cegisSample() != options::CegisSampleMode::NONE) { Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..." << std::endl; @@ -81,7 +81,8 @@ bool Cegis::processInitialize(Node conj, // grammar construction was not simple. bool useSymCons = false; if (options::sygusRepairConst() - || options::sygusGrammarConsMode() != SYGUS_GCONS_SIMPLE) + || options::sygusGrammarConsMode() + != options::SygusGrammarConsMode::SIMPLE) { TypeNode ctn = candidates[i].getType(); d_tds->registerSygusType(ctn); @@ -305,7 +306,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, return false; } - if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty()) + if (options::cegisSample() != options::CegisSampleMode::NONE && lems.empty()) { // if we didn't add a lemma, trying sampling to add a refinement lemma // that immediately refutes the candidate we just constructed @@ -636,7 +637,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, Trace("cegqi-engine") << " *** Refine by sampling" << std::endl; addRefinementLemma(rlem); // if trust, we are not interested in sending out refinement lemmas - if (options::cegisSample() != CEGIS_SAMPLE_TRUST) + if (options::cegisSample() != options::CegisSampleMode::TRUST) { Node lem = nm->mkNode(OR, d_parent->getGuard().negate(), rlem); lems.push_back(lem); |