mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-06 22:36:03 +00:00
Code Activity
20079 commits 50 branches 53 tags 183 MiB
Commit graph

271 commits

Author SHA1 Message Date
Nikolaj Bjorner
c387b20ac6 move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07: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
Nuno Lopes
3586b613f7 remove default destructors 2024-10-02 22:20:12 +01:00
Nikolaj Bjorner
826835fd7c fixes to build warnings 2024-09-30 08:23:31 -07:00
Nikolaj Bjorner
3df7299d1e update signature of operator== 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-26 14:47:51 +01:00
Nuno Lopes
499ed5d844 remove unneeded iterator functions 2024-09-23 12:59:04 +01:00
Nuno Lopes
737c2208fa delete more default constructors 
reduces code size by 0.1%
 2024-09-23 12:59:04 +01:00
Nikolaj Bjorner
4b4a28239f Add const qualifiers to comparison operators and update iterator equality checks in various classes 2024-09-23 11:45:11 +01:00
Bruce Mitchener
d66df2616f
Fix some typos. (#7075) 2023-12-29 15:20:06 +00:00
Bruce Mitchener
50e0fd3ba6
Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
Nikolaj Bjorner
dbb4bbe7dc remove debug out 2022-12-13 19:36:55 -08:00
Nikolaj Bjorner
9054e72920 fix #6467 2022-12-13 19:35:20 -08:00
Bruce Mitchener
5014b1a34d Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
Bruce Mitchener
1d9345c3de Fix typos. 2022-08-05 07:40:50 +03:00
Bruce Mitchener
82d853e5f8 Use = delete to delete special methods. 
This provides a better experience than just marking them as
private and leaving them as undefined symbols.
 2022-08-02 09:23:14 +03:00
Jakob Rath
79ee543d25 Move tbv to util 2022-08-01 18:37:11 +03:00
Bruce Mitchener
5d0dea05aa
Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
Nuno Lopes
73a24ca0a9 remove '#include <iostream>' from headers and from unneeded places 
It's harmful to have iostream everywhere as it injects functions in the compiled files
 2022-06-17 14:10:19 +01:00
Nikolaj Bjorner
011c1b2dd2 remove refs to bare_str 2022-04-09 12:06:27 +02:00
Nikolaj Bjorner
f053daa051 fix #5906 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-20 11:24:42 -07:00
Alexander Traud
1d45a33163
fix one typo and two misunderstandings for doxygen (#5633) 2021-10-29 15:35:05 +02:00
Nuno Lopes
f1e0d5dc8a remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
Nikolaj Bjorner
4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nuno Lopes
d6ce9cce95 fix clang warnings 2021-02-19 10:59:22 +00:00
Nuno Lopes
5e034e495f fix compiler warnings 2021-02-19 10:33:41 +00:00
Nikolaj Bjorner
8f577d3943 remove ast_manager get_sort method entirely 2021-02-02 13:57:01 -08:00
Nikolaj Bjorner
3ae4c6e9de refactor get_sort 2021-02-02 04:45:54 -08:00
Nikolaj Bjorner
22b0c3aa70 add priority queue to instantiation 2021-01-31 16:17:36 -08:00
Nikolaj Bjorner
f71204c222 fix #4879 2020-12-12 13:37:25 -08:00
Nikolaj Bjorner
8cb30d0505 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-12 12:21:34 -08:00
Nikolaj Bjorner
89fb55a864 fix #4890 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-12-12 12:20:53 -08:00
Nikolaj Bjorner
43ddb08332 fix #4874 2020-12-08 12:08:07 -08:00
Nikolaj Bjorner
430b4ea252 fix #4870 2020-12-07 17:52:56 -08:00
Nikolaj Bjorner
27dac3e1a0 fix #4844 2020-12-07 05:54:50 -08:00
Nikolaj Bjorner
6f63f8761c
optimizations to bv-solver and euf-egraph (#4698) 
* additional bit-vector propagators

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* rename restrict (not a keyword, but well) #4694, tune euf

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add pb rewriting to pb2bv #4697

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-20 06:47:27 -07:00
Nikolaj Bjorner
cfa7c733db
fixing #4670 (#4682) 
* fixing #4670

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* init

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* arrays

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* arrays

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* arrays

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-10 04:35:11 -07:00
Nikolaj Bjorner
00491148f0 string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-20 10:22:57 -07:00
Nuno Lopes
bb26f219fe remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
Nuno Lopes
23e6adcad3 fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string 2020-07-11 20:24:45 +01:00
Nikolaj Bjorner
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
a0de244487 pleay nice with alignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-26 23:29:42 -07:00
Nikolaj Bjorner
a884201d62 remove using insert_if_not_there2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-25 15:08:51 -07:00
Nikolaj Bjorner
4651bffafc fix #3831 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-09 17:45:05 -07:00
Nikolaj Bjorner
6e7e53e25c block selected configurations from HORN tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-07 19:14:01 -07:00
Nikolaj Bjorner
35f184a6b9 fix #3826 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-07 14:39:54 -07:00
Nikolaj Bjorner
b66360d0b5 fix #3809 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-07 11:15:34 -07:00
Nikolaj Bjorner
8dac9b7b94 fix #3814 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-07 10:40:36 -07:00
Nikolaj Bjorner
9bb579c5c8 fix #3814 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-06 19:43:32 -07:00
Nikolaj Bjorner
2b929cb31e fix #3797 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-06 17:36:35 -07:00
Nikolaj Bjorner
4b2e5ecca0 fix #3797 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-06 17:36:35 -07:00