Eliminate uses of rewrite from datatypes theory (#7354)

Also simplifies slightly how rewritten forms of operators in sygus grammars are obtained.

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index eb6073fbe4933a565fdf2c08ef75ec24e790395e..2a1d4e6c6636c14509b90901c22ba9176a91bfd6 100644 (file)
--- 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 d158cff08854fcd4d77432bc5cd5f7cab5c74af5..16a62101277b70d4ee4ea0b735770e22898a916b 100644 (file)
--- 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 23ca26a1fba4bfea38d40faec73fe9c8a76e8d32..cfeb72b5c757703f509a70cdaea81a494a504f9d 100644 (file)
--- 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 c68b87d85b4e2b59c80bd74df7ea81a4d56acdb7..711cb0a3bb0ecd3eb585f560b7208c09cf3f8bfe 100644 (file)
--- 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 e13dcfbca360b4864afa0c1b78ded2d781b39c55..8ccb4561d81ea51b01bd2743256df6baa54002da 100644 (file)
--- 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