Merge branch 'colibri_ocaml_wrapper' into 'master'

Add a wrapper for colibri in ocaml (cross-platform)

See merge request adacore/colibri!7

.gitlab-ci.yml

@@ -4,6 +4,8 @@ tests_without_recompilation:
   #Eclipse Prolog compilation of COLIBRI
    - ./compile_colibri.sh
   #Bundle in bundle directory
+   - apt-get update
+   - apt-get install -y ocaml-nox
    - ./bundle.sh bundle
    - cp -ra Bin/ECLIPSE_V7.0_45/ bundle/ECLIPSE/
   #Test

bundle.sh

@@ -8,5 +8,6 @@ cp -ra Src/COLIBRI/lib/v7 $PREFIX/COLIBRI/lib/
 cp -ra Src/COLIBRI/col_solve.eco Src/COLIBRI/filter_smtlib_file Src/COLIBRI/filter_smtlib_file.exe $PREFIX/COLIBRI/
 cp -ra compile_flag.pl $PREFIX/COLIBRI/
 cp -ra version $PREFIX/
-cp -ra colibri_for_bundle.sh $PREFIX/colibri
+ocamlopt unix.cmxa -o $PREFIX/colibri.exe colibri_for_bundle.ml
+cp $PREFIX/colibri.exe $PREFIX/colibri
 chmod u+x $PREFIX/colibri

colibri_for_bundle.ml

+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 ""
+
+let path_sep = if Sys.win32 then ";" else ":"
+
+let print_version () =
+  let cin = open_in (Filename.concat coldir "version") in
+  let s = input_line cin in
+  close_in cin;
+  Printf.printf "%s%!" s;
+  exit 0
+
+let add_to_conf s =
+  conf := (!conf)^","^s
+
+let argspec =
+  ["--version", Arg.Unit print_version, " print version";
+   "--memlimit", Arg.Set_int memlimit, " set memlimit in Megabyte (default 3000)";
+   "--conf", Arg.String add_to_conf, " evaluate the prolog expression (default true)";
+   "--per-call-simplex-timeout",
+   Arg.Int (fun sec -> add_to_conf (Printf.sprintf "set_simplex_timeout(%i)" sec)) ,
+   " timeout for each call of the rational simplex";
+   "--delay-simplex-deactivation",
+   Arg.Int (fun sec -> add_to_conf (Printf.sprintf "setval(simplex_delay_deactivation,%i)" sec)),
+   " stop delta and simplex algorithm after the given time (0 always activated)";
+   "--external-simplex",
+   Arg.Symbol (["z3";"z3-debug"],
+               (fun s -> Unix.putenv "COLIBRI_USE_SOLVER" s;
+                 let path = (try Unix.getenv "PATH" with Not_found -> "") in
+                 Unix.putenv "PATH" ((Filename.concat coldir "qf_lra_solver")^path_sep^path)
+               )),
+   " use the specified external solver \
+    (QF_LRA) instead of internal simplex \
+    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";
+   "--exec", Arg.Set_string exec_cmd,
+   " exec a command in interpreter mode"
+  ]
+
+let () = Arg.parse (Arg.align argspec)
+    (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" 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 = Filename.concat eclipselib arch
+
+let () =
+  if Sys.win32
+  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.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)
+                 |])
+         ]
+      )

compile_colibri.bat

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

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
 

merlin

+PKG unix