summaryrefslogtreecommitdiff
path: root/src/preprocessing
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing')
-rw-r--r--src/preprocessing/passes/ackermann.cpp6
-rw-r--r--src/preprocessing/passes/bv_to_int.cpp10
-rw-r--r--src/preprocessing/passes/foreign_theory_rewrite.cpp5
-rw-r--r--src/preprocessing/passes/fun_def_fmf.cpp3
-rw-r--r--src/preprocessing/passes/ite_simp.cpp9
-rw-r--r--src/preprocessing/passes/non_clausal_simp.cpp24
-rw-r--r--src/preprocessing/passes/pseudo_boolean_processor.cpp6
-rw-r--r--src/preprocessing/passes/real_to_int.cpp3
-rw-r--r--src/preprocessing/passes/sygus_inference.cpp4
-rw-r--r--src/preprocessing/passes/unconstrained_simplifier.cpp6
-rw-r--r--src/preprocessing/preprocessing_pass_context.cpp24
-rw-r--r--src/preprocessing/preprocessing_pass_context.h9
12 files changed, 39 insertions, 70 deletions
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index eb6410291..7f3d778fd 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -299,9 +299,9 @@ void usortsToBitVectors(const LogicInfo& d_logic,
Ackermann::Ackermann(PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "ackermann"),
- d_funcToSkolem(preprocContext->getUserContext()),
- d_usVarsToBVVars(preprocContext->getUserContext()),
- d_logic(preprocContext->getLogicInfo())
+ d_funcToSkolem(userContext()),
+ d_usVarsToBVVars(userContext()),
+ d_logic(logicInfo())
{
}
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index ad2707035..65c9bb012 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -928,11 +928,11 @@ Node BVToInt::reconstructNode(Node originalNode,
BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "bv-to-int"),
- d_binarizeCache(preprocContext->getUserContext()),
- d_eliminationCache(preprocContext->getUserContext()),
- d_rebuildCache(preprocContext->getUserContext()),
- d_bvToIntCache(preprocContext->getUserContext()),
- d_rangeAssertions(preprocContext->getUserContext())
+ d_binarizeCache(userContext()),
+ d_eliminationCache(userContext()),
+ d_rebuildCache(userContext()),
+ d_bvToIntCache(userContext()),
+ d_rangeAssertions(userContext())
{
d_nm = NodeManager::currentNM();
d_zero = d_nm->mkConst<Rational>(0);
diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp
index 888d5e43a..6040b3669 100644
--- a/src/preprocessing/passes/foreign_theory_rewrite.cpp
+++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp
@@ -28,9 +28,10 @@ namespace preprocessing {
namespace passes {
using namespace cvc5::theory;
-ForeignTheoryRewrite::ForeignTheoryRewrite(PreprocessingPassContext* preprocContext)
+ForeignTheoryRewrite::ForeignTheoryRewrite(
+ PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "foreign-theory-rewrite"),
- d_cache(preprocContext->getUserContext()){};
+ d_cache(userContext()){};
Node ForeignTheoryRewrite::simplify(Node n)
{
diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index 44dafefcb..2405702b0 100644
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -39,8 +39,7 @@ FunDefFmf::FunDefFmf(PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "fun-def-fmf"),
d_fmfRecFunctionsDefined(nullptr)
{
- d_fmfRecFunctionsDefined =
- new (true) NodeList(preprocContext->getUserContext());
+ d_fmfRecFunctionsDefined = new (true) NodeList(userContext());
}
FunDefFmf::~FunDefFmf() { d_fmfRecFunctionsDefined->deleteSelf(); }
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 54e2b657e..434256d28 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -144,16 +144,17 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
}
// Do theory specific preprocessing passes
- if (d_env.getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH)
+ if (logicInfo().isTheoryEnabled(theory::THEORY_ARITH)
&& !options::incrementalSolving())
{
if (!simpDidALotOfWork)
{
util::ContainsTermITEVisitor& contains =
*(d_iteUtilities.getContainsVisitor());
- arith::ArithIteUtils aiteu(contains,
- d_preprocContext->getUserContext(),
- d_preprocContext->getTopLevelSubstitutions().get());
+ arith::ArithIteUtils aiteu(
+ contains,
+ userContext(),
+ d_preprocContext->getTopLevelSubstitutions().get());
bool anyItes = false;
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 5610b0117..8f390a402 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -53,16 +53,12 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "non-clausal-simp"),
d_pnm(preprocContext->getProofNodeManager()),
d_llpg(d_pnm ? new smt::PreprocessProofGenerator(
- d_pnm,
- preprocContext->getUserContext(),
- "NonClausalSimp::llpg")
+ d_pnm, userContext(), "NonClausalSimp::llpg")
: nullptr),
- d_llra(d_pnm ? new LazyCDProof(d_pnm,
- nullptr,
- preprocContext->getUserContext(),
- "NonClausalSimp::llra")
+ d_llra(d_pnm ? new LazyCDProof(
+ d_pnm, nullptr, userContext(), "NonClausalSimp::llra")
: nullptr),
- d_tsubsList(preprocContext->getUserContext())
+ d_tsubsList(userContext())
{
}
@@ -91,7 +87,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
Trace("non-clausal-simplify") << "asserting to propagator" << std::endl;
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
- Assert(Rewriter::rewrite((*assertionsToPreprocess)[i])
+ Assert(rewrite((*assertionsToPreprocess)[i])
== (*assertionsToPreprocess)[i]);
// Don't reprocess substitutions
if (assertionsToPreprocess->isSubstsIndex(i))
@@ -122,7 +118,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
<< "Iterate through " << propagator->getLearnedLiterals().size()
<< " learned literals." << std::endl;
// No conflict, go through the literals and solve them
- context::Context* u = d_preprocContext->getUserContext();
+ context::Context* u = userContext();
TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions();
CVC5_UNUSED SubstitutionMap& top_level_substs = ttls.get();
// constant propagations
@@ -152,7 +148,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
{
// Simplify the literal we learned wrt previous substitutions
Node learnedLiteral = learned_literals[i].getNode();
- Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
+ Assert(rewrite(learnedLiteral) == learnedLiteral);
Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral);
// process the learned literal with substitutions and const propagations
learnedLiteral = processLearnedLit(
@@ -198,7 +194,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
// The literal should rewrite to true
Trace("non-clausal-simplify")
<< "solved " << learnedLiteral << std::endl;
- Assert(Rewriter::rewrite(nss.apply(learnedLiteral)).isConst());
+ Assert(rewrite(nss.apply(learnedLiteral)).isConst());
// else fall through
break;
}
@@ -282,7 +278,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos)
{
Assert((*pos).second.isConst());
- Assert(Rewriter::rewrite((*pos).first) == (*pos).first);
+ Assert(rewrite((*pos).first) == (*pos).first);
Assert(cps.apply((*pos).second) == (*pos).second);
}
#endif /* CVC5_ASSERTIONS */
@@ -304,7 +300,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
<< "assertionNew = " << assertionNew.getNode() << std::endl;
assertionsToPreprocess->replaceTrusted(i, assertionNew);
assertion = assertionNew.getNode();
- Assert(Rewriter::rewrite(assertion) == assertion);
+ Assert(rewrite(assertion) == assertion);
}
for (;;)
{
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index c60e636bd..ca61c9197 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -35,9 +35,9 @@ using namespace cvc5::theory::arith;
PseudoBooleanProcessor::PseudoBooleanProcessor(
PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "pseudo-boolean-processor"),
- d_pbBounds(preprocContext->getUserContext()),
- d_subCache(preprocContext->getUserContext()),
- d_pbs(preprocContext->getUserContext(), 0)
+ d_pbBounds(userContext()),
+ d_subCache(userContext()),
+ d_pbs(userContext(), 0)
{
}
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index a60b4a097..3cfc29ed6 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -34,8 +34,7 @@ namespace preprocessing {
namespace passes {
RealToInt::RealToInt(PreprocessingPassContext* preprocContext)
- : PreprocessingPass(preprocContext, "real-to-int"),
- d_cache(preprocContext->getUserContext())
+ : PreprocessingPass(preprocContext, "real-to-int"), d_cache(userContext())
{
}
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index c0cddda5e..d105c436a 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -295,9 +295,7 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions,
// make a separate smt call
std::unique_ptr<SmtEngine> rrSygus;
- theory::initializeSubsolver(rrSygus,
- d_preprocContext->getOptions(),
- d_preprocContext->getLogicInfo());
+ theory::initializeSubsolver(rrSygus, options(), logicInfo());
rrSygus->assertFormula(body);
Trace("sygus-infer") << "*** Check sat..." << std::endl;
Result r = rrSygus->checkSat();
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index f13de5e74..c8ddfc2fa 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -42,8 +42,8 @@ UnconstrainedSimplifier::UnconstrainedSimplifier(
: PreprocessingPass(preprocContext, "unconstrained-simplifier"),
d_numUnconstrainedElim(smtStatisticsRegistry().registerInt(
"preprocessor::number of unconstrained elims")),
- d_context(preprocContext->getDecisionContext()),
- d_substitutions(preprocContext->getDecisionContext())
+ d_context(context()),
+ d_substitutions(context())
{
}
@@ -591,7 +591,7 @@ void UnconstrainedSimplifier::processUnconstrained()
// Uninterpreted function - if domain is infinite, no quantifiers are
// used, and any child is unconstrained, result is unconstrained
case kind::APPLY_UF:
- if (d_preprocContext->getLogicInfo().isQuantified()
+ if (logicInfo().isQuantified()
|| !current.getType().getCardinality().isInfinite())
{
break;
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index ac0301cc0..a0894351d 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -31,20 +31,11 @@ PreprocessingPassContext::PreprocessingPassContext(
: EnvObj(env),
d_smt(smt),
d_circuitPropagator(circuitPropagator),
- d_llm(env.getTopLevelSubstitutions(),
- env.getUserContext(),
- env.getProofNodeManager()),
- d_symsInAssertions(env.getUserContext())
+ d_llm(
+ env.getTopLevelSubstitutions(), userContext(), getProofNodeManager()),
+ d_symsInAssertions(userContext())
{
}
-const Options& PreprocessingPassContext::getOptions() const
-{
- return d_env.getOptions();
-}
-const LogicInfo& PreprocessingPassContext::getLogicInfo() const
-{
- return d_env.getLogicInfo();
-}
theory::TrustSubstitutionMap&
PreprocessingPassContext::getTopLevelSubstitutions() const
@@ -60,14 +51,7 @@ prop::PropEngine* PreprocessingPassContext::getPropEngine() const
{
return d_smt->getPropEngine();
}
-context::Context* PreprocessingPassContext::getUserContext() const
-{
- return d_env.getUserContext();
-}
-context::Context* PreprocessingPassContext::getDecisionContext() const
-{
- return d_env.getContext();
-}
+
void PreprocessingPassContext::spendResource(Resource r)
{
d_env.getResourceManager()->spendResource(r);
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 29b2fda7f..79b89dda8 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -59,10 +59,6 @@ class PreprocessingPassContext : protected EnvObj
TheoryEngine* getTheoryEngine() const;
/** Get the associated Propengine. */
prop::PropEngine* getPropEngine() const;
- /** Get the current user context. */
- context::Context* getUserContext() const;
- /** Get the current decision context. */
- context::Context* getDecisionContext() const;
/** Get the associated circuit propagator. */
theory::booleans::CircuitPropagator* getCircuitPropagator() const
@@ -82,11 +78,6 @@ class PreprocessingPassContext : protected EnvObj
/** Spend resource in the resource manager of the associated Env. */
void spendResource(Resource r);
- /** Get the options of the environment */
- const Options& getOptions() const;
- /** Get the current logic info of the environment */
- const LogicInfo& getLogicInfo() const;
-
/** Get a reference to the top-level substitution map */
theory::TrustSubstitutionMap& getTopLevelSubstitutions() const;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback