mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-12 03:44:07 +00:00
Code Activity
20410 commits 53 branches 56 tags 172 MiB
Commit graph

102 commits

Author SHA1 Message Date
Copilot
2436943794
Standardize for-loop increments to prefix form (++i) (#8199) 
* Initial plan

* Convert postfix to prefix increment in for loops

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix member variable increment conversion bug

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update API generator to produce prefix increments

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-14 19:55:31 -08:00
LeeYoungJoon
0a93ff515d
Centralize and document TRACE tags using X-macros (#7657) 
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros

* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md

* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled

* trace: improve trace tag handling system with hierarchical tagging

- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
  (class names and descriptions to be refined in a future update)

* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals

* trace : add cstring header

* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py

* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.

* trace : Add TODO comment for future implementation of tag_class activation

* trace : Disable code related to tag_class until implementation is ready (#7663).
 2025-05-28 14:31:25 +01:00
Bruce Mitchener
50e0fd3ba6
Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
Christoph M. Wintersteiger
9d57bdd2ef
Assorted fixes for floats (#6968) 
* Improve 4be26eb543

* Add-on to 0f4f32c5d0

* Fix mk_numeral

* Fix corner-case in fp.div

* Fixes for corner-cases in mk_to_fp_(un)signed

* Fix out-of-range results in mpf_manager::fma

* Further adjustments for fp.to_fp_(un)signed

* fp.to_fp from real can't be NaN

* fp.to_fp from reals: add bounds

* Fix NaN encodings in theory_fpa.

* Fix fp.fma rounding with tiny floats

* Fix literal creation order in theory_fpa
 2023-10-29 17:29:42 -07:00
Nuno Lopes
8ad480ab59 fix compiler warnings 2022-10-12 09:43:50 +01:00
Nuno Lopes
a41520acf1 mpf: fix some string copies 2022-10-11 11:59:29 +01:00
Nuno Lopes
661a1624b4 avoid string copying in mpf_manager::set 2022-10-07 14:03:13 +01:00
Bruce Mitchener
eba29a280d
Use std::hexfloat more. (#6203) 
Previously, we were only using std::hexfloat on Windows on VS2013
and later.

Since std::hexfloat is part of C++11 and we require C++11 to build
the Z3 library, this should be supported everywhere.
 2022-07-29 11:49:56 +02:00
Christoph M. Wintersteiger
d722c73d4c
Fix corner case in MPF FMA (#6075) 2022-06-04 15:55:26 +01:00
Christoph M. Wintersteiger
eadf755628
Fix bonus subtraction in fp.rem. Fixes #4564. Fixes most of #2381. 2020-11-06 20:54:10 +00:00
Christoph M. Wintersteiger
c03c395267
Add missing assertion. Fixes #4642. 2020-10-30 14:09:51 +00:00
Nikolaj Bjorner
2611484525 fix #4642 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-17 08:35:15 -07:00
Christoph M. Wintersteiger
d3ae40130a
Fix rounding bug in mpf_manager. Fixes #2970. 2020-07-16 12:39:12 +00:00
Nuno Lopes
98b5abb1d4 buffer: require a move constructor to avoid copies 
remove unneded copy constructors from several classes
 2020-06-03 11:57:49 +01:00
Nikolaj Bjorner
eacde16b3e fix #3199 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 23:55:44 -07:00
Nikolaj Bjorner
7452e55698 fix #3190 fix #3168 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-08 12:54:03 +01:00
Florian Pigorsch
326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Nikolaj Bjorner
2dc92e2b94 merge with pull request #1557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-07 17:22:49 -07:00
Christoph M. Wintersteiger
793642f48d Fixed MPF to_sbv. Thanks to Florian Schanda for reporting this bug. 2018-04-05 15:23:16 +01:00
Bruce Mitchener
2fa304d8de Remove int64, uint64 typedefs in favor of int64_t / uint64_t. 2018-03-31 14:45:04 +07:00
Christoph M. Wintersteiger
c3ed986031 Fixed RNA FP rounding mode semantics. Fixes #1190 and bugs reported by Youcheng Sun. 2018-02-03 16:46:21 +00:00
Nuno Lopes
468e0207f7 add move constructor to mpf 2017-10-16 00:54:30 +01:00
Nikolaj Bjorner
cae414e575 fixes for #1296, removing COMPILE_TIME_ASSERT 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-09 13:59:44 -07:00
Christoph M. Wintersteiger
05447d612a Bugfixes for fp.to_* operators 2017-09-15 19:56:15 +01:00
Christoph M. Wintersteiger
4ff938f2c1 Fixed MPF fp.rem(0,0,0). Relates to #872. 2017-08-01 16:46:10 +01:00
Nikolaj Bjorner
063b6e9ea5 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 13:24:57 -07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Christoph M. Wintersteiger
ecfd241e19 Injected 3 missing bits of precision into fp.rem. Relates to #872. 2017-07-31 19:53:44 +01:00
Christoph M. Wintersteiger
a59907170d Fixed renormalization in fp.mul. Relates to #872. 2017-07-31 18:34:46 +01:00
Christoph M. Wintersteiger
175f042db8 Fixed renormalization in fp.fma. Relates to #872. 2017-07-28 23:01:01 +01:00
Christoph M. Wintersteiger
e677030b74 Fixed sign bug in mpf fp.fma. Relates to #872. 2017-07-28 21:39:44 +01:00
Christoph M. Wintersteiger
0610392a05 Bugfix for fp.fma. Fixes #872. 2017-07-28 20:16:13 +01:00
Christoph M. Wintersteiger
33ebdc8adc Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872. 2017-07-27 23:08:35 +01:00
Christoph M. Wintersteiger
75b533f050 Fixed normalization shift in MPF rounder. Relates to #872. 2017-07-25 20:29:10 +01:00
Christoph M. Wintersteiger
f1c0ac72e7 Fix for fp.fma encoding. Relates to #872. 2017-07-25 20:29:10 +01:00
Christoph M. Wintersteiger
16b32ecf12 Bugfix for special-case handling in fp.fma. 
Thanks to Florian Schanda for reporting this bug.

(+reversed accidental debug code commit).
 2016-12-09 15:03:31 +00:00
Christoph M. Wintersteiger
9df5c31485 Whitespace 2016-12-09 13:40:46 +00:00
Nikolaj Bjorner
5b497b6249 reduce set of mainly verbose warnings raised by -Wmaybe-uninitialized and unused variable warnings from release mode builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-22 20:25:47 -07:00
Christoph M. Wintersteiger
b3b5c6226b MPF code simplification 2016-06-02 17:12:24 +01:00
Nikolaj Bjorner
96e157e201 fix warnings for unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-17 13:54:22 -07:00
Christoph M. Wintersteiger
89598e0141 Merge pull request #608 from wintersteiger/fprti-rna-fix 
Fix for #586, RNA rounding for fp.roundToIntegral.
 2016-05-16 16:21:35 +01:00
Christoph M. Wintersteiger
99f5269b78 debug output fix 2016-05-16 16:15:44 +01:00
Christoph M. Wintersteiger
44b0a6ddbc Tentative fix for #586. 2016-05-14 18:42:10 +01:00
Christoph M. Wintersteiger
3fde81aea6 Style 2016-05-14 14:29:13 +01:00
Christoph M. Wintersteiger
0ddf2d92fe removed unused variables 2016-05-12 15:20:50 +01:00
Christoph M. Wintersteiger
12a8d0d02b mpf debug cleanup 2016-05-12 15:12:46 +01:00
Christoph M. Wintersteiger
dd83495d5d New implementation of mpf_manager::rem. 
Partially addresses #561
 2016-05-12 14:15:24 +01:00
Christoph M. Wintersteiger
a7c66356ae mpf partial remainder draft 2016-05-03 18:20:18 +01:00
Nikolaj Bjorner
6895cc7cc6 remove apostrophe, issue #582 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-03 07:21:15 -07:00
Nikolaj Bjorner
e375be767d remove apostrophe, issue #582 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-03 07:20:20 -07:00