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, 22 insertions, 14 deletions

diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 05b1b643c..60a8f29f0 100644
--- 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 96e2e7e6f..bb88b64ee 100644
--- 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() << "':"