From a975f3af51a3730f5b848d2b55f9c6d4027fe763 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 28 Feb 2020 13:35:09 -0600
Subject: [PATCH] Use enum for quantifiers rewrite steps (#3840)

Makes trace messages easier to understand.
---
 .../quantifiers/quantifiers_rewriter.cpp      | 34 ++++++++++++--
 src/theory/quantifiers/quantifiers_rewriter.h | 46 ++++++++++++++-----
 2 files changed, 64 insertions(+), 16 deletions(-)

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index e2ee99ceb..ee2461c23 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -35,6 +35,24 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+std::ostream& operator<<(std::ostream& out, RewriteStep s)
+{
+  switch (s)
+  {
+    case COMPUTE_ELIM_SYMBOLS: out << "COMPUTE_ELIM_SYMBOLS"; break;
+    case COMPUTE_MINISCOPING: out << "COMPUTE_MINISCOPING"; break;
+    case COMPUTE_AGGRESSIVE_MINISCOPING:
+      out << "COMPUTE_AGGRESSIVE_MINISCOPING";
+      break;
+    case COMPUTE_PROCESS_TERMS: out << "COMPUTE_PROCESS_TERMS"; break;
+    case COMPUTE_PRENEX: out << "COMPUTE_PRENEX"; break;
+    case COMPUTE_VAR_ELIMINATION: out << "COMPUTE_VAR_ELIMINATION"; break;
+    case COMPUTE_COND_SPLIT: out << "COMPUTE_COND_SPLIT"; break;
+    default: out << "UnknownRewriteStep"; break;
+  }
+  return out;
+}
+
 bool QuantifiersRewriter::isLiteral( Node n ){
   switch( n.getKind() ){
   case NOT:
@@ -166,7 +184,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
   RewriteStatus status = REWRITE_DONE;
   Node ret = in;
-  int rew_op = -1;
+  RewriteStep rew_op = COMPUTE_LAST;
   //get the body
   if( in.getKind()==EXISTS ){
     std::vector< Node > children;
@@ -185,7 +203,9 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
       //compute attributes
       QAttributes qa;
       QuantAttributes::computeQuantAttributes( in, qa );
-      for( int op=0; op<COMPUTE_LAST; op++ ){
+      for (unsigned i = 0; i < COMPUTE_LAST; ++i)
+      {
+        RewriteStep op = static_cast<RewriteStep>(i);
         if( doOperation( in, op, qa ) ){
           ret = computeOperation( in, op, qa );
           if( ret!=in ){
@@ -1978,7 +1998,10 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
   return mkForAll( args, body, qa );
 }
 
-bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){
+bool QuantifiersRewriter::doOperation(Node q,
+                                      RewriteStep computeOption,
+                                      QAttributes& qa)
+{
   bool is_strict_trigger =
       qa.d_hasPattern
       && options::userPatternsQuant() == options::UserPatMode::TRUST;
@@ -2021,7 +2044,10 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
 }
 
 //general method for computing various rewrites
-Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){
+Node QuantifiersRewriter::computeOperation(Node f,
+                                           RewriteStep computeOption,
+                                           QAttributes& qa)
+{
   Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl;
   std::vector< Node > args;
   for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
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:
-- 
2.30.2