Adding external solver, calling program, pipe a parity game and parse…

… it's solution

_oasis

@@ -16,12 +16,13 @@ Plugins:     META
 BuildTools: ocamlbuild
 Library "pgsolver"
   Path:       src
-  BuildDepends: num, str, TCSLib, extlib, ocaml-sat-solvers, minisat
+  BuildDepends: num, str, TCSLib, extlib, ocaml-sat-solvers, minisat, unix, threads
   Modules: pgsolver/Basics, pgsolver/Info,
            paritygame/Paritygame, paritygame/Verification, paritygame/Univsolve, paritygame/Solvers,
            paritygame/Solverregistry, paritygame/Mdp, paritygame/Paritygamebitset, paritygame/Parsers,
            paritygame/Specialsolve, paritygame/Transformations,
-           solvers/Bigstep, solvers/Dominiondecomp, solvers/Fpiter, solvers/Genetic, solvers/Guessstrategy,
+           solvers/Bigstep, solvers/Dominiondecomp, solvers/Externalsolver,
+           solvers/Fpiter, solvers/Genetic, solvers/Guessstrategy,
            solvers/Localmodelchecker, solvers/Optstratimprov, solvers/Prioprom, solvers/Priopromdelay,
            solvers/Priopromplus, solvers/Priopromrecovery, solvers/Recursive, solvers/Satsolve, solvers/Smallprogress,
            solvers/Stratimpralgs, solvers/Stratimprdisc, solvers/Stratimprlocal, solvers/Stratimprlocal2,
@@ -35,7 +36,7 @@ Library "pgsolver"
            generators/Randomgame, generators/Laddergame, generators/Clusteredrandomgame, generators/Cliquegame,
            generators/Modelcheckerladder, generators/Recursiveladder, generators/Steadygame, generators/Jurdzinskigame,
            generators/modelchecking/Mucalculus,
-           generators/modelchecking/Elevators, generators/modelchecking/Roadworks, 
+           generators/modelchecking/Elevators, generators/modelchecking/Roadworks,
            generators/Towersofhanoi, generators/Langincl,
            generators/Recursivedullgame,
            generators/policyiter/Stratimprgen, generators/policyiter/Stratimprgenerators,

src/paritygame/solvers.ml

@@ -25,6 +25,7 @@ let fold_partial_solvers = Solverregistry.fold_partial_solvers
 let _ =
     Bigstep.register ();
     Dominiondecomp.register ();
+    Externalsolver.register ();
     Fpiter.register ();
     Genetic.register ();
     Guessstrategy.register ();

src/solvers/externalsolver.ml

@@ -0,0 +1,33 @@
+open Paritygame ;;
+open Parsers ;;
+open Univsolve ;;
+open Basics;;
+
+let pipe : in_channel -> out_channel -> unit = fun c_in c_out ->
+  let size = 4 * 1024 in
+  let buffer = Bytes.create size in
+  let eof = ref false in
+  while not !eof do
+    let len = input c_in buffer 0 size in
+    if len > 0
+    then output_string c_out (String.sub buffer 0 len)
+    else eof := true
+  done;;
+
+let solve' : Solverregistry.global_solver_factory = fun args game ->
+  let cmd = Array.get args 0 in
+  let (c_out, c_in, c_err) : in_channel * out_channel * in_channel = Unix.open_process_full cmd [||] in
+  let thread =  (Thread.create (fun _ -> pipe c_err stderr) ()) in
+  output_game c_in game;
+  close_out c_in;
+  let sol  = parse_solution c_out in
+  close_in c_out;
+  Thread.join thread;
+  let ret = Unix.close_process_full (c_out, c_in, c_err) in
+  ignore ret;
+  sol ;;
+let solve  : Solverregistry.global_solver_factory = fun args ->
+  universal_solve (universal_solve_init_options_verbose !universal_solve_global_options) (solve' args);;
+let register _ =
+  Solverregistry.register_solver_factory solve "external_solver_univ" "esuniv" "directly solve by calling an executable";
+  Solverregistry.register_solver_factory solve' "external_solver" "es" "directly solve by calling an executable";;

src/solvers/externalsolver.mli

@@ -0,0 +1,5 @@
+open Paritygame ;;
+
+val solve' : string array -> paritygame -> solution * strategy
+val solve : string array -> paritygame -> solution * strategy
+val register: unit -> unit