diff options
Diffstat (limited to 'src/theory/fp/theory_fp.cpp')
| -rw-r--r-- | src/theory/fp/theory_fp.cpp | 23 |
1 files changed, 15 insertions, 8 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, |