mirror of
https://github.com/Z3Prover/z3
synced 2025-04-26 18:45:33 +00:00
removed legacy ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
e29abefb12
commit
2f3ea1f39d
58 changed files with 0 additions and 26161 deletions
|
|
@ -1,14 +0,0 @@
|
|||
# to set ARGS, invoke as e.g.: $ make ARGS='-DUNSAFE_ERRORS -DLEAK_CONTEXTS'
|
||||
ARGS=
|
||||
|
||||
|
||||
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
|
||||
|
|
@ -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
|
||||
|
|
@ -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!
|
||||
|
|
@ -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!
|
||||
|
|
@ -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.
|
||||
|
|
@ -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.
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
@echo off
|
||||
|
||||
call .\compile_mlapi.cmd ..\include ..\bin ..\bin
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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 *~
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
@echo off
|
||||
SETLOCAL
|
||||
set PATH=..\..\bin;%PATH%
|
||||
test_mlapi.exe
|
||||
ENDLOCAL
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
quote(mli,"
|
||||
(**
|
||||
Summary: Return a string describing the given error code.
|
||||
*)
|
||||
val get_error_msg: context -> error_code -> string
|
||||
");
|
||||
|
|
@ -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;;
|
||||
");
|
||||
|
|
@ -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)
|
||||
");
|
||||
|
|
@ -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);
|
||||
}
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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();;
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -1,3 +0,0 @@
|
|||
# output lines of input in reverse order
|
||||
|
||||
1!G;h;$!d
|
||||
|
|
@ -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
|
||||
|
|
@ -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 () ;
|
||||
;;
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -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()
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
");
|
||||
|
|
@ -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
|
||||
|
||||
");
|
||||
|
|
@ -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
|
||||
|
||||
");
|
||||
|
|
@ -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
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -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);
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue