diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/simplex.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 4 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 2 |
5 files changed, 11 insertions, 7 deletions
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index f39006788..1cd617b64 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -53,7 +53,6 @@ #pragma once -#include "expr/result.h" #include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" #include "theory/arith/error_set.h" @@ -61,6 +60,7 @@ #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" #include "util/dense_map.h" +#include "util/result.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1e3b21b17..3c5c1c414 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -28,9 +28,11 @@ namespace CVC4 { namespace theory { namespace arith { -TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) - , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) +TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals) + , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) {} TheoryArith::~TheoryArith(){ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index a0a8e2c89..d26a120ae 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -46,7 +46,9 @@ private: KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer"); public: - TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); virtual ~TheoryArith(); /** diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index ab800f10d..bf1810331 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -33,7 +33,6 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/result.h" #include "expr/statistics_registry.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() @@ -70,6 +69,7 @@ #include "util/dense_map.h" #include "util/integer.h" #include "util/rational.h" +#include "util/result.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 0c2a704e8..32c12eba7 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -31,7 +31,6 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/result.h" #include "expr/statistics_registry.h" #include "options/arith_options.h" #include "smt/logic_exception.h" @@ -67,6 +66,7 @@ #include "util/dense_map.h" #include "util/integer.h" #include "util/rational.h" +#include "util/result.h" namespace CVC4 { namespace theory { |