Refactor non-clausal simplify preprocessing pass. (#2425)

1 files changed, 22 insertions, 1 deletions

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index a2e83aa4c..ae989d700 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -55,6 +55,11 @@ class PreprocessingPassContext
     return d_circuitPropagator;
   }
 
+  context::CDHashSet<Node, NodeHashFunction>& getSymsInAssertions()
+  {
+    return d_symsInAssertions;
+  }
+
   void spendResource(unsigned amount)
   {
     d_resourceManager->spendResource(amount);
@@ -68,9 +73,18 @@ class PreprocessingPassContext
   /* Enable Integers. */
   void enableIntegers();
 
+  /** Record symbols in assertions
+   *
+   * This method is called when a set of assertions is finalized. It adds
+   * the symbols to d_symsInAssertions that occur in assertions.
+   */
+  void recordSymbolsInAssertions(const std::vector<Node>& assertions);
+
  private:
-  /* Pointer to the SmtEngine that this context was created in. */
+  /** Pointer to the SmtEngine that this context was created in. */
   SmtEngine* d_smt;
+
+  /** Pointer to the ResourceManager for this context. */
   ResourceManager* d_resourceManager;
 
   /** Instance of the ITE remover */
@@ -78,6 +92,13 @@ class PreprocessingPassContext
 
   /** Instance of the circuit propagator */
   theory::booleans::CircuitPropagator* d_circuitPropagator;
+
+  /**
+   * The (user-context-dependent) set of symbols that occur in at least one
+   * assertion in the current user context.
+   */
+  context::CDHashSet<Node, NodeHashFunction> d_symsInAssertions;
+
 };  // class PreprocessingPassContext
 
 }  // namespace preprocessing