From 96ac1d2a5d1f25eaa1b0b265bb21d1a8b3c3d872 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 29 Mar 2021 14:40:53 -0500 Subject: [PATCH] Eliminate the use of quantifiers engine in sygus solver (#6232) --- .../candidate_rewrite_database.cpp | 10 ++---- .../quantifiers/candidate_rewrite_database.h | 7 ++-- .../quantifiers/cegqi/ceg_instantiator.cpp | 24 ++++++-------- .../quantifiers/cegqi/ceg_instantiator.h | 16 +++------- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 +- src/theory/quantifiers/expr_miner_manager.cpp | 12 +++---- src/theory/quantifiers/expr_miner_manager.h | 6 ++-- .../sygus/ce_guided_single_inv.cpp | 17 +++++----- .../quantifiers/sygus/ce_guided_single_inv.h | 6 ++-- src/theory/quantifiers/sygus/cegis.cpp | 9 +++--- src/theory/quantifiers/sygus/cegis.h | 4 +-- .../sygus/cegis_core_connective.cpp | 6 ++-- .../quantifiers/sygus/cegis_core_connective.h | 4 +-- src/theory/quantifiers/sygus/cegis_unif.cpp | 13 ++++---- src/theory/quantifiers/sygus/cegis_unif.h | 10 +++--- src/theory/quantifiers/sygus/sygus_module.cpp | 6 ++-- src/theory/quantifiers/sygus/sygus_module.h | 9 ++---- src/theory/quantifiers/sygus/sygus_pbe.cpp | 8 ++--- src/theory/quantifiers/sygus/sygus_pbe.h | 4 +-- .../quantifiers/sygus/sygus_process_conj.cpp | 2 +- .../quantifiers/sygus/sygus_process_conj.h | 2 +- .../quantifiers/sygus/sygus_repair_const.cpp | 8 ++--- .../quantifiers/sygus/sygus_repair_const.h | 7 +--- src/theory/quantifiers/sygus/sygus_unif.cpp | 12 +++---- src/theory/quantifiers/sygus/sygus_unif.h | 11 ++----- .../quantifiers/sygus/sygus_unif_io.cpp | 5 ++- src/theory/quantifiers/sygus/sygus_unif_io.h | 2 +- .../quantifiers/sygus/sygus_unif_rl.cpp | 4 +-- src/theory/quantifiers/sygus/sygus_unif_rl.h | 2 +- .../quantifiers/sygus/sygus_unif_strat.cpp | 7 ++-- .../quantifiers/sygus/sygus_unif_strat.h | 13 ++++---- .../quantifiers/sygus/synth_conjecture.cpp | 32 +++++++++---------- .../quantifiers/sygus/synth_conjecture.h | 8 ++--- src/theory/quantifiers/sygus/synth_engine.cpp | 12 +++---- src/theory/quantifiers/sygus/synth_engine.h | 2 -- 35 files changed, 122 insertions(+), 180 deletions(-) diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 103b32be0..a0b9b20f4 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -21,7 +21,6 @@ #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" using namespace std; @@ -36,8 +35,7 @@ CandidateRewriteDatabase::CandidateRewriteDatabase(bool doCheck, bool rewAccel, bool silent, bool filterPairs) - : d_qe(nullptr), - d_tds(nullptr), + : d_tds(nullptr), d_ext_rewrite(nullptr), d_doCheck(doCheck), d_rewAccel(rewAccel), @@ -52,7 +50,6 @@ void CandidateRewriteDatabase::initialize(const std::vector& vars, Assert(ss != nullptr); d_candidate = Node::null(); d_using_sygus = false; - d_qe = nullptr; d_tds = nullptr; d_ext_rewrite = nullptr; if (d_filterPairs) @@ -63,15 +60,14 @@ void CandidateRewriteDatabase::initialize(const std::vector& vars, } void CandidateRewriteDatabase::initializeSygus(const std::vector& vars, - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, SygusSampler* ss) { Assert(ss != nullptr); d_candidate = f; d_using_sygus = true; - d_qe = qe; - d_tds = d_qe->getTermDatabaseSygus(); + d_tds = tds; d_ext_rewrite = nullptr; if (d_filterPairs) { diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 3313b507b..321880dc0 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -64,15 +64,14 @@ class CandidateRewriteDatabase : public ExprMiner * Serves the same purpose as the above function, but we will be using * sygus to enumerate terms and generate samples. * - * qe : pointer to quantifiers engine. We use the sygus term database of this - * quantifiers engine, and the extended rewriter of the corresponding term + * tds : pointer to sygus term database. We use the extended rewriter of this * database when computing candidate rewrites, * f : a term of some SyGuS datatype type whose values we will be * testing under the free variables in the grammar of f. This is the * "candidate variable" CegConjecture::d_candidates. */ void initializeSygus(const std::vector& vars, - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, SygusSampler* ss); /** add term @@ -102,8 +101,6 @@ class CandidateRewriteDatabase : public ExprMiner void setExtendedRewriter(ExtendedRewriter* er); private: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; /** (required) pointer to the sygus term database of d_qe */ TermDbSygus* d_tds; /** an extended rewriter object */ diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index ca9599ba3..fd6a087ca 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -315,16 +315,14 @@ CegHandledStatus CegInstantiator::isCbqiTerm(Node n) return ret; } -CegHandledStatus CegInstantiator::isCbqiSort(TypeNode tn, QuantifiersEngine* qe) +CegHandledStatus CegInstantiator::isCbqiSort(TypeNode tn) { std::map visited; - return isCbqiSort(tn, visited, qe); + return isCbqiSort(tn, visited); } CegHandledStatus CegInstantiator::isCbqiSort( - TypeNode tn, - std::map& visited, - QuantifiersEngine* qe) + TypeNode tn, std::map& visited) { std::map::iterator itv = visited.find(tn); if (itv != visited.end()) @@ -360,7 +358,7 @@ CegHandledStatus CegInstantiator::isCbqiSort( } for (const TypeNode& crange : consType) { - CegHandledStatus cret = isCbqiSort(crange, visited, qe); + CegHandledStatus cret = isCbqiSort(crange, visited); if (cret == CEG_UNHANDLED) { Trace("cegqi-debug2") @@ -380,14 +378,13 @@ CegHandledStatus CegInstantiator::isCbqiSort( return ret; } -CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q, - QuantifiersEngine* qe) +CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q) { CegHandledStatus hmin = CEG_HANDLED_UNCONDITIONAL; for (const Node& v : q[0]) { TypeNode tn = v.getType(); - CegHandledStatus handled = isCbqiSort(tn, qe); + CegHandledStatus handled = isCbqiSort(tn); if (handled == CEG_UNHANDLED) { return CEG_UNHANDLED; @@ -400,7 +397,7 @@ CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q, return hmin; } -CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe) +CegHandledStatus CegInstantiator::isCbqiQuant(Node q) { Assert(q.getKind() == FORALL); // compute attributes @@ -428,8 +425,7 @@ CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe) } CegHandledStatus ret = CEG_HANDLED; // if quantifier has a non-handled variable, then do not use cbqi - // if quantifier has an APPLY_UF term, then do not use cbqi unless EPR - CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q, qe); + CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q); Trace("cegqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv << std::endl; if (ncbqiv == CEG_UNHANDLED) @@ -668,7 +664,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, TypeNode pvtn = pv.getType(); TypeNode pvtnb = pvtn.getBaseType(); Node pvr = pv; - eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine(); + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); if (ee->hasTerm(pv)) { pvr = ee->getRepresentative(pv); @@ -1321,7 +1317,7 @@ void CegInstantiator::processAssertions() { d_curr_type_eqc.clear(); // must use master equality engine to avoid value instantiations - eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine(); + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); //for each variable for( unsigned i=0; i& visited, - QuantifiersEngine* qe); + TypeNode tn, std::map& visited); //------------------------------------ end static queries }; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 4f66e1034..8318c5f4c 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -410,7 +410,7 @@ bool InstStrategyCegqi::doCbqi(Node q) { std::map::iterator it = d_do_cbqi.find(q); if( it==d_do_cbqi.end() ){ - CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine); + CegHandledStatus ret = CegInstantiator::isCbqiQuant(q); Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; d_do_cbqi[q] = ret; return ret != CEG_UNHANDLED; diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index e482cb05e..6a77d8e45 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -13,7 +13,6 @@ **/ #include "theory/quantifiers/expr_miner_manager.h" -#include "theory/quantifiers_engine.h" #include "options/quantifiers_options.h" @@ -26,7 +25,6 @@ ExpressionMinerManager::ExpressionMinerManager() d_doQueryGen(false), d_doFilterLogicalStrength(false), d_use_sygus_type(false), - d_qe(nullptr), d_tds(nullptr), d_crd(options::sygusRewSynthCheck(), options::sygusRewSynthAccel(), false) { @@ -42,13 +40,12 @@ void ExpressionMinerManager::initialize(const std::vector& vars, d_doFilterLogicalStrength = false; d_sygus_fun = Node::null(); d_use_sygus_type = false; - d_qe = nullptr; d_tds = nullptr; // initialize the sampler d_sampler.initialize(tn, vars, nsamples, unique_type_ids); } -void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe, +void ExpressionMinerManager::initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples, bool useSygusType) @@ -58,8 +55,7 @@ void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe, d_doFilterLogicalStrength = false; d_sygus_fun = f; d_use_sygus_type = useSygusType; - d_qe = qe; - d_tds = qe->getTermDatabaseSygus(); + d_tds = tds; // initialize the sampler d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType); } @@ -77,8 +73,8 @@ void ExpressionMinerManager::enableRewriteRuleSynth() // initialize the candidate rewrite database if (!d_sygus_fun.isNull()) { - Assert(d_qe != nullptr); - d_crd.initializeSygus(vars, d_qe, d_sygus_fun, &d_sampler); + Assert(d_tds != nullptr); + d_crd.initializeSygus(vars, d_tds, d_sygus_fun, &d_sampler); } else { diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index aa6f3cb31..eb2a01fac 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -65,7 +65,7 @@ class ExpressionMinerManager * If useSygusType is false, the terms are the builtin equivalent of these * terms. The argument nsamples is used to initialize the sampler. */ - void initializeSygus(QuantifiersEngine* qe, + void initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples, bool useSygusType); @@ -102,9 +102,7 @@ class ExpressionMinerManager Node d_sygus_fun; /** whether we are using sygus types */ bool d_use_sygus_type; - /** pointer to the quantifiers engine, used if d_use_sygus is true */ - QuantifiersEngine* d_qe; - /** the sygus term database of d_qe */ + /** the sygus term database of the quantifiers engine */ TermDbSygus* d_tds; /** candidate rewrite database */ CandidateRewriteDatabase d_crd; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 066bcd769..c9b2559c1 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -29,7 +29,6 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" @@ -39,12 +38,12 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s) - : d_qe(qe), - d_sip(new SingleInvocationPartition), - d_srcons(new SygusReconstruct(qe->getTermDatabaseSygus(), s)), +CegSingleInv::CegSingleInv(TermRegistry& tr, SygusStatistics& s) + : d_sip(new SingleInvocationPartition), + d_srcons(new SygusReconstruct(tr.getTermDatabaseSygus(), s)), d_isSolved(false), - d_single_invocation(false) + d_single_invocation(false), + d_treg(tr) { } @@ -349,7 +348,7 @@ Node CegSingleInv::getSolutionFromInst(size_t index) ptn = ptn.getRangeType(); } Trace("csi-sol") << "Get solution for (unconstrained) " << prog << std::endl; - s = d_qe->getTermRegistry().getTermEnumeration()->getEnumerateTerm(ptn, 0); + s = d_treg.getTermEnumeration()->getEnumerateTerm(ptn, 0); } else { @@ -395,7 +394,7 @@ Node CegSingleInv::getSolutionFromInst(size_t index) } //simplify the solution using the extended rewriter Trace("csi-sol") << "Solution (pre-simplification): " << s << std::endl; - s = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s); + s = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s); Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl; // wrap into lambda, as needed return SygusUtils::wrapSolutionForSynthFun(prog, s); @@ -462,7 +461,7 @@ Node CegSingleInv::reconstructToSyntax(Node s, { Trace("csi-sol") << "Post-process solution..." << std::endl; Node prev = sol; - sol = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol); + sol = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol); if (prev != sol) { Trace("csi-sol") << "Solution (after post process) : " << sol diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index c73954195..8a2ed3a71 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -50,8 +50,6 @@ class CegSingleInv std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); private: - /** pointer to the quantifiers engine */ - QuantifiersEngine* d_qe; // single invocation inference utility SingleInvocationPartition* d_sip; /** solution reconstruction */ @@ -92,7 +90,7 @@ class CegSingleInv Node d_single_inv; public: - CegSingleInv(QuantifiersEngine* qe, SygusStatistics& s); + CegSingleInv(TermRegistry& tr, SygusStatistics& s); ~CegSingleInv(); // get simplified conjecture @@ -164,6 +162,8 @@ class CegSingleInv * calls to the above method getSolutionFromInst. */ void setSolution(); + /** Reference to the term registry */ + TermRegistry& d_treg; /** The conjecture */ Node d_quant; //-------------- decomposed conjecture diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 56743e264..678ce4ce1 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -31,12 +31,13 @@ namespace CVC4 { namespace theory { namespace quantifiers { -Cegis::Cegis(QuantifiersEngine* qe, - QuantifiersInferenceManager& qim, +Cegis::Cegis(QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qe, qim, p), d_eval_unfold(nullptr), d_usingSymCons(false) + : SygusModule(qim, tds, p), + d_eval_unfold(tds->getEvalUnfold()), + d_usingSymCons(false) { - d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold(); } bool Cegis::initialize(Node conj, diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 0a777a118..9d91a3d66 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -41,9 +41,7 @@ namespace quantifiers { class Cegis : public SygusModule { public: - Cegis(QuantifiersEngine* qe, - QuantifiersInferenceManager& qim, - SynthConjecture* p); + Cegis(QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); ~Cegis() override {} /** initialize */ virtual bool initialize(Node conj, diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 3c6ab6bc1..5211251fa 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -70,10 +70,10 @@ bool VariadicTrie::hasSubset(const std::vector& is) const return false; } -CegisCoreConnective::CegisCoreConnective(QuantifiersEngine* qe, - QuantifiersInferenceManager& qim, +CegisCoreConnective::CegisCoreConnective(QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* p) - : Cegis(qe, qim, p) + : Cegis(qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index d20755e47..5b8be444e 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -159,8 +159,8 @@ class VariadicTrie class CegisCoreConnective : public Cegis { public: - CegisCoreConnective(QuantifiersEngine* qe, - QuantifiersInferenceManager& qim, + CegisCoreConnective(QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* p); ~CegisCoreConnective() {} /** diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index ce7d058c3..0d4907a58 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -29,11 +29,11 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegisUnif::CegisUnif(QuantifiersEngine* qe, - QuantifiersState& qs, +CegisUnif::CegisUnif(QuantifiersState& qs, QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* p) - : Cegis(qe, qim, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, qim, p) + : Cegis(qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p) { } @@ -59,7 +59,7 @@ bool CegisUnif::processInitialize(Node conj, { // Init UNIF util for this candidate d_sygus_unif.initializeCandidate( - d_qe, f, d_cand_to_strat_pt[f], strategy_lemmas); + d_tds, f, d_cand_to_strat_pt[f], strategy_lemmas); if (!d_sygus_unif.usingUnif(f)) { Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl; @@ -401,17 +401,16 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, } CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( - QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* parent) : DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()), - d_qe(qe), d_qim(qim), + d_tds(tds), d_parent(parent) { d_initialized = false; - d_tds = d_qe->getTermDatabaseSygus(); options::SygusUnifPiMode mode = options::sygusUnifPi(); d_useCondPool = mode == options::SygusUnifPiMode::CENUM || mode == options::SygusUnifPiMode::CENUM_IGAIN; diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 7bcd3788b..e450c3fa7 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -48,9 +48,9 @@ namespace quantifiers { class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf { public: - CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, - QuantifiersState& qs, + CegisUnifEnumDecisionStrategy(QuantifiersState& qs, QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* parent); /** Make the n^th literal of this strategy (G_uq_n). * @@ -101,8 +101,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf void registerEvalPts(const std::vector& eis, Node e); private: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; /** Reference to the quantifiers inference manager */ QuantifiersInferenceManager& d_qim; /** sygus term database of d_qe */ @@ -208,9 +206,9 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf class CegisUnif : public Cegis { public: - CegisUnif(QuantifiersEngine* qe, - QuantifiersState& qs, + CegisUnif(QuantifiersState& qs, QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* p); ~CegisUnif() override; /** Retrieves enumerators for constructing solutions diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index d8186e592..e79841c81 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -20,10 +20,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusModule::SygusModule(QuantifiersEngine* qe, - QuantifiersInferenceManager& qim, +SygusModule::SygusModule(QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* p) - : d_qe(qe), d_qim(qim), d_tds(qe->getTermDatabaseSygus()), d_parent(p) + : d_qim(qim), d_tds(tds), d_parent(p) { } diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 86d113edc..9c543c6b6 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -23,9 +23,6 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { class SynthConjecture; @@ -53,8 +50,8 @@ class QuantifiersInferenceManager; class SygusModule { public: - SygusModule(QuantifiersEngine* qe, - QuantifiersInferenceManager& qim, + SygusModule(QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* p); virtual ~SygusModule() {} /** initialize @@ -150,8 +147,6 @@ class SygusModule virtual bool usingRepairConst() { return false; } protected: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; /** Reference to the quantifiers inference manager */ QuantifiersInferenceManager& d_qim; /** sygus term database of d_qe */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index bc9da0c4d..170cf6fd7 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -29,10 +29,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusPbe::SygusPbe(QuantifiersEngine* qe, - QuantifiersInferenceManager& qim, +SygusPbe::SygusPbe(QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qe, qim, p) + : SygusModule(qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -75,7 +75,7 @@ bool SygusPbe::initialize(Node conj, << std::endl; std::map> strategy_lemmas; d_sygus_unif[c]->initializeCandidate( - d_qe, c, d_candidate_to_enum[c], strategy_lemmas); + d_tds, c, d_candidate_to_enum[c], strategy_lemmas); Assert(!d_candidate_to_enum[c].empty()); Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size() << " enumerators for " << c << "..." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 7b20df8de..cbd307cab 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -85,8 +85,8 @@ class SynthConjecture; class SygusPbe : public SygusModule { public: - SygusPbe(QuantifiersEngine* qe, - QuantifiersInferenceManager& qim, + SygusPbe(QuantifiersInferenceManager& qim, + TermDbSygus* tds, SynthConjecture* p); ~SygusPbe(); diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index 93474b4ae..e58c209d4 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -520,7 +520,7 @@ void SynthConjectureProcessFun::getIrrelevantArgs( } } -SynthConjectureProcess::SynthConjectureProcess(QuantifiersEngine* qe) {} +SynthConjectureProcess::SynthConjectureProcess() {} SynthConjectureProcess::~SynthConjectureProcess() {} Node SynthConjectureProcess::preSimplify(Node q) { diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index d4ae48952..5185e549f 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -276,7 +276,7 @@ struct SynthConjectureProcessFun class SynthConjectureProcess { public: - SynthConjectureProcess(QuantifiersEngine* qe); + SynthConjectureProcess(); ~SynthConjectureProcess(); /** simplify the synthesis conjecture q * Returns a formula that is equivalent to q. diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index a96974908..a7d352740 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -27,7 +27,6 @@ #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers_engine.h" #include "theory/smt_engine_subsolver.h" using namespace CVC4::kind; @@ -36,10 +35,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusRepairConst::SygusRepairConst(QuantifiersEngine* qe) - : d_qe(qe), d_allow_constant_grammar(false) +SygusRepairConst::SygusRepairConst(TermDbSygus* tds) + : d_tds(tds), d_allow_constant_grammar(false) { - d_tds = d_qe->getTermDatabaseSygus(); } void SygusRepairConst::initialize(Node base_inst, @@ -218,7 +216,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, if (fo_body.getKind() == FORALL) { // must be a CBQI quantifier - CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body, d_qe); + CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body); if (hstatus < CEG_HANDLED) { // abort if less than fully handled diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 319497f77..78c17280c 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -25,9 +25,6 @@ namespace CVC4 { class LogicInfo; namespace theory { - -class QuantifiersEngine; - namespace quantifiers { class TermDbSygus; @@ -50,7 +47,7 @@ class TermDbSygus; class SygusRepairConst { public: - SygusRepairConst(QuantifiersEngine* qe); + SygusRepairConst(TermDbSygus* tds); ~SygusRepairConst() {} /** initialize * @@ -107,8 +104,6 @@ class SygusRepairConst static bool mustRepair(Node n); private: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; /** pointer to the sygus term database of d_qe */ TermDbSygus* d_tds; /** diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 4867fc402..621b5153f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -26,23 +26,19 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusUnif::SygusUnif() - : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false) -{ -} +SygusUnif::SygusUnif() : d_tds(nullptr), d_enableMinimality(false) {} SygusUnif::~SygusUnif() {} void SygusUnif::initializeCandidate( - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, std::vector& enums, std::map>& strategy_lemmas) { - d_qe = qe; - d_tds = qe->getTermDatabaseSygus(); + d_tds = tds; d_candidates.push_back(f); // initialize the strategy - d_strategy[f].initialize(qe, f, enums); + d_strategy[f].initialize(tds, f, enums); } Node SygusUnif::getMinimalTerm(const std::vector& terms) diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index a8a82b2cf..ca5eb0a73 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -23,9 +23,6 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { class TermDbSygus; @@ -67,7 +64,7 @@ class SygusUnif * the respective function-to-synthesize. */ virtual void initializeCandidate( - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, std::vector& enums, std::map>& strategy_lemmas); @@ -92,10 +89,8 @@ class SygusUnif std::vector& lemmas) = 0; protected: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; - /** sygus term database of d_qe */ - quantifiers::TermDbSygus* d_tds; + /** Pointer to the term database sygus */ + TermDbSygus* d_tds; //-----------------------debug printing /** print ind indentations on trace c */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index a9891aa72..813aaa2b5 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -20,7 +20,6 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" #include "theory/strings/word.h" #include "util/random.h" @@ -523,7 +522,7 @@ SygusUnifIo::SygusUnifIo(SynthConjecture* p) SygusUnifIo::~SygusUnifIo() {} void SygusUnifIo::initializeCandidate( - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, std::vector& enums, std::map>& strategy_lemmas) @@ -546,7 +545,7 @@ void SygusUnifIo::initializeCandidate( } } d_ecache.clear(); - SygusUnif::initializeCandidate(qe, f, enums, strategy_lemmas); + SygusUnif::initializeCandidate(tds, f, enums, strategy_lemmas); // learn redundant operators based on the strategy d_strategy[f].staticLearnRedundantOps(strategy_lemmas); } diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 6bb7ab7c5..d7b0e231c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -276,7 +276,7 @@ class SygusUnifIo : public SygusUnif * multiple functions can be separated. */ void initializeCandidate( - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, std::vector& enums, std::map>& strategy_lemmas) override; diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index a3cf5ed19..8859ba72b 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -36,14 +36,14 @@ SygusUnifRl::SygusUnifRl(SynthConjecture* p) } SygusUnifRl::~SygusUnifRl() {} void SygusUnifRl::initializeCandidate( - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, std::vector& enums, std::map>& strategy_lemmas) { // initialize std::vector all_enums; - SygusUnif::initializeCandidate(qe, f, all_enums, strategy_lemmas); + SygusUnif::initializeCandidate(tds, f, all_enums, strategy_lemmas); // based on the strategy inferred for each function, determine if we are // using a unification strategy that is compatible our approach. StrategyRestrictions restrictions; diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index dc012c8e4..4c40e39db 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -51,7 +51,7 @@ class SygusUnifRl : public SygusUnif /** initialize */ void initializeCandidate( - QuantifiersEngine* qe, + TermDbSygus* tds, Node f, std::vector& enums, std::map>& strategy_lemmas) override; diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index d9b75fc9d..3a61c5635 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers/sygus/sygus_unif.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" using namespace std; @@ -83,14 +82,14 @@ std::ostream& operator<<(std::ostream& os, StrategyType st) return os; } -void SygusUnifStrategy::initialize(QuantifiersEngine* qe, +void SygusUnifStrategy::initialize(TermDbSygus* tds, Node f, std::vector& enums) { Assert(d_candidate.isNull()); d_candidate = f; d_root = f.getType(); - d_qe = qe; + d_tds = tds; // collect the enumerator types and form the strategy buildStrategyGraph(d_root, role_equal); @@ -263,7 +262,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren); Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..." << std::endl; - eut = d_qe->getTermDatabaseSygus()->getEvalUnfold()->unfold(eut); + eut = d_tds->getEvalUnfold()->unfold(eut); Trace("sygus-unif-debug2") << " ...got " << eut; Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index de498dc38..a1d34ad4e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -22,11 +22,10 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { +class TermDbSygus; + /** roles for enumerators * * This indicates the role of an enumerator that is allocated by approaches @@ -279,7 +278,7 @@ struct StrategyRestrictions class SygusUnifStrategy { public: - SygusUnifStrategy() : d_qe(nullptr) {} + SygusUnifStrategy() : d_tds(nullptr) {} /** initialize * * This initializes this class with function-to-synthesize f. We also call @@ -288,7 +287,7 @@ class SygusUnifStrategy * This call constructs a set of enumerators for the relevant subfields of * the grammar of f and adds them to enums. */ - void initialize(QuantifiersEngine* qe, Node f, std::vector& enums); + void initialize(TermDbSygus* tds, Node f, std::vector& enums); /** Get the root enumerator for this class */ Node getRootEnumerator() const; /** @@ -329,8 +328,8 @@ class SygusUnifStrategy void debugPrint(const char* c); private: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; + /** pointer to the term database sygus */ + TermDbSygus* d_tds; /** The candidate variable this strategy is for */ Node d_candidate; /** maps enumerators to relevant information */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index d6afd2f66..72e69afae 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -34,7 +34,6 @@ #include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" @@ -45,28 +44,28 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SynthConjecture::SynthConjecture(QuantifiersEngine* qe, - QuantifiersState& qs, +SynthConjecture::SynthConjecture(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, SygusStatistics& s) - : d_qe(qe), - d_qstate(qs), + : d_qstate(qs), d_qim(qim), d_qreg(qr), + d_treg(tr), d_stats(s), - d_tds(qe->getTermDatabaseSygus()), + d_tds(tr.getTermDatabaseSygus()), d_hasSolution(false), - d_ceg_si(new CegSingleInv(qe, s)), + d_ceg_si(new CegSingleInv(tr, s)), d_templInfer(new SygusTemplateInfer), - d_ceg_proc(new SynthConjectureProcess(qe)), + d_ceg_proc(new SynthConjectureProcess), d_ceg_gc(new CegGrammarConstructor(d_tds, this)), - d_sygus_rconst(new SygusRepairConst(qe)), + d_sygus_rconst(new SygusRepairConst(d_tds)), d_exampleInfer(new ExampleInfer(d_tds)), - d_ceg_pbe(new SygusPbe(qe, qim, this)), - d_ceg_cegis(new Cegis(qe, qim, this)), - d_ceg_cegisUnif(new CegisUnif(qe, qs, qim, this)), - d_sygus_ccore(new CegisCoreConnective(qe, qim, this)), + d_ceg_pbe(new SygusPbe(qim, d_tds, this)), + d_ceg_cegis(new Cegis(qim, d_tds, this)), + d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)), + d_sygus_ccore(new CegisCoreConnective(qim, d_tds, this)), d_master(nullptr), d_set_ce_sk_vars(false), d_repair_index(0), @@ -409,10 +408,11 @@ bool SynthConjecture::doCheck(std::vector& lems) { Trace("sygus-engine") << " * Value is : "; std::stringstream sygusEnumOut; + FirstOrderModel* m = d_treg.getModel(); for (unsigned i = 0, size = terms.size(); i < size; i++) { Node nv = enum_values[i]; - Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv; + Node onv = nv.isNull() ? m->getValue(terms[i]) : nv; TypeNode tn = onv.getType(); std::stringstream ss; TermDbSygus::toStreamSygus(ss, onv); @@ -969,7 +969,7 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) Node SynthConjecture::getModelValue(Node n) { Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; - return d_qe->getModel()->getValue(n); + return d_treg.getModel()->getValue(n); } void SynthConjecture::debugPrint(const char* c) @@ -1071,7 +1071,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out) if (its == d_exprm.end()) { d_exprm[prog].initializeSygus( - d_qe, d_candidates[i], options::sygusSamples(), true); + d_tds, d_candidates[i], options::sygusSamples(), true); if (options::sygusRewSynth()) { d_exprm[prog].enableRewriteRuleSynth(); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 1b9f656bd..efb559889 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -81,10 +81,10 @@ class EnumValGenerator class SynthConjecture { public: - SynthConjecture(QuantifiersEngine* qe, - QuantifiersState& qs, + SynthConjecture(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, + TermRegistry& tr, SygusStatistics& s); ~SynthConjecture(); /** presolve */ @@ -203,14 +203,14 @@ class SynthConjecture SygusStatistics& getSygusStatistics() { return d_stats; }; private: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; /** Reference to the quantifiers state */ QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ QuantifiersInferenceManager& d_qim; /** The quantifiers registry */ QuantifiersRegistry& d_qreg; + /** Reference to the term registry */ + TermRegistry& d_treg; /** reference to the statistics of parent */ SygusStatistics& d_stats; /** term database sygus of d_qe */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index d77a42a14..f4d50118e 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -15,11 +15,10 @@ **/ #include "theory/quantifiers/sygus/synth_engine.h" -#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/term_registry.h" using namespace CVC4::kind; using namespace std; @@ -34,12 +33,11 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe, QuantifiersRegistry& qr, TermRegistry& tr) : QuantifiersModule(qs, qim, qr, tr, qe), - d_tds(tr.getTermDatabaseSygus()), d_conj(nullptr), d_sqp(qe) { d_conjs.push_back(std::unique_ptr( - new SynthConjecture(d_quantEngine, qs, qim, qr, d_statistics))); + new SynthConjecture(qs, qim, qr, tr, d_statistics))); d_conj = d_conjs.back().get(); } @@ -159,8 +157,8 @@ void SynthEngine::assignConjecture(Node q) // allocate a new synthesis conjecture if not assigned if (d_conjs.back()->isAssigned()) { - d_conjs.push_back(std::unique_ptr(new SynthConjecture( - d_quantEngine, d_qstate, d_qim, d_qreg, d_statistics))); + d_conjs.push_back(std::unique_ptr( + new SynthConjecture(d_qstate, d_qim, d_qreg, d_treg, d_statistics))); } d_conjs.back()->assign(q); } @@ -190,7 +188,7 @@ void SynthEngine::registerQuantifier(Node q) // If it is a recursive function definition, add it to the function // definition evaluator class. Trace("cegqi") << "Registering function definition : " << q << "\n"; - FunDefEvaluator* fde = d_tds->getFunDefEvaluator(); + FunDefEvaluator* fde = d_treg.getTermDatabaseSygus()->getFunDefEvaluator(); fde->assertDefinition(q); return; } diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index a4bed1737..4644c5877 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -81,8 +81,6 @@ class SynthEngine : public QuantifiersModule void preregisterAssertion(Node n); private: - /** term database sygus of d_qe */ - TermDbSygus* d_tds; /** the conjecture formula(s) we are waiting to assign */ std::vector d_waiting_conj; /** The synthesis conjectures that this class is managing. */ -- 2.30.2