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 3f6828a7b31a63308997202787590cc040da816f..7d1c5bf54cb268df24960c34b34fcebe8f263205 100644 (file)
--- 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 e3cb1385135e62389ed80c642f02d85f3df25d9e..3b2a088a25ed6e8f35b64c375ec5cfd80f407597 100644 (file)
--- 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 fe4c8784a14a5e073db82a7735b7e7fb3147b8ae..8a8bad20fa58efbcead3ab4aaa3d50c68efb1184 100644 (file)
--- 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 901322a1024c634a457faf40bedc7abf274e788e..a2407b953cf252b48e506fa68a8c9b86d19cbad2 100644 (file)
--- 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. */