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 a8b056d4503dff37e8fe6687d27e8b546adae142..785127db5ca4c26b4ecbc7638836001e877f0560 100644 (file)
--- 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 b4bb896ae5365824c426177af90ef4a505489857..627129c3ab5a5a06f5e0819ee8d7e54f1d62bd28 100644 (file)
--- 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 f5e08e2f59cada01679a78bee1e7cd20b9a16100..01b191e0afc79029af98f30b7a0e44b8e16a4bda 100644 (file)
--- 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 9d8cddb690a085ea5d398f2271e359a8150a6cc4..7bb87819ea4a9af6b6b079c78b8d3cb5b473c616 100644 (file)
--- 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 3a317e0a41b87a8e828180f7e7dc7e67701e5cb4..4c6140872daecc282f916b8c35b9fdbb90a38493 100644 (file)
--- 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 319a6698b14b929bcef9244d0ca7b7f48cb61e14..19713d0a1e2a9c29a2a00b5e91ad67c4e479071c 100644 (file)
--- 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 c1ce71cef7eef7e394a90b551f6df1908f5fd877..8f0205b483e1d21404c185e58b7458f6104f7dca 100644 (file)
--- 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 */