From f1b7e237f65ce06f94bfa13ba0ce0f9ff66accb1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 17 Jul 2020 16:17:49 +0200
Subject: [PATCH] Compile and execute on windows
---
colibri_for_bundle.ml | 72 ++++++++++++++++++++++++++++++-------------
compile_colibri.bat | 10 ++++++
compile_colibri.sh | 2 +-
3 files changed, 61 insertions(+), 23 deletions(-)
create mode 100644 compile_colibri.bat
diff --git a/colibri_for_bundle.ml b/colibri_for_bundle.ml
index 52c766d93..fe7a483ef 100644
--- a/colibri_for_bundle.ml
+++ b/colibri_for_bundle.ml
@@ -1,11 +1,13 @@
let coldir = Filename.dirname Sys.executable_name
-
let conf = ref "true"
let memlimit = ref 3000
let interpreter = ref false
+let get_steps = ref false
+let max_steps = ref 0
+let exec_cmd = ref ""
-let goal = ref "solve('smt_colibri.in')"
+let goal = ref ""
let path_sep = if Sys.win32 then ";" else ":"
@@ -40,51 +42,77 @@ let argspec =
acceptable values are (z3, z3-debug \
-- prints z3 inputs outputs to \
/tmp/{input,output}.smt2)";
+ "--get-steps", Arg.Set get_steps,
+ " output the number of steps at the end";
+ "--max-steps", Arg.Set_int max_steps,
+ " limit the number of steps";
"--interpreter-mode", Arg.Set interpreter,
- "run the prolog interactive interpreter";
+ " run the prolog interactive interpreter";
+ "--exec", Arg.Set_string exec_cmd,
+ " exec a command in interpreter mode"
]
let () = Arg.parse (Arg.align argspec)
- (fun s -> goal := Printf.sprintf "smt_solve('%s')" s)
+ (fun s -> goal := s)
"colibri <file>"
+let () = if !goal = "" then begin
+ print_endline "No input file given.";
+ exit 1
+ end
+
let eclipsedir = Filename.concat coldir "ECLIPSE"
let eclipselib = Filename.concat eclipsedir "lib"
let colibridir = Filename.concat coldir "COLIBRI"
+let arch = if Sys.win32 then "x86_64_nt" else "x86_64_linux"
+
let () = Unix.putenv "ECLIPSEDIR" eclipsedir
let () = Unix.putenv "FILTER_SMTLIB_FILE" (Filename.concat colibridir "filter_smtlib_file")
-let () = Unix.putenv "ARCH" "x86_64"
+let () = Unix.putenv "ARCH" arch
let extend_env var value =
match Unix.getenv var with
| exception Not_found -> Unix.putenv var value
| s -> Unix.putenv var (value^path_sep^s)
-let eclipseexe =
- if Sys.win32
- then
- Filename.concat eclipselib "x86_64_nt"
- else
- Filename.concat eclipselib "x86_64_linux"
+let eclipseexe = Filename.concat eclipselib arch
let () =
if Sys.win32
- then
- extend_env "PATH" eclipseexe
+ then begin
+ extend_env "PATH" eclipseexe;
+ extend_env "PATH" colibridir;
+ extend_env "PATH" (List.fold_left Filename.concat colibridir ["lib";"v7";arch])
+ end
else
extend_env "LD_LIBRARY_PATH" eclipseexe
+let quote_for_prolog f =
+ let s = Printf.sprintf "%S" f in
+ Printf.sprintf "'%s'" (String.sub s 1 (String.length s - 2))
+
let () =
let exe = Filename.concat eclipseexe "eclipse.exe" in
Unix.execv exe
- (Array.append
- [| exe;
- "-b"; Filename.concat colibridir "compile_flag";
- "-b"; Filename.concat colibridir "col_solve";
- "-g"; Printf.sprintf "%iM" !memlimit;
- |]
- (if !interpreter
- then [| |]
- else [| "-e"; Printf.sprintf "seed(0),%s,%s" !conf !goal |])
+ (Array.concat
+ [
+ [| exe;
+ "-b"; Filename.concat colibridir "compile_flag";
+ "-b"; Filename.concat colibridir "col_solve";
+ "-g"; Printf.sprintf "%iM" !memlimit;
+ |];
+ (if !exec_cmd = ""
+ then [| |]
+ else [| "-e"; !exec_cmd |])
+ ;
+ (if !interpreter
+ then [| |]
+ else [| "-e"; Printf.sprintf
+ "seed(0),%s,smt_solve%s(%s)"
+ !conf
+ (if !get_steps then "_stats" else "")
+ (quote_for_prolog !goal)
+ |])
+ ]
)
diff --git a/compile_colibri.bat b/compile_colibri.bat
new file mode 100644
index 000000000..029102276
--- /dev/null
+++ b/compile_colibri.bat
@@ -0,0 +1,10 @@
+@echo off
+
+set COLDIR=%~dp0
+set ECLIPSEDIR=%~dpnx1
+set PATH=%COLDIR%Src\COLIBRI;%COLDIR%Src\COLIBRI\lib\v7\x86_64_nt;%PATH%
+
+cd Src\COLIBRI
+
+@echo on
+"%ECLIPSEDIR%\lib\x86_64_nt\eclipse.exe" -g 3000M -b col_solve_dumpeco.pl -e halt
diff --git a/compile_colibri.sh b/compile_colibri.sh
index fa63f532c..d55a69de3 100755
--- a/compile_colibri.sh
+++ b/compile_colibri.sh
@@ -2,7 +2,7 @@
ARCH="x86_64_linux"
ECLIPSEDIR=$(pwd)/Bin/ECLIPSE_V7.0_45
-LD_LIBRARY_PATH="$ECLIPSEDIR/lib/$ARCH"
+LD_LIBRARY_PATH="$ECLIPSEDIR/lib/$ARCH:$LD_LIBRARY_PATH"
export ARCH ECLIPSEDIR LD_LIBRARY_PATH
--
GitLab