Use enum for quantifiers rewrite steps (#3840)

Makes trace messages easier to understand.

1 files changed, 34 insertions, 12 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 69e057c76..ac87f944c 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -27,6 +27,34 @@ namespace quantifiers {
 
 struct QAttributes;
 
+/**
+ * List of steps used by the quantifiers rewriter, details on these steps
+ * can be found in the class below.
+ */
+enum RewriteStep
+{
+  /** Eliminate symbols (e.g. implies, xor) */
+  COMPUTE_ELIM_SYMBOLS = 0,
+  /** Miniscoping */
+  COMPUTE_MINISCOPING,
+  /** Aggressive miniscoping */
+  COMPUTE_AGGRESSIVE_MINISCOPING,
+  /**
+   * Term processing (e.g. simplifying terms based on ITE conditions,
+   * eliminating extended arithmetic symbols).
+   */
+  COMPUTE_PROCESS_TERMS,
+  /** Prenexing */
+  COMPUTE_PRENEX,
+  /** Variable elimination */
+  COMPUTE_VAR_ELIMINATION,
+  /** Conditional splitting */
+  COMPUTE_COND_SPLIT,
+  /** Placeholder for end of steps */
+  COMPUTE_LAST
+};
+std::ostream& operator<<(std::ostream& out, RewriteStep s);
+
 class QuantifiersRewriter : public TheoryRewriter
 {
  public:
@@ -183,24 +211,18 @@ class QuantifiersRewriter : public TheoryRewriter
   static Node computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited );
   static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
 private:
-  enum{
-    COMPUTE_ELIM_SYMBOLS = 0,
-    COMPUTE_MINISCOPING,
-    COMPUTE_AGGRESSIVE_MINISCOPING,
-    COMPUTE_PROCESS_TERMS,
-    COMPUTE_PRENEX,
-    COMPUTE_VAR_ELIMINATION,
-    COMPUTE_COND_SPLIT,
-    COMPUTE_LAST
-  };
-  static Node computeOperation( Node f, int computeOption, QAttributes& qa );
+ static Node computeOperation(Node f,
+                              RewriteStep computeOption,
+                              QAttributes& qa);
+
 public:
  RewriteResponse preRewrite(TNode in) override;
  RewriteResponse postRewrite(TNode in) override;
 
 private:
   /** options */
-  static bool doOperation( Node f, int computeOption, QAttributes& qa );
+ static bool doOperation(Node f, RewriteStep computeOption, QAttributes& qa);
+
 private:
   static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
 public: