Refactor quantifier macros preprocessing pass (#1840)

Moved `src/theory/quantifiers/macros.{cpp,h}` to `src/preprocessing/passes/quantifier_macros.{cpp,h}`,
and added the necessary methods for inheritance from PreprocessingPass.

No need to add a test - regress0 fails when adding Assert(false) when assertions had changed.

5 files changed, 149 insertions, 98 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index d399602cb..e0a9fb807 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -95,6 +95,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/bv_to_bool.h \
 	preprocessing/passes/quantifiers_preprocess.cpp \
 	preprocessing/passes/quantifiers_preprocess.h \
+	preprocessing/passes/quantifier_macros.cpp \
+	preprocessing/passes/quantifier_macros.h \
 	preprocessing/passes/real_to_int.cpp \
 	preprocessing/passes/real_to_int.h \
 	preprocessing/passes/rewrite.cpp \
@@ -482,8 +484,6 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/lazy_trie.h \
 	theory/quantifiers/local_theory_ext.cpp \
 	theory/quantifiers/local_theory_ext.h \
-	theory/quantifiers/macros.cpp \
-	theory/quantifiers/macros.h \
 	theory/quantifiers/quant_conflict_find.cpp \
 	theory/quantifiers/quant_conflict_find.h \
 	theory/quantifiers/quant_epr.cpp \
diff --git a/src/theory/quantifiers/macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index d88f8eec9..e3bc02309 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file macros.cpp
+/*! \file quantifier_macros.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Kshitij Bansal
@@ -14,7 +14,7 @@
  ** This class implements quantifiers macro definitions.
  **/
 
-#include "theory/quantifiers/macros.h"
+#include "preprocessing/passes/quantifier_macros.h"
 
 #include <vector>
 
@@ -27,19 +27,48 @@
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4;
 using namespace std;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
 
-QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){
+QuantifierMacros::QuantifierMacros(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "quantifier-macros"),
+      d_ground_macros(false)
+{
+}
+
+PreprocessingPassResult QuantifierMacros::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  bool success;
+  do
+  {
+    success = simplify(assertionsToPreprocess->ref(), true);
+  } while (success);
+  finalizeDefinitions();
+  clearMaps();
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+void QuantifierMacros::clearMaps()
+{
+  d_macro_basis.clear();
+  d_macro_defs.clear();
+  d_macro_defs_new.clear();
+  d_macro_def_contains.clear();
+  d_simplify_cache.clear();
+  d_quant_macros.clear();
   d_ground_macros = false;
 }
-  
+
 bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
   unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1;
   for( unsigned r=0; r<rmax; r++ ){
@@ -72,14 +101,14 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
           //for now, it is dependent upon all assertions involving macros, this is an over-approximation.
           //a more fine-grained unsat core computation would require caching dependencies for each subterm of the formula, 
           // which is expensive.
-          PROOF( 
-            ProofManager::currentPM()->addDependence(curr, assertions[i]); 
-            for( unsigned j=0; j<macro_assertions.size(); j++ ){
-              if( macro_assertions[j]!=assertions[i] ){
-                ProofManager::currentPM()->addDependence(curr,macro_assertions[j]);
-              }
-            }
-          );
+          PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]);
+                for (unsigned j = 0; j < macro_assertions.size(); j++) {
+                  if (macro_assertions[j] != assertions[i])
+                  {
+                    ProofManager::currentPM()->addDependence(
+                        curr, macro_assertions[j]);
+                  }
+                });
           assertions[i] = curr;
           retVal = true;
         }
@@ -154,7 +183,10 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
 }
 
 bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
-  Node icn = d_qe->getTermUtil()->substituteBoundVariablesToInstConstants(n, f);
+  Node icn = d_preprocContext->getTheoryEngine()
+                 ->getQuantifiersEngine()
+                 ->getTermUtil()
+                 ->substituteBoundVariablesToInstConstants(n, f);
   Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
   std::vector< Node > var;
   quantifiers::TermUtil::computeInstConstContainsForQuant(f, icn, var);
@@ -512,3 +544,7 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
     }
   }
 }
+
+}  // passes
+}  // preprocessing
+}  // CVC4
diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
new file mode 100644
index 000000000..092a62942
--- /dev/null
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file quantifier_macros.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Pre-process step for detecting quantifier macro definitions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+#define __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+
+#include <map>
+#include <string>
+#include <vector>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class QuantifierMacros : public PreprocessingPass
+{
+ public:
+  QuantifierMacros(PreprocessingPassContext* preprocContext);
+  ~QuantifierMacros() {}
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  bool processAssertion(Node n);
+  bool isBoundVarApplyUf(Node n);
+  bool process(Node n, bool pol, std::vector<Node>& args, Node f);
+  bool containsBadOp(Node n,
+                     Node op,
+                     std::vector<Node>& opc,
+                     std::map<Node, bool>& visited);
+  bool isMacroLiteral(Node n, bool pol);
+  bool isGroundUfTerm(Node f, Node n);
+  void getMacroCandidates(Node n,
+                          std::vector<Node>& candidates,
+                          std::map<Node, bool>& visited);
+  Node solveInEquality(Node n, Node lit);
+  bool getFreeVariables(Node n,
+                        std::vector<Node>& v_quant,
+                        std::vector<Node>& vars,
+                        bool retOnly,
+                        std::map<Node, bool>& visited);
+  bool getSubstitution(std::vector<Node>& v_quant,
+                       std::map<Node, Node>& solved,
+                       std::vector<Node>& vars,
+                       std::vector<Node>& subs,
+                       bool reqComplete);
+  void addMacro(Node op, Node n, std::vector<Node>& opc);
+  void debugMacroDefinition(Node oo, Node n);
+  bool simplify(std::vector<Node>& assertions, bool doRewrite = false);
+  Node simplify(Node n);
+  void finalizeDefinitions();
+  void clearMaps();
+
+  // map from operators to macro basis terms
+  std::map<Node, std::vector<Node> > d_macro_basis;
+  // map from operators to macro definition
+  std::map<Node, Node> d_macro_defs;
+  std::map<Node, Node> d_macro_defs_new;
+  // operators to macro ops that contain them
+  std::map<Node, std::vector<Node> > d_macro_def_contains;
+  // simplify caches
+  std::map<Node, Node> d_simplify_cache;
+  std::map<Node, bool> d_quant_macros;
+  bool d_ground_macros;
+};
+
+}  // passes
+}  // preprocessing
+}  // CVC4
+
+#endif /*__CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 70e575487..0497c2814 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -85,6 +85,8 @@
 #include "preprocessing/passes/ite_simp.h"
 #include "preprocessing/passes/nl_ext_purify.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
+#include "preprocessing/passes/quantifier_macros.h"
+#include "preprocessing/passes/quantifier_macros.h"
 #include "preprocessing/passes/quantifiers_preprocess.h"
 #include "preprocessing/passes/real_to_int.h"
 #include "preprocessing/passes/rewrite.h"
@@ -118,7 +120,6 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/logic_info.h"
 #include "theory/quantifiers/fun_def_process.h"
-#include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/single_inv_partition.h"
 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
@@ -2686,6 +2687,8 @@ void SmtEnginePrivate::finishInit()
                                            std::move(bvAckermann));
   d_preprocessingPassRegistry.registerPass("bv-eager-atoms",
                                            std::move(bvEagerAtoms));
+  std::unique_ptr<QuantifierMacros> quantifierMacros(
+      new QuantifierMacros(d_preprocessingPassContext.get()));
   d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss));
   d_preprocessingPassRegistry.registerPass("bv-intro-pow2",
                                            std::move(bvIntroPow2));
@@ -2715,6 +2718,8 @@ void SmtEnginePrivate::finishInit()
                                            std::move(sygusInfer));
   d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc));
   d_preprocessingPassRegistry.registerPass("synth-rr", std::move(srrProc));
+  d_preprocessingPassRegistry.registerPass("quantifier-macros",
+                                           std::move(quantifierMacros));
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
@@ -4078,13 +4083,8 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-skolem-quant", d_assertions);
     if( options::macrosQuant() ){
       //quantifiers macro expansion
-      quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() );
-      bool success;
-      do{
-        success = qm.simplify( d_assertions.ref(), true );
-      }while( success );
-      //finalize the definitions
-      qm.finalizeDefinitions();
+      d_preprocessingPassRegistry.getPass("quantifier-macros")
+          ->apply(&d_assertions);
     }
 
     //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
deleted file mode 100644
index b36be7aec..000000000
--- a/src/theory/quantifiers/macros.h
+++ /dev/null
@@ -1,74 +0,0 @@
-/*********************                                                        */
-/*! \file macros.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Pre-process step for detecting quantifier macro definitions
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_MACROS_H
-#define __CVC4__QUANTIFIERS_MACROS_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class QuantifierMacros{
-private:
-  QuantifiersEngine * d_qe;
-private:
-  bool d_ground_macros;
-  bool processAssertion( Node n );
-  bool isBoundVarApplyUf( Node n );
-  bool process( Node n, bool pol, std::vector< Node >& args, Node f );
-  bool containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited );
-  bool isMacroLiteral( Node n, bool pol );
-  bool isGroundUfTerm( Node f, Node n );
-  void getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited );
-  Node solveInEquality( Node n, Node lit );
-  bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited );
-  bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
-                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete );
-  //map from operators to macro basis terms
-  std::map< Node, std::vector< Node > > d_macro_basis;
-  //map from operators to macro definition
-  std::map< Node, Node > d_macro_defs;
-  std::map< Node, Node > d_macro_defs_new;
-  //operators to macro ops that contain them
-  std::map< Node, std::vector< Node > > d_macro_def_contains;
-  //simplify caches
-  std::map< Node, Node > d_simplify_cache;
-  std::map< Node, bool > d_quant_macros;
-private:
-  Node simplify( Node n );
-  void addMacro( Node op, Node n, std::vector< Node >& opc );
-  void debugMacroDefinition( Node oo, Node n );
-public:
-  QuantifierMacros( QuantifiersEngine * qe );
-  ~QuantifierMacros(){}
-
-  bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
-  void finalizeDefinitions();
-};
-
-}
-}
-}
-
-#endif