From: yoni206 <yoni206@users.noreply.github.com>
Date: Sat, 25 Aug 2018 21:31:32 +0000 (-0700)
Subject: Refactor quantifier macros preprocessing pass (#1840)
X-Git-Tag: cvc5-1.0.0~4721
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c66033a67511b10b5ee22b7072b9ceab45552a79;p=cvc5.git

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.
---

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/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
new file mode 100644
index 000000000..e3bc02309
--- /dev/null
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -0,0 +1,550 @@
+/*********************                                                        */
+/*! \file quantifier_macros.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King, Kshitij Bansal
+ ** 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 Sort inference module
+ **
+ ** This class implements quantifiers macro definitions.
+ **/
+
+#include "preprocessing/passes/quantifier_macros.h"
+
+#include <vector>
+
+#include "options/quantifiers_modes.h"
+#include "options/quantifiers_options.h"
+#include "proof/proof_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/arith/arith_msum.h"
+#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 std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+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++ ){
+    d_ground_macros = (r==0);
+    Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
+    //first, collect macro definitions
+    std::vector< Node > macro_assertions;
+    for( int i=0; i<(int)assertions.size(); i++ ){
+      Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
+      if( processAssertion( assertions[i] ) ){
+        PROOF( 
+          if( std::find( macro_assertions.begin(), macro_assertions.end(), assertions[i] )==macro_assertions.end() ){
+            macro_assertions.push_back( assertions[i] );
+          }
+        );
+        //process this assertion again
+        i--;
+      }
+    }
+    Trace("macros") << "...finished process, #new def = " << d_macro_defs_new.size() << std::endl;
+    if( doRewrite && !d_macro_defs_new.empty() ){
+      bool retVal = false;
+      Trace("macros") << "Do simplifications..." << std::endl;
+      //now, rewrite based on macro definitions
+      for( unsigned i=0; i<assertions.size(); i++ ){
+        Node curr = simplify( assertions[i] );
+        if( curr!=assertions[i] ){
+          curr = Rewriter::rewrite( curr );
+          Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
+          //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]);
+                  }
+                });
+          assertions[i] = curr;
+          retVal = true;
+        }
+      }
+      d_macro_defs_new.clear();
+      if( retVal ){
+        return true;
+      }
+    }
+  }
+  if( Trace.isOn("macros-warn") ){
+    for( unsigned i=0; i<assertions.size(); i++ ){
+      debugMacroDefinition( assertions[i], assertions[i] );
+    }
+  }
+  return false;
+}
+
+bool QuantifierMacros::processAssertion( Node n ) {
+  if( n.getKind()==AND ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( processAssertion( n[i] ) ){
+        return true;
+      }
+    }
+  }else if( n.getKind()==FORALL && d_quant_macros.find( n )==d_quant_macros.end() ){
+    std::vector< Node > args;
+    for( size_t j=0; j<n[0].getNumChildren(); j++ ){
+      args.push_back( n[0][j] );
+    }
+    Node nproc = n[1];
+    if( !d_macro_defs_new.empty() ){
+      nproc = simplify( nproc );
+      if( nproc!=n[1] ){
+        nproc = Rewriter::rewrite( nproc );
+      }
+    }
+    //look at the body of the quantifier for macro definition
+    if( process( nproc, true, args, n ) ){
+      d_quant_macros[n] = true;
+      return true;
+    }
+  }
+  return false;
+}
+
+bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()==APPLY_UF ){
+      Node nop = n.getOperator();
+      if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end()  ){
+        return true;
+      }
+      if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
+        opc.push_back( nop );
+      }
+    }else if( d_ground_macros && n.getKind()==FORALL ){
+      return true;
+    }
+    for( size_t i=0; i<n.getNumChildren(); i++ ){
+      if( containsBadOp( n[i], op, opc, visited ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
+  return pol && n.getKind()==EQUAL;
+}
+
+bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
+  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);
+  Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
+  std::vector< Node > trigger_var;
+  inst::Trigger::getTriggerVariables( icn, f, trigger_var );
+  Trace("macros-debug2") << "Done." << std::endl;
+  //only if all variables are also trigger variables
+  return trigger_var.size()>=var.size();
+}
+
+bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
+  Assert( n.getKind()==APPLY_UF );
+  TypeNode tno = n.getOperator().getType();
+  std::map< Node, bool > vars;
+  // allow if a vector of unique variables of the same type as UF arguments
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    if( n[i].getKind()!=BOUND_VARIABLE ){
+      return false;
+    }
+    if( n[i].getType()!=tno[i] ){
+      return false;
+    }
+    if( vars.find( n[i] )==vars.end() ){
+      vars[n[i]] = true;
+    }else{
+      return false;
+    }
+  }
+  return true;
+}
+
+void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()==APPLY_UF ){
+      if( isBoundVarApplyUf( n ) ){
+        candidates.push_back( n );
+      }
+    }else if( n.getKind()==PLUS ){
+      for( size_t i=0; i<n.getNumChildren(); i++ ){
+        getMacroCandidates( n[i], candidates, visited );
+      }
+    }else if( n.getKind()==MULT ){
+      //if the LHS is a constant
+      if( n.getNumChildren()==2 && n[0].isConst() ){
+        getMacroCandidates( n[1], candidates, visited );
+      }
+    }else if( n.getKind()==NOT ){
+      getMacroCandidates( n[0], candidates, visited );
+    }
+  }
+}
+
+Node QuantifierMacros::solveInEquality( Node n, Node lit ){
+  if( lit.getKind()==EQUAL ){
+    //return the opposite side of the equality if defined that way
+    for( int i=0; i<2; i++ ){
+      if( lit[i]==n ){
+        return lit[i==0 ? 1 : 0];
+      }else if( lit[i].getKind()==NOT && lit[i][0]==n ){
+        return lit[i==0 ? 1 : 0].negate();
+      }
+    }
+    std::map<Node, Node> msum;
+    if (ArithMSum::getMonomialSumLit(lit, msum))
+    {
+      Node veq_c;
+      Node val;
+      int res = ArithMSum::isolate(n, msum, veq_c, val, EQUAL);
+      if (res != 0 && veq_c.isNull())
+      {
+        return val;
+      }
+    }
+  }
+  Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl;
+  return Node::null();
+}
+
+bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){
+      if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
+        if( retOnly ){
+          return true;
+        }else{
+          vars.push_back( n );
+        }
+      }
+    }
+    for( size_t i=0; i<n.getNumChildren(); i++ ){
+      if( getFreeVariables( n[i], v_quant, vars, retOnly, visited ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
+                                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){
+  bool success = true;
+  for( size_t a=0; a<v_quant.size(); a++ ){
+    if( !solved[ v_quant[a] ].isNull() ){
+      vars.push_back( v_quant[a] );
+      subs.push_back( solved[ v_quant[a] ] );
+    }else{
+      if( reqComplete ){
+        success = false;
+        break;
+      }
+    }
+  }
+  return success;
+}
+
+bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
+  Trace("macros-debug") << "  process " << n << std::endl;
+  if( n.getKind()==NOT ){
+    return process( n[0], !pol, args, f );
+  }else if( n.getKind()==AND || n.getKind()==OR ){
+    //bool favorPol = (n.getKind()==AND)==pol;
+    //conditional?
+  }else if( n.getKind()==ITE ){
+    //can not do anything
+  }else if( n.getKind()==APPLY_UF ){
+    //predicate case
+    if( isBoundVarApplyUf( n ) ){
+      Node op = n.getOperator();
+      if( d_macro_defs.find( op )==d_macro_defs.end() ){
+        Node n_def = NodeManager::currentNM()->mkConst( pol );
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          std::stringstream ss;
+          ss << "mda_" << op << "";
+          Node v = NodeManager::currentNM()->mkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" );
+          d_macro_basis[op].push_back( v );
+        }
+        //contains no ops
+        std::vector< Node > op_contains;
+        //add the macro
+        addMacro( op, n_def, op_contains );
+        return true;
+      }
+    }
+  }else{
+    //literal case
+    if( isMacroLiteral( n, pol ) ){
+      Trace("macros-debug") << "Check macro literal : " << n << std::endl;
+      std::map< Node, bool > visited;
+      std::vector< Node > candidates;
+      for( size_t i=0; i<n.getNumChildren(); i++ ){
+        getMacroCandidates( n[i], candidates, visited );
+      }
+      for( size_t i=0; i<candidates.size(); i++ ){
+        Node m = candidates[i];
+        Node op = m.getOperator();
+        Trace("macros-debug") << "Check macro candidate : " << m << std::endl;
+        if( d_macro_defs.find( op )==d_macro_defs.end() ){
+          std::vector< Node > fvs;
+          visited.clear();
+          getFreeVariables( m, args, fvs, false, visited );
+          //get definition and condition
+          Node n_def = solveInEquality( m, n ); //definition for the macro
+          if( !n_def.isNull() ){
+            Trace("macros-debug") << m << " is possible macro in " << f << std::endl;
+            Trace("macros-debug") << "  corresponding definition is : " << n_def << std::endl;
+            visited.clear();
+            //definition must exist and not contain any free variables apart from fvs
+            if( !getFreeVariables( n_def, args, fvs, true, visited ) ){
+              Trace("macros-debug") << "...free variables are contained." << std::endl;
+              visited.clear();
+              //cannot contain a defined operator, opc is list of functions it contains
+              std::vector< Node > opc;
+              if( !containsBadOp( n_def, op, opc, visited ) ){
+                Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl;
+                //must be ground UF term if mode is GROUND_UF
+                if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){
+                  Trace("macros-debug") << "...respects ground-uf constraint." << std::endl;
+                  //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
+                  // x1 ... xn are distinct variables
+                  if( d_macro_basis[op].empty() ){
+                    for( size_t a=0; a<m.getNumChildren(); a++ ){
+                      std::stringstream ss;
+                      ss << "mda_" << op << "";
+                      Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
+                      d_macro_basis[op].push_back( v );
+                    }
+                  }
+                  std::map< Node, Node > solved;
+                  for( size_t a=0; a<m.getNumChildren(); a++ ){
+                    solved[m[a]] = d_macro_basis[op][a];
+                  }
+                  std::vector< Node > vars;
+                  std::vector< Node > subs;
+                  if( getSubstitution( fvs, solved, vars, subs, true ) ){
+                    n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+                    addMacro( op, n_def, opc );
+                    return true;
+                  }
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  return false;
+}
+
+Node QuantifierMacros::simplify( Node n ){
+  if( n.getNumChildren()==0 ){
+    return n;
+  }else{
+    std::map< Node, Node >::iterator itn = d_simplify_cache.find( n );
+    if( itn!=d_simplify_cache.end() ){
+      return itn->second;
+    }else{
+      Node ret = n;
+      Trace("macros-debug") << "  simplify " << n << std::endl;
+      std::vector< Node > children;
+      bool childChanged = false;
+      for( size_t i=0; i<n.getNumChildren(); i++ ){
+        Node nn = simplify( n[i] );
+        children.push_back( nn );
+        childChanged = childChanged || nn!=n[i];
+      }
+      bool retSet = false;
+      if( n.getKind()==APPLY_UF ){
+        Node op = n.getOperator();
+        std::map< Node, Node >::iterator it = d_macro_defs.find( op );
+        if( it!=d_macro_defs.end() && !it->second.isNull() ){
+          //only apply if children are subtypes of arguments
+          bool success = true;
+          // FIXME : this can be eliminated when we have proper typing rules
+          std::vector< Node > cond;
+          TypeNode tno = op.getType();
+          for( unsigned i=0; i<children.size(); i++ ){
+            Node etc = TypeNode::getEnsureTypeCondition( children[i], tno[i] );
+            if( etc.isNull() ){
+              //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op, 
+              //  and not ensuring it applies to n when its types are correct.
+              //Assert( false );
+              success = false;
+              break;
+            }else if( !etc.isConst() ){
+              cond.push_back( etc );
+            }
+            Assert( children[i].getType().isSubtypeOf( tno[i] ) );
+          }
+          if( success ){
+            //do substitution if necessary
+            ret = it->second;
+            std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op );
+            if( itb!=d_macro_basis.end() ){
+              ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() );
+            }
+            if( !cond.empty() ){
+              Node cc = cond.size()==1 ? cond[0] : NodeManager::currentNM()->mkNode( kind::AND, cond );
+              ret = NodeManager::currentNM()->mkNode( kind::ITE, cc, ret, n );
+            }
+            retSet = true;
+          }
+        }
+      }
+      if( !retSet && childChanged ){
+        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.insert( children.begin(), n.getOperator() );
+        }
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+      d_simplify_cache[n] = ret;
+      return ret;
+    }
+  }
+}
+
+void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) {
+  //for debugging, ensure that all previous definitions have been eliminated
+  if( n.getKind()==APPLY_UF ){
+    Node op = n.getOperator();
+    if( d_macro_defs.find( op )!=d_macro_defs.end() ){
+      if( d_macro_defs.find( oo )!=d_macro_defs.end() ){
+        Trace("macros-warn") << "BAD DEFINITION for macro " << oo << " : " << d_macro_defs[oo] << std::endl;
+      }else{
+        Trace("macros-warn") << "BAD ASSERTION " << oo << std::endl;
+      }
+      Trace("macros-warn") << "  contains defined function " << op << "!!!" << std::endl;
+    }
+  }
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    debugMacroDefinition( oo, n[i] );
+  }
+}
+
+void QuantifierMacros::finalizeDefinitions() {
+  bool doDefs = false;
+  if( Trace.isOn("macros-warn") ){
+    doDefs = true;
+  }
+  if( options::incrementalSolving() || options::produceModels() || doDefs ){
+    Trace("macros") << "Store as defined functions..." << std::endl;
+    //also store as defined functions
+    for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
+      Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
+      Trace("macros-def") << "  basis is : ";
+      std::vector< Node > nargs;
+      std::vector< Expr > args;
+      for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
+        Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
+        Trace("macros-def") << d_macro_basis[it->first][i] << " ";
+        nargs.push_back( bv );
+        args.push_back( bv.toExpr() );
+      }
+      Trace("macros-def") << std::endl;
+      Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
+      smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() );
+
+      if( Trace.isOn("macros-warn") ){
+        debugMacroDefinition( it->first, sbody );
+      }
+    }
+    Trace("macros") << "done." << std::endl;
+  }
+}
+
+void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
+  Trace("macros") << "* " << n << " is a macro for " << op << ", #op contain = " << opc.size() << std::endl;
+  d_simplify_cache.clear();
+  d_macro_defs[op] = n;
+  d_macro_defs_new[op] = n;
+  //substitute into all previous
+  std::vector< Node > dep_ops;
+  dep_ops.push_back( op );
+  Trace("macros-debug") << "...substitute into " << d_macro_def_contains[op].size() << " previous definitions." << std::endl;
+  for( unsigned i=0; i<d_macro_def_contains[op].size(); i++ ){
+    Node cop = d_macro_def_contains[op][i];
+    Node def = d_macro_defs[cop];
+    def = simplify( def );
+    d_macro_defs[cop] = def;
+    if( d_macro_defs_new.find( cop )!=d_macro_defs_new.end() ){
+      d_macro_defs_new[cop] = def;
+    }
+    dep_ops.push_back( cop );
+  }
+  //store the contains op information
+  for( unsigned i=0; i<opc.size(); i++ ){
+    for( unsigned j=0; j<dep_ops.size(); j++ ){
+      Node dop = dep_ops[j];
+      if( std::find( d_macro_def_contains[opc[i]].begin(), d_macro_def_contains[opc[i]].end(), dop )==d_macro_def_contains[opc[i]].end() ){
+        d_macro_def_contains[opc[i]].push_back( dop );
+      }
+    }
+  }
+}
+
+}  // 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.cpp b/src/theory/quantifiers/macros.cpp
deleted file mode 100644
index d88f8eec9..000000000
--- a/src/theory/quantifiers/macros.cpp
+++ /dev/null
@@ -1,514 +0,0 @@
-/*********************                                                        */
-/*! \file macros.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Kshitij Bansal
- ** 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 Sort inference module
- **
- ** This class implements quantifiers macro definitions.
- **/
-
-#include "theory/quantifiers/macros.h"
-
-#include <vector>
-
-#include "options/quantifiers_modes.h"
-#include "options/quantifiers_options.h"
-#include "proof/proof_manager.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/ematching/trigger.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/rewriter.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-
-QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){
-  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++ ){
-    d_ground_macros = (r==0);
-    Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
-    //first, collect macro definitions
-    std::vector< Node > macro_assertions;
-    for( int i=0; i<(int)assertions.size(); i++ ){
-      Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
-      if( processAssertion( assertions[i] ) ){
-        PROOF( 
-          if( std::find( macro_assertions.begin(), macro_assertions.end(), assertions[i] )==macro_assertions.end() ){
-            macro_assertions.push_back( assertions[i] );
-          }
-        );
-        //process this assertion again
-        i--;
-      }
-    }
-    Trace("macros") << "...finished process, #new def = " << d_macro_defs_new.size() << std::endl;
-    if( doRewrite && !d_macro_defs_new.empty() ){
-      bool retVal = false;
-      Trace("macros") << "Do simplifications..." << std::endl;
-      //now, rewrite based on macro definitions
-      for( unsigned i=0; i<assertions.size(); i++ ){
-        Node curr = simplify( assertions[i] );
-        if( curr!=assertions[i] ){
-          curr = Rewriter::rewrite( curr );
-          Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
-          //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]);
-              }
-            }
-          );
-          assertions[i] = curr;
-          retVal = true;
-        }
-      }
-      d_macro_defs_new.clear();
-      if( retVal ){
-        return true;
-      }
-    }
-  }
-  if( Trace.isOn("macros-warn") ){
-    for( unsigned i=0; i<assertions.size(); i++ ){
-      debugMacroDefinition( assertions[i], assertions[i] );
-    }
-  }
-  return false;
-}
-
-bool QuantifierMacros::processAssertion( Node n ) {
-  if( n.getKind()==AND ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( processAssertion( n[i] ) ){
-        return true;
-      }
-    }
-  }else if( n.getKind()==FORALL && d_quant_macros.find( n )==d_quant_macros.end() ){
-    std::vector< Node > args;
-    for( size_t j=0; j<n[0].getNumChildren(); j++ ){
-      args.push_back( n[0][j] );
-    }
-    Node nproc = n[1];
-    if( !d_macro_defs_new.empty() ){
-      nproc = simplify( nproc );
-      if( nproc!=n[1] ){
-        nproc = Rewriter::rewrite( nproc );
-      }
-    }
-    //look at the body of the quantifier for macro definition
-    if( process( nproc, true, args, n ) ){
-      d_quant_macros[n] = true;
-      return true;
-    }
-  }
-  return false;
-}
-
-bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ){
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    if( n.getKind()==APPLY_UF ){
-      Node nop = n.getOperator();
-      if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end()  ){
-        return true;
-      }
-      if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
-        opc.push_back( nop );
-      }
-    }else if( d_ground_macros && n.getKind()==FORALL ){
-      return true;
-    }
-    for( size_t i=0; i<n.getNumChildren(); i++ ){
-      if( containsBadOp( n[i], op, opc, visited ) ){
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
-  return pol && n.getKind()==EQUAL;
-}
-
-bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
-  Node icn = d_qe->getTermUtil()->substituteBoundVariablesToInstConstants(n, f);
-  Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
-  std::vector< Node > var;
-  quantifiers::TermUtil::computeInstConstContainsForQuant(f, icn, var);
-  Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
-  std::vector< Node > trigger_var;
-  inst::Trigger::getTriggerVariables( icn, f, trigger_var );
-  Trace("macros-debug2") << "Done." << std::endl;
-  //only if all variables are also trigger variables
-  return trigger_var.size()>=var.size();
-}
-
-bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
-  Assert( n.getKind()==APPLY_UF );
-  TypeNode tno = n.getOperator().getType();
-  std::map< Node, bool > vars;
-  // allow if a vector of unique variables of the same type as UF arguments
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    if( n[i].getKind()!=BOUND_VARIABLE ){
-      return false;
-    }
-    if( n[i].getType()!=tno[i] ){
-      return false;
-    }
-    if( vars.find( n[i] )==vars.end() ){
-      vars[n[i]] = true;
-    }else{
-      return false;
-    }
-  }
-  return true;
-}
-
-void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ){
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    if( n.getKind()==APPLY_UF ){
-      if( isBoundVarApplyUf( n ) ){
-        candidates.push_back( n );
-      }
-    }else if( n.getKind()==PLUS ){
-      for( size_t i=0; i<n.getNumChildren(); i++ ){
-        getMacroCandidates( n[i], candidates, visited );
-      }
-    }else if( n.getKind()==MULT ){
-      //if the LHS is a constant
-      if( n.getNumChildren()==2 && n[0].isConst() ){
-        getMacroCandidates( n[1], candidates, visited );
-      }
-    }else if( n.getKind()==NOT ){
-      getMacroCandidates( n[0], candidates, visited );
-    }
-  }
-}
-
-Node QuantifierMacros::solveInEquality( Node n, Node lit ){
-  if( lit.getKind()==EQUAL ){
-    //return the opposite side of the equality if defined that way
-    for( int i=0; i<2; i++ ){
-      if( lit[i]==n ){
-        return lit[i==0 ? 1 : 0];
-      }else if( lit[i].getKind()==NOT && lit[i][0]==n ){
-        return lit[i==0 ? 1 : 0].negate();
-      }
-    }
-    std::map<Node, Node> msum;
-    if (ArithMSum::getMonomialSumLit(lit, msum))
-    {
-      Node veq_c;
-      Node val;
-      int res = ArithMSum::isolate(n, msum, veq_c, val, EQUAL);
-      if (res != 0 && veq_c.isNull())
-      {
-        return val;
-      }
-    }
-  }
-  Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl;
-  return Node::null();
-}
-
-bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ){
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){
-      if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
-        if( retOnly ){
-          return true;
-        }else{
-          vars.push_back( n );
-        }
-      }
-    }
-    for( size_t i=0; i<n.getNumChildren(); i++ ){
-      if( getFreeVariables( n[i], v_quant, vars, retOnly, visited ) ){
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
-                                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){
-  bool success = true;
-  for( size_t a=0; a<v_quant.size(); a++ ){
-    if( !solved[ v_quant[a] ].isNull() ){
-      vars.push_back( v_quant[a] );
-      subs.push_back( solved[ v_quant[a] ] );
-    }else{
-      if( reqComplete ){
-        success = false;
-        break;
-      }
-    }
-  }
-  return success;
-}
-
-bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
-  Trace("macros-debug") << "  process " << n << std::endl;
-  if( n.getKind()==NOT ){
-    return process( n[0], !pol, args, f );
-  }else if( n.getKind()==AND || n.getKind()==OR ){
-    //bool favorPol = (n.getKind()==AND)==pol;
-    //conditional?
-  }else if( n.getKind()==ITE ){
-    //can not do anything
-  }else if( n.getKind()==APPLY_UF ){
-    //predicate case
-    if( isBoundVarApplyUf( n ) ){
-      Node op = n.getOperator();
-      if( d_macro_defs.find( op )==d_macro_defs.end() ){
-        Node n_def = NodeManager::currentNM()->mkConst( pol );
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          std::stringstream ss;
-          ss << "mda_" << op << "";
-          Node v = NodeManager::currentNM()->mkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" );
-          d_macro_basis[op].push_back( v );
-        }
-        //contains no ops
-        std::vector< Node > op_contains;
-        //add the macro
-        addMacro( op, n_def, op_contains );
-        return true;
-      }
-    }
-  }else{
-    //literal case
-    if( isMacroLiteral( n, pol ) ){
-      Trace("macros-debug") << "Check macro literal : " << n << std::endl;
-      std::map< Node, bool > visited;
-      std::vector< Node > candidates;
-      for( size_t i=0; i<n.getNumChildren(); i++ ){
-        getMacroCandidates( n[i], candidates, visited );
-      }
-      for( size_t i=0; i<candidates.size(); i++ ){
-        Node m = candidates[i];
-        Node op = m.getOperator();
-        Trace("macros-debug") << "Check macro candidate : " << m << std::endl;
-        if( d_macro_defs.find( op )==d_macro_defs.end() ){
-          std::vector< Node > fvs;
-          visited.clear();
-          getFreeVariables( m, args, fvs, false, visited );
-          //get definition and condition
-          Node n_def = solveInEquality( m, n ); //definition for the macro
-          if( !n_def.isNull() ){
-            Trace("macros-debug") << m << " is possible macro in " << f << std::endl;
-            Trace("macros-debug") << "  corresponding definition is : " << n_def << std::endl;
-            visited.clear();
-            //definition must exist and not contain any free variables apart from fvs
-            if( !getFreeVariables( n_def, args, fvs, true, visited ) ){
-              Trace("macros-debug") << "...free variables are contained." << std::endl;
-              visited.clear();
-              //cannot contain a defined operator, opc is list of functions it contains
-              std::vector< Node > opc;
-              if( !containsBadOp( n_def, op, opc, visited ) ){
-                Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl;
-                //must be ground UF term if mode is GROUND_UF
-                if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){
-                  Trace("macros-debug") << "...respects ground-uf constraint." << std::endl;
-                  //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
-                  // x1 ... xn are distinct variables
-                  if( d_macro_basis[op].empty() ){
-                    for( size_t a=0; a<m.getNumChildren(); a++ ){
-                      std::stringstream ss;
-                      ss << "mda_" << op << "";
-                      Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
-                      d_macro_basis[op].push_back( v );
-                    }
-                  }
-                  std::map< Node, Node > solved;
-                  for( size_t a=0; a<m.getNumChildren(); a++ ){
-                    solved[m[a]] = d_macro_basis[op][a];
-                  }
-                  std::vector< Node > vars;
-                  std::vector< Node > subs;
-                  if( getSubstitution( fvs, solved, vars, subs, true ) ){
-                    n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-                    addMacro( op, n_def, opc );
-                    return true;
-                  }
-                }
-              }
-            }
-          }
-        }
-      }
-    }
-  }
-  return false;
-}
-
-Node QuantifierMacros::simplify( Node n ){
-  if( n.getNumChildren()==0 ){
-    return n;
-  }else{
-    std::map< Node, Node >::iterator itn = d_simplify_cache.find( n );
-    if( itn!=d_simplify_cache.end() ){
-      return itn->second;
-    }else{
-      Node ret = n;
-      Trace("macros-debug") << "  simplify " << n << std::endl;
-      std::vector< Node > children;
-      bool childChanged = false;
-      for( size_t i=0; i<n.getNumChildren(); i++ ){
-        Node nn = simplify( n[i] );
-        children.push_back( nn );
-        childChanged = childChanged || nn!=n[i];
-      }
-      bool retSet = false;
-      if( n.getKind()==APPLY_UF ){
-        Node op = n.getOperator();
-        std::map< Node, Node >::iterator it = d_macro_defs.find( op );
-        if( it!=d_macro_defs.end() && !it->second.isNull() ){
-          //only apply if children are subtypes of arguments
-          bool success = true;
-          // FIXME : this can be eliminated when we have proper typing rules
-          std::vector< Node > cond;
-          TypeNode tno = op.getType();
-          for( unsigned i=0; i<children.size(); i++ ){
-            Node etc = TypeNode::getEnsureTypeCondition( children[i], tno[i] );
-            if( etc.isNull() ){
-              //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op, 
-              //  and not ensuring it applies to n when its types are correct.
-              //Assert( false );
-              success = false;
-              break;
-            }else if( !etc.isConst() ){
-              cond.push_back( etc );
-            }
-            Assert( children[i].getType().isSubtypeOf( tno[i] ) );
-          }
-          if( success ){
-            //do substitution if necessary
-            ret = it->second;
-            std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op );
-            if( itb!=d_macro_basis.end() ){
-              ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() );
-            }
-            if( !cond.empty() ){
-              Node cc = cond.size()==1 ? cond[0] : NodeManager::currentNM()->mkNode( kind::AND, cond );
-              ret = NodeManager::currentNM()->mkNode( kind::ITE, cc, ret, n );
-            }
-            retSet = true;
-          }
-        }
-      }
-      if( !retSet && childChanged ){
-        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-          children.insert( children.begin(), n.getOperator() );
-        }
-        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-      d_simplify_cache[n] = ret;
-      return ret;
-    }
-  }
-}
-
-void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) {
-  //for debugging, ensure that all previous definitions have been eliminated
-  if( n.getKind()==APPLY_UF ){
-    Node op = n.getOperator();
-    if( d_macro_defs.find( op )!=d_macro_defs.end() ){
-      if( d_macro_defs.find( oo )!=d_macro_defs.end() ){
-        Trace("macros-warn") << "BAD DEFINITION for macro " << oo << " : " << d_macro_defs[oo] << std::endl;
-      }else{
-        Trace("macros-warn") << "BAD ASSERTION " << oo << std::endl;
-      }
-      Trace("macros-warn") << "  contains defined function " << op << "!!!" << std::endl;
-    }
-  }
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    debugMacroDefinition( oo, n[i] );
-  }
-}
-
-void QuantifierMacros::finalizeDefinitions() {
-  bool doDefs = false;
-  if( Trace.isOn("macros-warn") ){
-    doDefs = true;
-  }
-  if( options::incrementalSolving() || options::produceModels() || doDefs ){
-    Trace("macros") << "Store as defined functions..." << std::endl;
-    //also store as defined functions
-    for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
-      Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
-      Trace("macros-def") << "  basis is : ";
-      std::vector< Node > nargs;
-      std::vector< Expr > args;
-      for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
-        Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
-        Trace("macros-def") << d_macro_basis[it->first][i] << " ";
-        nargs.push_back( bv );
-        args.push_back( bv.toExpr() );
-      }
-      Trace("macros-def") << std::endl;
-      Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
-      smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() );
-
-      if( Trace.isOn("macros-warn") ){
-        debugMacroDefinition( it->first, sbody );
-      }
-    }
-    Trace("macros") << "done." << std::endl;
-  }
-}
-
-void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
-  Trace("macros") << "* " << n << " is a macro for " << op << ", #op contain = " << opc.size() << std::endl;
-  d_simplify_cache.clear();
-  d_macro_defs[op] = n;
-  d_macro_defs_new[op] = n;
-  //substitute into all previous
-  std::vector< Node > dep_ops;
-  dep_ops.push_back( op );
-  Trace("macros-debug") << "...substitute into " << d_macro_def_contains[op].size() << " previous definitions." << std::endl;
-  for( unsigned i=0; i<d_macro_def_contains[op].size(); i++ ){
-    Node cop = d_macro_def_contains[op][i];
-    Node def = d_macro_defs[cop];
-    def = simplify( def );
-    d_macro_defs[cop] = def;
-    if( d_macro_defs_new.find( cop )!=d_macro_defs_new.end() ){
-      d_macro_defs_new[cop] = def;
-    }
-    dep_ops.push_back( cop );
-  }
-  //store the contains op information
-  for( unsigned i=0; i<opc.size(); i++ ){
-    for( unsigned j=0; j<dep_ops.size(); j++ ){
-      Node dop = dep_ops[j];
-      if( std::find( d_macro_def_contains[opc[i]].begin(), d_macro_def_contains[opc[i]].end(), dop )==d_macro_def_contains[opc[i]].end() ){
-        d_macro_def_contains[opc[i]].push_back( dop );
-      }
-    }
-  }
-}
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