mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 03:11:30 +00:00
Code Activity
21808 commits 42 branches 58 tags 185 MiB
Commit graph

17805 commits

Author SHA1 Message Date
Filipe Marques
f0421879bb
Expose mk_re_allchar in OCaml API 2026-02-26 16:22:55 +00:00
Nikolaj Bjorner
070f760501
Merge pull request #8748 from Z3Prover/copilot/fix-floating-point-model-validation 
Fix fp.to_real bitvector encoding for denormal floating-point values
 2026-02-26 02:21:20 -08:00
copilot-swe-agent[bot]
b4f7d057d3 Add model_validate and invalid-check to fpa regression tests 
Add (set-option :model_validate true) to each SMT-LIB2 spec in
src/test/fpa.cpp, and add ENSURE checks that the output does not
contain the string "invalid".

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 03:21:33 +00:00
copilot-swe-agent[bot]
add65451fd Add fpa regression test for fp.to_real denormal encoding fix 
Adds src/test/fpa.cpp with test_fp_to_real_denormal() exercising the
bug reported in the issue: denormal floating-point values in
(_ FloatingPoint 2 24) were getting wrong fp.to_real values because
mk_to_real was not subtracting the normalization shift lz from the
exponent.

Tests verify:
- The specific denormal from the bug report is NOT > 1.0
- Two other denormals have correct real values (0.5 and 0.125)
- A normal value is correctly identified as > 1.0

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 22:04:03 +00:00
copilot-swe-agent[bot]
af2e60c069 code-simplifier: fix JavaDoc formatting in Context.java and extract ternary in Solver.cs 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 21:49:23 +00:00
Nikolaj Bjorner
fba1e4b648
Merge pull request #8737 from Z3Prover/copilot/fix-refutational-soundness-bug 
Fix soundness bug: RNE/RNA overflow to ±infinity in symbolic Real-to-FP conversion
 2026-02-25 13:34:59 -08:00
Nikolaj Bjorner
412c56ecc8
Merge pull request #8767 from Z3Prover/copilot/fix-ubv-to-int-bug 
Fix intblast: assert ubv_to_int(compound) = translation equality
 2026-02-25 13:32:40 -08:00
Nikolaj Bjorner
c51f45bf5e
Merge pull request #8766 from Z3Prover/copilot/fix-critical-bugs-from-discussion 
Fix critical static-analysis true positives: null deref, division by zero, dangling pointer
 2026-02-25 09:22:45 -08:00
Lev Nachmanson
a7ea22f24f remove an unnecessary template from levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-25 07:03:23 -10:00
Lev Nachmanson
66d19c4d3f
Merge pull request #8770 from Z3Prover/lws 
Optimizes the substitution of a non-nullified witness by an lc or a disc if they are added to the projection and do not vanish.
 2026-02-25 06:25:58 -10:00
Lev Nachmanson
0835420cc1 change the default of param lws_subs_witness_disc to true 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-24 15:24:35 -10:00
copilot-swe-agent[bot]
4860d57ae9 Fix intblast ubv_to_int bug: add bv2int axioms for compound expressions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 00:46:13 +00:00
copilot-swe-agent[bot]
ae4cb5557a Fix true positive critical bugs from static analysis discussion #8764 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 00:41:59 +00:00
Nikolaj Bjorner
c580bcd4d1
Merge pull request #8762 from TempuraFramework/master 
Add missing Java API for `as-array`
 2026-02-24 13:51:33 -08:00
Ruijie Fang
6b79297252 Add missing Java API method for as-array 2026-02-24 13:55:39 -06:00
Nikolaj Bjorner
23d8bdd47c
Merge pull request #8758 from Z3Prover/copilot/fix-issues-except-rust 
Add missing solver/optimize API methods across Java, .NET, OCaml, Go, and TypeScript bindings
 2026-02-24 11:47:09 -08:00
Lev Nachmanson
0074de0fce improve non-zero witness substitution logic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-24 09:19:13 -10:00
Nikolaj Bjorner
cfb3a01756
Update Solver.cs 2026-02-24 09:58:12 -08:00
copilot-swe-agent[bot]
ce04a24348 Improve TypeScript Optimize documentation for handle index clarity 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 17:28:45 +00:00
copilot-swe-agent[bot]
9802b32a3e Add missing API methods: dimacs, translate, proof, addSimplifier, getLower/getUpper, etc. 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 17:22:17 +00:00
copilot-swe-agent[bot]
575f4a8911 Simplify Go user propagator callbacks with withCallback helper 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 16:48:05 +00:00
Nikolaj Bjorner
e0161b2e2e
Merge pull request #8746 from Z3Prover/copilot/simplify-go-return-logic 
Simplify boolean return in goOnBindingCb
 2026-02-24 08:44:24 -08:00
Nikolaj Bjorner
aaa62efc90
Merge pull request #8725 from Z3Prover/copilot/convert-factor-to-simplifier 
Convert `factor` tactic to a `dependent_expr_simplifier`
 2026-02-24 08:42:30 -08:00
copilot-swe-agent[bot]
de3cf18899 Fix fp.to_real encoding for denormal floating-point values 
The mk_to_real function in fpa2bv_converter.cpp was missing the
normalization shift adjustment (lz) when computing the real-valued
exponent for denormal floating-point numbers.

When unpack(x, sgn, sig, exp, lz, normalize=true) normalizes a denormal
by shifting the significand left by lz positions, the returned exp does
not account for this shift. All other callers (mk_mul, mk_div, mk_fma)
correctly subtract lz from the exponent, but mk_to_real was missing this.

The fix subtracts zero-extended lz from the sign-extended exp to get the
true exponent, matching the convention used by other FP operations.

Fixes incorrect model with (_ FloatingPoint 2 24) and fp.to_real.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 05:22:54 +00:00
copilot-swe-agent[bot]
3feac95119 Simplify boolean return in goOnBindingCb 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 04:42:49 +00:00
Nikolaj Bjorner
8ec15639e0
Merge pull request #8726 from Z3Prover/copilot/convert-cofactor-term-ite-to-simplifier 
Convert `cofactor-term-ite` tactic to a simplifier
 2026-02-23 20:40:23 -08:00
Lev Nachmanson
cf3552c029 suppress witness subs optimization 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-23 09:59:08 -10:00
copilot-swe-agent[bot]
c0fd3513a2 Fix RNE/RNA overflow-to-infinity in Real-to-FP conversion (soundness bug) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-23 04:34:58 +00:00
copilot-swe-agent[bot]
fd424c7afd Delete factor_tactic.cpp (implementation moved to factor_simplifier.cpp) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-23 04:01:34 +00:00
copilot-swe-agent[bot]
afbd038924 Delete cofactor_term_ite_tactic.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-23 03:57:37 +00:00
Nikolaj Bjorner
2ea86d94dc
Merge pull request #8735 from Z3Prover/copilot/fix-discussed-issues 
Add missing API bindings: importModelConverter, OnClause, and user propagator (Go/Java)
 2026-02-22 19:46:11 -08:00
Nikolaj Bjorner
8fbc4ed26d
Merge pull request #8727 from Z3Prover/copilot/expose-max-bv-sharing-simplifier 
Expose max-bv-sharing as a registered simplifier
 2026-02-22 19:40:35 -08:00
Nikolaj Bjorner
0b5480b6c3
Merge pull request #8729 from Z3Prover/copilot/convert-bvarray2uf-to-simplifier 
Convert `bvarray2uf` tactic to a dependent_expr_simplifier
 2026-02-22 19:39:19 -08:00
copilot-swe-agent[bot]
d5030dfe30 Fix unsafe.Pointer usage in Go propagator - use uintptr_t for cgo.Handle 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-23 01:09:07 +00:00
copilot-swe-agent[bot]
0de7af9112 Add missing API bindings: importModelConverter, OnClause, and user propagator 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-23 01:01:26 +00:00
Nikolaj Bjorner
69eab28550
Merge pull request #8730 from Z3Prover/copilot/convert-der-tactic-to-simplifier 
Convert `der` tactic to a `dependent_expr_simplifier`
 2026-02-22 14:04:04 -08:00
copilot-swe-agent[bot]
1d2a76d27b Delete bvarray2uf_tactic.cpp (removed from CMakeLists.txt) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 08:57:39 +00:00
copilot-swe-agent[bot]
57d1667d28 Remove der_tactic.cpp from CMakeLists.txt (file was deleted) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 08:47:14 +00:00
Nikolaj Bjorner
b149f27e82
Delete src/tactic/core/der_tactic.cpp 2026-02-22 00:25:24 -08:00
copilot-swe-agent[bot]
b6e63f06fd Remove old cofactor_term_ite_tactic.cpp, use simplifier-based implementation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 00:45:44 +00:00
copilot-swe-agent[bot]
4f6c0637fc Remove old mk_factor_tactic, rename factor2 to factor 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 00:45:12 +00:00
copilot-swe-agent[bot]
d9d712f1d0 Remove old bvarray2uf_tactic implementation; use simplifier as basis 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 00:43:36 +00:00
copilot-swe-agent[bot]
7c4a3b2c1b Remove old der_tactic implementation; rename mk_der2_tactic to mk_der_tactic 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-22 00:40:49 +00:00
Nikolaj Bjorner
0d553f2ce9
Merge pull request #8712 from Z3Prover/copilot/fix-soundness-issue-conversion 
Fix FPA soundness issue in incremental (push/pop) solving
 2026-02-21 16:26:23 -08:00
copilot-swe-agent[bot]
c18db6080a Convert cofactor-term-ite tactic to also expose as a simplifier 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 23:52:01 +00:00
copilot-swe-agent[bot]
0cc4afa097 Add bvarray2uf_simplifier: convert tactic to simplifier 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 23:50:32 +00:00
copilot-swe-agent[bot]
c78b3d872d Convert der tactic to simplifier: add der_simplifier.h and update der_tactic.h 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 23:49:05 +00:00
copilot-swe-agent[bot]
42d3a13ddf Add factor_simplifier and factor2 tactic wrapping the simplifier 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 23:45:51 +00:00
copilot-swe-agent[bot]
ce905f91c3 Register max_bv_sharing simplifier via ADD_SIMPLIFIER 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-21 23:26:47 +00:00
Toby Shi
f5fba112bc
add parser_context in c++ api 2026-02-21 17:59:44 +08:00