Better explanations in equivalence closure

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
 

msat.mlpack

@@ -10,8 +10,10 @@ Tseitin
 Tseitin_intf
 
 # Smt Modules
-Unionfind
+Cc
+Sig
 Smt
+Unionfind
 
 # Old modules
 #Arith

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

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

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

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
 

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
+  List.iter aux h.forbid;
   h
-  else
-    raise Unsat
 
 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

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

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)

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))