The representation of the zero rcf numeral is nullptr, and the is_rational
and is_rational_function operations are not expecting to be called with
nullptr. But there isn't a way to test for that in the API, other than
checking if Z3_rcf_num_to_string returns "0".
This patch adds a couple conditions so that is_rational and
is_rational_function operations handle zero. Maybe this isn't the desired
change. For instance, the is_zero operation could instead be exposed in the
API and preconditions added to the relevant operations.
Signed-off-by: Josh Berdine <josh@berdine.net>
This is analogous to Z3_fpa_is_numeral_nan, Z3_fpa_is_numeral_inf, etc. and
can be needed to check that inputs are valid before calling those functions.
Signed-off-by: Josh Berdine <josh@berdine.net>
* Initial plan
* Add C API and Java bindings for str.replace_all, str.replace_re, str.replace_all_re
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add test for new Java string replace operations
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Remove author field from test file header
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Delete examples/java/StringReplaceTest.java
---------
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 finite_set_value_factory implementation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Remove unused dl_decl_plugin variable and include
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* 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.
* Update copyright information in finite_set_value_factory.h
Updated copyright year from 2006 to 2025.
* Implement finite_set_value_factory using array_util to create singleton sets
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Simplify empty set creation in finite_set_value_factory
Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic.
* Change family ID for finite_set_value_factory
* Fix build error by restoring array_decl_plugin include and implementation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update finite_set_value_factory.h
* Add SASSERT for finite set check in factory
Added assertion to check if the sort is a finite set.
* Rename member variable from m_util to u
* Refactor finite_set_value_factory for value handling
* Use register_value instead of direct set insertion
Replaced direct insertion into set with register_value calls.
* Update finite_set_value_factory.cpp
---------
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>
* add examples
* add lattice refutation solver class
* store partial order in vector
* capture partial order relations
* begin with the incremental reachability data structure
* implement data structure for incremental reachability
* fix bug in subset propagation
* add trace
* only propagate if new value was added
* begin implementing bitvector variant of reachability matrix
* fix path creation and cycle detection
* fix bug
* make conflict triggering more conservative
* check if theory vars are in bounds
* add cycle detection (including equality propagation)
* add examples
* remove example
* remove traces
* remove sln file
* Initial plan
* Add mkLastIndexOf method and CharSort support to Java API
- Added mkLastIndexOf method to Context.java for extracting last index of sub-string
- Added Z3_CHAR_SORT case to Sort.java's create() method switch statement
- Added test file to verify both fixes work correctly
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix author field in test file
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Delete examples/java/TestJavaAPICompleteness.java
---------
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 finite_set_value_factory implementation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Remove unused dl_decl_plugin variable and include
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* 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.
* Update copyright information in finite_set_value_factory.h
Updated copyright year from 2006 to 2025.
* Implement finite_set_value_factory using array_util to create singleton sets
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Simplify empty set creation in finite_set_value_factory
Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic.
* Change family ID for finite_set_value_factory
* Fix build error by restoring array_decl_plugin include and implementation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update finite_set_value_factory.h
* Add SASSERT for finite set check in factory
Added assertion to check if the sort is a finite set.
* Rename member variable from m_util to u
* Refactor finite_set_value_factory for value handling
* Use register_value instead of direct set insertion
Replaced direct insertion into set with register_value calls.
* Update finite_set_value_factory.cpp
---------
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 Z3_decl_kind enumeration for finite_set operators
- Added Z3_OP_FINITE_SET_* enumeration values (0xc000 range) to z3_api.h
- Added documentation for all 13 finite_set operators
- Added translation cases in api_ast.cpp for mapping internal finite_set
enum values to external Z3_decl_kind values
- All operators tested and working correctly
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Improve documentation for Z3_OP_FINITE_SET_EXT and Z3_OP_FINITE_SET_MAP_INVERSE
- Clarified that Z3_OP_FINITE_SET_EXT returns a witness element demonstrating
two sets are different (extensionality)
- Clarified that Z3_OP_FINITE_SET_MAP_INVERSE relates to pre-image reasoning
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>
