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

248 commits

Author SHA1 Message Date
Lev Nachmanson
82958565ed handle the case with no roots in add_zero_assumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
08ca76533a improve log_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
b088b3e7c0 log for smtrat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
0179ed855d use indexed root expressions id add_zero_assumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
50e4452e62 add coefficients from the elim_vanishing to m_todo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
f0b292dd16 remove unused method 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
d088bd669e t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
5dd3034000 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
f60d62794a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
905210b165 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
50d8a8049a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
37a5df8d95 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
602e7e906b t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
235c9b5d5a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
5bb0bf94c9 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
a9c84c7950 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
b4850019f2 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
4e38c440bd t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
b2a1293fe2 better state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
d93caa9c7f unsound lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
07501f7c1f change logic NRA->ALL in log_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:55 -08:00
Lev Nachmanson
e980f92a9e enable always add all coeffs in nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:35:25 +01:00
Lev Nachmanson
351c0401fb restore the method behavior 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:21 +01:00
Lev Nachmanson
d9ca739499 restore single cell 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:21 +01:00
Nikolaj Bjorner
2337e68169 fix #7822 2025-08-27 09:17:55 -07:00
Lev Nachmanson
cf8a17a6ae restore the square-free check 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-11 13:16:37 -07:00
Lev Nachmanson
e33dc47d83 remove unused square-free check 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-11 07:24:42 -07:00
Lev Nachmanson
8598a74cca rename add_lcs to add_lc 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-08 11:02:30 -07:00
Lev Nachmanson
88293bf45b get the finest factorizations before project 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-08-08 11:02:30 -07:00
Lev Nachmanson
d2990e2f68 use usize to suppress the data loss warnings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-07-02 14:42:55 -07:00
Nikolaj Bjorner
f544dd4ab2 deal with warnings 
@levnach - there are some additional warnings.
You could revert the change to std_vector or use usize() that I added to vector.h. Look at build logs from the pipelines or actions or figure out how to add a continuous AI script to fixup build warnings (I tried a few times earlier on but the features available to do this were not for laymen).
 2025-07-02 10:59:56 -07:00
Lev Nachmanson
8f88bf9998 use is_square_free_at_sample instead of is_well_oriented 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-17 07:22:03 -07:00
Lev Nachmanson
f2912b25a2 remove debug output 2025-06-17 07:22:03 -07:00
Lev Nachmanson
0e71a9d11c comment and restore 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-17 07:22:03 -07:00
Lev Nachmanson
84c8a93ca5 renaming 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-17 07:22:03 -07:00
Lev Nachmanson
945eef7ab6 work on well-orientedness 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-17 07:22:03 -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
Lev Nachmanson
f89e133d52
revert the behavior of add_zero_assumption (#7631) 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-28 16:07:46 -07:00
Lev Nachmanson
e4897fff00 replace Exists by ForAll in the mathematica lemmas 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-27 12:32:37 -07:00
Lev Nachmanson
39df8999c8 enable shorterter mathematica printouts in nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-27 12:23:32 -07:00
Nikolaj Bjorner
92065462b4 use std::exception as base class to z3_exception 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-04 11:08:15 -08:00
Nuno Lopes
3586b613f7 remove default destructors 2024-10-02 22:20:12 +01:00
Lev Nachmanson
fa1a2cdc1e disable simple check in nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-09-23 10:10:46 -07:00
Nikolaj Bjorner
a3f35b6830 Add command to set initial value hints for solver in various components 2024-09-18 17:48:03 +03:00
Nikolaj Bjorner
b84b4e7f9a fix attribute order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 11:38:27 -07:00
Nikolaj Bjorner
49ba3bc12f address compiler warnings gcc-13 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 11:33:54 -07:00
Kirill A. Korinsky
cff1e9233f
Avoid broken stack at few places (#7353) 
* Avoid broken stack by degree_lit_num_lt

* Avoid broken stack by fix_dl_var_tactic

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 10:02:54 -07:00
Lev Nachmanson
f2d35ddc5e more cleanup 2024-08-12 08:32:01 -10:00
Lev Nachmanson
8999e1a340 use standard name conventions and add file headers 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-12 08:29:06 -10:00
Lev Nachmanson
33f0256e20 cleanup 2024-08-11 12:45:36 -10:00