From: Gereon Kremer Date: Mon, 16 Aug 2021 16:11:18 +0000 (-0700) Subject: Use InferenceManager in ExtTheory (#7006) X-Git-Tag: cvc5-1.0.0~1383 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=11b6d67d32160681d4495fd92930ffb6ddb79abe;p=cvc5.git Use InferenceManager in ExtTheory (#7006) This PR refactors the ExtTheory class to use a given inference manager instead of a given output channel. --- diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index a8b056d45..785127db5 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -48,7 +48,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_extTheory(d_extTheoryCb, containing.getSatContext(), containing.getUserContext(), - containing.getOutputChannel()), + d_im), d_model(containing.getSatContext()), d_trSlv(d_im, d_model, pnm, containing.getUserContext()), d_extState(d_im, d_model, pnm, containing.getUserContext()), diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index b4bb896ae..627129c3a 100644 --- a/src/theory/ext_theory.cpp +++ b/src/theory/ext_theory.cpp @@ -84,9 +84,9 @@ bool ExtTheoryCallback::getReduction(int effort, ExtTheory::ExtTheory(ExtTheoryCallback& p, context::Context* c, context::UserContext* u, - OutputChannel& out) + TheoryInferenceManager& im) : d_parent(p), - d_out(out), + d_im(im), d_ext_func_terms(c), d_extfExtReducedIdMap(c), d_ci_inactive(u), @@ -237,7 +237,7 @@ bool ExtTheory::doInferencesInternal(int effort, if (!nr.isNull() && n != nr) { Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, n, nr); - if (sendLemma(lem, true)) + if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY, true)) { Trace("extt-lemma") << "ExtTheory : reduction lemma : " << lem << std::endl; @@ -287,7 +287,7 @@ bool ExtTheory::doInferencesInternal(int effort, Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq << " by " << exp[i] << std::endl; Trace("extt-debug") << "...send lemma " << lem << std::endl; - if (sendLemma(lem)) + if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY)) { Trace("extt-lemma") << "ExtTheory : substitution + rewrite lemma : " << lem @@ -359,14 +359,14 @@ bool ExtTheory::doInferencesInternal(int effort, return false; } -bool ExtTheory::sendLemma(Node lem, bool preprocess) +bool ExtTheory::sendLemma(Node lem, InferenceId id, bool preprocess) { if (preprocess) { if (d_pp_lemmas.find(lem) == d_pp_lemmas.end()) { d_pp_lemmas.insert(lem); - d_out.lemma(lem); + d_im.lemma(lem, id); return true; } } @@ -375,7 +375,7 @@ bool ExtTheory::sendLemma(Node lem, bool preprocess) if (d_lemmas.find(lem) == d_lemmas.end()) { d_lemmas.insert(lem); - d_out.lemma(lem); + d_im.lemma(lem, id); return true; } } diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h index f5e08e2f5..01b191e0a 100644 --- a/src/theory/ext_theory.h +++ b/src/theory/ext_theory.h @@ -41,6 +41,7 @@ #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" +#include "theory/theory_inference_manager.h" namespace cvc5 { namespace theory { @@ -176,7 +177,7 @@ class ExtTheory ExtTheory(ExtTheoryCallback& p, context::Context* c, context::UserContext* u, - OutputChannel& out); + TheoryInferenceManager& im); virtual ~ExtTheory() {} /** Tells this class to treat terms with Kind k as extended functions */ void addFunctionKind(Kind k) { d_extf_kind[k] = true; } @@ -291,11 +292,11 @@ class ExtTheory bool batch, bool isRed); /** send lemma on the output channel */ - bool sendLemma(Node lem, bool preprocess = false); + bool sendLemma(Node lem, InferenceId id, bool preprocess = false); /** reference to the callback */ ExtTheoryCallback& d_parent; - /** Reference to the output channel we are using */ - OutputChannel& d_out; + /** inference manager used to send lemmas */ + TheoryInferenceManager& d_im; /** the true node */ Node d_true; /** extended function terms, map to whether they are active */ diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 9d8cddb69..7bb87819e 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -28,6 +28,7 @@ const char* toString(InferenceId i) { case InferenceId::EQ_CONSTANT_MERGE: return "EQ_CONSTANT_MERGE"; case InferenceId::COMBINATION_SPLIT: return "COMBINATION_SPLIT"; + case InferenceId::EXTT_SIMPLIFY: return "EXTT_SIMPLIFY"; case InferenceId::ARITH_BLACK_BOX: return "ARITH_BLACK_BOX"; case InferenceId::ARITH_CONF_EQ: return "ARITH_CONF_EQ"; case InferenceId::ARITH_CONF_LOWER: return "ARITH_CONF_LOWER"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 3a317e0a4..4c6140872 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -45,6 +45,9 @@ enum class InferenceId EQ_CONSTANT_MERGE, // a split from theory combination COMBINATION_SPLIT, + // ---------------------------------- ext theory + // a simplification from the extended theory utility + EXTT_SIMPLIFY, // ---------------------------------- arith theory //-------------------- linear core // black box conflicts. It's magic. diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 319a6698b..19713d0a1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -58,8 +58,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_eagerSolver(d_state), d_termReg(d_state, d_statistics, d_pnm), d_extTheoryCb(), - d_extTheory(d_extTheoryCb, getSatContext(), getUserContext(), out), d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), + d_extTheory(d_extTheoryCb, getSatContext(), getUserContext(), d_im), d_rewriter(&d_statistics.d_rewrites), d_bsolver(d_state, d_im), d_csolver(d_state, d_im, d_termReg, d_bsolver), diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c1ce71cef..8f0205b48 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -262,10 +262,10 @@ class TheoryStrings : public Theory { TermRegistry d_termReg; /** The extended theory callback */ StringsExtfCallback d_extTheoryCb; - /** Extended theory, responsible for context-dependent simplification. */ - ExtTheory d_extTheory; /** The (custom) output channel of the theory of strings */ InferenceManager d_im; + /** Extended theory, responsible for context-dependent simplification. */ + ExtTheory d_extTheory; /** The theory rewriter for this theory. */ StringsRewriter d_rewriter; /** The proof rule checker */