Push Env class into TheoryState (#7012)

This PR is a follow-up to #7011, making the Env object available in the TheoryState base class.

diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp
index 93d410bf801934f995b501ef9c011991bcb26753..3d43077e59430255223e40f9078f6e939153ae72 100644 (file)
--- a/src/theory/arith/arith_state.cpp
+++ b/src/theory/arith/arith_state.cpp
@@ -21,10 +21,8 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-ArithState::ArithState(context::Context* c,
-                       context::UserContext* u,
-                       Valuation val)
-    : TheoryState(c, u, val), d_parent(nullptr)
+ArithState::ArithState(Env& env, Valuation val)
+    : TheoryState(env, val), d_parent(nullptr)
 {
 }
 

diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h
index a54ae6bf0249f1d1a26eed319ec8e9efa34a0c0a..0f0f02f028f0b56513c553bc2fe61a2dac31dae7 100644 (file)
--- a/src/theory/arith/arith_state.h
+++ b/src/theory/arith/arith_state.h
@@ -38,7 +38,8 @@ class TheoryArithPrivate;
 class ArithState : public TheoryState
 {
  public:
-  ArithState(context::Context* c, context::UserContext* u, Valuation val);
+  ArithState(Env& env,
+             Valuation val);
   ~ArithState() {}
   /** Are we currently in conflict? */
   bool isInConflict() const override;

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 8cb607dd7de1efee10f63f9f17e5bacde9bf7408..37069d8b80bbab26f4249462d835eb57dcb23f0d 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -39,7 +39,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_ARITH, env, out, valuation),
       d_ppRewriteTimer(smtStatisticsRegistry().registerTimer(
           "theory::arith::ppRewriteTimer")),
-      d_astate(getSatContext(), getUserContext(), valuation),
+      d_astate(env, valuation),
       d_im(*this, d_astate, d_pnm),
       d_ppre(getSatContext(), d_pnm),
       d_bab(d_astate, d_im, d_ppre, d_pnm),

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index eaa9c9294786dcc47e8ae146a6a58d82f96f8a2a..1a6dfedbbdd09d52a4057cf0b0d5d5305cd5c5c0 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -83,7 +83,7 @@ TheoryArrays::TheoryArrays(Env& env,
       d_ppEqualityEngine(getUserContext(), name + "pp", true),
       d_ppFacts(getUserContext()),
       d_rewriter(d_pnm),
-      d_state(getSatContext(), getUserContext(), valuation),
+      d_state(env, valuation),
       d_im(*this, d_state, d_pnm),
       d_literalsToPropagate(getSatContext()),
       d_literalsToPropagateIndex(getSatContext(), 0),

diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp
index 6c80e00bd5daeb4cfcc010f7a488ca19727673fe..50c6919fa28a795be4480292a85cb49e339255cf 100644 (file)
--- a/src/theory/bags/solver_state.cpp
+++ b/src/theory/bags/solver_state.cpp
@@ -27,10 +27,7 @@ namespace cvc5 {
 namespace theory {
 namespace bags {
 
-SolverState::SolverState(context::Context* c,
-                         context::UserContext* u,
-                         Valuation val)
-    : TheoryState(c, u, val)
+SolverState::SolverState(Env& env, Valuation val) : TheoryState(env, val)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);

diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
index 9c2222e955c0bf41408f1c678c2b812286f9978c..68fffacbd0bf45cc1f674bf35a7689c137d4e0d9 100644 (file)
--- a/src/theory/bags/solver_state.h
+++ b/src/theory/bags/solver_state.h
@@ -29,7 +29,8 @@ namespace bags {
 class SolverState : public TheoryState
 {
  public:
-  SolverState(context::Context* c, context::UserContext* u, Valuation val);
+  SolverState(Env& env,
+              Valuation val);
 
   /**
    * This function adds the bag representative n to the set d_bags if it is not

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 42a1e2c6bbf8202ad21da97bcda4ebcfc753cac7..f8483064d59030e2fcac5e64e393a36f84c60498 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -29,7 +29,7 @@ namespace bags {
 
 TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_BAGS, env, out, valuation),
-      d_state(getSatContext(), getUserContext(), valuation),
+      d_state(env, valuation),
       d_im(*this, d_state, d_pnm),
       d_ig(&d_state, &d_im),
       d_notify(*this, d_im),

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index f12d2caf97de2cc75209f9b7be82f6760e84f814..092bcc9ab5db95e825cd0986980abe10e42f7ec5 100644 (file)
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -27,7 +27,7 @@ namespace builtin {
 
 TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_BUILTIN, env, out, valuation),
-      d_state(getSatContext(), getUserContext(), valuation),
+      d_state(env, valuation),
       d_im(*this, d_state, d_pnm, "theory::builtin::")
 {
   // indicate we are using the default theory state and inference managers

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 1976177b79221d191816153945a30945ba21f858..d4926a785413a469115088f70b8c0aee99c9d893 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -37,7 +37,7 @@ TheoryBV::TheoryBV(Env& env,
     : Theory(THEORY_BV, env, out, valuation, name),
       d_internal(nullptr),
       d_rewriter(),
-      d_state(getSatContext(), getUserContext(), valuation),
+      d_state(env, valuation),
       d_im(*this, d_state, nullptr, "theory::bv::"),
       d_notify(d_im),
       d_invalidateModelCache(getSatContext(), true),

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 759cc4c877414bab89a49f17d30e1160448bc7c2..3dfd9b458d898108eef7a244fa366e981eea9e2b 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -60,7 +60,7 @@ TheoryDatatypes::TheoryDatatypes(Env& env,
       d_singleton_eq(getUserContext()),
       d_lemmas_produced_c(getUserContext()),
       d_sygusExtension(nullptr),
-      d_state(getSatContext(), getUserContext(), valuation),
+      d_state(env, valuation),
       d_im(*this, d_state, d_pnm),
       d_notify(d_im, *this)
 {

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index a016c789740a60213e67f1de038b1f1cc60274d1..bd5662cdd81637786876f96939e042817271cedd 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -70,7 +70,7 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation)
       d_floatToRealMap(getUserContext()),
       d_abstractionMap(getUserContext()),
       d_rewriter(getUserContext()),
-      d_state(getSatContext(), getUserContext(), valuation),
+      d_state(env, valuation),
       d_im(*this, d_state, d_pnm, "theory::fp::", false),
       d_wbFactsCache(getUserContext())
 {

diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
index 7654a6326d8d27a3f536f0ada8c66285914b7c75..39af9c2c9e8a0dab6d14349c900b8e1647e828e3 100644 (file)
--- a/src/theory/quantifiers/quantifiers_state.cpp
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -22,11 +22,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-QuantifiersState::QuantifiersState(context::Context* c,
-                                   context::UserContext* u,
+QuantifiersState::QuantifiersState(Env& env,
                                    Valuation val,
                                    const LogicInfo& logicInfo)
-    : TheoryState(c, u, val), d_ierCounterc(c), d_logicInfo(logicInfo)
+    : TheoryState(env, val),
+      d_ierCounterc(env.getContext()),
+      d_logicInfo(logicInfo)
 {
   // allow theory combination to go first, once initially
   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;

diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h
index e4a05b0787a7ece6f3269758d7ffa5487d591a23..92b744cd033b9e5635156764fcdcef674eb61ef8 100644 (file)
--- a/src/theory/quantifiers/quantifiers_state.h
+++ b/src/theory/quantifiers/quantifiers_state.h
@@ -32,8 +32,7 @@ namespace quantifiers {
 class QuantifiersState : public TheoryState
 {
  public:
-  QuantifiersState(context::Context* c,
-                   context::UserContext* u,
+  QuantifiersState(Env& env,
                    Valuation val,
                    const LogicInfo& logicInfo);
   ~QuantifiersState() {}

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 3adf53b57a8a67b88bb6090b26e96731c8d89f41..a108d4614187cf217c7a8097d16b0d8008162d12 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -34,7 +34,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env,
                                      OutputChannel& out,
                                      Valuation valuation)
     : Theory(THEORY_QUANTIFIERS, env, out, valuation),
-      d_qstate(getSatContext(), getUserContext(), valuation, getLogicInfo()),
+      d_qstate(env, valuation, getLogicInfo()),
       d_qreg(),
       d_treg(d_qstate, d_qreg),
       d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm),

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 0b16ddd27efbcb5a9ca2fd05c3dea8fc98538a4b..92d15653e328e3c8dc932fe94d60e3398f54759e 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -46,7 +46,7 @@ TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_SEP, env, out, valuation),
       d_lemmas_produced_c(getUserContext()),
       d_bounds_init(false),
-      d_state(getSatContext(), getUserContext(), valuation),
+      d_state(env, valuation),
       d_im(*this, d_state, d_pnm, "theory::sep::"),
       d_notify(*this),
       d_reduce(getUserContext()),

diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 2aaa82706d1f773f7a8fbcc07b112d79494713a4..6f8976f4d1340f4d4332976d584993dd336fa99c 100644 (file)
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -26,11 +26,8 @@ namespace cvc5 {
 namespace theory {
 namespace sets {
 
-SolverState::SolverState(context::Context* c,
-                         context::UserContext* u,
-                         Valuation val,
-                         SkolemCache& skc)
-    : TheoryState(c, u, val), d_skCache(skc), d_members(c)
+SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc)
+    : TheoryState(env, val), d_skCache(skc), d_members(env.getContext())
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);

diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h
index 63039eddd0c96599361854b20b0e6a0aa0cfe716..ff9bc8bf9c7d771c6c0049514238d3d32073b817 100644 (file)
--- a/src/theory/sets/solver_state.h
+++ b/src/theory/sets/solver_state.h
@@ -46,8 +46,7 @@ class SolverState : public TheoryState
   typedef context::CDHashMap<Node, size_t> NodeIntMap;
 
  public:
-  SolverState(context::Context* c,
-              context::UserContext* u,
+  SolverState(Env& env,
               Valuation val,
               SkolemCache& skc);
   //-------------------------------- initialize per check

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 5ea13ea4dd96ba4a7154b00d1995566f77d8cc73..23ac0874936c6eed4ec38953be1f1ecb5c789cc3 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -30,7 +30,7 @@ namespace sets {
 TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_SETS, env, out, valuation),
       d_skCache(),
-      d_state(getSatContext(), getUserContext(), valuation, d_skCache),
+      d_state(env, valuation, d_skCache),
       d_im(*this, d_state, d_pnm),
       d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, d_pnm)),
       d_notify(*d_internal.get(), d_im)

diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 1ddf2af5864f806181b766088642aad09d1d03b0..32ed6896ce7b8bce1cece14cc04129001b641c16 100644 (file)
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -28,10 +28,11 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-SolverState::SolverState(context::Context* c,
-                         context::UserContext* u,
-                         Valuation& v)
-    : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false), d_pendingConflict(InferenceId::UNKNOWN)
+SolverState::SolverState(Env& env, Valuation& v)
+    : TheoryState(env, v),
+      d_eeDisequalities(env.getContext()),
+      d_pendingConflictSet(env.getContext(), false),
+      d_pendingConflict(InferenceId::UNKNOWN)
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -64,7 +65,7 @@ EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake)
   }
   if (doMake)
   {
-    EqcInfo* ei = new EqcInfo(d_context);
+    EqcInfo* ei = new EqcInfo(d_env.getContext());
     d_eqcInfo[eqc] = ei;
     return ei;
   }

diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index 422c29760b19c938480dab423482df0f541a83d1..bbeb470f79d2675053ca3a11c5efd0e0f16fe042 100644 (file)
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -48,8 +48,7 @@ class SolverState : public TheoryState
   typedef context::CDList<Node> NodeList;
 
  public:
-  SolverState(context::Context* c,
-              context::UserContext* u,
+  SolverState(Env& env,
               Valuation& v);
   ~SolverState();
   //-------------------------------------- disequality information

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 19713d0a1e2a9c29a2a00b5e91ad67c4e479071c..8b71df31bd2b66bfa6bb30d2cd7ff640818e7e75 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -54,7 +54,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_STRINGS, env, out, valuation),
       d_notify(*this),
       d_statistics(),
-      d_state(getSatContext(), getUserContext(), d_valuation),
+      d_state(env, d_valuation),
       d_eagerSolver(d_state),
       d_termReg(d_state, d_statistics, d_pnm),
       d_extTheoryCb(),

diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index 5ac5e6ae9349a3cd8010bbcbe8fcb9f104f30230..72ab24a7edb2280c4dcabbee7375ca08e9b2e311 100644 (file)
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -20,22 +20,25 @@
 namespace cvc5 {
 namespace theory {
 
-TheoryState::TheoryState(context::Context* c,
-                         context::UserContext* u,
-                         Valuation val)
-    : d_context(c),
-      d_ucontext(u),
+TheoryState::TheoryState(Env& env, Valuation val)
+    : d_env(env),
       d_valuation(val),
       d_ee(nullptr),
-      d_conflict(c, false)
+      d_conflict(d_env.getContext(), false)
 {
 }
 
 void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
 
-context::Context* TheoryState::getSatContext() const { return d_context; }
+context::Context* TheoryState::getSatContext() const
+{
+  return d_env.getContext();
+}
 
-context::UserContext* TheoryState::getUserContext() const { return d_ucontext; }
+context::UserContext* TheoryState::getUserContext() const
+{
+  return d_env.getUserContext();
+}
 
 bool TheoryState::hasTerm(TNode a) const
 {

diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 2c7bad60b07467b9431f6a349b07e77170c9286e..58a66ef462ec14e38bdc57cdb4dba601d26e5749 100644 (file)
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -20,6 +20,7 @@
 
 #include "context/cdo.h"
 #include "expr/node.h"
+#include "smt/env.h"
 #include "theory/valuation.h"
 
 namespace cvc5 {
@@ -32,7 +33,8 @@ class EqualityEngine;
 class TheoryState
 {
  public:
-  TheoryState(context::Context* c, context::UserContext* u, Valuation val);
+  TheoryState(Env& env,
+              Valuation val);
   virtual ~TheoryState() {}
   /**
    * Set equality engine, where ee is a pointer to the official equality engine
@@ -43,6 +45,8 @@ class TheoryState
   context::Context* getSatContext() const;
   /** Get the user context */
   context::UserContext* getUserContext() const;
+  /** Get the environment */
+  Env& getEnv() const { return d_env; }
   //-------------------------------------- equality information
   /** Is t registered as a term in the equality engine of this class? */
   virtual bool hasTerm(TNode a) const;
@@ -111,10 +115,8 @@ class TheoryState
   Valuation& getValuation();
 
  protected:
-  /** Pointer to the SAT context object used by the theory. */
-  context::Context* d_context;
-  /** Pointer to the user context object used by the theory. */
-  context::UserContext* d_ucontext;
+  /** Reference to the environment. */
+  Env& d_env;
   /**
    * The valuation proxy for the Theory to communicate back with the
    * theory engine (and other theories).

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 633934f6163294ef616552e089b2562e75d30677..3525786d5a3fdffdbfff2b126f00618d613cc2f4 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -49,7 +49,7 @@ TheoryUF::TheoryUF(Env& env,
       d_ho(nullptr),
       d_functionsTerms(getSatContext()),
       d_symb(getUserContext(), instanceName),
-      d_state(getSatContext(), getUserContext(), valuation),
+      d_state(env, valuation),
       d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false),
       d_notify(d_im, *this)
 {

diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index c27c0292500cc7ee5be849d62e2b2f6635321332..f1644dfcd7bcfb4c8c11baac0aaffc8f431f219f 100644 (file)
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -208,7 +208,7 @@ class DummyTheory : public theory::Theory
  public:
   DummyTheory(Env& env, theory::OutputChannel& out, theory::Valuation valuation)
       : Theory(theoryId, env, out, valuation),
-        d_state(getSatContext(), getUserContext(), valuation)
+        d_state(env, valuation)
   {
     // use a default theory state object
     d_theoryState = &d_state;