Avoid calling rewriter from type checker (#3548)

Fixes #3536. The type checker for the chain operator was calling the
rewriter. However, the floating-point rewriter was expecting
`TheoryFp::expandDefinition()` to be applied before rewriting. If the
chain operator had subterms that were supposed to be removed by
`TheoryFp::expandDefinition()`, the FP rewriter was throwing an
exception. This commit fixes the issue by not calling the full rewriter
in the type checker but by just expanding the chain operator. This is a
bit less efficient than before because the rewriter does not cache the
result of expanding the chain operator anymore but assuming that there
are no long chains, the performance impact should be negligible. It also
seemed like a reasonable assumption that the rewriter can expect to run
after `expandDefinition()` because otherwise the rewriter has to expand
definitions, which may be too restrictive.

2 files changed, 21 insertions, 19 deletions

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index fa143a1d0..6a4dc542e 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -813,33 +813,40 @@ void TheoryFp::registerTerm(TNode node) {
   Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl;
 
   if (!isRegistered(node)) {
+    Kind k = node.getKind();
+    Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC
+           && k != kind::FLOATINGPOINT_SUB && k != kind::FLOATINGPOINT_EQ
+           && k != kind::FLOATINGPOINT_GEQ && k != kind::FLOATINGPOINT_GT);
+
     bool success = d_registeredTerms.insert(node);
     (void)success;  // Only used for assertion
     Assert(success);
 
     // Add to the equality engine
-    if (node.getKind() == kind::EQUAL) {
+    if (k == kind::EQUAL)
+    {
       d_equalityEngine.addTriggerEquality(node);
-    } else {
+    }
+    else
+    {
       d_equalityEngine.addTerm(node);
     }
 
     // Give the expansion of classifications in terms of equalities
     // This should make equality reasoning slightly more powerful.
-    if ((node.getKind() == kind::FLOATINGPOINT_ISNAN)
-        || (node.getKind() == kind::FLOATINGPOINT_ISZ)
-        || (node.getKind() == kind::FLOATINGPOINT_ISINF))
+    if ((k == kind::FLOATINGPOINT_ISNAN) || (k == kind::FLOATINGPOINT_ISZ)
+        || (k == kind::FLOATINGPOINT_ISINF))
     {
       NodeManager *nm = NodeManager::currentNM();
       FloatingPointSize s = node[0].getType().getConst<FloatingPointSize>();
       Node equalityAlias = Node::null();
 
-      if (node.getKind() == kind::FLOATINGPOINT_ISNAN)
+      if (k == kind::FLOATINGPOINT_ISNAN)
       {
         equalityAlias = nm->mkNode(
             kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s)));
       }
-      else if (node.getKind() == kind::FLOATINGPOINT_ISZ)
+      else if (k == kind::FLOATINGPOINT_ISZ)
       {
         equalityAlias = nm->mkNode(
             kind::OR,
@@ -850,7 +857,7 @@ void TheoryFp::registerTerm(TNode node) {
                        node[0],
                        nm->mkConst(FloatingPoint::makeZero(s, false))));
       }
-      else if (node.getKind() == kind::FLOATINGPOINT_ISINF)
+      else if (k == kind::FLOATINGPOINT_ISINF)
       {
         equalityAlias = nm->mkNode(
             kind::OR,
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 5d1e3d4da..8854b400d 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -1048,7 +1048,7 @@ TheoryFpRewriter::TheoryFpRewriter()
       rewrite::identity;
   d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] =
       rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed;
+  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::identity;
   d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
   d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
   d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
@@ -1096,7 +1096,7 @@ TheoryFpRewriter::TheoryFpRewriter()
   d_postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
   d_postRewriteTable[kind::FLOATINGPOINT_PLUS] =
       rewrite::reorderBinaryOperation;
-  d_postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::removed;
+  d_postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::identity;
   d_postRewriteTable[kind::FLOATINGPOINT_MULT] =
       rewrite::reorderBinaryOperation;
   d_postRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
@@ -1110,11 +1110,11 @@ TheoryFpRewriter::TheoryFpRewriter()
   d_postRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
 
   /******** Comparisons ********/
-  d_postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::removed;
+  d_postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::identity;
   d_postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::leqId;
   d_postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::ltId;
-  d_postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::removed;
-  d_postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::removed;
+  d_postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::identity;
+  d_postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::identity;
 
   /******** Classifications ********/
   d_postRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::removeSignOperations;
@@ -1135,7 +1135,7 @@ TheoryFpRewriter::TheoryFpRewriter()
       rewrite::identity;
   d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] =
       rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed;
+  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::identity;
   d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
   d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
   d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
@@ -1186,7 +1186,6 @@ TheoryFpRewriter::TheoryFpRewriter()
   d_constantFoldTable[kind::FLOATINGPOINT_ABS] = constantFold::abs;
   d_constantFoldTable[kind::FLOATINGPOINT_NEG] = constantFold::neg;
   d_constantFoldTable[kind::FLOATINGPOINT_PLUS] = constantFold::plus;
-  d_constantFoldTable[kind::FLOATINGPOINT_SUB] = rewrite::removed;
   d_constantFoldTable[kind::FLOATINGPOINT_MULT] = constantFold::mult;
   d_constantFoldTable[kind::FLOATINGPOINT_DIV] = constantFold::div;
   d_constantFoldTable[kind::FLOATINGPOINT_FMA] = constantFold::fma;
@@ -1199,11 +1198,8 @@ TheoryFpRewriter::TheoryFpRewriter()
   d_constantFoldTable[kind::FLOATINGPOINT_MAX_TOTAL] = constantFold::maxTotal;
 
   /******** Comparisons ********/
-  d_constantFoldTable[kind::FLOATINGPOINT_EQ] = rewrite::removed;
   d_constantFoldTable[kind::FLOATINGPOINT_LEQ] = constantFold::leq;
   d_constantFoldTable[kind::FLOATINGPOINT_LT] = constantFold::lt;
-  d_constantFoldTable[kind::FLOATINGPOINT_GEQ] = rewrite::removed;
-  d_constantFoldTable[kind::FLOATINGPOINT_GT] = rewrite::removed;
 
   /******** Classifications ********/
   d_constantFoldTable[kind::FLOATINGPOINT_ISN] = constantFold::isNormal;
@@ -1225,7 +1221,6 @@ TheoryFpRewriter::TheoryFpRewriter()
       constantFold::convertFromSBV;
   d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] =
       constantFold::convertFromUBV;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed;
   d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV] = constantFold::convertToUBV;
   d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV] = constantFold::convertToSBV;
   d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL] =