diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 7601e2117..453ac5c18 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -30,11 +30,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusPbe::SygusPbe(QuantifiersState& qs, +SygusPbe::SygusPbe(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qs, qim, tds, p) + : SygusModule(env, qs, qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -131,7 +132,7 @@ bool SygusPbe::initialize(Node conj, // Apply extended rewriting on the lemma. This helps utilities like // SygusEnumerator more easily recognize the shape of this lemma, e.g. // ( ~is-ite(x) or ( ~is-ite(x) ^ P ) ) --> ~is-ite(x). - lem = d_tds->getExtRewriter()->extendedRewrite(lem); + lem = extendedRewrite(lem); Trace("sygus-pbe") << " static redundant op lemma : " << lem << std::endl; // Register as a symmetry breaking lemma with the term database. |