mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 23:14:40 +00:00
Code Activity
20460 commits 50 branches 58 tags 179 MiB
Commit graph

183 commits

Author SHA1 Message Date
Copilot
de825be4c7 Replace fall-through comments with Z3_fallthrough macro (#8219) 
* Initial plan

* Fix switch fall-through warnings with Z3_fallthrough attribute

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-02-18 20:57:31 -08:00
Nikolaj Bjorner
e4697fe18e remove set cardinality operators from array theory. Make final-check use priority levels 
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation.
To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
 2026-02-18 20:56:51 -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
Nikolaj Bjorner
826835fd7c fixes to build warnings 2024-09-30 08:23:31 -07:00
Nikolaj Bjorner
50deece29e fix #7098 2024-01-30 20:38:01 -08:00
Nikolaj Bjorner
c0f80f92ba deal with compiler warnings (unused variables etc) 2023-02-18 17:53:37 -08:00
Nikolaj Bjorner
63f48f8fd4 add options for logging learned lemmas and theory axioms 
- add solver.axioms2files
  - prints negated theory axioms to files. Each file should be unsat
- add solver.lemmas2console
  - prints lemmas to the console.
- remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
 2022-08-08 11:18:56 +03:00
Bruce Mitchener
1d9345c3de Fix typos. 2022-08-05 07:40:50 +03: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
0059e88036 fix #5808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-07 20:10:32 +02:00
Nikolaj Bjorner
9958cab5cc fix #5808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-07 07:43:30 +02: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
Nikolaj Bjorner
026065ff71 streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
Nikolaj Bjorner
a152bb1e80 remove template Context dependency in every trail object 2021-02-08 15:41:57 -08:00
Nikolaj Bjorner
223bffd035 fix #4920 2021-01-09 02:02:50 -08:00
Nikolaj Bjorner
1b768c9b3a fix #4805 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-20 12:11:38 -08:00
Nikolaj Bjorner
c41abf2241 fix #4624 #4633 #4632 #4631 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-13 08:36:16 -07:00
Nikolaj Bjorner
c4204d3365 fix #4330 2020-05-15 10:12:06 -07:00
Nikolaj Bjorner
becf423c77
remove level of indirection for context and ast_manager in smt_theory (#4253) 
* remove level of indirection for context and ast_manager in smt_theory

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

* add request by #4252

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

* move to def

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

* int

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-08 16:46:03 -07:00
Nikolaj Bjorner
2d08baf3d5 fix #4219 2020-05-06 12:20:40 -07:00
Nikolaj Bjorner
029edcfabd fix #4114 2020-04-26 16:17:42 -07:00
Nikolaj Bjorner
31ff658f5e fix #3416 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-19 08:54:08 -07:00
Nikolaj Bjorner
78a1736bd2 prepare symbols to be more abstract, update mbi, delay initialize some modules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:02:08 -08:00
Nikolaj Bjorner
8ec6219010 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-06 09:42:57 +03:00
Nikolaj Bjorner
a92c82d895 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-06 09:42:57 +03:00
Nikolaj Bjorner
e816d16724 fix #2527 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-31 10:09:52 -04:00
Nikolaj Bjorner
de43e05102 fix overflow bug exposed by #2476 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-29 22:34:04 -03:00
Nikolaj Bjorner
3d1c40ce23 fixing #2448 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-02 15:06:34 -07:00
Nikolaj Bjorner
48fc3d752e add clause proof module, small improvements to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 15:49:19 -07:00
Nikolaj Bjorner
94dae2da3a fix fourth bug produced by repros by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-27 18:11:18 -08:00
Nikolaj Bjorner
0b84c60886 fix another bug uncovered by Dunlop, prepare grounds for equality solving within NNFs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 01:25:25 -08:00
Nikolaj Bjorner
4159b987ce purge unused code from theory_pb, fix bug reported by Mark Dunlop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 03:23:57 -08:00
Nikolaj Bjorner
4b35ef29c9 fix #2081 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-13 01:18:03 -08:00
Nikolaj Bjorner
b8d18c6c6d speed-up handling of cnf input to inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-11 20:52:19 -08:00
Nikolaj Bjorner
9c318ed304 fix #2076, add option to handle .cnf files into dimacs parser 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-09 15:43:45 -08:00
Nikolaj Bjorner
0d400a5ad6 fix bit2bool bug reported by Jianying Li 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-04 07:46:53 -08:00
Nikolaj Bjorner
360d6f963e reduce output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 17:05:48 -08:00
Nikolaj Bjorner
bd96eaff47 axiomatize pb-eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 08:26:59 -08:00
Nikolaj Bjorner
f4d03edf22 remove unreachable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:54:30 -08:00
Nikolaj Bjorner
f56749a241 fix #2041, fix #2043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:18:49 -08:00
Bruce Mitchener
373b691709 Use 'override' where possible. 2018-10-02 10:26:38 +07:00
Bruce Mitchener
cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nikolaj Bjorner
3ae0ea8246 add circuit and unate encoding besides sorting option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 21:09:13 -07:00
Nikolaj Bjorner
026265f9a3 fix memory leak in proof production in theory_pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-03 08:55:26 -07:00
Nikolaj Bjorner
dc8ec50137 enable proof objects for PB 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 13:53:55 -07:00
Nikolaj Bjorner
b73aa3642a check with cube and clause 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
8eeaa27cf3 remove interp from documentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-25 07:33:43 -07:00
Nikolaj Bjorner
0708ecb543 dealing with compilers that don't take typename in non-template classes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-23 09:11:33 -07:00
Nikolaj Bjorner
618d394ab5 unreferenced variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-10 09:41:12 +01:00
Nikolaj Bjorner
ad571510f3 disable slow validation code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-09 10:49:32 +01:00