From f6db1c40f085002954bfb69fc59568079b33a6e7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 20 Mar 2026 11:49:46 +0000 Subject: [PATCH 1/2] Add fp.isSubnormal, fp.isNegative, fp.isPositive to SMT2 parser Implement the three missing FP predicates in the SMT2 parser: - fp.isSubnormal: finite, non-zero, and not normal -- mirrors SMT-LIB's own definition (Theory of Floating-Point Numbers, fp.isSubnormal). Encoded with isfinite_exprt and the existing is-not-zero / is-not-normal helpers. - fp.isNegative: sign bit is 1 and not NaN. The explicit not(isnan) is required: float_bvt::sign_bit returns the raw top bit (true for -NaN), whereas SMT-LIB's fp.isNegative is false for any NaN. - fp.isPositive: symmetric counterpart, sign bit is 0 and not NaN. These are expressed as compound expressions using existing predicates, requiring no back-end changes. Regression test in regression/smt2_solver/fp-predicates/ exercises both directions: - under-approximation: a (check-sat) over six declared constants and a handful of concrete-bit-pattern witnesses (smallest positive Float32 subnormal, +/-0, NaN) checks that each predicate holds on values it should accept; - over-approximation: three (check-sat-assuming ...) calls assert that the predicates do *not* return true on values they should reject (-0 is not positive, +0 is not negative, 1.0 is not subnormal). Each is expected to return unsat. Co-authored-by: Kiro --- regression/smt2_solver/fp/fp-predicates1.desc | 14 ++++ regression/smt2_solver/fp/fp-predicates1.smt2 | 45 +++++++++++++ src/solvers/smt2/smt2_parser.cpp | 66 +++++++++++++++++++ 3 files changed, 125 insertions(+) create mode 100644 regression/smt2_solver/fp/fp-predicates1.desc create mode 100644 regression/smt2_solver/fp/fp-predicates1.smt2 diff --git a/regression/smt2_solver/fp/fp-predicates1.desc b/regression/smt2_solver/fp/fp-predicates1.desc new file mode 100644 index 00000000000..73b5fe937a7 --- /dev/null +++ b/regression/smt2_solver/fp/fp-predicates1.desc @@ -0,0 +1,14 @@ +CORE +fp-predicates1.smt2 + +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +^sat$[\s\S]*?^unsat$[\s\S]*?^unsat$[\s\S]*?^unsat$ +-- +Test fp.isSubnormal, fp.isNegative, fp.isPositive predicates. +The leading sat covers the under-approximation cases: each +predicate must hold on a witness. The three trailing unsat +results from check-sat-assuming cover over-approximation: -0 +must not be positive, +0 must not be negative, and 1.0 must not +be subnormal. diff --git a/regression/smt2_solver/fp/fp-predicates1.smt2 b/regression/smt2_solver/fp/fp-predicates1.smt2 new file mode 100644 index 00000000000..c3f0d96527a --- /dev/null +++ b/regression/smt2_solver/fp/fp-predicates1.smt2 @@ -0,0 +1,45 @@ +; Test fp.isSubnormal, fp.isNegative, fp.isPositive predicates. + +(set-logic QF_FP) + +; A subnormal Float32 exists, and at least one concrete subnormal +; bit-pattern is classified as subnormal (and not zero / not normal). +(declare-const s (_ FloatingPoint 8 24)) +(assert (fp.isSubnormal s)) +(assert (not (fp.isZero s))) + +; Smallest positive Float32 subnormal: exponent = 0, mantissa = 0...01 +(assert (fp.isSubnormal + (fp #b0 #b00000000 #b00000000000000000000001))) +(assert (not (fp.isNormal + (fp #b0 #b00000000 #b00000000000000000000001)))) + +; A negative normal value exists +(declare-const n (_ FloatingPoint 8 24)) +(assert (fp.isNegative n)) +(assert (fp.isNormal n)) + +; A positive value exists +(declare-const p (_ FloatingPoint 8 24)) +(assert (fp.isPositive p)) + +; NaN is neither negative nor positive +(assert (not (fp.isNegative (_ NaN 8 24)))) +(assert (not (fp.isPositive (_ NaN 8 24)))) + +; Negative zero is negative, positive zero is positive +(assert (fp.isNegative (fp #b1 #b00000000 #b00000000000000000000000))) +(assert (not (fp.isNegative (fp #b0 #b00000000 #b00000000000000000000000)))) +(assert (fp.isPositive (fp #b0 #b00000000 #b00000000000000000000000))) +(assert (not (fp.isPositive (fp #b1 #b00000000 #b00000000000000000000000)))) + +(check-sat) + +; Negative coverage: each of these would be `sat` if the corresponding +; predicate over-approximated. Expect `unsat` instead. +(check-sat-assuming + ((fp.isPositive (fp #b1 #b00000000 #b00000000000000000000000)))) ; -0 +(check-sat-assuming + ((fp.isNegative (fp #b0 #b00000000 #b00000000000000000000000)))) ; +0 +(check-sat-assuming + ((fp.isSubnormal (fp #b0 #b01111111 #b00000000000000000000000)))) ; 1.0 diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index f233905dd20..9b60f8d6563 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -1369,6 +1369,72 @@ void smt2_parsert::setup_expressions() return not_exprt(typecast_exprt(op[0], bool_typet())); }; + expressions["fp.isSubnormal"] = [this] + { + auto op = operands(); + + if(op.size() != 1) + throw error("fp.isSubnormal takes one operand"); + + if(op[0].type().id() != ID_floatbv) + throw error("fp.isSubnormal takes FloatingPoint operand"); + + // subnormal iff finite, non-zero, and not normal -- mirrors + // SMT-LIB's own definition of fp.isSubnormal (Theory of + // Floating-Point Numbers). + // + // Do *not* turn the third reference to `op[0]` below into + // `std::move(op[0])` to avoid the extra copy. Although C++17 + // [dcl.init.list]/4 mandates left-to-right evaluation of the + // initializer-clauses of a braced-init-list, MSVC's + // implementation has been unreliable for direct-list-init of a + // constructor (observed under cl.exe on the windows-2022 and + // windows-2025 GitHub Actions runners). With the move, the + // last clause is sequenced before the earlier clauses read + // `op[0]`; the earlier clauses then see a moved-from `op[0]` + // whose `type()` is `nil`, which trips + // `boolbv_widtht::get_entry(nil)` further down the conversion + // pipeline. Three copies are correct, portable, and cheap + // (irept uses sharing, so each copy is a refcount bump). + return and_exprt{ + isfinite_exprt{op[0]}, + typecast_exprt{op[0], bool_typet{}}, // != 0 + not_exprt{isnormal_exprt{op[0]}}}; + }; + + expressions["fp.isNegative"] = [this] + { + auto op = operands(); + + if(op.size() != 1) + throw error("fp.isNegative takes one operand"); + + if(op[0].type().id() != ID_floatbv) + throw error("fp.isNegative takes FloatingPoint operand"); + + // negative iff sign bit is 1 and not NaN. The explicit + // not(isnan) is required: float_bvt::sign_bit returns the raw + // top bit of the bit-vector encoding (true for -NaN), whereas + // SMT-LIB's fp.isNegative is false for any NaN. Do not drop the + // NaN guard. + return and_exprt{not_exprt{isnan_exprt{op[0]}}, sign_exprt{op[0]}}; + }; + + expressions["fp.isPositive"] = [this] + { + auto op = operands(); + + if(op.size() != 1) + throw error("fp.isPositive takes one operand"); + + if(op[0].type().id() != ID_floatbv) + throw error("fp.isPositive takes FloatingPoint operand"); + + // positive iff sign bit is 0 and not NaN + return and_exprt{ + not_exprt{isnan_exprt{op[0]}}, not_exprt{sign_exprt{op[0]}}}; + }; + expressions["fp"] = [this] { return function_application_fp(operands()); }; expressions["fp.add"] = [this] { From c4d1cdddcae7a216789d68cdf1acf67c1bc18eb9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 30 Mar 2026 12:00:20 +0000 Subject: [PATCH 2/2] Factor out common FP predicate operand validation Extract a shared fp_unary_operand helper lambda that parses and validates the single FloatingPoint operand common to all unary FP handlers. This removes the duplicated arity and type checks from fp.abs, fp.isNaN, fp.isInfinite, fp.isNormal, fp.isZero, fp.isSubnormal, fp.isNegative, and fp.isPositive. The helper sits just before fp.abs so it covers every unary FP handler in the file. Also uses typed expression classes (isnan_exprt, isinf_exprt) consistently in the pre-existing handlers. Co-authored-by: Kiro --- src/solvers/smt2/smt2_parser.cpp | 113 +++++++++---------------------- 1 file changed, 33 insertions(+), 80 deletions(-) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 9b60f8d6563..65d602dc7f8 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -1309,130 +1309,83 @@ void smt2_parsert::setup_expressions() return with_exprt(op[0], op[1], op[2]); }; - expressions["fp.abs"] = [this] { - auto op = operands(); - - if(op.size() != 1) - throw error("fp.abs takes one operand"); - - if(op[0].type().id() != ID_floatbv) - throw error("fp.abs takes FloatingPoint operand"); - - return abs_exprt(op[0]); - }; - - expressions["fp.isNaN"] = [this] { - auto op = operands(); - - if(op.size() != 1) - throw error("fp.isNaN takes one operand"); - - if(op[0].type().id() != ID_floatbv) - throw error("fp.isNaN takes FloatingPoint operand"); - - return unary_predicate_exprt(ID_isnan, op[0]); - }; - - expressions["fp.isInfinite"] = [this] { + // Helper: parse and validate a single FloatingPoint operand. + auto fp_unary_operand = [this](const std::string &name) + { auto op = operands(); if(op.size() != 1) - throw error("fp.isInfinite takes one operand"); + throw error(name + " takes one operand"); if(op[0].type().id() != ID_floatbv) - throw error("fp.isInfinite takes FloatingPoint operand"); + throw error(name + " takes FloatingPoint operand"); - return unary_predicate_exprt(ID_isinf, op[0]); + return std::move(op[0]); }; - expressions["fp.isNormal"] = [this] { - auto op = operands(); - - if(op.size() != 1) - throw error("fp.isNormal takes one operand"); - - if(op[0].type().id() != ID_floatbv) - throw error("fp.isNormal takes FloatingPoint operand"); - - return isnormal_exprt(op[0]); - }; + expressions["fp.abs"] = [fp_unary_operand] + { return abs_exprt{fp_unary_operand("fp.abs")}; }; - expressions["fp.isZero"] = [this] { - auto op = operands(); + expressions["fp.isNaN"] = [fp_unary_operand] + { return isnan_exprt{fp_unary_operand("fp.isNaN")}; }; - if(op.size() != 1) - throw error("fp.isZero takes one operand"); + expressions["fp.isInfinite"] = [fp_unary_operand] + { return isinf_exprt{fp_unary_operand("fp.isInfinite")}; }; - if(op[0].type().id() != ID_floatbv) - throw error("fp.isZero takes FloatingPoint operand"); + expressions["fp.isNormal"] = [fp_unary_operand] + { return isnormal_exprt{fp_unary_operand("fp.isNormal")}; }; - return not_exprt(typecast_exprt(op[0], bool_typet())); + expressions["fp.isZero"] = [fp_unary_operand] + { + return not_exprt{ + typecast_exprt{fp_unary_operand("fp.isZero"), bool_typet{}}}; }; - expressions["fp.isSubnormal"] = [this] + expressions["fp.isSubnormal"] = [fp_unary_operand] { - auto op = operands(); - - if(op.size() != 1) - throw error("fp.isSubnormal takes one operand"); - - if(op[0].type().id() != ID_floatbv) - throw error("fp.isSubnormal takes FloatingPoint operand"); + auto op = fp_unary_operand("fp.isSubnormal"); // subnormal iff finite, non-zero, and not normal -- mirrors // SMT-LIB's own definition of fp.isSubnormal (Theory of // Floating-Point Numbers). // - // Do *not* turn the third reference to `op[0]` below into - // `std::move(op[0])` to avoid the extra copy. Although C++17 + // Do *not* turn the third reference to `op` below into + // `std::move(op)` to avoid the extra copy. Although C++17 // [dcl.init.list]/4 mandates left-to-right evaluation of the // initializer-clauses of a braced-init-list, MSVC's // implementation has been unreliable for direct-list-init of a // constructor (observed under cl.exe on the windows-2022 and // windows-2025 GitHub Actions runners). With the move, the // last clause is sequenced before the earlier clauses read - // `op[0]`; the earlier clauses then see a moved-from `op[0]` - // whose `type()` is `nil`, which trips + // `op`; the earlier clauses then see a moved-from `op` whose + // `type()` is `nil`, which trips // `boolbv_widtht::get_entry(nil)` further down the conversion // pipeline. Three copies are correct, portable, and cheap // (irept uses sharing, so each copy is a refcount bump). return and_exprt{ - isfinite_exprt{op[0]}, - typecast_exprt{op[0], bool_typet{}}, // != 0 - not_exprt{isnormal_exprt{op[0]}}}; + isfinite_exprt{op}, + typecast_exprt{op, bool_typet{}}, // != 0 + not_exprt{isnormal_exprt{op}}}; }; - expressions["fp.isNegative"] = [this] + expressions["fp.isNegative"] = [fp_unary_operand] { - auto op = operands(); - - if(op.size() != 1) - throw error("fp.isNegative takes one operand"); - - if(op[0].type().id() != ID_floatbv) - throw error("fp.isNegative takes FloatingPoint operand"); + auto op = fp_unary_operand("fp.isNegative"); // negative iff sign bit is 1 and not NaN. The explicit // not(isnan) is required: float_bvt::sign_bit returns the raw // top bit of the bit-vector encoding (true for -NaN), whereas // SMT-LIB's fp.isNegative is false for any NaN. Do not drop the // NaN guard. - return and_exprt{not_exprt{isnan_exprt{op[0]}}, sign_exprt{op[0]}}; + return and_exprt{not_exprt{isnan_exprt{op}}, sign_exprt{op}}; }; - expressions["fp.isPositive"] = [this] + expressions["fp.isPositive"] = [fp_unary_operand] { - auto op = operands(); - - if(op.size() != 1) - throw error("fp.isPositive takes one operand"); - - if(op[0].type().id() != ID_floatbv) - throw error("fp.isPositive takes FloatingPoint operand"); + auto op = fp_unary_operand("fp.isPositive"); // positive iff sign bit is 0 and not NaN - return and_exprt{ - not_exprt{isnan_exprt{op[0]}}, not_exprt{sign_exprt{op[0]}}}; + return and_exprt{not_exprt{isnan_exprt{op}}, not_exprt{sign_exprt{op}}}; }; expressions["fp"] = [this] { return function_application_fp(operands()); };