mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 23:14:40 +00:00
Code Activity
z3/src/api
History
Copilot d867eb3cd8 Add Goal, ApplyResult, and Tactic APIs to TypeScript bindings (#8141) 
* Initial plan

* Add Goal, ApplyResult, and enhanced Tactic/Probe APIs to TypeScript bindings

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

* Fix async tactic.apply and add comprehensive tests for new APIs

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

* Address code review feedback: fix proxy handler, factory method, and type improvements

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

* Add API examples documentation and format code with Prettier

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

* Fix merge conflict in test file - complete truncated tactic test

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

* Add test case for tactic.apply method

missing bracket,

* Change tactic from 'simplify' to 'smt'

* Delete src/api/js/TACTICS_API_EXAMPLES.md

---------

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-02-18 20:57:07 -08:00
..
c++ Add missing array API functions and fix BitVec method typos (#8132) 2026-02-18 20:57:07 -08:00
dll Tabs, formatting. 2017-09-17 14:54:09 +01:00
dotnet Add missing C# API functions for solver introspection and congruence closure (#8126) 2026-02-18 20:57:06 -08:00
java Add missing API methods: Java substituteFuns, TypeScript Fixedpoint and substitution APIs (#8138) 2026-02-18 20:57:07 -08:00
js Add Goal, ApplyResult, and Tactic APIs to TypeScript bindings (#8141) 2026-02-18 20:57:07 -08:00
julia Add finite_set API bindings for ML, TypeScript, and Julia (#8005) 2025-10-30 03:15:01 -07:00
mcp remove non-working ts mcp server, settle with python variant 2025-04-18 10:10:12 -07:00
ml open_log returns bool 2026-02-18 20:56:01 -08:00
python set build be configurable by env 2026-02-18 20:57:02 -08:00
api_algebraic.cpp Use nullptr consistently instead of 0 or NULL. 2022-08-01 14:24:32 +03:00
api_arith.cpp Add check that argument of Z3_is_algebraic_number is_expr (#8027) 2026-02-18 20:55:56 -08:00
api_array.cpp remove references to set_has_size 2026-02-18 20:56:03 -08:00
api_ast.cpp remove references to set_has_size 2026-02-18 20:56:03 -08:00
api_ast_map.cpp remove a few string copies 2023-12-20 16:55:09 +00:00
api_ast_map.h booyah 2020-07-04 15:56:30 -07:00
api_ast_vector.cpp remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
api_ast_vector.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
api_bv.cpp fix #7572 and fix #7574 2025-03-07 10:46:29 -08:00
api_config_params.cpp fix #7622 2025-04-17 11:05:49 -07:00
api_context.cpp Add finite set API functions to access term constructors from finite_set_decl_plugin.h (#7996) 2025-10-23 17:10:47 +02:00
api_context.h Add finite set API functions to access term constructors from finite_set_decl_plugin.h (#7996) 2025-10-23 17:10:47 +02:00
api_datalog.cpp fix #7603: race condition in Ctrl-C handling (#7755) 2025-08-06 14:27:28 -07:00
api_datalog.h move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
api_datatype.cpp Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966) 2025-10-26 15:32:21 +01:00
api_finite_set.cpp Add finite set API functions to access term constructors from finite_set_decl_plugin.h (#7996) 2025-10-23 17:10:47 +02:00
api_fpa.cpp Return sign from Z3_fpa_get_numeral_sign as bool instead of int (#8047) 2026-02-18 20:56:01 -08:00
api_goal.cpp fix #7609 2025-04-04 18:40:15 -07:00
api_goal.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
api_log.cpp api: avoid some string copies when using mk_external_string 2024-12-28 09:42:54 +00:00
api_model.cpp remove theory_str and classes that are only used by it 2025-08-07 21:05:12 -07:00
api_model.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
api_numeral.cpp Note that Z3_get_numeral_small is essentially redundant (#7599) 2025-03-29 10:02:32 -07:00
api_opt.cpp Implement Z3_optimize_translate for context translation (#8072) 2026-02-18 20:56:58 -08:00
api_params.cpp api: avoid some string copies when using mk_external_string 2024-12-28 09:42:54 +00:00
api_parsers.cpp add py_value to selected classes in python bindings, add mode for input-assertion based lookahead solving 2025-01-04 13:40:49 -08:00
api_pb.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
api_polynomial.cpp remove virtual destructor from api::pmanager 2018-07-09 10:37:26 +01:00
api_polynomial.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
api_qe.cpp filter out terms that are not solved 2025-04-30 09:40:45 -07:00
api_quant.cpp Fix build when Z3_API macro is non-empty (#7553) 2025-02-13 08:46:08 -08:00
api_rcf.cpp Return bool instead of int from Z3_rcf_interval (#8046) 2026-02-18 20:56:01 -08:00
api_seq.cpp Add missing string replace operations to Java API (#8011) 2026-02-18 20:55:56 -08:00
api_solver.cpp Use solver factory translate method in Z3_solver_translate (#7782) 2025-08-14 18:13:23 -07:00
api_solver.h add API for creating and attaching simplifiers 2023-01-31 17:06:03 -08:00
api_special_relations.cpp remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
api_stats.cpp fix infinite loop in internalize 2022-09-14 11:50:53 +01:00
api_stats.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
api_tactic.cpp fix #7603: race condition in Ctrl-C handling (#7755) 2025-08-06 14:27:28 -07:00
api_tactic.h add API for creating and attaching simplifiers 2023-01-31 17:06:03 -08:00
api_util.h Add parameter validation for selected API functions 2025-07-27 13:38:37 -07:00
CMakeLists.txt Add finite set API functions to access term constructors from finite_set_decl_plugin.h (#7996) 2025-10-23 17:10:47 +02:00
z3.h z3.h: Don't include stdio.h (#7014) 2023-11-24 16:46:32 +01:00
z3_algebraic.h fix grouping for latest doxygen (#5626) 2021-10-27 23:46:31 +02:00
z3_api.h Fix _in vs _out def_API param for Z3_solver_get_levels (#8050) 2026-02-18 20:56:56 -08:00
z3_ast_containers.h fix grouping for latest doxygen (#5626) 2021-10-27 23:46:31 +02:00
z3_fixedpoint.h Added function to select the next variable to split on (User-Propagator) (#6096) 2022-06-19 10:49:25 -07:00
z3_fpa.h Return sign from Z3_fpa_get_numeral_sign as bool instead of int (#8047) 2026-02-18 20:56:01 -08:00
z3_logger.h Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
z3_macros.h Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
z3_optimization.h Implement Z3_optimize_translate for context translation (#8072) 2026-02-18 20:56:58 -08:00
z3_polynomial.h fix grouping for latest doxygen (#5626) 2021-10-27 23:46:31 +02:00
z3_private.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
z3_rcf.h Return bool instead of int from Z3_rcf_interval (#8046) 2026-02-18 20:56:01 -08:00
z3_replayer.cpp Return sign from Z3_fpa_get_numeral_sign as bool instead of int (#8047) 2026-02-18 20:56:01 -08:00
z3_replayer.h Return sign from Z3_fpa_get_numeral_sign as bool instead of int (#8047) 2026-02-18 20:56:01 -08:00
z3_spacer.h add projection with witnesses 2024-11-27 10:26:34 -08:00
z3_v1.h booyah 2020-07-04 15:56:30 -07:00