mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

ML API: bugfixes; starting to replace objects with normal types.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-01-12 00:01:50 +00:00
parent 0e59d05629
commit bbd1e465bb
3 changed files with 382 additions and 335 deletions
Download patch file Download diff file Expand all files Collapse all files

3
examples/ml/ml_example.ml
View file

@ -14,6 +14,7 @@ open Z3.Tactic.ApplyResult
open Z3.Probe open Z3.Probe
open Z3.Solver open Z3.Solver
open Z3.Arithmetic open Z3.Arithmetic
open Z3.Fixedpoints
exception TestFailedException of string exception TestFailedException of string
@ -216,8 +217,8 @@ let _ =
Printf.printf "bool sort: %s\n" (Sort.to_string bs); Printf.printf "bool sort: %s\n" (Sort.to_string bs);
Printf.printf "int sort: %s\n" (Sort.to_string ints); Printf.printf "int sort: %s\n" (Sort.to_string ints);
Printf.printf "real sort: %s\n" (Sort.to_string rs); Printf.printf "real sort: %s\n" (Sort.to_string rs);
Printf.printf "Disposing...\n";
basic_tests ctx ; basic_tests ctx ;
Printf.printf "Disposing...\n";
Gc.full_major () Gc.full_major ()
); );
Printf.printf "Exiting.\n"; Printf.printf "Exiting.\n";

3
scripts/update_api.py
View file

@ -1300,7 +1300,8 @@ def mk_ml():
ml_wrapper.write('extern "C" {\n') ml_wrapper.write('extern "C" {\n')
ml_wrapper.write('#endif\n\n') ml_wrapper.write('#endif\n\n')
ml_wrapper.write('CAMLprim value n_is_null(value p) {\n') ml_wrapper.write('CAMLprim value n_is_null(value p) {\n')
ml_wrapper.write(' return Val_bool(Data_custom_val(p) == 0);\n') ml_wrapper.write(' void * t = * (void**) Data_custom_val(p);\n')
ml_wrapper.write(' return Val_bool(t == 0);\n')
ml_wrapper.write('}\n\n') ml_wrapper.write('}\n\n')
ml_wrapper.write('CAMLprim value n_mk_null( void ) {\n') ml_wrapper.write('CAMLprim value n_mk_null( void ) {\n')
ml_wrapper.write(' CAMLparam0();\n') ml_wrapper.write(' CAMLparam0();\n')

707
src/api/ml/z3.ml
View file

File diff suppressed because it is too large Load diff