diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-21 14:09:12 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-21 22:09:12 +0300 |
commit | caf65a13994dc1d39cc31a8cea76c6a7fddb338c (patch) | |
tree | 2c52e2a6b9a06be048d111d267923778d9789c39 /src/theory/quantifiers/sygus/cegis.cpp | |
parent | c975ef8d15438e151f94a0a7f3d1adb6ac7918dc (diff) |
Refactor sygus eval unfold (#1946)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index ec17294f9..fc41c7561 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -28,7 +28,14 @@ namespace CVC4 { namespace theory { namespace quantifiers { -Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) {} +Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) + : SygusModule(qe, p), d_eval_unfold(nullptr) +{ + if (options::sygusEvalUnfold()) + { + d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold(); + } +} bool Cegis::initialize(Node n, const std::vector<Node>& candidates, @@ -100,7 +107,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, add the lemmas below as well, in parallel. */ } } - if (options::sygusEvalUnfold()) + if (d_eval_unfold != nullptr) { Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl; std::vector<Node> eager_terms, eager_vals, eager_exps; @@ -108,11 +115,11 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, { Trace("cegqi-debug") << " register " << candidates[i] << " -> " << candidate_values[i] << std::endl; - d_tds->registerModelValue(candidates[i], - candidate_values[i], - eager_terms, - eager_vals, - eager_exps); + d_eval_unfold->registerModelValue(candidates[i], + candidate_values[i], + eager_terms, + eager_vals, + eager_exps); } Trace("cegqi-debug") << "...produced " << eager_terms.size() << " evaluation unfold lemmas.\n"; |