summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.h31
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h5
-rw-r--r--src/theory/fp/theory_fp.cpp23
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp17
-rw-r--r--src/theory/theory_rewriter.h7
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress0/fp/issue3536.smt26
7 files changed, 57 insertions, 33 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() << "':"
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] =
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback