* 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>
* 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>
* Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it.
* Fix configuration error for non-MSVC compilers.
* Reviewed and updated configuration for Python build and added comment for CFG.
When the inputs are already the same sort, we can skip most of the
coercion logic and just return.
Currently, `_coerce_exprs` is by far the most expensive part of
building up many common Z3 ASTs, so this fast-path is a substantial
speedup for many use-cases.
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.
