From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 13 Apr 2021 20:38:36 +0000 (-0500)
Subject: Refactor quantifiers macros (#6348)
X-Git-Tag: cvc5-1.0.0~1914
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f7dcb4875bba33b7712732a874581639681926f8;p=cvc5.git

Refactor quantifiers macros (#6348)

This does some refactoring of quantifiers macros preprocessing pass to use up-to-date utility methods, including lambdas, substitutions, methods for getting free variables.

This is work towards adding proofs for macros.
---

diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index b3a80de2c..66837267a 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -19,6 +19,7 @@
 
 #include <vector>
 
+#include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
@@ -57,7 +58,7 @@ PreprocessingPassResult QuantifierMacros::applyInternal(
   bool success;
   do
   {
-    success = simplify(assertionsToPreprocess, true);
+    success = simplify(assertionsToPreprocess);
   } while (success);
   finalizeDefinitions();
   clearMaps();
@@ -66,16 +67,13 @@ PreprocessingPassResult QuantifierMacros::applyInternal(
 
 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_macroDefs.clear();
+  d_macroDefsNew.clear();
   d_quant_macros.clear();
   d_ground_macros = false;
 }
 
-bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
+bool QuantifierMacros::simplify(AssertionPipeline* ap)
 {
   const std::vector<Node>& assertions = ap->ref();
   unsigned rmax =
@@ -100,13 +98,17 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
         i--;
       }
     }
-    Trace("macros") << "...finished process, #new def = " << d_macro_defs_new.size() << std::endl;
-    if( doRewrite && !d_macro_defs_new.empty() ){
+    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( unsigned i=0; i<assertions.size(); i++ ){
-        Node curr = simplify( assertions[i] );
+      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;
@@ -130,17 +132,12 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
           retVal = true;
         }
       }
-      d_macro_defs_new.clear();
+      d_macroDefsNew.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;
 }
 
@@ -152,16 +149,12 @@ bool QuantifierMacros::processAssertion( Node n ) {
       }
     }
   }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] );
-    }
+    std::vector<Node> args(n[0].begin(), n[0].end());
     Node nproc = n[1];
-    if( !d_macro_defs_new.empty() ){
-      nproc = simplify( nproc );
-      if( nproc!=n[1] ){
-        nproc = Rewriter::rewrite( nproc );
-      }
+    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 ) ){
@@ -177,7 +170,8 @@ bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc,
     visited[n] = true;
     if( n.getKind()==APPLY_UF ){
       Node nop = n.getOperator();
-      if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end()  ){
+      if (nop == op || d_macroDefs.find(nop) != d_macroDefs.end())
+      {
         return true;
       }
       if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
@@ -195,10 +189,6 @@ bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc,
   return false;
 }
 
-bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
-  return pol && n.getKind()==EQUAL;
-}
-
 bool QuantifierMacros::isGroundUfTerm(Node q, Node n)
 {
   Node icn = d_preprocContext->getTheoryEngine()
@@ -221,7 +211,8 @@ bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
   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++ ){
+  for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+  {
     if( n[i].getKind()!=BOUND_VARIABLE ){
       return false;
     }
@@ -285,297 +276,131 @@ Node QuantifierMacros::solveInEquality( Node n, Node lit ){
   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;
   NodeManager* nm = NodeManager::currentNM();
-  SkolemManager* sm = nm->getSkolemManager();
   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() ){
+      if (d_macroDefs.find(op) == d_macroDefs.end())
+      {
         Node n_def = nm->mkConst(pol);
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          std::stringstream ss;
-          ss << "mda_" << op << "";
-          Node v =
-              sm->mkDummySkolem(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;
+        return addMacroEq(n, n_def);
       }
     }
-  }else{
+  }
+  else if (pol && n.getKind() == EQUAL)
+  {
     //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()
-                        != options::MacrosQuantMode::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 = sm->mkDummySkolem(
-                          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;
-                  }
-                }
-              }
-            }
-          }
-        }
-      }
+    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);
     }
-  }
-  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];
+    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;
       }
-      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.
-              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;
-          }
-        }
+      // get definition and condition
+      Node n_def = solveInEquality(m, n);  // definition for the macro
+      if (n_def.isNull())
+      {
+        continue;
       }
-      if( !retSet && childChanged ){
-        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-          children.insert( children.begin(), n.getOperator() );
+      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;
+          }
         }
-        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] );
-  }
+  return false;
 }
 
 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;
+  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( 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;
+    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 > nargs;
-      std::vector<Node> 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);
-      }
-      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->defineFunction(it->first, args, sbody);
-
-      if( Trace.isOn("macros-warn") ){
-        debugMacroDefinition( it->first, sbody );
-      }
+      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") << "done." << std::endl;
+    Trace("macros-def") << "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 );
+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);
   }
-  //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 );
-      }
-    }
+  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
index 8ee878c29..54215b620 100644
--- a/src/preprocessing/passes/quantifier_macros.h
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -44,49 +44,38 @@ class QuantifierMacros : public PreprocessingPass
                      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);
+  /**
+   * 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.
+   * whether there are any quantified formulas corresponding to macros,
+   * and rewrites the given assertions pipeline.
    *
    * @param ap The pipeline to apply macros to.
-   * @param doRewrite Whether we also wish to rewrite the assertions based on
-   * the discovered macro definitions.
    * @return Whether new definitions were inferred and we rewrote the assertions
    * based on them.
    */
-  bool simplify(AssertionPipeline* ap, bool doRewrite = false);
-  Node simplify(Node n);
+  bool simplify(AssertionPipeline* ap);
   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;
+  /** 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;
 };
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e84281a0d..5c3ceec21 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -851,6 +851,7 @@ set(regress_0_tests
   regress0/quantifiers/issue5645-dt-cm-spurious.smt2
   regress0/quantifiers/issue5693-prenex.smt2
   regress0/quantifiers/lra-triv-gn.smt2
+  regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2
   regress0/quantifiers/macros-real-arg.smt2
   regress0/quantifiers/matching-lia-1arg.smt2
diff --git a/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 b/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
new file mode 100644
index 000000000..34b7422a5
--- /dev/null
+++ b/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --macros-quant
+; EXPECT: sat
+(set-logic UFLIA)
+(declare-fun A (Int) Int)
+(declare-fun B (Int) Int)
+(declare-fun C (Int) Int)
+
+(assert (forall ((x Int)) (= (A x) (C (B x)))))
+(assert (forall ((x Int)) (= (B x) 0)))
+
+(assert (= (A 3) (B 4)))
+
+(check-sat)