diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-09-01 16:54:47 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-01 23:54:47 +0000 |
commit | 351fe43811e35f04ced22ca459fa31f7dd94937f (patch) | |
tree | b4b95d3fa9bc5545256f4b50b89346019aa090ee | |
parent | 847ce3697de4a26e085049496ae1efb7cfb85a99 (diff) |
Clean up and document PP context. (#7102)
This marks methods const where possible and adds missing documentation.
-rw-r--r-- | src/preprocessing/passes/sort_infer.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.cpp | 25 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 53 |
4 files changed, 58 insertions, 22 deletions
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<Node> PreprocessingPassContext::getLearnedLiterals() +std::vector<Node> 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<Node>& 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<Node>& 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<Node> getLearnedLiterals(); + std::vector<Node> 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<Node>& 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. */ |