mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-10 02:50:55 +00:00
Code Activity
20509 commits 50 branches 56 tags 170 MiB
Commit graph

17135 commits

Author SHA1 Message Date
Lev Nachmanson
97f7e6fac4 remove the debug print 2025-11-24 07:54:06 -10:00
Lev Nachmanson
98a3d2af15 remove the exit statement 2025-11-24 07:51:11 -10:00
Lev Nachmanson
cc3328be8d disable add_zero_disc(disc) by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41: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
2768962aa8 improve log_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
0ee272a9d1 log for smtrat 
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
847f471015 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
36c711d95b t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
c8959dc67a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
7eb18771c2 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
bce477530a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
27f4150e2e t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
5fec29f4cd t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
54c23bb446 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
d0fea0b714 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
3c07fa40a6 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
Nikolaj Bjorner
662e4293a5 check cancelation in invariant checker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-23 09:09:55 -08:00
Nikolaj Bjorner
7395152632
factor out coi, use polynomial elaboration for nlsat solver (#8039) 
* factor out coi, use polynomial elaboration for nlsat solver

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

* remove unused functionality

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

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-23 08:59:55 -08:00
Nikolaj Bjorner
59eec25102 fix #8024 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-16 10:08:21 -08:00
Nikolaj Bjorner
81211254eb strengthen filter for unknown by checking relevancy of parents #8022 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 17:14:00 -08:00
Nikolaj Bjorner
bf6ff56fd6 update package lock 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 16:56:18 -08:00
Nikolaj Bjorner
bd2ead977e add back statistics to smt-parallel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 16:49:22 -08:00
Josh Berdine
5690be8cfc
Make rcf is_rational and is_rational_function operations handle zero (#8025) 
The representation of the zero rcf numeral is nullptr, and the is_rational
and is_rational_function operations are not expecting to be called with
nullptr. But there isn't a way to test for that in the API, other than
checking if Z3_rcf_num_to_string returns "0".

This patch adds a couple conditions so that is_rational and
is_rational_function operations handle zero. Maybe this isn't the desired
change. For instance, the is_zero operation could instead be exposed in the
API and preconditions added to the relevant operations.

Signed-off-by: Josh Berdine <josh@berdine.net>
 2025-11-15 16:36:32 -08:00
Josh Berdine
28b31cfe91
Add Z3_fpa_is_numeral to the API (#8026) 
This is analogous to Z3_fpa_is_numeral_nan, Z3_fpa_is_numeral_inf, etc. and
can be needed to check that inputs are valid before calling those functions.

Signed-off-by: Josh Berdine <josh@berdine.net>
 2025-11-15 16:21:08 -08:00
Josh Berdine
43525481f0
Add check that argument of Z3_is_algebraic_number is_expr (#8027) 
To make sure that the `to_expr` cast is safe.

Signed-off-by: Josh Berdine <josh@berdine.net>
 2025-11-15 16:19:39 -08:00
Nikolaj Bjorner
6d19c045d8 fix infinite loop in update function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 15:47:33 -08:00
Nikolaj Bjorner
11fb5c7dc4 comment out parameter check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-04 16:11:58 -08:00
Nikolaj Bjorner
2503b35dc6 check propagate ineqs setting before applying simplifier 2025-11-04 15:57:02 -08:00
Copilot
fc7660d0b5
Add missing string replace operations to Java API (#8011) 
* Initial plan

* Add C API and Java bindings for str.replace_all, str.replace_re, str.replace_all_re

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

* Add test for new Java string replace operations

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

* Remove author field from test file header

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

* Delete examples/java/StringReplaceTest.java

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-04 09:48:20 -08:00
Lev Nachmanson
c845c9810a add tests showing shortcomings of factorization 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-03 10:54:07 -10:00
Lev Nachmanson
38a346fa1b change logic NRA->ALL in log_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-01 08:47:30 -10:00
Nikolaj Bjorner
c88295a7c7 fix C++ example and add polymorphic interface for C++ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-29 03:08:49 -07:00
Nikolaj Bjorner
1b9a636910 fix build break introduced when adding support for polymorphic datatypes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-28 18:55:47 -07:00
Copilot
3570073c29
Add missing mkLastIndexOf method and CharSort case to Java API (#8002) 
* Initial plan

* Add mkLastIndexOf method and CharSort support to Java API

- Added mkLastIndexOf method to Context.java for extracting last index of sub-string
- Added Z3_CHAR_SORT case to Sort.java's create() method switch statement
- Added test file to verify both fixes work correctly

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

* Fix author field in test file

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

* Delete examples/java/TestJavaAPICompleteness.java

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-28 15:46:48 -07: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
887ecc0c98 throttle grobner method more actively 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-22 21:36:22 -07:00
Lev Nachmanson
58e64ea826 try exponential delay in grobner 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-22 17:00:16 -07:00