From: Aina Niemetz Date: Wed, 1 Sep 2021 23:54:47 +0000 (-0700) Subject: Clean up and document PP context. (#7102) X-Git-Tag: cvc5-1.0.0~1301 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=351fe43811e35f04ced22ca459fa31f7dd94937f;p=cvc5.git Clean up and document PP context. (#7102) This marks methods const where possible and adds missing documentation. --- diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 3f6828a7b..7d1c5bf54 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -20,6 +20,7 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/dump_manager.h" +#include "smt/smt_engine.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" #include "theory/theory_engine.h" diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index e3cb13851..3b2a088a2 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -20,6 +20,7 @@ #include "printer/printer.h" #include "smt/dump.h" #include "smt/output_manager.h" +#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "util/statistics_stats.h" diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index fe4c8784a..8a8bad20f 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -17,6 +17,7 @@ #include "expr/node_algorithm.h" #include "smt/env.h" +#include "smt/smt_engine.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" @@ -36,31 +37,39 @@ PreprocessingPassContext::PreprocessingPassContext( d_symsInAssertions(env.getUserContext()) { } -const Options& PreprocessingPassContext::getOptions() +const Options& PreprocessingPassContext::getOptions() const { return d_env.getOptions(); } -const LogicInfo& PreprocessingPassContext::getLogicInfo() +const LogicInfo& PreprocessingPassContext::getLogicInfo() const { return d_env.getLogicInfo(); } -theory::Rewriter* PreprocessingPassContext::getRewriter() +theory::Rewriter* PreprocessingPassContext::getRewriter() const { return d_env.getRewriter(); } theory::TrustSubstitutionMap& -PreprocessingPassContext::getTopLevelSubstitutions() +PreprocessingPassContext::getTopLevelSubstitutions() const { return d_env.getTopLevelSubstitutions(); } -context::Context* PreprocessingPassContext::getUserContext() +TheoryEngine* PreprocessingPassContext::getTheoryEngine() const +{ + return d_smt->getTheoryEngine(); +} +prop::PropEngine* PreprocessingPassContext::getPropEngine() const +{ + return d_smt->getPropEngine(); +} +context::Context* PreprocessingPassContext::getUserContext() const { return d_env.getUserContext(); } -context::Context* PreprocessingPassContext::getDecisionContext() +context::Context* PreprocessingPassContext::getDecisionContext() const { return d_env.getContext(); } @@ -88,7 +97,7 @@ void PreprocessingPassContext::notifyLearnedLiteral(TNode lit) d_llm.notifyLearnedLiteral(lit); } -std::vector PreprocessingPassContext::getLearnedLiterals() +std::vector PreprocessingPassContext::getLearnedLiterals() const { return d_llm.getLearnedLiterals(); } @@ -108,7 +117,7 @@ void PreprocessingPassContext::addSubstitution(const Node& lhs, getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args); } -ProofNodeManager* PreprocessingPassContext::getProofNodeManager() +ProofNodeManager* PreprocessingPassContext::getProofNodeManager() const { return d_env.getProofNodeManager(); } diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 901322a10..a2407b953 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -24,53 +24,78 @@ #include "context/cdhashset.h" #include "preprocessing/learned_literal_manager.h" -#include "smt/smt_engine.h" +#include "theory/logic_info.h" #include "util/resource_manager.h" namespace cvc5 { + +class Env; class SmtEngine; class TheoryEngine; + +namespace theory { +class Rewriter; +} + namespace theory::booleans { class CircuitPropagator; } + namespace prop { class PropEngine; } + namespace preprocessing { class PreprocessingPassContext { public: + /** Constructor. */ PreprocessingPassContext( SmtEngine* smt, Env& env, theory::booleans::CircuitPropagator* circuitPropagator); - SmtEngine* getSmt() { return d_smt; } - TheoryEngine* getTheoryEngine() { return d_smt->getTheoryEngine(); } - prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); } - context::Context* getUserContext(); - context::Context* getDecisionContext(); + /** Get the associated SmtEngine. */ + SmtEngine* getSmt() const { return d_smt; } - theory::booleans::CircuitPropagator* getCircuitPropagator() + /** Get the associated TheoryEngine. */ + 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 { return d_circuitPropagator; } - context::CDHashSet& getSymsInAssertions() { return d_symsInAssertions; } + /** + * Get the (user-context-dependent) set of symbols that occur in at least one + * assertion in the current user context. + */ + const context::CDHashSet& getSymsInAssertions() const + { + return d_symsInAssertions; + } + /** Spend resource in the resource manager of the associated Env. */ void spendResource(Resource r); /** Get the options of the environment */ - const Options& getOptions(); + const Options& getOptions() const; /** Get the current logic info of the environment */ - const LogicInfo& getLogicInfo(); + const LogicInfo& getLogicInfo() const; /** Get a pointer to the Rewriter owned by the associated Env. */ - theory::Rewriter* getRewriter(); + theory::Rewriter* getRewriter() const; /** Get a reference to the top-level substitution map */ - theory::TrustSubstitutionMap& getTopLevelSubstitutions(); + theory::TrustSubstitutionMap& getTopLevelSubstitutions() const; /** Record symbols in assertions * @@ -90,7 +115,7 @@ class PreprocessingPassContext /** * Get the learned literals */ - std::vector getLearnedLiterals(); + std::vector getLearnedLiterals() const; /** * Add substitution to the top-level substitutions, which also as a * consequence is used by the theory model. @@ -108,7 +133,7 @@ class PreprocessingPassContext const std::vector& args); /** The the proof node manager associated with this context, if it exists */ - ProofNodeManager* getProofNodeManager(); + ProofNodeManager* getProofNodeManager() const; private: /** Pointer to the SmtEngine that this context was created in. */