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.

diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 05b1b643c5f3b3c5f8c385a91172b6191aa9066a..60a8f29f0ebbcb7b8b4a9cd77fa89bed9c5e032b 100644 (file)
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -30,18 +30,29 @@ namespace builtin {
 class TheoryBuiltinRewriter : public TheoryRewriter
 {
   static Node blastDistinct(TNode node);
-  static Node blastChain(TNode node);
 
-public:
+ public:
+  /**
+   * Takes a chained application of a binary operator and returns a conjunction
+   * of binary applications of that operator.
+   *
+   * For example:
+   *
+   * (= x y z) ---> (and (= x y) (= y z))
+   *
+   * @param node A node that is a chained application of a binary operator
+   * @return A conjunction of binary applications of the chained operator
+   */
+  static Node blastChain(TNode node);
 
-  static inline RewriteResponse doRewrite(TNode node) {
-    switch(node.getKind()) {
-    case kind::DISTINCT:
-      return RewriteResponse(REWRITE_DONE, blastDistinct(node));
-    case kind::CHAIN:
-      return RewriteResponse(REWRITE_DONE, blastChain(node));
-    default:
-      return RewriteResponse(REWRITE_DONE, node);
+  static inline RewriteResponse doRewrite(TNode node)
+  {
+    switch (node.getKind())
+    {
+      case kind::DISTINCT:
+        return RewriteResponse(REWRITE_DONE, blastDistinct(node));
+      case kind::CHAIN: return RewriteResponse(REWRITE_DONE, blastChain(node));
+      default: return RewriteResponse(REWRITE_DONE, node);
     }
   }
 

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 96e2e7e6f26dd027b03d674465dc6a4a18e7f2e1..bb88b64ee5eb3542c7ed818e123cc693cdbcd8c0 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -205,10 +205,7 @@ class ChainTypeRule {
 
     TypeNode tn;
     try {
-      // Actually do the expansion to do the typechecking.
-      // Shouldn't be extra work to do this, since the rewriter
-      // keeps a cache.
-      tn = nodeManager->getType(Rewriter::rewrite(n), check);
+      tn = nodeManager->getType(TheoryBuiltinRewriter::blastChain(n), check);
     } catch(TypeCheckingExceptionPrivate& e) {
       std::stringstream ss;
       ss << "Cannot typecheck the expansion of chained operator `" << n.getOperator() << "':"

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index fa143a1d02fb1df64b132bb1ad0dec9925946e66..6a4dc542e788400e0a8c814d8e173c1f9b2aae1f 100644 (file)
--- 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 5d1e3d4da11b9ea8b07deca3e3f560780ecefce4..8854b400d1266da595a2dfe23d2faf76d6db157c 100644 (file)
--- 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] =

diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h
index b0171813bcdc42ac3c87119a0142241494ca403f..61f0fc27a2202092cb075ef6ff82ac95aab69a8a 100644 (file)
--- a/src/theory/theory_rewriter.h
+++ b/src/theory/theory_rewriter.h
@@ -53,6 +53,13 @@ struct RewriteResponse
   }
 }; /* struct RewriteResponse */
 
+/**
+ * The interface that a theory rewriter has to implement.
+ *
+ * Note: A theory rewriter is expected to handle all kinds of a theory, even
+ * the ones that are removed by `Theory::expandDefinition()` since it may be
+ * called on terms before the definitions have been expanded.
+ */
 class TheoryRewriter
 {
  public:

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b0539325885dfb94789aa34bdf2ad6215cf47701..7bd626ff0573824e5a7eda9d142852007da7f1a8 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -470,6 +470,7 @@ set(regress_0_tests
   regress0/fp/abs-unsound2.smt2
   regress0/fp/down-cast-RNA.smt2
   regress0/fp/ext-rew-test.smt2
+  regress0/fp/issue3536.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/rti_3_5_bug_report.smt2
   regress0/fp/simple.smt2

diff --git a/test/regress/regress0/fp/issue3536.smt2 b/test/regress/regress0/fp/issue3536.smt2
new file mode 100644 (file)
index 0000000..4293cbd
--- /dev/null
+++ b/test/regress/regress0/fp/issue3536.smt2
@@ -0,0 +1,6 @@
+; REQUIRES: symfpu
+(set-logic QF_FP)
+(declare-const x (_ FloatingPoint 11 53))
+(assert (= true (fp.eq x ((_ to_fp 11 53) (_ bv13831004815617530266 64))) true))
+(set-info :status sat)
+(check-sat)