mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 22:05:36 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-01-24 19:13:09 +00:00
parent e1d469fcbf b92bdaeebe
commit b6c40c6c0e
78 changed files with 7473 additions and 39818 deletions

7
.gitignore vendored
View file

@ -9,6 +9,7 @@ callgrind.out.*
# OCaml generated files
*.a
*.cma
*.cmo
*.cmi
*.cmxa
ocamlz3
@ -64,6 +65,12 @@ src/util/version.h
src/api/java/Native.cpp
src/api/java/Native.java
src/api/java/enumerations/*.java
src/api/ml/z3native_stubs.c
src/api/ml/z3native.ml
src/api/ml/z3enums.ml
src/api/ml/z3native.mli
src/api/ml/z3enums.mli
src/api/ml/z3.mllib
*.bak
doc/api
doc/code

22
examples/ml/README Normal file
View file

@ -0,0 +1,22 @@
Small example using the Z3 ML bindings.
To build the example execute
make examples
in the build directory.
It will create ml_example in the build directory,
which can be run in the build directory via
LD_LIBRARY_PATH=. ./ml_example
or
LD_LIBRARY_PATH=. ./ml_example.byte
for the byte-code version.
If Z3 was installed into the ocamlfind package repository (see src/api/ml/README),
then we can compile this example as follows:
ocamlfind ocamlc -o ml_example.byte -package Z3 -linkpkg ml_example.ml
ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg ml_example.ml
Note that the resulting binaries depend on the shared z3 library, which needs to be
in the PATH (Windows), LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX). If Z3 was
installed into ocamlfind, the path that should be added is
`ocamlfind printconf destdir`/Z3

350
examples/ml/ml_example.ml Normal file
View file

@ -0,0 +1,350 @@
(*
Copyright (C) 2012 Microsoft Corporation
Author: CM Wintersteiger (cwinter) 2012-12-17
*)
open Z3
open Z3.Symbol
open Z3.Sort
open Z3.Expr
open Z3.Boolean
open Z3.FuncDecl
open Z3.Goal
open Z3.Tactic
open Z3.Tactic.ApplyResult
open Z3.Probe
open Z3.Solver
open Z3.Arithmetic
open Z3.Arithmetic.Integer
open Z3.Arithmetic.Real
open Z3.BitVector
exception TestFailedException of string
(**
Model Converter test
*)
let model_converter_test ( ctx : context ) =
Printf.printf "ModelConverterTest\n";
let xr = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Real.mk_sort ctx)) in
let yr = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Real.mk_sort ctx)) in
let g4 = (mk_goal ctx true false false ) in
(Goal.add g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ;
(Goal.add g4 [ (mk_eq ctx
yr
(Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1 1) ])) ]) ;
(Goal.add g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)) ]) ;
(
let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in
if ((get_num_subgoals ar) == 1 &&
((is_decided_sat (get_subgoal ar 0)) ||
(is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let ar = (Tactic.apply (and_then ctx (mk_tactic ctx ("simplify")) (mk_tactic ctx "solve-eqs") []) g4 None) in
if ((get_num_subgoals ar) == 1 &&
((is_decided_sat (get_subgoal ar 0)) ||
(is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
;
let solver = (mk_solver ctx None) in
let f e = (Solver.add solver [ e ]) in
ignore (List.map f (get_formulas (get_subgoal ar 0))) ;
let q = (check solver []) in
if q != SATISFIABLE then
raise (TestFailedException "")
else
let m = (get_model solver) in
match m with
| None -> raise (TestFailedException "")
| Some (m) ->
Printf.printf "Solver says: %s\n" (string_of_status q) ;
Printf.printf "Model: \n%s\n" (Model.to_string m) ;
Printf.printf "Converted Model: \n%s\n" (Model.to_string (convert_model ar 0 m))
)
(**
Some basic tests.
*)
let basic_tests ( ctx : context ) =
Printf.printf "BasicTests\n" ;
let fname = (mk_string ctx "f") in
let x = (mk_string ctx "x") in
let y = (mk_string ctx "y") in
let bs = (Boolean.mk_sort ctx) in
let domain = [ bs; bs ] in
let f = (FuncDecl.mk_func_decl ctx fname domain bs) in
let fapp = (mk_app ctx f
[ (Expr.mk_const ctx x bs); (Expr.mk_const ctx y bs) ]) in
let fargs2 = [ (mk_fresh_const ctx "cp" bs) ] in
let domain2 = [ bs ] in
let fapp2 = (mk_app ctx (mk_fresh_func_decl ctx "fp" domain2 bs) fargs2) in
let trivial_eq = (mk_eq ctx fapp fapp) in
let nontrivial_eq = (mk_eq ctx fapp fapp2) in
let g = (mk_goal ctx true false false) in
(Goal.add g [ trivial_eq ]) ;
(Goal.add g [ nontrivial_eq ]) ;
Printf.printf "%s\n" ("Goal: " ^ (Goal.to_string g)) ;
(
let solver = (mk_solver ctx None) in
(List.iter (fun a -> (Solver.add solver [ a ])) (get_formulas g)) ;
if (check solver []) != SATISFIABLE then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let ar = (Tactic.apply (mk_tactic ctx "simplify") g None) in
if ((get_num_subgoals ar) == 1 &&
((is_decided_sat (get_subgoal ar 0)) ||
(is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_sat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(Goal.add g [ (mk_eq ctx
(mk_numeral_int ctx 1 (BitVector.mk_sort ctx 32))
(mk_numeral_int ctx 2 (BitVector.mk_sort ctx 32))) ] )
;
(
let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let g2 = (mk_goal ctx true true false) in
let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_sat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let g2 = (mk_goal ctx true true false) in
(Goal.add g2 [ (Boolean.mk_false ctx) ]) ;
let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let g3 = (mk_goal ctx true true false) in
let xc = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Integer.mk_sort ctx)) in
let yc = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Integer.mk_sort ctx)) in
(Goal.add g3 [ (mk_eq ctx xc (mk_numeral_int ctx 1 (Integer.mk_sort ctx))) ]) ;
(Goal.add g3 [ (mk_eq ctx yc (mk_numeral_int ctx 2 (Integer.mk_sort ctx))) ]) ;
let constr = (mk_eq ctx xc yc) in
(Goal.add g3 [ constr ] ) ;
let ar = (Tactic.apply (mk_tactic ctx "smt") g3 None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
) ;
model_converter_test ctx ;
(* Real num/den test. *)
let rn = Real.mk_numeral_nd ctx 42 43 in
let inum = (get_numerator rn) in
let iden = get_denominator rn in
Printf.printf "Numerator: %s Denominator: %s\n" (Real.numeral_to_string inum) (Real.numeral_to_string iden) ;
if ((Real.numeral_to_string inum) <> "42" || (Real.numeral_to_string iden) <> "43") then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
;
if ((to_decimal_string rn 3) <> "0.976?") then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
;
if (to_decimal_string (Real.mk_numeral_s ctx "-1231231232/234234333") 5 <> "-5.25640?") then
raise (TestFailedException "")
else if (to_decimal_string (Real.mk_numeral_s ctx "-123123234234234234231232/234234333") 5 <> "-525641278361333.28170?") then
raise (TestFailedException "")
else if (to_decimal_string (Real.mk_numeral_s ctx "-234234333") 5 <> "-234234333") then
raise (TestFailedException "")
else if (to_decimal_string (Real.mk_numeral_s ctx "234234333/2") 5 <> "117117166.5") then
raise (TestFailedException "")
;
(* Error handling test. *)
try (
let i = Integer.mk_numeral_s ctx "1/2" in
raise (TestFailedException (numeral_to_string i)) (* unreachable *)
)
with Z3native.Exception(_) -> (
Printf.printf "Exception caught, OK.\n"
)
(**
A basic example of how to use quantifiers.
**)
let quantifier_example1 ( ctx : context ) =
Printf.printf "QuantifierExample\n" ;
let is = (Integer.mk_sort ctx) in
let types = [ is; is; is ] in
let names = [ (Symbol.mk_string ctx "x_0");
(Symbol.mk_string ctx "x_1");
(Symbol.mk_string ctx "x_2") ] in
let vars = [ (Quantifier.mk_bound ctx 2 (List.nth types 0));
(Quantifier.mk_bound ctx 2 (List.nth types 1));
(Quantifier.mk_bound ctx 2 (List.nth types 2)) ] in
let xs = [ (Integer.mk_const ctx (List.nth names 0));
(Integer.mk_const ctx (List.nth names 1));
(Integer.mk_const ctx (List.nth names 2)) ] in
let body_vars = (Boolean.mk_and ctx
[ (mk_eq ctx
(Arithmetic.mk_add ctx [ (List.nth vars 0) ; (Integer.mk_numeral_i ctx 1)])
(Integer.mk_numeral_i ctx 2)) ;
(mk_eq ctx
(Arithmetic.mk_add ctx [ (List.nth vars 1); (Integer.mk_numeral_i ctx 2)])
(Arithmetic.mk_add ctx [ (List.nth vars 2); (Integer.mk_numeral_i ctx 3)])) ]) in
let body_const = (Boolean.mk_and ctx
[ (mk_eq ctx
(Arithmetic.mk_add ctx [ (List.nth xs 0); (Integer.mk_numeral_i ctx 1)])
(Integer.mk_numeral_i ctx 2)) ;
(mk_eq ctx
(Arithmetic.mk_add ctx [ (List.nth xs 1); (Integer.mk_numeral_i ctx 2)])
(Arithmetic.mk_add ctx [ (List.nth xs 2); (Integer.mk_numeral_i ctx 3)])) ]) in
let x = (Quantifier.mk_forall ctx types names body_vars (Some 1) [] [] (Some (Symbol.mk_string ctx "Q1")) (Some (Symbol.mk_string ctx "skid1"))) in
Printf.printf "Quantifier X: %s\n" (Quantifier.to_string x) ;
let y = (Quantifier.mk_forall_const ctx xs body_const (Some 1) [] [] (Some (Symbol.mk_string ctx "Q2")) (Some (Symbol.mk_string ctx "skid2"))) in
Printf.printf "Quantifier Y: %s\n" (Quantifier.to_string y) ;
if (is_true (Quantifier.expr_of_quantifier x)) then
raise (TestFailedException "") (* unreachable *)
else if (is_false (Quantifier.expr_of_quantifier x)) then
raise (TestFailedException "") (* unreachable *)
else if (is_const (Quantifier.expr_of_quantifier x)) then
raise (TestFailedException "") (* unreachable *)
open Z3.FloatingPoint
(**
A basic example of floating point arithmetic
**)
let fpa_example ( ctx : context ) =
Printf.printf "FPAExample\n" ;
(* let str = ref "" in *)
(* (read_line ()) ; *)
let double_sort = (FloatingPoint.mk_sort_double ctx) in
let rm_sort = (FloatingPoint.RoundingMode.mk_sort ctx) in
(** Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode). *)
let s_rm = (mk_string ctx "rm") in
let rm = (mk_const ctx s_rm rm_sort) in
let s_x = (mk_string ctx "x") in
let s_y = (mk_string ctx "y") in
let x = (mk_const ctx s_x double_sort) in
let y = (mk_const ctx s_y double_sort)in
let n = (FloatingPoint.mk_numeral_f ctx 42.0 double_sort) in
let s_x_plus_y = (mk_string ctx "x_plus_y") in
let x_plus_y = (mk_const ctx s_x_plus_y double_sort) in
let c1 = (mk_eq ctx x_plus_y (mk_add ctx rm x y)) in
let args = [ c1 ; (mk_eq ctx x_plus_y n) ] in
let c2 = (Boolean.mk_and ctx args) in
let args2 = [ c2 ; (Boolean.mk_not ctx (Boolean.mk_eq ctx rm (RoundingMode.mk_rtz ctx))) ] in
let c3 = (Boolean.mk_and ctx args2) in
let and_args = [ (Boolean.mk_not ctx (mk_is_zero ctx y)) ;
(Boolean.mk_not ctx (mk_is_nan ctx y)) ;
(Boolean.mk_not ctx (mk_is_infinite ctx y)) ] in
let args3 = [ c3 ; (Boolean.mk_and ctx and_args) ] in
let c4 = (Boolean.mk_and ctx args3) in
(Printf.printf "c4: %s\n" (Expr.to_string c4)) ;
(
let solver = (mk_solver ctx None) in
(Solver.add solver [ c4 ]) ;
if (check solver []) != SATISFIABLE then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(* Show that the following are equal: *)
(* (fp #b0 #b10000000001 #xc000000000000) *)
(* ((_ to_fp 11 53) #x401c000000000000)) *)
(* ((_ to_fp 11 53) RTZ 1.75 2))) *)
(* ((_ to_fp 11 53) RTZ 7.0))) *)
let c1 = (mk_fp ctx
(mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1))
(mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52))
(mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11))) in
let c2 = (mk_to_fp_bv ctx
(mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64))
(mk_sort ctx 11 53)) in
let c3 = (mk_to_fp_int_real ctx
(RoundingMode.mk_rtz ctx)
(mk_numeral_string ctx "2" (Integer.mk_sort ctx))
(mk_numeral_string ctx "1.75" (Real.mk_sort ctx))
(FloatingPoint.mk_sort ctx 11 53)) in
let c4 = (mk_to_fp_real ctx (RoundingMode.mk_rtz ctx)
(mk_numeral_string ctx "7.0" (Real.mk_sort ctx))
(FloatingPoint.mk_sort ctx 11 53)) in
let args3 = [ (mk_eq ctx c1 c2) ;
(mk_eq ctx c1 c3) ;
(mk_eq ctx c1 c4) ] in
let c5 = (Boolean.mk_and ctx args3) in
(Printf.printf "c5: %s\n" (Expr.to_string c5)) ;
(
let solver = (mk_solver ctx None) in
(Solver.add solver [ c5 ]) ;
if (check solver []) != SATISFIABLE then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
)
let _ =
try (
if not (Log.open_ "z3.log") then
raise (TestFailedException "Log couldn't be opened.")
else
(
Printf.printf "Running Z3 version %s\n" Version.to_string ;
let cfg = [("model", "true"); ("proof", "false")] in
let ctx = (mk_context cfg) in
let is = (Symbol.mk_int ctx 42) in
let ss = (Symbol.mk_string ctx "mySymbol") in
let bs = (Boolean.mk_sort ctx) in
let ints = (Integer.mk_sort ctx) in
let rs = (Real.mk_sort ctx) in
Printf.printf "int symbol: %s\n" (Symbol.to_string is);
Printf.printf "string symbol: %s\n" (Symbol.to_string ss);
Printf.printf "bool sort: %s\n" (Sort.to_string bs);
Printf.printf "int sort: %s\n" (Sort.to_string ints);
Printf.printf "real sort: %s\n" (Sort.to_string rs);
basic_tests ctx ;
quantifier_example1 ctx ;
fpa_example ctx ;
Printf.printf "Disposing...\n";
Gc.full_major ()
);
Printf.printf "Exiting.\n" ;
exit 0
) with Z3native.Exception(msg) -> (
Printf.printf "Z3 EXCEPTION: %s\n" msg ;
exit 1
)
;;

2
scripts/mk_project.py
View file

@ -87,6 +87,7 @@ def init_project_def():
export_files=API_files)
add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest')
add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml')
add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])
set_z3py_dir('api/python')
# Examples
@ -97,6 +98,7 @@ def init_project_def():
add_c_example('maxsat')
add_dotnet_example('dotnet_example', 'dotnet')
add_java_example('java_example', 'java')
add_ml_example('ml_example', 'ml')
add_z3py_example('py_example', 'python')
return API_files

414
scripts/mk_util.py
View file

@ -32,6 +32,10 @@ CXXFLAGS=getenv("CXXFLAGS", "")
EXAMP_DEBUG_FLAG=''
LDFLAGS=getenv("LDFLAGS", "")
JNI_HOME=getenv("JNI_HOME", None)
OCAMLC=getenv("OCAMLC", "ocamlc")
OCAMLOPT=getenv("OCAMLOPT", "ocamlopt")
OCAML_LIB=getenv("OCAML_LIB", None)
OCAMLFIND=getenv("OCAMLFIND", "ocamlfind")
CXX_COMPILERS=['g++', 'clang++']
C_COMPILERS=['gcc', 'clang']
@ -49,6 +53,7 @@ UTIL_COMPONENT='util'
API_COMPONENT='api'
DOTNET_COMPONENT='dotnet'
JAVA_COMPONENT='java'
ML_COMPONENT='ml'
CPP_COMPONENT='cpp'
#####################
IS_WINDOWS=False
@ -66,6 +71,7 @@ VS_PROJ = False
TRACE = False
DOTNET_ENABLED=False
JAVA_ENABLED=False
ML_ENABLED=False
STATIC_LIB=False
VER_MAJOR=None
VER_MINOR=None
@ -334,6 +340,55 @@ def check_java():
if JNI_HOME == None:
raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")
def check_ml():
t = TempFile('hello.ml')
t.add('print_string "Hello world!\n";;')
t.commit()
if is_verbose():
print ('Testing %s...' % OCAMLC)
r = exec_cmd([OCAMLC, '-o', 'a.out', 'hello.ml'])
if r != 0:
raise MKException('Failed testing ocamlc compiler. Set environment variable OCAMLC with the path to the Ocaml compiler')
if is_verbose():
print ('Testing %s...' % OCAMLOPT)
r = exec_cmd([OCAMLOPT, '-o', 'a.out', 'hello.ml'])
if r != 0:
raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.')
rmf('hello.cmi')
rmf('hello.cmo')
rmf('hello.cmx')
rmf('a.out')
find_ml_lib()
find_ocaml_find()
def find_ocaml_find():
global OCAMLFIND
if is_verbose():
print ("Testing %s..." % OCAMLFIND)
r = exec_cmd([OCAMLFIND, 'printconf'])
if r != 0:
OCAMLFIND=''
def find_ml_lib():
global OCAML_LIB
if is_verbose():
print ('Finding OCAML_LIB...')
t = TempFile('output')
null = open(os.devnull, 'wb')
try:
subprocess.call([OCAMLC, '-where'], stdout=t.fname, stderr=null)
t.commit()
except:
raise MKException('Failed to find Ocaml library; please set OCAML_LIB')
t = open('output', 'r')
for line in t:
OCAML_LIB = line[:-1]
if is_verbose():
print ('OCAML_LIB=%s' % OCAML_LIB)
t.close()
rmf('output')
return
def is64():
global LINUX_X64
return LINUX_X64 and sys.maxsize >= 2**32
@ -460,7 +515,8 @@ def display_help(exit_code):
if IS_WINDOWS:
print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.")
print(" -j, --java generate Java bindings.")
print(" --staticlib build Z3 static library.")
print(" --ml generate OCaml bindings.")
print(" --staticlib build Z3 static library.")
if not IS_WINDOWS:
print(" -g, --gmp use GMP.")
print(" --gprof enable gprof")
@ -475,19 +531,22 @@ def display_help(exit_code):
print(" CXXFLAGS C++ compiler flags")
print(" JDK_HOME JDK installation directory (only relevant if -j or --java option is provided)")
print(" JNI_HOME JNI bindings directory (only relevant if -j or --java option is provided)")
print(" OCAMLC Ocaml byte-code compiler (only relevant with --ml)")
print(" OCAMLOPT Ocaml native compiler (only relevant with --ml)")
print(" OCAML_LIB Ocaml library directory (only relevant with --ml)")
exit(exit_code)
# Parse configuration option for mk_make script
def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
global LINUX_X64
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:df:sxhmcvtnp:gj',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
'githash=', 'x86'])
'githash=', 'x86', 'ml'])
except:
print("ERROR: Invalid command line option")
display_help(1)
@ -542,6 +601,8 @@ def parse_options():
GPROF = True
elif opt == '--githash':
GIT_HASH=arg
elif opt in ('', '--ml'):
ML_ENABLED = True
else:
print("ERROR: Invalid command line option '%s'" % opt)
display_help(1)
@ -628,6 +689,9 @@ def is_verbose():
def is_java_enabled():
return JAVA_ENABLED
def is_ml_enabled():
return ML_ENABLED
def is_compiler(given, expected):
"""
Return True if the 'given' compiler is the expected one.
@ -672,6 +736,9 @@ def get_cs_files(path):
def get_java_files(path):
return filter(lambda f: f.endswith('.java'), os.listdir(path))
def get_ml_files(path):
return filter(lambda f: f.endswith('.ml'), os.listdir(path))
def find_all_deps(name, deps):
new_deps = []
for dep in deps:
@ -1275,6 +1342,124 @@ class JavaDLLComponent(Component):
shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
os.path.join(dist_path, 'bin', 'libz3java.%s' % so))
class MLComponent(Component):
def __init__(self, name, lib_name, path, deps):
Component.__init__(self, name, path, deps)
if lib_name == None:
lib_name = name
self.lib_name = lib_name
def mk_ml_meta(self, ml_meta_in, ml_meta_out, major, minor, build, revision):
ver_pat = re.compile('version = "VERSION"*')
fin = open(ml_meta_in, 'r')
fout = open(ml_meta_out, 'w')
num_updates = 0
for line in fin:
if ver_pat.match(line):
fout.write('version = "%s.%s.%s.%s"\n' % (major, minor, build, revision))
num_updates = num_updates + 1
else:
fout.write(line)
assert num_updates == 1, "unexpected number of version number updates"
fin.close()
fout.close()
if VERBOSE:
print("Updated '%s'" % ml_meta_out)
def mk_makefile(self, out):
if is_ml_enabled():
CP_CMD = "cp"
if IS_WINDOWS:
CP_CMD = "copy"
src_dir = self.to_src_dir
sub_dir = os.path.join('api', 'ml')
mk_dir(os.path.join(BUILD_DIR, sub_dir))
api_src = get_component(API_COMPONENT).to_src_dir
for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)):
out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
out.write(str)
for f in filter(lambda f: f.endswith('.mli'), os.listdir(self.src_dir)):
out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
out.write(str)
for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)):
out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
out.write(str)
modules = ["z3enums", "z3native", "z3"] # dependencies in this order!
mls = ''
mlis = ''
cmis = ''
archives = ''
for m in modules:
fn = os.path.join(self.src_dir, ('%s.mli' % m))
if not os.path.exists(fn):
out.write('%s.mli: %s.ml%s\n' % (os.path.join(sub_dir,m),os.path.join(sub_dir,m),mlis))
out.write('\t%s -I %s -i -c %s.ml > %s.mli\n' % (OCAMLC,sub_dir,os.path.join(sub_dir, m),os.path.join(sub_dir, m)))
out.write('%s.cmi: %s.mli%s\n' % (os.path.join(sub_dir,m),os.path.join(sub_dir,m), cmis))
out.write('\t%s -I %s -c %s.mli\n' % (OCAMLC,sub_dir,os.path.join(sub_dir,m)))
out.write('%s.cma: %s.ml %s.cmi%s\n' % (os.path.join(sub_dir,m),os.path.join(sub_dir,m),os.path.join(sub_dir,m), archives))
out.write('\t%s -a -o %s.ml -o %s.cma\n' % (OCAMLC,os.path.join(sub_dir,m), os.path.join(sub_dir,m)))
mlis = mlis + ' ' + os.path.join(sub_dir, m) + '.mli'
cmis = cmis + ' ' + os.path.join(sub_dir,m) + '.cmi'
archives = archives + ' ' + os.path.join(sub_dir,m) + '.cma'
mls = mls + ' ' + os.path.join(sub_dir, m) + '.ml'
out.write('%s: %s %s\n' %
(os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'),
os.path.join(sub_dir, 'z3native_stubs.c'),
get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)'));
out.write('\t$(CC) $(CXXFLAGS) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' %
(OCAML_LIB, api_src, os.path.join(sub_dir, 'z3native_stubs.c'), os.path.join(sub_dir, 'z3native_stubs')))
out.write('%s: %s %s %s$(SO_EXT)' % (
os.path.join(sub_dir, "z3ml.cmxa"),
cmis,
archives,
get_component(Z3_DLL_COMPONENT).dll_name))
out.write(' %s\n' % (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)')))
out.write('\tocamlmklib -o %s -I %s -ldopt \"-L. -lz3\" ' % (os.path.join(sub_dir, 'z3ml'), sub_dir))
for m in modules:
out.write(' %s' % (os.path.join(sub_dir, m+'.ml')))
out.write(' %s\n' % (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)')))
out.write('ml: %s\n' % (os.path.join(sub_dir, 'z3ml.cmxa')))
self.mk_ml_meta(os.path.join('src/api/ml/META'), os.path.join(BUILD_DIR, sub_dir, 'META'), VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION)
if OCAMLFIND != '':
out.write('\nocamlfind_install: %s %s %s\n' % (
get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)',
os.path.join(sub_dir, 'z3ml.cmxa'),
os.path.join(sub_dir, 'META')))
out.write('\t%s remove Z3\n' % (OCAMLFIND))
out.write('\t%s install Z3 %s' % (OCAMLFIND, (os.path.join(sub_dir, 'META'))))
for m in modules:
out.write(' %s.cma' % (os.path.join(sub_dir, m)))
out.write(' %s.cmx' % (os.path.join(sub_dir, m)))
out.write(' %s.cmi' % (os.path.join(sub_dir, m)))
out.write(' %s.cmo' % (os.path.join(sub_dir, m)))
out.write(' %s.ml' % (os.path.join(sub_dir, m)))
out.write(' %s.mli' % (os.path.join(sub_dir, m)))
out.write(' %s$(OBJ_EXT)' % (os.path.join(sub_dir, m)))
out.write(' %s' % ((os.path.join(sub_dir, 'z3ml$(LIB_EXT)'))))
out.write(' %s' % ((os.path.join(sub_dir, 'z3ml.cma'))))
out.write(' %s' % ((os.path.join(sub_dir, 'z3ml.cmxa'))))
out.write(' %s' % ((os.path.join(sub_dir, 'libz3ml$(LIB_EXT)'))))
out.write(' %s' % ((os.path.join(sub_dir, 'dllz3ml'))))
if IS_WINDOWS:
out.write('.dll')
else:
out.write('.so') # .so also on OSX!
out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)')
if IS_WINDOWS:
out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)')
out.write('\n\n')
def main_component(self):
return is_ml_enabled()
class ExampleComponent(Component):
def __init__(self, name, path):
Component.__init__(self, name, path, [])
@ -1384,6 +1569,39 @@ class JavaExampleComponent(ExampleComponent):
out.write(' -d .\n')
out.write('_ex_%s: JavaExample.class\n\n' % (self.name))
class MLExampleComponent(ExampleComponent):
def __init__(self, name, path):
ExampleComponent.__init__(self, name, path)
def is_example(self):
return ML_ENABLED
def mk_makefile(self, out):
if ML_ENABLED:
out.write('ml_example.byte: api/ml/z3ml.cmxa ')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
out.write('\n')
out.write('\t%s ' % OCAMLC)
if DEBUG_MODE:
out.write('-g ')
out.write('-custom -o ml_example.byte -I api/ml -cclib "-L. -lz3" nums.cma z3ml.cma')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s/%s' % (self.to_ex_dir, mlfile))
out.write('\n')
out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa ml_example.byte')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
out.write('\n')
out.write('\t%s ' % OCAMLOPT)
if DEBUG_MODE:
out.write('-g ')
out.write('-o ml_example$(EXE_EXT) -I api/ml -cclib "-L. -lz3" nums.cmxa z3ml.cmxa')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s/%s' % (self.to_ex_dir, mlfile))
out.write('\n')
out.write('_ex_%s: ml_example.byte ml_example$(EXE_EXT)\n\n' % self.name)
class PythonExampleComponent(ExampleComponent):
def __init__(self, name, path):
ExampleComponent.__init__(self, name, path)
@ -1437,6 +1655,10 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man
c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps)
reg_component(name, c)
def add_ml_lib(name, deps=[], path=None, lib_name=None):
c = MLComponent(name, lib_name, path, deps)
reg_component(name, c)
def add_cpp_example(name, path=None):
c = CppExampleComponent(name, path)
reg_component(name, c)
@ -1453,6 +1675,10 @@ def add_java_example(name, path=None):
c = JavaExampleComponent(name, path)
reg_component(name, c)
def add_ml_example(name, path=None):
c = MLExampleComponent(name, path)
reg_component(name, c)
def add_z3py_example(name, path=None):
c = PythonExampleComponent(name, path)
reg_component(name, c)
@ -1523,6 +1749,10 @@ def mk_config():
if is_java_enabled():
print('JNI Bindings: %s' % JNI_HOME)
print('Java Compiler: %s' % JAVAC)
if is_ml_enabled():
print('OCaml Compiler: %s' % OCAMLC)
print('OCaml Native: %s' % OCAMLOPT)
print('OCaml Library: %s' % OCAML_LIB)
else:
global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG
OS_DEFINES = ""
@ -1641,16 +1871,22 @@ def mk_config():
print('64-bit: %s' % is64())
if GPROF:
print('gprof: enabled')
print('Python version: %s' % distutils.sysconfig.get_python_version())
print('Python version: %s' % distutils.sysconfig.get_python_version())
if is_java_enabled():
print('JNI Bindings: %s' % JNI_HOME)
print('Java Compiler: %s' % JAVAC)
if is_ml_enabled():
print('OCaml Compiler: %s' % OCAMLC)
print('OCaml Native: %s' % OCAMLOPT)
print('OCaml Library: %s' % OCAML_LIB)
def mk_install(out):
out.write('install: ')
for c in get_components():
c.mk_install_deps(out)
out.write(' ')
if is_ml_enabled() and OCAMLFIND != '':
out.write('ocamlfind_install')
out.write('\n')
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'bin'))
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'include'))
@ -2211,6 +2447,9 @@ def mk_bindings(api_files):
mk_z3consts_java(api_files)
_execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
cp_z3py_to_build()
if is_ml_enabled():
check_ml()
mk_z3consts_ml(api_files)
# Extract enumeration types from API files, and add python definitions.
def mk_z3consts_py(api_files):
@ -2482,6 +2721,171 @@ def mk_z3consts_java(api_files):
if VERBOSE:
print("Generated '%s'" % ('%s' % gendir))
# Extract enumeration types from z3_api.h, and add ML definitions
def mk_z3consts_ml(api_files):
blank_pat = re.compile("^ *$")
comment_pat = re.compile("^ *//.*$")
typedef_pat = re.compile("typedef enum *")
typedef2_pat = re.compile("typedef enum { *")
openbrace_pat = re.compile("{ *")
closebrace_pat = re.compile("}.*;")
ml = get_component(ML_COMPONENT)
DeprecatedEnums = [ 'Z3_search_failure' ]
gendir = ml.src_dir
if not os.path.exists(gendir):
os.mkdir(gendir)
efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w')
efile.write('(* Automatically generated file *)\n\n')
efile.write('(** The enumeration types of Z3. *)\n\n')
for api_file in api_files:
api_file_c = ml.find_file(api_file, ml.name)
api_file = os.path.join(api_file_c.src_dir, api_file)
api = open(api_file, 'r')
SEARCHING = 0
FOUND_ENUM = 1
IN_ENUM = 2
mode = SEARCHING
decls = {}
idx = 0
linenum = 1
for line in api:
m1 = blank_pat.match(line)
m2 = comment_pat.match(line)
if m1 or m2:
# skip blank lines and comments
linenum = linenum + 1
elif mode == SEARCHING:
m = typedef_pat.match(line)
if m:
mode = FOUND_ENUM
m = typedef2_pat.match(line)
if m:
mode = IN_ENUM
decls = {}
idx = 0
elif mode == FOUND_ENUM:
m = openbrace_pat.match(line)
if m:
mode = IN_ENUM
decls = {}
idx = 0
else:
assert False, "Invalid %s, line: %s" % (api_file, linenum)
else:
assert mode == IN_ENUM
words = re.split('[^\-a-zA-Z0-9_]+', line)
m = closebrace_pat.match(line)
if m:
name = words[1]
if name not in DeprecatedEnums:
efile.write('(** %s *)\n' % name[3:])
efile.write('type %s =\n' % name[3:]) # strip Z3_
for k, i in decls.iteritems():
efile.write(' | %s \n' % k[3:]) # strip Z3_
efile.write('\n')
efile.write('(** Convert %s to int*)\n' % name[3:])
efile.write('let int_of_%s x : int =\n' % (name[3:])) # strip Z3_
efile.write(' match x with\n')
for k, i in decls.iteritems():
efile.write(' | %s -> %d\n' % (k[3:], i))
efile.write('\n')
efile.write('(** Convert int to %s*)\n' % name[3:])
efile.write('let %s_of_int x : %s =\n' % (name[3:],name[3:])) # strip Z3_
efile.write(' match x with\n')
for k, i in decls.iteritems():
efile.write(' | %d -> %s\n' % (i, k[3:]))
# use Z3.Exception?
efile.write(' | _ -> raise (Failure "undefined enum value")\n\n')
mode = SEARCHING
else:
if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x':
idx = int(words[2], 16)
else:
idx = int(words[2])
decls[words[1]] = idx
idx = idx + 1
linenum = linenum + 1
if VERBOSE:
print ('Generated "%s/z3enums.ml"' % ('%s' % gendir))
efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')
efile.write('(* Automatically generated file *)\n\n')
efile.write('(** The enumeration types of Z3. *)\n\n')
for api_file in api_files:
api_file_c = ml.find_file(api_file, ml.name)
api_file = os.path.join(api_file_c.src_dir, api_file)
api = open(api_file, 'r')
SEARCHING = 0
FOUND_ENUM = 1
IN_ENUM = 2
mode = SEARCHING
decls = {}
idx = 0
linenum = 1
for line in api:
m1 = blank_pat.match(line)
m2 = comment_pat.match(line)
if m1 or m2:
# skip blank lines and comments
linenum = linenum + 1
elif mode == SEARCHING:
m = typedef_pat.match(line)
if m:
mode = FOUND_ENUM
m = typedef2_pat.match(line)
if m:
mode = IN_ENUM
decls = {}
idx = 0
elif mode == FOUND_ENUM:
m = openbrace_pat.match(line)
if m:
mode = IN_ENUM
decls = {}
idx = 0
else:
assert False, "Invalid %s, line: %s" % (api_file, linenum)
else:
assert mode == IN_ENUM
words = re.split('[^\-a-zA-Z0-9_]+', line)
m = closebrace_pat.match(line)
if m:
name = words[1]
if name not in DeprecatedEnums:
efile.write('(** %s *)\n' % name[3:])
efile.write('type %s =\n' % name[3:]) # strip Z3_
for k, i in decls.iteritems():
efile.write(' | %s \n' % k[3:]) # strip Z3_
efile.write('\n')
efile.write('(** Convert %s to int*)\n' % name[3:])
efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_
efile.write('(** Convert int to %s*)\n' % name[3:])
efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_
efile.write('\n')
mode = SEARCHING
else:
if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x':
idx = int(words[2], 16)
else:
idx = int(words[2])
decls[words[1]] = idx
idx = idx + 1
linenum = linenum + 1
if VERBOSE:
print ('Generated "%s/z3enums.mli"' % ('%s' % gendir))
def mk_gui_str(id):
return '4D2F40D8-E5F9-473B-B548-%012d' % id
@ -2639,3 +3043,5 @@ def mk_unix_dist(build_path, dist_path):
if __name__ == '__main__':
import doctest
doctest.testmod()

481
scripts/update_api.py
View file

@ -1,3 +1,4 @@
############################################
# Copyright (c) 2012 Microsoft Corporation
#
@ -156,6 +157,10 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I
FLOAT : 'jfloat', STRING : 'jstring', STRING_PTR : 'jobject',
BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'}
# Mapping to ML types
Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**',
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' }
next_type_id = FIRST_OBJ_ID
@ -179,6 +184,7 @@ def def_Types():
v = Type2Str[k]
if is_obj(k):
Type2Dotnet[k] = v
Type2ML[k] = v.lower()
def type2str(ty):
global Type2Str
@ -206,6 +212,10 @@ def type2javaw(ty):
else:
return Type2JavaW[ty]
def type2ml(ty):
global Type2ML
return Type2ML[ty]
def _in(ty):
return (IN, ty);
@ -314,6 +324,22 @@ def param2pystr(p):
else:
return type2pystr(param_type(p))
def param2ml(p):
k = param_kind(p)
if k == OUT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == INT64 or param_type(p) == UINT64:
return "int"
elif param_type(p) == STRING:
return "string"
else:
return "ptr"
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
return "%s array" % type2ml(param_type(p))
elif k == OUT_MANAGED_ARRAY:
return "%s array" % type2ml(param_type(p));
else:
return type2ml(param_type(p))
# Save name, result, params to generate wrapper
_API2PY = []
@ -1043,6 +1069,460 @@ def mk_bindings():
exe_c.write(" in.register_cmd(%s, exec_%s);\n" % (key, val))
exe_c.write("}\n")
def ml_method_name(name):
return name[3:] # Remove Z3_
def is_out_param(p):
if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_MANAGED_ARRAY:
return True
else:
return False
def outparams(params):
op = []
for param in params:
if is_out_param(param):
op.append(param)
return op
def is_in_param(p):
if param_kind(p) == IN or param_kind(p) == INOUT or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY:
return True
else:
return False
def inparams(params):
ip = []
for param in params:
if is_in_param(param):
ip.append(param)
return ip
def is_array_param(p):
if param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_ARRAY:
return True
else:
return False
def arrayparams(params):
op = []
for param in params:
if is_array_param(param):
op.append(param)
return op
def ml_unwrap(t, ts, s):
if t == STRING:
return '(' + ts + ') String_val(' + s + ')'
elif t == BOOL:
return '(' + ts + ') Bool_val(' + s + ')'
elif t == INT or t == PRINT_MODE or t == ERROR_CODE:
return '(' + ts + ') Int_val(' + s + ')'
elif t == UINT:
return '(' + ts + ') Unsigned_int_val(' + s + ')'
elif t == INT64:
return '(' + ts + ') Long_val(' + s + ')'
elif t == UINT64:
return '(' + ts + ') Unsigned_long_val(' + s + ')'
elif t == DOUBLE:
return '(' + ts + ') Double_val(' + s + ')'
else:
return '* (' + ts + '*) Data_custom_val(' + s + ')'
def ml_set_wrap(t, d, n):
if t == VOID:
return d + ' = Val_unit;'
elif t == BOOL:
return d + ' = Val_bool(' + n + ');'
elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE:
return d + ' = Val_int(' + n + ');'
elif t == INT64 or t == UINT64:
return d + ' = Val_long(' + n + ');'
elif t == DOUBLE:
return 'Store_double_val(' + d + ', ' + n + ');'
elif t == STRING:
return d + ' = caml_copy_string((const char*) ' + n + ');'
else:
ts = type2str(t)
return d + ' = caml_alloc_custom(&default_custom_ops, sizeof(' + ts + '), 0, 1); memcpy( Data_custom_val(' + d + '), &' + n + ', sizeof(' + ts + '));'
def mk_ml():
global Type2Str
if not is_ml_enabled():
return
ml_dir = get_component('ml').src_dir
ml_nativef = os.path.join(ml_dir, 'z3native.ml')
ml_nativefi = os.path.join(ml_dir, 'z3native.mli')
ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c')
ml_native = open(ml_nativef, 'w')
ml_i = open(ml_nativefi, 'w')
ml_native.write('(* Automatically generated file *)\n\n')
ml_native.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n')
ml_i.write('(* Automatically generated file *)\n\n')
ml_i.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n')
ml_i.write('(**/**)\n\n');
ml_native.write('open Z3enums\n\n')
ml_native.write('(**/**)\n')
ml_native.write('type ptr\n')
ml_i.write('type ptr\n')
ml_native.write('and z3_symbol = ptr\n')
ml_i.write('and z3_symbol = ptr\n')
for k, v in Type2Str.iteritems():
if is_obj(k):
ml_native.write('and %s = ptr\n' % v.lower())
ml_i.write('and %s = ptr\n' % v.lower())
ml_native.write('\n')
ml_i.write('\n')
ml_native.write('external is_null : ptr -> bool\n = "n_is_null"\n\n')
ml_native.write('external mk_null : unit -> ptr\n = "n_mk_null"\n\n')
ml_native.write('external set_internal_error_handler : ptr -> unit\n = "n_set_internal_error_handler"\n\n')
ml_native.write('exception Exception of string\n\n')
ml_i.write('val is_null : ptr -> bool\n')
ml_i.write('val mk_null : unit -> ptr\n')
ml_i.write('val set_internal_error_handler : ptr -> unit\n\n')
ml_i.write('exception Exception of string\n\n')
# ML declarations
ml_native.write('module ML2C = struct\n\n')
for name, result, params in _dotnet_decls:
ml_native.write(' external n_%s : ' % ml_method_name(name))
ml_i.write('val %s : ' % ml_method_name(name))
ip = inparams(params)
op = outparams(params)
if len(ip) == 0:
ml_native.write(' unit -> ')
ml_i.write(' unit -> ')
for p in ip:
ml_native.write('%s -> ' % param2ml(p))
ml_i.write('%s -> ' % param2ml(p))
if len(op) > 0:
ml_native.write('(')
ml_i.write('(')
first = True
if result != VOID or len(op) == 0:
ml_native.write('%s' % type2ml(result))
ml_i.write('%s' % type2ml(result))
first = False
for p in op:
if first:
first = False
else:
ml_native.write(' * ')
ml_i.write(' * ')
ml_native.write('%s' % param2ml(p))
ml_i.write('%s' % param2ml(p))
if len(op) > 0:
ml_native.write(')')
ml_i.write(')')
ml_native.write('\n')
ml_i.write('\n')
if len(ip) > 5:
ml_native.write(' = "n_%s_bytecode"\n' % ml_method_name(name))
ml_native.write(' "n_%s"\n' % ml_method_name(name))
else:
ml_native.write(' = "n_%s"\n' % ml_method_name(name))
ml_native.write('\n')
ml_native.write(' end\n\n')
ml_i.write('\n(**/**)\n');
# Exception wrappers
for name, result, params in _dotnet_decls:
ip = inparams(params)
op = outparams(params)
ml_native.write(' let %s ' % ml_method_name(name))
first = True
i = 0;
for p in params:
if is_in_param(p):
if first:
first = False;
else:
ml_native.write(' ')
ml_native.write('a%d' % i)
i = i + 1
if len(ip) == 0:
ml_native.write('()')
ml_native.write(' = \n')
ml_native.write(' ')
if result == VOID and len(op) == 0:
ml_native.write('let _ = ')
else:
ml_native.write('let res = ')
ml_native.write('(ML2C.n_%s' % (ml_method_name(name)))
if len(ip) == 0:
ml_native.write(' ()')
first = True
i = 0;
for p in params:
if is_in_param(p):
ml_native.write(' a%d' % i)
i = i + 1
ml_native.write(') in\n')
if name not in Unwrapped and len(params) > 0 and param_type(params[0]) == CONTEXT:
ml_native.write(' let err = (error_code_of_int (ML2C.n_get_error_code a0)) in \n')
ml_native.write(' if err <> OK then\n')
ml_native.write(' raise (Exception (ML2C.n_get_error_msg_ex a0 (int_of_error_code err)))\n')
ml_native.write(' else\n')
if result == VOID and len(op) == 0:
ml_native.write(' ()\n')
else:
ml_native.write(' res\n')
ml_native.write('\n')
ml_native.write('(**/**)\n')
# C interface
ml_wrapper = open(ml_wrapperf, 'w')
ml_wrapper.write('// Automatically generated file\n\n')
ml_wrapper.write('#include <stddef.h>\n')
ml_wrapper.write('#include <string.h>\n\n')
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('extern "C" {\n')
ml_wrapper.write('#endif\n')
ml_wrapper.write('#include <caml/mlvalues.h>\n')
ml_wrapper.write('#include <caml/memory.h>\n')
ml_wrapper.write('#include <caml/alloc.h>\n')
ml_wrapper.write('#include <caml/fail.h>\n')
ml_wrapper.write('#include <caml/callback.h>\n')
ml_wrapper.write('#ifdef Custom_tag\n')
ml_wrapper.write('#include <caml/custom.h>\n')
ml_wrapper.write('#include <caml/bigarray.h>\n')
ml_wrapper.write('#endif\n')
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('}\n')
ml_wrapper.write('#endif\n\n')
ml_wrapper.write('#include <z3.h>\n\n')
ml_wrapper.write('#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \\\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLlocal1(X6) \n')
ml_wrapper.write('#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \\\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLlocal2(X6,X7) \n')
ml_wrapper.write('#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLlocal3(X6,X7,X8) \n')
ml_wrapper.write('\n')
ml_wrapper.write('#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam2(X6,X7) \n')
ml_wrapper.write('#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam3(X6,X7,X8) \n')
ml_wrapper.write('#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam4(X6,X7,X8,X9) \n')
ml_wrapper.write('#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n')
ml_wrapper.write(' CAMLxparam2(X11,X12) \n')
ml_wrapper.write('#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n')
ml_wrapper.write(' CAMLxparam3(X11,X12,X13) \n')
ml_wrapper.write('\n\n')
ml_wrapper.write('static struct custom_operations default_custom_ops = {\n')
ml_wrapper.write(' (char*) "default handling",\n')
ml_wrapper.write(' custom_finalize_default,\n')
ml_wrapper.write(' custom_compare_default,\n')
ml_wrapper.write(' custom_hash_default,\n')
ml_wrapper.write(' custom_serialize_default,\n')
ml_wrapper.write(' custom_deserialize_default\n')
ml_wrapper.write('};\n\n')
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('extern "C" {\n')
ml_wrapper.write('#endif\n\n')
ml_wrapper.write('CAMLprim value n_is_null(value p) {\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('CAMLprim value n_mk_null( void ) {\n')
ml_wrapper.write(' CAMLparam0();\n')
ml_wrapper.write(' CAMLlocal1(result);\n')
ml_wrapper.write(' void * z3_result = 0;\n')
ml_wrapper.write(' result = caml_alloc_custom(&default_custom_ops, sizeof(void*), 0, 1);\n')
ml_wrapper.write(' memcpy( Data_custom_val(result), &z3_result, sizeof(void*));\n')
ml_wrapper.write(' CAMLreturn (result);\n')
ml_wrapper.write('}\n\n')
ml_wrapper.write('void MLErrorHandler(Z3_context c, Z3_error_code e)\n')
ml_wrapper.write('{\n')
ml_wrapper.write(' // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n')
ml_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n')
ml_wrapper.write(' // wrappers below.\n')
ml_wrapper.write('}\n\n')
ml_wrapper.write('void n_set_internal_error_handler(value a0)\n')
ml_wrapper.write('{\n')
ml_wrapper.write(' Z3_context _a0 = * (Z3_context*) Data_custom_val(a0);\n')
ml_wrapper.write(' Z3_set_error_handler(_a0, MLErrorHandler);\n')
ml_wrapper.write('}\n\n')
for name, result, params in _dotnet_decls:
ip = inparams(params)
op = outparams(params)
ap = arrayparams(params)
ret_size = len(op)
if result != VOID:
ret_size = ret_size + 1
# Setup frame
ml_wrapper.write('CAMLprim value n_%s(' % ml_method_name(name))
first = True
i = 0
for p in params:
if is_in_param(p):
if first:
first = False
else:
ml_wrapper.write(', ')
ml_wrapper.write('value a%d' % i)
i = i + 1
ml_wrapper.write(') {\n')
ml_wrapper.write(' CAMLparam%d(' % len(ip))
i = 0
first = True
for p in params:
if is_in_param(p):
if first:
first = False
else:
ml_wrapper.write(', ')
ml_wrapper.write('a%d' % i)
i = i + 1
ml_wrapper.write(');\n')
i = 0
if len(op) + len(ap) == 0:
ml_wrapper.write(' CAMLlocal1(result);\n')
else:
c = 0
for p in params:
if is_out_param(p) or is_array_param(p):
c = c + 1
ml_wrapper.write(' CAMLlocal%s(result, res_val' % (c+2))
for p in params:
if is_out_param(p) or is_array_param(p):
ml_wrapper.write(', _a%s_val' % i)
i = i + 1
ml_wrapper.write(');\n')
if len(ap) != 0:
ml_wrapper.write(' unsigned _i;\n')
# declare locals, preprocess arrays, strings, in/out arguments
i = 0
for param in params:
k = param_kind(param)
if k == OUT_ARRAY:
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % (
type2str(param_type(param)),
i,
type2str(param_type(param)),
type2str(param_type(param)),
param_array_capacity_pos(param)))
elif k == OUT_MANAGED_ARRAY:
ml_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i))
elif k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param)
ts = type2str(t)
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param)))
elif k == IN:
t = param_type(param)
ml_wrapper.write(' %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i))))
elif k == OUT:
ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
elif k == INOUT:
ml_wrapper.write(' %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i))
i = i + 1
if result != VOID:
ml_wrapper.write(' %s z3_result;\n' % type2str(result))
i = 0
for param in params:
k = param_kind(param)
if k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param)
ts = type2str(t)
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) { _a%s[_i] = %s; }\n' % (param_array_capacity_pos(param), i, ml_unwrap(t, ts, 'Field(a' + str(i) + ', _i)')))
i = i + 1
# invoke procedure
ml_wrapper.write(' ')
if result != VOID:
ml_wrapper.write('z3_result = ')
ml_wrapper.write('%s(' % name)
i = 0
first = True
for param in params:
if first:
first = False
else:
ml_wrapper.write(', ')
k = param_kind(param)
if k == OUT or k == INOUT or k == OUT_MANAGED_ARRAY:
ml_wrapper.write('&_a%s' % i)
else:
ml_wrapper.write('_a%i' % i)
i = i + 1
ml_wrapper.write(');\n')
# convert output params
if len(op) > 0:
if result != VOID:
ml_wrapper.write(' %s\n' % ml_set_wrap(result, "res_val", "z3_result"))
i = 0;
for p in params:
if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p)))
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) { value t; %s Store_field(_a%s_val, _i, t); }\n' % (param_array_capacity_pos(p), ml_set_wrap(param_type(p), 't', '_a' + str(i) + '[_i]'), i))
elif param_kind(p) == OUT_MANAGED_ARRAY:
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) ))
elif is_out_param(p):
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) ))
i = i + 1
# return tuples
if len(op) == 0:
ml_wrapper.write(' %s\n' % ml_set_wrap(result, "result", "z3_result"))
else:
ml_wrapper.write(' result = caml_alloc(%s, 0);\n' % ret_size)
i = j = 0
if result != VOID:
ml_wrapper.write(' Store_field(result, 0, res_val);\n')
j = j + 1
for p in params:
if is_out_param(p):
ml_wrapper.write(' Store_field(result, %s, _a%s_val);\n' % (j, i))
j = j + 1;
i = i + 1
# local array cleanup
i = 0
for p in params:
k = param_kind(p)
if k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY:
ml_wrapper.write(' free(_a%s);\n' % i)
i = i + 1
# return
ml_wrapper.write(' CAMLreturn(result);\n')
ml_wrapper.write('}\n\n')
if len(ip) > 5:
ml_wrapper.write('CAMLprim value n_%s_bytecode(value * argv, int argn) {\n' % ml_method_name(name))
ml_wrapper.write(' return n_%s(' % ml_method_name(name))
i = 0
while i < len(ip):
if i == 0:
ml_wrapper.write('argv[0]')
else:
ml_wrapper.write(', argv[%s]' % i)
i = i + 1
ml_wrapper.write(');\n}\n')
ml_wrapper.write('\n\n')
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('}\n')
ml_wrapper.write('#endif\n')
if is_verbose():
print ('Generated "%s"' % ml_nativef)
# Collect API(...) commands from
def def_APIs():
pat1 = re.compile(" *def_API.*")
@ -1067,6 +1547,7 @@ mk_py_wrappers()
mk_dotnet()
mk_dotnet_wrappers()
mk_java()
mk_ml()
log_h.close()
log_c.close()

2
src/api/dotnet/Expr.cs
View file

@ -1311,7 +1311,7 @@ namespace Microsoft.Z3
#region Relational Terms
/// <summary>
/// Indicates whether the term is of an array sort.
/// Indicates whether the term is of relation sort.
/// </summary>
public bool IsRelation
{

2
src/api/dotnet/Params.cs
View file

@ -23,7 +23,7 @@ using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// A ParameterSet represents a configuration in the form of Symbol/value pairs.
/// A Params objects represents a configuration in the form of Symbol/value pairs.
/// </summary>
[ContractVerification(true)]
public class Params : Z3Object

11
src/api/ml/META Normal file
View file

@ -0,0 +1,11 @@
# META file for the "z3" package:
version = "VERSION"
description = "Z3 Theorem Prover (OCaml API)"
requires = "num"
archive(byte) = "z3ml.cma"
archive(native) = "z3ml.cmxa"
archive(byte,plugin) = "z3ml.cma"
archive(native,plugin) = "z3ml.cmxa"
archive(byte,toploop) = "z3ml.cma"
archive(native,toploop) = "z3ml.cmxa"
linkopts = "-cclib -lz3"

20
src/api/ml/Makefile
View file

@ -1,14 +1,10 @@
# to set ARGS, invoke as e.g.: $ make ARGS='-DUNSAFE_ERRORS -DLEAK_CONTEXTS'
ARGS=
# This is a temporary support file for emacs annotations.
# It does not compile the Z3 ML API; this will be built
# in the top-level build directory.
all:
ocamlbuild -cflag -annot z3.cmxa
default: z3.ml z3.mli z3_stubs.c
%.ml %.mli %_stubs.c: ../%_api.h %.0.idl x3.ml x3V3.ml x3V3.mli \
error_handling.idl mlx_get_app_args.idl mlx_get_array_sort.idl mlx_get_datatype_sort.idl mlx_get_domains.idl mlx_get_error_msg.idl mlx_get_pattern_terms.idl mlx_get_tuple_sort.idl mlx_mk_context_x.idl mlx_mk_datatypes.idl mlx_mk_numeral.idl mlx_mk_sort.idl mlx_mk_symbol.idl mlx_model.idl mlx_numeral_refine.idl mlx_parse_smtlib.idl mlx_sort_refine.idl mlx_statistics.idl mlx_symbol_refine.idl mlx_term_refine.idl \
generate_mlapi.sh add_error_checking.V3.sed add_error_checking.sed preprocess.sed postprocess.sed reverse.sed
./generate_mlapi.sh $(ARGS)
clean:
rm -f z3.ml z3.mli z3_stubs.c
doc: *.ml
mkdir -p doc
ocamldoc -html -d doc -I _build -sort *.mli -hide Z3

69
src/api/ml/Makefile.build
View file

@ -1,69 +0,0 @@
# Makefile to compile OCaml interface to Z3
#
# Parameters: ARGS and DEPS environment variables
# ARGS is passed through to the Makefile that generates the OCaml interface
# DEPS is a sequence of files that are deleted when the OCaml interface changes
SRC_ML=../../../src/api/ml
ifeq (${OS}, Windows_NT)
# the BLD_ML path ends up stored in z3.cm{,x}a, so it must be in windows format
BLD_ML=$(shell cygpath -m $(CURDIR))
CFLAGS=-ccopt -wd4090 -ccopt -I$(SRC_ML)/..
XCDBG=-g $(CFLAGS)
XCOPT=-ccopt -Ox -ccopt -Oy- $(CFLAGS)
# ole32 is needed by camlidl (COM support)
XLIB=-cclib ole32.lib
AR=lib /nologo /LIBPATH:../../build ../../libz3.lib /out:
O=obj
A=lib
else
BLD_ML=$(CURDIR)
CFLAGS=-ccopt -Wno-discard-qual -ccopt -Wno-unused-variable -ccopt -I$(SRC_ML)/..
XCDBG=-g -ccopt -g $(CFLAGS)
XCOPT=-ccopt -O3 -ccopt -fomit-frame-pointer $(CFLAGS)
XLIB=
AR=ar rcs # note trailing space is significant
O=o
A=a
endif
all: z3.cma z3.cmxa ocamlz3
# keep these files to avoid repeatedly rebuilding them
.PRECIOUS: $(SRC_ML)/z3.ml $(SRC_ML)/z3.mli $(SRC_ML)/z3_stubs.c z3.ml z3.mli z3_stubs.c z3_theory_stubs.c
# regenerate OCaml API if needed
$(SRC_ML)/%.mli $(SRC_ML)/%.ml $(SRC_ML)/%_stubs.c: $(SRC_ML)/Makefile
make -C $(SRC_ML) z3.mli z3.ml z3_stubs.c
# copy OCaml API from src to build directories
%.mli %.ml %_stubs.c %_theory_stubs.c: $(SRC_ML)/%.mli $(SRC_ML)/%.ml $(SRC_ML)/%_stubs.c Makefile
cp $(SRC_ML)/z3.mli $(SRC_ML)/z3.ml $(SRC_ML)/z3_stubs.c $(SRC_ML)/z3_theory_stubs.c .
# OCaml library module for native code clients
%.cmxa %.cmi lib%stubs.a %.a: %.mli %.ml %_stubs.c %_theory_stubs.c Makefile
rm -f $(DEPS)
ocamlopt.opt -c $(XCOPT) z3.mli z3.ml z3_stubs.c z3_theory_stubs.c
$(AR)libz3stubs.$(A) z3.$(O) z3_stubs.$(O) z3_theory_stubs.$(O)
ocamlopt.opt -a -cclib -L$(BLD_ML)/../.. $(XLIB) -cclib -lcamlidl -cclib -lz3 -cclib -lz3stubs z3.cmx -o z3.cmxa
rm -f z3_theory_stubs.$(O) z3_stubs.$(O) z3.$(O) z3.cmx
# OCaml library module for byte code clients
%.cma %.cmi lib%stubs_dbg.a: %.mli %.ml %_stubs.c %_theory_stubs.c Makefile
rm -f $(DEPS)
ocamlc.opt -c $(XCDBG) z3.mli z3.ml z3_stubs.c z3_theory_stubs.c
$(AR)libz3stubs_dbg.$(A) z3_stubs.$(O) z3_theory_stubs.$(O)
ocamlc.opt -custom -a $(CXDBG) -cclib -L$(BLD_ML)/../.. $(XLIB) -cclib -lcamlidl -cclib -lz3 -cclib -lz3stubs_dbg z3.cmo -o z3.cma
rm -f z3_theory_stubs.$(O) z3_stubs.$(O) z3.cmo
# OCaml custom toplevel system pre-linked with Z3
ocamlz3: z3.cma Makefile
ocamlmktop -o ocamlz3 z3.cma -cclib -L.
clean: Makefile
make -C $(SRC_ML) clean
rm -rf Makefile libz3stubs.$(A) libz3stubs_dbg.$(A) ocamlz3 ocamlz3.dSYM z3.$(O) z3.$(A) z3.cma z3.cmi z3.cmo z3.cmx z3.cmxa z3.ml z3.mli z3_stubs.$(O) z3_stubs.c z3_theory_stubs.$(O) z3_theory_stubs.c

11
src/api/ml/README Normal file
View file

@ -0,0 +1,11 @@
This is the new ML API introduced with Z3 4.4. For the legacy bindings, please
refer to previous releases of Z3.
On Windows, there are no less than four different ports of OCaml. The Z3 build
system assumes that either the win32 or the win64 port is installed. This means
that OCaml will use `cl' as the underlying C compiler and not the cygwin or
mingw compilers.
By default, a make target called `ocamlfind_install' is added. This installs Z3
into the ocamlfind package repository such that programs can be compiled via
ocamlfind.

22
src/api/ml/README-linux
View file

@ -1,22 +0,0 @@
The OCaml API for Z3 was tested using OCaml 3.12.1.
You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- To build the OCaml API for Z3:
./build-lib.sh
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Remark: Building the OCaml API copies some pathnames into files,
so the OCaml API must be recompiled if the Z3 library files are moved.
See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3.
Acknowledgements:
The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg.
Many thanks to them!

22
src/api/ml/README-osx
View file

@ -1,22 +0,0 @@
The OCaml API for Z3 was tested using OCaml 3.12.1.
You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- To build the OCaml API for Z3:
./build-lib.sh
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Remark: Building the OCaml API copies some pathnames into files,
so the OCaml API must be recompiled if the Z3 library files are moved.
See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3.
Acknowledgements:
The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg.
Many thanks to them!

17
src/api/ml/README-test-linux
View file

@ -1,17 +0,0 @@
This directory contains scripts to build the test application using
OCaml. You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- One must build the OCaml library before compiling the example.
Go to directory ../ocaml
- Use 'build-test.sh' to build the test application using the OCaml compiler.
Remark: The OCaml and C compiler tool chains must be configured in your environment.
- Use 'exec.sh' to execute test_mlapi. The script sets LD_LIBRARY_PATH, and invokes test_mlapi.

17
src/api/ml/README-test-osx
View file

@ -1,17 +0,0 @@
This directory contains scripts to build the test application using
OCaml. You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- One must build the OCaml library before compiling the example.
Go to directory ../ocaml
- Use 'build-test.sh' to build the test application using the OCaml compiler.
Remark: The OCaml and C compiler tool chains must be configured in your environment.
- Use 'exec.sh' to execute test_mlapi. The script sets DYLD_LIBRARY_PATH, and invokes test_mlapi.

23
src/api/ml/README-test-win
View file

@ -1,23 +0,0 @@
This directory contains scripts to build the test application using
OCaml. You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- One must build the OCaml library before compiling the example.
Go to directory ../ocaml
- Use 'build-test.cmd' to build the test application using the OCaml compiler.
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Running from the Visual Studio Command Prompt configures the Microsoft C compiler.
- The script 'exec.cmd' adds the bin directory to the path. So,
test_mlapi.exe can find z3.dll.

23
src/api/ml/README-win
View file

@ -1,23 +0,0 @@
The OCaml API for Z3 was tested using OCaml 3.12.1.
You also need CamlIDL to be able to generate the OCaml API.
- To download OCaml:
http://caml.inria.fr/ocaml/
- To download CamlIDL:
http://forge.ocamlcore.org/projects/camlidl/
- To build the OCaml API for Z3:
.\build-lib.cmd
Remark: The OCaml and C compiler tool chains must be configured in your environment.
Running from the Visual Studio Command Prompt configures the Microsoft C compiler.
Remark: Building the OCaml API copies some pathnames into files,
so the OCaml API must be recompiled if the Z3 library files are moved.
See ..\examples\ocaml\build-test.cmd for an example of how to compile and link with Z3.
Acknowledgements:
The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg.
Many thanks to them!

2
src/api/ml/add_error_checking.V3.sed
View file

@ -1,2 +0,0 @@
# Customize error handling for contexts created in ML:
s/Z3_API Z3_mk_context(\(.*\))/Z3_API Z3_mk_context(\1) quote(dealloc,\"Z3_set_error_handler(_res, (void*)caml_z3_error_handler);\")/g

113
src/api/ml/add_error_checking.sed
View file

@ -1,113 +0,0 @@
# Do not add epilogue to Z3_del_context
/Z3_API .*Z3_del_context.*/b endt
# Add error checking epilogue for all Z3_API functions that accept two Z3_contexts
:begincc
# add epilogue for two Z3_context parameters and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5\6) quote(dealloc,\"check_error_code(\3);\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5) quote(dealloc,\"check_error_code(\3);\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\))[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5\6) quote(dealloc,\"check_error_code(\3);\")/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5) quote(dealloc,\"check_error_code(\3);\")/g
t endt
# if complete prototype, done with two Z3_contexts
/Z3_API .*(.*);[ ]*$/b endcc
/Z3_API .*(.*)[ ]*$/b endcc
# if incomplete prototype
/Z3_API .*(.*/{
# read another line
N
# add epilogue for two Z3_context parameters and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5\6) quote(dealloc,\"check_error_code(\3); check_error_code(\5);\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5) quote(dealloc,\"check_error_code(\3); check_error_code(\5);\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\))[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5\6) quote(dealloc,\"check_error_code(\3); check_error_code(\5);\")/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\(.*\)Z3_context \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_context \3\4Z3_context \5) quote(dealloc,\"check_error_code(\3); check_error_code(\5);\")/g
t endt
# else keep looking for two Z3_contexts
b begincc
}
:endcc
# Add error checking epilogue for all Z3_API functions that accept one Z3_context
:beginc
# add epilogue for one Z3_context parameter and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_context \3\4) quote(dealloc,\"check_error_code(\3);\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_context \3) quote(dealloc,\"check_error_code(\3);\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\)[ ]*$/Z3_API \1(\2Z3_context \3\4) quote(dealloc,\"check_error_code(\3);\")/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_context \3) quote(dealloc,\"check_error_code(\3);\")/g
t endt
# if complete prototype, done with all Z3_contexts
/Z3_API .*(.*);[ ]*$/b endc
/Z3_API .*(.*)[ ]*$/b endc
# if incomplete prototype
/Z3_API .*(.*/{
# read another line
N
# add epilogue for one Z3_context parameter and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_context \3\4) quote(dealloc,\"check_error_code(\3);\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_context \3) quote(dealloc,\"check_error_code(\3);\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\)\([^a-zA-Z].*\))[ ]*$/Z3_API \1(\2Z3_context \3\4) quote(dealloc,\"check_error_code(\3);\")/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_context \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_context \3) quote(dealloc,\"check_error_code(\3);\")/g
t endt
# else keep looking for one Z3_context
b beginc
}
:endc
# Add error checking epilogue for all Z3_API functions that accept a Z3_theory
:begint
# add epilogue for one Z3_theory parameter and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_theory \3\4) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_theory \3) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\)\([^a-zA-Z].*\))[ ]*$/Z3_API \1(\2Z3_theory \3\4) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\")/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_theory \3) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\")/g
t endt
# if complete prototype, done with all Z3_theorys
/Z3_API .*(.*);[ ]*$/b endt
/Z3_API .*(.*)[ ]*$/b endt
/Z3_API .*(.*/{
# read another line
N
# add epilogue for one Z3_theory parameter and if a match was found, done with all Z3_contexts and Z3_theorys so jump to endt
s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\)\([^a-zA-Z].*\));[ ]*$/Z3_API \1(\2Z3_theory \3\4) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\));[ ]*$/Z3_API \1(\2Z3_theory \3) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\");/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\)\([^a-zA-Z].*\))[ ]*$/Z3_API \1(\2Z3_theory \3\4) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\")/g
t endt
s/Z3_API \(.*\)(\(.*\)Z3_theory \([a-zA-Z]*\))[ ]*$/Z3_API \1(\2Z3_theory \3) quote(dealloc,\"check_error_code(Z3_theory_get_context(\3));\")/g
t endt
# else keep looking for one Z3_theory
b begint
}
:endt

3
src/api/ml/build-lib.cmd
View file

@ -1,3 +0,0 @@
@echo off
call .\compile_mlapi.cmd ..\include ..\bin ..\bin

31
src/api/ml/build-lib.sh
View file

@ -1,31 +0,0 @@
#!/bin/bash
# Script to compile the Z3 OCaml API
# Expects to find ../lib/libz3{,_dbg}.{a,so,dylib}
CFLAGS="-ccopt -Wno-discard-qual -ccopt -I../include"
XCDBG="-g -ccopt -g $CFLAGS"
XCOPT="-ccopt -O3 -ccopt -fomit-frame-pointer $CFLAGS"
ocamlc -c $XCDBG z3_stubs.c z3_theory_stubs.c z3.mli z3.ml
ocamlopt -c $XCDBG z3_stubs.c z3_theory_stubs.c z3.mli z3.ml
ar rcs libz3stubs_dbg.a z3.o z3_stubs.o z3_theory_stubs.o
ocamlopt -c $XCOPT z3_stubs.c z3_theory_stubs.c z3.mli z3.ml
ar rcs libz3stubs.a z3.o z3_stubs.o z3_theory_stubs.o
ocamlc -custom -a $XCDBG -cclib -L$PWD/../lib -cclib -lz3_dbg -cclib -lcamlidl -cclib -lz3stubs_dbg z3.cmo -o z3_dbg.cma
ocamlc -custom -a $XCDBG -cclib -L$PWD/../lib -cclib -lz3 -cclib -lcamlidl -cclib -lz3stubs z3.cmo -o z3.cma
ocamlopt -a $XCDBG -cclib -L$PWD/../lib -cclib -lz3_dbg -cclib -lcamlidl -cclib -lz3stubs_dbg z3.cmx -o z3_dbg.cmxa
ocamlopt -a $XCOPT -cclib -L$PWD/../lib -cclib -lz3 -cclib -lcamlidl -cclib -lz3stubs z3.cmx -o z3.cmxa
ocamlmktop -o ocamlz3 z3.cma -cclib -L.
rm z3.cm{o,x} *.o

19
src/api/ml/build-test.cmd
View file

@ -1,19 +0,0 @@
@echo off
if not exist ..\..\ocaml\z3.cmxa (
echo "YOU MUST BUILD OCAML API! Go to directory ..\ocaml"
goto :EOF
)
REM ocaml (>= 3.11) calls the linker through flexlink
ocamlc -version >> ocaml_version
set /p OCAML_VERSION= <ocaml_version
if %OCAML_VERSION% GEQ 3.11 (
set XCFLAGS=
) else (
set XCFLAGS=/nologo /MT /DWIN32
)
ocamlc -w A -ccopt "%XCFLAGS%" -o test_mlapi_byte.exe -I ..\..\ocaml z3.cma test_mlapi.ml
ocamlopt -w A -ccopt "%XCFLAGS%" -o test_mlapi.exe -I ..\..\ocaml z3.cmxa test_mlapi.ml

6
src/api/ml/build-test.sh
View file

@ -1,6 +0,0 @@
#!/bin/bash
ocamlc -o test_mlapi.byte -I ../../ocaml/ z3.cma test_mlapi.ml
ocamlopt -o test_mlapi -I ../../ocaml/ z3.cmxa test_mlapi.ml
rm *.cm{i,o,x} *.o

53
src/api/ml/build.cmd
View file

@ -1,53 +0,0 @@
@echo off
SETLOCAL
REM Script to generate, compile, test, and document the Z3 OCaml API
REM
REM Assumes that environment variables are set to provide access to the C and OCaml compilers, including flexdll and camlidl, as well as the following commands: diff, dos2unix, grep, sed, unix2dos
REM
REM usage: build.cmd [32|64] [-D UNSAFE_ERRORS] [-D LEAK_CONTEXTS]
REM
REM Invoke with "-D UNSAFE_ERRORS" to build version that does not support recoverable errors, but avoids some error-checking overhead.
REM Invoke with "-D LEAK_CONTEXTS" to build version that leaks Z3_context objects, but avoids some garbage-collection overhead.
if ""%1 == "" (
set BITS=32
) else (
set BITS=%1
)
if %BITS% == 32 (
set ARCH=x86
set Z3BIN= ..\external
set Z3DBG= ..\Debug
) else (
set ARCH=x64
set Z3BIN= ..\x64\external_64
set Z3DBG= ..\x64\Debug
)
echo { Cleaning
call .\clean.cmd
echo }
echo { Generating OCaml API %3 %5
call .\generate_mlapi.cmd %2 %3 %4 %5
if errorlevel 1 goto :EOF
echo }
echo { Compiling OCaml API
call .\compile_mlapi.cmd ..\lib %Z3BIN% %Z3DBG%
if errorlevel 1 goto :EOF
echo }
echo { Testing OCaml API
call .\test_mlapi.cmd ..\lib %Z3BIN% %Z3DBG%
if errorlevel 1 goto :EOF
echo }
echo { Generating OCaml API documentation
call .\update-ml-doc.cmd ..\doc
if errorlevel 1 goto :EOF
echo }
ENDLOCAL

13
src/api/ml/clean.cmd
View file

@ -1,13 +0,0 @@
@echo off
REM Script to delete generated Z3 OCaml API files
call .\cleantmp.cmd
REM files produced by generate_mlapi.cmd
del /q 2>NUL z3_stubs.c z3.mli z3.ml z3V3_stubs.*.c z3V3.*.mli z3V3.*.ml
REM files produced by update-ml-doc.cmd
rd 2>NUL /s /q doc
exit /B 0

15
src/api/ml/cleantmp.cmd
View file

@ -1,15 +0,0 @@
@echo off
REM Script to delete intermediate temporary files from generating Z3 OCaml API
REM files produced by generate_mlapi.cmd
del /q 2>NUL z3_api.idl
REM files produced by compile_mlapi.cmd
del /q 2>NUL *.cmi *.cmo *.cmx *.cma *.cmxa *.obj *.lib *.pdb ocamlz3.exe
REM files produced by test_mlapi.cmd
del /q 2>NUL test*.exe queen*.exe test_*api.out test_*apiV3.out test_*api.err test_*apiV3.err queen.out queen.err z3.log ml.log test_mlapi.log .z3-trace
REM backup files
del /q 2>NUL *~

98
src/api/ml/compile_mlapi.cmd
View file

@ -1,98 +0,0 @@
@echo off
SETLOCAL
REM Script to compile the Z3 OCaml API
REM
REM Compiles byte and debug native code versions with debug info, optimized native code versions without
REM
REM Assumes that environment variables are set to provide access to the C and OCaml compilers
REM directory containing z3_api.h
set Z3SRC=%1
REM directory containing z3.dll
set Z3BIN=%2
REM directory containing debug z3.dll
set Z3BINDBG=%3
REM link Z3 statically or dynamically
set STATIC=false
REM set STATIC=true
if %STATIC% == true (
set Z3LIB=z3lib.lib
set Z3DBGLIB=z3lib.lib
) else (
set Z3LIB=z3.lib
set Z3DBGLIB=z3.lib
)
REM ocaml 3.11 and later calls the linker through flexlink
ocamlc -version >> ocaml_version
set /p OCAML_VERSION= <ocaml_version
del ocaml_version
if %OCAML_VERSION% GEQ 3.11 (
set XCFLAGS=
) else (
REM add /MT if building the multithreaded version
set XCFLAGS=/nologo /DWIN32
)
set XINCLUDE=-ccopt -I%Z3SRC%
set XLIBPATH=/LIBPATH:%Z3BIN%
set XCDBG=-g %XCFLAGS% %XINCLUDE%
set XCOPT=-ccopt /Ox -ccopt /Oy- %XCFLAGS% %XINCLUDE%
REM z3_stubs.c z3_theory_stubs.c z3.mli z3.ml -> DBG z3_stubs.obj z3.{cmi,cmo,obj}
ocamlc -c %XCDBG% z3_stubs.c z3_theory_stubs.c z3.mli z3.ml
if errorlevel 1 goto :EOF
REM z3_stubs.c z3_theory_stubs.c z3.mli z3.ml -> DBG z3_stubs.obj z3.{cmi,cmx,obj}
ocamlopt -c %XCDBG% z3_stubs.c z3_theory_stubs.c z3.mli z3.ml
if errorlevel 1 goto :EOF
REM %Z3DBGLIB% z3.obj z3_stubs.obj z3_theory_stubs.obj -> libz3_dbg.lib:
lib /nologo %XLIBPATH% /out:libz3_dbg.lib %Z3BINDBG%\%Z3DBGLIB% z3.obj z3_stubs.obj z3_theory_stubs.obj
if errorlevel 1 goto :EOF
REM z3_stubs.c z3_theory_stubs.c z3.mli z3.ml -> OPT z3_stubs.obj z3.{cmi,cmx,obj}
ocamlopt -c %XCOPT% z3_stubs.c z3_theory_stubs.c z3.mli z3.ml
if errorlevel 1 goto :EOF
REM %Z3LIB% z3.obj z3_stubs.obj z3_theory_stubs.obj -> libz3.lib:
lib /nologo %XLIBPATH% /out:libz3.lib %Z3BIN%\%Z3LIB% z3.obj z3_stubs.obj z3_theory_stubs.obj
if errorlevel 1 goto :EOF
REM ole32.lib is needed by camlidl
REM camlidl.lib is the runtime library for camlidl
REM psapi.lib is needed when statically linking Z3 for process statistics functions
REM libz3_dbg.lib ole32.lib camlidl.lib z3.cmo -> z3_dbg.cma
ocamlc -custom -a %XCDBG% -cclib -L"%CD%\..\bin" -cclib -lz3_dbg -cclib ole32.lib -cclib -lcamlidl -cclib psapi.lib z3.cmo -o z3_dbg.cma
if errorlevel 1 goto :EOF
REM libz3.lib ole32.lib camlidl.lib z3.cmo -> z3.cma
ocamlc -custom -a -cclib -L"%CD%\..\bin" -cclib -lz3 -cclib ole32.lib -cclib -lcamlidl -cclib psapi.lib z3.cmo -o z3.cma
if errorlevel 1 goto :EOF
REM libz3_dbg.lib ole32.lib camlidl.lib z3.cmx -> z3_dbg.cmxa
ocamlopt -a -cclib -L"%CD%\..\bin" -cclib -lz3_dbg -cclib ole32.lib -cclib -lcamlidl -cclib psapi.lib z3.cmx -o z3_dbg.cmxa
if errorlevel 1 goto :EOF
REM libz3.lib ole32.lib camlidl.lib z3.cmx -> z3.cmxa
ocamlopt -a -cclib -L"%CD%\..\bin" -cclib -lz3 -cclib ole32.lib -cclib -lcamlidl -cclib psapi.lib z3.cmx -o z3.cmxa
if errorlevel 1 goto :EOF
REM build OCaml toplevel 'ocamlz3' pre-linked with Z3
ocamlmktop -o ocamlz3 z3.cma
if errorlevel 1 goto :EOF
del /q 2>NUL z3.cmo z3.cmx *.obj
ENDLOCAL

165
src/api/ml/error_handling.idl
View file

@ -1,165 +0,0 @@
/*++
Copyright (c) Microsoft Corporation
Module Name:
error_handling
Abstract:
Error handling in the OCaml API for Z3.
The wrapper of each Z3 API routine that takes a Z3_context or a Z3_theory
argument calls check_error_code before returning. (These calls are added
in generate_mlapi.cmd using the build.sed script.)
There are two error handling schemes implemented, depending on whether
(UN)SAFE_ERRORS is set.
- SAFE_ERRORS checks Z3_error_code after each call and raises an OCaml
exception in error conditions. Z3_set_error_handler is not exposed by
the SAFE_ERRORS version.
- UNSAFE_ERRORS sets a Z3 error handler routine that either calls a
globally registered OCaml function or, by default, raises an OCaml
exception. This avoids overhead of repeatedly checking
Z3_get_error_code, but leaves Z3 in a broken state.
Notes:
The current SAFE_ERRORS implementation interacts badly with theory plugin
callbacks. Z3 errors are converted into OCaml exceptions, which the
wrappers of theory plugin callbacks are not expecting. Therefore, if a
theory plugin calls a Z3 API routine that triggers an error, an OCaml
exception will be raised and bypass any C++ destructors pushed onto the
stack by Z3 before the call to the plugin and after the preceding OCaml
exception handler. One solution to this would be to modify the theory
plugin callback registration functions to wrap callbacks in an OCaml
exception handler. Since OCaml exceptions are cheap to raise at the
expense of some cost to install a handler, this may not be desirable.
Another solution would be to modify check_error_code to detect if it is
executing in a plugin callback and simply maintain the Z3_error_code, or
raise a C++ exception, instead of raising an OCaml exception.
Author:
Josh Berdine (jjb) 2012-03-21
--*/
#if !defined(UNSAFE_ERRORS) && !defined(SAFE_ERRORS)
#define SAFE_ERRORS
#endif
// The V3 API uses a single handler irregardless of UNSAFE_ERRORS
quote(c,"
/* All contexts share the same handler */
static value caml_z3_error_handler = 0;
");
#ifdef SAFE_ERRORS
quote(mlmli,"
(** Exceptions raised by Z3. It is safe to continue interacting with Z3 after
catching [Error] exceptions.
- {b See also}: {!get_error_msg}
*)
exception Error of context * error_code
");
quote(ml,"
(* Register dynamically-generated exception tag for use from C *)
let _ = Callback.register_exception \"Z3.Error\" (Error (Obj.magic None, OK))
");
quote(c,"
value camlidl_c2ml_z3_Z3_error_code(Z3_error_code * _c2, camlidl_ctx _ctx);
/* Error checking routine that raises OCaml Error exceptions */
void check_error_code (Z3_context c)
{
static struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
value* exn_tag = NULL;
value ctx_err[2];
Z3_error_code e;
e = Z3_get_error_code(c);
if (e != Z3_OK) {
ctx_err[0] = c2ml_Z3_context(&c);
ctx_err[1] = camlidl_c2ml_z3_Z3_error_code(&e, &_ctxs);
exn_tag = caml_named_value(\"Z3.Error\");
if (*exn_tag == 0) {
fprintf(stderr, \"Z3.Error not found\");
exit(1);
}
caml_raise_with_args(*exn_tag, 2, ctx_err);
}
}
/* Disable default error handler, all error checking is done by check_error_code */
void* error_handler_static = NULL;
");
#else
quote(mlmli,"
(** Exceptions raised by Z3. {b Warning}: It is unsafe to continue
interacting with Z3 after catching [Error] exceptions. To recover from
error conditions, use {!set_error_handler} to set an error handler that
does nothing, and then test {!get_error_code} after every call to Z3.
- {b See also}: {!get_error_msg}
*)
exception Error of context * error_code
");
quote(ml,"
(* Register dynamically-generated exception tag for use from C *)
let _ = Callback.register_exception \"Z3.Error\" (Error (Obj.magic None, OK))
");
quote(c,"
/* Error checking routine that does nothing */
void check_error_code(Z3_context c) {}
static void error_handler_static (Z3_context c, Z3_error_code e)
{
static struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
value* exn_tag = NULL;
value ctx_err[2];
ctx_err[0] = c2ml_Z3_context(&c);
ctx_err[1] = camlidl_c2ml_z3_Z3_error_code(&e, &_ctxs);
if (caml_z3_error_handler) {
caml_callback2(caml_z3_error_handler, ctx_err[0], ctx_err[1]);
} else {
/* if no handler set, raise OCaml Error exception */
exn_tag = caml_named_value(\"Z3.Error\");
if (*exn_tag == 0) {
fprintf(stderr, \"Z3.Error not found\");
exit(1);
}
caml_raise_with_args(*exn_tag, 2, ctx_err);
}
}
void ml2c_Z3_error_handler (value ml_handler, void* c_handler)
{
caml_z3_error_handler = ml_handler;
c_handler = (void*)error_handler_static;
}
/* Never called */
value c2ml_Z3_error_handler (void* _)
{
return 0;
}
");
typedef [mltype("context -> error_code -> unit"),
ml2c(ml2c_Z3_error_handler),
c2ml(c2ml_Z3_error_handler)
] void Z3_error_handler;
quote(c,"#define Z3_error_handler void*");
#endif

5
src/api/ml/exec.cmd
View file

@ -1,5 +0,0 @@
@echo off
SETLOCAL
set PATH=..\..\bin;%PATH%
test_mlapi.exe
ENDLOCAL

4
src/api/ml/exec.sh
View file

@ -1,4 +0,0 @@
#!/bin/sh
export LD_LIBRARY_PATH=../../lib:$LD_LIBRARY_PATH # for linux
export DYLD_LIBRARY_PATH=../../lib:$DYLD_LIBRARY_PATH # for osx
./test_mlapi

72
src/api/ml/generate_mlapi.cmd
View file

@ -1,72 +0,0 @@
@echo off
REM Script to generate the Z3 OCaml API
REM
REM Assumes that environment variables are set to provide access to the following commands: camlidl, dos2unix, grep, sed, unix2dos
REM
REM Invoke with "-D UNSAFE_ERRORS" to build version that does not support recoverable errors, but avoids some error-checking overhead.
REM Invoke with "-D LEAK_CONTEXTS" to build version that leaks Z3_context objects, but avoids some garbage-collection overhead.
REM ../lib/z3_api.h -> z3V3_api.idl using add_error_checking.V3.sed and build.sed
sed -f add_error_checking.V3.sed ../lib/z3_api.h | sed -f build.sed >z3V3_api.idl
if errorlevel 1 goto :EOF
REM z3.idl -> z3V3_stubs.c, z3V3.mli, z3V3.ml
camlidl -D MLAPIV3 %* z3.idl
move >NUL z3_stubs.c z3V3_stubs.c
move >NUL z3.ml z3V3.ml
move >NUL z3.mli z3V3.mli
if errorlevel 1 goto :EOF
REM ../lib/z3_api.h -> z3_api.idl
REM add calls to error checking routine
REM convert from doxygen to ocamldoc markup and other syntactic munging
sed <../lib/z3_api.h -f add_error_checking.sed | ^
sed -f build.sed >z3_api.idl
if errorlevel 1 goto :EOF
REM z3.idl -> z3_stubs.c, z3.mli, z3.ml
camlidl %* z3.idl
if errorlevel 1 goto :EOF
REM sometimes z3_stubs.c can be generated with mixed line endings, which can confuse sed and grep
dos2unix 2>NUL z3V3_stubs.c ; unix2dos 2>NUL z3V3_stubs.c
dos2unix 2>NUL z3_stubs.c ; unix2dos 2>NUL z3_stubs.c
REM modify generated z3.ml{,i} to remove "Z3_" prefix from names
move >NUL z3V3.mli z3V3.1.mli && sed "s/{\!Z3\./{!/g;s/\<[zZ]3_//g" z3V3.1.mli >z3V3.mli && del z3V3.1.mli
move >NUL z3V3.ml z3V3.1.ml && sed "s/{\!Z3\./{!/g;s/\<[zZ]3_//g" z3V3.1.ml >z3V3.ml && del z3V3.1.ml
move >NUL z3.mli z3.1.mli && sed "s/{\!Z3\./{!/g;s/\<[zZ]3_//g" z3.1.mli >z3.mli && del z3.1.mli
move >NUL z3.ml z3.1.ml && sed "s/{\!Z3\./{!/g;s/\<[zZ]3_//g" z3.1.ml >z3.ml && del z3.1.ml
REM modify generated z3V3 files to rename z3_ to z3V3_
move >NUL z3V3.mli z3V3.2.mli && sed "s/camlidl\(.*\)_z3_/camlidl\1_z3V3_/g" z3V3.2.mli >z3V3.mli && del z3V3.2.mli
move >NUL z3V3.ml z3V3.2.ml && sed "s/camlidl\(.*\)_z3_/camlidl\1_z3V3_/g" z3V3.2.ml >z3V3.ml && del z3V3.2.ml
move >NUL z3V3_stubs.c z3V3_stubs.2.c && sed "s/camlidl\(.*\)_z3_/camlidl\1_z3V3_/g" z3V3_stubs.2.c >z3V3_stubs.c && del z3V3_stubs.2.c
REM substitute out type equations for enums and options
REM reverse order of substitution of enums to avoid matching prefixes such as enum_1 of enum_10
grep "^and \([a-z][a-zA-Z_]*\) = \([a-z][a-zA-Z_]*[0-9]*\)$" z3.mli | sed "s|and \([a-zA-Z_]*\) = \([ a-zA-Z_0-9]*\)|s/\2/\1/g|g" | sed "1!G;h;$!d" >rename.sed
grep "^and \([a-z][a-zA-Z_]*\) = \([a-z][a-zA-Z_]* option*\)$" z3.mli | sed "s|and \([a-zA-Z_]*\) = \([ a-zA-Z_0-9]*\)|s/\1/\2/g|g" >>rename.sed
move >NUL z3.mli z3.3.mli && sed -f rename.sed z3.3.mli >z3.mli && del z3.3.mli
move >NUL z3.ml z3.3.ml && sed -f rename.sed z3.3.ml >z3.ml && del z3.3.ml
del rename.sed
grep "^and \([a-z][a-zA-Z_]*\) = \([a-z][a-zA-Z_]*[0-9]*\)$" z3V3.mli | sed "s|and \([a-zA-Z_]*\) = \([ a-zA-Z_0-9]*\)|s/\2/\1/g|g" | sed "1!G;h;$!d" >rename.sed
grep "^and \([a-z][a-zA-Z_]*\) = \([a-z][a-zA-Z_]* option*\)$" z3V3.mli | sed "s|and \([a-zA-Z_]*\) = \([ a-zA-Z_0-9]*\)|s/\1/\2/g|g" >>rename.sed
move >NUL z3V3.mli z3V3.3.mli && sed -f rename.sed z3V3.3.mli >z3V3.mli && del z3V3.3.mli
move >NUL z3V3.ml z3V3.3.ml && sed -f rename.sed z3V3.3.ml >z3V3.ml && del z3V3.3.ml
del rename.sed
REM remove cyclic definitions introduced by substituting type equations
move >NUL z3V3.mli z3V3.4.mli && sed "s/^and \([a-z][a-zA-Z_ ]*\) = \1$//g" z3V3.4.mli >z3V3.mli && del z3V3.4.mli
move >NUL z3V3.ml z3V3.4.ml && sed "s/^and \([a-z][a-zA-Z_ ]*\) = \1$//g" z3V3.4.ml >z3V3.ml && del z3V3.4.ml
move >NUL z3.mli z3.4.mli && sed "s/^and \([a-z][a-zA-Z_ ]*\) = \1$//g" z3.4.mli >z3.mli && del z3.4.mli
move >NUL z3.ml z3.4.ml && sed "s/^and \([a-z][a-zA-Z_ ]*\) = \1$//g" z3.4.ml >z3.ml && del z3.4.ml
REM append Z3.V3 module onto Z3 module
type z3V3.ml >> z3.ml
type z3V3.mli >> z3.mli
sed "1,22d" z3V3_stubs.c >> z3_stubs.c
del /q 2>NUL z3V3_api.idl z3V3.ml z3V3.mli z3V3_stubs.c

53
src/api/ml/generate_mlapi.sh
View file

@ -1,53 +0,0 @@
#!/bin/bash
# Script to generate the Z3 OCaml API
#
# Assumes that environment variables are set to provide access to the following commands: camlidl, gcc, grep, sed
#
# This script uses 'gcc -E' as the C preprocessor, other C preprocessors may work but have not been tested.
#
# Invoke with "-DUNSAFE_ERRORS" to build version that does not support recoverable errors, but avoids some error-checking overhead.
# Invoke with "-DLEAK_CONTEXTS" to build version that leaks Z3_context objects, but avoids some garbage-collection overhead.
# add calls to error checking routine
# convert from doxygen to ocamldoc markup and other syntactic munging
# ../z3_api.h -> z3V3_api.idl
sed -f add_error_checking.V3.sed -f preprocess.sed ../z3_api.h > z3V3_api.idl
# z3.idl (z3V3_api.idl x3V3.mli x3V3.ml) -> z3V3_stubs.c, z3V3.mli, z3V3.ml
gcc -E -w -P -CC -xc -DCAMLIDL -DMLAPIV3 $@ z3.0.idl > z3V3.idl
camlidl -nocpp z3V3.idl
# reverse.sed to reverse order of substitution of enums to avoid matching prefixes such as enum_1 of enum_10
grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_]*$" z3V3.mli | sed -e "s|and z3_\([a-zA-Z0-9_]*\) = \([a-zA-Z0-9_]*\)|s/\2/\1/g|g" -f reverse.sed > /tmp/renameV3.sed
grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_ ]* option$" z3V3.mli | sed -e "s|and \(z3_[a-zA-Z0-9_]*\) = \([a-zA-Z0-9_ ]*\)|s/\1/\2/g|g" >> /tmp/renameV3.sed
# rename.sed to substitute out type equations for enums and options, then postprocess
cp -f z3V3.mli z3V3.ml /tmp
sed -f /tmp/renameV3.sed -f postprocess.sed /tmp/z3V3.mli > z3V3.mli
sed -f /tmp/renameV3.sed -f postprocess.sed /tmp/z3V3.ml > z3V3.ml
# ../z3_api.h -> z3_api.idl
sed -f add_error_checking.sed -f preprocess.sed ../z3_api.h > z3_api.idl
# z3.idl (z3_api.idl x3.ml) -> z3_stubs.c, z3.mli, z3.ml
gcc -E -w -P -CC -xc -I. -DCAMLIDL $@ z3.0.idl > z3.idl
camlidl -nocpp z3.idl
# reverse.sed to reverse order of substitution of enums to avoid matching prefixes such as enum_1 of enum_10
grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_]*$" z3.mli | sed -e "s|and z3_\([a-zA-Z0-9_]*\) = \([a-zA-Z0-9_]*\)|s/\2/\1/g|g" -f reverse.sed > /tmp/rename.sed
grep "^and z3_[a-zA-Z0-9_]* = [a-z][a-zA-Z0-9_ ]* option$" z3.mli | sed -e "s|and \(z3_[a-zA-Z0-9_]*\) = \([a-zA-Z0-9_ ]*\)|s/\1/\2/g|g" >> /tmp/rename.sed
# rename.sed to substitute out type equations for enums and options, then postprocess
cp z3.mli z3.ml /tmp
sed -f /tmp/rename.sed -f postprocess.sed /tmp/z3.mli > z3.mli
sed -f /tmp/rename.sed -f postprocess.sed /tmp/z3.ml > z3.ml
# append Z3.V3 module onto Z3 module
cat z3V3.mli >> z3.mli
cat z3V3.ml >> z3.ml
sed "1,22d" z3V3_stubs.c >> z3_stubs.c
rm -f z3V3_api.idl z3V3.idl z3V3.ml z3V3.mli z3V3_stubs.c z3_api.idl z3.idl

55
src/api/ml/import.cmd
View file

@ -1,55 +0,0 @@
@echo off
SETLOCAL
:CHECKARG1
if not "%1"=="" (
set SDTROOT=%1
goto :CHECKARG2
)
goto :FAIL
:CHECKARG2
if "%2"=="" (
goto :IMPORT
)
goto :FAIL
:IMPORT
cd import
sd edit ...
del z3.h z3_api.h z3_macros.h z3lib.lib msbig_rational.lib z3.exe test_capi.c test_mlapi_header.html z3_mlapi_header.html mldoc_footer.html tabs.css z3.png z3_ml.css
copy %SDTROOT%\lib\z3.h
copy %SDTROOT%\lib\z3_api.h
copy %SDTROOT%\lib\z3_macros.h
copy %SDTROOT%\release_mt\z3lib.lib
copy %SDTROOT%\release_mt\msbig_rational.lib
copy %SDTROOT%\release_mt\z3.exe
copy %SDTROOT%\test_capi\test_capi.c
copy %SDTROOT%\doc\test_mlapi_header.html
copy %SDTROOT%\doc\z3_mlapi_header.html
copy %SDTROOT%\doc\mldoc_footer.html
copy %SDTROOT%\doc\html\tabs.css
copy %SDTROOT%\doc\z3.png
copy %SDTROOT%\doc\z3_ml.css
sd add ...
sd revert -a ...
cd ..
goto :END
:FAIL
echo "Usage:"
echo " %0 SDTROOT"
echo ""
echo "Examples:"
echo " %0 \\risebuild\drops\z32\2.0.51220.7"
echo " %0 \\risebuild\drops\z32\latest"
echo " %0 J:\SD\other\sdt1\src\z3_2"
echo ""
goto :END
:END
ENDLOCAL

11
src/api/ml/mlx_get_app_args.idl
View file

@ -1,11 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mli,"
(**
Summary: \[ [ get_app_args c a ] \] is the array of arguments of an application. If [t] is a constant, then the array is empty.
- {b See also}: {!get_app_num_args}
- {b See also}: {!get_app_arg}
*)
val get_app_args: context -> app -> ast array
");

11
src/api/ml/mlx_get_array_sort.idl
View file

@ -1,11 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mli,"
(**
Summary: \[ [ get_array_sort c t ] \] is the domain and the range of [t].
- {b See also}: {!get_array_sort_domain}
- {b See also}: {!get_array_sort_range}
*)
val get_array_sort: context -> sort -> sort * sort
");

13
src/api/ml/mlx_get_datatype_sort.idl
View file

@ -1,13 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mli,"
(**
Summary: \[ [ get_datatype_sort c ty ] \] is the array of triples [(constructor, recognizer, fields)] where [constructor] is the constructor declaration of [ty], [recognizer] is the recognizer for the [constructor], and [fields] is the array of fields in [ty].
- {b See also}: {!get_datatype_sort_num_constructors}
- {b See also}: {!get_datatype_sort_constructor}
- {b See also}: {!get_datatype_sort_recognizer}
- {b See also}: {!get_datatype_sort_constructor_accessor}
*)
val get_datatype_sort: context -> sort -> datatype_constructor array
");

11
src/api/ml/mlx_get_domains.idl
View file

@ -1,11 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mli,"
(**
Summary: \[ [ get_domains c d ] \] is the array of parameters of [d].
- {b See also}: {!get_domain_size}
- {b See also}: {!get_domain}
*)
val get_domains: context -> func_decl -> sort array
");

6
src/api/ml/mlx_get_error_msg.idl
View file

@ -1,6 +0,0 @@
quote(mli,"
(**
Summary: Return a string describing the given error code.
*)
val get_error_msg: context -> error_code -> string
");

11
src/api/ml/mlx_get_pattern_terms.idl
View file

@ -1,11 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mli,"
(**
Summary: \[ [ get_pattern_terms c p ] \] is the ast's in pattern.
- {b See also}: {!get_pattern_num_terms}
- {b See also}: {!get_pattern}
*)
val get_pattern_terms: context -> pattern -> ast array;;
");

12
src/api/ml/mlx_get_tuple_sort.idl
View file

@ -1,12 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mli,"
(**
Summary: \[ [ get_tuple_sort c ty ] \] is the pair [(mk_decl, fields)] where [mk_decl] is the constructor declaration of [ty], and [fields] is the array of fields in [ty].
- {b See also}: {!get_tuple_sort_mk_decl}
- {b See also}: {!get_tuple_sort_num_fields}
- {b See also}: {!get_tuple_sort_field_decl}
*)
val get_tuple_sort: context -> sort -> (func_decl * func_decl array)
");

36
src/api/ml/mlx_mk_context_x.idl
View file

@ -1,36 +0,0 @@
quote(mlmli,"external mk_context: (string * string) list -> context = \"caml_z3_mk_context\"
");
// Note: lack of whitespace and comments in the previous 2 lines is important for the documentation generation
quote(c,"
value caml_z3_mk_context(value key_val_list)
{
CAMLparam1( key_val_list );
CAMLlocal4( item, vkey, vval, _vres );
char * ckey;
char * cval;
Z3_config cfg;
Z3_context _res;
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
camlidl_ctx _ctx = &_ctxs;
cfg = Z3_mk_config();
while (key_val_list != Val_emptylist)
{
item = Field(key_val_list, 0);
vkey = Field(item, 0);
vval = Field(item, 1);
ckey = camlidl_malloc_string(vkey, _ctx);
cval = camlidl_malloc_string(vval, _ctx);
Z3_set_param_value(cfg, ckey, cval);
key_val_list = Field(key_val_list, 1);
}
_res = Z3_mk_context_rc(cfg);
Z3_del_config(cfg);
_vres = camlidl_c2ml_z3_Z3_context(&_res, _ctx);
camlidl_free(_ctx);
Z3_set_error_handler(_res, error_handler_static);
CAMLreturn(_vres);
}
");

28
src/api/ml/mlx_mk_datatypes.idl
View file

@ -1,28 +0,0 @@
quote(mlmli,"
(** A constructor of a datatype is described by: *)
type datatype_constructor_desc = {
constructor_desc : symbol; (** name of the constructor function *)
recognizer_desc : symbol; (** name of the recognizer function *)
accessor_descs : (symbol * sort) array; (** names and sorts of the fields *)
}
(** A datatype is described by a name and constructor descriptors. *)
type datatype_desc = symbol * datatype_constructor_desc array
(** A constructor of a datatype is represented by: *)
type datatype_constructor = {
constructor : func_decl; (** constructor function *)
recognizer : func_decl; (** recognizer function *)
accessors : func_decl array; (** field accessor functions *)
}
(** A datatype is represented by a sort and constructors. *)
type datatype = sort * datatype_constructor array
");
quote(mli,"
(** [mk_datatypes ctx sorts_to_descriptors] creates mutually recursive datatypes described by
[sorts_to_descriptors], which is a function from the sorts of the datatypes to be created to
descriptors of the datatypes' constructors. {b See also}: {!Test_mlapi.forest_example} *)
val mk_datatypes: context -> (sort array -> (datatype_desc array) option) -> datatype array
");

21
src/api/ml/mlx_mk_numeral.idl
View file

@ -1,21 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mlmli,"
(**
Summary: \[ [ numeral_refined ] \] is the refined view of a numeral .
*)
type numeral_refined =
| Numeral_int of int * sort
| Numeral_int64 of int64 * sort
| Numeral_large of string * sort
| Numeral_rational of numeral_refined * numeral_refined
");
quote(mli,"
(**
Summary: \[ [ embed_numeral c nr ] \] constructs the numeral described by [nr].
- {b See also}: {!numeral_refine}
*)
val embed_numeral: context -> numeral_refined -> ast
");

69
src/api/ml/mlx_mk_sort.idl
View file

@ -1,69 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mlmli,"
(**
A datatype constructor descriptor.
*)
type datatype_constructor_desc = {
constructor_desc : symbol; (** name of the constructor function *)
recognizer_desc : symbol; (** name of the recognizer function *)
accessor_descs : (symbol * sort) array; (** names and sorts of the fields *)
}
(**
A datatype is described by a name and constructor descriptors.
*)
type datatype_desc = symbol * datatype_constructor_desc array
(**
A datatype constructor representation.
*)
type datatype_constructor = {
constructor : func_decl; (** constructor function *)
recognizer : func_decl; (** recognizer function *)
accessors : func_decl array; (** field accessor functions *)
}
(**
A datatype is represented by a sort and constructors.
*)
type datatype = sort * datatype_constructor array
(**
Refined view of a {!sort}.
- {b See also}: {!mk_sort}
- {b See also}: {!sort_refine}
*)
type sort_refined =
| Sort_uninterpreted of symbol
| Sort_bool
| Sort_int
| Sort_bv of int
| Sort_finite_domain of symbol * int64
| Sort_real
| Sort_array of sort * sort
| Sort_datatype of datatype_constructor array
| Sort_relation of sort array
| Sort_unknown
");
quote(mli,"
(**
Summary: \[ [ mk_sort c sr ] \] constructs the sort described by [sr].
- {b Precondition}: [sr] is not of form [Sort_relation] or [Sort_unknown], which cannot be directly constructed
- {b See also}: {!mk_datatypes}
- {b See also}: {!sort_refine}
*)
val mk_sort: context -> sort_refined -> sort
(**
\[ [mk_datatypes ctx sorts_to_descriptors] \] creates mutually recursive datatypes described by
[sorts_to_descriptors], which is a function from the sorts of the datatypes to be created to
descriptors of the datatypes' constructors.
- {b See also}: {!Test_mlapi.forest_example}
*)
val mk_datatypes: context -> (sort array -> (datatype_desc array) option) -> datatype array
");

22
src/api/ml/mlx_mk_symbol.idl
View file

@ -1,22 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mlmli,"
(**
Refined view of a {!symbol}.
- {b See also}: {!mk_symbol}
- {b See also}: {!symbol_refine}
*)
type symbol_refined =
| Symbol_int of int
| Symbol_string of string
");
quote(mli,"
(**
Summary: \[ [ mk_symbol c sr ] \] constructs the symbol described by [sr].
- {b See also}: {!symbol_refine}
*)
val mk_symbol: context -> symbol_refined -> symbol
");

19
src/api/ml/mlx_model.idl
View file

@ -1,19 +0,0 @@
quote(mlmli,"
(**
A model assigns uninterpreted sorts to finite universes of distinct values, constants to values,
and arrays and functions to finite maps from argument values to result values plus a default
value for all other arguments.
*)
type model_refined = {
sorts : (sort, ast_vector) Hashtbl.t;
consts : (func_decl, ast) Hashtbl.t;
arrays : (func_decl, (ast, ast) Hashtbl.t * ast) Hashtbl.t;
funcs : (func_decl, (ast array, ast) Hashtbl.t * ast) Hashtbl.t;
}
");
quote(mli,"
(**
Summary: [model_refine c m] is the refined model of [m].
*)
val model_refine : context -> model -> model_refined
");

10
src/api/ml/mlx_numeral_refine.idl
View file

@ -1,10 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mli,"
(**
Summary: \[ [ numeral_refine c a ] \] is the refined view of [a].
- {b Precondition}: [get_ast_kind c a = NUMERAL_AST]
*)
val numeral_refine : context -> ast -> numeral_refined
");

40
src/api/ml/mlx_parse_smtlib.idl
View file

@ -1,40 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mli,"
(**
Summary: \[ [ parse_smtlib_string_x c str sort_names sorts decl_names decls ] \]
Parse the given string using the SMT-LIB parser.
The symbol table of the parser can be initialized using the given sorts and declarations.
The symbols in the arrays [sort_names] and [decl_names] don't need to match the names
of the sorts and declarations in the arrays [sorts] and [decls]. This is an useful feature
since we can use arbitrary names to reference sorts and declarations defined using the API.
- {b See also}: {!parse_smtlib_file_x}
*)
val parse_smtlib_string_x: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> (ast array * ast array * func_decl array)
(**
Summary: Similar to {!parse_smtlib_string_x}, but reads the benchmark from a file.
- {b See also}: {!parse_smtlib_string_x}
*)
val parse_smtlib_file_x: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> (ast array * ast array * func_decl array)
(**
Summary: \[ [ parse_smtlib_string_formula c ... ] \] calls [(parse_smtlib_string c ...)] and returns the single formula produced.
- {b See also}: {!parse_smtlib_file_formula}
- {b See also}: {!parse_smtlib_string_x}
*)
val parse_smtlib_string_formula: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast
(**
Summary: \[ [ parse_smtlib_file_formula c ... ] \] calls [(parse_smtlib_file c ...)] and returns the single formula produced.
- {b See also}: {!parse_smtlib_string_formula}
- {b See also}: {!parse_smtlib_file_x}
*)
val parse_smtlib_file_formula: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast
");

8
src/api/ml/mlx_sort_refine.idl
View file

@ -1,8 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mli,"
(**
Summary: \[ [ sort_refine c s ] \] is the refined view of [s].
*)
val sort_refine: context -> sort -> sort_refined
");

10
src/api/ml/mlx_statistics.idl
View file

@ -1,10 +0,0 @@
quote(mlmli,"
type stat_datum = Stat_int of int | Stat_float of float
type stats_refined = (string, stat_datum) Hashtbl.t
");
quote(mli,"
(**
Summary: [stats_refine c s] is the refined stats of [s].
*)
val stats_refine : context -> stats -> stats_refined
");

8
src/api/ml/mlx_symbol_refine.idl
View file

@ -1,8 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mli,"
(**
Summary: \[ [ symbol_refine c s ] \] is the refined view of [s].
*)
val symbol_refine: context -> symbol -> symbol_refined
");

37
src/api/ml/mlx_term_refine.idl
View file

@ -1,37 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote(mlmli,"
(**
Summary: \[ [ binder_type ] \] is a universal or existential quantifier.
- {b See also}: {!term_refined}
*)
type binder_type = Forall | Exists
(**
Summary: \[ [ term_refined ] \] is the refinement of a {!ast} .
- {b See also}: {!term_refine}
*)
type term_refined =
| Term_numeral of numeral_refined
| Term_app of decl_kind * func_decl * ast array
| Term_quantifier of binder_type * int * ast array array * (symbol * sort) array * ast
| Term_var of int * sort
");
quote(mli,"
(**
Summary: \[ [ mk_term c tr ] \] constructs the term described by [tr].
- {b Precondition}: [tr] is not of form
- {b See also}: {!term_refine}
*)
(* val mk_term: context -> term_refined -> ast *)
(**
Summary: \[ [ term_refine c a ] \] is the refined view of [a].
*)
val term_refine : context -> ast -> term_refined
");

8
src/api/ml/postprocess.sed
View file

@ -1,8 +0,0 @@
# remove 'z3_' and 'Z3_' prefixes on names
s/{\!Z3\./{\!/g
s/\([^_]\)[zZ]3_/\1/g
# remove cyclic definitions introduced by substituting type equations
s/^and \([a-z][a-zA-Z_ ]*\) = \1$//g

82
src/api/ml/preprocess.sed
View file

@ -1,82 +0,0 @@
# attempt to clean up the mess with 'unsigned'
s/ unsigned/ unsigned int/g
s/unsigned int long/unsigned long/g
s/unsigned int __/unsigned __/g
# '@name ' -> 'Section: '
# '\sa ' -> 'See also: '
# '\brief ' -> 'Summary: '
# '\remark ' -> 'Remark: '
# '\pre ' -> 'Precondition: '
# '\param ' -> '@param'
# '\warning ' -> 'Warning: '
# '\code' -> 'C Example:'
# '\endcode' -> ''
/\\pre/s/(/ /g;/\\pre/s/,//g;/\\pre/s/)//g;s/\\pre /- {b Precondition}: /g
/\\ccode/s/(/ /g;/\\ccode/s/\\,//g;/\\ccode/s/)//g;s/\\ccode{\(.*\)}/\[\1\]/g
s/\\defgroup .*//g
s/@name \(.*\)/{2 {L \1}}/g
s/\\sa \(.*\)/- {b See also}: {!Z3.\1}/g
s/\\see \(.*\)/- {b See}: {!Z3.\1}/g
s/<tt>/{e /g
s|</tt>| }|g
s/\\nicebox{/{e/g
s/\\brief /Summary: /g
s/\\remark /- {b Remarks}: /g
s/\\pre /- {b Precondition}: /g
s/\\param /@param /g
s/\\conly .*//g
s/\\warning /- {b Warning}: /g
s/\\code/{v /g
s/\\endcode/ v}/g
s/\\verbatim/{v /g
s/\\endverbatim/ v}/g
s/\\mlonly//g
s/\\endmlonly//g
s/\\mlh/\\\[ \[/g
s/\\endmlh/\] \\\]/g
s/\\deprecated/@deprecated/g
s/\\ / /g
# '\c code ' -> '[code]'
s/\\c \([^ .,:]*\)/[\1]/g
# '#Z3_' -> 'Z3.'
s/#Z3_\([^ \.,) ]*\)/{!Z3.\1}/g
# '/*@}*/' -> ''
s/\/\*@{\*\///g
# '/*@{*/' -> ''
s/\/\*@}\*\///g
# '/*...*/' -> ''
s/\/\*.*\*\///g
s|(\*\*/\*\*)|(\*\*%\*\*)|g
# '/**' -> 'quote(mli,"(**'
s|/\*\*|quote(mli,\"(**|g
# '...*/' -> '*)");'
s|[ ]*\*/|*)\");|g
s|(\*\*%\*\*)|(\*\*/\*\*)|g
# 'extern "C"' -> 'extern ~~C~~'
# 'quote(foo,"bar")' -> quote(foo,~~bar~~)
# mltype("foo") -> mltype(~~foo~~)
s/extern \"C\"/extern ~~C~~/g
s/quote(\(.*\),\"\(.*\)\")/quote(\1,~~\2~~)/g
s/quote(\(.*\),\"/quote(\1,~~/g
s/\")\;/~~);/g
s/\;\"/;~~/g
s/mltype(\"\(.*\)\")/mltype(~~\1~~)/g
# '"' -> '\"'
s/\\\"/\"/g
s/\"/\\\"/g
# '~~' -> '"'
s/~~/\"/g

112
src/api/ml/queen.ml
View file

@ -1,112 +0,0 @@
(*
queen.exe - JakobL@2007-09-22
Demonstration of how Z3 can be used to find solutions to the
N-Queens problem.
See: http://en.wikipedia.org/wiki/Eight_queens_puzzle
Problem specification: Is the following constraint system satisfiable,
for increasing n>=1, what are the models?
constant
n: 8;
variable
row: array n of [0..n-1];
rule
forall i in [0..n-2]:
(forall j in [i+1..n-1]:
((row[i] <> row[j]) and
(i+row[i]) <> (j+row[j]) and
(i+row[j]) <> (j+row[i])));
The answer is yes for n different from 2 and 3. The number of solutions are:
* n=1: 1
* n=2: 0
* n=3: 0
* n=4: 2
* n=5: 10
* n=6: 4
* n=7: 40
* n=8: 92
* n=9: 352
* n=10: 724
...
*)
module Z3 = Z3.V3
(* Auxillary functions *)
let ( |> ) x f = f x;;
let printf = Printf.printf;;
let mk_var ctx name ty = Z3.mk_const ctx (Z3.mk_int_symbol ctx name) ty;;
let mk_int_var ctx name = Z3.mk_int_sort ctx |> mk_var ctx name;;
let mk_int ctx v = Z3.mk_int ctx v (Z3.mk_int_sort ctx);;
let checkreturn v = match v with | (true,r) -> r | _ -> failwith "checkreturn";;
let get_numeral_value_int a1 a2 = Z3.get_numeral_int a1 a2 |> checkreturn;;
let iterate_x lower upper f = for i = lower to upper do f i done;;
let forall_x ctx lower upper f = Z3.mk_and ctx (Array.init (1+upper-lower) (fun i->f (i+lower)))
let exist_x ctx lower upper f = Z3.mk_or ctx (Array.init (1+upper-lower) (fun i->f (i+lower)))
let get_value ctx model f = let (ok, v) = Z3.eval_func_decl ctx model f in (assert ok; v)
let queen_n n =
let ctx = Z3.mk_context_x
[|("MODEL","true");
("RELEVANCY","0")|] in
let ( &&& ) x y = Z3.mk_and ctx [|x;y|] in
let ( <~> ) x y = Z3.mk_not ctx (Z3.mk_eq ctx x y) in
let ( <<= ) x y = Z3.mk_le ctx x y in
let ( +++ ) x y = Z3.mk_add ctx [|x;y|] in
let row = Array.init n (fun i->mk_int_var ctx i) in
let c x = mk_int ctx x in (* make constant *)
let v x = row.(x) in (* make variable *)
let constraint_domain=forall_x ctx (0) (n-1) (fun x-> ((c 0) <<= (v x)) &&& ((v x) <<= (c (n-1)))) in
let constraint_queen=
forall_x ctx (0) (n-2) (fun i->
forall_x ctx (i+1) (n-1) (fun j->
((v i) <~> (v j)) &&&
(((c i)+++(v i)) <~> ((c j)+++(v j))) &&&
(((c i)+++(v j)) <~> ((c j)+++(v i)))
)
) in
let res = constraint_domain &&& constraint_queen in
Z3.assert_cnstr ctx res;
let rec f i =
(match Z3.check_and_get_model ctx with
| (Z3.L_FALSE,_) ->
printf "queen %d, total models: %d\n" n i;
flush stdout;
| (Z3.L_UNDEF,_) -> failwith "Z3.L_UNDEF"
| (Z3.L_TRUE,model) ->
begin
let model_constants=Z3.get_model_constants ctx model in
let vars=Array.map (fun mc->Z3.mk_app ctx mc [||]) model_constants in
let vals=Array.map (fun mc->get_value ctx model mc |> get_numeral_value_int ctx) model_constants in
Z3.del_model ctx model;
let line = String.make n '-' in
let q_line i = let r = String.make n ' ' in String.set r i 'Q'; r in
printf "queen %d, model #%d:\n" n (i+1);
printf "\n";
printf " /%s\\\n" line;
iterate_x 0 (n-1) (fun x->printf " |%s|\n" (q_line (vals.(x))));
printf " \\%s/\n" line;
printf "\n";
flush stdout;
let negated_model = exist_x ctx 0 (n-1) (fun x->(vars.(x)) <~> (c (vals.(x)))) in
Z3.assert_cnstr ctx negated_model;
f (i+1);
end
) in
f 0;
Z3.del_context ctx;
();;
let queen() =
for n = 1 to 8 do
queen_n n
done;;
let _ = queen();;

0
src/api/ml/queen.regress.err
View file

1852
src/api/ml/queen.regress.out
View file

File diff suppressed because it is too large Load diff

3
src/api/ml/reverse.sed
View file

@ -1,3 +0,0 @@
# output lines of input in reverse order
1!G;h;$!d

5
src/api/ml/test_capi.regress.err
View file

@ -1,5 +0,0 @@
WARNING: invalid function application, sort mismatch on argument at position 1
WARNING: (define iff Bool Bool Bool) applied to:
x of sort Int
y of sort Bool

386
src/api/ml/test_capi.regress.out
View file

@ -1,386 +0,0 @@
Z3 4.2.0.0
simple_example
CONTEXT:
(solver)END OF CONTEXT
DeMorgan
DeMorgan is valid
find_model_example1
model for: x xor y
sat
y -> false
x -> true
find_model_example2
model for: x < y + 1, x > 2
sat
y -> 3
x -> 3
model for: x < y + 1, x > 2, not(x = y)
sat
y -> 4
x -> 3
prove_example1
prove: x = y implies g(x) = g(y)
valid
disprove: x = y implies g(g(x)) = g(y)
invalid
counterexample:
y -> U!val!0
x -> U!val!0
g -> {
U!val!0 -> U!val!1
U!val!1 -> U!val!2
else -> U!val!1
}
prove_example2
prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0
valid
disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1
invalid
counterexample:
z -> (- 1)
y -> (- 7719)
x -> (- 7719)
g -> {
(- 7719) -> 0
0 -> 2
(- 1) -> 3
else -> 0
}
push_pop_example1
assert: x >= 'big number'
push
number of scopes: 1
assert: x <= 3
unsat
pop
number of scopes: 0
sat
x = 1000000000000000000000000000000000000000000000000000000:int
function interpretations:
assert: y > x
sat
y = 1000000000000000000000000000000000000000000000000000001:int
x = 1000000000000000000000000000000000000000000000000000000:int
function interpretations:
quantifier_example1
pattern: {(f #0 #1)}
assert axiom:
(forall (k!0 Int) (k!1 Int) (= (inv!0 (f k!1 k!0)) k!0) :pat {(f k!1 k!0)})
prove: f(x, y) = f(w, v) implies y = v
valid
disprove: f(x, y) = f(w, v) implies x = w
that is: not(f(x, y) = f(w, v) implies x = w) is satisfiable
unknown
potential model:
w = 2:int
v = 1:int
y = 1:int
x = 0:int
function interpretations:
f = {(else|->(define f!52 Int Int Int)[(define k!50 Int Int)[#unknown], (define k!51 Int Int)[#unknown]])}
#51 = {(2:int|->2:int), (1:int|->1:int), (15:int|->15:int), (11:int|->11:int), (0:int|->0:int), (19:int|->19:int), (else|->2:int)}
f!52 = {(0:int, 1:int|->3:int), (2:int, 1:int|->3:int), (0:int, 0:int|->4:int), (2:int, 0:int|->5:int), (6:int, 2:int|->7:int), (2:int, 2:int|->8:int), (0:int, 2:int|->9:int), (6:int, 0:int|->10:int), (0:int, 11:int|->12:int), (2:int, 11:int|->13:int), (6:int, 11:int|->14:int), (0:int, 15:int|->16:int), (2:int, 15:int|->17:int), (6:int, 15:int|->18:int), (0:int, 19:int|->20:int), (6:int, 19:int|->21:int), (2:int, 19:int|->22:int), (else|->3:int)}
inv!0 = {(3:int|->1:int), (4:int|->0:int), (5:int|->0:int), (7:int|->2:int), (8:int|->2:int), (9:int|->2:int), (10:int|->0:int), (12:int|->11:int), (13:int|->11:int), (14:int|->11:int), (16:int|->15:int), (17:int|->15:int), (18:int|->15:int), (20:int|->19:int), (21:int|->19:int), (22:int|->19:int), (else|->2:int)}
#50 = {(2:int|->2:int), (6:int|->6:int), (0:int|->0:int), (else|->2:int)}
reason for last failure: 7 (7 = quantifiers)
array_example1
prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))
(=> (= (store a1 i1 v1) (store a2 i2 v2))
(or (= i1 i3) (= i2 i3) (= (select a1 i3) (select a2 i3))))
valid
array_example2
n = 2
(distinct k!0 k!1)
sat
#0 = (define as-array[k!0] (Array Bool Bool))
#1 = (define as-array[k!1] (Array Bool Bool))
function interpretations:
#0 = {((define false Bool)|->(define true Bool)), (else|->(define true Bool))}
#1 = {((define false Bool)|->(define false Bool)), (else|->(define false Bool))}
n = 3
(distinct k!0 k!1 k!2)
sat
#0 = (define as-array[k!0] (Array Bool Bool))
#1 = (define as-array[k!1] (Array Bool Bool))
#2 = (define as-array[k!2] (Array Bool Bool))
function interpretations:
#0 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define false Bool)), (else|->(define true Bool))}
#1 = {((define false Bool)|->(define true Bool)), (else|->(define true Bool))}
#2 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define false Bool)), (else|->(define false Bool))}
n = 4
(distinct k!0 k!1 k!2 k!3)
sat
#0 = (define as-array[k!0] (Array Bool Bool))
#1 = (define as-array[k!1] (Array Bool Bool))
#2 = (define as-array[k!2] (Array Bool Bool))
#3 = (define as-array[k!3] (Array Bool Bool))
function interpretations:
#0 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define true Bool)), (else|->(define false Bool))}
#1 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define false Bool)), (else|->(define true Bool))}
#2 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define true Bool)), (else|->(define true Bool))}
#3 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define false Bool)), (else|->(define false Bool))}
n = 5
(distinct k!0 k!1 k!2 k!3 k!4)
unsat
array_example3
domain: int
range: bool
tuple_example1
tuple_sort: (real, real)
prove: get_x(mk_pair(x, y)) = 1 implies x = 1
valid
disprove: get_x(mk_pair(x, y)) = 1 implies y = 1
invalid
counterexample:
y -> 0
x -> 1
prove: get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2
valid
disprove: get_x(p1) = get_x(p2) implies p1 = p2
invalid
counterexample:
p1 -> (mk_pair 1 0)
p2 -> (mk_pair 1 2)
prove: p2 = update(p1, 0, 10) implies get_x(p2) = 10
valid
disprove: p2 = update(p1, 0, 10) implies get_y(p2) = 10
invalid
counterexample:
p2 -> (mk_pair 10 1)
p1 -> (mk_pair 0 1)
bitvector_example1
disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers
invalid
counterexample:
x -> bv2147483656[32]
bitvector_example2
find values of x and y, such that x ^ y - 103 == x * y
sat
y -> bv3905735879[32]
x -> bv3787456528[32]
eval_example1
MODEL:
y -> 4
x -> 3
evaluating x+y
result = 7:int
two_contexts_example1
k!0
error_code_example1
last call succeeded.
last call failed.
error_code_example2
before Z3_mk_iff
Z3 error: type error.
parser_example1
formula 0: (> x y)
formula 1: (> x 0)
sat
y -> 0
x -> 1
parser_example2
formula: (> x y)
sat
y -> (- 1)
x -> 0
parser_example3
assert axiom:
(forall (x Int) (y Int) (= (g x y) (g y x)) :qid {k!1})
formula: (forall (x Int) (y Int) (=> (= x y) (= (g x 0) (g 0 y))) :qid {k!1})
valid
parser_example4
declaration 0: (define y Int)
declaration 1: (define sk_hack Bool Bool)
declaration 2: (define x Int)
assumption 0: (= x 20)
formula 0: (> x y)
formula 1: (> x 0)
parser_example5
Z3 error: parser error.
Error message: 'ERROR: line 1 column 41: could not find sort symbol 'y'.
'.
numeral_example
Numerals n1:1/2 n2:1/2
valid
Numerals n1:(- 1/3) n2:(- 33333333333333333333333333333333333333333333333333/100000000000000000000000000000000000000000000000000)
valid
ite_example
term: (if false 1 0)
list_example
valid
valid
valid
valid
valid
valid
valid
Formula (=> (is_cons u) (= u (cons (head u) (tail u))))
valid
invalid
counterexample:
u -> nil
tree_example
valid
valid
valid
valid
valid
Formula (=> (is_cons u) (= u (cons (car u) (cdr u))))
valid
invalid
counterexample:
u -> nil
forest_example
valid
valid
valid
valid
valid
valid
binary_tree_example
valid
valid
valid
valid
valid
enum_example
(define apple[fruit:0] fruit)
(define banana[fruit:1] fruit)
(define orange[fruit:2] fruit)
(define is_apple[fruit:0] fruit Bool)
(define is_banana[fruit:1] fruit Bool)
(define is_orange[fruit:2] fruit Bool)
valid
valid
invalid
counterexample:
valid
valid
unsat_core_and_proof_example
unsat
proof: [unit-resolution
[def-axiom (or (or (not PredA) PredB (not PredC)) (not PredB))]
[unit-resolution
[def-axiom (or (or (not PredA) (not PredB) (not PredC)) PredB)]
[unit-resolution
[mp
[asserted (or (and PredA PredB PredC) P1)]
[monotonicity
[rewrite
(iff (and PredA PredB PredC)
(not (or (not PredA) (not PredB) (not PredC))))]
(iff (or (and PredA PredB PredC) P1)
(or (not (or (not PredA) (not PredB) (not PredC))) P1))]
(or (not (or (not PredA) (not PredB) (not PredC))) P1)]
[asserted (not P1)]
(not (or (not PredA) (not PredB) (not PredC)))]
PredB]
[unit-resolution
[mp
[asserted (or (and PredA (not PredB) PredC) P2)]
[monotonicity
[rewrite
(iff (and PredA (not PredB) PredC)
(not (or (not PredA) PredB (not PredC))))]
(iff (or (and PredA (not PredB) PredC) P2)
(or (not (or (not PredA) PredB (not PredC))) P2))]
(or (not (or (not PredA) PredB (not PredC))) P2)]
[asserted (not P2)]
(not (or (not PredA) PredB (not PredC)))]
false]
core:
(not P1)
(not P2)
get_implied_equalities example
Class a |-> 0
Class b |-> 0
Class c |-> 0
Class d |-> 3
Class (f a) |-> 0
Class (f b) |-> 0
Class (f c) |-> 0
asserting f(a) <= b
Class a |-> 0
Class b |-> 0
Class c |-> 0
Class d |-> 3
Class (f a) |-> 0
Class (f b) |-> 0
Class (f c) |-> 0
incremental_example1
unsat core: 0 2 3
unsat
sat
unsat core: 0 2 3
unsat
unsat core: 0 2 3
unsat
sat
reference_counter_example
model for: x xor y
sat
y -> false
x -> true
smt2parser_example
formulas: (and (bvuge a bv16[8]) (bvule a bv240[8]))
substitute_example
substitution result: (f (f a 0) 1)
substitute_vars_example
substitution result: (f (f a (g b)) a)

61
src/api/ml/test_mlapi.cmd
View file

@ -1,61 +0,0 @@
@echo off
SETLOCAL
REM Script to test the Z3 OCaml API
REM
REM Assumes that environment variables are set to provide access to the C and OCaml compilers, as well as the following commands: diff, dos2unix, sed
REM directory containing z3_api.h
set Z3SRC=%1
REM directory containing z3.dll and z3.lib
set Z3BIN=%2
REM directory containing debug z3.dll
set Z3BINDBG=%3
set PATH=.;%2;%3;%PATH%
echo Build test_capi
cl /nologo /I %Z3SRC% %Z3BIN%\z3.lib ..\test_capi\test_capi.c
echo Build test_mlapi
ocamlc -w -a -o test_mlapi.byte.exe z3.cma test_mlapi.ml
ocamlopt -w -a -o test_mlapi.exe z3.cmxa test_mlapi.ml
ocamlc -g -w -a -o test_mlapi.byte.dbg.exe z3_dbg.cma test_mlapi.ml
ocamlopt -g -w -a -o test_mlapi.dbg.exe z3_dbg.cmxa test_mlapi.ml
echo Build test_mlapiV3
ocamlopt -g -w -a -o test_mlapiV3.dbg.exe z3_dbg.cmxa test_mlapiV3.ml
echo Build test_theory
ocamlopt -g -w -a -o test_theory.dbg.exe z3_dbg.cmxa test_theory.ml
echo Build queen
ocamlopt -g -w -a -o queen.exe z3_dbg.cmxa queen.ml
echo Execute test_capi, test_mlapi, test_mlapiV3 and queen
test_capi.exe >test_capi.out 2>test_capi.orig.err
test_mlapi.dbg.exe >test_mlapi.out 2>test_mlapi.orig.err
test_mlapiV3.dbg.exe >test_mlapiV3.out 2>test_mlapiV3.orig.err
queen.exe >queen.out 2>queen.orig.err
REM Strip pointers as they will always differ
sed <test_capi.orig.err >test_capi.err "s/ \[.*\]/ [...]/g"
sed <test_mlapi.orig.err >test_mlapi.err "s/ \[.*\]/ [...]/g"
sed <test_mlapiV3.orig.err >test_mlapiV3.err "s/ \[.*\]/ [...]/g"
sed <queen.orig.err >queen.err "s/ \[.*\]/ [...]/g"
del test_capi.orig.err test_mlapi.orig.err test_mlapiV3.orig.err queen.orig.err
REM Compare with regressions
dos2unix *.out *.err 2>NUL
diff test_capi.regress.out test_capi.out >NUL || echo Regression failed, see: diff test_capi.regress.out test_capi.out
diff test_mlapi.regress.out test_mlapi.out >NUL || echo Regression failed, see: diff test_mlapi.regress.out test_mlapi.out
diff test_mlapiV3.regress.out test_mlapiV3.out >NUL || echo Regression failed, see: diff test_mlapiV3.regress.out test_mlapiV3.out
diff test_capi.regress.err test_capi.err >NUL || echo Regression failed, see: diff test_capi.regress.err test_capi.err
diff test_mlapi.regress.err test_mlapi.err >NUL || echo Regression failed, see: diff test_mlapi.regress.err test_mlapi.err
diff test_mlapiV3.regress.err test_mlapiV3.err >NUL || echo Regression failed, see: diff test_mlapiV3.regress.err test_mlapiV3.err
diff queen.regress.out queen.out >NUL || echo Regression failed, see: diff queen.regress.out queen.out
diff queen.regress.err queen.err >NUL || echo Regression failed, see: diff queen.regress.err queen.err
ENDLOCAL

209
src/api/ml/test_mlapi.ml
View file

@ -1,209 +0,0 @@
(** Examples of using the OCaml API for Z3. *)
(**/**)
(* pause documentation *)
(*
@name Auxiliary Functions
*)
(**
printf
*)
let printf = Printf.printf
;;
(**
fprintf
*)
let fprintf = Printf.fprintf
;;
(**
Exit gracefully in case of error.
*)
let exitf message = fprintf stderr "BUG: %s.\n" message ; exit 1
;;
(**
Create and print datatypes
*)
let mk_datatypes ctx generator =
let datatypes = Z3.mk_datatypes ctx generator in
printf "datatype created:\n%!" ;
Array.iter (fun (sort, ctors) ->
printf "sort: %s\n%!" (Z3.sort_to_string ctx sort) ;
Array.iter (fun {Z3.constructor; recognizer; accessors} ->
printf "constructor: %s%! recognizer: %s%! accessors:"
(Z3.func_decl_to_string ctx constructor)
(Z3.func_decl_to_string ctx recognizer) ;
Array.iter (fun accessor ->
printf " %s%!" (Z3.func_decl_to_string ctx accessor)
) accessors ;
printf "\n"
) ctors
) datatypes ;
printf "\n" ;
datatypes
;;
(**
Create a variable using the given name and type.
*)
let mk_var ctx name ty = Z3.mk_const ctx (Z3.mk_string_symbol ctx name) ty
;;
(* resume documentation *)
(**/**)
(**
Prove that the constraints already asserted into the logical
context implies the given formula. The result of the proof is
displayed.
Z3 is a satisfiability checker. So, one can prove {e f } by showing
that {e (not f) } is unsatisfiable.
The context {e ctx } is not modified by this function.
*)
let prove ctx slv f is_valid =
(* save the current state of the context *)
Z3.solver_push ctx slv ;
let not_f = Z3.mk_not ctx f in
Z3.solver_assert ctx slv not_f ;
(match Z3.solver_check ctx slv with
| Z3.L_FALSE ->
(* proved *)
printf "valid\n" ;
if not is_valid then exitf "unexpected result"
| Z3.L_UNDEF ->
(* Z3 failed to prove/disprove f. *)
printf "unknown\n" ;
let m = Z3.solver_get_model ctx slv in
(* m should be viewed as a potential counterexample. *)
printf "potential counterexample:\n%s\n" (Z3.model_to_string ctx m) ;
if is_valid then exitf "unexpected result"
| Z3.L_TRUE ->
(* disproved *)
printf "invalid\n" ;
let m = Z3.solver_get_model ctx slv in
(* the model returned by Z3 is a counterexample *)
printf "counterexample:\n%s\n" (Z3.model_to_string ctx m) ;
if is_valid then exitf "unexpected result"
);
(* restore context *)
Z3.solver_pop ctx slv 1
;;
(* n-ary trees and forests in OCaml *)
type tree = Leaf of int | Node of forest
and forest = tree list
(**
Demonstrates the usage of {!Z3.mk_datatypes} with an example of forests of trees.
*)
let forest_example () =
let ctx = Z3.mk_context [] in
let slv = Z3.mk_solver ctx
in
let int_sort = Z3.mk_int_sort ctx in
let sym name = Z3.mk_string_symbol ctx name
in
(* n-ary trees and forests in Z3 *)
match
mk_datatypes ctx
(function [|tree; forest|] -> Some
[|(sym"tree",
[|{Z3.constructor_desc= sym"leaf"; recognizer_desc= sym"is_leaf"; accessor_descs= [|(sym"data", int_sort)|]};
{Z3.constructor_desc= sym"node"; recognizer_desc= sym"is_node"; accessor_descs= [|(sym"children", forest)|]}|]);
(sym"forest",
[|{Z3.constructor_desc= sym"nil" ; recognizer_desc= sym"is_nil" ; accessor_descs= [||]};
{Z3.constructor_desc= sym"cons"; recognizer_desc= sym"is_cons"; accessor_descs= [|(sym"hd", tree); (sym"tl", forest)|]}|])|]
| _ -> None
)
with
[|(tree,
[|{Z3.constructor= leaf; recognizer= is_leaf; accessors= [|data|]};
{Z3.constructor= node; recognizer= is_node; accessors= [|children|]}|]);
(forest,
[|{Z3.constructor= nil ; recognizer= is_nil ; accessors= [||]};
{Z3.constructor= cons; recognizer= is_cons; accessors= [|hd; tl|]}|])|]
->
(* translate from OCaml to Z3 *)
let rec ml2z3_tree = function
| Leaf(i) -> Z3.mk_app ctx leaf [|Z3.mk_int ctx i (Z3.mk_int_sort ctx)|]
| Node(f) -> Z3.mk_app ctx node [|ml2z3_forest f|]
and ml2z3_forest = function
| [] -> Z3.mk_app ctx nil [||]
| t :: f -> Z3.mk_app ctx cons [|ml2z3_tree t; ml2z3_forest f|]
in
(* construct some OCaml trees *)
let t0 = Leaf 0 in
let t12 = Node [Leaf 1; Leaf 2] in
let t123 = Node [t12; Leaf 3] in
let t1212 = Node [t12; t12] in
let t412 = Node [Leaf 4; t12] in
(* construct some Z3 trees using the translation from OCaml *)
let t1 = ml2z3_tree t12 in printf "t1: %s\n%!" (Z3.ast_to_string ctx t1) ;
let t2 = ml2z3_tree t123 in printf "t2: %s\n%!" (Z3.ast_to_string ctx t2) ;
let t3 = ml2z3_tree t1212 in printf "t3: %s\n%!" (Z3.ast_to_string ctx t3) ;
let t4 = ml2z3_tree t412 in printf "t4: %s\n%!" (Z3.ast_to_string ctx t4) ;
let f1 = ml2z3_forest [t0] in printf "f1: %s\n%!" (Z3.ast_to_string ctx f1) ;
let f2 = ml2z3_forest [t12] in printf "f2: %s\n%!" (Z3.ast_to_string ctx f2) ;
let f3 = ml2z3_forest [t12; t0] in printf "f3: %s\n%!" (Z3.ast_to_string ctx f3) ;
(* or using the Z3 API *)
let nil = Z3.mk_app ctx nil [||] in
let cons t f = Z3.mk_app ctx cons [|t; f|] in
let leaf i = Z3.mk_app ctx leaf [|Z3.mk_int ctx i (Z3.mk_int_sort ctx)|] in
let node f = Z3.mk_app ctx node [|f|] in
let t0 = leaf 0 in
let t12 = node (cons (leaf 1) (cons (leaf 2) nil)) in
let t123 = node (cons t12 (cons (leaf 3) nil)) in
let t1212 = node (cons t12 (cons t12 nil)) in
let t412 = node (cons (leaf 4) (cons t12 nil)) in
let t1 = t12 in printf "t1: %s\n%!" (Z3.ast_to_string ctx t1) ;
let t2 = t123 in printf "t2: %s\n%!" (Z3.ast_to_string ctx t2) ;
let t3 = t1212 in printf "t3: %s\n%!" (Z3.ast_to_string ctx t3) ;
let t4 = t412 in printf "t4: %s\n%!" (Z3.ast_to_string ctx t4) ;
let f1 = cons t0 nil in printf "f1: %s\n%!" (Z3.ast_to_string ctx f1) ;
let f2 = cons t12 nil in printf "f2: %s\n%!" (Z3.ast_to_string ctx f2) ;
let f3 = cons t12 f1 in printf "f3: %s\n%!" (Z3.ast_to_string ctx f3) ;
(* nil != cons(nil,nil) *)
prove ctx slv (Z3.mk_not ctx (Z3.mk_eq ctx nil f1)) true ;
prove ctx slv (Z3.mk_not ctx (Z3.mk_eq ctx (leaf 5) t1)) true ;
(* cons(x,u) = cons(x, v) => u = v *)
let u = mk_var ctx "u" forest in
let v = mk_var ctx "v" forest in
let x = mk_var ctx "x" tree in
let y = mk_var ctx "y" tree in
let l1 = cons x u in printf "l1: %s\n%!" (Z3.ast_to_string ctx l1) ;
let l2 = cons y v in printf "l2: %s\n%!" (Z3.ast_to_string ctx l2) ;
prove ctx slv (Z3.mk_implies ctx (Z3.mk_eq ctx l1 l2) (Z3.mk_eq ctx u v)) true ;
prove ctx slv (Z3.mk_implies ctx (Z3.mk_eq ctx l1 l2) (Z3.mk_eq ctx x y)) true ;
(* is_nil(u) or is_cons(u) *)
prove ctx slv (Z3.mk_or ctx [|Z3.mk_app ctx is_nil [|u|]; Z3.mk_app ctx is_cons [|u|]|]) true ;
(* occurs check u != cons(x,u) *)
prove ctx slv (Z3.mk_not ctx (Z3.mk_eq ctx u l1)) true ;
| _ ->
exitf "unexpected datatype signature"
;;
let _ =
ignore( Z3.open_log "test_mlapi.log" );
forest_example () ;
;;

0
src/api/ml/test_mlapi.regress.err
View file

32
src/api/ml/test_mlapi.regress.out
View file

@ -1,32 +0,0 @@
datatype created:
sort: tree
constructor: (define leaf[tree:0] Int tree) recognizer: (define is_leaf[tree:0] tree Bool) accessors: (define data[tree:0:0] tree Int)
constructor: (define node[tree:1] forest tree) recognizer: (define is_node[tree:1] tree Bool) accessors: (define children[tree:1:0] tree forest)
sort: forest
constructor: (define nil[forest:0] forest) recognizer: (define is_nil[forest:0] forest Bool) accessors:
constructor: (define cons[forest:1] tree forest forest) recognizer: (define is_cons[forest:1] forest Bool) accessors: (define hd[forest:1:0] forest tree) (define tl[forest:1:1] forest forest)
t1: (node (cons (leaf 1) (cons (leaf 2) nil)))
t2: (node (cons (node (cons (leaf 1) (cons (leaf 2) nil))) (cons (leaf 3) nil)))
t3: (node (cons (node (cons (leaf 1) (cons (leaf 2) nil)))
(cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil)))
t4: (node (cons (leaf 4) (cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil)))
f1: (cons (leaf 0) nil)
f2: (cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil)
f3: (cons (node (cons (leaf 1) (cons (leaf 2) nil))) (cons (leaf 0) nil))
t1: (node (cons (leaf 1) (cons (leaf 2) nil)))
t2: (node (cons (node (cons (leaf 1) (cons (leaf 2) nil))) (cons (leaf 3) nil)))
t3: (node (cons (node (cons (leaf 1) (cons (leaf 2) nil)))
(cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil)))
t4: (node (cons (leaf 4) (cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil)))
f1: (cons (leaf 0) nil)
f2: (cons (node (cons (leaf 1) (cons (leaf 2) nil))) nil)
f3: (cons (node (cons (leaf 1) (cons (leaf 2) nil))) (cons (leaf 0) nil))
valid
valid
l1: (cons x u)
l2: (cons y v)
valid
valid
valid
valid

1418
src/api/ml/test_mlapiV3.ml
View file

File diff suppressed because it is too large Load diff

5
src/api/ml/test_mlapiV3.regress.err
View file

@ -1,5 +0,0 @@
WARNING: invalid function application, sort mismatch on argument at position 1
WARNING: (define iff Bool Bool Bool) applied to:
x of sort Int
y of sort Bool

315
src/api/ml/test_mlapiV3.regress.out
View file

@ -1,315 +0,0 @@
Z3 4.2.0.0
simple_example
CONTEXT:
(solver)END OF CONTEXT
DeMorgan
DeMorgan is valid
find_model_example1
model for: x xor y
sat
y -> false
x -> true
find_model_example2
model for: x < y + 1, x > 2
sat
y -> 3
x -> 3
model for: x < y + 1, x > 2, not(x = y)
sat
y -> 4
x -> 3
prove_example1
prove: x = y implies g(x) = g(y)
valid
disprove: x = y implies g(g(x)) = g(y)
invalid
counterexample:
y -> U!val!0
x -> U!val!0
g -> {
U!val!0 -> U!val!1
U!val!1 -> U!val!2
else -> U!val!1
}
prove_example2
prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0
valid
disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1
invalid
counterexample:
z -> (- 1)
y -> (- 7719)
x -> (- 7719)
g -> {
(- 7719) -> 0
0 -> 2
(- 1) -> 3
else -> 0
}
push_pop_example1
assert: x >= 'big number'
push
number of scopes: 1
assert: x <= 3
unsat
pop
number of scopes: 0
sat
x = 1000000000000000000000000000000000000000000000000000000:int
function interpretations:
assert: y > x
sat
y = 1000000000000000000000000000000000000000000000000000001:int
x = 1000000000000000000000000000000000000000000000000000000:int
function interpretations:
quantifier_example1
pattern: {(f #0 #1)}
assert axiom:
(forall (k!0 Int) (k!1 Int) (= (inv!0 (f k!1 k!0)) k!0) :pat {(f k!1 k!0)})
prove: f(x, y) = f(w, v) implies y = v
valid
disprove: f(x, y) = f(w, v) implies x = w
that is: not(f(x, y) = f(w, v) implies x = w) is satisfiable
unknown
potential model:
w = 2:int
v = 1:int
y = 1:int
x = 0:int
function interpretations:
f = {(else|->(define f!52 Int Int Int)[(define k!50 Int Int)[#unknown], (define k!51 Int Int)[#unknown]])}
#51 = {(2:int|->2:int), (1:int|->1:int), (15:int|->15:int), (11:int|->11:int), (0:int|->0:int), (19:int|->19:int), (else|->2:int)}
f!52 = {(0:int, 1:int|->3:int), (2:int, 1:int|->3:int), (0:int, 0:int|->4:int), (2:int, 0:int|->5:int), (6:int, 2:int|->7:int), (2:int, 2:int|->8:int), (0:int, 2:int|->9:int), (6:int, 0:int|->10:int), (0:int, 11:int|->12:int), (2:int, 11:int|->13:int), (6:int, 11:int|->14:int), (0:int, 15:int|->16:int), (2:int, 15:int|->17:int), (6:int, 15:int|->18:int), (0:int, 19:int|->20:int), (6:int, 19:int|->21:int), (2:int, 19:int|->22:int), (else|->3:int)}
inv!0 = {(3:int|->1:int), (4:int|->0:int), (5:int|->0:int), (7:int|->2:int), (8:int|->2:int), (9:int|->2:int), (10:int|->0:int), (12:int|->11:int), (13:int|->11:int), (14:int|->11:int), (16:int|->15:int), (17:int|->15:int), (18:int|->15:int), (20:int|->19:int), (21:int|->19:int), (22:int|->19:int), (else|->2:int)}
#50 = {(2:int|->2:int), (6:int|->6:int), (0:int|->0:int), (else|->2:int)}
reason for last failure: 7 (7 = quantifiers)
array_example1
prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))
(=> (= (store a1 i1 v1) (store a2 i2 v2))
(or (= i1 i3) (= i2 i3) (= (select a1 i3) (select a2 i3))))
valid
array_example2
n = 2
(distinct k!0 k!1)
sat
#0 = (define as-array[k!0] (Array Bool Bool))
#1 = (define as-array[k!1] (Array Bool Bool))
function interpretations:
#0 = {((define false Bool)|->(define true Bool)), (else|->(define true Bool))}
#1 = {((define false Bool)|->(define false Bool)), (else|->(define false Bool))}
n = 3
(distinct k!0 k!1 k!2)
sat
#0 = (define as-array[k!0] (Array Bool Bool))
#1 = (define as-array[k!1] (Array Bool Bool))
#2 = (define as-array[k!2] (Array Bool Bool))
function interpretations:
#0 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define false Bool)), (else|->(define true Bool))}
#1 = {((define false Bool)|->(define true Bool)), (else|->(define true Bool))}
#2 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define false Bool)), (else|->(define false Bool))}
n = 4
(distinct k!0 k!1 k!2 k!3)
sat
#0 = (define as-array[k!0] (Array Bool Bool))
#1 = (define as-array[k!1] (Array Bool Bool))
#2 = (define as-array[k!2] (Array Bool Bool))
#3 = (define as-array[k!3] (Array Bool Bool))
function interpretations:
#0 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define true Bool)), (else|->(define false Bool))}
#1 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define false Bool)), (else|->(define true Bool))}
#2 = {((define true Bool)|->(define true Bool)), ((define false Bool)|->(define true Bool)), (else|->(define true Bool))}
#3 = {((define true Bool)|->(define false Bool)), ((define false Bool)|->(define false Bool)), (else|->(define false Bool))}
n = 5
(distinct k!0 k!1 k!2 k!3 k!4)
unsat
array_example3
domain: int
range: bool
tuple_example1
tuple_sort: (real, real)
prove: get_x(mk_pair(x, y)) = 1 implies x = 1
valid
disprove: get_x(mk_pair(x, y)) = 1 implies y = 1
invalid
counterexample:
y -> 0
x -> 1
prove: get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2
valid
disprove: get_x(p1) = get_x(p2) implies p1 = p2
invalid
counterexample:
p1 -> (mk_pair 1 0)
p2 -> (mk_pair 1 2)
prove: p2 = update(p1, 0, 10) implies get_x(p2) = 10
valid
disprove: p2 = update(p1, 0, 10) implies get_y(p2) = 10
invalid
counterexample:
p2 -> (mk_pair 10 1)
p1 -> (mk_pair 0 1)
bitvector_example1
disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers
invalid
counterexample:
x -> bv2147483656[32]
bitvector_example2
find values of x and y, such that x ^ y - 103 == x * y
sat
y -> bv3905735879[32]
x -> bv3787456528[32]
eval_example1
MODEL:
y -> 4
x -> 3
evaluating x+y
result = 7:int
two_contexts_example1
k!0
error_code_example1
last call succeeded.
last call failed.
error_code_example2
before Z3_mk_iff
Z3 error: type error.
parser_example1
formula 0: (> x y)
formula 1: (> x 0)
sat
y -> 0
x -> 1
parser_example2
formula: (> x y)
sat
y -> (- 1)
x -> 0
parser_example3
assert axiom:
(forall (x Int) (y Int) (= (g x y) (g y x)) :qid {k!1})
formula: (forall (x Int) (y Int) (=> (= x y) (= (g x 0) (g 0 y))) :qid {k!1})
valid
parser_example4
declaration 0: (define y Int)
declaration 1: (define sk_hack Bool Bool)
declaration 2: (define x Int)
assumption 0: (= x 20)
formula 0: (> x y)
formula 1: (> x 0)
parser_example5
Z3 error: parser error.
Error message: 'ERROR: line 1 column 41: could not find sort symbol 'y'.
'.
ite_example
term: (if false 1 0)
enum_example
(define apple[fruit:0] fruit)
(define banana[fruit:1] fruit)
(define orange[fruit:2] fruit)
(define is_apple[fruit:0] fruit Bool)
(define is_banana[fruit:1] fruit Bool)
(define is_orange[fruit:2] fruit Bool)
valid
valid
invalid
counterexample:
valid
valid
unsat_core_and_proof_example
unsat
proof: [unit-resolution
[def-axiom (or (or (not PredA) PredC (not PredB)) (not PredC))]
[unit-resolution
[def-axiom (or (or (not PredA) (not PredB) (not PredC)) PredC)]
[unit-resolution
[mp
[asserted (or (and PredA PredB PredC) P1)]
[monotonicity
[rewrite
(iff (and PredA PredB PredC)
(not (or (not PredA) (not PredB) (not PredC))))]
(iff (or (and PredA PredB PredC) P1)
(or (not (or (not PredA) (not PredB) (not PredC))) P1))]
(or (not (or (not PredA) (not PredB) (not PredC))) P1)]
[asserted (not P1)]
(not (or (not PredA) (not PredB) (not PredC)))]
PredC]
[unit-resolution
[mp
[asserted (or (and PredA (not PredC) PredB) P2)]
[monotonicity
[rewrite
(iff (and PredA (not PredC) PredB)
(not (or (not PredA) PredC (not PredB))))]
(iff (or (and PredA (not PredC) PredB) P2)
(or (not (or (not PredA) PredC (not PredB))) P2))]
(or (not (or (not PredA) PredC (not PredB))) P2)]
[asserted (not P2)]
(not (or (not PredA) PredC (not PredB)))]
false]
core:
(not P2)
(not P1)
abstract_example
formula: (> x y)
abstracted formula: (> #0 y)
get_implied_equalities example
Class a |-> 0
Class b |-> 0
Class c |-> 0
Class d |-> 3
Class (f a) |-> 0
Class (f b) |-> 0
Class (f c) |-> 0
asserting f(a) <= b
Class a |-> 0
Class b |-> 0
Class c |-> 0
Class d |-> 3
Class (f a) |-> 0
Class (f b) |-> 0
Class (f c) |-> 0

42
src/api/ml/test_theory.ml
View file

@ -1,42 +0,0 @@
module Z3 = Z3.V3
let print_lbool lb =
match lb with
| Z3.L_FALSE -> Printf.printf "false\n"
| Z3.L_TRUE -> Printf.printf "true\n"
| Z3.L_UNDEF -> Printf.printf "undef\n"
(* simple sanity test of theory plugin *)
let test_theory() =
let ctx = Z3.mk_context_x [| |] in
let th = Z3.mk_theory ctx "test-theory" in
let _ = Z3.set_push_callback th (fun () -> Printf.printf "push\n") in
let _ = Z3.set_pop_callback th (fun () -> Printf.printf "pop\n") in
let _ = Z3.set_delete_callback th (fun () -> Printf.printf "delete\n") in
let _ = Z3.set_final_check_callback th (fun () -> (Printf.printf "final\n"; true)) in
let _ = Z3.set_delete_callback th (fun () -> Printf.printf "deleted\n") in
let f_sym = Z3.mk_string_symbol ctx "f" in
let a_sym = Z3.mk_string_symbol ctx "a" in
let b_sym = Z3.mk_string_symbol ctx "b" in
let int_sort = Z3.mk_int_sort ctx in
let f = Z3.theory_mk_func_decl ctx th f_sym [|int_sort |] int_sort in
let a = Z3.theory_mk_constant ctx th a_sym int_sort in
let b = Z3.theory_mk_constant ctx th b_sym int_sort in
let reduce_f g args =
Printf.printf "reduce %s\n" (Z3.func_decl_to_string ctx g);
match g, args with
| _, [| a' |] when Z3.is_eq_func_decl ctx g f && Z3.is_eq_ast ctx a' a -> Some b
| _, _ -> None
in
let _ = Z3.set_reduce_app_callback th reduce_f in
(* b != f(b) is consistent *)
let _ = Z3.assert_cnstr ctx (Z3.mk_not ctx (Z3.mk_eq ctx b (Z3.mk_app ctx f [| b |]))) in
let res = Z3.check ctx in
print_lbool res;
(* b != f(a) is not consistent *)
let _ = Z3.assert_cnstr ctx (Z3.mk_not ctx (Z3.mk_eq ctx b (Z3.mk_app ctx f [| a |]))) in
let res = Z3.check ctx in
print_lbool res;
Z3.del_context ctx
let _ = test_theory()

38
src/api/ml/update-ml-doc.cmd
View file

@ -1,38 +0,0 @@
@echo off
SETLOCAL
REM Script to generate Z3 OCaml API documentation
REM
REM Assumes that environment variables are set to provide access to the OCaml compilers, as well as the following commands: sed
rd 2>NUL /s /q doc
md doc
cd doc
set MLDIR=..
set DOCDIR=..\%1
ocamldoc.opt -hide Z3,Z3.V3,Test_mlapi -html -css-style z3_ml.css -I %MLDIR% %MLDIR%\test_mlapi.ml %MLDIR%\z3.mli
sed "s|<pre><span class=\"keyword\">val\(.*\)</pre>|<div class=\"function\"><span class=\"keyword\">val\1</div>|g;s|<pre><span class=\"keyword\">type\(.*\)</pre>|<div class=\"function\"><span class=\"keyword\">type\1</div>|g;s|<code><span class=\"keyword\">type\(.*\) = </code>|<div class=\"function\"><span class=\"keyword\">type\1 = </div>|g" Z3.html > Z3.new.html
move >NUL Z3.new.html Z3.html
sed "s|<pre><span class=\"keyword\">val\(.*\)</pre>|<div class=\"function\"><span class=\"keyword\">val\1</div>|g" Test_mlapi.html > Test_mlapi.new.html
move >NUL Test_mlapi.new.html Test_mlapi.html
sed "s|<h1>Index of values</h1>|<h1>OCaml: Index</h1>|" Index_values.html > Index_values.new.html
move >NUL Index_values.new.html Index_values.html
copy >NUL %DOCDIR%\tabs.css
copy >NUL %DOCDIR%\z3.png
copy >NUL %DOCDIR%\z3_ml.css
sed "1,23d" Test_mlapi.html | sed "$d" > Test_mlapi.new.html
type 2>NUL %DOCDIR%\test_mlapi_header.html Test_mlapi.new.html %DOCDIR%\mldoc_footer.html >Test_mlapi.html
sed "1,37d" Z3.html > Z3.new.html
type 2>NUL %DOCDIR%\z3_mlapi_header.html Z3.new.html >Z3.html
exit /B 0
ENDLOCAL

366
src/api/ml/x3.ml
View file

@ -1,366 +0,0 @@
/* Copyright (c) Microsoft Corporation */
quote (ml,"
(* Internal auxiliary functions: *)
(*
(* Transform a pair of arrays into an array of pairs *)
let array_combine a b =
if Array.length a <> Array.length b then raise (Invalid_argument \"array_combine\");
Array.init (Array.length a) (fun i -> (a.(i), b.(i)))
(* [a |> b] is the pipeline operator for [b(a)] *)
let ( |> ) x f = f x
*)
(* Find the index of an element in an array, raises Not_found is missing *)
let find equal x a =
let len = Array.length a in
let rec find_ i =
if i >= len then
raise Not_found
else
if equal x a.(i) then
i
else
find_ (i+1)
in
find_ 0
(* Symbols *)
let symbol_refine c s =
match get_symbol_kind c s with
| INT_SYMBOL -> Symbol_int (get_symbol_int c s)
| STRING_SYMBOL -> Symbol_string (get_symbol_string c s)
let mk_symbol c = function
| Symbol_int(i) -> mk_int_symbol c i
| Symbol_string(s) -> mk_string_symbol c s
(* Sorts *)
let get_datatype_sort c s =
Array.init (get_datatype_sort_num_constructors c s) (fun i ->
let constructor = get_datatype_sort_constructor c s i in
let recognizer = get_datatype_sort_recognizer c s i in
let accessors =
Array.init (get_domain_size c constructor) (fun j ->
get_datatype_sort_constructor_accessor c s i j
) in
{constructor; recognizer; accessors}
)
let sort_refine c s =
match get_sort_kind c s with
| UNINTERPRETED_SORT -> Sort_uninterpreted (get_sort_name c s)
| BOOL_SORT -> Sort_bool
| INT_SORT -> Sort_int
| BV_SORT -> Sort_bv (get_bv_sort_size c s)
| FINITE_DOMAIN_SORT ->
(match get_finite_domain_sort_size c s with
| Some(sz) -> Sort_finite_domain (get_sort_name c s, sz)
| None -> failwith \"Z3.sort_refine: failed to get size of finite-domain sort\"
)
| REAL_SORT -> Sort_real
| ARRAY_SORT -> Sort_array (get_array_sort_domain c s, get_array_sort_range c s)
| DATATYPE_SORT -> Sort_datatype (get_datatype_sort c s)
| RELATION_SORT -> Sort_relation (Array.init (get_relation_arity c s) (fun i -> get_relation_column c s i))
| UNKNOWN_SORT -> Sort_unknown
let mk_sort c = function
| Sort_uninterpreted(s) -> mk_uninterpreted_sort c s
| Sort_bool -> mk_bool_sort c
| Sort_int -> mk_int_sort c
| Sort_bv(size) -> mk_bv_sort c size
| Sort_finite_domain(name,size) -> mk_finite_domain_sort c name size
| Sort_real -> mk_real_sort c
| Sort_array(domain,range) -> mk_array_sort c domain range
| Sort_datatype(constructors) -> get_range c constructors.(0).constructor
| Sort_relation(_) -> invalid_arg \"Z3.mk_sort: cannot construct relation sorts\"
| Sort_unknown(_) -> invalid_arg \"Z3.mk_sort: cannot construct unknown sorts\"
(* Replacement datatypes creation API *)
let mk_datatypes ctx generator =
let usort0 = mk_uninterpreted_sort ctx (mk_int_symbol ctx 0)
in
let rec find_num_sorts i =
if i = max_int then invalid_arg \"mk_datatypes: too many sorts\"
else
match generator (Array.make i usort0) with
| None -> find_num_sorts (i+1)
| Some(a) when Array.length a = i -> i
| Some _ -> invalid_arg \"mk_datatypes: number of sorts and datatype descriptors must be equal\"
in
let num_sorts = find_num_sorts 0
in
let sorts0 = Array.init num_sorts (fun i -> mk_uninterpreted_sort ctx (mk_int_symbol ctx i))
in
let ctorss_descriptors =
match generator sorts0 with
| Some(ctorss_descriptors) -> ctorss_descriptors
| None -> invalid_arg \"mk_datatypes: generator failed\"
in
let names = Array.map fst ctorss_descriptors
in
let ctorss =
Array.map (fun (_, ctors_descriptor) ->
Array.map (fun {constructor_desc; recognizer_desc; accessor_descs} ->
let field_names = Array.map fst accessor_descs
in
let sort_refs = Array.make (Array.length accessor_descs) 0
in
let field_sorts =
Array.mapi (fun i (_, sort) ->
try
let j = find (fun s t -> is_eq_sort ctx s t) sort sorts0 in
sort_refs.(i) <- j ;
None
with Not_found ->
Some(sort)
) accessor_descs
in
mk_constructor ctx constructor_desc recognizer_desc field_names field_sorts sort_refs
) ctors_descriptor
) ctorss_descriptors
in
let constructor_lists = Array.map (mk_constructor_list ctx) ctorss
in
let sorts,_ = mk_datatypes ctx names constructor_lists
in
let datatypes =
Array.mapi (fun i sort ->
(sort,
Array.mapi (fun j ctor ->
let num_fields = Array.length (snd ctorss_descriptors.(i)).(j).accessor_descs in
let constructor, recognizer, accessors = query_constructor ctx ctor num_fields in
{constructor; recognizer; accessors}
) ctorss.(i))
) sorts
in
Array.iter (fun ctor_list ->
del_constructor_list ctx ctor_list
) constructor_lists
;
Array.iter (fun ctors ->
Array.iter (fun ctor ->
del_constructor ctx ctor
) ctors
) ctorss
;
datatypes
(* Numerals *)
let rec numeral_refine c t =
assert( get_ast_kind c t = NUMERAL_AST );
let sort = get_sort c t in
let is_int, i = get_numeral_int c t in
if is_int then
Numeral_int (i, sort)
else
let is_int64, i = get_numeral_int64 c t in
if is_int64 then
Numeral_int64 (i, sort)
else
if get_sort_kind c sort <> REAL_SORT then
Numeral_large (get_numeral_string c t, sort)
else
let n = numeral_refine c (get_numerator c t) in
let d = numeral_refine c (get_denominator c t) in
Numeral_rational (n, d)
let to_real c x =
if get_sort_kind c (get_sort c x) = REAL_SORT then
x
else
mk_int2real c x
let rec embed_numeral c = function
| Numeral_int (i, s) -> mk_int c i s
| Numeral_int64 (i, s) -> mk_int64 c i s
| Numeral_large (l, s) -> mk_numeral c l s
| Numeral_rational (Numeral_int(n,_), Numeral_int(d,_)) -> mk_real c n d
| Numeral_rational (n, d) ->
mk_div c (to_real c (embed_numeral c n)) (to_real c (embed_numeral c d))
(* Or should the following be used instead?
let n_str = get_numeral_string c (embed_numeral c n) in
let d_str = get_numeral_string c (embed_numeral c d) in
mk_numeral c (n_str ^ \" / \" ^ d_str) (mk_real_sort c)
*)
(* Terms *)
let get_app_args c a =
Array.init (get_app_num_args c a) (get_app_arg c a);;
let get_domains c d =
Array.init (get_domain_size c d) (get_domain c d);;
let get_pattern_terms c p =
Array.init (get_pattern_num_terms c p) (get_pattern c p)
let term_refine c t =
match get_ast_kind c t with
| NUMERAL_AST ->
Term_numeral (numeral_refine c t)
| APP_AST ->
let t' = to_app c t in
let f = get_app_decl c t' in
let num_args = get_app_num_args c t' in
let args = Array.init num_args (get_app_arg c t') in
let k = get_decl_kind c f in
Term_app (k, f, args)
| QUANTIFIER_AST ->
let bt = if is_quantifier_forall c t then Forall else Exists in
let w = get_quantifier_weight c t in
let np = get_quantifier_num_patterns c t in
let pats = Array.init np (get_quantifier_pattern_ast c t) in
let pats = Array.map (get_pattern_terms c) pats in
let nb = get_quantifier_num_bound c t in
let bound =
Array.init nb (fun i ->
(get_quantifier_bound_name c t i, get_quantifier_bound_sort c t i)
) in
let body = get_quantifier_body c t in
Term_quantifier (bt, w, pats, bound, body)
| VAR_AST ->
Term_var (get_index_value c t, get_sort c t)
| _ ->
assert false
(* let mk_term c = function *)
(* | Term_numeral (numeral, sort) -> mk_numeral c numeral sort *)
(* | Term_app (kind, decl, args) -> *)
(* | Term_quantifier (strength, weight, pats, bound, body) -> *)
(* | Term_var (index, sort) -> *)
(* Refined model API *)
let model_refine c m =
let num_sorts = model_get_num_sorts c m in
let sorts = Hashtbl.create num_sorts in
for i = 0 to num_sorts - 1 do
let sort = model_get_sort c m i in
let universe = model_get_sort_universe c m sort in
Hashtbl.add sorts sort universe
done;
let num_consts = model_get_num_consts c m in
let consts = Hashtbl.create num_consts in
let arrays = Hashtbl.create 0 in
for i = 0 to num_consts - 1 do
let const_decl = model_get_const_decl c m i in
match model_get_const_interp c m const_decl with
| Some(const_interp) ->
if is_as_array c const_interp then
let array_decl = get_as_array_func_decl c const_interp in
match model_get_func_interp c m array_decl with
| Some(array_interp) ->
let num_entries = func_interp_get_num_entries c array_interp in
let tbl = Hashtbl.create num_entries in
for i = 0 to num_entries - 1 do
let entry = func_interp_get_entry c array_interp i in
assert( func_entry_get_num_args c entry = 1 );
let arg = func_entry_get_arg c entry 0 in
let value = func_entry_get_value c entry in
Hashtbl.add tbl arg value
done;
let default = func_interp_get_else c array_interp in
Hashtbl.add arrays const_decl (tbl, default)
| None ->
()
else
Hashtbl.add consts const_decl const_interp
| None ->
()
done;
let num_funcs = model_get_num_funcs c m in
let funcs = Hashtbl.create num_funcs in
for i = 0 to num_funcs - 1 do
let func_decl = model_get_func_decl c m i in
if not (Hashtbl.mem arrays func_decl) then
match model_get_func_interp c m func_decl with
| Some(func_interp) ->
let num_entries = func_interp_get_num_entries c func_interp in
let tbl = Hashtbl.create num_entries in
for i = 0 to num_entries - 1 do
let entry = func_interp_get_entry c func_interp i in
let num_args = func_entry_get_num_args c entry in
let args = Array.init num_args (fun i -> func_entry_get_arg c entry i) in
let value = func_entry_get_value c entry in
Hashtbl.add tbl args value
done;
let default = func_interp_get_else c func_interp in
Hashtbl.add funcs func_decl (tbl, default)
| None ->
()
done;
{sorts; consts; arrays; funcs}
(* Extended parser API *)
let get_smtlib_formulas c =
Array.init (get_smtlib_num_formulas c) (get_smtlib_formula c)
let get_smtlib_assumptions c =
Array.init (get_smtlib_num_assumptions c) (get_smtlib_assumption c)
let get_smtlib_decls c =
Array.init (get_smtlib_num_decls c) (get_smtlib_decl c)
let get_smtlib_parse_results c =
(get_smtlib_formulas c, get_smtlib_assumptions c, get_smtlib_decls c)
let parse_smtlib_string_x c a1 a2 a3 a4 a5 =
parse_smtlib_string c a1 a2 a3 a4 a5 ;
get_smtlib_parse_results c
let parse_smtlib_file_x c a1 a2 a3 a4 a5 =
parse_smtlib_file c a1 a2 a3 a4 a5 ;
get_smtlib_parse_results c
let parse_smtlib_string_formula c a1 a2 a3 a4 a5 =
parse_smtlib_string c a1 a2 a3 a4 a5 ;
match get_smtlib_formulas c with [|f|] -> f | _ -> failwith \"Z3: parse_smtlib_string_formula\"
let parse_smtlib_file_formula c a1 a2 a3 a4 a5 =
parse_smtlib_file c a1 a2 a3 a4 a5 ;
match get_smtlib_formulas c with [|f|] -> f | _ -> failwith \"Z3: parse_smtlib_file_formula\"
(* Error handling *)
let get_error_msg c e =
match e with
| PARSER_ERROR -> (get_error_msg_ex c e) ^ \": \" ^ (get_smtlib_error c)
| _ -> get_error_msg_ex c e
(* Refined stats API *)
let stats_refine c s =
let num_stats = stats_size c s in
let tbl = Hashtbl.create num_stats in
for i = 0 to num_stats - 1 do
let key = stats_get_key c s i in
let datum =
if stats_is_uint c s i then
Stat_int(stats_get_uint_value c s i)
else
Stat_float(stats_get_double_value c s i) in
Hashtbl.add tbl key datum
done;
tbl
");

378
src/api/ml/x3V3.ml
View file

@ -1,378 +0,0 @@
quote (ml,"
(* Internal auxillary functions: *)
(* Transform a pair of arrays into an array of pairs *)
let array_combine a b =
if Array.length a <> Array.length b then raise (Invalid_argument \"array_combine\");
Array.init (Array.length a) (fun i->(a.(i),b.(i)));;
(* [a |> b] is the pipeline operator for [b(a)] *)
let ( |> ) x f = f x;;
(* Extensions, except for refinement: *)
let mk_context_x configs =
let config = mk_config() in
let f(param_id,param_value) = set_param_value config param_id param_value in
Array.iter f configs;
let context = mk_context config in
del_config config;
context;;
let get_app_args c a =
Array.init (get_app_num_args c a) (get_app_arg c a);;
let get_domains c d =
Array.init (get_domain_size c d) (get_domain c d);;
let get_array_sort c t = (get_array_sort_domain c t, get_array_sort_range c t);;
let get_tuple_sort c ty =
(get_tuple_sort_mk_decl c ty,
Array.init (get_tuple_sort_num_fields c ty) (get_tuple_sort_field_decl c ty));;
type datatype_constructor_refined = {
constructor : func_decl;
recognizer : func_decl;
accessors : func_decl array
}
let get_datatype_sort c ty =
Array.init (get_datatype_sort_num_constructors c ty)
(fun idx_c ->
let constr = get_datatype_sort_constructor c ty idx_c in
let recog = get_datatype_sort_recognizer c ty idx_c in
let num_acc = get_domain_size c constr in
{ constructor = constr;
recognizer = recog;
accessors = Array.init num_acc (get_datatype_sort_constructor_accessor c ty idx_c);
})
let get_model_constants c m =
Array.init (get_model_num_constants c m) (get_model_constant c m);;
let get_model_func_entry c m i j =
(Array.init
(get_model_func_entry_num_args c m i j)
(get_model_func_entry_arg c m i j),
get_model_func_entry_value c m i j);;
let get_model_func_entries c m i =
Array.init (get_model_func_num_entries c m i) (get_model_func_entry c m i);;
let get_model_funcs c m =
Array.init (get_model_num_funcs c m)
(fun i->(get_model_func_decl c m i |> get_decl_name c,
get_model_func_entries c m i,
get_model_func_else c m i));;
let get_smtlib_formulas c =
Array.init (get_smtlib_num_formulas c) (get_smtlib_formula c);;
let get_smtlib_assumptions c =
Array.init (get_smtlib_num_assumptions c) (get_smtlib_assumption c);;
let get_smtlib_decls c =
Array.init (get_smtlib_num_decls c) (get_smtlib_decl c);;
let get_smtlib_parse_results c =
(get_smtlib_formulas c, get_smtlib_assumptions c, get_smtlib_decls c);;
let parse_smtlib_string_formula c a1 a2 a3 a4 a5 =
(parse_smtlib_string c a1 a2 a3 a4 a5;
match get_smtlib_formulas c with [|f|] -> f | _ -> failwith \"Z3: parse_smtlib_string_formula\");;
let parse_smtlib_file_formula c a1 a2 a3 a4 a5 =
(parse_smtlib_file c a1 a2 a3 a4 a5;
match get_smtlib_formulas c with [|f|] -> f | _ -> failwith \"Z3: parse_smtlib_file_formula\");;
let parse_smtlib_string_x c a1 a2 a3 a4 a5 =
(parse_smtlib_string c a1 a2 a3 a4 a5; get_smtlib_parse_results c);;
let parse_smtlib_file_x c a1 a2 a3 a4 a5 =
(parse_smtlib_file c a1 a2 a3 a4 a5; get_smtlib_parse_results c);;
(* Refinement: *)
type symbol_refined =
| Symbol_int of int
| Symbol_string of string
| Symbol_unknown;;
let symbol_refine c s =
match get_symbol_kind c s with
| INT_SYMBOL -> Symbol_int (get_symbol_int c s)
| STRING_SYMBOL -> Symbol_string (get_symbol_string c s);;
type sort_refined =
| Sort_uninterpreted of symbol
| Sort_bool
| Sort_int
| Sort_real
| Sort_bv of int
| Sort_array of (sort * sort)
| Sort_datatype of datatype_constructor_refined array
| Sort_relation
| Sort_finite_domain
| Sort_unknown of symbol;;
let sort_refine c ty =
match get_sort_kind c ty with
| UNINTERPRETED_SORT -> Sort_uninterpreted (get_sort_name c ty)
| BOOL_SORT -> Sort_bool
| INT_SORT -> Sort_int
| REAL_SORT -> Sort_real
| BV_SORT -> Sort_bv (get_bv_sort_size c ty)
| ARRAY_SORT -> Sort_array (get_array_sort_domain c ty, get_array_sort_range c ty)
| DATATYPE_SORT -> Sort_datatype (get_datatype_sort c ty)
| RELATION_SORT -> Sort_relation
| FINITE_DOMAIN_SORT -> Sort_finite_domain
| UNKNOWN_SORT -> Sort_unknown (get_sort_name c ty);;
let get_pattern_terms c p =
Array.init (get_pattern_num_terms c p) (get_pattern c p)
type binder_type = | Forall | Exists
type numeral_refined =
| Numeral_small of int64 * int64
| Numeral_large of string
type term_refined =
| Term_app of decl_kind * func_decl * ast array
| Term_quantifier of binder_type * int * ast array array * (symbol *sort) array * ast
| Term_numeral of numeral_refined * sort
| Term_var of int * sort
let term_refine c t =
match get_ast_kind c t with
| NUMERAL_AST ->
let (is_small, n, d) = get_numeral_small c t in
if is_small then
Term_numeral(Numeral_small(n,d), get_sort c t)
else
Term_numeral(Numeral_large(get_numeral_string c t), get_sort c t)
| APP_AST ->
let t' = to_app c t in
let f = get_app_decl c t' in
let num_args = get_app_num_args c t' in
let args = Array.init num_args (get_app_arg c t') in
let k = get_decl_kind c f in
Term_app (k, f, args)
| QUANTIFIER_AST ->
let bt = if is_quantifier_forall c t then Forall else Exists in
let w = get_quantifier_weight c t in
let np = get_quantifier_num_patterns c t in
let pats = Array.init np (get_quantifier_pattern_ast c t) in
let pats = Array.map (get_pattern_terms c) pats in
let nb = get_quantifier_num_bound c t in
let bound = Array.init nb
(fun i -> (get_quantifier_bound_name c t i, get_quantifier_bound_sort c t i)) in
let body = get_quantifier_body c t in
Term_quantifier(bt, w, pats, bound, body)
| VAR_AST ->
Term_var(get_index_value c t, get_sort c t)
| _ -> assert false
type theory_callbacks =
{
mutable delete_theory : unit -> unit;
mutable reduce_eq : ast -> ast -> ast option;
mutable reduce_app : func_decl -> ast array -> ast option;
mutable reduce_distinct : ast array -> ast option;
mutable final_check : unit -> bool;
mutable new_app : ast -> unit;
mutable new_elem : ast -> unit;
mutable init_search: unit -> unit;
mutable push: unit -> unit;
mutable pop: unit -> unit;
mutable restart : unit -> unit;
mutable reset: unit -> unit;
mutable new_eq : ast -> ast -> unit;
mutable new_diseq : ast -> ast -> unit;
mutable new_assignment: ast -> bool -> unit;
mutable new_relevant : ast -> unit;
}
let mk_theory_callbacks() =
{
delete_theory = (fun () -> ());
reduce_eq = (fun _ _ -> None);
reduce_app = (fun _ _ -> None);
reduce_distinct = (fun _ -> None);
final_check = (fun _ -> true);
new_app = (fun _ -> ());
new_elem = (fun _ -> ());
init_search= (fun () -> ());
push= (fun () -> ());
pop= (fun () -> ());
restart = (fun () -> ());
reset= (fun () -> ());
new_eq = (fun _ _ -> ());
new_diseq = (fun _ _ -> ());
new_assignment = (fun _ _ -> ());
new_relevant = (fun _ -> ());
}
external get_theory_callbacks : theory -> theory_callbacks = \"get_theory_callbacks\"
external mk_theory_register : context -> string -> theory_callbacks -> theory = \"mk_theory_register\"
external set_delete_callback_register : theory -> unit = \"set_delete_callback_register\"
external set_reduce_app_callback_register : theory -> unit = \"set_reduce_app_callback_register\"
external set_reduce_eq_callback_register : theory -> unit = \"set_reduce_eq_callback_register\"
external set_reduce_distinct_callback_register : theory -> unit = \"set_reduce_distinct_callback_register\"
external set_new_app_callback_register : theory -> unit = \"set_new_app_callback_register\"
external set_new_elem_callback_register : theory -> unit = \"set_new_elem_callback_register\"
external set_init_search_callback_register : theory -> unit = \"set_init_search_callback_register\"
external set_push_callback_register : theory -> unit = \"set_push_callback_register\"
external set_pop_callback_register : theory -> unit = \"set_pop_callback_register\"
external set_restart_callback_register : theory -> unit = \"set_restart_callback_register\"
external set_reset_callback_register : theory -> unit = \"set_reset_callback_register\"
external set_final_check_callback_register : theory -> unit = \"set_final_check_callback_register\"
external set_new_eq_callback_register : theory -> unit = \"set_new_eq_callback_register\"
external set_new_diseq_callback_register : theory -> unit = \"set_new_diseq_callback_register\"
external set_new_assignment_callback_register : theory -> unit = \"set_new_assignment_callback_register\"
external set_new_relevant_callback_register : theory -> unit = \"set_new_relevant_callback_register\"
let is_some opt =
match opt with
| Some v -> true
| None -> false
let get_some opt =
match opt with
| Some v -> v
| None -> failwith \"None unexpected\"
let apply_delete (th:theory_callbacks) = th.delete_theory ()
let set_delete_callback th cb =
let cbs = get_theory_callbacks th in
cbs.delete_theory <- cb;
set_delete_callback_register th
let mk_theory context name =
Callback.register \"is_some\" is_some;
Callback.register \"get_some\" get_some;
Callback.register \"apply_delete\" apply_delete;
let cbs = mk_theory_callbacks() in
mk_theory_register context name cbs
let apply_reduce_app (th:theory_callbacks) f args = th.reduce_app f args
let set_reduce_app_callback th cb =
Callback.register \"apply_reduce_app\" apply_reduce_app;
let cbs = get_theory_callbacks th in
cbs.reduce_app <- cb;
set_reduce_app_callback_register th
let apply_reduce_eq (th:theory_callbacks) a b = th.reduce_eq a b
let set_reduce_eq_callback th cb =
Callback.register \"apply_reduce_eq\" apply_reduce_eq;
let cbs = get_theory_callbacks th in
cbs.reduce_eq <- cb;
set_reduce_eq_callback_register th
let apply_reduce_distinct (th:theory_callbacks) args = th.reduce_distinct args
let set_reduce_distinct_callback th cb =
Callback.register \"apply_reduce_distinct\" apply_reduce_distinct;
let cbs = get_theory_callbacks th in
cbs.reduce_distinct <- cb;
set_reduce_distinct_callback_register th
let apply_new_app (th:theory_callbacks) a = th.new_app a
let set_new_app_callback th cb =
Callback.register \"apply_new_app\" apply_new_app;
let cbs = get_theory_callbacks th in
cbs.new_app <- cb;
set_new_app_callback_register th
let apply_new_elem (th:theory_callbacks) a = th.new_elem a
let set_new_elem_callback th cb =
Callback.register \"apply_new_elem\" apply_new_elem;
let cbs = get_theory_callbacks th in
cbs.new_elem <- cb;
set_new_elem_callback_register th
let apply_init_search (th:theory_callbacks) = th.init_search()
let set_init_search_callback th cb =
Callback.register \"apply_init_search\" apply_init_search;
let cbs = get_theory_callbacks th in
cbs.init_search <- cb;
set_init_search_callback_register th
let apply_push (th:theory_callbacks) = th.push()
let set_push_callback th cb =
Callback.register \"apply_push\" apply_push;
let cbs = get_theory_callbacks th in
cbs.push <- cb;
set_push_callback_register th
let apply_pop (th:theory_callbacks) = th.pop()
let set_pop_callback th cb =
Callback.register \"apply_pop\" apply_pop;
let cbs = get_theory_callbacks th in
cbs.pop <- cb;
set_pop_callback_register th
let apply_restart (th:theory_callbacks) = th.restart()
let set_restart_callback th cb =
Callback.register \"apply_restart\" apply_restart;
let cbs = get_theory_callbacks th in
cbs.restart <- cb;
set_restart_callback_register th
let apply_reset (th:theory_callbacks) = th.reset()
let set_reset_callback th cb =
Callback.register \"apply_reset\" apply_reset;
let cbs = get_theory_callbacks th in
cbs.reset <- cb;
set_reset_callback_register th
let apply_final_check (th:theory_callbacks) = th.final_check()
let set_final_check_callback th cb =
Callback.register \"apply_final_check\" apply_final_check;
let cbs = get_theory_callbacks th in
cbs.final_check <- cb;
set_final_check_callback_register th
let apply_new_eq (th:theory_callbacks) a b = th.new_eq a b
let set_new_eq_callback th cb =
Callback.register \"apply_new_eq\" apply_new_eq;
let cbs = get_theory_callbacks th in
cbs.new_eq <- cb;
set_new_eq_callback_register th
let apply_new_diseq (th:theory_callbacks) a b = th.new_diseq a b
let set_new_diseq_callback th cb =
Callback.register \"apply_new_diseq\" apply_new_diseq;
let cbs = get_theory_callbacks th in
cbs.new_diseq <- cb;
set_new_diseq_callback_register th
let apply_new_assignment (th:theory_callbacks) a b = th.new_assignment a b
let set_new_assignment_callback th cb =
Callback.register \"apply_new_assignment\" apply_new_assignment;
let cbs = get_theory_callbacks th in
cbs.new_assignment <- cb;
set_new_assignment_callback_register th
let apply_new_relevant (th:theory_callbacks) a = th.new_relevant a
let set_new_relevant_callback th cb =
Callback.register \"apply_new_relevant\" apply_new_relevant;
let cbs = get_theory_callbacks th in
cbs.new_relevant <- cb;
set_new_relevant_callback_register th
");

361
src/api/ml/x3V3.mli
View file

@ -1,361 +0,0 @@
quote (mli,"
(** {2 {L ML Extensions}} *)
(**
\[ [ mk_context_x configs] \] is a shorthand for the context with configurations in [configs].
*)
val mk_context_x: (string * string) array -> context;;
(**
\[ [ get_app_args c a ] \] is the array of arguments of an application. If [t] is a constant, then the array is empty.
- {b See also}: {!Z3.get_app_num_args}
- {b See also}: {!Z3.get_app_arg}
*)
val get_app_args: context -> app -> ast array
(**
\[ [ get_app_args c d ] \] is the array of parameters of [d].
- {b See also}: {!Z3.get_domain_size}
- {b See also}: {!Z3.get_domain}
*)
val get_domains: context -> func_decl -> sort array
(**
\[ [ get_array_sort c t ] \] is the domain and the range of [t].
- {b See also}: {!Z3.get_array_sort_domain}
- {b See also}: {!Z3.get_array_sort_range}
*)
val get_array_sort: context -> sort -> sort * sort
(**
\[ [ get_tuple_sort c ty ] \] is the pair [(mk_decl, fields)] where [mk_decl] is the constructor declaration of [ty], and [fields] is the array of fields in [ty].
- {b See also}: {!Z3.get_tuple_sort_mk_decl}
- {b See also}: {!Z3.get_tuple_sort_num_fields}
- {b See also}: {!Z3.get_tuple_sort_field_decl}
*)
val get_tuple_sort: context -> sort -> (func_decl * func_decl array)
(**
\[ [ datatype_constructor_refined ] \] is the refinement of a datatype constructor.
It contains the constructor declaration, recognizer, and list of accessor functions.
*)
type datatype_constructor_refined = {
constructor : func_decl;
recognizer : func_decl;
accessors : func_decl array
}
(**
\[ [ get_datatype_sort c ty ] \] is the array of triples [(constructor, recognizer, fields)] where [constructor] is the constructor declaration of [ty], [recognizer] is the recognizer for the [constructor], and [fields] is the array of fields in [ty].
- {b See also}: {!Z3.get_datatype_sort_num_constructors}
- {b See also}: {!Z3.get_datatype_sort_constructor}
- {b See also}: {!Z3.get_datatype_sort_recognizer}
- {b See also}: {!Z3.get_datatype_sort_constructor_accessor}
*)
val get_datatype_sort: context -> sort -> datatype_constructor_refined array
(**
\[ [ get_model_constants c m ] \] is the array of constants in the model [m].
- {b See also}: {!Z3.get_model_num_constants}
- {b See also}: {!Z3.get_model_constant}
*)
val get_model_constants: context -> model -> func_decl array
(**
\[ [ get_model_func_entry c m i j ] \] is the [j]'th entry in the [i]'th function in the model [m].
- {b See also}: {!Z3.get_model_func_entry_num_args}
- {b See also}: {!Z3.get_model_func_entry_arg}
- {b See also}: {!Z3.get_model_func_entry_value}
*)
val get_model_func_entry: context -> model -> int -> int -> (ast array * ast);;
(**
\[ [ get_model_func_entries c m i ] \] is the array of entries in the [i]'th function in the model [m].
- {b See also}: {!Z3.get_model_func_num_entries}
- {b See also}: {!Z3.get_model_func_entry}
*)
val get_model_func_entries: context -> model -> int -> (ast array * ast) array;;
(**
\[ [ get_model_funcs c m ] \] is the array of functions in the model [m]. Each function is represented by the triple [(decl, entries, else)], where [decl] is the declaration name for the function, [entries] is the array of entries in the function, and [else] is the default (else) value for the function.
- {b See also}: {!Z3.get_model_num_funcs}
- {b See also}: {!Z3.get_model_func_decl}
- {b See also}: {!Z3.get_model_func_entries}
- {b See also}: {!Z3.get_model_func_else}
*)
val get_model_funcs: context -> model ->
(symbol *
(ast array * ast) array *
ast) array
(**
\[ [ get_smtlib_formulas c ] \] is the array of formulas created by a preceding call to {!Z3.parse_smtlib_string} or {!Z3.parse_smtlib_file}.
Recommend use {!Z3.parse_smtlib_string_x} or {!Z3.parse_smtlib_file_x} for functional style interface to the SMT-LIB parser.
- {b See also}: {!Z3.parse_smtlib_string_x}
- {b See also}: {!Z3.parse_smtlib_file_x}
- {b See also}: {!Z3.parse_smtlib_string}
- {b See also}: {!Z3.parse_smtlib_file}
- {b See also}: {!Z3.get_smtlib_num_formulas}
- {b See also}: {!Z3.get_smtlib_formula}
*)
val get_smtlib_formulas: context -> ast array
(**
\[ [get_smtlib_assumptions c] \] is the array of assumptions created by a preceding call to {!Z3.parse_smtlib_string} or {!Z3.parse_smtlib_file}.
Recommend use {!Z3.parse_smtlib_string_x} or {!Z3.parse_smtlib_file_x} for functional style interface to the SMT-LIB parser.
- {b See also}: {!Z3.parse_smtlib_string_x}
- {b See also}: {!Z3.parse_smtlib_file_x}
- {b See also}: {!Z3.parse_smtlib_string}
- {b See also}: {!Z3.parse_smtlib_file}
- {b See also}: {!Z3.get_smtlib_num_assumptions}
- {b See also}: {!Z3.get_smtlib_assumption}
*)
val get_smtlib_assumptions: context -> ast array
(**
\[ [ get_smtlib_decls c ] \] is the array of declarations created by a preceding call to {!Z3.parse_smtlib_string} or {!Z3.parse_smtlib_file}.
Recommend use {!Z3.parse_smtlib_string_x} or {!Z3.parse_smtlib_file_x} for functional style interface to the SMT-LIB parser.
- {b See also}: {!Z3.parse_smtlib_string_x}
- {b See also}: {!Z3.parse_smtlib_file_x}
- {b See also}: {!Z3.parse_smtlib_string}
- {b See also}: {!Z3.parse_smtlib_file}
- {b See also}: {!Z3.get_smtlib_num_decls}
- {b See also}: {!Z3.get_smtlib_decl}
*)
val get_smtlib_decls: context -> func_decl array
(**
\[ [ get_smtlib_parse_results c ] \] is the triple [(get_smtlib_formulas c, get_smtlib_assumptions c, get_smtlib_decls c)].
Recommend use {!Z3.parse_smtlib_string_x} or {!Z3.parse_smtlib_file_x} for functional style interface to the SMT-LIB parser.
- {b See also}: {!Z3.parse_smtlib_string_x}
- {b See also}: {!Z3.parse_smtlib_file_x}
- {b See also}: {!Z3.parse_smtlib_string}
- {b See also}: {!Z3.parse_smtlib_file}
- {b See also}: {!Z3.get_smtlib_formulas}
- {b See also}: {!Z3.get_smtlib_assumptions}
- {b See also}: {!Z3.get_smtlib_decls}
*)
val get_smtlib_parse_results: context -> (ast array * ast array * func_decl array)
(**
\[ [ parse_smtlib_string_formula c ... ] \] calls [(parse_smtlib_string c ...)] and returns the single formula produced.
Recommended for functional style interface to the SMT-LIB parser.
- {b See also}: {!Z3.parse_smtlib_file_formula}
- {b See also}: {!Z3.parse_smtlib_string_x}
*)
val parse_smtlib_string_formula: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast
(**
\[ [ parse_smtlib_file_formula c ... ] \] calls [(parse_smtlib_file c ...)] and returns the single formula produced.
Recommended for functional style interface to the SMT-LIB parser.
- {b See also}: {!Z3.parse_smtlib_file_formula}
- {b See also}: {!Z3.parse_smtlib_file_x}
*)
val parse_smtlib_file_formula: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast
(**
\[ [ parse_smtlib_string_x c ... ] \] is [(parse_smtlib_string c ...; get_smtlib_parse_results c)]
Recommended for functional style interface to the SMT-LIB parser.
- {b See also}: {!Z3.parse_smtlib_file_x}
- {b See also}: {!Z3.parse_smtlib_string}
- {b See also}: {!Z3.get_smtlib_parse_results}
*)
val parse_smtlib_string_x: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> (ast array * ast array * func_decl array)
(**
\[ [ parse_smtlib_file_x c ... ] \] is [(parse_smtlib_file c ...; get_smtlib_parse_results c)]
Recommended for functional style interface to the SMT-LIB parser.
- {b See also}: {!Z3.parse_smtlib_string_x}
- {b See also}: {!Z3.parse_smtlib_file}
- {b See also}: {!Z3.get_smtlib_parse_results}
*)
val parse_smtlib_file_x: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> (ast array * ast array * func_decl array)
(**
\[ [ symbol_refined ] \] is the refinement of a {!Z3.symbol} .
- {b See also}: {!Z3.symbol_refine}
- {b See also}: {!Z3.get_symbol_kind}
*)
type symbol_refined =
| Symbol_int of int
| Symbol_string of string
| Symbol_unknown;;
(**
\[ [ symbol_refine c s ] \] is the refined symbol of [s].
- {b See also}: {!Z3.symbol_refined}
- {b See also}: {!Z3.get_symbol_kind}
*)
val symbol_refine: context -> symbol -> symbol_refined;;
(**
\[ [ sort_refined ] \] is the refinement of a {!Z3.sort} .
- {b See also}: {!Z3.sort_refine}
- {b See also}: {!Z3.get_sort_kind}
*)
type sort_refined =
| Sort_uninterpreted of symbol
| Sort_bool
| Sort_int
| Sort_real
| Sort_bv of int
| Sort_array of (sort * sort)
| Sort_datatype of datatype_constructor_refined array
| Sort_relation
| Sort_finite_domain
| Sort_unknown of symbol
(**
\[ [ sort_refine c t ] \] is the refined sort of [t].
- {b See also}: {!Z3.sort_refined}
- {b See also}: {!Z3.get_sort_kind}
*)
val sort_refine: context -> sort -> sort_refined;;
(**
\[ [ binder_type ] \] is a universal or existential quantifier.
- {b See also}: {!Z3.term_refined}
*)
type binder_type = | Forall | Exists
(**
\[ [ numeral_refined ] \] is the refinement of a numeral .
Numerals whose fractional representation can be fit with
64 bit integers are treated as small.
*)
type numeral_refined =
| Numeral_small of int64 * int64
| Numeral_large of string
(**
\[ [ term_refined ] \] is the refinement of a {!Z3.ast} .
- {b See also}: {!Z3.term_refine}
*)
type term_refined =
| Term_app of decl_kind * func_decl * ast array
| Term_quantifier of binder_type * int * ast array array * (symbol * sort) array * ast
| Term_numeral of numeral_refined * sort
| Term_var of int * sort
(**
\[ [ term_refine c a ] \] is the refined term of [a].
- {b See also}: {!Z3.term_refined}
*)
val term_refine : context -> ast -> term_refined
(**
\[ [mk_theory c name ] \] create a custom theory.
*)
val mk_theory : context -> string -> theory
(**
\[ [set_delete_callback th cb] \] set callback when theory gets deleted.
*)
val set_delete_callback : theory -> (unit -> unit) -> unit
(**
\[ [set_reduce_app_callback th cb] \] set callback for simplifying theory terms.
*)
val set_reduce_app_callback : theory -> (func_decl -> ast array -> ast option) -> unit
(**
\[ [set_reduce_eq_callback th cb] \] set callback for simplifying equalities over theory terms.
*)
val set_reduce_eq_callback : theory -> (ast -> ast -> ast option) -> unit
(**
\[ [set_reduce_distinct_callback th cb] \] set callback for simplifying disequalities over theory terms.
*)
val set_reduce_distinct_callback : theory -> (ast array -> ast option) -> unit
(**
\[ [set_new_app_callback th cb] \] set callback for registering new application.
*)
val set_new_app_callback : theory -> (ast -> unit) -> unit
(**
\[ [set_new_elem_callback th cb] \] set callback for registering new element.
- {b See also}: the help for the corresponding C API function.
*)
val set_new_elem_callback : theory -> (ast -> unit) -> unit
(**
\[ [set_init_search_callback th cb] \] set callback when Z3 starts searching for a satisfying assignment.
*)
val set_init_search_callback : theory -> (unit -> unit) -> unit
(**
\[ [set_push_callback th cb] \] set callback for a logical context push.
*)
val set_push_callback : theory -> (unit -> unit) -> unit
(**
\[ [set_pop_callback th cb] \] set callback for a logical context pop.
*)
val set_pop_callback : theory -> (unit -> unit) -> unit
(**
\[ [set_restart_callback th cb] \] set callback for search restart.
*)
val set_restart_callback : theory -> (unit -> unit) -> unit
val set_reset_callback : theory -> (unit -> unit) -> unit
val set_final_check_callback : theory -> (unit -> bool) -> unit
val set_new_eq_callback : theory -> (ast -> ast -> unit) -> unit
val set_new_diseq_callback : theory -> (ast -> ast -> unit) -> unit
val set_new_assignment_callback : theory -> (ast -> bool -> unit) -> unit
val set_new_relevant_callback : theory -> (ast -> unit) -> unit
");

597
src/api/ml/z3.0.idl
View file

@ -1,597 +0,0 @@
/*++
Copyright (c) Microsoft Corporation
Module Name:
Z3
Abstract:
OCaml API for Z3.
The following design is used for the treatment of reference counting:
- The conversion of Z3_context from ML to C remembers the Z3 context, and
registers a finalizer using Gc.finalize that calls Z3_del_context.
- The conversion of Z3_ast and other reference counted types from C to ML:
+ stores the last translated context with the Z3_ast in the wrapper
object;
+ registers a finalizer using Gc.finalize that decrements the reference
counter of the Z3_ast;
+ increments the reference count of the Z3_ast.
The finalizers are registered using (the C interface to) Gc.finalize,
not attaching a finalizer to a custom block. The finalizers registered
by Gc.finalize are guaranteed to be called in reverse
registration-order, which is necessary to ensure that Z3_context's are
finalized only after all the Z3_ast's within them.
- ML Z3.ast (and subtypes) are given generic hash and comparison
operations using Z3_get_ast_hash and Z3_get_ast_id. Other types could
be handled similarly if analogous hash and id operations were exported
by the C API.
- The wrapper for Z3_mk_context is customized (using quote(call,...) in
z3_api.patched.h) to call Z3_mk_context_rc, and the ML API does not
include mk_context_rc.
This scheme relies on the property that all reference counted values
returned from C to ML are in the Z3_context that was last sent from ML to
C. This is normally straightforward, but note that it depends on the
argument order of e.g. the Z3_*translate functions.
Non-reference counted Z3 types that have delete operations have finalizers
that call the delete operations. The exposed delete operations are
shadowed by nop functions. The types whose delete operation accepts a
context use Gc.finalize while those that do not use custom block
finalizers.
Custom c2ml functions check the Z3 error code prior to allocating ML
values or registering finalizers. Other functions check the Z3 error code
after making a Z3 library call.
Some operations return NULL pointers when operations fail, or accept NULL
pointers. To handle these cases Z3_{ast,func_interp,sort}_opt types are
introduced. These are synonyms of Z3_{ast,func_interp,sort} but are
translated into OCaml option types. If the NULL pointers were passed to
ML, even if the user does not access them, they will have finalizers
registered, so when they die the OCaml GC will crash trying to call
dec_ref on NULL.
There is an alternate implementation, enabled by setting LEAK_CONTEXTS,
that avoids the overhead of Gc.finalize finalizers, but at the price of
leaking Z3_context objects.
Notes:
OCaml does not support unsigned types, so CamlIDL conflates signed and
unsigned types of the same size. Therefore, functions in the C API
operating on unsigned values that become redundant after this conflation
are excluded from the ML API using [#ifndef CAMLIDL] in z3_api.h.
CamlIDL does not support function pointers, so functions in the C API with
function pointer arguments are handled manually.
Author:
Jakob Lichtenberg (JakobL) 2007-08-08
Josh Berdine (jjb) 2012-03-21
--*/
// cpp trick to include expanded macro arguments in string literals
#define xstr(s) str(s)
#define str(s) #s
quote(c,"#define xstr(s) str(s)");
quote(c,"#define str(s) #s");
#ifndef MLAPIV3
#define DEFINE_TYPE(T) typedef [abstract] void* T
#define DEFINE_VOID(T) typedef [abstract] void* T
#define BEGIN_MLAPI_EXCLUDE quote(mli,"(*");
#define END_MLAPI_EXCLUDE quote(mli,"*)");
#ifdef LEAK_CONTEXTS
// Declare pointer type with custom conversion functions.
#define DEFINE_CUST_TYPE(T) \
typedef [abstract, ml2c(ml2c_Z3_ ## T), c2ml(c2ml_Z3_ ## T)] void* Z3_ ## T
#else
// Declare pointer type with custom conversion functions.
// Register an OCaml closure that just calls a C finalization function.
#define DEFINE_CUST_TYPE(T) \
quote(ml,xstr(\
external finalize_Z3_ ## T : T -> unit = xstr(finalize_Z3_ ## T);; \
let _ = Callback.register xstr(finalize_Z3_ ## T) finalize_Z3_ ## T \
)); \
typedef [abstract, ml2c(ml2c_Z3_ ## T), c2ml(c2ml_Z3_ ## T)] void* Z3_ ## T
#endif
// Z3_context
quote(c,"
void check_error_code (Z3_context c);
Z3_context last_ctx;
");
#ifdef LEAK_CONTEXTS
quote(c,"
value c2ml_Z3_context(Z3_context* c)
{
value v;
v = caml_alloc_small(1, Abstract_tag);
*((Z3_context *) Bp_val(v)) = *c;
return v;
}
void ml2c_Z3_context(value v, Z3_context* c)
{
*c = *((Z3_context *) Bp_val(v));
last_ctx = *c;
}
");
#else
quote(c,"
// caml_final_register is the implementation of Gc.finalize
value caml_final_register (value f, value v);
void register_finalizer(value** closure, char* name, Z3_context ctx, value v)
{
if (*closure == NULL) {
*closure = caml_named_value(name);
if (*closure == NULL) {
Z3_set_error(ctx, Z3_INTERNAL_FATAL);
return;
}
}
caml_final_register(**closure, v);
}
value c2ml_Z3_context (Z3_context* c)
{
static value* finalize_Z3_context_closure = NULL;
value v;
v = caml_alloc_small(1, Abstract_tag);
Field(v, 0) = (value) *c;
register_finalizer(&finalize_Z3_context_closure, \"finalize_Z3_context\",
(Z3_context) *c, v);
return v;
}
void ml2c_Z3_context (value v, Z3_context* c)
{
*c = (Z3_context) Field(v, 0);
last_ctx = *c;
}
value finalize_Z3_context (value v)
{
Z3_context c;
c = (Z3_context) Field(v, 0);
Z3_del_context(c);
return Val_unit;
}
");
#endif
DEFINE_CUST_TYPE(context);
// Z3_symbol
typedef [abstract] void* Z3_symbol;
// Z3_ast: reference counted type with hashing and comparison
quote(c,"
typedef struct _Z3_ast_context {
Z3_ast ast;
Z3_context ctx;
} Z3_ast_context;
void ml2c_Z3_ast (value v, Z3_ast* c)
{
*c = ((Z3_ast_context*) Data_custom_val(v))->ast;
}
static int compare_Z3_ast (value v1, value v2)
{
Z3_ast_context* ac1;
Z3_ast_context* ac2;
unsigned id1, id2;
ac1 = Data_custom_val(v1);
ac2 = Data_custom_val(v2);
id1 = Z3_get_ast_id(ac1->ctx, ac1->ast);
check_error_code(ac1->ctx);
id2 = Z3_get_ast_id(ac2->ctx, ac2->ast);
check_error_code(ac2->ctx);
return id2 - id1;
}
static intnat hash_Z3_ast (value v)
{
Z3_ast_context* ac;
unsigned hash;
ac = Data_custom_val(v);
hash = Z3_get_ast_hash(ac->ctx, ac->ast);
check_error_code(ac->ctx);
return hash;
}
");
#ifdef LEAK_CONTEXTS
quote(c,"
static void finalize_Z3_ast (value v)
{
Z3_ast_context* ac;
ac = Data_custom_val(v);
Z3_dec_ref(ac->ctx, ac->ast);
check_error_code(ac->ctx);
}
static struct custom_operations cops_Z3_ast = {
NULL,
finalize_Z3_ast,
compare_Z3_ast,
hash_Z3_ast,
custom_serialize_default,
custom_deserialize_default
};
value c2ml_Z3_ast (Z3_ast* c)
{
value v;
Z3_ast_context* ac;
check_error_code(last_ctx);
v = alloc_custom(&cops_Z3_ast, sizeof(Z3_ast_context), 0, 1);
ac = Data_custom_val(v);
ac->ctx = last_ctx;
ac->ast = *c;
Z3_inc_ref(ac->ctx, ac->ast);
return v;
}
");
#else
quote(c,"
value finalize_Z3_ast (value v)
{
Z3_ast_context* ac;
ac = Data_custom_val(v);
Z3_dec_ref(ac->ctx, ac->ast);
check_error_code(ac->ctx);
return Val_unit;
}
static struct custom_operations cops_Z3_ast = {
NULL,
custom_finalize_default,
compare_Z3_ast,
hash_Z3_ast,
custom_serialize_default,
custom_deserialize_default
};
value c2ml_Z3_ast (Z3_ast* c)
{
static value* finalize_Z3_ast_closure = NULL;
value v;
Z3_ast_context* ac;
check_error_code(last_ctx);
v = caml_alloc_custom(&cops_Z3_ast, sizeof(Z3_ast_context), 0, 1);
ac = Data_custom_val(v);
ac->ast = *c;
ac->ctx = last_ctx;
register_finalizer(&finalize_Z3_ast_closure, \"finalize_Z3_ast\",
(Z3_context) *c, v);
Z3_inc_ref(last_ctx, *c);
return v;
}
");
#endif
DEFINE_CUST_TYPE(ast);
// subtypes of Z3_ast
quote(c,"\
#define DEFINE_SUBAST_OPS(T) \
void ml2c_ ## T (value v, T * a) \
{ \
ml2c_Z3_ast(v, (Z3_ast*) a); \
} \
\
value c2ml_ ## T (T * a) \
{ \
return c2ml_Z3_ast((Z3_ast*) a); \
} \
");
#define DEFINE_SUBAST(T) \
typedef [mltype("private ast"), ml2c(ml2c_ ## T), c2ml(c2ml_ ## T)] Z3_ast T
quote(c,"DEFINE_SUBAST_OPS(Z3_sort)"); DEFINE_SUBAST(Z3_sort);
quote(c,"DEFINE_SUBAST_OPS(Z3_func_decl)"); DEFINE_SUBAST(Z3_func_decl);
quote(c,"DEFINE_SUBAST_OPS(Z3_app)"); DEFINE_SUBAST(Z3_app);
quote(c,"DEFINE_SUBAST_OPS(Z3_pattern)"); DEFINE_SUBAST(Z3_pattern);
// reference counted types without hashing and comparison
#ifdef LEAK_CONTEXTS
quote(c,"\
#define DEFINE_RC_OPS(T) \
typedef struct _ ## T ## _context { \
T dat; \
Z3_context ctx; \
} T ## _context; \
\
static void finalize_ ## T (value v) \
{ \
T ## _context* ac; \
ac = Data_custom_val(v); \
T ## _dec_ref(ac->ctx, ac->dat); \
check_error_code(ac->ctx); \
} \
\
static struct custom_operations cops_ ## T = { \
NULL, \
finalize_ ## T, \
custom_compare_default, \
custom_hash_default, \
custom_serialize_default, \
custom_deserialize_default \
}; \
\
value c2ml_ ## T (T * c) \
{ \
value v; \
T ## _context* ac; \
check_error_code(last_ctx); \
v = alloc_custom(&cops_ ## T, sizeof(T ## _context), 0, 1); \
ac = Data_custom_val(v); \
ac->dat = *c; \
ac->ctx = last_ctx; \
T ## _inc_ref(ac->ctx, ac->dat); \
return v; \
} \
\
void ml2c_ ## T (value v, T * c) \
{ \
*c = ((T ## _context*) Data_custom_val(v))->dat; \
} \
");
#else
quote(c,"\
#define DEFINE_RC_OPS(T) \
value c2ml_ ## T (T * c) \
{ \
static value* finalize_ ## T ## _closure = NULL; \
value v; \
check_error_code(last_ctx); \
v = caml_alloc_small(2, Abstract_tag); \
Field(v, 0) = (value) *c; \
Field(v, 1) = (value) last_ctx; \
register_finalizer(&finalize_ ## T ## _closure, xstr(finalize_ ## T), \
(Z3_context) *c, v); \
T ## _inc_ref(last_ctx, *c); \
return v; \
} \
\
void ml2c_ ## T (value v, T * c) \
{ \
*c = (T) Field(v, 0); \
} \
\
value finalize_ ## T (value v) \
{ \
Z3_context c; \
c = (Z3_context) Field(v, 1); \
T ## _dec_ref(c, (T) Field(v, 0)); \
check_error_code(c); \
return Val_unit; \
} \
");
#endif
quote(c,"DEFINE_RC_OPS(Z3_params)"); DEFINE_CUST_TYPE(params);
quote(c,"DEFINE_RC_OPS(Z3_param_descrs)"); DEFINE_CUST_TYPE(param_descrs);
quote(c,"DEFINE_RC_OPS(Z3_model)"); DEFINE_CUST_TYPE(model);
quote(c,"DEFINE_RC_OPS(Z3_func_interp)"); DEFINE_CUST_TYPE(func_interp);
quote(c,"DEFINE_RC_OPS(Z3_func_entry)"); DEFINE_CUST_TYPE(func_entry);
quote(c,"DEFINE_RC_OPS(Z3_fixedpoint)"); DEFINE_CUST_TYPE(fixedpoint);
quote(c,"DEFINE_RC_OPS(Z3_ast_vector)"); DEFINE_CUST_TYPE(ast_vector);
quote(c,"DEFINE_RC_OPS(Z3_ast_map)"); DEFINE_CUST_TYPE(ast_map);
quote(c,"DEFINE_RC_OPS(Z3_goal)"); DEFINE_CUST_TYPE(goal);
quote(c,"DEFINE_RC_OPS(Z3_tactic)"); DEFINE_CUST_TYPE(tactic);
quote(c,"DEFINE_RC_OPS(Z3_probe)"); DEFINE_CUST_TYPE(probe);
quote(c,"DEFINE_RC_OPS(Z3_apply_result)"); DEFINE_CUST_TYPE(apply_result);
quote(c,"DEFINE_RC_OPS(Z3_solver)"); DEFINE_CUST_TYPE(solver);
quote(c,"DEFINE_RC_OPS(Z3_stats)"); DEFINE_CUST_TYPE(stats);
// possibly-NULL pointer types, translated to OCaml option types
quote(c,"\
#define DEFINE_OPT_OPS(T) \
void ml2c_ ## T ## _opt (value v, T* c) \
{ \
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL }; \
camlidl_ctx _ctx = &_ctxs; \
if (v != Val_int(0)) { \
camlidl_ml2c_z3_ ## T(Field(v, 0), c, _ctx); \
} else { \
*c = NULL; \
} \
} \
\
value c2ml_ ## T ## _opt (T* c) \
{ \
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL }; \
camlidl_ctx _ctx = &_ctxs; \
value v; \
value a; \
if (*c) { \
a = camlidl_c2ml_z3_ ## T(c, _ctx); \
Begin_root(a) \
v = caml_alloc_small(1, 0); \
Field(v, 0) = a; \
End_roots(); \
} else { \
v = Val_int(0); \
} \
return v; \
}
");
#define DEFINE_OPT_TYPE(T) \
typedef [mltype(xstr(T option)), \
ml2c(ml2c_Z3_ ## T ## _opt), \
c2ml(c2ml_Z3_ ## T ## _opt) \
] Z3_ ## T Z3_ ## T ## _opt
quote(c,"DEFINE_OPT_OPS(Z3_ast)");
DEFINE_OPT_TYPE(ast);
quote(c,"DEFINE_OPT_OPS(Z3_sort)");
DEFINE_OPT_TYPE(sort);
quote(c,"DEFINE_OPT_OPS(Z3_func_interp)");
DEFINE_OPT_TYPE(func_interp);
// ToDo: these unnecessarily appear in the API documentation
DEFINE_TYPE(Z3_constructor);
DEFINE_TYPE(Z3_constructor_list);
// shadow delete operations with nops
quote(ml,"
let del_constructor _ _ = ()
let del_constructor_list _ _ = ()
let del_model _ _ = ()
let del_context _ = ()
let reset_memory () = ()
");
#else // MLAPIV3
// Provide custom error handler:
quote (c,"Z3_error_handler caml_z3_error_handler;");
quote (c,"void caml_z3_error_handler(Z3_context c, Z3_error_code e) { static char buffer[128]; char * msg = Z3_get_error_msg_ex(c, e); if (strlen(msg) > 100) { failwith(\"Z3: error message is too big to fit in buffer\"); } else { sprintf(buffer, \"Z3: %s\", msg); failwith(buffer); } }");
#define DEFINE_TYPE(T) typedef [abstract] void* T
#define DEFINE_VOID(T) typedef [abstract] void* T
#define BEGIN_MLAPI_EXCLUDE
#define END_MLAPI_EXCLUDE
#endif // MLAPIV3
#ifndef __in
#define __in [in]
#endif
#ifndef __out
#define __out [out]
#endif
#ifndef __out_opt
#define __out_opt [out,unique]
#endif
#ifndef __ecount
#define __ecount(num_args) [NOT_SUPPORTED]
#endif
#ifndef __in_ecount
#define __in_ecount(num_args) [in, size_is(num_args), length_is(num_args)]
#endif
#ifndef __out_ecount
#define __out_ecount(num_args) [out, size_is(num_args), length_is(num_args)]
#endif
#ifndef __inout_ecount
#define __inout_ecount(num_args) [in, out, size_is(num_args), length_is(num_args)]
#endif
#ifndef __inout
#define __inout [in, out]
#endif
#ifndef Z3_bool_opt
#define Z3_bool_opt void
#endif
#define Z3_API
#ifdef MLAPIV3
#include "z3V3_api.idl"
#include "x3V3.mli"
#include "x3V3.ml"
#else
#include "z3_api.idl"
#include "x3.ml"
quote(ml,"
let _ =
Printexc.register_printer (function
| Error(c,e) -> Some (\"Z3 \"^(get_error_msg c e))
| _ -> None
)
");
quote(mli,"
(**
{2 {L Legacy V3 API}}
*)
module V3 : sig
(**
{2 {L Legacy V3 API}}
*)
");
quote(ml,"
module V3 = struct
");
#endif
#ifdef MLAPIV3
quote(mlmli,"
end
");
#endif

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

File diff suppressed because it is too large Load diff

12727
src/api/ml/z3.mli
View file

File diff suppressed because it is too large Load diff

19044
src/api/ml/z3_stubs.c
View file

File diff suppressed because it is too large Load diff

339
src/api/ml/z3_theory_stubs.c
View file

@ -1,339 +0,0 @@
/*++
Copyright (c) Microsoft Corporation
Module Name:
z3_theory_stubs.c
Abstract:
OCaml C bindings for callbacks between OCaml and C for
theory plugins.
The API for theory plugins require associating a set of
callbacks as C function pointers.
We use the following strategy:
- store in the user_ext_data blob that theory constructors allow
a record of callback functions.
- define catch-all static callback functions that access the
ML record with the callbacks. It then invokes these through user-registered
application functions that apply the callback stored in the record to the
actual parameters.
It is tempting to avoid this user-registered callback and directly access
the record of callback functions and apply the proper field.
However, the layout of records appears to be opaque, or at least we assume it is
so, from the C runtime.
Author:
Revision History:
--*/
#include <stddef.h>
#include <string.h>
#include <caml/mlvalues.h>
#include <caml/memory.h>
#include <caml/alloc.h>
#include <caml/fail.h>
#include <caml/callback.h>
#ifdef Custom_tag
#include <caml/custom.h>
#include <caml/bigarray.h>
#endif
#include "z3.h"
#define ML_SIZE(_ty) ((sizeof(_ty) + sizeof(value) - 1)/ sizeof(value))
static value mk_func_decl(Z3_func_decl f) {
value _f = alloc(ML_SIZE(Z3_func_decl), Abstract_tag);
*((Z3_func_decl*) Bp_val(_f)) = f;
return _f;
}
static value Val_ast(Z3_ast a) {
value _a = alloc(ML_SIZE(Z3_ast), Abstract_tag);
*((Z3_ast*) Bp_val(_a)) = a;
return _a;
}
static value Val_ast_array(unsigned int sz, Z3_ast const args[]) {
value res;
Z3_ast* args1;
unsigned int i;
args1 = malloc((sz+1)*sizeof(Z3_ast));
for (i = 0; i < sz; ++i) {
args1[i] = args[i];
}
args1[sz] = 0;
res = alloc_array((value (*)(char const*))Val_ast, (const char**)args1);
free(args1);
return res;
}
// ------------------
// get_theory_callbacks
//
value get_theory_callbacks(value th)
{
Z3_theory _th = *((Z3_theory*) Bp_val(th));
return (value) Z3_theory_get_ext_data(_th);
}
// ------------------
// delete_theory
//
static void delete_callback_static(Z3_theory th)
{
CAMLparam0();
CAMLlocal1(f);
value user_data = (value) Z3_theory_get_ext_data(th);
f = *(caml_named_value("apply_delete")) ;
callback(f, user_data);
remove_global_root(&user_data);
CAMLreturn0;
}
#define SET_CALLBACK(_cb_name) \
value set_ ## _cb_name ## _callback_register(value th) \
{ \
CAMLparam1(th); \
Z3_theory _th = *((Z3_theory*) Bp_val(th)); \
Z3_set_ ## _cb_name ## _callback(_th, _cb_name ## _callback_static); \
CAMLreturn(Val_unit); \
} \
SET_CALLBACK(delete);
// ------------------
// mk_theory
//
value mk_theory_register(value context, value name, value user_data)
{
CAMLparam3(context, name, user_data);
Z3_context _context = *((Z3_context *) Bp_val(context));
value _th;
Z3_theory th;
register_global_root(&user_data);
th = Z3_mk_theory(_context, String_val(name), (void*)user_data);
// jjb: test th == NULL ?
Z3_set_delete_callback(th, delete_callback_static);
_th = alloc(ML_SIZE(Z3_context), Abstract_tag);
*((Z3_theory*) Bp_val(_th)) = th;
CAMLreturn(_th);
}
// -------------------
// reduce_app_callback
static Z3_bool reduce_app_callback_static(Z3_theory th, Z3_func_decl f, unsigned num_args, Z3_ast const args[], Z3_ast* r) {
CAMLparam0();
CAMLlocal4(cb, _r, _v, _args);
value user_data;
Z3_bool result;
_args = Val_ast_array(num_args, args);
user_data = (value) Z3_theory_get_ext_data(th);
cb = *(caml_named_value("apply_reduce_app"));
_r = callback3(cb, user_data, mk_func_decl(f), _args);
cb = *(caml_named_value("is_some"));
_v = callback(cb, _r);
result = 0 != Bool_val(_v);
if (result && r) {
cb = *(caml_named_value("get_some"));
_v = callback(cb, _r);
*r = *((Z3_ast*) Bp_val(_v));
}
CAMLreturn (result);
}
SET_CALLBACK(reduce_app);
// -------------------
// reduce_eq_callback
static Z3_bool reduce_eq_callback_static(Z3_theory th, Z3_ast a, Z3_ast b, Z3_ast * r)
{
CAMLparam0();
CAMLlocal5(cb, _r, _a, _b, _v);
value user_data;
Z3_bool result;
_a = Val_ast(a);
_b = Val_ast(b);
user_data = (value) Z3_theory_get_ext_data(th);
cb = *(caml_named_value("apply_reduce_eq"));
_r = callback3(cb, user_data, _a, _b);
cb = *(caml_named_value("is_some"));
_v = callback(cb, _r);
result = 0 != Bool_val(_v);
if (result && r) {
cb = *(caml_named_value("get_some"));
_v = callback(cb, _r);
*r = *((Z3_ast*) Bp_val(_v));
}
CAMLreturn (result);
}
SET_CALLBACK(reduce_eq);
// -------------------
// reduce_distinct
static Z3_bool reduce_distinct_callback_static(Z3_theory th, unsigned n, Z3_ast const args[], Z3_ast * r)
{
CAMLparam0();
CAMLlocal4(cb, _r, _args, _v);
value user_data;
Z3_bool result;
_args = Val_ast_array(n, args);
user_data = (value) Z3_theory_get_ext_data(th);
cb = *(caml_named_value("apply_reduce_distinct"));
_r = callback2(cb, user_data, _args);
cb = *(caml_named_value("is_some"));
_v = callback(cb, _r);
result = 0 != Bool_val(_v);
if (result && r) {
cb = *(caml_named_value("get_some"));
_v = callback(cb, _r);
*r = *((Z3_ast*) Bp_val(_v));
}
CAMLreturn (result);
}
SET_CALLBACK(reduce_distinct);
// -------------------
// new_app
#define AST_CALLBACK(_cb_name) \
static void _cb_name##_callback_static(Z3_theory th, Z3_ast a) \
{ \
CAMLparam0(); \
CAMLlocal3(cb, _a, user_data); \
_a = Val_ast(a); \
user_data = (value) Z3_theory_get_ext_data(th); \
cb = *(caml_named_value("apply_" #_cb_name)); \
callback2(cb, user_data, _a); \
CAMLreturn0; \
} \
AST_CALLBACK(new_app);
SET_CALLBACK(new_app);
// -------------------
// new_elem
AST_CALLBACK(new_elem);
SET_CALLBACK(new_elem);
// -------------------
// init_search
#define TH_CALLBACK(_cb_name) \
static void _cb_name##_callback_static(Z3_theory th) \
{ \
CAMLparam0(); \
CAMLlocal2(cb, user_data); \
user_data = (value) Z3_theory_get_ext_data(th); \
cb = *(caml_named_value("apply_" #_cb_name)); \
callback(cb, user_data); \
CAMLreturn0; \
} \
TH_CALLBACK(init_search);
SET_CALLBACK(init_search);
// -------------------
// push
TH_CALLBACK(push);
SET_CALLBACK(push);
TH_CALLBACK(pop);
SET_CALLBACK(pop);
TH_CALLBACK(restart);
SET_CALLBACK(restart);
TH_CALLBACK(reset);
SET_CALLBACK(reset);
#define FC_CALLBACK(_cb_name) \
static Z3_bool _cb_name##_callback_static(Z3_theory th) \
{ \
CAMLparam0(); \
CAMLlocal3(cb, r, user_data); \
user_data = (value) Z3_theory_get_ext_data(th); \
cb = *(caml_named_value("apply_" #_cb_name)); \
r = callback(cb, user_data); \
CAMLreturn (Bool_val(r) != 0); \
} \
FC_CALLBACK(final_check);
SET_CALLBACK(final_check);
#define AST_AST_CALLBACK(_cb_name) \
static void _cb_name##_callback_static(Z3_theory th, Z3_ast a, Z3_ast b) \
{ \
CAMLparam0(); \
CAMLlocal4(cb, _a, _b, user_data); \
_a = Val_ast(a); \
_b = Val_ast(b); \
user_data = (value) Z3_theory_get_ext_data(th); \
cb = *(caml_named_value("apply_" #_cb_name)); \
callback3(cb, user_data, _a, _b); \
CAMLreturn0; \
} \
AST_AST_CALLBACK(new_eq);
SET_CALLBACK(new_eq);
AST_AST_CALLBACK(new_diseq);
SET_CALLBACK(new_diseq);
#define AST_BOOL_CALLBACK(_cb_name) \
static void _cb_name##_callback_static(Z3_theory th, Z3_ast a, Z3_bool b) \
{ \
CAMLparam0(); \
CAMLlocal4(cb, _a, _b, user_data); \
_a = Val_ast(a); \
_b = Val_bool(b); \
user_data = (value) Z3_theory_get_ext_data(th); \
cb = *(caml_named_value("apply_" #_cb_name)); \
callback3(cb, user_data, _a, _b); \
CAMLreturn0; \
} \
AST_BOOL_CALLBACK(new_assignment);
SET_CALLBACK(new_assignment);
AST_CALLBACK(new_relevant);
SET_CALLBACK(new_relevant);