mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-06 12:44:51 +00:00
Code Activity
21876 commits 60 branches 58 tags 216 MiB
Commit graph

17836 commits

Author SHA1 Message Date
Lev Nachmanson
33ae08ab29 fixing the order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-13 21:00:54 +02:00
Nikolaj Bjorner
1344d8f8d7 Remove unused variable 'first' in mpz.cpp 
Removed unused variable 'first' from the function.
 2025-10-13 21:00:54 +02:00
Copilot
0972ab08bb [WIP] Add a mutex to warning.cpp to ensure that warning messages from different threads don't interfere (#7963) 
* Initial plan

* Add mutex to warning.cpp for thread safety

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>
 2025-10-13 21:00:54 +02:00
Philipp Danzinger
a3a8803e64
register finite_set plugin (#7969) 2025-10-13 14:06:58 +02:00
Copilot
df4052ec69
Implement finite_set_decl_plugin with complete operator support and polymorphism infrastructure (#7961) 
* Initial plan

* Implement finite_sets_decl_plugin with all specified operations

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

* Add tests for finite_sets_decl_plugin

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

* Add set.singleton operator to finite_sets_decl_plugin

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

* Refactor finite_sets_decl_plugin to use polymorphic signatures and Array sorts

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

* Rename finite_sets to finite_set everywhere including file names

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

* Rename set.filter to set.select

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

* Refactor finite_set_decl_plugin to use polymorphism_util

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

* Move psig and match method to polymorphism_util

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

* Add MATCH macros and fix is_fully_interp return value

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

* Add is_finite_set helper and parameter count validation

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>
 2025-10-13 10:58:53 +02:00
Lev Nachmanson
641741f3a8 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:30:58 -07:00
Lev Nachmanson
8af9a20e01 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:26:40 -07:00
Lev Nachmanson
6a9520bdc2 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:21:09 -07:00
Lev Nachmanson
8ccf4cd8f7 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:19:24 -07:00
Lev Nachmanson
40b980079b parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:14:02 -07:00
Lev Nachmanson
a41549eee6 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 10:06:43 -07:00
Lev Nachmanson
2b3068d85f parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-07 09:17:12 -07:00
Lev Nachmanson
3a2bbf4802 param eval order 2025-10-07 09:13:21 -07:00
Lev Nachmanson
6e52b9584c param eval 2025-10-07 09:04:24 -07:00
Lev Nachmanson
93ff8c76db parameter evaluation order 2025-10-07 08:53:49 -07:00
Lev Nachmanson
00f1e6af7e parameter eval order 2025-10-07 08:40:24 -07:00
Lev Nachmanson
c154b9df90 param order evaluation 2025-10-07 08:34:56 -07:00
Lev Nachmanson
77c70bf812 param order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 15:52:09 -07:00
Lev Nachmanson
63bb367a10 param order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 15:52:09 -07:00
Lev Nachmanson
5a9663247b fix the order of parameter evaluation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 13:44:19 -07:00
Lev Nachmanson
5ae858f66b fixing the order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 13:44:19 -07:00
Lev Nachmanson
aa5645b54b fixing the order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-06 13:44:19 -07:00
Nikolaj Bjorner
542e015550
Remove unused variable 'first' in mpz.cpp 
Removed unused variable 'first' from the function.
 2025-10-06 13:39:27 -07:00
Copilot
cd1ceb6efe
[WIP] Add a mutex to warning.cpp to ensure that warning messages from different threads don't interfere (#7963) 
* Initial plan

* Add mutex to warning.cpp for thread safety

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>
 2025-10-06 13:38:18 -07:00
Nikolaj Bjorner
7356b5ff88 outline finite_set theory solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-05 16:22:28 -07:00
Nikolaj Bjorner
97c8fb15fa update contract 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-05 14:15:08 -07:00
Nikolaj Bjorner
2ce30019ee remove old files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-05 14:06:36 -07:00
Nikolaj Bjorner
ad7b248956 add outline of axiomatization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-05 14:04:51 -07:00
Nikolaj Bjorner
522be5d8c2 add stub for rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-04 18:14:43 -07:00
Nikolaj Bjorner
fb41fbf5e1 placeholder for finite set signature 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-04 17:30:25 -07:00
Nikolaj Bjorner
e0fca3ba25 placeholder for finite set signature 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-04 17:18:12 -07:00
Nikolaj Bjorner
e137aaa249 add user propagators to opt_solver 2025-10-02 19:44:22 -07:00
Nikolaj Bjorner
0e6b3a922a Add commands for forcing preferences during search 
Add commands:

(prefer <formula>)
- will instruct case split queue to assign formula to true.
- prefer commands added within a scope are forgotten after leaving the scope.

(reset-preferences)
- resets asserted preferences. Has to be invoked at base level.

This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2
 2025-10-02 10:47:10 -07:00
Nikolaj Bjorner
72c89e1a4e fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-30 15:58:48 -07:00
Nikolaj Bjorner
65c9a18c3a fix #7956 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-30 15:41:49 -07:00
Ruijie Fang
339f0cd5f9
Correctly distinguish between Lambda and Quantifier in Z3 Java API (#7955) 
* Distinguish between Quantifier and Lambda in AST.java

* Distinguish betwee Lambda and Quantifier in Expr.java

* Make things compile
 2025-09-30 09:55:14 -07:00
Nikolaj Bjorner
bda98d8da4 fix #7948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-28 12:52:20 +03:00
Nikolaj Bjorner
b7eb21efed fix #7948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-28 12:52:19 +03:00
Wael Boutglay
391880b6fc
Add missing ::z3::sdiv to z3++.h (#7947) 2025-09-25 22:04:15 +03:00
Nikolaj Bjorner
6173a0d025 propagate value initialization to atoms 2025-09-24 11:01:24 +03:00
Nikolaj Bjorner
eae4de075b fix latent bug in factorization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-23 10:47:24 +03:00
Nikolaj Bjorner
04ddade2dd remove stale comment 2025-09-22 04:43:41 +03:00
Nikolaj Bjorner
f5c28a0b76 household cleanup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-22 03:58:04 +03:00
Nikolaj Bjorner
e26f7b900c fix unsound axiom for lower-bounding 2025-09-21 19:24:13 +03:00
Nikolaj Bjorner
dcdae5a61c add smt debug output for nla_core 2025-09-21 19:24:13 +03:00
Nikolaj Bjorner
ce53e06e29
Par (#7945) 
* port parallel

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

* updates

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

* update smt-parallel

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

* cleanup

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

* neat

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

* configuration parameter renaming

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

* config parameters

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

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-21 10:11:04 +03:00
Nikolaj Bjorner
2b5b985492 fix divergence regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-20 02:18:44 -07:00
Nikolaj Bjorner
9876e85a45 turn on max of sums transformation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-20 00:55:37 -07:00
Nikolaj Bjorner
3256d1cc8b fix bug in unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-20 00:44:49 -07:00
Nikolaj Bjorner
0e8648c7d7 fix compile of lp.cpp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-20 00:33:23 -07:00