mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-29 23:33:38 +00:00
Code Activity

refactor: extract run_fp_test helper in fpa.cpp

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-26 23:54:17 +00:00
parent f2e00b3589
commit cf0ffa2673
1 changed files with 33 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

82
src/test/fpa.cpp
View file

@ -9,71 +9,55 @@ Copyright (c) 2025 Microsoft Corporation
#include "util/debug.h" #include "util/debug.h"
#include <string.h> #include <string.h>
static void run_fp_test(const char * assertion, bool expect_sat) {
Z3_context ctx = Z3_mk_context(nullptr);
const char * result = Z3_eval_smtlib2_string(ctx, assertion);
if (expect_sat) {
ENSURE(strstr(result, "sat") != nullptr);
ENSURE(strstr(result, "unsat") == nullptr);
} else {
ENSURE(strstr(result, "unsat") != nullptr);
}
ENSURE(strstr(result, "invalid") == nullptr);
Z3_del_context(ctx);
}
// Test that fp.to_real produces correct values for denormal floating-point numbers. // Test that fp.to_real produces correct values for denormal floating-point numbers.
// Regression test for: incorrect model with (_ FloatingPoint 2 24) and fp.to_real. // Regression test for: incorrect model with (_ FloatingPoint 2 24) and fp.to_real.
// Denormal numbers require subtracting the normalization shift (lz) from the exponent; // Denormal numbers require subtracting the normalization shift (lz) from the exponent;
// without this fix, denormals in fp.to_real were ~2^lz times too large. // without this fix, denormals in fp.to_real were ~2^lz times too large.
static void test_fp_to_real_denormal() { static void test_fp_to_real_denormal() {
Z3_context ctx;
// Test 1: the specific denormal from the bug report (fp #b0 #b00 #b00111011011111001011101) // Test 1: the specific denormal from the bug report (fp #b0 #b00 #b00111011011111001011101)
// has fp.to_real ~= 0.232, which must NOT be > 1.0 // has fp.to_real ~= 0.232, which must NOT be > 1.0
ctx = Z3_mk_context(nullptr); run_fp_test(
{ "(set-option :model_validate true)\n"
const char * spec = "(assert (> (fp.to_real (fp #b0 #b00 #b00111011011111001011101)) 1.0))\n"
"(set-option :model_validate true)\n" "(check-sat)\n",
"(assert (> (fp.to_real (fp #b0 #b00 #b00111011011111001011101)) 1.0))\n" false);
"(check-sat)\n";
const char * result = Z3_eval_smtlib2_string(ctx, spec);
ENSURE(strstr(result, "unsat") != nullptr);
ENSURE(strstr(result, "invalid") == nullptr);
}
Z3_del_context(ctx);
// Test 2: denormal with leading significand bit = 1, fp.to_real should be 0.5 // Test 2: denormal with leading significand bit = 1, fp.to_real should be 0.5
// (fp #b0 #b00 #b10000000000000000000000) in (_ FloatingPoint 2 24) // (fp #b0 #b00 #b10000000000000000000000) in (_ FloatingPoint 2 24)
ctx = Z3_mk_context(nullptr); run_fp_test(
{ "(set-option :model_validate true)\n"
const char * spec = "(assert (= (fp.to_real (fp #b0 #b00 #b10000000000000000000000)) (/ 1.0 2.0)))\n"
"(set-option :model_validate true)\n" "(check-sat)\n",
"(assert (= (fp.to_real (fp #b0 #b00 #b10000000000000000000000)) (/ 1.0 2.0)))\n" true);
"(check-sat)\n";
const char * result = Z3_eval_smtlib2_string(ctx, spec);
ENSURE(strstr(result, "sat") != nullptr);
ENSURE(strstr(result, "unsat") == nullptr);
ENSURE(strstr(result, "invalid") == nullptr);
}
Z3_del_context(ctx);
// Test 3: denormal with significand bit pattern giving fp.to_real = 0.125 // Test 3: denormal with significand bit pattern giving fp.to_real = 0.125
// (fp #b0 #b00 #b00100000000000000000000) in (_ FloatingPoint 2 24) // (fp #b0 #b00 #b00100000000000000000000) in (_ FloatingPoint 2 24)
ctx = Z3_mk_context(nullptr); run_fp_test(
{ "(set-option :model_validate true)\n"
const char * spec = "(assert (= (fp.to_real (fp #b0 #b00 #b00100000000000000000000)) (/ 1.0 8.0)))\n"
"(set-option :model_validate true)\n" "(check-sat)\n",
"(assert (= (fp.to_real (fp #b0 #b00 #b00100000000000000000000)) (/ 1.0 8.0)))\n" true);
"(check-sat)\n";
const char * result = Z3_eval_smtlib2_string(ctx, spec);
ENSURE(strstr(result, "sat") != nullptr);
ENSURE(strstr(result, "unsat") == nullptr);
ENSURE(strstr(result, "invalid") == nullptr);
}
Z3_del_context(ctx);
// Test 4: a normal value (fp #b0 #b01 #b11111111111111111111111) must be > 1.0 // Test 4: a normal value (fp #b0 #b01 #b11111111111111111111111) must be > 1.0
// This is the maximum finite normal number in (_ FloatingPoint 2 24) // This is the maximum finite normal number in (_ FloatingPoint 2 24)
ctx = Z3_mk_context(nullptr); run_fp_test(
{ "(set-option :model_validate true)\n"
const char * spec = "(assert (> (fp.to_real (fp #b0 #b01 #b11111111111111111111111)) 1.0))\n"
"(set-option :model_validate true)\n" "(check-sat)\n",
"(assert (> (fp.to_real (fp #b0 #b01 #b11111111111111111111111)) 1.0))\n" true);
"(check-sat)\n";
const char * result = Z3_eval_smtlib2_string(ctx, spec);
ENSURE(strstr(result, "sat") != nullptr);
ENSURE(strstr(result, "unsat") == nullptr);
ENSURE(strstr(result, "invalid") == nullptr);
}
Z3_del_context(ctx);
} }
void tst_fpa() { void tst_fpa() {