Sat Solver is broken.

.gitignore

@@ -1,17 +1,9 @@
 _build/
+tests/main
 *.annot
-*.cma
-*.cmi
-*.cmo
-*.cmx
-*.cmxa
-*.cmxs
-*.o
-*.a
 *.native
 *.log
 *.status
 .*.swp
-TAGS
 .session
 *.docdir

Makefile

@@ -3,8 +3,9 @@
 LOG=build.log
 COMP=ocamlbuild -log $(LOG) -use-ocamlfind -package num,zarith,unix -classic-display
 FLAGS=
-DIRS=-Is sat,smt,common
+DIRS=-Is sat,smt,common,util
 DOC=msat.docdir/index.html
+TEST=test.d.byte
 
 NAME=msat
 
@@ -18,6 +19,13 @@ $(LIB):
 doc:
 	$(COMP) $(FLAGS) $(DIRS) $(DOC)
 
+test: $(TEST)
+	./tests/main
+
+$(TEST): $(LIB)
+	$(COMP) $(FLAGS) $(DIRS) $(TEST)
+	cp $(TEST) tests/main && rm $(TEST)
+
 log:
 	cat _build/$(LOG) || true
 

sat/sat.ml

@@ -3,6 +3,8 @@
 module Fsat = struct
     exception Out_of_int
 
+    (* Until the constant true_ and false_ are not needed anymore,
+     * wa can't simply use sigend integers to represent literals *)
     type t = {
         (* Invariant : var >= 0 *)
         var : int;
@@ -65,10 +67,39 @@ module Tsat = struct
     let assume ~cs:_ _ _ _ = ()
 end
 
-module Sat = struct
+module Make(Dummy : sig end) = struct
     module SatSolver = Solver.Make(Fsat)(Stypes)(Exp)(Tsat)
 
+    type res =
+        | Sat
+        | Unsat
+
+    let _i = ref 0
+
     type atom = Fsat.t
     type state = SatSolver.t
 
+    let neg = Fsat.neg
+    let new_atom = Fsat.create
+
+    let hash = Fsat.hash
+    let equal = Fsat.equal
+    let compare = Fsat.compare
+
+    let print_atom = Fsat.print
+    let iter_atoms = Fsat.iter
+
+    let solve () =
+        try
+            SatSolver.solve ();
+            assert false
+        with
+        | SatSolver.Sat -> Sat
+        | SatSolver.Unsat _ -> Unsat
+
+    let assume l =
+        incr _i;
+        SatSolver.assume l !_i
+
+    let eval = SatSolver.eval
 end

sat/sat.mli

@@ -0,0 +1,22 @@
+(* Copyright 2014 Guillaume Bury *)
+
+module Make(Dummy: sig end) : sig
+    type atom
+    type state
+    type res = Sat | Unsat
+
+    val new_atom : unit -> atom
+    val neg : atom -> atom
+
+    val hash : atom -> int
+    val equal : atom -> atom -> bool
+    val compare : atom -> atom -> int
+
+    val print_atom : Format.formatter -> atom -> unit
+    val iter_atoms : (atom -> unit) -> unit
+
+    val solve : unit -> res
+    val eval : atom -> bool
+    val assume : atom list list -> unit
+end
+

tests/eval.ml

@@ -1,32 +0,0 @@
-(** Random tests *)
-
-open Aez
-
-let hs = Hstring.make
-
-module S = Smt.Make(struct end)
-
-let ty = Smt.Type.type_proc;; (hs "tau");;
-Smt.Symbol.declare (hs "a") [] ty;;
-Smt.Symbol.declare (hs "b") [] ty;;
-Smt.Symbol.declare (hs "c") [] ty;;
-
-let a = Smt.Term.make_app (hs "a") [];;
-let b = Smt.Term.make_app (hs "b") [];;
-let c = Smt.Term.make_app (hs "c") [];;
-
-S.assume ~id:0 Smt.Formula.(make_imply (make_pred ~sign:false a) (make_pred b));;
-S.assume ~id:1 Smt.Formula.(make_imply (make_pred b) (make_pred c));;
-S.assume ~id:2 Smt.Formula.(make_not (make_pred c));;
-
-try
-  S.check ();
-  Printf.printf "problem is sat, checking model...\n";
-  let v_a = S.eval a in
-  let v_b = S.eval b in
-  let v_c = S.eval c in
-  Printf.printf "a=%B, b=%B, c=%B\n" v_a v_b v_c;
-  assert (v_a && not v_b && not v_c);
-  ()
-with Smt.Unsat l ->
-  Printf.printf "problem deemed unsat, shouldn't be\n"

util/.merlin

@@ -0,0 +1,8 @@
+S ./
+S ../sat/
+S ../common/
+
+B ../_build/
+B ../_build/sat/
+B ../_build/smt/
+B ../_build/common/

util/test.ml

@@ -0,0 +1,33 @@
+
+module S = Sat.Make(struct end)
+
+let init () =
+    let v = Array.init 5 (fun _ -> S.new_atom ()) in
+    [ [
+        [v.(0); v.(1)];
+        [S.neg v.(0); v.(2)];
+        [S.neg v.(1); v.(2)];
+        [v.(3); v.(4)];
+        [S.neg v.(3); S.neg v.(2)];
+        [S.neg v.(4); S.neg v.(2)];
+    ] ]
+
+let print_assign fmt () =
+    S.iter_atoms (fun a ->
+        Format.fprintf fmt "%a -> %s,@ "
+        S.print_atom a
+        (if S.eval a then "true" else "false")
+    )
+
+let main () =
+    Format.printf "Hello World !@.";
+    List.iter (fun l ->
+        List.iter (fun c -> Format.printf "Adding : %a@."
+                    (fun _ -> List.iter (fun a -> Format.printf "%a " S.print_atom a)) c) l;
+        S.assume l;
+        match S.solve () with
+        | S.Sat -> Format.printf "Sat@\n%a@." print_assign ()
+        | S.Unsat -> Format.printf "Unsat@.") (init ());
+;;
+
+main ()