Compile and execute on windows

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 "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)
+                 |])
+         ]
       )

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