summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/nl')
-rw-r--r--src/theory/arith/nl/cad/cdcac.cpp9
-rw-r--r--src/theory/arith/nl/cad/cdcac.h6
-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.cpp14
-rw-r--r--src/theory/arith/nl/pow2_solver.cpp7
-rw-r--r--src/theory/arith/nl/pow2_solver.h5
7 files changed, 35 insertions, 29 deletions
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index 9b37a135f..9b7678388 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -23,7 +23,7 @@
#include "theory/arith/nl/cad/projections.h"
#include "theory/arith/nl/cad/variable_ordering.h"
#include "theory/arith/nl/nl_model.h"
-#include "theory/quantifiers/extended_rewrite.h"
+#include "theory/rewriter.h"
namespace std {
/** Generic streaming operator for std::vector. */
@@ -42,7 +42,7 @@ namespace nl {
namespace cad {
CDCAC::CDCAC(Env& env, const std::vector<poly::Variable>& ordering)
- : d_env(env), d_variableOrdering(ordering)
+ : EnvObj(env), d_variableOrdering(ordering)
{
if (d_env.isTheoryProofProducing())
{
@@ -276,9 +276,8 @@ PolyVector requiredCoefficientsLazardModified(
Kind::EQUAL, nl::as_cvc_polynomial(coeff, vm), zero));
}
// if phi is false (i.e. p can not vanish)
- quantifiers::ExtendedRewriter rew;
- Node rewritten =
- rew.extendedRewrite(NodeManager::currentNM()->mkAnd(conditions));
+ Node rewritten = Rewriter::callExtendedRewrite(
+ NodeManager::currentNM()->mkAnd(conditions));
if (rewritten.isConst())
{
Assert(rewritten.getKind() == Kind::CONST_BOOLEAN);
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index b504998d8..be72e4063 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -26,6 +26,7 @@
#include <vector>
#include "smt/env.h"
+#include "smt/env_obj.h"
#include "theory/arith/nl/cad/cdcac_utils.h"
#include "theory/arith/nl/cad/constraints.h"
#include "theory/arith/nl/cad/proof_generator.h"
@@ -44,7 +45,7 @@ namespace cad {
* This class implements Cylindrical Algebraic Coverings as presented in
* https://arxiv.org/pdf/2003.05633.pdf
*/
-class CDCAC
+class CDCAC : protected EnvObj
{
public:
/** Initialize this method with the given variable ordering. */
@@ -184,9 +185,6 @@ class CDCAC
*/
void pruneRedundantIntervals(std::vector<CACInterval>& intervals);
- /** A reference to the environment */
- Env& d_env;
-
/**
* The current assignment. When the method terminates with SAT, it contains a
* model for the input constraints.
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..b8170df45 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -49,17 +49,17 @@ NonlinearExtension::NonlinearExtension(Env& env,
d_extTheoryCb(state.getEqualityEngine()),
d_extTheory(d_extTheoryCb, context(), userContext(), d_im),
d_model(),
- d_trSlv(d_im, d_model, d_astate.getEnv()),
- d_extState(d_im, d_model, d_astate.getEnv()),
+ d_trSlv(d_im, d_model, d_env),
+ d_extState(d_im, d_model, d_env),
d_factoringSlv(&d_extState),
d_monomialBoundsSlv(&d_extState),
d_monomialSlv(&d_extState),
d_splitZeroSlv(&d_extState),
d_tangentPlaneSlv(&d_extState),
- d_cadSlv(d_astate.getEnv(), d_im, d_model),
+ d_cadSlv(d_env, 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);
@@ -72,9 +72,9 @@ NonlinearExtension::NonlinearExtension(Env& env,
d_one = NodeManager::currentNM()->mkConst(Rational(1));
d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
- if (d_astate.getEnv().isTheoryProofProducing())
+ if (d_env.isTheoryProofProducing())
{
- ProofChecker* pc = d_astate.getEnv().getProofNodeManager()->getChecker();
+ ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
d_proofChecker.registerTo(pc);
}
}
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback