mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 10:35:36 +00:00
Code Activity
20607 commits 46 branches 56 tags 170 MiB
Commit graph

96 commits

Author SHA1 Message Date
Lev Nachmanson
8577877d13 call levelwise on a correct set of polynomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
3ebac99ff1 add stats to track levelwise calls 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
92577c39f6 rebase with master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
387bd49ae3 normalize before pushing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
8a3e05e507 fix an assert statement 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:42 -10:00
Lev Nachmanson
3cb6ed6227 fixing factoring and hitting NOT_IMPLEMENTED on ir_ord 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
f0dde9d3ee t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
5ac4b8d06d add parameter to suppress/enable levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
da66586a9d t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
e9d0addb32 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
35fac9c578 remove a parameter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
8f726c11e6 work on seed_properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
5da5bed466 rename explain::main_operator to compute_conflict_explanation 2026-01-31 15:56:41 -10:00
Lev Nachmanson
e6aeb027ca define indexed root expression 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
51778e3ef7 refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
8cb7373c21 refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
0ccdbf96e5 use new display functions 2026-01-31 15:56:41 -10:00
Lev Nachmanson
b53317bb9a t1 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:40 -10:00
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
Lev Nachmanson
7de648ff81 remove unused *_signed_project() methods 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-02 18:46:16 -10:00
Lev Nachmanson
97f7e6fac4 remove the debug print 2025-11-24 07:54:06 -10:00
Lev Nachmanson
784ea42521 optionally call add_zero_assumption on a vanishing discriminant 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
ac58f53703 restart projection when found a non-trivial nullified polynomial, and remove is_square_free 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
82f0cfb7cc refactoring 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
26a472fb3c remove unused code 2025-11-24 06:41:06 -10:00
Lev Nachmanson
0886513de1 remve add_zero_assumption from pcs() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
fe6b777638 improve logging 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
ebecfb8e6f handle the case with no roots in add_zero_assumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
6856a61a83 use indexed root expressions id add_zero_assumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
eeb83d48dc add coefficients from the elim_vanishing to m_todo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
573ab2bbbf remove unused method 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
c6eb9d7eb7 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
8e4557647f t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
a512005d5c better state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
f49f5376b0 unsound lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
efd5d04af5 enable always add all coeffs in nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-24 17:47:16 -07:00
Lev Nachmanson
a179286183 restore the method behavior 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-15 16:44:13 -07:00
Lev Nachmanson
1921260c42 restore single cell 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-15 16:44:13 -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
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
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
Nuno Lopes
3586b613f7 remove default destructors 2024-10-02 22:20:12 +01:00
Nikolaj Bjorner
b84b4e7f9a fix attribute order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 11:38:27 -07:00