* Add cube tree optimization about resolving cores recursively up the path, to prune. Also integrate asms into the tree so they're not tracked separately (#7960)
* draft attempt at optimizing cube tree with resolvents. have not tested/ran yet
* adding comments
* fix bug about needing to bubble resolvent upwards to highest ancestor
* fix bug where we need to cover the whole resolvent in the path when bubbling up
* clean up comments
* close entire tree when sibling resolvent is empty
* integrate asms directly into cube tree, remove separate tracking
* try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function
* separate the logic again to avoid mutual recursion
* Refactor search tree closure and resolution logic
Refactor close_with_core to simplify logic and remove unnecessary parameters. Update sibling resolvent computation and try_resolve_upwards for clarity.
* apply formatting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Refactor close_with_core to use current node in lambda
* Fix formatting issues in search_tree.h
* fix build issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update smt_parallel.cpp
* Change loop variable type in unsat core processing
* Change method to retrieve unsat core from root
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Initial plan
* Disable C++98 compatibility warnings for Clang to fix vcpkg build freeze
Add -Wno-c++98-compat and -Wno-c++98-compat-pedantic flags to prevent
excessive warning output when building with clang-cl or when -Weverything
is enabled. These warnings are not useful for Z3 since it requires C++20.
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>
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation.
To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
The underlying `mpf_manager::sgn` function returns a `bool`, and functions
such as `Z3_mk_fpa_numeral_int_uint` take the sign as a `bool`.
Signed-off-by: Josh Berdine <josh@berdine.net>
In the underlying realclosure implementation, the interval operations for
{`lower`,`upper`}`_is_`{`inf`,`open`} return `bool` results. Currently these
are cast to `int` when surfacing them to the API. This patch keeps them at
type `bool` through to `Z3_rcf_interval`.
Signed-off-by: Josh Berdine <josh@berdine.net>
