From 6338f682df886aef475208dbfe0cd3e209085aa4 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 11 Nov 2014 12:25:16 +0100
Subject: [PATCH] Added unsat-core option in sat_solve Cleaned up a bit
 soler_types and added some doc

---
 TODO.md                  |  3 ---
 sat/res.ml               | 25 +++++++++++++++++++++++++
 sat/res_intf.ml          |  3 +++
 sat/sat.ml               |  6 +++++-
 sat/sat.mli              | 15 ++++++++++++---
 sat/solver.ml            |  3 +++
 sat/solver_types.ml      | 21 ++++++++++++++++-----
 sat/solver_types_intf.ml | 37 ++++++++++++++++++++++++-------------
 util/sat_solve.ml        | 16 ++++++++++++----
 9 files changed, 100 insertions(+), 29 deletions(-)

diff --git a/TODO.md b/TODO.md
index 2a7dcf30..6d19013c 100644
--- a/TODO.md
+++ b/TODO.md
@@ -2,7 +2,6 @@
 
 ## Main goals
 
-- Include cnf conversion in 'sat' library
 - Modify theories to allow passing bulk of assumed literals
     * Create shared "vector" (formulas/atoms ?)
     * Allow theory propagation
@@ -11,7 +10,6 @@
     * Clean Solver_types interface
 - Add proof output for smt/theories
     * Each theory brings its own proof output (tautologies), somehow
-- Add model extraction (at least for SAT)
 - Allow to plug one's code into boolean propagation
     * react upon propagation (possibly by propagating more, or side-effect)
     * more advanced/specific propagation (2-clauses)?
@@ -20,5 +18,4 @@
 
 ## Long term goals
 
-- unsat-core (easy from resolution proofs)
 - max-sat/max-smt
diff --git a/sat/res.ml b/sat/res.ml
index 30f32667..516add36 100644
--- a/sat/res.ml
+++ b/sat/res.ml
@@ -257,6 +257,29 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
     assert_can_prove_unsat c;
     return_proof (St.empty_clause, [])
 
+  (* Compute unsat-core *)
+  let compare_cl c d =
+    let rec aux = function
+    | [], [] -> 0
+    | a :: r, a' :: r' -> begin match compare_atoms a a' with
+      | 0 -> aux (r, r')
+      | x -> x
+    end
+    | _ :: _ , [] -> -1
+    | [], _ :: _ -> 1
+    in
+    aux (to_list c, to_list d)
+
+  let unsat_core proof =
+    let rec aux proof =
+      let p = proof () in
+      match p.step with
+      | Hypothesis | Lemma _ -> [p.conclusion]
+      | Resolution (proof1, proof2, _) ->
+              List.rev_append (aux proof1) (aux proof2)
+    in
+    List.sort_uniq compare_cl (aux proof)
+
   (* Print proof graph *)
   let _i = ref 0
   let new_id () = incr _i; "id_" ^ (string_of_int !_i)
@@ -284,6 +307,8 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
     else
       ()
 
+  (* We use a custom function instead of the functions in Solver_type,
+     so that atoms are sorted before printing. *)
   let print_clause fmt c = print_cl fmt (to_list c)
 
   let print_dot_rule opt f arg fmt cl =
diff --git a/sat/res_intf.ml b/sat/res_intf.ml
index a6635208..89ff6abf 100644
--- a/sat/res_intf.ml
+++ b/sat/res_intf.ml
@@ -30,6 +30,9 @@ module type S = sig
   val prove_unsat : clause -> proof
   (** Given a conflict clause [c], returns a proof of the empty clause. *)
 
+  val unsat_core : proof -> clause list
+  (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. *)
+
   val print_dot : Format.formatter -> proof -> unit
   (** Print the given proof in dot format on the given formatter. *)
 
diff --git a/sat/sat.ml b/sat/sat.ml
index 265c1c97..802e81c1 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -81,6 +81,7 @@ module Make(Dummy : sig end) = struct
   exception Bad_atom
 
   type atom = Fsat.t
+  type clause = Stypes.clause
   type proof = SatSolver.Proof.proof
 
   type res =
@@ -107,7 +108,6 @@ module Make(Dummy : sig end) = struct
   let equal = Fsat.equal
   let compare = Fsat.compare
 
-  let print_atom = Fsat.print
   let iter_atoms = Fsat.iter
 
   let solve () =
@@ -130,6 +130,10 @@ module Make(Dummy : sig end) = struct
     | None -> assert false
     | Some c -> SatSolver.Proof.prove_unsat c
 
+  let unsat_core = SatSolver.Proof.unsat_core
+
+  let print_atom = Fsat.print
+  let print_clause = Stypes.print_clause
   let print_proof = SatSolver.Proof.print_dot
 
 end
diff --git a/sat/sat.mli b/sat/sat.mli
index 06fc967e..fc17df9f 100644
--- a/sat/sat.mli
+++ b/sat/sat.mli
@@ -13,6 +13,9 @@ module Make(Dummy: sig end) : sig
   type atom = Fsat.t
   (** Type for atoms, i.e boolean literals. *)
 
+  type clause
+  (** Abstract type for clauses *)
+
   type proof
   (** Abstract type for resolution proofs *)
 
@@ -36,9 +39,6 @@ module Make(Dummy: sig end) : sig
   (** Usual hash and comparison functions. For now, directly uses
       [Pervasives] and [Hashtbl] builtins. *)
 
-  val print_atom : Format.formatter -> atom -> unit
-  (** Print the atom on the given formatter. *)
-
   val iter_atoms : (atom -> unit) -> unit
   (** Allows iteration over all atoms created (even if unused). *)
 
@@ -54,6 +54,15 @@ module Make(Dummy: sig end) : sig
   val get_proof : unit -> proof
   (** Returns the resolution proof found, if [solve] returned [Unsat]. *)
 
+  val unsat_core : proof -> clause list
+  (** Returns the unsat-core of the proof. *)
+
+  val print_atom : Format.formatter -> atom -> unit
+  (** Print the atom on the given formatter. *)
+
+  val print_clause : Format.formatter -> clause -> unit
+  (** Print the clause on the given formatter. *)
+
   val print_proof : Format.formatter -> proof -> unit
   (** Print the given proof in dot format. *)
 
diff --git a/sat/solver.ml b/sat/solver.ml
index b50fb34f..a80ac63e 100644
--- a/sat/solver.ml
+++ b/sat/solver.ml
@@ -155,6 +155,9 @@ module Make (F : Formula_intf.S)
     tatoms_queue = Queue.create ();
   }
 
+  let to_float i = float_of_int i
+  let to_int f = int_of_float f
+
   let f_weight i j =
     (Vec.get env.vars j).weight < (Vec.get env.vars i).weight
 
diff --git a/sat/solver_types.ml b/sat/solver_types.ml
index 103a2f24..54296111 100644
--- a/sat/solver_types.ml
+++ b/sat/solver_types.ml
@@ -39,7 +39,7 @@ module Make (F : Formula_intf.S) = struct
 
   and clause =
     { name : string;
-      mutable atoms : atom Vec.t ;
+      atoms : atom Vec.t ;
       mutable activity : float;
       mutable removed : bool;
       learnt : bool;
@@ -154,14 +154,25 @@ module Make (F : Formula_intf.S) = struct
     let cpt = ref 0 in
     fun () -> incr cpt; "C" ^ (string_of_int !cpt)
 
-  let to_float i = float_of_int i
-
-  let to_int f = int_of_float f
-
   let clear () =
     cpt_mk_var := 0;
     ma := MA.empty
 
+  (* Pretty printing for atoms and clauses *)
+  let print_atom fmt a = F.print fmt a.lit
+
+  let print_atoms fmt v =
+      print_atom fmt (Vec.get v 0);
+      if (Vec.size v) > 1 then begin
+          for i = 1 to (Vec.size v) - 1 do
+              Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i)
+          done
+      end
+
+  let print_clause fmt c =
+      Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms
+
+  (* Complete debug printing *)
   let sign a = if a==a.var.pa then "" else "-"
 
   let level a =
diff --git a/sat/solver_types_intf.ml b/sat/solver_types_intf.ml
index bcb22161..e0bcdca2 100644
--- a/sat/solver_types_intf.ml
+++ b/sat/solver_types_intf.ml
@@ -15,6 +15,8 @@ module type S = sig
   (** The signatures of clauses used in the Solver. *)
 
   type formula
+  type varmap
+  val ma : varmap ref
 
   type var = {
     vid : int;
@@ -38,7 +40,7 @@ module type S = sig
 
   and clause = {
     name : string;
-    mutable atoms : atom Vec.t;
+    atoms : atom Vec.t;
     mutable activity : float;
     mutable removed : bool;
     learnt : bool;
@@ -46,37 +48,46 @@ module type S = sig
   }
 
   and reason = clause option
-
   and premise = clause list
-
-  val cpt_mk_var : int ref
-  type varmap
-  val ma : varmap ref
+  (** Recursive types for literals (atoms) and clauses *)
 
   val dummy_var : var
   val dummy_atom : atom
   val dummy_clause : clause
-  val empty_clause : clause
+  (** Dummy values for use in vector dummys *)
 
-  val make_var : formula -> var * bool
+  val empty_clause : clause
+  (** The empty clause *)
 
   val add_atom : formula -> atom
+  (** Returns the atom associated with the given formula *)
+
+  val make_var : formula -> var * bool
+  (** Returns the variable linked with the given formula, and wether the atom associated with the formula
+      is [var.pa] or [var.na] *)
 
   val make_clause : string -> atom list -> int -> bool -> premise -> clause
+  (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *)
 
   val fresh_name : unit -> string
-
   val fresh_lname : unit -> string
-
   val fresh_dname : unit -> string
+  (** Fresh names for clauses *)
 
-  val to_float : int -> float
-
-  val to_int : float -> int
   val made_vars_info : var Vec.t -> int
+  (** Returns the number of variables created, and fill the given vector with the variables created.
+      Each variable is set in the vecotr with its [vid] as index. *)
+
   val clear : unit -> unit
+  (** Forget all variables cretaed *)
+
+  val print_atom : Format.formatter -> atom -> unit
+  val print_clause : Format.formatter -> clause -> unit
+  (** Pretty printing functions for atoms and clauses *)
 
   val pp_atom : Buffer.t -> atom -> unit
   val pp_clause : Buffer.t -> clause -> unit
+  (** Debug function for atoms and clauses (very verbose) *)
+
 end
 
diff --git a/util/sat_solve.ml b/util/sat_solve.ml
index aec6385a..e28716db 100644
--- a/util/sat_solve.ml
+++ b/util/sat_solve.ml
@@ -89,8 +89,11 @@ let rec print_cl fmt = function
     | [a] -> Sat.Fsat.print fmt a
     | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" Sat.Fsat.print a print_cl r
 
-let print_cnf cnf =
-    List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) cnf
+let print_lcl l =
+    List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l
+
+let print_lclause l =
+    List.iter (fun c -> Format.fprintf std "%a@\n" S.print_clause c) l
 
 (* Arguments parsing *)
 let file = ref ""
@@ -98,6 +101,7 @@ let p_cnf = ref false
 let p_assign = ref false
 let p_proof_check = ref false
 let p_proof_print = ref false
+let p_unsat_core = ref false
 let time_limit = ref 300.
 let size_limit = ref 1000_000_000.
 
@@ -150,6 +154,8 @@ let argspec = Arg.align [
     "<s>[kMGT] Sets the size limit for the sat solver";
     "-time", Arg.String (int_arg time_limit),
     "<t>[smhd] Sets the time limit for the sat solver";
+    "-u", Arg.Set p_unsat_core,
+    " Prints the unsat-core explanation of the unsat proof";
     "-v", Arg.Int (fun i -> Log.set_debug i),
     "<lvl> Sets the debug verbose level";
   ]
@@ -179,7 +185,7 @@ let main () =
   (* Interesting stuff happening *)
   let cnf = get_cnf () in
   if !p_cnf then
-      print_cnf cnf;
+      print_lcl cnf;
   S.assume cnf;
   match S.solve () with
   | S.Sat ->
@@ -190,7 +196,9 @@ let main () =
     print "Unsat";
     if !p_proof_check then begin
       let p = S.get_proof () in
-      print_proof p
+      print_proof p;
+      if !p_unsat_core then
+          print_lclause (S.unsat_core p)
     end
 
 let () =