mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
20123 commits 49 branches 53 tags 182 MiB
Commit graph

20123 commits

This branch
This branch
All branches
Author SHA1 Message Date
dependabot[bot]
64295b5876 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-26 15:32:20 +01:00
Lev Nachmanson
23ce6917c5 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:20 +01:00
Lev Nachmanson
6bca12d399 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:20 +01:00
Lev Nachmanson
e75da050d2 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:20 +01:00
Lev Nachmanson
4f93fc7b2a parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:20 +01:00
Lev Nachmanson
5a3d33a615 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:20 +01:00
Lev Nachmanson
6146fe9ff8 parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:20 +01:00
Lev Nachmanson
0a2328af1d parameter eval order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:20 +01:00
Lev Nachmanson
0fbf4010a5 param eval order 2025-10-26 15:32:20 +01:00
Lev Nachmanson
b22f4d8802 param eval 2025-10-26 15:32:20 +01:00
Lev Nachmanson
e113d39aa8 parameter evaluation order 2025-10-26 15:32:20 +01:00
Lev Nachmanson
28c625a170 parameter eval order 2025-10-26 15:32:19 +01:00
Lev Nachmanson
1aaf2f8448 param order evaluation 2025-10-26 15:32:19 +01:00
Lev Nachmanson
97bb035416 param order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:19 +01:00
Lev Nachmanson
74c28532f4 param order 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-10-26 15:32:19 +01:00
Nikolaj Bjorner
f8b2268424 base implementation for cardinality constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-26 10:35:37 +01:00
Nikolaj Bjorner
4068460a0f fix bogus axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-24 13:35:41 +02:00
Nikolaj Bjorner
5079b10597 fix up documentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-24 13:13:52 +02:00
Copilot
bfe6670b73
Fix finite_set sort cardinality computation for finite base sorts (#7997) 
* Initial plan

* Implement cardinality computation for finite_set sorts

- Modified mk_sort in finite_set_decl_plugin.cpp to compute 2^|s| for finite base sorts
- If base sort size > 30, mark finite_set sort as very_big
- Added comprehensive tests to verify sort size calculations
- All tests pass successfully

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

* Update finite_set_decl_plugin.cpp

* Fix unit tests for infinite base sorts

Updated test to check is_infinite() instead of is_very_big() for FiniteSet(Int) since infinite element sorts now result in infinite FiniteSet sorts (not very_big). Also updated comment to clarify the behavior.

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-23 17:30:17 +02:00
Nikolaj Bjorner
69e0793f6c add overloads for finite sets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-23 17:29:11 +02:00
Copilot
541a554ecd
Add finite set API functions to access term constructors from finite_set_decl_plugin.h (#7996) 
* Initial plan

* Add C API for finite sets

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

* Add Python bindings for finite sets

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

* Add C++ bindings for finite sets

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

* Add documentation for finite set API

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-23 17:10:47 +02:00
Nikolaj Bjorner
4c67a7271e extend proof logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-23 09:48:43 +02:00
Nikolaj Bjorner
b96624727d remove ad-hoc membership axioms, enable boundary point saturatino 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-23 09:42:25 +02:00
Nikolaj Bjorner
2e4402c8f3 add interpretations when there are ranges 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-20 23:21:30 +02:00
Nikolaj Bjorner
65f38eac16 fixup proof log annotations of rules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-19 10:04:18 +02:00
Nikolaj Bjorner
6485808b49 adding proof hint output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-18 19:26:19 +02:00
Copilot
eb10ab1633
Rename set.select to set.filter and OP_FINITE_SET_SELECT to OP_FINITE_SET_FILTER (#7989) 
* Initial plan

* Rename set.select to set.filter and OP_FINITE_SET_SELECT to OP_FINITE_SET_FILTER

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-18 17:16:32 +02:00
Nikolaj Bjorner
ba5bc90d7c remove debug code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-18 13:34:27 +02:00
Nikolaj Bjorner
7d585b5cfd fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-18 13:30:46 +02:00
Nikolaj Bjorner
af432668be fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-18 12:58:27 +02:00
Nikolaj Bjorner
43d40ac142 revise axiom instantiation scheme for finite-sets 
Instead of asserting theory axioms lazily we create them on the fly and allow propagation eagerly.
The approach uses a waterfall model as follows:
- terms are created: they are inserted into an index for (set.in x S) axiom creation.
- two terms are merged by an equality.
  Loop over all new opportunities for axiom instantiation
  New axioms are added to a queue of recently created axioms.
- an atomic formula was asserted by the SAT solver.
  Update the watch list to find new propagations.

During propagation recently created axioms are either inserted into a propagation queue, or inserted into a watch list.
They are inserted into a propagation queue all or all but one literal is assigned to false.
They are inserted into a watch list if at least two literals are unassigned
They are dropped if the axiom contains a literal that is assigned to true

The propagation queue is processed by by asserting the theory axiom to the core.

Also add some elementary statistics.

A breaking change is to change the datatype for undo-trail in smt_context to not use a custom data-structure.
This can likely cause regressions. For example, the region allocator now comes from the stack_trail instead of being
owned within smt_context with a different declaration order. smt_context could crash during destruction or maybe even pop.
We take the risk as the change is overdue.

Add swap method to ref_vector.
 2025-10-18 12:08:39 +02:00
Nikolaj Bjorner
aa1f1f56b6 prepare for incremental axiom propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-17 16:54:12 +02:00
Nikolaj Bjorner
5169e552fa rename finite_set_value_factor to finite_set_factory. Fix type bugs when creating unions of values 2025-10-17 15:09:12 +02:00
Nikolaj Bjorner
af2082a1aa add a comment, remove } 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-17 14:52:53 +02:00
Nikolaj Bjorner
d6908a3d4b support AC parsing 
By tagging union and intersection as AC we allow parsing set union and intersection as n-ary functions.
The internal representation remains binary.
 2025-10-17 14:49:43 +02:00
Copilot
8dd91e4698
Implement get_fresh_value algorithm for finite_set_value_factory (#7987) 
* Initial plan

* Implement get_fresh_value algorithm for finite_set_value_factory

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

* Replace values.back() with values.get(N) as requested

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-17 14:46:04 +02:00
Nikolaj Bjorner
df62e5e9e6 add assume-eqs and extensionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-17 09:37:11 +02:00
Nikolaj Bjorner
981c7d27ea adding factory for model initialization 2025-10-16 22:43:20 +02:00
Nikolaj Bjorner
9e79fe0a51 merge comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-16 13:39:17 +02:00
Copilot
0371bbd192
Extend finite_set_decl_plugin::is_value to support unions of empty/singleton sets (#7980) 
* Initial plan

* Initial state - all tests passing

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

* Implement is_value for unions of empty/singleton sets

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-16 13:36:55 +02:00
Nikolaj Bjorner
1536b4fde3 register the value factory in model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-16 13:35:55 +02:00
Nikolaj Bjorner
a4f5a08edf add comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-16 13:32:12 +02:00
Nikolaj Bjorner
ed369dee08 fixup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-16 13:30:02 +02:00
Nikolaj Bjorner
26d37c7b30 fixup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-16 13:29:38 +02:00
Nikolaj Bjorner
cc8bfd7890 add fintie_set_value_factory outline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-16 13:27:26 +02:00
Nikolaj Bjorner
1b918ce4ec restructure base class struct_factory so that enumeration of values for a sort comes together with hash-table access. This allows to use the enumeration view during value creations for finite sets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-16 13:15:23 +02:00
Nikolaj Bjorner
b53e87dcba updated with immediate axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-16 09:20:46 +02:00
Nikolaj Bjorner
d0a7b19806 add comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-16 08:53:38 +02:00
Copilot
2bb22c6489
Fix finite_set::is_fully_interp to check element sort interpretation (#7982) 
* Initial plan

* Implement finite_set is_fully_interp to check element sort

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

* Refine is_fully_interp implementation with SASSERT

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-15 21:47:32 +02:00
Nikolaj Bjorner
e781648499 fix test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-15 20:55:27 +02:00