Home

minisat2 ocaml bindings

Mon, 03/29/2010 - 16:38 — abate

Release early, release often !

I've been working with Falvio Lerda to update the ocaml binding to minisat2.

The biggest change from Fabio's original version is the object oriented interface (mimicking the library c++ interface) and the addition of a couple of bindings.

You can find the git repo here.

I've also been working on the debian package and I've committed a draft package on git.debian.org.

A simple example is includes in the source where this is the main function.

(* Reads a given file and solves the instance. *)
let solve file =
  let solver = new solver in
  let vars = process_file solver file in
  match solver#solve with
  | Minisat.UNSAT -> printf "unsat\n"
  | Minisat.SAT   ->
      printf "sat\n";
      Hashtbl.iter
        (fun name v ->
          printf "  %s=%s\n"
            name
            (Minisat.string_of_value (solver#value_of v))
        )
        vars

Now I plan to finish the binding to minisat2 and then to attach minisat+. It should not be too difficult, if anyone is interested to lend me a hand, drop me a line.

No votes yet