summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/arith_preprocess.cpp5
-rw-r--r--src/theory/arith/arith_preprocess.h6
-rw-r--r--src/theory/arith/branch_and_bound.cpp10
-rw-r--r--src/theory/arith/branch_and_bound.h6
-rw-r--r--src/theory/arith/equality_solver.cpp9
-rw-r--r--src/theory/arith/equality_solver.h5
-rw-r--r--src/theory/arith/inference_manager.cpp4
-rw-r--r--src/theory/arith/nl/iand_solver.cpp18
-rw-r--r--src/theory/arith/nl/iand_solver.h5
-rw-r--r--src/theory/arith/nl/nonlinear_extension.cpp4
-rw-r--r--src/theory/arith/nl/pow2_solver.cpp7
-rw-r--r--src/theory/arith/nl/pow2_solver.h5
-rw-r--r--src/theory/arith/theory_arith.cpp6
13 files changed, 55 insertions, 35 deletions
diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 6ab399348..ba2de9fdf 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -23,11 +23,12 @@ namespace cvc5 {
namespace theory {
namespace arith {
-ArithPreprocess::ArithPreprocess(ArithState& state,
+ArithPreprocess::ArithPreprocess(Env& env,
+ ArithState& state,
InferenceManager& im,
ProofNodeManager* pnm,
OperatorElim& oe)
- : d_im(im), d_opElim(oe), d_reduced(state.getUserContext())
+ : EnvObj(env), d_im(im), d_opElim(oe), d_reduced(userContext())
{
}
TrustNode ArithPreprocess::eliminate(TNode n,
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index a537c33c7..939306a6e 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -19,6 +19,7 @@
#define CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
#include "context/cdhashmap.h"
+#include "smt/env_obj.h"
#include "theory/arith/operator_elim.h"
#include "theory/logic_info.h"
@@ -40,10 +41,11 @@ class OperatorElim;
* extends that utility with the ability to generate lemmas on demand via
* the provided inference manager.
*/
-class ArithPreprocess
+class ArithPreprocess : protected EnvObj
{
public:
- ArithPreprocess(ArithState& state,
+ ArithPreprocess(Env& env,
+ ArithState& state,
InferenceManager& im,
ProofNodeManager* pnm,
OperatorElim& oe);
diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp
index ca1a2fa6f..31017dea6 100644
--- a/src/theory/arith/branch_and_bound.cpp
+++ b/src/theory/arith/branch_and_bound.cpp
@@ -28,14 +28,16 @@ namespace cvc5 {
namespace theory {
namespace arith {
-BranchAndBound::BranchAndBound(ArithState& s,
+BranchAndBound::BranchAndBound(Env& env,
+ ArithState& s,
InferenceManager& im,
PreprocessRewriteEq& ppre,
ProofNodeManager* pnm)
- : d_astate(s),
+ : EnvObj(env),
+ d_astate(s),
d_im(im),
d_ppre(ppre),
- d_pfGen(new EagerProofGenerator(pnm, s.getUserContext())),
+ d_pfGen(new EagerProofGenerator(pnm, userContext())),
d_pnm(pnm)
{
}
@@ -45,7 +47,7 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value)
TrustNode lem = TrustNode::null();
NodeManager* nm = NodeManager::currentNM();
Integer floor = value.floor();
- if (d_astate.options().arith.brabTest)
+ if (options().arith.brabTest)
{
Trace("integers") << "branch-round-and-bound enabled" << std::endl;
Integer ceil = value.ceiling();
diff --git a/src/theory/arith/branch_and_bound.h b/src/theory/arith/branch_and_bound.h
index 4281ba678..52acf6aae 100644
--- a/src/theory/arith/branch_and_bound.h
+++ b/src/theory/arith/branch_and_bound.h
@@ -23,6 +23,7 @@
#include "expr/node.h"
#include "proof/proof_node_manager.h"
#include "proof/trust_node.h"
+#include "smt/env_obj.h"
#include "theory/arith/arith_state.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/pp_rewrite_eq.h"
@@ -37,10 +38,11 @@ namespace arith {
* agnostic to the state of solver; instead is simply given (variable, value)
* pairs in branchIntegerVariable below and constructs the appropriate lemma.
*/
-class BranchAndBound
+class BranchAndBound : protected EnvObj
{
public:
- BranchAndBound(ArithState& s,
+ BranchAndBound(Env& env,
+ ArithState& s,
InferenceManager& im,
PreprocessRewriteEq& ppre,
ProofNodeManager* pnm);
diff --git a/src/theory/arith/equality_solver.cpp b/src/theory/arith/equality_solver.cpp
index 8b4e1b8dd..8e5cc9a28 100644
--- a/src/theory/arith/equality_solver.cpp
+++ b/src/theory/arith/equality_solver.cpp
@@ -23,12 +23,15 @@ namespace cvc5 {
namespace theory {
namespace arith {
-EqualitySolver::EqualitySolver(ArithState& astate, InferenceManager& aim)
- : d_astate(astate),
+EqualitySolver::EqualitySolver(Env& env,
+ ArithState& astate,
+ InferenceManager& aim)
+ : EnvObj(env),
+ d_astate(astate),
d_aim(aim),
d_notify(*this),
d_ee(nullptr),
- d_propLits(astate.getSatContext())
+ d_propLits(context())
{
}
diff --git a/src/theory/arith/equality_solver.h b/src/theory/arith/equality_solver.h
index bce30e697..8528650f0 100644
--- a/src/theory/arith/equality_solver.h
+++ b/src/theory/arith/equality_solver.h
@@ -21,6 +21,7 @@
#include "context/cdhashset.h"
#include "expr/node.h"
#include "proof/trust_node.h"
+#include "smt/env_obj.h"
#include "theory/arith/arith_state.h"
#include "theory/ee_setup_info.h"
#include "theory/uf/equality_engine.h"
@@ -39,12 +40,12 @@ class InferenceManager;
* the literals that it propagates and only explains the literals that
* originated from this class.
*/
-class EqualitySolver
+class EqualitySolver : protected EnvObj
{
using NodeSet = context::CDHashSet<Node>;
public:
- EqualitySolver(ArithState& astate, InferenceManager& aim);
+ EqualitySolver(Env& env, ArithState& astate, InferenceManager& aim);
~EqualitySolver() {}
//--------------------------------- initialization
/**
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 5ab606f96..0c6b18893 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -30,7 +30,7 @@ InferenceManager::InferenceManager(Env& env,
ProofNodeManager* pnm)
: InferenceManagerBuffered(env, ta, astate, pnm, "theory::arith::"),
// currently must track propagated literals if using the equality solver
- d_trackPropLits(astate.options().arith.arithEqSolver),
+ d_trackPropLits(options().arith.arithEqSolver),
d_propLits(context())
{
}
@@ -128,7 +128,7 @@ bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem)
{
- if (d_theoryState.options().arith.nlExtEntailConflicts)
+ if (options().arith.nlExtEntailConflicts)
{
Node ch_lemma = lem.d_node.negate();
ch_lemma = Rewriter::rewrite(ch_lemma);
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index eb5620a82..76d964934 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -34,11 +34,15 @@ namespace theory {
namespace arith {
namespace nl {
-IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model)
- : d_im(im),
+IAndSolver::IAndSolver(Env& env,
+ InferenceManager& im,
+ ArithState& state,
+ NlModel& model)
+ : EnvObj(env),
+ d_im(im),
d_model(model),
d_astate(state),
- d_initRefine(state.getUserContext())
+ d_initRefine(userContext())
{
NodeManager* nm = NodeManager::currentNM();
d_false = nm->mkConst(false);
@@ -152,7 +156,7 @@ void IAndSolver::checkFullRefine()
}
// ************* additional lemma schemas go here
- if (d_astate.options().smt.iandMode == options::IandMode::SUM)
+ if (options().smt.iandMode == options::IandMode::SUM)
{
Node lem = sumBasedLemma(i); // add lemmas based on sum mode
Trace("iand-lemma")
@@ -162,7 +166,7 @@ void IAndSolver::checkFullRefine()
d_im.addPendingLemma(
lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true);
}
- else if (d_astate.options().smt.iandMode == options::IandMode::BITWISE)
+ else if (options().smt.iandMode == options::IandMode::BITWISE)
{
Node lem = bitwiseLemma(i); // check for violated bitwise axioms
Trace("iand-lemma")
@@ -245,7 +249,7 @@ Node IAndSolver::sumBasedLemma(Node i)
Node x = i[0];
Node y = i[1];
size_t bvsize = i.getOperator().getConst<IntAnd>().d_size;
- uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity;
+ uint64_t granularity = options().smt.BVAndIntegerGranularity;
NodeManager* nm = NodeManager::currentNM();
Node lem = nm->mkNode(
EQUAL, i, d_iandUtils.createSumNode(x, y, bvsize, granularity));
@@ -259,7 +263,7 @@ Node IAndSolver::bitwiseLemma(Node i)
Node y = i[1];
unsigned bvsize = i.getOperator().getConst<IntAnd>().d_size;
- uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity;
+ uint64_t granularity = options().smt.BVAndIntegerGranularity;
Rational absI = d_model.computeAbstractModelValue(i).getConst<Rational>();
Rational concI = d_model.computeConcreteModelValue(i).getConst<Rational>();
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index 1be469259..0b6a1fac6 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -21,6 +21,7 @@
#include "context/cdhashset.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/arith/nl/iand_utils.h"
namespace cvc5 {
@@ -37,12 +38,12 @@ class NlModel;
/** Integer and solver class
*
*/
-class IAndSolver
+class IAndSolver : protected EnvObj
{
typedef context::CDHashSet<Node> NodeSet;
public:
- IAndSolver(InferenceManager& im, ArithState& state, NlModel& model);
+ IAndSolver(Env& env, InferenceManager& im, ArithState& state, NlModel& model);
~IAndSolver();
/** init last call
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index db92009f4..742e5ca49 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -58,8 +58,8 @@ NonlinearExtension::NonlinearExtension(Env& env,
d_tangentPlaneSlv(&d_extState),
d_cadSlv(d_astate.getEnv(), d_im, d_model),
d_icpSlv(d_im),
- d_iandSlv(d_im, state, d_model),
- d_pow2Slv(d_im, state, d_model)
+ d_iandSlv(env, d_im, state, d_model),
+ d_pow2Slv(env, d_im, state, d_model)
{
d_extTheory.addFunctionKind(kind::NONLINEAR_MULT);
d_extTheory.addFunctionKind(kind::EXPONENTIAL);
diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp
index d708e86e1..597a0df96 100644
--- a/src/theory/arith/nl/pow2_solver.cpp
+++ b/src/theory/arith/nl/pow2_solver.cpp
@@ -33,8 +33,11 @@ namespace theory {
namespace arith {
namespace nl {
-Pow2Solver::Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model)
- : d_im(im), d_model(model), d_initRefine(state.getUserContext())
+Pow2Solver::Pow2Solver(Env& env,
+ InferenceManager& im,
+ ArithState& state,
+ NlModel& model)
+ : EnvObj(env), d_im(im), d_model(model), d_initRefine(userContext())
{
NodeManager* nm = NodeManager::currentNM();
d_false = nm->mkConst(false);
diff --git a/src/theory/arith/nl/pow2_solver.h b/src/theory/arith/nl/pow2_solver.h
index 4c6fb8014..b4e12616c 100644
--- a/src/theory/arith/nl/pow2_solver.h
+++ b/src/theory/arith/nl/pow2_solver.h
@@ -20,6 +20,7 @@
#include "context/cdhashset.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
@@ -35,12 +36,12 @@ class NlModel;
/** pow2 solver class
*
*/
-class Pow2Solver
+class Pow2Solver : protected EnvObj
{
using NodeSet = context::CDHashSet<Node>;
public:
- Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model);
+ Pow2Solver(Env& env, InferenceManager& im, ArithState& state, NlModel& model);
~Pow2Solver();
/** init last call
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d94f81e9c..9642bf394 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -42,12 +42,12 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
d_astate(env, valuation),
d_im(env, *this, d_astate, d_pnm),
d_ppre(context(), d_pnm),
- d_bab(d_astate, d_im, d_ppre, d_pnm),
+ d_bab(env, d_astate, d_im, d_ppre, d_pnm),
d_eqSolver(nullptr),
d_internal(new TheoryArithPrivate(*this, env, d_bab)),
d_nonlinearExtension(nullptr),
d_opElim(d_pnm, logicInfo()),
- d_arithPreproc(d_astate, d_im, d_pnm, d_opElim),
+ d_arithPreproc(env, d_astate, d_im, d_pnm, d_opElim),
d_rewriter(d_opElim)
{
// currently a cyclic dependency to TheoryArithPrivate
@@ -58,7 +58,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
if (options().arith.arithEqSolver)
{
- d_eqSolver.reset(new EqualitySolver(d_astate, d_im));
+ d_eqSolver.reset(new EqualitySolver(env, d_astate, d_im));
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback