From 9c2c0581e0a325aad8cef463cfcc72b1164f79f5 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 18 Dec 2019 00:27:18 -0800 Subject: [PATCH] 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. --- src/theory/builtin/theory_builtin_rewriter.h | 31 +++++++++++++------ .../builtin/theory_builtin_type_rules.h | 5 +-- src/theory/fp/theory_fp.cpp | 23 +++++++++----- src/theory/fp/theory_fp_rewriter.cpp | 17 ++++------ src/theory/theory_rewriter.h | 7 +++++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/fp/issue3536.smt2 | 6 ++++ 7 files changed, 57 insertions(+), 33 deletions(-) create mode 100644 test/regress/regress0/fp/issue3536.smt2 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() << "':" 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(); 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] = diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h index b0171813b..61f0fc27a 100644 --- 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 b05393258..7bd626ff0 100644 --- 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 index 000000000..4293cbdee --- /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) -- 2.30.2