From f33c9b608b2045a438062ac25bd30231291cfd7f Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 4 Feb 2022 07:01:42 -0800 Subject: [PATCH] FP: Rename tester kinds. (#8037) This renames FP tester kinds for consistency: FLOATINGPOINT_ISINF -> FLOATINGPOINT_IS_INF FLOATINGPOINT_ISN -> FLOATINGPOINT_IS_NORMAL FLOATINGPOINT_ISNAN -> FLOATINGPOINT_IS_NAN FLOATINGPOINT_ISNEG -> FLOATINGPOINT_IS_NEG FLOATINGPOINT_ISPOS -> FLOATINGPOINT_IS_POS FLOATINGPOINT_ISZ -> FLOATINGPOINT_IS_ZERO --- examples/api/cpp/floating_point_arith.cpp | 2 +- examples/api/java/FloatingPointArith.java | 2 +- src/api/cpp/cvc5.cpp | 28 ++--- src/api/cpp/cvc5_kind.h | 14 +-- src/api/parsekinds.py | 4 +- src/parser/smt2/smt2.cpp | 14 +-- src/printer/smt2/smt2_printer.cpp | 14 +-- src/theory/fp/fp_word_blaster.cpp | 14 +-- src/theory/fp/kinds | 28 ++--- src/theory/fp/theory_fp.cpp | 36 +++---- src/theory/fp/theory_fp_rewriter.cpp | 100 ++++++++++-------- .../quantifiers/sygus/sygus_grammar_cons.cpp | 14 +-- test/api/cpp/issue4889.cpp | 2 +- 13 files changed, 142 insertions(+), 130 deletions(-) diff --git a/examples/api/cpp/floating_point_arith.cpp b/examples/api/cpp/floating_point_arith.cpp index 1448f7d1f..4e44965d1 100644 --- a/examples/api/cpp/floating_point_arith.cpp +++ b/examples/api/cpp/floating_point_arith.cpp @@ -76,7 +76,7 @@ int main() Op op = solver.mkOp(FLOATINGPOINT_TO_SBV, 16); // (_ fp.to_sbv 16) lhs = solver.mkTerm(op, rtp, d); rhs = solver.mkTerm(op, rtn, d); - solver.assertFormula(solver.mkTerm(FLOATINGPOINT_ISN, d)); + solver.assertFormula(solver.mkTerm(FLOATINGPOINT_IS_NORMAL, d)); solver.assertFormula(solver.mkTerm(NOT, solver.mkTerm(EQUAL, lhs, rhs))); r = solver.checkSat(); // result is sat diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java index 7f601eee8..92b03ec6c 100644 --- a/examples/api/java/FloatingPointArith.java +++ b/examples/api/java/FloatingPointArith.java @@ -75,7 +75,7 @@ public class FloatingPointArith Op op = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 16); // (_ fp.to_sbv 16) lhs = solver.mkTerm(op, rtp, d); rhs = solver.mkTerm(op, rtn, d); - solver.assertFormula(solver.mkTerm(Kind.FLOATINGPOINT_ISN, d)); + solver.assertFormula(solver.mkTerm(Kind.FLOATINGPOINT_IS_NORMAL, d)); solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, lhs, rhs))); r = solver.checkSat(); // result is sat diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 54174aec4..b246b7547 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -230,13 +230,13 @@ const static std::unordered_map s_kinds{ {FLOATINGPOINT_LT, cvc5::Kind::FLOATINGPOINT_LT}, {FLOATINGPOINT_GEQ, cvc5::Kind::FLOATINGPOINT_GEQ}, {FLOATINGPOINT_GT, cvc5::Kind::FLOATINGPOINT_GT}, - {FLOATINGPOINT_ISN, cvc5::Kind::FLOATINGPOINT_ISN}, - {FLOATINGPOINT_ISSN, cvc5::Kind::FLOATINGPOINT_ISSN}, - {FLOATINGPOINT_ISZ, cvc5::Kind::FLOATINGPOINT_ISZ}, - {FLOATINGPOINT_ISINF, cvc5::Kind::FLOATINGPOINT_ISINF}, - {FLOATINGPOINT_ISNAN, cvc5::Kind::FLOATINGPOINT_ISNAN}, - {FLOATINGPOINT_ISNEG, cvc5::Kind::FLOATINGPOINT_ISNEG}, - {FLOATINGPOINT_ISPOS, cvc5::Kind::FLOATINGPOINT_ISPOS}, + {FLOATINGPOINT_IS_NORMAL, cvc5::Kind::FLOATINGPOINT_IS_NORMAL}, + {FLOATINGPOINT_IS_SUBNORMAL, cvc5::Kind::FLOATINGPOINT_IS_SUBNORMAL}, + {FLOATINGPOINT_IS_ZERO, cvc5::Kind::FLOATINGPOINT_IS_ZERO}, + {FLOATINGPOINT_IS_INF, cvc5::Kind::FLOATINGPOINT_IS_INF}, + {FLOATINGPOINT_IS_NAN, cvc5::Kind::FLOATINGPOINT_IS_NAN}, + {FLOATINGPOINT_IS_NEG, cvc5::Kind::FLOATINGPOINT_IS_NEG}, + {FLOATINGPOINT_IS_POS, cvc5::Kind::FLOATINGPOINT_IS_POS}, {FLOATINGPOINT_TO_FP_FLOATINGPOINT, cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT}, {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, @@ -525,13 +525,13 @@ const static std::unordered_map {cvc5::Kind::FLOATINGPOINT_LT, FLOATINGPOINT_LT}, {cvc5::Kind::FLOATINGPOINT_GEQ, FLOATINGPOINT_GEQ}, {cvc5::Kind::FLOATINGPOINT_GT, FLOATINGPOINT_GT}, - {cvc5::Kind::FLOATINGPOINT_ISN, FLOATINGPOINT_ISN}, - {cvc5::Kind::FLOATINGPOINT_ISSN, FLOATINGPOINT_ISSN}, - {cvc5::Kind::FLOATINGPOINT_ISZ, FLOATINGPOINT_ISZ}, - {cvc5::Kind::FLOATINGPOINT_ISINF, FLOATINGPOINT_ISINF}, - {cvc5::Kind::FLOATINGPOINT_ISNAN, FLOATINGPOINT_ISNAN}, - {cvc5::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG}, - {cvc5::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS}, + {cvc5::Kind::FLOATINGPOINT_IS_NORMAL, FLOATINGPOINT_IS_NORMAL}, + {cvc5::Kind::FLOATINGPOINT_IS_SUBNORMAL, FLOATINGPOINT_IS_SUBNORMAL}, + {cvc5::Kind::FLOATINGPOINT_IS_ZERO, FLOATINGPOINT_IS_ZERO}, + {cvc5::Kind::FLOATINGPOINT_IS_INF, FLOATINGPOINT_IS_INF}, + {cvc5::Kind::FLOATINGPOINT_IS_NAN, FLOATINGPOINT_IS_NAN}, + {cvc5::Kind::FLOATINGPOINT_IS_NEG, FLOATINGPOINT_IS_NEG}, + {cvc5::Kind::FLOATINGPOINT_IS_POS, FLOATINGPOINT_IS_POS}, {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 112b53eb7..e97adf53b 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -1569,7 +1569,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - FLOATINGPOINT_ISN, + FLOATINGPOINT_IS_NORMAL, /** * Floating-point is sub-normal. * @@ -1579,7 +1579,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - FLOATINGPOINT_ISSN, + FLOATINGPOINT_IS_SUBNORMAL, /** * Floating-point is zero. * @@ -1589,7 +1589,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - FLOATINGPOINT_ISZ, + FLOATINGPOINT_IS_ZERO, /** * Floating-point is infinite. * @@ -1599,7 +1599,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - FLOATINGPOINT_ISINF, + FLOATINGPOINT_IS_INF, /** * Floating-point is NaN. * @@ -1609,7 +1609,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - FLOATINGPOINT_ISNAN, + FLOATINGPOINT_IS_NAN, /** * Floating-point is negative. * @@ -1619,7 +1619,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - FLOATINGPOINT_ISNEG, + FLOATINGPOINT_IS_NEG, /** * Floating-point is positive. * @@ -1629,7 +1629,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - FLOATINGPOINT_ISPOS, + FLOATINGPOINT_IS_POS, /** * Operator for to_fp from bit vector. * diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py index db72b20c9..84d154f36 100644 --- a/src/api/parsekinds.py +++ b/src/api/parsekinds.py @@ -96,7 +96,7 @@ class KindsParser: 4. replace Bitvector with BV There is one exception: - FLOATINGPOINT_ISNAN --> FPIsNan + FLOATINGPOINT_IS_NAN --> FPIsNan For every "_IS" in the name, there's an underscore added before step 1, so that the word after "Is" is capitalized @@ -104,7 +104,7 @@ class KindsParser: Examples: BITVECTOR_ADD --> BVAdd APPLY_SELECTOR --> ApplySelector - FLOATINGPOINT_ISNAN --> FPIsNan + FLOATINGPOINT_IS_NAN --> FPIsNan SET_MINUS --> Setminus See the generated .pxi file for an explicit mapping diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3352bde1b..0f0e3060c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -225,13 +225,13 @@ void Smt2::addFloatingPointOperators() { addOperator(api::FLOATINGPOINT_LT, "fp.lt"); addOperator(api::FLOATINGPOINT_GEQ, "fp.geq"); addOperator(api::FLOATINGPOINT_GT, "fp.gt"); - addOperator(api::FLOATINGPOINT_ISN, "fp.isNormal"); - addOperator(api::FLOATINGPOINT_ISSN, "fp.isSubnormal"); - addOperator(api::FLOATINGPOINT_ISZ, "fp.isZero"); - addOperator(api::FLOATINGPOINT_ISINF, "fp.isInfinite"); - addOperator(api::FLOATINGPOINT_ISNAN, "fp.isNaN"); - addOperator(api::FLOATINGPOINT_ISNEG, "fp.isNegative"); - addOperator(api::FLOATINGPOINT_ISPOS, "fp.isPositive"); + addOperator(api::FLOATINGPOINT_IS_NORMAL, "fp.isNormal"); + addOperator(api::FLOATINGPOINT_IS_SUBNORMAL, "fp.isSubnormal"); + addOperator(api::FLOATINGPOINT_IS_ZERO, "fp.isZero"); + addOperator(api::FLOATINGPOINT_IS_INF, "fp.isInfinite"); + addOperator(api::FLOATINGPOINT_IS_NAN, "fp.isNaN"); + addOperator(api::FLOATINGPOINT_IS_NEG, "fp.isNegative"); + addOperator(api::FLOATINGPOINT_IS_POS, "fp.isPositive"); addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real"); addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC, diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 420c176f7..05252b291 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1150,13 +1150,13 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::FLOATINGPOINT_GEQ: return "fp.geq"; case kind::FLOATINGPOINT_GT: return "fp.gt"; - case kind::FLOATINGPOINT_ISN: return "fp.isNormal"; - case kind::FLOATINGPOINT_ISSN: return "fp.isSubnormal"; - case kind::FLOATINGPOINT_ISZ: return "fp.isZero"; - case kind::FLOATINGPOINT_ISINF: return "fp.isInfinite"; - case kind::FLOATINGPOINT_ISNAN: return "fp.isNaN"; - case kind::FLOATINGPOINT_ISNEG: return "fp.isNegative"; - case kind::FLOATINGPOINT_ISPOS: return "fp.isPositive"; + case kind::FLOATINGPOINT_IS_NORMAL: return "fp.isNormal"; + case kind::FLOATINGPOINT_IS_SUBNORMAL: return "fp.isSubnormal"; + case kind::FLOATINGPOINT_IS_ZERO: return "fp.isZero"; + case kind::FLOATINGPOINT_IS_INF: return "fp.isInfinite"; + case kind::FLOATINGPOINT_IS_NAN: return "fp.isNaN"; + case kind::FLOATINGPOINT_IS_NEG: return "fp.isNegative"; + case kind::FLOATINGPOINT_IS_POS: return "fp.isPositive"; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "to_fp"; case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "to_fp"; diff --git a/src/theory/fp/fp_word_blaster.cpp b/src/theory/fp/fp_word_blaster.cpp index 70d77abed..2ff2ec4aa 100644 --- a/src/theory/fp/fp_word_blaster.cpp +++ b/src/theory/fp/fp_word_blaster.cpp @@ -1156,7 +1156,7 @@ Node FpWordBlaster::wordBlast(TNode node) break; /* ---- Tester -------------------------------------------- */ - case kind::FLOATINGPOINT_ISN: + case kind::FLOATINGPOINT_IS_NORMAL: Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); d_boolMap.insert( cur, @@ -1164,7 +1164,7 @@ Node FpWordBlaster::wordBlast(TNode node) (*d_fpMap.find(cur[0])).second)); break; - case kind::FLOATINGPOINT_ISSN: + case kind::FLOATINGPOINT_IS_SUBNORMAL: Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); d_boolMap.insert( cur, @@ -1172,7 +1172,7 @@ Node FpWordBlaster::wordBlast(TNode node) (*d_fpMap.find(cur[0])).second)); break; - case kind::FLOATINGPOINT_ISZ: + case kind::FLOATINGPOINT_IS_ZERO: Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); d_boolMap.insert( cur, @@ -1180,7 +1180,7 @@ Node FpWordBlaster::wordBlast(TNode node) (*d_fpMap.find(cur[0])).second)); break; - case kind::FLOATINGPOINT_ISINF: + case kind::FLOATINGPOINT_IS_INF: Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); d_boolMap.insert( cur, @@ -1188,7 +1188,7 @@ Node FpWordBlaster::wordBlast(TNode node) (*d_fpMap.find(cur[0])).second)); break; - case kind::FLOATINGPOINT_ISNAN: + case kind::FLOATINGPOINT_IS_NAN: Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); d_boolMap.insert( cur, @@ -1196,7 +1196,7 @@ Node FpWordBlaster::wordBlast(TNode node) (*d_fpMap.find(cur[0])).second)); break; - case kind::FLOATINGPOINT_ISNEG: + case kind::FLOATINGPOINT_IS_NEG: Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); d_boolMap.insert( cur, @@ -1204,7 +1204,7 @@ Node FpWordBlaster::wordBlast(TNode node) (*d_fpMap.find(cur[0])).second)); break; - case kind::FLOATINGPOINT_ISPOS: + case kind::FLOATINGPOINT_IS_POS: Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); d_boolMap.insert( cur, diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index fca5363fc..08ccde2f5 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -134,26 +134,26 @@ typerule FLOATINGPOINT_GT ::cvc5::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_ISN 1 "floating-point is normal" -typerule FLOATINGPOINT_ISN ::cvc5::theory::fp::FloatingPointTestTypeRule +operator FLOATINGPOINT_IS_NORMAL 1 "floating-point is normal" +typerule FLOATINGPOINT_IS_NORMAL ::cvc5::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_ISSN 1 "floating-point is sub-normal" -typerule FLOATINGPOINT_ISSN ::cvc5::theory::fp::FloatingPointTestTypeRule +operator FLOATINGPOINT_IS_SUBNORMAL 1 "floating-point is sub-normal" +typerule FLOATINGPOINT_IS_SUBNORMAL ::cvc5::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_ISZ 1 "floating-point is zero" -typerule FLOATINGPOINT_ISZ ::cvc5::theory::fp::FloatingPointTestTypeRule +operator FLOATINGPOINT_IS_ZERO 1 "floating-point is zero" +typerule FLOATINGPOINT_IS_ZERO ::cvc5::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_ISINF 1 "floating-point is infinite" -typerule FLOATINGPOINT_ISINF ::cvc5::theory::fp::FloatingPointTestTypeRule +operator FLOATINGPOINT_IS_INF 1 "floating-point is infinite" +typerule FLOATINGPOINT_IS_INF ::cvc5::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_ISNAN 1 "floating-point is NaN" -typerule FLOATINGPOINT_ISNAN ::cvc5::theory::fp::FloatingPointTestTypeRule +operator FLOATINGPOINT_IS_NAN 1 "floating-point is NaN" +typerule FLOATINGPOINT_IS_NAN ::cvc5::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_ISNEG 1 "floating-point is negative" -typerule FLOATINGPOINT_ISNEG ::cvc5::theory::fp::FloatingPointTestTypeRule +operator FLOATINGPOINT_IS_NEG 1 "floating-point is negative" +typerule FLOATINGPOINT_IS_NEG ::cvc5::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_ISPOS 1 "floating-point is positive" -typerule FLOATINGPOINT_ISPOS ::cvc5::theory::fp::FloatingPointTestTypeRule +operator FLOATINGPOINT_IS_POS 1 "floating-point is positive" +typerule FLOATINGPOINT_IS_POS ::cvc5::theory::fp::FloatingPointTestTypeRule diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 547e52503..1817e53ff 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -114,13 +114,13 @@ void TheoryFp::finishInit() d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_LT); // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_GEQ); // Removed // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_GT); // Removed - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISN); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISSN); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISZ); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISINF); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISNAN); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISNEG); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISPOS); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_NORMAL); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_SUBNORMAL); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_ZERO); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_INF); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_NAN); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_NEG); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_POS); d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR); d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT); @@ -221,9 +221,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) Node defined = nm->mkNode( kind::AND, nm->mkNode(kind::NOT, - nm->mkNode(kind::FLOATINGPOINT_ISNAN, concrete[0])), + nm->mkNode(kind::FLOATINGPOINT_IS_NAN, concrete[0])), nm->mkNode(kind::NOT, - nm->mkNode(kind::FLOATINGPOINT_ISINF, concrete[0]))); + nm->mkNode(kind::FLOATINGPOINT_IS_INF, concrete[0]))); // First the "forward" constraints Node fg = nm->mkNode( kind::IMPLIES, @@ -508,19 +508,19 @@ void TheoryFp::registerTerm(TNode node) // Give the expansion of classifications in terms of equalities // This should make equality reasoning slightly more powerful. - if ((k == kind::FLOATINGPOINT_ISNAN) || (k == kind::FLOATINGPOINT_ISZ) - || (k == kind::FLOATINGPOINT_ISINF)) + if ((k == kind::FLOATINGPOINT_IS_NAN) || (k == kind::FLOATINGPOINT_IS_ZERO) + || (k == kind::FLOATINGPOINT_IS_INF)) { NodeManager* nm = NodeManager::currentNM(); FloatingPointSize s = node[0].getType().getConst(); Node equalityAlias = Node::null(); - if (k == kind::FLOATINGPOINT_ISNAN) + if (k == kind::FLOATINGPOINT_IS_NAN) { equalityAlias = nm->mkNode( kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s))); } - else if (k == kind::FLOATINGPOINT_ISZ) + else if (k == kind::FLOATINGPOINT_IS_ZERO) { equalityAlias = nm->mkNode( kind::OR, @@ -531,7 +531,7 @@ void TheoryFp::registerTerm(TNode node) node[0], nm->mkConst(FloatingPoint::makeZero(s, false)))); } - else if (k == kind::FLOATINGPOINT_ISINF) + else if (k == kind::FLOATINGPOINT_IS_INF) { equalityAlias = nm->mkNode(kind::OR, @@ -562,14 +562,14 @@ void TheoryFp::registerTerm(TNode node) Node pd = nm->mkNode(kind::IMPLIES, nm->mkNode(kind::OR, - nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]), - nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])), + nm->mkNode(kind::FLOATINGPOINT_IS_NAN, node[0]), + nm->mkNode(kind::FLOATINGPOINT_IS_INF, node[0])), nm->mkNode(kind::EQUAL, node, node[1])); handleLemma(pd, InferenceId::FP_REGISTER_TERM); Node z = nm->mkNode( kind::IMPLIES, - nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]), + nm->mkNode(kind::FLOATINGPOINT_IS_ZERO, node[0]), nm->mkNode(kind::EQUAL, node, nm->mkConstReal(Rational(0U)))); handleLemma(z, InferenceId::FP_REGISTER_TERM); return; @@ -586,7 +586,7 @@ void TheoryFp::registerTerm(TNode node) d_abstractionMap.insert(sk, node); Node nnan = - nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node)); + nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_IS_NAN, node)); handleLemma(nnan, InferenceId::FP_REGISTER_TERM); Node z = nm->mkNode( diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 779d02ab3..0fddbe9b4 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -186,16 +186,22 @@ namespace rewrite { Assert(node.getKind() == kind::FLOATINGPOINT_EQ); NodeManager *nm = NodeManager::currentNM(); - return RewriteResponse(REWRITE_DONE, - nm->mkNode(kind::AND, - nm->mkNode(kind::AND, - nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0])), - nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[1]))), - nm->mkNode(kind::OR, - nm->mkNode(kind::EQUAL, node[0], node[1]), - nm->mkNode(kind::AND, - nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]), - nm->mkNode(kind::FLOATINGPOINT_ISZ, node[1]))))); + return RewriteResponse( + REWRITE_DONE, + nm->mkNode( + kind::AND, + nm->mkNode( + kind::AND, + nm->mkNode(kind::NOT, + nm->mkNode(kind::FLOATINGPOINT_IS_NAN, node[0])), + nm->mkNode(kind::NOT, + nm->mkNode(kind::FLOATINGPOINT_IS_NAN, node[1]))), + nm->mkNode( + kind::OR, + nm->mkNode(kind::EQUAL, node[0], node[1]), + nm->mkNode(kind::AND, + nm->mkNode(kind::FLOATINGPOINT_IS_ZERO, node[0]), + nm->mkNode(kind::FLOATINGPOINT_IS_ZERO, node[1]))))); } RewriteResponse geqToleq(TNode node, bool isPreRewrite) @@ -303,11 +309,11 @@ namespace rewrite { } RewriteResponse removeSignOperations (TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_ISN - || node.getKind() == kind::FLOATINGPOINT_ISSN - || node.getKind() == kind::FLOATINGPOINT_ISZ - || node.getKind() == kind::FLOATINGPOINT_ISINF - || node.getKind() == kind::FLOATINGPOINT_ISNAN); + Assert(node.getKind() == kind::FLOATINGPOINT_IS_NORMAL + || node.getKind() == kind::FLOATINGPOINT_IS_SUBNORMAL + || node.getKind() == kind::FLOATINGPOINT_IS_ZERO + || node.getKind() == kind::FLOATINGPOINT_IS_INF + || node.getKind() == kind::FLOATINGPOINT_IS_NAN); Assert(node.getNumChildren() == 1); Kind childKind(node[0].getKind()); @@ -363,7 +369,7 @@ namespace rewrite { return RewriteResponse( isPreRewrite ? REWRITE_DONE : REWRITE_AGAIN_FULL, nm->mkNode(kind::NOT, - nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]))); + nm->mkNode(kind::FLOATINGPOINT_IS_NAN, node[0]))); } return RewriteResponse(REWRITE_DONE, node); } @@ -716,7 +722,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse isNormal(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_ISN); + Assert(node.getKind() == kind::FLOATINGPOINT_IS_NORMAL); Assert(node.getNumChildren() == 1); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst().isNormal())); @@ -724,7 +730,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse isSubnormal(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_ISSN); + Assert(node.getKind() == kind::FLOATINGPOINT_IS_SUBNORMAL); Assert(node.getNumChildren() == 1); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst().isSubnormal())); @@ -732,7 +738,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse isZero(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_ISZ); + Assert(node.getKind() == kind::FLOATINGPOINT_IS_ZERO); Assert(node.getNumChildren() == 1); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst().isZero())); @@ -740,7 +746,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse isInfinite(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_ISINF); + Assert(node.getKind() == kind::FLOATINGPOINT_IS_INF); Assert(node.getNumChildren() == 1); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst().isInfinite())); @@ -748,7 +754,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse isNaN(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_ISNAN); + Assert(node.getKind() == kind::FLOATINGPOINT_IS_NAN); Assert(node.getNumChildren() == 1); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst().isNaN())); @@ -756,7 +762,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse isNegative(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_ISNEG); + Assert(node.getKind() == kind::FLOATINGPOINT_IS_NEG); Assert(node.getNumChildren() == 1); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst().isNegative())); @@ -764,7 +770,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse isPositive(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_ISPOS); + Assert(node.getKind() == kind::FLOATINGPOINT_IS_POS); Assert(node.getNumChildren() == 1); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst().isPositive())); @@ -1159,13 +1165,13 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) rewrite::then; /******** Classifications ********/ - d_preRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::identity; - d_preRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::identity; - d_preRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::identity; - d_preRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::identity; - d_preRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::identity; - d_preRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity; - d_preRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_IS_ZERO] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_IS_INF] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_IS_NAN] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity; /******** Conversions ********/ d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = @@ -1245,13 +1251,18 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::identity; /******** Classifications ********/ - d_postRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::removeSignOperations; - d_postRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::removeSignOperations; - d_postRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::removeSignOperations; - d_postRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::removeSignOperations; - d_postRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::removeSignOperations; - d_postRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity; - d_postRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity; + d_postRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] = + rewrite::removeSignOperations; + d_postRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] = + rewrite::removeSignOperations; + d_postRewriteTable[kind::FLOATINGPOINT_IS_ZERO] = + rewrite::removeSignOperations; + d_postRewriteTable[kind::FLOATINGPOINT_IS_INF] = + rewrite::removeSignOperations; + d_postRewriteTable[kind::FLOATINGPOINT_IS_NAN] = + rewrite::removeSignOperations; + d_postRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity; + d_postRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity; /******** Conversions ********/ d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = @@ -1331,13 +1342,14 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_constantFoldTable[kind::FLOATINGPOINT_LT] = constantFold::lt; /******** Classifications ********/ - d_constantFoldTable[kind::FLOATINGPOINT_ISN] = constantFold::isNormal; - d_constantFoldTable[kind::FLOATINGPOINT_ISSN] = constantFold::isSubnormal; - d_constantFoldTable[kind::FLOATINGPOINT_ISZ] = constantFold::isZero; - d_constantFoldTable[kind::FLOATINGPOINT_ISINF] = constantFold::isInfinite; - d_constantFoldTable[kind::FLOATINGPOINT_ISNAN] = constantFold::isNaN; - d_constantFoldTable[kind::FLOATINGPOINT_ISNEG] = constantFold::isNegative; - d_constantFoldTable[kind::FLOATINGPOINT_ISPOS] = constantFold::isPositive; + d_constantFoldTable[kind::FLOATINGPOINT_IS_NORMAL] = constantFold::isNormal; + d_constantFoldTable[kind::FLOATINGPOINT_IS_SUBNORMAL] = + constantFold::isSubnormal; + d_constantFoldTable[kind::FLOATINGPOINT_IS_ZERO] = constantFold::isZero; + d_constantFoldTable[kind::FLOATINGPOINT_IS_INF] = constantFold::isInfinite; + d_constantFoldTable[kind::FLOATINGPOINT_IS_NAN] = constantFold::isNaN; + d_constantFoldTable[kind::FLOATINGPOINT_IS_NEG] = constantFold::isNegative; + d_constantFoldTable[kind::FLOATINGPOINT_IS_POS] = constantFold::isPositive; /******** Conversions ********/ d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index c2a589565..1eb722372 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -1412,13 +1412,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( else if (types[i].isFloatingPoint()) { Trace("sygus-grammar-def") << "...add FP predicates" << std::endl; - std::vector fp_unary_predicates = {FLOATINGPOINT_ISN, - FLOATINGPOINT_ISSN, - FLOATINGPOINT_ISZ, - FLOATINGPOINT_ISINF, - FLOATINGPOINT_ISNAN, - FLOATINGPOINT_ISNEG, - FLOATINGPOINT_ISPOS}; + std::vector fp_unary_predicates = {FLOATINGPOINT_IS_NORMAL, + FLOATINGPOINT_IS_SUBNORMAL, + FLOATINGPOINT_IS_ZERO, + FLOATINGPOINT_IS_INF, + FLOATINGPOINT_IS_NAN, + FLOATINGPOINT_IS_NEG, + FLOATINGPOINT_IS_POS}; for (const Kind kind : fp_unary_predicates) { sdtBool.addConstructor(kind, cargs); diff --git a/test/api/cpp/issue4889.cpp b/test/api/cpp/issue4889.cpp index 8e0853682..373aa6d00 100644 --- a/test/api/cpp/issue4889.cpp +++ b/test/api/cpp/issue4889.cpp @@ -30,7 +30,7 @@ int main() Term const2 = slv.mkConst(sort_bool, "_c4"); Term ite = slv.mkTerm(ITE, const2, const1, const0); Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1); - Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem); + Term isnan = slv.mkTerm(FLOATINGPOINT_IS_NAN, rem); slv.checkSatAssuming(isnan); return 0; } -- 2.30.2