mirror of
https://github.com/Z3Prover/z3
synced 2026-07-26 17:02:38 +00:00
Move SMTLIB2 verdict unit tests to z3test regressions
These tests fed a fixed SMTLIB2 string to Z3_eval_smtlib2_string and checked a sat/unsat verdict. They are now data-driven regression files under z3test regressions/smt2 (with .expected.out ground truth), so remove them from the C++ test suite: - fpa.cpp: removed entirely (all tests transferred) - seq_rewriter.cpp: removed the two seq.foldl model-validation tests - simplifier.cpp: removed the sat.smt QF_UFBV predicate model-validation test - mod_factor.cpp: removed the const-array store-chain unsat test The API-constructed mod/idiv internalization-order tests remain in mod_factor.cpp. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
This commit is contained in:
Nikolaj Bjorner
parent
8a9beaf882
commit
1d83ecb9de
6 changed files with 0 additions and 267 deletions
|
|
@ -60,7 +60,6 @@ add_executable(test-z3
|
|||
f2n.cpp
|
||||
finite_set.cpp
|
||||
finite_set_rewriter.cpp
|
||||
fpa.cpp
|
||||
factor_rewriter.cpp
|
||||
finder.cpp
|
||||
fixed_bit_vector.cpp
|
||||
|
|
|
|||
147
src/test/fpa.cpp
147
src/test/fpa.cpp
|
|
@ -1,147 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2025 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
// Regression tests for floating-point arithmetic encoding and model generation.
|
||||
|
||||
#include "api/z3.h"
|
||||
#include "util/debug.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.
|
||||
// Regression test for: incorrect model with (_ FloatingPoint 2 24) and fp.to_real.
|
||||
// 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.
|
||||
static void test_fp_to_real_denormal() {
|
||||
// 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
|
||||
run_fp_test(
|
||||
"(set-option :model_validate true)\n"
|
||||
"(assert (> (fp.to_real (fp #b0 #b00 #b00111011011111001011101)) 1.0))\n"
|
||||
"(check-sat)\n",
|
||||
false);
|
||||
|
||||
// Test 2: denormal with leading significand bit = 1, fp.to_real should be 0.5
|
||||
// (fp #b0 #b00 #b10000000000000000000000) in (_ FloatingPoint 2 24)
|
||||
run_fp_test(
|
||||
"(set-option :model_validate true)\n"
|
||||
"(assert (= (fp.to_real (fp #b0 #b00 #b10000000000000000000000)) (/ 1.0 2.0)))\n"
|
||||
"(check-sat)\n",
|
||||
true);
|
||||
|
||||
// Test 3: denormal with significand bit pattern giving fp.to_real = 0.125
|
||||
// (fp #b0 #b00 #b00100000000000000000000) in (_ FloatingPoint 2 24)
|
||||
run_fp_test(
|
||||
"(set-option :model_validate true)\n"
|
||||
"(assert (= (fp.to_real (fp #b0 #b00 #b00100000000000000000000)) (/ 1.0 8.0)))\n"
|
||||
"(check-sat)\n",
|
||||
true);
|
||||
|
||||
// Test 4: a normal value (fp #b0 #b01 #b11111111111111111111111) must be > 1.0
|
||||
// This is the maximum finite normal number in (_ FloatingPoint 2 24)
|
||||
run_fp_test(
|
||||
"(set-option :model_validate true)\n"
|
||||
"(assert (> (fp.to_real (fp #b0 #b01 #b11111111111111111111111)) 1.0))\n"
|
||||
"(check-sat)\n",
|
||||
true);
|
||||
}
|
||||
|
||||
// Regression test for soundness bug in to_fp (from real) with symbolic real interval.
|
||||
// When the rounding mode is RTZ and the real variable is constrained to an interval
|
||||
// that includes the exact rational value of a float, Z3 should return SAT.
|
||||
// This was broken because mk_to_real computed 2^(1/|exp|) instead of 1/(2^|exp|)
|
||||
// for floats with negative exponents, causing a conflict in the NRA solver.
|
||||
static void test_to_fp_from_real_interval() {
|
||||
// The interval (-4127125/16777216, -16508499/67108864] contains -16508499/67108864
|
||||
// which is the exact rational value of fp #b1 #b01111100 #b11110111110011001010011.
|
||||
// to_fp(RTZ, r) for r in this closed interval must equal that float.
|
||||
run_fp_test(
|
||||
"(set-logic QF_FPLRA)\n"
|
||||
"(declare-const x Float32)\n"
|
||||
"(assert (= x (fp #b1 #b01111100 #b11110111110011001010011)))\n"
|
||||
"(declare-const r Real)\n"
|
||||
"(assert (and (> r (- (/ 4127125.0 16777216.0))) (<= r (- (/ 16508499.0 67108864.0)))))\n"
|
||||
"(declare-const w Float32)\n"
|
||||
"(assert (= w ((_ to_fp 8 24) RTZ r)))\n"
|
||||
"(assert (= x w))\n"
|
||||
"(check-sat)\n",
|
||||
true);
|
||||
}
|
||||
|
||||
// Preserve the signed value of the internal exponent when converting a symbolic
|
||||
// unsigned bit-vector. In-range values must not take the overflow path.
|
||||
static void test_to_fp_unsigned_exponent_width_boundary() {
|
||||
run_fp_test(
|
||||
"(set-logic QF_BVFP)\n"
|
||||
"(set-option :model_validate true)\n"
|
||||
"(declare-const high (_ BitVec 13))\n"
|
||||
"(assert (or (= high #b1111111111110) (= high #b1111111111111)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 2 11) RTN high) (fp #b0 #b10 #b1111111111)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 2 11) RTZ high) (fp #b0 #b10 #b1111111111)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 2 11) RTP high) (_ +oo 2 11)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 2 11) RNE high) (_ +oo 2 11)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 2 11) RNA high) (_ +oo 2 11)))\n"
|
||||
"(declare-const small (_ BitVec 13))\n"
|
||||
"(assert (or (= small #b0000000000001) (= small #b0000000000010)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 2 11) RTN small)\n"
|
||||
" (ite (= small #b0000000000001)\n"
|
||||
" (fp #b0 #b01 #b0000000000)\n"
|
||||
" (fp #b0 #b10 #b0000000000))))\n"
|
||||
"(check-sat)\n",
|
||||
true);
|
||||
}
|
||||
|
||||
static void test_to_fp_unsigned_common_widths() {
|
||||
run_fp_test(
|
||||
"(set-logic QF_BVFP)\n"
|
||||
"(set-option :model_validate true)\n"
|
||||
"(declare-const high (_ BitVec 32))\n"
|
||||
"(assert (or (= high #xfffffffe) (= high #xffffffff)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 8 24) RTN high)\n"
|
||||
" (fp #b0 #b10011110 #b11111111111111111111111)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 8 24) RTZ high)\n"
|
||||
" (fp #b0 #b10011110 #b11111111111111111111111)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 8 24) RTP high)\n"
|
||||
" (fp #b0 #b10011111 #b00000000000000000000000)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 8 24) RNE high)\n"
|
||||
" (fp #b0 #b10011111 #b00000000000000000000000)))\n"
|
||||
"(assert (= ((_ to_fp_unsigned 8 24) RNA high)\n"
|
||||
" (fp #b0 #b10011111 #b00000000000000000000000)))\n"
|
||||
"(check-sat)\n",
|
||||
true);
|
||||
}
|
||||
|
||||
static void test_recfun_defined_function_soundness() {
|
||||
run_fp_test(
|
||||
"(set-option :model_validate true)\n"
|
||||
"(declare-fun fixedAdd () Int)\n"
|
||||
"(declare-fun variableAdd () Int)\n"
|
||||
"(define-fun-rec $$add$$ ((a Int) (b Int)) Int\n"
|
||||
" (ite (= 0 b) 2 (- a (+ 0 (- fixedAdd b)))))\n"
|
||||
"(assert (= fixedAdd (* 9 fixedAdd)))\n"
|
||||
"(assert (= 1 ($$add$$ 1 3)))\n"
|
||||
"(check-sat)\n",
|
||||
false);
|
||||
}
|
||||
|
||||
void tst_fpa() {
|
||||
test_fp_to_real_denormal();
|
||||
test_to_fp_from_real_interval();
|
||||
test_to_fp_unsigned_exponent_width_boundary();
|
||||
test_to_fp_unsigned_common_widths();
|
||||
test_recfun_defined_function_soundness();
|
||||
}
|
||||
|
|
@ -198,7 +198,6 @@
|
|||
X(finite_set) \
|
||||
X(finite_set_rewriter) \
|
||||
X(seq_split) \
|
||||
X(fpa) \
|
||||
X(seq_regex_bisim) \
|
||||
X(term_enumeration) \
|
||||
X(lcube) \
|
||||
|
|
|
|||
|
|
@ -4,7 +4,6 @@ Copyright (c) 2025 Microsoft Corporation
|
|||
|
||||
#include "api/z3.h"
|
||||
#include "util/util.h"
|
||||
#include <string>
|
||||
|
||||
// x mod 7 = 0 & (x*y) mod 7 != 0 should be unsat
|
||||
// Exercises: mod internalization path (is_mod with numeric divisor)
|
||||
|
|
@ -61,31 +60,7 @@ static void test_mod_factor_idiv_path() {
|
|||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
static void test_const_array_store_chain_unsat() {
|
||||
Z3_config cfg = Z3_mk_config();
|
||||
Z3_context ctx = Z3_mk_context(cfg);
|
||||
const char* script = R"(
|
||||
(set-logic QF_ABV)
|
||||
(declare-const x (_ BitVec 8))
|
||||
(declare-const y (_ BitVec 8))
|
||||
(define-fun A0 () (Array (_ BitVec 2) (_ BitVec 8)) ((as const (Array (_ BitVec 2) (_ BitVec 8))) x))
|
||||
(define-fun A1 () (Array (_ BitVec 2) (_ BitVec 8)) ((as const (Array (_ BitVec 2) (_ BitVec 8))) y))
|
||||
(declare-const i0 (_ BitVec 2))
|
||||
(declare-const e0 (_ BitVec 8))
|
||||
(declare-const i1 (_ BitVec 2))
|
||||
(declare-const e1 (_ BitVec 8))
|
||||
(assert (distinct x y))
|
||||
(assert (= (store A0 i0 e0) (store A1 i1 e1)))
|
||||
(check-sat)
|
||||
)";
|
||||
std::string resp = Z3_eval_smtlib2_string(ctx, script);
|
||||
ENSURE(resp.find("unsat") != std::string::npos);
|
||||
Z3_del_config(cfg);
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
void tst_mod_factor() {
|
||||
test_mod_factor_mod_path();
|
||||
test_mod_factor_idiv_path();
|
||||
test_const_array_store_chain_unsat();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -23,11 +23,8 @@ Tests:
|
|||
#include "ast/reg_decl_plugins.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "api/z3.h"
|
||||
#include "smt/smt_context.h"
|
||||
#include <cstring>
|
||||
#include <iostream>
|
||||
#include <sstream>
|
||||
#include <string>
|
||||
|
||||
// Build a single-char string literal expression.
|
||||
|
|
@ -35,72 +32,6 @@ static expr_ref mk_str(ast_manager& m, seq_util& su, unsigned c) {
|
|||
return expr_ref(su.str.mk_string(zstring(c)), m);
|
||||
}
|
||||
|
||||
static void test_seq_foldl_nth_model_validation() {
|
||||
Z3_context ctx = Z3_mk_context(nullptr);
|
||||
char const* result =
|
||||
Z3_eval_smtlib2_string(ctx,
|
||||
"(set-option :model_validate true)\n"
|
||||
"(declare-const initial Int)\n"
|
||||
"(declare-const all (Seq Int))\n"
|
||||
"(declare-const final Int)\n"
|
||||
"(declare-const elements (Seq Int))\n"
|
||||
"(define-fun all_sums ((prev_sums (Seq Int)) (elem Int)) (Seq Int)\n"
|
||||
" (seq.++ (seq.unit (+ (seq.nth prev_sums 0) elem)) prev_sums))\n"
|
||||
"(assert (= all (seq.foldl all_sums (seq.unit initial) elements)))\n"
|
||||
"(assert (= final (seq.nth all 0)))\n"
|
||||
"(assert (= initial 0))\n"
|
||||
"(assert (= final 6))\n"
|
||||
"(check-sat)\n"
|
||||
"(get-model)\n");
|
||||
ENSURE(std::strstr(result, "sat") != nullptr);
|
||||
ENSURE(std::strstr(result, "invalid model") == nullptr);
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
static void test_seq_foldl_foldli_scalar_model_validation() {
|
||||
Z3_context ctx = Z3_mk_context(nullptr);
|
||||
char const* result =
|
||||
Z3_eval_smtlib2_string(ctx,
|
||||
"(set-option :model_validate true)\n"
|
||||
"(push)\n"
|
||||
"(declare-fun f (Int Int) Int)\n"
|
||||
"(declare-const il (Seq Int))\n"
|
||||
"(assert (= (seq.foldl f 0 il) 5))\n"
|
||||
"(check-sat)\n"
|
||||
"(pop)\n"
|
||||
"(push)\n"
|
||||
"(declare-const il (Seq Int))\n"
|
||||
"(declare-const F (Array Bool Int Bool))\n"
|
||||
"(assert (= (seq.foldl F true il) true))\n"
|
||||
"(assert (> (seq.len il) 0))\n"
|
||||
"(assert (not (= F ((as const (Array Bool Int Bool)) true))))\n"
|
||||
"(check-sat)\n"
|
||||
"(pop)\n"
|
||||
"(push)\n"
|
||||
"(declare-fun f (Int Int Int) Int)\n"
|
||||
"(declare-const il (Seq Int))\n"
|
||||
"(assert (= (seq.foldli f 0 0 il) 5))\n"
|
||||
"(check-sat)\n"
|
||||
"(pop)\n"
|
||||
"(push)\n"
|
||||
"(declare-const il (Seq Int))\n"
|
||||
"(declare-const F (Array Int Bool Int Bool))\n"
|
||||
"(assert (= (seq.foldli F 5 true il) true))\n"
|
||||
"(assert (> (seq.len il) 0))\n"
|
||||
"(assert (not (= F ((as const (Array Int Bool Int Bool)) true))))\n"
|
||||
"(check-sat)\n"
|
||||
"(pop)\n");
|
||||
ENSURE(std::strstr(result, "unknown") == nullptr);
|
||||
ENSURE(std::strstr(result, "invalid model") == nullptr);
|
||||
unsigned sat_count = 0;
|
||||
std::istringstream in{std::string(result)};
|
||||
for (std::string line; std::getline(in, line);)
|
||||
if (line == "sat")
|
||||
++sat_count;
|
||||
ENSURE(sat_count == 4);
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
void tst_seq_rewriter() {
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
|
|
@ -365,8 +296,5 @@ void tst_seq_rewriter() {
|
|||
}
|
||||
}
|
||||
|
||||
test_seq_foldl_nth_model_validation();
|
||||
test_seq_foldl_foldli_scalar_model_validation();
|
||||
|
||||
std::cout << "tst_seq_rewriter: all tests passed\n";
|
||||
}
|
||||
|
|
|
|||
|
|
@ -212,26 +212,6 @@ static void test_array() {
|
|||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
static void test_sat_smt_ufbv_predicate_model_validation() {
|
||||
Z3_context ctx = Z3_mk_context(nullptr);
|
||||
const char* result =
|
||||
Z3_eval_smtlib2_string(ctx,
|
||||
"(set-logic QF_UFBV)\n"
|
||||
"(set-option :sat.smt true)\n"
|
||||
"(set-option :model_validate true)\n"
|
||||
"(declare-fun p ((_ BitVec 4)) Bool)\n"
|
||||
"(declare-const x (_ BitVec 4))\n"
|
||||
"(declare-const y (_ BitVec 4))\n"
|
||||
"(assert (xor (p x) (p y)))\n"
|
||||
"(assert (bvuge x (_ bv1 4)))\n"
|
||||
"(assert (bvult y (_ bv1 4)))\n"
|
||||
"(check-sat)\n"
|
||||
"(get-model)\n");
|
||||
ENSURE(std::strstr(result, "sat") != nullptr);
|
||||
ENSURE(std::strstr(result, "invalid model") == nullptr);
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
void tst_simplifier() {
|
||||
|
||||
test_array();
|
||||
|
|
@ -239,5 +219,4 @@ void tst_simplifier() {
|
|||
test_datatypes();
|
||||
test_bool();
|
||||
test_skolemize_bug();
|
||||
test_sat_smt_ufbv_predicate_model_validation();
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue