Anonymous avatar Anonymous committed 453587d

New Makefile that works on Mavericks with OCaml 4.01 and is more standard anyway

Comments (0)

Files changed (13)

src/api/ml/Makefile

 
 .PHONY: all install clean uninstall remove
 
-LIBS=z3.cmi z3.cmo z3.cmx z3.o libz3caml.a
-#dllz3caml.so z3caml.cma z3caml.cmxa z3caml.a 
+LIBS=z3.cmi z3.cma z3.cmxa libz3ml.a z3.a z3.cmo z3.cmx
 all : $(LIBS)
 
 install : META $(LIBS)
 	$(OCAMLFIND) install z3 META $(LIBS)
 
-# build the library
-#$(OCAMLMKLIB) -custom -verbose z3_stubs.o z3_theory_stubs.o z3.mli z3.ml -cclib -L$(OCAML_LOC) -cclib -lz3caml -cclib -lcamlidl -cclib -lz3 -ccopt -fopenmp -o z3caml
-$(LIBS) : z3_theory_stubs.o z3_stubs.o
-	ar rc ./libz3caml.a  z3_stubs.o z3_theory_stubs.o; ranlib ./libz3caml.a
-	$(OCAMLC) -custom -a -o z3caml.cma      -ccopt -fopenmp z3.mli z3.ml -cclib -lz3caml -cclib -lz3 -cclib -L/usr/local/lib/ocaml -cclib -lcamlidl 
-	$(OCAMLOPT) -a -o z3caml.cmxa      -ccopt -fopenmp z3.mli z3.ml -cclib -lz3caml -cclib -lz3 -cclib -L/usr/local/lib/ocaml -cclib -lcamlidl 
+# Build OCaml Library
+z3.cmi z3.cma z3.cmxa: libz3ml.a
+	ocamlc -c z3.mli
+	ocamlc -custom -cclib '-L/usr/local/lib -lz3 -L/usr/local/lib/ocaml -lcamlidl' -cclib "-L. -lz3ml" -I . z3.ml -a -o z3.cma -linkall
+	ocamlopt -cclib '-L/usr/local/lib -lz3 -L/usr/local/lib/ocaml -lcamlidl' -cclib "-L. -lz3ml" -I . z3.ml -a -o z3.cmxa -linkall
 
-# build the stubs
-z3_theory_stubs.o z3_stubs.o : z3_theory_stubs.c z3_stubs.c
-	$(OCAMLC) -verbose -c -I .. z3_theory_stubs.c z3_stubs.c > /dev/null 2>&1
+# Build Native Library
+libz3ml.a: z3_stubs.c z3_theory_stubs.c
+	clang -c -I /usr/local/lib/ocaml z3_stubs.c z3_theory_stubs.c
+	ar rcs libz3ml.a z3_stubs.o z3_theory_stubs.o
 
-# construct the meta file
+# Write the Meta File
 META :
-	@echo "version=\"$(Z3_VERSION)\"" > META
-	@echo "description=\"Z3 Theorem Prover\"" >> META
-	@echo "archive(byte)=\"z3.cmo\"" >> META
-	@echo "archive(native)=\"z3.cmx\"" >> META
-	@echo "linkopts(byte)=\"-custom -cclib -lz3caml -cclib -lz3 -cclib -L$(OCAML_LOC) -cclib -lcamlidl -cclib -fopenmp\"" >> META
-	@echo "linkopts=\"-cclib -lz3caml -cclib -lz3 -cclib -L$(OCAML_LOC) -cclib -lcamlidl -cclib -fopenmp\"" >> META
+	@echo "version = \"$(Z3_VERSION)\"" > META
+	@echo "description = \"Z3 Theorem Prover\"" >> META
+	@echo "archive(byte) = \"z3.cma\"" >> META
+	@echo "archive(native) = \"z3.cmxa\"" >> META
 
 clean :
-	-rm -rf META $(LIBS) z3_theory_stubs.o z3_stubs.o z3caml.a z3caml.cmxa z3caml.cma
+	-rm -rf META $(LIBS) z3_theory_stubs.o z3_stubs.o z3.o
 
 remove uninstall :
 	$(OCAMLFIND) remove z3

src/api/ml/build-lib.cmd

-@echo off
-
-call .\compile_mlapi.cmd ..\include ..\bin ..\bin

src/api/ml/build-test.cmd

-@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

src/api/ml/build.cmd

-@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

src/api/ml/clean.cmd

-@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

src/api/ml/cleantmp.cmd

-@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 *~

src/api/ml/compile_mlapi.cmd

-@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

src/api/ml/exec.cmd

-@echo off
-SETLOCAL
-set PATH=..\..\bin;%PATH%
-test_mlapi.exe
-ENDLOCAL

src/api/ml/generate_mlapi.cmd

-@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

src/api/ml/import.cmd

-@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

src/api/ml/test_mlapi.cmd

-@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

src/api/ml/update-ml-doc.cmd

-@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
 #include <fenv.h>
 #endif
 
-#ifndef _M_IA64
-#define USE_INTRINSICS
-#endif
+//#ifndef _M_IA64
+//#define USE_INTRINSICS
+//#endif
 
 #include<sstream>
 
 // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects
 // the x87 FPU, even when /arch:SSE2 is on. 
 // Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
-#include <emmintrin.h>
+//#include <emmintrin.h>
 
 
 hwf_manager::hwf_manager() :
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.