mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-04 12:40:23 +00:00
Code Activity
20075 commits 44 branches 58 tags 187 MiB
Commit graph

16888 commits

Author SHA1 Message Date
Nikolaj Bjorner
0e068e4567
Update finite_set_value_factory.cpp 2025-10-16 13:16:30 +02:00
Nikolaj Bjorner
d3e262af85
Use register_value instead of direct set insertion 
Replaced direct insertion into set with register_value calls.
 2025-10-16 12:56:05 +02:00
Nikolaj Bjorner
48a8269a8d
Refactor finite_set_value_factory for value handling 2025-10-16 12:54:22 +02:00
Nikolaj Bjorner
ab642f4c89
Rename member variable from m_util to u 2025-10-16 12:49:08 +02:00
Nikolaj Bjorner
295d02397b
Add SASSERT for finite set check in factory 
Added assertion to check if the sort is a finite set.
 2025-10-16 12:48:50 +02:00
Nikolaj Bjorner
75749dc441
Update finite_set_value_factory.h 2025-10-16 12:47:59 +02:00
copilot-swe-agent[bot]
8c68432675 Fix build error by restoring array_decl_plugin include and implementation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-10-15 20:18:37 +00:00
Nikolaj Bjorner
1f6f4c14c0
Change family ID for finite_set_value_factory 2025-10-15 21:59:47 +02:00
Nikolaj Bjorner
8b55214817
Simplify empty set creation in finite_set_value_factory 
Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic.
 2025-10-15 21:59:14 +02:00
copilot-swe-agent[bot]
ea3dc7e217 Implement finite_set_value_factory using array_util to create singleton sets 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-10-15 19:56:32 +00:00
Nikolaj Bjorner
430deb511a
Update copyright information in finite_set_value_factory.h 
Updated copyright year from 2006 to 2025.
 2025-10-15 21:33:30 +02:00
Nikolaj Bjorner
698e71283c
Update copyright and add TODOs in finite_set_value_factory 
Updated copyright information and added TODO comments for handling in finite_set_value_factory methods.
 2025-10-15 21:33:02 +02:00
copilot-swe-agent[bot]
605ee863e1 Remove unused dl_decl_plugin variable and include 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-10-15 19:24:32 +00:00
copilot-swe-agent[bot]
bcc7076ebf Add finite_set_value_factory implementation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-10-15 19:19:24 +00: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
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