Fully incorporate quantifiers macros into ppAssert / non-clausal simplification (#6394)

This PR removes the quantifiers macro preprocessing pass, which had several shortcomings, both in terms of performance and features.

This makes it so that quantifier macros are the (optional) implementation of TheoryQuantifiers::ppAssert.

In other words, quantifiers can now be put into "solved form", forall x. P(x) ---> P = lambda x. true.

This is part of an effort to improve proofs for preprocessing, as well as centralizing our reason about substitutions for the sake of efficiency.

12 files changed, 423 insertions, 503 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 81105e817..b86435eb7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -82,8 +82,6 @@ libcvc4_add_sources(
   preprocessing/passes/non_clausal_simp.h
   preprocessing/passes/pseudo_boolean_processor.cpp
   preprocessing/passes/pseudo_boolean_processor.h
-  preprocessing/passes/quantifier_macros.cpp
-  preprocessing/passes/quantifier_macros.h
   preprocessing/passes/quantifiers_preprocess.cpp
   preprocessing/passes/quantifiers_preprocess.h
   preprocessing/passes/real_to_int.cpp
@@ -755,6 +753,8 @@ libcvc4_add_sources(
   theory/quantifiers/quantifiers_attributes.h
   theory/quantifiers/quantifiers_inference_manager.cpp
   theory/quantifiers/quantifiers_inference_manager.h
+  theory/quantifiers/quantifiers_macros.cpp
+  theory/quantifiers/quantifiers_macros.h
   theory/quantifiers/quantifiers_modules.cpp
   theory/quantifiers/quantifiers_modules.h
   theory/quantifiers/quantifiers_registry.cpp
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
deleted file mode 100644
index 952ced4d5..000000000
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ /dev/null
@@ -1,406 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Yoni Zohar, Haniel Barbosa
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Sort inference module.
- *
- * This class implements quantifiers macro definitions.
- */
-
-#include "preprocessing/passes/quantifier_macros.h"
-
-#include <vector>
-
-#include "expr/node_algorithm.h"
-#include "expr/skolem_manager.h"
-#include "options/quantifiers_options.h"
-#include "options/smt_options.h"
-#include "preprocessing/assertion_pipeline.h"
-#include "preprocessing/preprocessing_pass_context.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/pattern_term_selector.h"
-#include "theory/quantifiers/quantifiers_registry.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/rewriter.h"
-#include "theory/theory_engine.h"
-
-using namespace std;
-using namespace cvc5::theory;
-using namespace cvc5::theory::quantifiers;
-using namespace cvc5::kind;
-
-namespace cvc5 {
-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);
-  } while (success);
-  finalizeDefinitions();
-  clearMaps();
-  return PreprocessingPassResult::NO_CONFLICT;
-}
-
-void QuantifierMacros::clearMaps()
-{
-  d_macroDefs.clear();
-  d_macroDefsNew.clear();
-  d_quant_macros.clear();
-  d_ground_macros = false;
-}
-
-bool QuantifierMacros::simplify(AssertionPipeline* ap)
-{
-  const std::vector<Node>& assertions = ap->ref();
-  unsigned rmax =
-      options::macrosQuantMode() == options::MacrosQuantMode::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] ) ){
-        if (options::unsatCores()
-            && 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_macroDefsNew.size() << std::endl;
-    if (!d_macroDefsNew.empty())
-    {
-      bool retVal = false;
-      Trace("macros") << "Do simplifications..." << std::endl;
-      //now, rewrite based on macro definitions
-      for (size_t i = 0, nassert = assertions.size(); i < nassert; i++)
-      {
-        Node curr = assertions[i].substitute(d_macroDefsNew.begin(),
-                                             d_macroDefsNew.end());
-        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.
-          if (options::unsatCores())
-          {
-            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]);
-              }
-            }
-          }
-          ap->replace(i, curr);
-          retVal = true;
-        }
-      }
-      d_macroDefsNew.clear();
-      if( retVal ){
-        return true;
-      }
-    }
-  }
-  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(n[0].begin(), n[0].end());
-    Node nproc = n[1];
-    if (!d_macroDefsNew.empty())
-    {
-      nproc = nproc.substitute(d_macroDefsNew.begin(), d_macroDefsNew.end());
-      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_macroDefs.find(nop) != d_macroDefs.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::isGroundUfTerm(Node q, Node n)
-{
-  Node icn = d_preprocContext->getTheoryEngine()
-                 ->getQuantifiersEngine()
-                 ->getQuantifiersRegistry()
-                 .substituteBoundVariablesToInstConstants(n, q);
-  Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
-  std::vector< Node > var;
-  quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var);
-  Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
-  std::vector< Node > trigger_var;
-  inst::PatternTermSelector::getTriggerVariables(icn, q, 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 (size_t i = 0, nchild = n.getNumChildren(); i < nchild; 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::process( Node n, bool pol, std::vector< Node >& args, Node f ){
-  Trace("macros-debug") << "  process " << n << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  if( n.getKind()==NOT ){
-    return process( n[0], !pol, args, f );
-  }else if( n.getKind()==APPLY_UF ){
-    //predicate case
-    if( isBoundVarApplyUf( n ) ){
-      Node op = n.getOperator();
-      if (d_macroDefs.find(op) == d_macroDefs.end())
-      {
-        Node n_def = nm->mkConst(pol);
-        //add the macro
-        return addMacroEq(n, n_def);
-      }
-    }
-  }
-  else if (pol && n.getKind() == EQUAL)
-  {
-    //literal case
-    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 (const Node& m : candidates)
-    {
-      Node op = m.getOperator();
-      Trace("macros-debug") << "Check macro candidate : " << m << std::endl;
-      if (d_macroDefs.find(op) != d_macroDefs.end())
-      {
-        continue;
-      }
-      // get definition and condition
-      Node n_def = solveInEquality(m, n);  // definition for the macro
-      if (n_def.isNull())
-      {
-        continue;
-      }
-      Trace("macros-debug") << m << " is possible macro in " << f << std::endl;
-      Trace("macros-debug")
-          << "  corresponding definition is : " << n_def << 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() != options::MacrosQuantMode::GROUND_UF
-            || isGroundUfTerm(f, n_def))
-        {
-          Trace("macros-debug")
-              << "...respects ground-uf constraint." << std::endl;
-          if (addMacroEq(m, n_def))
-          {
-            return true;
-          }
-        }
-      }
-    }
-  }
-  return false;
-}
-
-void QuantifierMacros::finalizeDefinitions() {
-  if (options::incrementalSolving() || options::produceModels())
-  {
-    Trace("macros-def") << "Store as defined functions..." << std::endl;
-    //also store as defined functions
-    SmtEngine* smt = d_preprocContext->getSmt();
-    for (const std::pair<const Node, Node>& m : d_macroDefs)
-    {
-      Trace("macros-def") << "Macro definition for " << m.first << " : "
-                          << m.second << std::endl;
-      Trace("macros-def") << "  basis is : ";
-      std::vector<Node> args(m.second[0].begin(), m.second[0].end());
-      Node sbody = m.second[1];
-      smt->defineFunction(m.first, args, sbody);
-    }
-    Trace("macros-def") << "done." << std::endl;
-  }
-}
-
-bool QuantifierMacros::addMacroEq(Node n, Node ndef)
-{
-  Assert(n.getKind() == APPLY_UF);
-  NodeManager* nm = NodeManager::currentNM();
-  Trace("macros-debug") << "Add macro eq for " << n << std::endl;
-  Trace("macros-debug") << "  def: " << ndef << std::endl;
-  std::vector<Node> vars;
-  std::vector<Node> fvars;
-  for (const Node& nc : n)
-  {
-    vars.push_back(nc);
-    Node v = nm->mkBoundVar(nc.getType());
-    fvars.push_back(v);
-  }
-  Node fdef =
-      ndef.substitute(vars.begin(), vars.end(), fvars.begin(), fvars.end());
-  fdef = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, fvars), fdef);
-  // If the definition has a free variable, it is malformed. This can happen
-  // if the right hand side of a macro definition contains a variable not
-  // contained in the left hand side
-  if (expr::hasFreeVar(fdef))
-  {
-    return false;
-  }
-  TNode op = n.getOperator();
-  TNode fdeft = fdef;
-  for (std::pair<const Node, Node>& prev : d_macroDefsNew)
-  {
-    d_macroDefsNew[prev.first] = prev.second.substitute(op, fdeft);
-  }
-  Assert(op.getType().isComparableTo(fdef.getType()));
-  d_macroDefs[op] = fdef;
-  d_macroDefsNew[op] = fdef;
-  Trace("macros") << "(macro " << op << " " << fdef[0] << " " << fdef[1] << ")"
-                  << std::endl;
-  return true;
-}
-
-}  // passes
-}  // preprocessing
-}  // namespace cvc5
diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
deleted file mode 100644
index b856222f8..000000000
--- a/src/preprocessing/passes/quantifier_macros.h
+++ /dev/null
@@ -1,86 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Yoni Zohar, Andrew Reynolds, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Pre-process step for detecting quantifier macro definitions.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
-#define CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
-
-#include <map>
-#include <vector>
-#include "expr/node.h"
-#include "preprocessing/preprocessing_pass.h"
-
-namespace cvc5 {
-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 isGroundUfTerm(Node f, Node n);
-  void getMacroCandidates(Node n,
-                          std::vector<Node>& candidates,
-                          std::map<Node, bool>& visited);
-  Node solveInEquality(Node n, Node lit);
-  /**
-   * Called when we have inferred a quantified formula is of the form
-   *   forall x1 ... xn. n = ndef
-   * where n is of the form U(x1...xn). Returns true if this is a legal
-   * macro definition for U.
-   */
-  bool addMacroEq(Node n, Node ndef);
-  /**
-   * This applies macro elimination to the given pipeline, which discovers
-   * whether there are any quantified formulas corresponding to macros,
-   * and rewrites the given assertions pipeline.
-   *
-   * @param ap The pipeline to apply macros to.
-   * @return Whether new definitions were inferred and we rewrote the assertions
-   * based on them.
-   */
-  bool simplify(AssertionPipeline* ap);
-  void finalizeDefinitions();
-  void clearMaps();
-
-  /** All macros inferred by this class */
-  std::map<Node, Node> d_macroDefs;
-  /** The current list of macros inferring during a call to simplify */
-  std::map<Node, Node> d_macroDefsNew;
-  /** Map from quantified formulas to whether they are macro definitions */
-  std::map<Node, bool> d_quant_macros;
-  /** Whether we are currently limited to inferring ground macros */
-  bool d_ground_macros;
-};
-
-}  // passes
-}  // preprocessing
-}  // namespace cvc5
-
-#endif /*CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index 43acf5b17..6f846dc74 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -45,7 +45,6 @@
 #include "preprocessing/passes/nl_ext_purify.h"
 #include "preprocessing/passes/non_clausal_simp.h"
 #include "preprocessing/passes/pseudo_boolean_processor.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"
@@ -149,7 +148,6 @@ PreprocessingPassRegistry::PreprocessingPassRegistry()
   registerPassInfo("ackermann", callCtor<Ackermann>);
   registerPassInfo("ext-rew-pre", callCtor<ExtRewPre>);
   registerPassInfo("theory-preprocess", callCtor<TheoryPreprocess>);
-  registerPassInfo("quantifier-macros", callCtor<QuantifierMacros>);
   registerPassInfo("nl-ext-purify", callCtor<NlExtPurify>);
   registerPassInfo("bool-to-bv", callCtor<BoolToBV>);
   registerPassInfo("ho-elim", callCtor<HoElim>);
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 1aa46c73c..fa230cd54 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -236,11 +236,6 @@ bool ProcessAssertions::apply(Assertions& as)
   {
     // remove rewrite rules, apply pre-skolemization to existential quantifiers
     d_passes["quantifiers-preprocess"]->apply(&assertions);
-    if (options::macrosQuant())
-    {
-      // quantifiers macro expansion
-      d_passes["quantifier-macros"]->apply(&assertions);
-    }
 
     // fmf-fun : assume admissible functions, applying preprocessing reduction
     // to FMF
diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp
new file mode 100644
index 000000000..c7d74228f
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_macros.cpp
@@ -0,0 +1,283 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Yoni Zohar, Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Utility for quantifiers macro definitions.
+ */
+
+#include "theory/quantifiers/quantifiers_macros.h"
+
+#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
+#include "options/quantifiers_options.h"
+#include "proof/proof_manager.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/quantifiers_registry.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+QuantifiersMacros::QuantifiersMacros(QuantifiersRegistry& qr) : d_qreg(qr) {}
+
+Node QuantifiersMacros::solve(Node lit, bool reqGround)
+{
+  Trace("macros-debug") << "QuantifiersMacros::solve " << lit << std::endl;
+  if (lit.getKind() != FORALL)
+  {
+    return Node::null();
+  }
+  lit = lit[1];
+  bool pol = lit.getKind() != NOT;
+  Node n = pol ? lit : lit[0];
+  NodeManager* nm = NodeManager::currentNM();
+  if (n.getKind() == APPLY_UF)
+  {
+    // predicate case
+    if (isBoundVarApplyUf(n))
+    {
+      Node op = n.getOperator();
+      Node n_def = nm->mkConst(pol);
+      Node fdef = solveEq(n, n_def);
+      Assert(!fdef.isNull());
+      return fdef;
+    }
+  }
+  else if (pol && n.getKind() == EQUAL)
+  {
+    // literal case
+    Trace("macros-debug") << "Check macro literal : " << n << std::endl;
+    std::map<Node, bool> visited;
+    std::vector<Node> candidates;
+    for (const Node& nc : n)
+    {
+      getMacroCandidates(nc, candidates, visited);
+    }
+    for (const Node& m : candidates)
+    {
+      Node op = m.getOperator();
+      Trace("macros-debug") << "Check macro candidate : " << m << std::endl;
+      // get definition and condition
+      Node n_def = solveInEquality(m, n);  // definition for the macro
+      if (n_def.isNull())
+      {
+        continue;
+      }
+      Trace("macros-debug")
+          << m << " is possible macro in " << lit << std::endl;
+      Trace("macros-debug")
+          << "  corresponding definition is : " << n_def << std::endl;
+      visited.clear();
+      // cannot contain a defined operator
+      if (!containsBadOp(n_def, op, reqGround))
+      {
+        Trace("macros-debug")
+            << "...does not contain bad (recursive) operator." << std::endl;
+        // must be ground UF term if mode is GROUND_UF
+        if (options::macrosQuantMode() != options::MacrosQuantMode::GROUND_UF
+            || preservesTriggerVariables(lit, n_def))
+        {
+          Trace("macros-debug")
+              << "...respects ground-uf constraint." << std::endl;
+          Node fdef = solveEq(m, n_def);
+          if (!fdef.isNull())
+          {
+            return fdef;
+          }
+        }
+      }
+    }
+  }
+  return Node::null();
+}
+
+bool QuantifiersMacros::containsBadOp(Node n, Node op, bool reqGround)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.isClosure() && reqGround)
+      {
+        return true;
+      }
+      else if (cur == op)
+      {
+        return true;
+      }
+      else if (cur.hasOperator() && cur.getOperator() == op)
+      {
+        return true;
+      }
+      visit.insert(visit.end(), cur.begin(), cur.end());
+    }
+  } while (!visit.empty());
+  return false;
+}
+
+bool QuantifiersMacros::preservesTriggerVariables(Node q, Node n)
+{
+  Node icn = d_qreg.substituteBoundVariablesToInstConstants(n, q);
+  Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
+  std::vector<Node> var;
+  quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var);
+  Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
+  std::vector<Node> trigger_var;
+  inst::PatternTermSelector::getTriggerVariables(icn, q, trigger_var);
+  Trace("macros-debug2") << "Done." << std::endl;
+  // only if all variables are also trigger variables
+  return trigger_var.size() >= var.size();
+}
+
+bool QuantifiersMacros::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 (size_t i = 0, nchild = n.getNumChildren(); i < nchild; 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 QuantifiersMacros::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 QuantifiersMacros::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();
+}
+
+Node QuantifiersMacros::solveEq(Node n, Node ndef)
+{
+  Assert(n.getKind() == APPLY_UF);
+  NodeManager* nm = NodeManager::currentNM();
+  Trace("macros-debug") << "Add macro eq for " << n << std::endl;
+  Trace("macros-debug") << "  def: " << ndef << std::endl;
+  std::vector<Node> vars;
+  std::vector<Node> fvars;
+  for (const Node& nc : n)
+  {
+    vars.push_back(nc);
+    Node v = nm->mkBoundVar(nc.getType());
+    fvars.push_back(v);
+  }
+  Node fdef =
+      ndef.substitute(vars.begin(), vars.end(), fvars.begin(), fvars.end());
+  fdef = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, fvars), fdef);
+  // If the definition has a free variable, it is malformed. This can happen
+  // if the right hand side of a macro definition contains a variable not
+  // contained in the left hand side
+  if (expr::hasFreeVar(fdef))
+  {
+    return Node::null();
+  }
+  TNode op = n.getOperator();
+  TNode fdeft = fdef;
+  Assert(op.getType().isComparableTo(fdef.getType()));
+  return op.eqNode(fdef);
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quantifiers_macros.h b/src/theory/quantifiers/quantifiers_macros.h
new file mode 100644
index 000000000..77ce91829
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_macros.h
@@ -0,0 +1,98 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yoni Zohar, Andrew Reynolds, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Utility for detecting quantifier macro definitions.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MACROS_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MACROS_H
+
+#include <map>
+#include <vector>
+#include "expr/node.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifiersRegistry;
+
+/**
+ * A utility for inferring macros from quantified formulas. This can be seen as
+ * a method for putting quantified formulas in solved form, e.g.
+ *   forall x. P(x) ---> P = (lambda x. true)
+ */
+class QuantifiersMacros
+{
+ public:
+  QuantifiersMacros(QuantifiersRegistry& qr);
+  ~QuantifiersMacros() {}
+  /**
+   * Called on quantified formulas lit of the form
+   *   forall x1 ... xn. n = ndef
+   * where n is of the form U(x1...xn). Returns an equality of the form
+   *   U = lambda x1 ... xn. ndef
+   * if this is a legal macro definition for U, and the null node otherwise.
+   *
+   * @param lit The body of the quantified formula
+   * @param reqGround Whether we require the macro definition to be ground,
+   * i.e. does not contain quantified formulas as subterms.
+   * @return If a macro can be inferred, an equality of the form
+   * (op = lambda x1 ... xn. def)), or the null node otherwise.
+   */
+  Node solve(Node lit, bool reqGround = false);
+
+ private:
+  /**
+   * Return true n is an APPLY_UF with pairwise unique BOUND_VARIABLE as
+   * children.
+   */
+  bool isBoundVarApplyUf(Node n);
+  /**
+   * Returns true if n contains op, or if n contains a quantified formula
+   * as a subterm and reqGround is true.
+   */
+  bool containsBadOp(Node n, Node op, bool reqGround);
+  /**
+   * Return true if n preserves trigger variables in quantified formula q, that
+   * is, triggers can be inferred containing all variables in q in term n.
+   */
+  bool preservesTriggerVariables(Node q, Node n);
+  /**
+   * From n, get a list of possible subterms of n that could be the head of a
+   * macro definition.
+   */
+  void getMacroCandidates(Node n,
+                          std::vector<Node>& candidates,
+                          std::map<Node, bool>& visited);
+  /**
+   * Solve n in literal lit, return n' such that n = n' is equivalent to lit
+   * if possible, or null otherwise.
+   */
+  Node solveInEquality(Node n, Node lit);
+  /**
+   * Called when we have inferred a quantified formula is of the form
+   *   forall x1 ... xn. n = ndef
+   * where n is of the form U(x1...xn).
+   */
+  Node solveEq(Node n, Node ndef);
+  /** Reference to the quantifiers registry */
+  QuantifiersRegistry& d_qreg;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /*CVC5__THEORY__QUANTIFIERS__QUANTIFIER_MACROS_H */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index b1ea5762f..27b16e411 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -17,8 +17,10 @@
 
 #include "expr/proof_node_manager.h"
 #include "options/quantifiers_options.h"
+#include "theory/quantifiers/quantifiers_macros.h"
 #include "theory/quantifiers/quantifiers_modules.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 
 using namespace cvc5::kind;
@@ -68,6 +70,11 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
   // pointer will be retreived by TheoryEngine and set to all theories
   // post-construction.
   d_quantEngine = d_qengine.get();
+
+  if (options::macrosQuant())
+  {
+    d_qmacros.reset(new QuantifiersMacros(d_qreg));
+  }
 }
 
 TheoryQuantifiers::~TheoryQuantifiers() {
@@ -116,6 +123,26 @@ void TheoryQuantifiers::presolve() {
   }
 }
 
+Theory::PPAssertStatus TheoryQuantifiers::ppAssert(
+    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
+{
+  if (d_qmacros != nullptr)
+  {
+    bool reqGround =
+        options::macrosQuantMode() != options::MacrosQuantMode::ALL;
+    Node eq = d_qmacros->solve(tin.getProven(), reqGround);
+    if (!eq.isNull())
+    {
+      // must be legal
+      if (isLegalElimination(eq[0], eq[1]))
+      {
+        outSubstitutions.addSubstitution(eq[0], eq[1]);
+        return Theory::PP_ASSERT_STATUS_SOLVED;
+      }
+    }
+  }
+  return Theory::PP_ASSERT_STATUS_UNSOLVED;
+}
 void TheoryQuantifiers::ppNotifyAssertions(
     const std::vector<Node>& assertions) {
   Trace("quantifiers-presolve")
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index b5411aaba..544be84d6 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -33,6 +33,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
+class QuantifiersMacros;
+
 class TheoryQuantifiers : public Theory {
  public:
   TheoryQuantifiers(context::Context* c,
@@ -56,6 +58,11 @@ class TheoryQuantifiers : public Theory {
 
   void preRegisterTerm(TNode n) override;
   void presolve() override;
+  /**
+   * Preprocess assert, which solves for quantifier macros when enabled.
+   */
+  PPAssertStatus ppAssert(TrustNode tin,
+                          TrustSubstitutionMap& outSubstitutions) override;
   void ppNotifyAssertions(const std::vector<Node>& assertions) override;
   //--------------------------------- standard check
   /** Post-check, called after the fact queue of the theory is processed. */
@@ -95,6 +102,8 @@ class TheoryQuantifiers : public Theory {
   QuantifiersInferenceManager d_qim;
   /** The quantifiers engine, which lives here */
   std::unique_ptr<QuantifiersEngine> d_qengine;
+  /** The quantifiers macro module, used for ppAssert. */
+  std::unique_ptr<QuantifiersMacros> d_qmacros;
 };/* class TheoryQuantifiers */
 
 }  // namespace quantifiers
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 402cb9a3d..6793e5e02 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -715,6 +715,8 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() {
   for( std::map< Node, std::vector< Node > >::iterator it = d_uf_terms.begin(); it != d_uf_terms.end(); ++it ){
     Node n = it->first;
     Assert(!n.isNull());
+    // should not have been solved for in a substitution
+    Assert(d_substitutions.apply(n) == n);
     if( !hasAssignedFunctionDefinition( n ) ){
       Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl;
       if( options::ufHo() ){
diff --git a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
index 7993910fd..d65a92aa5 100644
--- a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
+++ b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --macros-quant
+; COMMAND-LINE: --macros-quant -q
 ; EXPECT: sat
 (set-logic AUFNIRA)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 b/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
index 34b7422a5..bdb389a63 100644
--- a/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
+++ b/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --macros-quant
+; COMMAND-LINE: --macros-quant -q
 ; EXPECT: sat
 (set-logic UFLIA)
 (declare-fun A (Int) Int)