3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +00:00
z3/src
Copilot f690afa6b1
Add AtMost, AtLeast, unsatCore, and reasonUnknown to JS/TS API (#8118)
* Initial plan

* Add AtMost, AtLeast, checkAssumptions, and unsatCore methods to JS/TS API

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

* Format code with prettier

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

* Add comprehensive documentation for Solver.check, checkAssumptions, and unsatCore methods

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

* Remove redundant checkAssumptions method, use check() for assumptions

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

* Enable unsat_core tracking in test to fix 'unknown' result

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

* Add reasonUnknown() method and use it in test to debug unknown results

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>
2026-01-08 19:53:08 -08:00
..
ackermannization Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
api Add AtMost, AtLeast, unsatCore, and reasonUnknown to JS/TS API (#8118) 2026-01-08 19:53:08 -08:00
ast fix #8109 2026-01-07 10:56:50 -08:00
cmd_context allow parsing declared arrays without requiring explicit select 2025-12-06 18:02:15 -08:00
math when deleting the last row from m_e_matrix go over fresh variables defined for this row and mark the rows depending on them as changed 2026-01-02 11:56:35 -10:00
model fix #8109 2026-01-07 10:56:50 -08:00
muz fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables 2025-09-30 15:58:48 -07:00
nlsat remove unused *_signed_project() methods 2025-12-02 18:46:16 -10:00
opt refine maxresw option 2026-01-02 16:23:51 -08:00
params fix #8109 2026-01-07 10:56:50 -08:00
parsers fix #7956 2025-09-30 15:41:49 -07:00
qe remove unused *_signed_project() methods 2025-12-02 18:46:16 -10:00
sat remove stale experimental code #8063 2025-12-12 05:49:05 +00:00
shell move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
smt AIX compat (#8113) 2026-01-05 07:23:05 -08:00
solver Add commands for forcing preferences during search 2025-10-02 10:47:10 -07:00
tactic fix #8105 2025-12-30 11:30:22 -08:00
test AIX compat (#8113) 2026-01-05 07:23:05 -08:00
util Fix DEL character (0x7F) not being escaped in string literals (#8080) 2025-12-15 22:23:49 +00:00
CMakeLists.txt BLD: Add CMake option to build Python bindings without rebuilding libz3 (redux) (#8088) 2025-12-16 17:50:37 +00:00