From 3c235e259da6f57b098b754b5f60deadc0390df7 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 1 Nov 2014 02:12:17 +0100 Subject: [PATCH] Sat Solver is broken. --- .gitignore | 10 +--------- Makefile | 10 +++++++++- sat/sat.ml | 33 ++++++++++++++++++++++++++++++++- sat/sat.mli | 22 ++++++++++++++++++++++ tests/eval.ml | 32 -------------------------------- util/.merlin | 8 ++++++++ util/test.ml | 33 +++++++++++++++++++++++++++++++++ 7 files changed, 105 insertions(+), 43 deletions(-) create mode 100644 sat/sat.mli delete mode 100644 tests/eval.ml create mode 100644 util/.merlin create mode 100644 util/test.ml diff --git a/.gitignore b/.gitignore index 3481c37b..06560aa5 100644 --- a/.gitignore +++ b/.gitignore @@ -1,17 +1,9 @@ _build/ +tests/main *.annot -*.cma -*.cmi -*.cmo -*.cmx -*.cmxa -*.cmxs -*.o -*.a *.native *.log *.status .*.swp -TAGS .session *.docdir diff --git a/Makefile b/Makefile index d7e31f45..09f2eae7 100644 --- a/Makefile +++ b/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 diff --git a/sat/sat.ml b/sat/sat.ml index 82e1950c..57483417 100644 --- a/sat/sat.ml +++ b/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 diff --git a/sat/sat.mli b/sat/sat.mli new file mode 100644 index 00000000..b20982d9 --- /dev/null +++ b/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 + diff --git a/tests/eval.ml b/tests/eval.ml deleted file mode 100644 index 5e8676ca..00000000 --- a/tests/eval.ml +++ /dev/null @@ -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" diff --git a/util/.merlin b/util/.merlin new file mode 100644 index 00000000..daa95b7d --- /dev/null +++ b/util/.merlin @@ -0,0 +1,8 @@ +S ./ +S ../sat/ +S ../common/ + +B ../_build/ +B ../_build/sat/ +B ../_build/smt/ +B ../_build/common/ diff --git a/util/test.ml b/util/test.ml new file mode 100644 index 00000000..4608e5e6 --- /dev/null +++ b/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 ()