Draft
Conversation
Collaborator
tautschnig
commented
Mar 28, 2026
tautschnig
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
fmaf does x*y+z with two roundings instead of one. For fmaf(1+eps, 1+eps, -(1+2*eps)), double rounding gives 0 but true FMA gives eps^2 > 0. Needs __CPROVER_fmaf built-in. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Three tests for fp.fma which is not yet supported by the SMT2 parser. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Documents that fp.fma is not supported by CBMC's SMT2 solver parser. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add float_utilst::fma(a, b, c) which computes round(a*b + c) with a single rounding. The product a*b is computed exactly using double-width multiplication, then c is added using the same alignment and addition logic as add_sub, and the result is rounded once. This differs from separate mul+add which rounds the product before adding c, potentially losing precision in the intermediate result. Add unit tests verifying: - Basic FMA operations (2*3+4 = 10, etc.) - FMA vs mul+add precision difference (0x1.fffffep+23 * 0x1.000002p+0 + 1) - FMA for remainder computation (fma(-5, y, x) gives more precise x-5*y) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Thread FMA support through the entire pipeline: - Add ID_floatbv_fma to irep_ids and floatbv_fma_exprt expression class (ternary: multiply_lhs, multiply_rhs, addend) - Add __CPROVER_fma/__CPROVER_fmaf/__CPROVER_fmal built-in declarations and lowering to floatbv_fma_exprt in the C front-end - Replace the C library fma/fmaf/fmal implementations (which incorrectly used x*y+z with two roundings) with calls to the built-in - Add propositional back-end support (boolbv_floatbv_fma.cpp) using float_utilst::fma - Add SMT2 back-end support using fp.fma (FPA theory) or float_bv fallback - Mark floatbv_fma as already adjusted in adjust_float_expressions - Add expr2c display support - Add regression test verifying FMA precision vs separate mul+add - Add fp.fma parser entry to smt2_solver. - Implement FMA in float_bvt with single rounding: Proper fused multiply-add: multiply at double width (exact), align and add the third operand (exact), then round once. This matches the float_utilst::fma implementation and ensures the remainder algorithm's correctness (the exact intermediate result is representable, so single rounding returns it exactly). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Test IEEE 754 FMA special cases that were previously handled by the C library model but are now handled by float_utilst::fma: - fma(NaN, y, z) = NaN - fma(x, NaN, z) = NaN - fma(x, y, NaN) = NaN - fma(0, inf, z) = NaN (0 * inf undefined) - fma(inf, 0, z) = NaN - fma(inf, x, -inf) = NaN (inf + (-inf) undefined) - fma(inf, x, z) = +inf for finite z - fma(x, y, inf) = +inf for finite x*y Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Verify that --smt2 --fpa emits fp.fma (not bitvector encoding) for both normal FMA operations and special cases (NaN, infinity). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Run main_03.c (NaN, infinity, 0*inf) through an external SMT solver with --smt2 --fpa to verify the fp.fma emission produces correct verification results, not just correct syntax. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
With concurrently running tests we might have had z3 vs cvc5 test execution scribble over each other, resulting in non-reproducible test failures.
Float-typed mod is handled by convert_floatbv_mod_rem, not here. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The existing ID_floatbv_rem was used for both fmod and IEEE remainder, but these have different semantics (truncation vs round-to-nearest-even). Add ID_floatbv_mod for fmod, keeping ID_floatbv_rem for IEEE remainder. Update adjust_float_expressions to recognize the new ID, expr2c to display it, and the incremental SMT2 back-end. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Replace the old __sort_of_CPROVER_remainder helper functions (which used extended precision as a workaround) with direct calls to __CPROVER_fmod and __CPROVER_remainder built-ins. These lower to ID_floatbv_mod and ID_floatbv_rem respectively, which are handled natively by the solvers. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The propositional back-end crashed on IEEE remainder because to_signed_integer has a precondition requiring round-to-zero, but remainder uses round-to-even. Fix: use round_to_integral instead of to_signed_integer. The round_to_integral function respects the current rounding mode (ROUND_TO_ZERO for fmod, ROUND_TO_EVEN for IEEE remainder). Set the rounding mode correctly in boolbv_floatbv_mod_rem based on whether the expression is ID_floatbv_mod or ID_floatbv_rem. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
SMT2 with FPA theory: add convert_floatbv_mod using fp.roundToIntegral with roundTowardZero for fmod. IEEE remainder already used fp.rem. SMT2 without FPA theory (float_bvt): add mod() and rem() methods that compute x - round_to_integer(x/y) * y with appropriate rounding. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Verify concrete values and add float-overflow-check and nan-check. Mark fmodl as THOROUGH due to long double divider size The integer significand divider for long double (80-bit, e=15) is 32834 bits wide, causing the test to take ~15 minutes. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Verify concrete values and add float-overflow-check and nan-check. Mark remainderl as THOROUGH due to long double divider size The integer significand divider for long double is 32834 bits wide, causing the test to take ~4 minutes. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Test remainder with inputs where fp division rounds the quotient across an integer boundary. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Test IEEE 754 tie-breaking behavior when quotient is near n+0.5. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Test the Java % operator on doubles, which uses fmod semantics. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
SMT-LIB tests: - fp-rem-nonstandard/fp-rem1: fp.rem(3.0, 2.0) correctness (KNOWNBUG) - fp-rem-nonstandard/fp-rem-nonstandard1: fp.rem on non-standard sort - Tests from Z3 issues z3#2381 and z3#6553 (correctness, KNOWNBUG) C test: - Float-rem1: remainderf(3.0f, 2.0f) (KNOWNBUG) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add float_utilst::fma(a, b, c) which computes round(a*b + c) with a single rounding. The product a*b is computed exactly using double-width multiplication, then c is added using the same alignment and addition logic as add_sub, and the result is rounded once. This differs from separate mul+add which rounds the product before adding c, potentially losing precision in the intermediate result. Add unit tests verifying: - Basic FMA operations (2*3+4 = 10, etc.) - FMA vs mul+add precision difference (0x1.fffffep+23 * 0x1.000002p+0 + 1) - FMA for remainder computation (fma(-5, y, x) gives more precise x-5*y) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Replace the extended-precision approach with FMA-based comparison for
the IEEE remainder correction step. FMA computes x - n*y with a single
rounding (the product n*y is exact internally), which provides a much
stronger soundness argument than the extended-precision approach.
Soundness proof sketch (included as comments in the code):
(a) The tentative n from round_to_integral(fp_div(x,y)) is off by at
most 1 from the correct n_correct.
(b) fma(-n_correct, y, x) = R_correct exactly, because IEEE 754
specifies that the remainder is exactly representable.
(c) fma(-n_wrong, y, x) = round(R_wrong). Since |R_wrong| >= |y|/2
and |R_correct| <= |y|/2, the gap |R_wrong| - |R_correct| >= ulp(y),
which exceeds the FMA rounding error of 1/2 ulp(R_wrong).
(d) In the true tie case (|R_correct| == |y|/2), both FMA results are
exact and equal in magnitude. The rint-chosen even n is kept, which
is correct per IEEE 754 tie-breaking.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add __CPROVER_fmodf16, __CPROVER_remainderf16, __CPROVER_fmaf16 declarations and typechecker support. This enables verification of floating-point remainder on _Float16, where the integer significand division produces a manageable formula (~16K variables vs ~194K for float). Add a CORE regression test that verifies |remainder(x,y)| <= |y|/2 for ALL finite _Float16 inputs (completes in ~3s with MiniSat). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add a Coq/Flocq proof (doc/proofs/fma_remainder.v) that machine-checks correctness properties of the FMA-based IEEE remainder algorithm. Fully proved (zero admits, Coq 8.18 + Flocq): remainder_format: x - n*y is exactly representable in FLX format when |x - n*y| <= |y|/2 (both exponent orderings). fma_remainder_exact: round(x - n*y) = x - n*y, so FMA returns the exact remainder without rounding. comparison_step: the wrong candidate (n +/- 1) has strictly larger |remainder| than the correct one in exact arithmetic. Add nearest_int_small, fmod_then_remainder, and rounding_preserves_remainder_comparison. Move comparison_step out of the FMA_Remainder section. Remove dead comments. Add nearest_integer_from_ratio_lt for ey > ex case. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Port core theorems using native int type with div/rem and real_zpow for integer exponents. All proved with zero mk_thm. Update check_proof.sh to verify both Coq and HOL Light. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add a CI workflow that triggers when float implementation or proof files change. It verifies: 1. Coq proofs compile (zero admits) 2. HOL Light proofs pass (zero mk_thm) 3. _Float16 exhaustive tests pass (linking proofs to implementation) Add _Float16 tests for specific proved properties: - special_cases: fmod(inf,y)=NaN, fmod(x,0)=NaN, etc. - fmod_bound: |fmod(x,y)| < |y| for all finite inputs Add cross-reference comments in float_utilst::rem mapping each proof theorem to its corresponding _Float16 test. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Catalogue 55 floating-point issues from Z3 (Floats label), CVC5, and Bitwuzla. Extract SMT-LIB reproducers and categorize by FP operation. This document will track CBMC's behavior on each issue and guide regression test creation. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
SMT-LIB tests (regression/smt2_solver/): - fp-nan-eq-uf: NaN equality through UFs (Z3#6728) - fp-sub-fma-rounding: fp.sub with all rounding modes (Z3#7162) - fp-div-fma: fp.div with RTN and non-standard sorts - fp/fp-overflow1: overflow to infinity (Z3#4673) - fp/fp-to-real-unsupported1: documents fp.to_real gap C tests (regression/cbmc/): - Float-nan-uf1, Float-sub-rounding1, Float-div-rounding1, Float-fma1, Float-overflow-inf1 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Document 4 bugs/gaps found in CBMC: 1. fp.rem always returns +0.0 in SMT2 solver 2. remainderf/remainder crashes CBMC C front-end 3. fp.fma not supported in SMT2 solver 4. fp.to_real not supported in SMT2 solver Update status of all explicitly listed issues and several additional Z3 Floats-labeled issues. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Reviewed branch tautschnig/cleanup/floatbv-mod-rem which addresses: - fp.rem (complete rewrite with FMA-based algorithm + Coq proof) - fmod vs remainder distinction (new ID_floatbv_mod) - remainderf/remainder crash (new __CPROVER_remainder built-in) - FMA implementation (float_utilst::fma, boolbv, smt2 output) Remaining gaps with effort estimates: - Quick wins (~8-12h): fp.fma parser, fp.isSubnormal/isNegative/ isPositive, to_fp from BV, fp.to_sbv/to_ubv crash, roundToIntegral non-standard sort fix - Medium (~4-8h): fp.min/max, fp.to_real basic support - Larger (1-3d): fp.sqrt New bug found: fp.to_sbv/fp.to_ubv crash with non-RTZ rounding modes due to hard precondition in float_utilst::to_integer(). Root cause identified for roundToIntegral non-standard sort bug: magic number 2^f exceeds max representable value when f >= 2^(e-1). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Implement the three missing FP predicates in the SMT2 parser: - fp.isSubnormal: not NaN, not infinite, not zero, and not normal - fp.isNegative: sign bit is 1 and not NaN - fp.isPositive: sign bit is 0 and not NaN These are expressed as compound expressions using existing predicates, requiring no back-end changes. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Support the 1-argument form of to_fp: ((_ to_fp eb sb) BitVec) which reinterprets a bitvector as a floating-point value without rounding. The parser now peeks at the next token after the first operand to distinguish the 1-arg form from the 2-arg form. The reinterpret cast goes through bv_typet to ensure bit-level identity (not value conversion). Turns KNOWNBUG test fp-to-fp-bv-unsupported1 into CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The solver crashed with an invariant violation in float_utilst::to_integer() which requires round_to_zero. Fix by first rounding to integral with the given rounding mode, then converting to integer with RTZ. This is semantically correct: fp.to_sbv(rm, x) = to_sbv(RTZ, roundToIntegral(rm, x)) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
For sorts where 2^f exceeds the maximum representable value (e.g., (_ FloatingPoint 2 6) where f=5 but max value is 3.96875), the magic-number trick fails because the magic number is not representable. Fix: detect this case by constructing the magic number with ROUND_TO_PLUS_INF (so overflow produces infinity rather than clamping). When the magic number is infinity, fall back to converting to a wider format where the trick works, rounding there, and converting back. Turns KNOWNBUG tests roundToIntegral-nonstandard1 and roundToIntegral-combined1 into CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Document 4 fixes implemented: - fp.isSubnormal/isNegative/isPositive predicates - to_fp from BitVec reinterpret cast - fp.to_sbv/fp.to_ubv crash fix - fp.roundToIntegral non-standard sort fix Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Create 29 additional SMT-LIB tests covering catalogued issues from Z3, CVC5, and Bitwuzla (excluding fp.isZero(-0) test, committed separately). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
fp.isZero(-0) should be true but returns false because the implementation checks bitvector non-zero instead of using float_utilst::is_zero() which handles both +0 and -0. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Total test count: 47 SMT-LIB tests + 9 C tests covering all 55 catalogued external solver issues. KNOWNBUG tests document remaining gaps: fp.fma, fp.to_real, fp.rem, fp.isZero(-0), to_fp overflow. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Fill gaps for issues that previously had no tests (excluding fp.fma test, committed separately). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
71 total tests: 48 in fp-issues/ (31 CORE, 17 KNOWNBUG) + 14 in other fp-* directories + 9 C tests. Only 6 issues intentionally without tests (Z3-specific features, performance, incremental). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The previous implementation used not(typecast_to_bool) which checks if the bitvector is all-zeros, but -0 has sign bit 1 so it was incorrectly reported as non-zero. Fix: use ieee_float_equal with +0, which correctly treats -0 == +0 per IEEE 754 semantics. Turns KNOWNBUG test z3-isZero-neg-zero into CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Implement fp.min and fp.max in the SMT2 parser as compound expressions: - NaN handling: if either operand is NaN, return the other - Comparison: use fp.lt/fp.gt for normal ordering - Zero tie-breaking: fp.min prefers negative sign, fp.max prefers positive Fix fp.isZero to use ieee_float_equal with +0 instead of bitvector non-zero check, correctly handling -0. New CORE tests: fp-min-max, z3-4880-min-neg-zero, z3-isZero-neg-zero KNOWNBUG→CORE: z3-isZero-neg-zero Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add IEEE 754 square root support: - New ID_floatbv_sqrt expression type - float_utilst::sqrt() implementation using nondeterministic result with SAT constraints: r >= 0, r*r (rounded down) <= x <= r*r (rounded up) - Parser entry for fp.sqrt (rounding mode + one FP operand) - boolbv dispatch to float_utilst::sqrt() Special cases handled: - sqrt(NaN) = NaN - sqrt(negative) = NaN - sqrt(+/-0) = +/-0 - sqrt(+inf) = +inf Note: fp.sqrt should also be added to the C front-end in a future change (currently sqrtf/sqrt use a C library model with __VERIFIER_nondet). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Document two known limitations of the current fp.sqrt implementation: 1. fp-sqrt-rtz: Rounding mode is ignored — sqrt(2.0) with RTZ returns the RNE result (0x3FB504F3) instead of the correctly rounded-down value (0x3FB504F2). The constraint r*r_low <= x <= r*r_high finds a valid square root but doesn't enforce the rounding direction. 2. fp-sqrt-subnormal: Incorrect result for subnormal inputs. The constraint-based approach doesn't correctly handle subnormals where the relationship between r*r and x is affected by subnormal precision loss. Additional known gaps not yet tested: - SMT2 output converter (smt2_conv.cpp) doesn't handle ID_floatbv_sqrt - float_bvt::convert() doesn't handle ID_floatbv_sqrt (constant folding) - C front-end sqrtf/sqrt still uses __VERIFIER_nondet model, not built-in Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
fminf(+0, -0) returns +0 instead of -0. The C library model uses (f <= g) ? f : g which doesn't distinguish -0 from +0 in the tie case. Needs __CPROVER_fminf built-in mapping to fp.min semantics. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
sqrtf with FE_TOWARDZERO gives wrong result. The C library __VERIFIER_nondet model doesn't correctly handle non-RNE rounding modes. Needs __CPROVER_sqrtf built-in. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Structured into three phases: - Phase 1 (~1h): after floatbv-mod-rem branch lands — fp.fma parser, fp.rem/fma/remainder KNOWNBUG→CORE - Phase 2 (~8-12h): independent — fp.sqrt rounding/subnormal fixes, C front-end built-ins for sqrt/fmin/fmax - Phase 3 (~2-3d): larger — fp.to_real, to_fp from Real, quantifiers Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The original tests used 1e40 (scientific notation) which is not valid SMT-LIB syntax. Using the full decimal representation works correctly: to_fp of a very large constant properly overflows to infinity. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The sqrt implementation now correctly: - Finds r_low (floor of sqrt) via SAT constraints - Selects r_high = r_low + ulp for RTP when not exact - Returns r_low for RTZ/RTN/RNE (correct for RNE in most cases) - Handles all special cases (NaN, -0, +inf, negative) Known remaining issues (documented via KNOWNBUG tests): - RTZ/RTP: r_low constraint is too loose due to RTZ multiplication rounding. Needs exact squaring via wider format (conversion() precondition issue to be debugged). - Subnormals: same root cause. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Completed: - 3.3: to_fp from large Real constant — was already working with proper SMT-LIB syntax (full decimal, not scientific notation). KNOWNBUG→CORE for z3-8183 and cvc5-12371. Partially completed: - 2.1/2.2: fp.sqrt rounding — works for RNE and exact cases. RTZ/RTP/subnormal still broken due to imprecise squaring constraints. Root cause: conversion() precondition prevents using wider format for exact squaring. Needs further debugging. Deferred to next session: - 2.3: __CPROVER_sqrtf C built-in - 2.4: __CPROVER_fminf/__CPROVER_fmaxf C built-ins - fp.sqrt RTZ/RTP/subnormal fix (needs conversion() investigation) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Root cause of previous crash: conversion() mutates spec as a side effect. Fixed by saving/restoring spec around each conversion() call, and pre-computing is_infinity(r_high) before the spec change. The wide-format squaring (2x significand width) now works correctly, giving exact r_low^2 and r_high^2 for precise distance comparison. Rounding mode selection: - RTZ/RTN: use r_low (floor of sqrt) - RTP: use r_high unless exact - RNE: use whichever of r_low/r_high is closer; ties to even - RNA: use whichever is closer; ties away from zero Previous KNOWNBUG tests had wrong expected values. Both now CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add fmin/fmax as proper CBMC built-in operations:
- New ID_floatbv_min/ID_floatbv_max expression types
- __CPROVER_fmin{,f,l} and __CPROVER_fmax{,f,l} built-in headers
- Type-checking in c_typecheck_expr.cpp
- boolbv handler using float_utilst predicates for NaN handling
and sign-bit tie-breaking
- SMT2 output: emits fp.min/fp.max when using FPA theory
- C library math.c updated to use built-ins
The key fix: fmin(+0, -0) now correctly returns -0 per IEEE 754-2019
(the old C model used (f <= g) ? f : g which returned +0).
Turns KNOWNBUG Float-fmin-zero-sign1 into CORE.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Replace the old __VERIFIER_nondet + __CPROVER_assume model for
sqrtf/sqrt/sqrtl with proper __CPROVER_sqrt{,f,l} built-ins that
map to ID_floatbv_sqrt.
Changes:
- cprover_builtin_headers.h: declare __CPROVER_sqrt{,f,l}
- c_typecheck_expr.cpp: type-check sqrt built-ins, create
binary_exprt with ID_floatbv_sqrt
- adjust_float_expressions.cpp: add rounding mode as 3rd operand
- math.c: replace ~150 lines of nondet model with 3 one-liners
- smt2_conv.cpp: emit (fp.sqrt RM x) for external SMT solvers
The old model had known issues with non-RNE rounding modes and
subnormals (documented in comments). The new built-in handles all
rounding modes correctly via wide-format exact squaring.
Turns KNOWNBUG Float-sqrt-rounding1 into CORE.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The test had (declare-fun c (_ FloatingPoint 8 24)) which is missing the () for the empty argument list. Use declare-const instead. The quantifier is still ignored (pre-existing limitation) but the test now parses correctly. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The SMT2 parser now handles ((_ to_fp eb sb) RM (/ p q)) where p and q are decimal constants. Each is parsed as a base-10 number, converted to ieee_floatt, and then p/q is computed with the specified rounding. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
fp.to_real: encode as wide signed integer (2^e + f bits) representing the exact real value scaled by 2^(f+bias). Real constants in comparisons are converted to the same scaled representation. to_fp from (/ p q): evaluate rational constants at parse time. Turns 5 KNOWNBUG tests into CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Implement a finite-domain quantifier instantiation strategy based on: Reynolds et al., CADE 2013 (doi:10.1007/978-3-642-38574-2_26) Niemetz et al., CAV 2018 (doi:10.1007/978-3-319-96142-2_16) For finite-domain types (floatbv, bitvectors) where bounded-range extraction fails, instantiate over a relevant value set: type boundary values + ground terms/free symbols from the formula + sign-flipped FP variants. Sound for both universal (conjunction) and existential (disjunction) quantifiers. Incomplete but sufficient for common FP verification patterns. Turns 3 KNOWNBUG quantifier tests into CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
1. Enable bv_refinementt in smt2_solver. Add fp.rem/fmod refinement with concrete evaluation via ieee_floatt. Skip refinement for constant operands (use exact float_bvt encoding instead). 2. Fix float_bvt::rem tie-breaking: use even-quotient rule when |best_alt| == |result| (same fix as float_utilst::rem). 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
1 participant
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.