mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 19:26:53 +00:00
Code Activity
21779 commits 42 branches 58 tags 185 MiB
Commit graph

21779 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
1b9f27a798 patch definitions, add pretty print support 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-13 22:39:32 +02:00
Nikolaj Bjorner
fc3bd95cc2 AI slop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-13 21:01:22 +02:00
Lev Nachmanson
fc2c5c7f58 fix the order of parameter evaluation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-13 21:01:22 +02:00
Lev Nachmanson
e1db3c0b17 fixing the order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-13 21:01:22 +02:00
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
dependabot[bot]
d6d1d7f19c Bump actions/checkout from 4 to 5 (#7954) 
Bumps [actions/checkout](https://github.com/actions/checkout) from 4 to 5.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](https://github.com/actions/checkout/compare/v4...v5)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: '5'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@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
Nikolaj Bjorner
e9a2766e6c remove AI slop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-06 13:53:37 -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
dependabot[bot]
3ce8aca411
Bump actions/checkout from 4 to 5 (#7954) 
Bumps [actions/checkout](https://github.com/actions/checkout) from 4 to 5.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](https://github.com/actions/checkout/compare/v4...v5)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: '5'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2025-10-04 01:22:52 -07:00
Nikolaj Bjorner
c8bdbd2dc4 remove directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-03 11:58:57 -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
5d8fcaa3ee update clang format 2025-10-02 10:39:37 -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
0881a71ed2 update format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-30 15:42:01 -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
Ruijie Fang
d86c049df2 Make things compile 2025-09-29 21:52:54 -05:00
Ruijie Fang
c791694af8
Distinguish betwee Lambda and Quantifier in Expr.java 2025-09-29 21:48:33 -05:00
Ruijie Fang
121f66c19c
Distinguish between Quantifier and Lambda in AST.java 2025-09-29 21:47:11 -05:00
Nikolaj Bjorner
253a7245d0 add analysis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-28 13:05:04 +03:00