mirror of
https://github.com/Z3Prover/z3
synced 2025-07-21 11:52:05 +00:00
7fdcbbaee9
* [Draft] Added unfinished code for high level bindings for js * * Rewrote structure of js api files * Added more high level apis * Minor fixes * Fixed wasm github action * Fix JS test * Removed ContextOptions type * * Added Ints to JS Api * Added tests to JS Api * Added run-time checks for contexts * Removed default contexts * Merged Context and createContext so that the api behaves the sames as in other constructors * Added a test for Solver * Added Reals * Added classes for IntVals and RealVals * Added abillity to specify logic for solver * Try to make CI tests not fail * Changed APIs after a round of review * Fix test * Added BitVectors * Made sort into getter * Added initial JS docs * Added more coercible types * Removed done TODOs
20 lines
570 B
TypeScript
20 lines
570 B
TypeScript
// things which you probably want to do off-thread
|
|
// from https://github.com/Z3Prover/z3/issues/5746#issuecomment-1006289146
|
|
export const asyncFuncs = [
|
|
'Z3_eval_smtlib2_string',
|
|
'Z3_simplify',
|
|
'Z3_simplify_ex',
|
|
'Z3_solver_check',
|
|
'Z3_solver_check_assumptions',
|
|
'Z3_solver_cube',
|
|
'Z3_solver_get_consequences',
|
|
'Z3_tactic_apply',
|
|
'Z3_tactic_apply_ex',
|
|
'Z3_optimize_check',
|
|
'Z3_algebraic_roots',
|
|
'Z3_algebraic_eval',
|
|
'Z3_fixedpoint_query',
|
|
'Z3_fixedpoint_query_relations',
|
|
'Z3_fixedpoint_query_from_lvl',
|
|
'Z3_polynomial_subresultants',
|
|
];
|