diff options
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/ackermann.cpp | 6 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 10 | ||||
-rw-r--r-- | src/preprocessing/passes/foreign_theory_rewrite.cpp | 5 | ||||
-rw-r--r-- | src/preprocessing/passes/fun_def_fmf.cpp | 3 | ||||
-rw-r--r-- | src/preprocessing/passes/ite_simp.cpp | 9 | ||||
-rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 24 | ||||
-rw-r--r-- | src/preprocessing/passes/pseudo_boolean_processor.cpp | 6 | ||||
-rw-r--r-- | src/preprocessing/passes/real_to_int.cpp | 3 | ||||
-rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 4 | ||||
-rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 6 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.cpp | 24 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 9 |
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; |