mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-25 01:31:18 +00:00
Code Activity
21693 commits 39 branches 58 tags 182 MiB
Commit graph

21693 commits

This branch
This branch
All branches
Author SHA1 Message Date
Copilot
2e7f80f597
Add comprehensive algebraic rewrite rules to finite_set_rewriter (#7975) 
* Initial plan

* Add comprehensive rewrite rules for finite set operations

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

* Add comprehensive unit tests for finite set rewrite rules

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

* Fix order of checks in mk_in to handle singleton same element case first

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>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-15 18:46:10 +02:00
Nikolaj Bjorner
4225f1a0f1 prove your first finite set theorem 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-15 18:33:35 +02:00
kper
30878541c8
Changed sort of mk_empty to fix test (#7979) 2025-10-15 17:03:46 +02:00
Nikolaj Bjorner
54980a38d4 fixup theory_finite_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-15 15:02:58 +02:00
Copilot
b4d41ffe81
Complete theory_finite_set.h header and implement finite set theory solver (#7976) 
* Initial plan

* Implement theory_finite_set header and implementation

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

* Add theory registration to smt_setup

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

* Update theory_finite_set.cpp

* Refactor membership_atoms and add elements list

Renamed membership_atoms to membership_elements and added elements list.

* Change membership elements to use enode type

* Update theory_finite_set.cpp

* Fix typo in internalize_atom function

* Update theory_finite_set.cpp

* Refactor final_check_eh by removing comments

Removed redundant comments and cleaned up code.

* Add m_lemmas member to theory_finite_set class

* Improve clause management and instantiation logic

Refactor clause handling and instantiate logic in finite set theory.

* Add friend class declaration for testing

* Add placeholder methods for lemma instantiation

Added placeholder methods for lemma instantiation.

---------

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-15 14:55:08 +02:00
kper
7446112fbe
Implement more cases for finite_set_decl_plugin::are_distinct (#7978) 
* Implement more cases for finite_set_decl_plugin::are_distinct

* Adapted distinctive checks for finite sets
 2025-10-15 14:35:57 +02:00
kper
b24aec3c4c
Fixed tests by making methods public for finite sets (#7977) 2025-10-15 14:03:00 +02:00
Nikolaj Bjorner
f674d22ec8 update description for signature of the theory solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-15 08:54:00 +02:00
dependabot[bot]
e669fbe557
Bump github/codeql-action from 3 to 4 (#7971) 
Bumps [github/codeql-action](https://github.com/github/codeql-action) from 3 to 4.
- [Release notes](https://github.com/github/codeql-action/releases)
- [Changelog](https://github.com/github/codeql-action/blob/main/CHANGELOG.md)
- [Commits](https://github.com/github/codeql-action/compare/v3...v4)

---
updated-dependencies:
- dependency-name: github/codeql-action
  dependency-version: '4'
  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-14 18:08:27 +02:00
Nikolaj Bjorner
f2260d959d test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-14 18:01:41 +02:00
Nikolaj Bjorner
a1b831a3e1 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-14 17:50:08 +02:00
Copilot
930ba5ebd6
Implement inverter functions for finite-set operators (#7974) 
* Initial plan

* Add set operator inverters to array_expr_inverter

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

* Refactor expr_inverter to remove set operations

Removed handling for set operations like union, intersection, and difference in expr_inverter.cpp. Introduced finite_set_inverter class to manage set union operation.

* Remove OP_SET_COMPLEMENT case from expr_inverter

Removed handling for OP_SET_COMPLEMENT in expr_inverter.

* Change OP_SET_UNION to OP_FINITE_SET_UNION

---------

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-14 17:48:40 +02:00
Nikolaj Bjorner
0efe3820fc build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-14 17:46:49 +02:00
Nikolaj Bjorner
5dacb270f8 add to spec 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-14 17:33:19 +02:00
Copilot
75bac9c0ce
Implement finite_set_axioms.cpp and fix empty set constructor bug (#7973) 
* Initial plan

* Add finite_set_axioms.cpp implementation and update CMakeLists.txt

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

* Fix finite_set_decl_plugin bug and complete implementation

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

* Use array select instead of function application for map and select axioms

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

* Simplify range assignment in finite_set_decl_plugin

---------

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-14 17:16:29 +02:00
Copilot
c526c20cfc
Implement finite_set_rewriter with basic algebraic simplification rules (#7972) 
* Initial plan

* Add finite_set_rewriter implementation with basic rewrite rules

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

* Fix finite_set_decl_plugin bug and complete implementation

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

* Revert finite_set_decl_plugin changes and disable difference rule

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

* Re-enable difference rule using set_sort directly

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

* Update finite_set_rewriter.h

---------

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-14 17:13:18 +02:00
Nikolaj Bjorner
9442b41716 remove debug output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-13 22:40:21 +02:00
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