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.

5 files changed, 419 insertions, 0 deletions

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() ){