OPAM Preparations

.gitignore

@@ -15,3 +15,7 @@ src/externalsat/satsolutionparser.mli
 _build
 SatConfig
 temp
+src/local/generatedsat.ml
+setup.data
+setup.log
+compile.include

README.md

@@ -10,62 +10,4 @@ It is developed and maintained by:
 - (c) Martin Lange, University of Kassel (http://carrick.fmv.informatik.uni-kassel.de/~mlange/)
 
 We currently support the following SAT Solvers:
-- zChaff (c) Princeton University (http://www.princeton.edu/~chaff/zchaff.html)
 - MiniSAT (c) Niklas Eén, Niklas Sörensson (http://minisat.se)
-- PicoSAT (c) JKU Linz (http://fmv.jku.at/picosat/)
-
-
-## Installation
-
-Install OCaml, OUnit, OPAM, Ocamlbuild.
-
-Then:
-```bash	
-git clone https://github.com/tcsprojects/satsolversforocaml.git
-cd satsolversforocaml
-make
-```
-
-
-## Usage
-
-- See the two test application for example use cases
-
-
-### Sat Solvers
-
-#### Picosat
-
-```bash	
-wget http://fmv.jku.at/picosat/picosat-965.tar.gz
-tar xzvf picosat-965.tar.gz
-cd picosat-965
-./configure.sh && make
-cd ..
-echo "PICOSAT = `pwd`/picosat-965/libpicosat.a" >> satsolversforocaml/SatConfig
-```
-#### ZChaff
-
-```bash	
-wget https://www.princeton.edu/~chaff/zchaff/zchaff.64bit.2007.3.12.zip
-tar xzvf zchaff.64bit.2007.3.12.zip 
-cd zchaff64
-make
-cd ..
-echo "ZCHAFF = `pwd`/zchaff64/libsat.a" >> satsolversforocaml/SatConfig
-```
-
-#### MiniSat
-
-```bash
-git clone https://github.com/niklasso/minisat
-cd minisat
-make
-cd ..
-echo "MINISAT = `pwd`/minisat/build/release/lib/libminisat.a" >> satsolversforocaml/SatConfig
-echo "MINISAT_INC = `pwd`/minisat" >> satsolversforocaml/SatConfig
-```
-
-If you're on a Mac and make fails, please have a look at these resources:
-- https://github.com/u-u-h/minisat/commit/e768238f8ecbbeb88342ec0332682ca8413a88f9
-- http://web.cecs.pdx.edu/~hook/logicw11/Assignments/MinisatOnMac.html

_oasis

@@ -0,0 +1,24 @@
+OASISFormat: 0.4
+Name:        SATSolversForOcaml
+Version:     0.1
+Synopsis:    This library contains an abstraction layer for integrating SAT
+  Solvers into OCaml.
+Description: This library contains an abstraction layer for integrating SAT
+  Solvers into OCaml.
+Authors:     Oliver Friedmann, Martin Lange
+Maintainers: Oliver Friedmann, Martin Lange
+OCamlVersion: >= 4.03.0
+License:     BSD-3-clause
+Homepage: https://github.com/tcsprojects/satsolversforocaml
+SourceRepository head
+  Type: git
+  Location: git://github.com/tcsprojects/satsolversforocaml.git
+  Browser: https://github.com/tcsprojects/satsolversforocaml
+Plugins:     META
+BuildTools: ocamlbuild
+Library "SATSolversForOcaml"
+  Path:       src
+  BuildDepends: minisat
+  InternalModules: minisat/Minisatwrapper, Satsolverregistry
+  Modules:    Satsolvers, Satwrapper, pseudosat/Pseudosatwrapper, preprocessor/Preprocessor,
+              externalsat/Externalsat, externalsat/Satsolutionlexer, externalsat/Satsolutionparser

_tags

@@ -1,9 +1,24 @@
-"tester": include
-"src": include
-"src/pseudosat": include
-"src/externalsat": include
-"src/preprocessor": include
-"src/picosat": include
-"src/zchaff": include
-"src/minisat": include
-"temp": include
+# OASIS_START
+# DO NOT EDIT (digest: a78bab6c57f18998f829519fda9cf2ed)
+# Ignore VCS directories, you can use the same kind of rule outside
+# OASIS_START/STOP if you want to exclude directories that contains
+# useless stuff for the build process
+true: annot, bin_annot
+<**/.svn>: -traverse
+<**/.svn>: not_hygienic
+".bzr": -traverse
+".bzr": not_hygienic
+".hg": -traverse
+".hg": not_hygienic
+".git": -traverse
+".git": not_hygienic
+"_darcs": -traverse
+"_darcs": not_hygienic
+# Library SATSolversForOcaml
+"src/SATSolversForOcaml.cmxs": use_SATSolversForOcaml
+<src/*.ml{,i,y}>: package(minisat)
+<src/externalsat/*.ml{,i,y}>: package(minisat)
+<src/preprocessor/*.ml{,i,y}>: package(minisat)
+<src/pseudosat/*.ml{,i,y}>: package(minisat)
+<src/minisat/*.ml{,i,y}>: package(minisat)
+# OASIS_STOP

deprecated/configure.ml

@@ -0,0 +1,147 @@
+print_string "FOOBAR\n\n\n";
+
+let parameters = [(
+    "PICOSAT", "Picosat Library file (usually called libpicosat.a)", ref "", ["Picosat"; "Picosatwrapper"], "picosatSolverFactory"
+); (
+    "ZCHAFF", "ZChaff Library file (usually called libsat.a)", ref "", ["Zchaff"; "Zchaffwrapper"], "zchaffSolverFactory"
+); (
+    "MINISAT", "Minisat Library file (usually called libminisat.a)", ref "", ["Minisat"; "Minisatwrapper"], "minisatSolverFactory"
+); (
+    "MINISAT_INC", "Minisat Inclusion directory (usually the Minisat root diredtory)", ref "", [], ""
+)] in
+
+(*
+let filename_config = "./SatConfig" in
+*)
+
+let filename_config = (Sys.getenv "HOME") ^ "/.satconfig" in
+
+
+(try (
+    let file_config = open_in filename_config in
+
+    let strings = Hashtbl.create 10 in
+
+    try
+      while true do
+        let line = input_line file_config in
+        let split = Array.of_list (String.split_on_char '=' line) in
+        if Array.length split = 2
+        then Hashtbl.add strings (String.trim split.(0)) (String.trim split.(1))
+      done
+    with End_of_file -> ();
+
+    close_in file_config;
+
+    List.iter (fun (key, _, value, _, _) ->
+        try
+            value := Hashtbl.find strings key
+        with Not_found -> ()
+    ) parameters
+) with Sys_error _ -> ());
+(*
+print_string "\nSATSolversForOcaml Configuration\n\n";
+
+List.iter (fun (key, desc, value, _) ->
+    print_string ("Configuring " ^ desc ^ "\n");
+    print_string ("  Current value: " ^ !value ^ " (empty to disable)\n");
+    print_string ("  Hit return to keep current value, 'null' to erase current value and path to set current value.\n");
+    print_string ("  " ^ key ^ ": ");
+    let new_value = String.trim (read_line ()) in
+    print_string ("\n");
+    if (new_value = "null")
+    then value := ""
+    else if (not (new_value = ""))
+    then value := new_value
+) parameters;
+
+let file_config = open_out filename_config in
+
+List.iter (fun (key, desc, value, _) ->
+    output_string file_config ("# " ^ desc ^ "\n");
+    if (not (!value = ""))
+    then output_string file_config (key ^ " = " ^ !value ^ "\n")
+    else output_string file_config ("# " ^ key ^ " = \n");
+    output_string file_config "\n"
+) parameters;
+
+close_out file_config;
+*)
+let filename_include = "./src/local/generatedsat.ml" in
+
+let file_include = open_out filename_include in
+
+List.iter (fun (_, _, value, includes, _) ->
+    List.iter (fun incl ->
+        if (not (!value = ""))
+        then output_string file_include ("open " ^ incl ^";;\n")
+        else output_string file_include ("(*open " ^ incl ^";;*)\n")
+    ) includes
+) parameters;
+output_string file_include "\nlet register_solvers register_solver =\n";
+List.iter (fun (_, _, value, _, factory) ->
+    if (not (!value = "") && not (factory = ""))
+    then output_string file_include ("    register_solver (new " ^ factory ^ ");\n")
+) parameters;
+
+close_out file_include;
+
+
+
+
+
+let stdlib = Sys.argv.(1) in (*`ocamlfind printconf stdlib`*)
+let pwd = Sys.getcwd () in
+
+
+let parameters = [(
+    ["PICOSAT"],
+    (fun (args) -> "gcc -c -g -I " ^ stdlib ^ " -o ./_build/PicoSATWrap.o ./src/picosat/backend/PicoSATWrap.cc"),
+    (fun (args) -> "-lflag " ^ pwd ^ "/_build/PicoSATWrap.o -lflag " ^ args.(0))
+); (
+    ["ZCHAFF"],
+    (fun (args) -> "gcc -c -g -I " ^ stdlib ^ " -o ./_build/ZchaffWrap.o ./src/zchaff/backend/ZchaffWrap.cc"),
+    (fun (args) -> "-ocamlopt 'ocamlopt -cc g++' -lflag " ^ pwd ^ "/_build/ZchaffWrap.o -lflag " ^ args.(0))
+); (
+    ["MINISAT"; "MINISAT_INC"],
+    (fun (args) -> "gcc -D__STDC_LIMIT_MACROS -c -I " ^ stdlib ^ " -I " ^ args.(1) ^ " -o ./_build/MiniSATWrap.o ./src/minisat/backend/MiniSATWrap.cc"),
+    (fun (args) -> "-ocamlopt 'ocamlopt -cc g++' -lflag " ^ pwd ^ "/_build/MiniSATWrap.o -lflag " ^ args.(0))
+)] in
+
+
+let filename_config = (Sys.getenv "HOME") ^ "/.satconfig" in
+let strings = Hashtbl.create 10 in
+
+(try (
+    let file_config = open_in filename_config in
+
+    try
+      while true do
+        let line = input_line file_config in
+        let split = Array.of_list (String.split_on_char '=' line) in
+        if Array.length split = 2
+        then Hashtbl.add strings (String.trim split.(0)) (String.trim split.(1))
+      done
+    with End_of_file -> ();
+
+    close_in file_config
+) with Sys_error _ -> ());
+
+let compilelines = ref [] in
+List.iter (fun (argkeys, f, g) ->
+    try
+        let argvalues = Array.of_list (List.map (Hashtbl.find strings) argkeys) in
+        let cmd = f argvalues in
+        print_string (cmd ^ "\n");
+        let _ = Sys.command(cmd) in
+        compilelines := (g argvalues)::!compilelines
+    with Not_found -> ()
+) parameters;
+
+let compileline = String.concat " " !compilelines in
+
+let filename_compileline = "./compile.include" in
+
+let file_compileline = open_out filename_compileline in
+output_string file_compileline compileline;
+close_out file_compileline;;