From 76c8bc4c963b494db36074afac74e51ab39917e4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Aug 2021 11:27:03 -0500 Subject: [PATCH] Eliminate calls to currentSmtEngine (#7060) Work towards supporting multiple solvers running in parallel. There are now only 5 remaining internal calls to smt::currentSmtEngine. More will be eliminated on future PRs. --- src/preprocessing/passes/sort_infer.cpp | 3 +- src/theory/datatypes/sygus_extension.cpp | 2 +- .../candidate_rewrite_database.cpp | 9 +++--- .../quantifiers/candidate_rewrite_database.h | 4 ++- src/theory/quantifiers/expr_miner.cpp | 3 -- src/theory/quantifiers/expr_miner.h | 10 +++++-- src/theory/quantifiers/expr_miner_manager.cpp | 12 ++++++-- src/theory/quantifiers/expr_miner_manager.h | 8 +++-- src/theory/quantifiers/instantiate.cpp | 2 -- src/theory/quantifiers/query_generator.cpp | 4 +-- src/theory/quantifiers/query_generator.h | 2 +- src/theory/quantifiers/solution_filter.cpp | 9 +++--- src/theory/quantifiers/solution_filter.h | 2 +- .../sygus/ce_guided_single_inv.cpp | 6 ++-- .../quantifiers/sygus/ce_guided_single_inv.h | 2 +- .../sygus/cegis_core_connective.cpp | 2 -- .../quantifiers/sygus/enum_value_manager.cpp | 8 ++++- .../quantifiers/sygus/enum_value_manager.h | 3 ++ .../quantifiers/sygus/rcons_type_info.cpp | 5 ++-- .../quantifiers/sygus/rcons_type_info.h | 4 ++- .../sygus/sygus_enumerator_callback.cpp | 11 +++++-- .../sygus/sygus_enumerator_callback.h | 5 +++- .../quantifiers/sygus/sygus_grammar_norm.cpp | 2 -- src/theory/quantifiers/sygus/sygus_interpol.h | 4 ++- .../quantifiers/sygus/sygus_reconstruct.cpp | 8 +++-- .../quantifiers/sygus/sygus_reconstruct.h | 5 +++- .../quantifiers/sygus/sygus_repair_const.cpp | 13 ++++----- .../quantifiers/sygus/sygus_repair_const.h | 9 ++++-- .../quantifiers/sygus/synth_conjecture.cpp | 29 ++++++++++--------- .../quantifiers/sygus/synth_conjecture.h | 2 +- src/theory/quantifiers/sygus/synth_verify.cpp | 8 ++--- src/theory/quantifiers/sygus/synth_verify.h | 2 +- src/theory/quantifiers/sygus_sampler.cpp | 14 ++++----- src/theory/quantifiers/sygus_sampler.h | 6 +++- src/theory/quantifiers_engine.cpp | 1 - 35 files changed, 123 insertions(+), 96 deletions(-) diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 53f3feffc..3f6828a7b 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -20,7 +20,6 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/dump_manager.h" -#include "smt/smt_engine_scope.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" #include "theory/theory_engine.h" @@ -72,7 +71,7 @@ PreprocessingPassResult SortInferencePass::applyInternal( assertionsToPreprocess->push_back(nar); } // indicate correspondence between the functions - SmtEngine* smt = smt::currentSmtEngine(); + SmtEngine* smt = d_preprocContext->getSmt(); smt::DumpManager* dm = smt->getDumpManager(); for (const std::pair& mrf : model_replace_f) { diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 63af57592..e66b70934 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -1108,7 +1108,7 @@ Node SygusExtension::registerSearchValue(Node a, its = d_sampler[a].find(tn); } // check equivalent - its->second.checkEquivalent(bv, bvr); + its->second.checkEquivalent(bv, bvr, *d_state.options().base.out); } } diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index c2ee563e3..0fd0eebd6 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -33,11 +33,10 @@ namespace cvc5 { namespace theory { namespace quantifiers { -CandidateRewriteDatabase::CandidateRewriteDatabase(bool doCheck, - bool rewAccel, - bool silent, - bool filterPairs) - : d_tds(nullptr), +CandidateRewriteDatabase::CandidateRewriteDatabase( + Env& env, bool doCheck, bool rewAccel, bool silent, bool filterPairs) + : ExprMiner(env), + d_tds(nullptr), d_ext_rewrite(nullptr), d_doCheck(doCheck), d_rewAccel(rewAccel), diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 309aaf4b7..71ae5649f 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -45,6 +45,7 @@ class CandidateRewriteDatabase : public ExprMiner public: /** * Constructor + * @param env Reference to the environment * @param doCheck Whether to check rewrite rules using subsolvers. * @param rewAccel Whether to construct symmetry breaking lemmas based on * discovered rewrites (see option sygusRewSynthAccel()). @@ -53,7 +54,8 @@ class CandidateRewriteDatabase : public ExprMiner * @param filterPairs Whether to filter rewrite pairs using filtering * techniques from the SAT 2019 paper above. */ - CandidateRewriteDatabase(bool doCheck, + CandidateRewriteDatabase(Env& env, + bool doCheck, bool rewAccel = false, bool silent = false, bool filterPairs = true); diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 0f46fa790..fa156c839 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -17,11 +17,8 @@ #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -#include "theory/smt_engine_subsolver.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 79d0c6650..8a5ce1c1f 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -23,10 +23,14 @@ #include #include "expr/node.h" -#include "smt/smt_engine.h" #include "theory/quantifiers/sygus_sampler.h" +#include "theory/smt_engine_subsolver.h" namespace cvc5 { + +class Env; +class SmtEngine; + namespace theory { namespace quantifiers { @@ -39,7 +43,7 @@ namespace quantifiers { class ExprMiner { public: - ExprMiner() : d_sampler(nullptr) {} + ExprMiner(Env& env) : d_env(env), d_sampler(nullptr) {} virtual ~ExprMiner() {} /** initialize * @@ -60,6 +64,8 @@ class ExprMiner virtual bool addTerm(Node n, std::ostream& out) = 0; protected: + /** Reference to the env */ + Env& d_env; /** the set of variables used by this class */ std::vector d_vars; /** diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index 24ab7c30a..92b7c105d 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -21,13 +21,19 @@ namespace cvc5 { namespace theory { namespace quantifiers { -ExpressionMinerManager::ExpressionMinerManager() - : d_doRewSynth(false), +ExpressionMinerManager::ExpressionMinerManager(Env& env) + : d_env(env), + d_doRewSynth(false), d_doQueryGen(false), d_doFilterLogicalStrength(false), d_use_sygus_type(false), d_tds(nullptr), - d_crd(options::sygusRewSynthCheck(), options::sygusRewSynthAccel(), false) + d_crd(env, + options::sygusRewSynthCheck(), + options::sygusRewSynthAccel(), + false), + d_qg(env), + d_sols(env) { } diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index 32bc4744f..b38de1337 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -26,10 +26,10 @@ #include "theory/quantifiers/sygus_sampler.h" namespace cvc5 { -namespace theory { -class QuantifiersEngine; +class Env; +namespace theory { namespace quantifiers { /** ExpressionMinerManager @@ -42,7 +42,7 @@ namespace quantifiers { class ExpressionMinerManager { public: - ExpressionMinerManager(); + ExpressionMinerManager(Env& env); ~ExpressionMinerManager() {} /** Initialize this class * @@ -93,6 +93,8 @@ class ExpressionMinerManager bool addTerm(Node sol, std::ostream& out, bool& rew_print); private: + /** Reference to the env */ + Env& d_env; /** whether we are doing rewrite synthesis */ bool d_doRewSynth; /** whether we are doing query generation */ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 05361eaa1..be1633d16 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -24,8 +24,6 @@ #include "proof/lazy_proof.h" #include "proof/proof_node_manager.h" #include "smt/logic_exception.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/first_order_model.h" diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 3c3dd8d84..31d8c3c22 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -20,8 +20,6 @@ #include #include "options/quantifiers_options.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "util/random.h" using namespace std; @@ -31,7 +29,7 @@ namespace cvc5 { namespace theory { namespace quantifiers { -QueryGenerator::QueryGenerator() : d_queryCount(0) {} +QueryGenerator::QueryGenerator(Env& env) : ExprMiner(env), d_queryCount(0) {} void QueryGenerator::initialize(const std::vector& vars, SygusSampler* ss) { Assert(ss != nullptr); diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index 90b30a016..7738a4fe5 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -52,7 +52,7 @@ namespace quantifiers { class QueryGenerator : public ExprMiner { public: - QueryGenerator(); + QueryGenerator(Env& env); ~QueryGenerator() {} /** initialize */ void initialize(const std::vector& vars, diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index ccc0763b7..8844950c7 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -19,8 +19,6 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "util/random.h" using namespace cvc5::kind; @@ -29,7 +27,10 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SolutionFilterStrength::SolutionFilterStrength() : d_isStrong(true) {} +SolutionFilterStrength::SolutionFilterStrength(Env& env) + : ExprMiner(env), d_isStrong(true) +{ +} void SolutionFilterStrength::initialize(const std::vector& vars, SygusSampler* ss) { @@ -91,7 +92,7 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) } else { - Options& opts = smt::currentSmtEngine()->getOptions(); + const Options& opts = d_env.getOptions(); std::ostream* smtOut = opts.base.out; (*smtOut) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")" << std::endl; diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h index 43545d6d9..e3da8c986 100644 --- a/src/theory/quantifiers/solution_filter.h +++ b/src/theory/quantifiers/solution_filter.h @@ -40,7 +40,7 @@ namespace quantifiers { class SolutionFilterStrength : public ExprMiner { public: - SolutionFilterStrength(); + SolutionFilterStrength(Env& d_env); ~SolutionFilterStrength() {} /** initialize */ void initialize(const std::vector& vars, diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 99a5126aa..f1caca1c4 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -17,8 +17,6 @@ #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "smt/logic_exception.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -39,9 +37,9 @@ namespace cvc5 { namespace theory { namespace quantifiers { -CegSingleInv::CegSingleInv(TermRegistry& tr, SygusStatistics& s) +CegSingleInv::CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s) : d_sip(new SingleInvocationPartition), - d_srcons(new SygusReconstruct(tr.getTermDatabaseSygus(), s)), + d_srcons(new SygusReconstruct(env, tr.getTermDatabaseSygus(), s)), d_isSolved(false), d_single_invocation(false), d_treg(tr) diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 72d41592a..13757dba9 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -91,7 +91,7 @@ class CegSingleInv Node d_single_inv; public: - CegSingleInv(TermRegistry& tr, SygusStatistics& s); + CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s); ~CegSingleInv(); // get simplified conjecture diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 4bcede905..165326db7 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -19,8 +19,6 @@ #include "options/base_options.h" #include "printer/printer.h" #include "proof/unsat_core.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/transition_inference.h" diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp index fd92e4d23..8a2d70bfa 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.cpp +++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp @@ -14,6 +14,7 @@ */ #include "theory/quantifiers/sygus/enum_value_manager.h" +#include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -33,11 +34,13 @@ namespace theory { namespace quantifiers { EnumValueManager::EnumValueManager(Node e, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermRegistry& tr, SygusStatistics& s, bool hasExamples) : d_enum(e), + d_qstate(qs), d_qim(qim), d_treg(tr), d_stats(s), @@ -98,14 +101,17 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) // create the enumerator callback if (options::sygusSymBreakDynamic()) { + std::ostream* out = nullptr; if (options::sygusRewVerify()) { d_samplerRrV.reset(new SygusSampler); d_samplerRrV->initializeSygus( d_tds, e, options::sygusSamples(), false); + // use the default output for the output of sygusRewVerify + out = d_qstate.options().base.out; } d_secd.reset(new SygusEnumeratorCallbackDefault( - e, &d_stats, d_eec.get(), d_samplerRrV.get())); + e, &d_stats, d_eec.get(), d_samplerRrV.get(), out)); } // if sygus repair const is enabled, we enumerate terms with free // variables as arguments to any-constant constructors diff --git a/src/theory/quantifiers/sygus/enum_value_manager.h b/src/theory/quantifiers/sygus/enum_value_manager.h index e610764e0..c786bb6f1 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.h +++ b/src/theory/quantifiers/sygus/enum_value_manager.h @@ -42,6 +42,7 @@ class EnumValueManager { public: EnumValueManager(Node e, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermRegistry& tr, SygusStatistics& s, @@ -71,6 +72,8 @@ class EnumValueManager Node getModelValue(Node n); /** The enumerator */ Node d_enum; + /** Reference to the quantifiers state */ + QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ QuantifiersInferenceManager& d_qim; /** Reference to the term registry */ diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp index a1ae53ad1..78f8d303c 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp @@ -23,7 +23,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { -void RConsTypeInfo::initialize(TermDbSygus* tds, +void RConsTypeInfo::initialize(Env& env, + TermDbSygus* tds, SygusStatistics& s, TypeNode stn, const std::vector& builtinVars) @@ -33,7 +34,7 @@ void RConsTypeInfo::initialize(TermDbSygus* tds, d_enumerator.reset(new SygusEnumerator(tds, nullptr, &s, true)); d_enumerator->initialize(sm->mkDummySkolem("sygus_rcons", stn)); - d_crd.reset(new CandidateRewriteDatabase(true, false, true, false)); + d_crd.reset(new CandidateRewriteDatabase(env, true, false, true, false)); // since initial samples are not always useful for equivalence checks, set // their number to 0 d_sygusSampler.initialize(stn, builtinVars, 0); diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h index 4c9ae48e0..294454fe2 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.h +++ b/src/theory/quantifiers/sygus/rcons_type_info.h @@ -41,13 +41,15 @@ class RConsTypeInfo * Initialize a sygus enumerator and a candidate rewrite database for this * class' sygus datatype type. * + * @param env Reference to the environment * @param tds Database for sygus terms * @param s Statistics managed for the synth engine * @param stn The sygus datatype type encoding the syntax restrictions * @param builtinVars A list containing the builtin analog of sygus variable * list for the sygus datatype type */ - void initialize(TermDbSygus* tds, + void initialize(Env& env, + TermDbSygus* tds, SygusStatistics& s, TypeNode stn, const std::vector& builtinVars); diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp index 7b3236832..3b536695f 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp @@ -63,8 +63,12 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set& bterms) } SygusEnumeratorCallbackDefault::SygusEnumeratorCallbackDefault( - Node e, SygusStatistics* s, ExampleEvalCache* eec, SygusSampler* ssrv) - : SygusEnumeratorCallback(e, s), d_eec(eec), d_samplerRrV(ssrv) + Node e, + SygusStatistics* s, + ExampleEvalCache* eec, + SygusSampler* ssrv, + std::ostream* out) + : SygusEnumeratorCallback(e, s), d_eec(eec), d_samplerRrV(ssrv), d_out(out) { } void SygusEnumeratorCallbackDefault::notifyTermInternal(Node n, @@ -73,7 +77,8 @@ void SygusEnumeratorCallbackDefault::notifyTermInternal(Node n, { if (d_samplerRrV != nullptr) { - d_samplerRrV->checkEquivalent(bn, bnr); + Assert(d_out != nullptr); + d_samplerRrV->checkEquivalent(bn, bnr, *d_out); } } diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h index 46ca68c51..5ed28b309 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h @@ -86,7 +86,8 @@ class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback SygusEnumeratorCallbackDefault(Node e, SygusStatistics* s = nullptr, ExampleEvalCache* eec = nullptr, - SygusSampler* ssrv = nullptr); + SygusSampler* ssrv = nullptr, + std::ostream* out = nullptr); virtual ~SygusEnumeratorCallbackDefault() {} protected: @@ -101,6 +102,8 @@ class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback ExampleEvalCache* d_eec; /** sampler (for --sygus-rr-verify) */ SygusSampler* d_samplerRrV; + /** The output stream to print unsound rewrites for above */ + std::ostream* d_out; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index d4d1398f4..209d10297 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -21,8 +21,6 @@ #include "expr/dtype_cons.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "options/quantifiers_options.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 07f5ed4ad..e86ac624a 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -22,9 +22,11 @@ #include "expr/node.h" #include "expr/type_node.h" -#include "smt/smt_engine.h" namespace cvc5 { + +class SmtEngine; + namespace theory { namespace quantifiers { /** diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp index 5da282606..3073a472d 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp @@ -26,8 +26,10 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusReconstruct::SygusReconstruct(TermDbSygus* tds, SygusStatistics& s) - : d_tds(tds), d_stats(s) +SygusReconstruct::SygusReconstruct(Env& env, + TermDbSygus* tds, + SygusStatistics& s) + : d_env(env), d_tds(tds), d_stats(s) { } @@ -408,7 +410,7 @@ void SygusReconstruct::initialize(TypeNode stn) // the database. for (TypeNode tn : sfTypes) { - d_stnInfo[tn].initialize(d_tds, d_stats, tn, builtinVars); + d_stnInfo[tn].initialize(d_env, d_tds, d_stats, tn, builtinVars); } } diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index e86b1688c..4102db713 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -144,10 +144,11 @@ class SygusReconstruct : public expr::NotifyMatch /** * Constructor. * + * @param env reference to the environment * @param tds database for sygus terms * @param s statistics managed for the synth engine */ - SygusReconstruct(TermDbSygus* tds, SygusStatistics& s); + SygusReconstruct(Env& env, TermDbSygus* tds, SygusStatistics& s); /** Reconstruct solution. * @@ -297,6 +298,8 @@ class SygusReconstruct : public expr::NotifyMatch void printPool( const std::unordered_map>& pool) const; + /** Reference to the env */ + Env& d_env; /** pointer to the sygus term database */ TermDbSygus* d_tds; /** reference to the statistics of parent */ diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 739e9ab0d..d4611e6ca 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -21,9 +21,6 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "smt/smt_statistics_registry.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/logic_info.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" @@ -37,8 +34,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusRepairConst::SygusRepairConst(TermDbSygus* tds) - : d_tds(tds), d_allow_constant_grammar(false) +SygusRepairConst::SygusRepairConst(Env& env, TermDbSygus* tds) + : d_env(env), d_tds(tds), d_allow_constant_grammar(false) { } @@ -192,7 +189,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, // check whether it is not in the current logic, e.g. non-linear arithmetic. // if so, undo replacements until it is in the current logic. - LogicInfo logic = smt::currentSmtEngine()->getLogicInfo(); + const LogicInfo& logic = d_env.getLogicInfo(); if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear()) { fo_body = fitToLogic(sygusBody, @@ -531,7 +528,7 @@ Node SygusRepairConst::getFoQuery(Node body, } Node SygusRepairConst::fitToLogic(Node body, - LogicInfo& logic, + const LogicInfo& logic, Node n, const std::vector& candidates, std::vector& candidate_skeletons, @@ -570,7 +567,7 @@ Node SygusRepairConst::fitToLogic(Node body, return Node::null(); } -bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic, +bool SygusRepairConst::getFitToLogicExcludeVar(const LogicInfo& logic, Node n, Node& exvar) { diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index f0452a59c..ce6c81011 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -23,6 +23,7 @@ namespace cvc5 { +class Env; class LogicInfo; namespace theory { @@ -48,7 +49,7 @@ class TermDbSygus; class SygusRepairConst { public: - SygusRepairConst(TermDbSygus* tds); + SygusRepairConst(Env& env, TermDbSygus* tds); ~SygusRepairConst() {} /** initialize * @@ -105,6 +106,8 @@ class SygusRepairConst static bool mustRepair(Node n); private: + /** Reference to the env */ + Env& d_env; /** pointer to the sygus term database of d_qe */ TermDbSygus* d_tds; /** @@ -188,7 +191,7 @@ class SygusRepairConst * sk_vars. */ Node fitToLogic(Node body, - LogicInfo& logic, + const LogicInfo& logic, Node n, const std::vector& candidates, std::vector& candidate_skeletons, @@ -205,7 +208,7 @@ class SygusRepairConst * exvar to x. * If n is in the given logic, this method returns true. */ - bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar); + bool getFitToLogicExcludeVar(const LogicInfo& logic, Node n, Node& exvar); }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 3f7ce158c..eeadbdd54 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -24,7 +24,6 @@ #include "options/quantifiers_options.h" #include "printer/printer.h" #include "smt/logic_exception.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/first_order_model.h" @@ -57,13 +56,13 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs, d_treg(tr), d_stats(s), d_tds(tr.getTermDatabaseSygus()), - d_verify(d_tds), + d_verify(qs.options(), d_tds), d_hasSolution(false), - d_ceg_si(new CegSingleInv(tr, s)), + d_ceg_si(new CegSingleInv(qs.getEnv(), tr, s)), d_templInfer(new SygusTemplateInfer), d_ceg_proc(new SynthConjectureProcess), d_ceg_gc(new CegGrammarConstructor(d_tds, this)), - d_sygus_rconst(new SygusRepairConst(d_tds)), + d_sygus_rconst(new SygusRepairConst(qs.getEnv(), d_tds)), d_exampleInfer(new ExampleInfer(d_tds)), d_ceg_pbe(new SygusPbe(qim, d_tds, this)), d_ceg_cegis(new Cegis(qim, d_tds, this)), @@ -514,7 +513,7 @@ bool SynthConjecture::doCheck() { if (printDebug) { - Options& sopts = smt::currentSmtEngine()->getOptions(); + const Options& sopts = d_qstate.options(); std::ostream& out = *sopts.base.out; out << "(sygus-candidate "; Assert(d_quant[0].getNumChildren() == candidate_values.size()); @@ -764,7 +763,7 @@ EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e) bool hasExamples = (d_exampleInfer->hasExamples(f) && d_exampleInfer->getNumExamples(f) != 0); d_enumManager[e].reset( - new EnumValueManager(e, d_qim, d_treg, d_stats, hasExamples)); + new EnumValueManager(e, d_qstate, d_qim, d_treg, d_stats, hasExamples)); EnumValueManager* eman = d_enumManager[e].get(); // set up the examples if (hasExamples) @@ -800,7 +799,7 @@ void SynthConjecture::printAndContinueStream(const std::vector& enums, Assert(d_master != nullptr); // we have generated a solution, print it // get the current output stream - Options& sopts = smt::currentSmtEngine()->getOptions(); + const Options& sopts = d_qstate.options(); printSynthSolutionInternal(*sopts.base.out); excludeCurrentSolution(enums, values); } @@ -881,19 +880,21 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) != options::SygusFilterSolMode::NONE)) { Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl; - std::map::iterator its = + std::map>::iterator its = d_exprm.find(prog); if (its == d_exprm.end()) { - d_exprm[prog].initializeSygus( + d_exprm[prog].reset(new ExpressionMinerManager(d_qstate.getEnv())); + ExpressionMinerManager* emm = d_exprm[prog].get(); + emm->initializeSygus( d_tds, d_candidates[i], options::sygusSamples(), true); if (options::sygusRewSynth()) { - d_exprm[prog].enableRewriteRuleSynth(); + emm->enableRewriteRuleSynth(); } if (options::sygusQueryGen()) { - d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh()); + emm->enableQueryGeneration(options::sygusQueryGenThresh()); } if (options::sygusFilterSolMode() != options::SygusFilterSolMode::NONE) @@ -901,18 +902,18 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) if (options::sygusFilterSolMode() == options::SygusFilterSolMode::STRONG) { - d_exprm[prog].enableFilterStrongSolutions(); + emm->enableFilterStrongSolutions(); } else if (options::sygusFilterSolMode() == options::SygusFilterSolMode::WEAK) { - d_exprm[prog].enableFilterWeakSolutions(); + emm->enableFilterWeakSolutions(); } } its = d_exprm.find(prog); } bool rew_print = false; - is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print); + is_unique_term = its->second->addTerm(sol, out, rew_print); if (rew_print) { ++(d_stats.d_candidate_rewrites_print); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index c1635c05c..9cc488fd2 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -363,7 +363,7 @@ class SynthConjecture * This is used for the sygusRewSynth() option to synthesize new candidate * rewrite rules. */ - std::map d_exprm; + std::map> d_exprm; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp index 2d7255415..23ee0e648 100644 --- a/src/theory/quantifiers/sygus/synth_verify.cpp +++ b/src/theory/quantifiers/sygus/synth_verify.cpp @@ -19,7 +19,6 @@ #include "options/arith_options.h" #include "options/base_options.h" #include "options/quantifiers_options.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -33,12 +32,11 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SynthVerify::SynthVerify(TermDbSygus* tds) : d_tds(tds) +SynthVerify::SynthVerify(const Options& opts, TermDbSygus* tds) : d_tds(tds) { // determine the options to use for the verification subsolvers we spawn - // we start with the options of the current SmtEngine - SmtEngine* smtCurr = smt::currentSmtEngine(); - d_subOptions.copyValues(smtCurr->getOptions()); + // we start with the provided options + d_subOptions.copyValues(opts); // limit the number of instantiation rounds on subcalls d_subOptions.quantifiers.instMaxRounds = d_subOptions.quantifiers.sygusVerifyInstMaxRounds; diff --git a/src/theory/quantifiers/sygus/synth_verify.h b/src/theory/quantifiers/sygus/synth_verify.h index 794908ee5..c4d1052da 100644 --- a/src/theory/quantifiers/sygus/synth_verify.h +++ b/src/theory/quantifiers/sygus/synth_verify.h @@ -34,7 +34,7 @@ namespace quantifiers { class SynthVerify { public: - SynthVerify(TermDbSygus* tds); + SynthVerify(const Options& opts, TermDbSygus* tds); ~SynthVerify(); /** * Verification call, which takes into account specific aspects of the diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index c072fd7b4..0cbc4df5b 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -23,8 +23,6 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "theory/quantifiers/lazy_trie.h" #include "theory/rewriter.h" #include "util/bitvector.h" @@ -780,7 +778,7 @@ void SygusSampler::registerSygusType(TypeNode tn) } } -void SygusSampler::checkEquivalent(Node bv, Node bvr) +void SygusSampler::checkEquivalent(Node bv, Node bvr, std::ostream& out) { if (bv == bvr) { @@ -831,14 +829,12 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr) return; } // we have detected unsoundness in the rewriter - Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream* out = sopts.base.out; - (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl; + out << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl; // debugging information - (*out) << "Terms are not equivalent for : " << std::endl; - (*out) << ptOut.str(); + out << "Terms are not equivalent for : " << std::endl; + out << ptOut.str(); Assert(bve != bvre); - (*out) << "where they evaluate to " << bve << " and " << bvre << std::endl; + out << "where they evaluate to " << bve << " and " << bvre << std::endl; if (options::sygusRewVerifyAbort()) { diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index c56b1c0b1..85606adc6 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -170,8 +170,12 @@ class SygusSampler : public LazyTrieEvaluator * * Check whether bv and bvr are equivalent on all sample points, print * an error if not. Used with --sygus-rr-verify. + * + * @param bv The original term + * @param bvr The rewritten form of bvr + * @param out The output stream to write if the rewrite was unsound. */ - void checkEquivalent(Node bv, Node bvr); + void checkEquivalent(Node bv, Node bvr, std::ostream& out); protected: /** sygus term database of d_qe */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ccd177b7d..213b6c55e 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -21,7 +21,6 @@ #include "options/smt_options.h" #include "options/strings_options.h" #include "options/uf_options.h" -#include "smt/smt_engine_scope.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/first_order_model_fmc.h" -- 2.30.2