Add fp.isSubnormal, fp.isNegative, fp.isPositive to SMT2 parser#8889
Merged
Conversation
tautschnig
requested review from
TGWDB,
kroening,
martin-cs and
peterschrammel
as code owners
kroening
reviewed
Mar 24, 2026
kroening
reviewed
Mar 24, 2026
There was a problem hiding this comment.
Pull request overview
Adds support for three missing SMT-LIB FP predicates (fp.isSubnormal, fp.isNegative, fp.isPositive) in the SMT2 parser by lowering them to compound expressions over existing internal FP predicates, and introduces a regression test to exercise the new parse paths.
Changes:
- Implement
fp.isSubnormal,fp.isNegative, andfp.isPositiveinsmt2_parsert::setup_expressions(). - Add a new regression test case under
regression/smt2_solver/fp-predicates/to check satisfiability and NaN behavior.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 9 comments.
| File | Description |
|---|---|
| src/solvers/smt2/smt2_parser.cpp | Adds parser handlers for the three FP predicates via existing internal expressions. |
| regression/smt2_solver/fp-predicates/fp-predicates1.smt2 | New SMT2 input covering the new predicates (sat + NaN checks). |
| regression/smt2_solver/fp-predicates/fp-predicates1.desc | Registers the new regression test and expected output. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8889 +/- ##
===========================================
- Coverage 80.57% 80.56% -0.01%
===========================================
Files 1708 1708
Lines 189217 189212 -5
Branches 73 73
===========================================
- Hits 152460 152446 -14
- Misses 36757 36766 +9 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
fp.isSNP
branch
2 times, most recently
from
3a0d0b4 to
2c49481
Compare
Collaborator
|
Put the tests into |
Collaborator
Author
Done. |
kroening
approved these changes
May 26, 2026
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 <kiro-agent@users.noreply.github.com>
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 <kiro-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implement the three missing FP predicates in the SMT2 parser:
These are expressed as compound expressions using existing predicates, requiring no back-end changes.