From 55ce505ca757dc241bf4c1e10023bc43ac531a23 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 13 Oct 2021 10:22:03 -0500
Subject: [PATCH] Eliminate uses of rewrite from datatypes theory (#7354)

Also simplifies slightly how rewritten forms of operators in sygus grammars are obtained.
---
 src/smt/sygus_solver.cpp                      |  1 +
 src/theory/datatypes/inference_manager.cpp    |  2 +-
 src/theory/datatypes/proof_checker.cpp        |  2 +-
 src/theory/datatypes/sygus_datatype_utils.cpp | 42 ++++++-------------
 src/theory/evaluator.h                        |  2 +-
 5 files changed, 17 insertions(+), 32 deletions(-)

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index eb6073fbe..2a1d4e6c6 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -435,6 +435,7 @@ void SygusSolver::expandDefinitionsSygusDt(TypeNode tn) const
       Node eop = op.isConst()
                      ? op
                      : d_smtSolver.getPreprocessor()->expandDefinitions(op);
+      eop = rewrite(eop);
       datatypes::utils::setExpandedDefinitionForm(op, eop);
       // also must consider the arguments
       for (unsigned j = 0, nargs = c->getNumArgs(); j < nargs; ++j)
diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index d158cff08..16a621012 100644
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -159,7 +159,7 @@ Node InferenceManager::prepareDtInference(Node conc,
   if (conc.getKind() == EQUAL && conc[0].getType().isBoolean())
   {
     // must turn (= conc false) into (not conc)
-    conc = Rewriter::rewrite(conc);
+    conc = rewrite(conc);
   }
   if (isProofEnabled())
   {
diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
index 23ca26a1f..cfeb72b5c 100644
--- a/src/theory/datatypes/proof_checker.cpp
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -74,7 +74,7 @@ Node DatatypesProofRuleChecker::checkInternal(PfRule id,
       return Node::null();
     }
     Node tester = utils::mkTester(t, i, dt);
-    Node ticons = Rewriter::rewrite(utils::getInstCons(t, dt, i));
+    Node ticons = utils::getInstCons(t, dt, i);
     return tester.eqNode(t.eqNode(ticons));
   }
   else if (id == PfRule::DT_COLLAPSE)
diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index c68b87d85..711cb0a3b 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -111,12 +111,6 @@ Kind getOperatorKindForSygusBuiltin(Node op)
   return NodeManager::getKindForFunction(op);
 }
 
-struct SygusOpRewrittenAttributeId
-{
-};
-typedef expr::Attribute<SygusOpRewrittenAttributeId, Node>
-    SygusOpRewrittenAttribute;
-
 Kind getEliminateKind(Kind ok)
 {
   Kind nk = ok;
@@ -154,36 +148,26 @@ Node mkSygusTerm(const DType& dt,
   {
     // Get the normalized version of the sygus operator. We do this by
     // expanding definitions, rewriting it, and eliminating partial operators.
-    if (!op.hasAttribute(SygusOpRewrittenAttribute()))
+    if (op.isConst())
     {
-      if (op.isConst())
+      // If it is a builtin operator, convert to total version if necessary.
+      // First, get the kind for the operator.
+      Kind ok = NodeManager::operatorToKind(op);
+      Trace("sygus-grammar-normalize-debug")
+          << "...builtin kind is " << ok << std::endl;
+      Kind nk = getEliminateKind(ok);
+      if (nk != ok)
       {
-        // If it is a builtin operator, convert to total version if necessary.
-        // First, get the kind for the operator.
-        Kind ok = NodeManager::operatorToKind(op);
         Trace("sygus-grammar-normalize-debug")
-            << "...builtin kind is " << ok << std::endl;
-        Kind nk = getEliminateKind(ok);
-        if (nk != ok)
-        {
-          Trace("sygus-grammar-normalize-debug")
-              << "...replace by builtin operator " << nk << std::endl;
-          opn = NodeManager::currentNM()->operatorOf(nk);
-        }
-      }
-      else
-      {
-        // Get the expanded definition form, if it has been marked. This ensures
-        // that user-defined functions have been eliminated from op.
-        opn = getExpandedDefinitionForm(op);
-        opn = Rewriter::rewrite(opn);
-        SygusOpRewrittenAttribute sora;
-        op.setAttribute(sora, opn);
+            << "...replace by builtin operator " << nk << std::endl;
+        opn = NodeManager::currentNM()->operatorOf(nk);
       }
     }
     else
     {
-      opn = op.getAttribute(SygusOpRewrittenAttribute());
+      // Get the expanded definition form, if it has been marked. This ensures
+      // that user-defined functions have been eliminated from op.
+      opn = getExpandedDefinitionForm(op);
     }
   }
   return mkSygusTerm(opn, children, doBetaReduction);
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index e13dcfbca..8ccb4561d 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -108,7 +108,7 @@ class Evaluator
    * rewriter for computing the result of this method.
    *
    * The result of this call is either equivalent to:
-   * (1) Rewriter::rewrite(n.substitute(args,vars))
+   * (1) rewrite(n.substitute(args,vars))
    * (2) Node::null().
    * If d_rr is non-null, then we are always in the first case. If
    * useRewriter is null, then we may be in case (2) if computing the
-- 
2.30.2