From 384bcb7270637427051eb1137a165019cb524a44 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 15 Nov 2014 18:39:19 +0100 Subject: [PATCH] Better explanations in equivalence closure --- Makefile | 2 +- msat.mlpack | 4 +- smt/cc.ml | 91 +++++++++++++++++++++++++++++++++++++++ smt/cc.mli | 15 +++++++ smt/sig.mli | 13 ++++++ smt/smt.ml | 31 +++++++------ smt/unionfind.ml | 20 +++------ smt/unionfind.mli | 13 +++--- tests/unsat/test-009.smt2 | 2 + util/smtlib/smtlib.ml | 4 +- 10 files changed, 161 insertions(+), 34 deletions(-) create mode 100644 smt/cc.ml create mode 100644 smt/cc.mli create mode 100644 smt/sig.mli create mode 100644 tests/unsat/test-009.smt2 diff --git a/Makefile b/Makefile index 26047ca6..cf1b8dfb 100644 --- a/Makefile +++ b/Makefile @@ -5,7 +5,7 @@ COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display FLAGS= DIRS=-Is sat,smt,util,util/smtlib DOC=msat.docdir/index.html -TEST=sat_solve.native smt_solve.native +TEST=sat_solve.native NAME=msat diff --git a/msat.mlpack b/msat.mlpack index 71440c17..06c0082b 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -10,8 +10,10 @@ Tseitin Tseitin_intf # Smt Modules -Unionfind +Cc +Sig Smt +Unionfind # Old modules #Arith diff --git a/smt/cc.ml b/smt/cc.ml new file mode 100644 index 00000000..3bc8569b --- /dev/null +++ b/smt/cc.ml @@ -0,0 +1,91 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Make(T : Sig.OrderedType) = struct + + module M = Map.Make(T) + module U = Unionfind.Make(T) + + exception Unsat of (T.t * T.t * (T.t list)) + + type t = { + repr : U.t; + expl : T.t M.t; + size : int M.t; + } + + let empty = { + repr = U.empty; + expl = M.empty; + size = M.empty; + } + + let map_find m v default = try M.find v m with Not_found -> default + let find_parent v m = map_find m v v + + let rev_root m root = + let rec aux m curr next = + if T.compare curr next = 0 then + m, curr + else + let parent = find_parent next m in + let m' = M.add next curr (M.remove curr m) in + aux m' next parent + in + aux m root (find_parent root m) + + let rec root m acc curr = + let parent = find_parent curr m in + if T.compare curr parent = 0 then + curr :: acc + else + root m (curr :: acc) parent + + let expl t a b = + let rec aux last = function + | x :: r, y :: r' when T.compare x y = 0 -> + aux (Some x) (r, r') + | l, l' -> begin match last with + | Some z -> List.rev_append (z :: l) l' + | None -> List.rev_append l l' + end + in + aux None (root t.expl [] a, root t.expl [] b) + + let add_eq_aux t i j = + if T.compare (U.find t.repr i) (U.find t.repr j) = 0 then + t + else + let m, old_root_i = rev_root t.expl i in + let m, old_root_j = rev_root m j in + let nb_i = map_find t.size old_root_i 0 in + let nb_j = map_find t.size old_root_j 0 in + if nb_i < nb_j then { + repr = t.repr; + expl = M.add i j m; + size = M.add j (nb_i + nb_j + 1) t.size; } + else { + repr = t.repr; + expl = M.add j i m; + size = M.add i (nb_i + nb_j + 1) t.size; } + + let add_eq t i j = + let t' = add_eq_aux t i j in + try + let u' = U.union t.repr i j in + { t' with repr = u' } + with U.Unsat (a, b) -> + raise (Unsat (a, b, expl t' a b)) + + let add_neq t i j = + try + let u' = U.forbid t.repr i j in + { t with repr = u' } + with U.Unsat (a, b) -> + raise (Unsat (a, b, expl t a b)) + + +end diff --git a/smt/cc.mli b/smt/cc.mli new file mode 100644 index 00000000..ef14aebc --- /dev/null +++ b/smt/cc.mli @@ -0,0 +1,15 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Make(T : Sig.OrderedType) : sig + type t + + exception Unsat of (T.t * T.t * (T.t list)) + + val empty : t + val add_eq : t -> T.t -> T.t -> t + val add_neq : t -> T.t -> T.t -> t +end diff --git a/smt/sig.mli b/smt/sig.mli new file mode 100644 index 00000000..d75d565b --- /dev/null +++ b/smt/sig.mli @@ -0,0 +1,13 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + + +module type OrderedType = sig + (** Signature for ordered types (mainly for use in Map.Make) *) + + type t + val compare : t -> t -> int +end diff --git a/smt/smt.ml b/smt/smt.ml index 45e084f2..02407d3f 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -62,7 +62,7 @@ module Tseitin = Tseitin.Make(Fsmt) module Tsmt = struct - module U = Unionfind.Make(String) + module CC = Cc.Make(String) type formula = Fsmt.t type proof = unit @@ -72,37 +72,44 @@ module Tsmt = struct get : int -> formula; push : formula -> formula list -> proof -> unit; } - type level = { - uf : U.t; - seen : formula list - } + type level = CC.t type res = | Sat of level | Unsat of formula list * proof - let dummy = { uf = U.empty; seen = [] } + let dummy = CC.empty let env = ref dummy let current_level () = !env + let to_clause (a, b, l) = + Log.debug 10 "Expl : %s; %s" a b; + List.iter (fun s -> Log.debug 10 " |- %s" s) l; + let rec aux acc = function + | [] | [_] -> acc + | x :: ((y :: _) as r) -> + aux (Fsmt.mk_eq x y :: acc) r + in + (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) + let assume s = try for i = s.start to s.start + s.length - 1 do + Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print (s.get i)); match s.get i with | Fsmt.Prop _ -> () | Fsmt.Equal (i, j) as f -> - env := { !env with seen = f :: !env.seen }; - env := { !env with uf = U.union !env.uf i j } + env := CC.add_eq !env i j | Fsmt.Distinct (i, j) as f -> - env := { !env with seen = f :: !env.seen }; - env := { !env with uf = U.forbid !env.uf i j } + env := CC.add_neq !env i j | _ -> assert false done; Sat (current_level ()) - with U.Unsat -> - Unsat (List.rev_map Fsmt.neg !env.seen, ()) + with CC.Unsat x -> + Log.debug 8 "Making explanation clause..."; + Unsat (to_clause x, ()) let backtrack l = env := l diff --git a/smt/unionfind.ml b/smt/unionfind.ml index 92764b95..fcf98da4 100644 --- a/smt/unionfind.ml +++ b/smt/unionfind.ml @@ -1,12 +1,7 @@ -module type OrderedType = sig - type t - val compare : t -> t -> int -end - (* Union-find Module *) -module Make(T : OrderedType) = struct - exception Unsat +module Make(T : Sig.OrderedType) = struct + exception Unsat of T.t * T.t type var = T.t module M = Map.Make(T) @@ -48,12 +43,11 @@ let possible h = let aux (a, b) = let ca = find h a in let cb = find h b in - ca != cb + if T.compare ca cb = 0 then + raise (Unsat (a, b)) in - if List.for_all aux h.forbid then - h - else - raise Unsat + List.iter aux h.forbid; + h let union_aux h x y = let cx = find h x in @@ -78,7 +72,7 @@ let forbid h x y = let cx = find h x in let cy = find h y in if cx = cy then - raise Unsat + raise (Unsat (x, y)) else { h with forbid = (x, y) :: h.forbid } end diff --git a/smt/unionfind.mli b/smt/unionfind.mli index 7416751a..29df1f71 100644 --- a/smt/unionfind.mli +++ b/smt/unionfind.mli @@ -1,11 +1,12 @@ -module type OrderedType = sig - type t - val compare : t -> t -> int -end +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) -module Make(T : OrderedType) : sig +module Make(T : Sig.OrderedType) : sig type t - exception Unsat + exception Unsat of T.t * T.t val empty : t val find : t -> T.t -> T.t val union : t -> T.t -> T.t -> t diff --git a/tests/unsat/test-009.smt2 b/tests/unsat/test-009.smt2 new file mode 100644 index 00000000..2fbc62df --- /dev/null +++ b/tests/unsat/test-009.smt2 @@ -0,0 +1,2 @@ +(assert (and (= a b) (or (= b c) (= b d)) (not (= a d)) (not (= a c)))) +(check-sat) diff --git a/util/smtlib/smtlib.ml b/util/smtlib/smtlib.ml index c018d01f..99d81c8e 100644 --- a/util/smtlib/smtlib.ml +++ b/util/smtlib/smtlib.ml @@ -72,7 +72,9 @@ let rec translate_term = function | "or", l -> T.make_or l | "xor" as s, l -> left_assoc s T.make_xor l | "=>" as s, l -> right_assoc s T.make_imply l - | _ -> raise Unknown_command + | _ -> + Format.printf "unknown : %s@." s; + raise Unknown_command end end | e -> (get_atom (translate_atom e))