Progressing. Conflict clause computing is broken

.merlin

@@ -1,12 +1,10 @@
 S sat
 S smt
 S solver
-S mcsolver
 S util
 
 B _build/
 B _build/sat
 B _build/smt
 B _build/solver
-B _build/mcsolver
 B _build/util

Makefile

@@ -3,7 +3,7 @@
 LOG=build.log
 COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display
 FLAGS=
-DIRS=-Is mcsolver,solver,sat,smt,util,util/smtlib
+DIRS=-Is solver,sat,smt,util,util/smtlib
 DOC=msat.docdir/index.html
 TEST=sat_solve.native bench_stats.native
 

_tags

@@ -3,7 +3,6 @@
 <smt/*.cmx>: for-pack(Msat), package(zarith)
 <sat/*.cmx>: for-pack(Msat)
 <solver/*.cmx>: for-pack(Msat)
-<mcsolver/*.cmx>: for-pack(Msat)
 
 # enable stronger inlining everywhere
 <util/{vec,hashcons,hstring,iheap}.cmx>: inline(15)

msat.mlpack

@@ -12,6 +12,7 @@ Plugin_intf
 
 # Auxiliary modules
 Res
+Mcproof
 Tseitin
 Tseitin_intf
 

solver/.merlin

@@ -1,7 +1,6 @@
 S ./
-S ../common/
+S ../util/
 
 B ../_build/
-B ../_build/sat/
+B ../_build/solver/
 B ../_build/util/
-B ../_build/common/

solver/mcproof.ml

@@ -0,0 +1,375 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+module type S = Res_intf.S
+
+module Make(St : Mcsolver_types.S) = struct
+
+  (* Type definitions *)
+  type lemma = St.proof
+  type clause = St.clause
+  type atom = St.atom
+  type int_cl = clause * St.atom list
+
+  type node =
+    | Assumption
+    | Lemma of lemma
+    | Resolution of atom * int_cl * int_cl
+    (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *)
+
+  exception Insuficient_hyps
+  exception Resolution_error of string
+
+  (* Proof graph *)
+  let hash_cl cl =
+    Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl)
+
+  let equal_cl cl_c cl_d =
+    try
+      List.for_all2 (==) cl_c cl_d
+    with Invalid_argument _ ->
+      false
+
+  module H = Hashtbl.Make(struct
+      type t = St.atom list
+      let hash = hash_cl
+      let equal = equal_cl
+    end)
+  let proof : node H.t = H.create 1007;;
+  let unit_hyp : (clause * St.atom list) H.t = H.create 37;;
+
+  (* Misc functions *)
+  let equal_atoms a b = St.(a.aid) = St.(b.aid)
+  let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
+
+  let merge = List.merge compare_atoms
+
+  let _c = ref 0
+  let fresh_pcl_name () = incr _c; "P" ^ (string_of_int !_c)
+
+  (* Printing functions *)
+  let rec print_cl fmt = function
+    | [] -> Format.fprintf fmt "[]"
+    | [a] -> St.print_atom fmt a
+    | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" St.print_atom a print_cl r
+
+  (* Compute resolution of 2 clauses *)
+  let resolve l =
+    let rec aux resolved acc = function
+      | [] -> resolved, acc
+      | [a] -> resolved, a :: acc
+      | a :: b :: r ->
+        if equal_atoms a b then
+          aux resolved (a :: acc) r
+        else if equal_atoms St.(a.neg) b then
+          aux (St.(a.var.tag.pa) :: resolved) acc r
+        else
+          aux resolved (a :: acc) (b :: r)
+    in
+    let resolved, new_clause = aux [] [] l in
+    resolved, List.rev new_clause
+
+  let to_list c =
+    let v = St.(c.atoms) in
+    let l = ref [] in
+    for i = 0 to Vec.size v - 1 do
+      l := (Vec.get v i) :: !l
+    done;
+    let l, res = resolve (List.sort_uniq compare_atoms !l) in
+    if l <> [] then
+      raise (Resolution_error "Input cause is a tautology");
+    res
+
+  (* Adding hyptoheses *)
+  let is_unit_hyp = function
+    | [a] -> St.(a.var.level = 0 && a.var.tag.reason = Bcp None && a.var.tag.vpremise <> History [])
+    | _ -> false
+
+  let make_unit_hyp a =
+    let aux a = St.(make_clause (fresh_name ()) [a] 1 false (History [])) in
+    if St.(a.is_true) then
+      aux a
+    else if St.(a.neg.is_true) then
+      aux St.(a.neg)
+    else
+      assert false
+
+  let unit_hyp a =
+    let a = St.(a.var.tag.pa) in
+    try
+      H.find unit_hyp [a]
+    with Not_found ->
+      let c = make_unit_hyp a in
+      let cl = to_list c in
+      H.add unit_hyp [a] (c, cl);
+      (c, cl)
+
+  let is_proved (c, cl) =
+    if H.mem proof cl then
+      true
+    else if is_unit_hyp cl || not St.(c.learnt) then begin
+      H.add proof cl Assumption;
+      true
+    end else match St.(c.cpremise) with
+      | St.Lemma p -> H.add proof cl (Lemma p); true
+      | St.History _ -> false
+
+  let is_proven c = is_proved (c, to_list c)
+
+  let add_res (c, cl_c) (d, cl_d) =
+    Log.debug 7 "  Resolving clauses :";
+    Log.debug 7 "    %a" St.pp_clause c;
+    Log.debug 7 "    %a" St.pp_clause d;
+    assert (is_proved (c, cl_c));
+    assert (is_proved (d, cl_d));
+    let l = merge cl_c cl_d in
+    let resolved, new_clause = resolve l in
+    match resolved with
+    | [] -> raise (Resolution_error "No literal to resolve over")
+    | [a] ->
+      H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d)));
+      let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause) true St.(History [c; d]) in
+      Log.debug 5 "New clause : %a" St.pp_clause new_c;
+      new_c, new_clause
+    | _ -> raise (Resolution_error "Resolved to a tautology")
+
+  let rec diff_learnt acc l l' =
+    match l, l' with
+    | [], _ -> l' @ acc
+    | a :: r, b :: r' ->
+      if equal_atoms a b then
+        diff_learnt acc r r'
+      else
+        diff_learnt (b :: acc) l r'
+    | _ -> raise (Resolution_error "Impossible to derive correct clause")
+
+  let clause_unit a = match St.(a.var.level, a.var.tag.reason) with
+    | 0, St.Bcp Some c -> c, to_list c
+    | 0, St.Bcp None ->
+      let c, cl = unit_hyp a in
+      if is_proved (c, cl) then
+        c, cl
+      else
+        assert false
+    | _ ->
+      raise (Resolution_error "Could not find a reason needed to resolve")
+
+  let add_clause c cl l = (* We assume that all clauses in l are already proved ! *)
+    match l with
+    | a :: r ->
+      Log.debug 5 "Resolving (with history) %a" St.pp_clause c;
+      let temp_c, temp_cl = List.fold_left add_res a r in
+      Log.debug 10 " Switching to unit resolutions";
+      let new_c, new_cl = (ref temp_c, ref temp_cl) in
+      while not (equal_cl cl !new_cl) do
+        let unit_to_use = diff_learnt [] cl !new_cl in
+        let unit_r = List.map (fun a -> clause_unit a) unit_to_use in
+        let temp_c, temp_cl = List.fold_left add_res (!new_c, !new_cl) unit_r in
+        new_c := temp_c;
+        new_cl := temp_cl;
+      done
+    | _ -> assert false
+
+  let need_clause (c, cl) =
+    if is_proved (c, cl) then
+      []
+    else
+      match St.(c.cpremise) with
+      | St.History l -> l
+      | St.Lemma _ -> assert false
+
+  let rec do_clause = function
+    | [] -> ()
+    | c :: r ->
+      let cl = to_list c in
+      match need_clause (c, cl) with
+      | [] -> do_clause r
+      | history ->
+        let history_cl = List.rev_map (fun c -> c, to_list c) history in
+        let to_prove = List.filter (fun (c, cl) -> not (is_proved (c, cl))) history_cl in
+        let to_prove = (List.rev_map fst to_prove) in
+        begin match to_prove with
+          | [] ->
+            add_clause c cl history_cl;
+            do_clause r
+          | _ -> do_clause (to_prove @ (c :: r))
+        end
+
+  let prove c =
+    Log.debug 3 "Proving : %a" St.pp_clause c;
+    do_clause [c];
+    Log.debug 3 "Proved : %a" St.pp_clause c
+
+  let rec prove_unsat_cl (c, cl) = match cl with
+    | [] -> true
+    | a :: r ->
+      Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
+      let d = match St.(a.var.level, a.var.tag.reason) with
+        | 0, St.Bcp Some d -> d
+        | 0, St.Bcp None ->
+          let d, cl_d = unit_hyp a in
+          if is_proved (d, cl_d) then d else raise Exit
+        | _ -> raise Exit
+      in
+      prove d;
+      let cl_d = to_list d in
+      prove_unsat_cl (add_res (c, cl) (d, cl_d))
+
+  let prove_unsat_cl c =
+    try
+      prove_unsat_cl c
+    with Exit ->
+      false
+
+  let learn v =
+    Vec.iter (fun c -> Log.debug 15 "history : %a" St.pp_clause c) v;
+    Vec.iter prove v
+
+  let assert_can_prove_unsat c =
+    Log.debug 1 "=================== Proof =====================";
+    prove c;
+    if not (prove_unsat_cl (c, to_list c)) then
+      raise Insuficient_hyps
+
+  (* Interface exposed *)
+  type proof_node = {
+    conclusion : clause;
+    step : step;
+  }
+  and proof = unit -> proof_node
+  and step =
+    | Hypothesis
+    | Lemma of lemma
+    | Resolution of proof * proof * atom
+
+  let rec return_proof (c, cl) () =
+    Log.debug 8 "Returning proof for : %a" St.pp_clause c;
+    let st = match H.find proof cl with
+      | Assumption -> Hypothesis
+      | Lemma l -> Lemma l
+      | Resolution (a, cl_c, cl_d) ->
+        Resolution (return_proof cl_c, return_proof cl_d, a)
+    in
+    { conclusion = c; step = st }
+
+  let prove_unsat c =
+    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)
+
+  let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;;
+  let c_id c =
+    try
+      snd (Hashtbl.find ids c)
+    with Not_found ->
+      let id = new_id () in
+      Hashtbl.add ids c (false, id);
+      id
+
+  let clear_ids () =
+    Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids
+
+  let is_drawn c =
+    ignore (c_id c);
+    fst (Hashtbl.find ids c)
+
+  let has_drawn c =
+    if not (is_drawn c) then
+      let b, id = Hashtbl.find ids c in
+      Hashtbl.replace ids c (true, id)
+    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 =
+    Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %s %s>%a</TABLE>>];@\n"
+      (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" opt f arg
+
+  let print_dot_edge id_c fmt id_d =
+    Format.fprintf fmt "%s -> %s;@\n" id_c id_d
+
+  let print_res_atom id fmt a =
+    Format.fprintf fmt "%s [label=\"%a\"]" id St.print_atom a
+
+  let print_res_node concl p1 p2 fmt atom =
+    let id = new_id () in
+    Format.fprintf fmt "%a;@\n%a%a%a"
+      (print_res_atom id) atom
+      (print_dot_edge (c_id concl)) id
+      (print_dot_edge id) (c_id p1)
+      (print_dot_edge id) (c_id p2)
+
+  let color s = match s.[0] with
+      | 'E' -> "BGCOLOR=\"GREEN\""
+      | 'L' -> "BGCOLOR=\"GREEN\""
+      | _ -> "BGCOLOR=\"GREY\""
+
+  let rec print_dot_proof fmt p =
+    if not (is_drawn p.conclusion) then begin
+      has_drawn p.conclusion;
+      match p.step with
+      | Hypothesis ->
+        let aux fmt () =
+          Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD>Hypothesis</TD><TD>%s</TD></TR>"
+            print_clause p.conclusion St.(p.conclusion.name)
+        in
+        print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
+      | Lemma _ ->
+        let aux fmt () =
+          Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"YELLOW\">Lemma</TD><TD>%s</TD></TR>"
+            print_clause p.conclusion St.(p.conclusion.name)
+        in
+        print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
+      | Resolution (proof1, proof2, a) ->
+        let aux fmt () =
+          Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD>%s</TD><TD>%s</TD></TR>"
+            print_clause p.conclusion
+            "Resolution" St.(p.conclusion.name)
+        in
+        let p1 = proof1 () in
+        let p2 = proof2 () in
+        Format.fprintf fmt "%a%a%a%a"
+          (print_dot_rule (color p.conclusion.St.name) aux ()) p.conclusion
+          (print_res_node p.conclusion p1.conclusion p2.conclusion) a
+          print_dot_proof p1
+          print_dot_proof p2
+    end
+
+  let print_dot fmt proof =
+    clear_ids ();
+    Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ())
+
+end
+

solver/mcproof.mli

@@ -0,0 +1,11 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+module type S = Res_intf.S
+
+module Make : functor (St : Mcsolver_types.S)
+  -> S with type atom = St.atom and type clause = St.clause and type lemma = St.proof
+(** Functor to create a module building proofs from a sat-solver unsat trace. *)

solver/mcsolver.ml

@@ -14,7 +14,7 @@ module Make (E : Expr_intf.S)
     (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct
 
   module St = Mcsolver_types.Make(E)(Th)
-  (* module Proof = Res.Make(St) *)
+  module Proof = Mcproof.Make(St)
 
   open St
 
@@ -30,11 +30,6 @@ module Make (E : Expr_intf.S)
     ul_learnt : int; (* number of learnt clauses *)
   }
 
-  (* Type for trail elements *)
-  type trail_elt =
-      | Semantic of semantic var
-      | Boolean of atom
-
   (* Singleton type containing the current state *)
   type env = {
 
@@ -56,7 +51,7 @@ module Make (E : Expr_intf.S)
     mutable var_inc : float;
     (* increment for variables' activity *)
 
-    trail : trail_elt Vec.t;
+    trail : (semantic var, atom) Either.t Vec.t;
     (* decision stack + propagated atoms *)
 
     trail_lim : int Vec.t;
@@ -127,7 +122,7 @@ module Make (E : Expr_intf.S)
     learnts = Vec.make 0 dummy_clause; (*updated during parsing*)
     clause_inc = 1.;
     var_inc = 1.;
-    trail = Vec.make 601 (Boolean dummy_atom);
+    trail = Vec.make 601 (Either.mk_right dummy_atom);
     trail_lim = Vec.make 601 (-1);
     user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0};
     qhead = 0;
@@ -161,17 +156,20 @@ module Make (E : Expr_intf.S)
   let to_float i = float_of_int i
   let to_int f = int_of_float f
 
-  let get_elt_weight = function
+  (* Accessors for variables *)
-      | Term v -> v.weight
+  let get_var_id v = v.vid
-      | Formula v -> v.weight
+  let get_var_level v = v.level
+  let get_var_weight v = v.weight
 
-  let set_elt_weight e w = match e with
+  let set_var_weight v w = v.weight <- w
-      | Term v -> v.weight <- w
+  let set_var_level v l = v.level <- l
-      | Formula v -> v.weight <- w
 
-  let get_elt_level = function
+  let get_elt_id e = Either.destruct e get_var_id get_var_id
-      | Term v -> v.level
+  let get_elt_weight e = Either.destruct e get_var_weight get_var_weight
-      | Formula v -> v.level
+  let get_elt_level e = Either.destruct e get_var_level get_var_level
+
+  let set_elt_weight e = Either.destruct e set_var_weight set_var_weight
+  let set_elt_level e = Either.destruct e set_var_level set_var_level
 
   let f_weight i j =
     get_elt_weight (St.get_var j) < get_elt_weight (St.get_var i)
@@ -180,13 +178,12 @@ module Make (E : Expr_intf.S)
     get_elt_level (St.get_var i) < 0
 
   (* Var/clause activity *)
-  let rec insert_var_order = function
+  let rec insert_var_order e = Either.destruct e
-      | Term v ->
+      (fun v -> Iheap.insert f_weight env.order v.vid)
-              Iheap.insert f_weight env.order v.vid
+      (fun v ->
-      | Formula v ->
+          Iheap.insert f_weight env.order v.vid;
-              Iheap.insert f_weight env.order v.vid;
+          Th.iter_assignable (fun t ->
-              Th.iter_assignable
+              insert_var_order (Either.mk_left (St.add_term t))) v.tag.pa.lit)
-                (fun t -> insert_var_order (Term (St.add_term t))) v.tag.pa.lit
 
   let var_decay_activity () =
     env.var_inc <- env.var_inc *. env.var_decay
@@ -263,15 +260,15 @@ module Make (E : Expr_intf.S)
       env.qhead <- Vec.get env.trail_lim lvl;
       env.tatoms_qhead <- env.qhead;
       for c = Vec.size env.trail - 1 downto env.qhead do
-        match Vec.get env.trail c with
+        Either.destruct (Vec.get env.trail c)
-        | Boolean a ->
+        (fun a -> ())
+        (fun a ->
           a.is_true <- false;
           a.neg.is_true <- false;
           a.var.level <- -1;
           a.var.tag.reason <- Bcp None;
           a.var.tag.vpremise <- History [];
-          insert_var_order (Formula a.var)
+          insert_var_order (Either.mk_right a.var))
-        | Semantic a -> ()
       done;
       Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *)
       Vec.shrink env.trail ((Vec.size env.trail) - env.qhead);
@@ -296,24 +293,58 @@ module Make (E : Expr_intf.S)
     a.var.level <- lvl;
     a.var.tag.reason <- reason;
     Log.debug 8 "Enqueue: %a" pp_atom a;
-    Vec.push env.trail (Boolean a)
+    Vec.push env.trail (Either.mk_right a)
 
   let enqueue_assign v value lvl =
     v.tag.assigned <- Some value;
     v.level <- lvl;
-    Vec.push env.trail (Semantic v)
+    Log.debug 5 "Enqueue: %a" St.pp_semantic_var v;
+    Vec.push env.trail (Either.mk_left v)
 
   (* conflict analysis *)
+  let max_lvl_atoms l =
+      List.fold_left (fun (max_lvl, acc) a ->
+          if a.var.level = max_lvl then (max_lvl, a :: acc)
+          else if a.var.level > max_lvl then (a.var.level, [a])
+          else (max_lvl, acc)) (0, []) l
+
   let analyze c_clause =
-    let pathC  = ref 0 in
+    let tr_ind  = ref (Vec.size env.trail) in
-    let learnt = ref [] in
+    let blevel  = ref 0 in
-    let cond   = ref true in
+    let is_uip  = ref false in
-    let blevel = ref 0 in
+    let c       = ref (Proof.to_list c_clause) in
-    let seen   = ref [] in
-    let c      = ref c_clause in
-    let tr_ind = ref (Vec.size env.trail - 1) in
-    let size   = ref 1 in
     let history = ref [] in
+
+    let is_semantic a = match a.var.tag.reason with
+        | Semantic _ -> true
+        | _ -> false
+    in
+
+    try while true do
+        let l, atoms = max_lvl_atoms !c in
+        match atoms with
+        | [] |  _ :: [] ->
+                blevel := -1;
+                raise Exit
+        | _ when List.for_all is_semantic atoms ->
+                blevel := l - 1;
+                raise Exit
+        | _ ->
+                decr tr_ind;
+                Either.destruct (Vec.get env.trail !tr_ind)
+                (fun v -> ())
+                (fun a -> match a.var.tag.reason with
+                    | Bcp (Some d) ->
+                            let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in
+                            begin match tmp with
+                            | [b] when b == a.neg -> c := !c
+                            | _ -> ()
+                            end
+                    | _ -> ())
+    done; assert false
+    with Exit ->
+      !blevel, !c, !history, !is_uip
+    (*
     while !cond do
       if !c.learnt then clause_bump_activity !c;
       history := !c :: !history;
@@ -349,27 +380,33 @@ module Make (E : Expr_intf.S)
       | n, Some cl -> c := cl
     done;
     List.iter (fun q -> q.var.seen <- false) !seen;
-    !blevel, !learnt, !history, !size
+    *)
 
-  let record_learnt_clause blevel learnt history size =
+  let record_learnt_clause blevel learnt history is_uip =
     begin match learnt with
       | [] -> assert false
       | [fuip] ->
         assert (blevel = 0);
         fuip.var.tag.vpremise <- history;
         let name = fresh_lname () in
-        let uclause = make_clause name learnt size true history in
+        let uclause = make_clause name learnt (List.length learnt) true history in
         Log.debug 2 "Unit clause learnt : %a" St.pp_clause uclause;
         Vec.push env.learnts uclause;
         enqueue_bool fuip 0 (Bcp (Some uclause))
       | fuip :: _ ->
         let name = fresh_lname () in
-        let lclause = make_clause name learnt size true history in
+        let lclause = make_clause name learnt (List.length learnt) true history in
         Log.debug 2 "New clause learnt : %a" St.pp_clause lclause;
         Vec.push env.learnts lclause;
         attach_clause lclause;
         clause_bump_activity lclause;
-        enqueue_bool fuip blevel (Bcp (Some lclause))
+        if is_uip then
+            enqueue_bool fuip blevel (Bcp (Some lclause))
+        else begin
+            env.decisions <- env.decisions + 1;
+            new_decision_level();
+            enqueue_bool fuip blevel (Bcp None)
+        end
     end;
     var_decay_activity ();
     clause_decay_activity ()
@@ -377,9 +414,9 @@ module Make (E : Expr_intf.S)
   let add_boolean_conflict confl =
     env.conflicts <- env.conflicts + 1;
     if decision_level() = 0 then report_unsat confl; (* Top-level conflict *)
-    let blevel, learnt, history, size = analyze confl in
+    let blevel, learnt, history, is_uip = analyze confl in
     cancel_until blevel;
-    record_learnt_clause blevel learnt (History history) size
+    record_learnt_clause blevel learnt (History history) is_uip
 
   (* Add a new clause *)
   exception Trivial
@@ -536,16 +573,15 @@ module Make (E : Expr_intf.S)
 
   (* Propagation (boolean and theory *)
   let _th_cnumber = ref 0
-  let slice_get i = match (Vec.get env.trail i) with
+  let slice_get i = Either.destruct (Vec.get env.trail i)
-    | Boolean a -> Th.Lit a.lit
+    (function {tag={term; assigned = Some v}} -> Th.Assign (term, v) | _ -> assert false)
-    | Semantic {tag={term; assigned = Some v}} -> Th.Assign (term, v)
+    (fun a -> Th.Lit a.lit)
-    | _ -> assert false
 
   let slice_push l lemma =
     decr _th_cnumber;
     let atoms = List.rev_map (fun x -> add_atom x) l in
     Iheap.grow_to_by_double env.order (St.nb_vars ());
-    List.iter (fun a -> insert_var_order (Formula a.var)) atoms;
+    List.iter (fun a -> insert_var_order (Either.mk_right a.var)) atoms;
     add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma)
 
   let current_slice () = Th.({
@@ -573,12 +609,12 @@ module Make (E : Expr_intf.S)
       let num_props = ref 0 in
       let res = ref None in
       while env.qhead < Vec.size env.trail do
-        match Vec.get env.trail env.qhead with
+        Either.destruct (Vec.get env.trail env.qhead)
-        | Boolean a ->
+        (fun a -> ())
+        (fun a ->
           env.qhead <- env.qhead + 1;
           incr num_props;
-          propagate_atom a res
+          propagate_atom a res)
-        | Semantic a -> ()
       done;
       env.propagations <- env.propagations + !num_props;
       env.simpDB_props <- env.simpDB_props - !num_props;
@@ -598,7 +634,7 @@ module Make (E : Expr_intf.S)
     if sz1 > 2 && (sz2 = 2 || c < 0) then -1
     else 1
 
-  (* returns true if the clause is used as a reason for a propagation,
+(* returns true if the clause is used as a reason for a propagation,
       and therefore can be needed in case of conflict. In this case
       the clause can't be forgotten *)
   let locked c = false (*
@@ -662,16 +698,16 @@ module Make (E : Expr_intf.S)
   (* Decide on a new litteral *)
   let rec pick_branch_lit () =
     let max = Iheap.remove_min f_weight env.order in
-    match St.get_var max with
+    Either.destruct (St.get_var max)
-    | Term v ->
+    (fun v ->
         let value = Th.assign v.tag.term in
         env.decisions <- env.decisions + 1;
         new_decision_level();
         let current_level = decision_level () in
         assert (v.level < 0);
-(*         Log.debug 5 "Assigning %a to %a" St.pp_atom v.tag.pa; *)
+        Log.debug 5 "Deciding on %a" St.pp_semantic_var v;
-        enqueue_assign v value current_level
+        enqueue_assign v value current_level)
-    | Formula v ->
+    (fun v ->
       if v.level>= 0 then begin
           assert (v.tag.pa.is_true || v.tag.na.is_true);
           pick_branch_lit ()
@@ -683,9 +719,9 @@ module Make (E : Expr_intf.S)
           assert (v.level < 0);
           Log.debug 5 "Deciding on %a" St.pp_atom v.tag.pa;
           enqueue_bool v.tag.pa current_level (Bcp None)
-        | Th.Bool b ->
+        | Th.Valued (b, lvl) ->
           let a = if b then v.tag.pa else v.tag.na in
-          enqueue_bool a (decision_level ()) (Bcp None)
+          enqueue_bool a lvl (Bcp None))
 
   let search n_of_conflicts n_of_learnts =
     let conflictC = ref 0 in

solver/mcsolver_types.ml

@@ -65,30 +65,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
       | History of clause list
       | Lemma of proof
 
-  type elt =
+  type elt = (semantic var, boolean var) Either.t
-      | Term of semantic var
-      | Formula of boolean var
-
-  (* Accessors for variables *)
-  let get_elt_id = function
-      | Term v -> v.vid
-      | Formula v -> v.vid
-
-  let get_elt_weight = function
-      | Term v -> v.weight
-      | Formula v -> v.weight
-
-  let get_elt_level = function
-      | Term v -> v.level
-      | Formula v -> v.level
-
-  let set_elt_weight e w = match e with
-      | Term v -> v.weight <- w
-      | Formula v -> v.weight <- w
-
-  let set_elt_level e l = match e with
-      | Term v -> v.level <- l
-      | Formula v -> v.level <- l
 
   (* Dummy values *)
   let dummy_lit = E.dummy
@@ -100,7 +77,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
       tag = {
         pa = dummy_atom;
         na = dummy_atom;
-        reason = None;
+        reason = Bcp None;
         seen = false;
         vpremise = History []; };
     }
@@ -131,7 +108,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
   let f_map = ref MF.empty
   let t_map = ref MT.empty
 
-  let vars = Vec.make 107 (Formula dummy_var)
+  let vars = Vec.make 107 (Either.mk_right dummy_var)
   let nb_vars () = Vec.size vars
   let get_var i = Vec.get vars i
   let iter_vars f = Vec.iter f vars
@@ -171,7 +148,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
             aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
         f_map := MF.add lit var !f_map;
         incr cpt_mk_var;
-        Vec.push vars (Formula var);
+        Vec.push vars (Either.mk_right var);
         var, negated
 
   let make_semantic_var t =
@@ -187,7 +164,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
         } in
         incr cpt_mk_var;
         t_map := MT.add t res !t_map;
-        Vec.push vars (Term res);
+        Vec.push vars (Either.mk_left res);
         res
 
   let add_term t = make_semantic_var t
@@ -221,6 +198,8 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
     fun () -> incr cpt; "C" ^ (string_of_int !cpt)
 
   (* Pretty printing for atoms and clauses *)
+  let print_semantic_var fmt v = E.Term.print fmt v.tag.term
+
   let print_atom fmt a = E.Formula.print fmt a.lit
 
   let print_atoms fmt v =
@@ -255,6 +234,14 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
       | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v
       | Lemma _ -> bprintf b "th_lemma"
 
+  let pp_assign b = function
+      | None -> ()
+      | Some t -> bprintf b "[assignment: %s]" (Log.on_fmt E.Term.print t)
+
+  let pp_semantic_var b v =
+    bprintf b "%d [lit:%s]%a"
+      (v.vid+1) (Log.on_fmt E.Term.print v.tag.term) pp_assign v.tag.assigned
+
   let pp_atom b a =
     bprintf b "%s%d%s [lit:%s] vpremise={{%a}}"
       (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit)

solver/mcsolver_types.mli

@@ -14,5 +14,5 @@
 module type S = Mcsolver_types_intf.S
 
 module Make : functor (E : Expr_intf.S)(Th : Plugin_intf.S)
-  -> S with type term= E.Term.t and type formula = E.Formula.t and type proof = Th.proof
+  -> S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof
 (** Functor to instantiate the types of clauses for the Solver. *)

solver/mcsolver_types_intf.ml

@@ -18,7 +18,6 @@ module type S = sig
   type formula
   type proof
 
-
   type 'a var =
     { vid : int;
       tag : 'a;
@@ -62,9 +61,7 @@ module type S = sig
       | History of clause list
       | Lemma of proof
 
-  type elt =
+  type elt = (semantic var, boolean var) Either.t
-      | Term of semantic var
-      | Formula of boolean var
   (** Recursive types for literals (atoms) and clauses *)
 
   val dummy_var : boolean var
@@ -96,10 +93,12 @@ module type S = sig
   (** Fresh names for clauses *)
 
   val print_atom : Format.formatter -> atom -> unit
+  val print_semantic_var : Format.formatter -> semantic var -> unit
   val print_clause : Format.formatter -> clause -> unit
   (** Pretty printing functions for atoms and clauses *)
 
   val pp_atom : Buffer.t -> atom -> unit
+  val pp_semantic_var : Buffer.t -> semantic var -> unit
   val pp_clause : Buffer.t -> clause -> unit
   (** Debug function for atoms and clauses (very verbose) *)
 

solver/plugin_intf.ml

@@ -50,7 +50,7 @@ module type S = sig
     | Unsat of formula list * proof
 
   type eval_res =
-    | Bool of bool
+    | Valued of bool * int
     | Unknown
 
   val dummy : level

solver/res.ml

@@ -45,6 +45,8 @@ module Make(St : Solver_types.S) = struct
   let equal_atoms a b = St.(a.aid) = St.(b.aid)
   let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
 
+  let merge = List.merge compare_atoms
+
   let _c = ref 0
   let fresh_pcl_name () = incr _c; "P" ^ (string_of_int !_c)
 
@@ -123,7 +125,7 @@ module Make(St : Solver_types.S) = struct
     Log.debug 7 "    %a" St.pp_clause d;
     assert (is_proved (c, cl_c));
     assert (is_proved (d, cl_d));
-    let l = List.merge compare_atoms cl_c cl_d in
+    let l = merge cl_c cl_d in
     let resolved, new_clause = resolve l in
     match resolved with
     | [] -> raise (Resolution_error "No literal to resolve over")

solver/res_intf.ml

@@ -1,24 +1,18 @@
 (* Copyright 2014 Guillaume Bury *)
 
 module type S = sig
-  (** Sinature for a module handling proof by resolution from sat solving traces *)
+  (** Signature for a module handling proof by resolution from sat solving traces *)
+
+    (** {3 Type declarations} *)
+
+  exception Insuficient_hyps
+  (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *)
 
   type atom
   type clause
   type lemma
   (** Abstract types for atoms, clauses and theoriy-specific lemmas *)
 
-  val is_proven : clause -> bool
-  (** Returns [true] if the clause has a derivation in the current proof graph, and [false] otherwise. *)
-
-  exception Insuficient_hyps
-  val learn : clause Vec.t -> unit
-  (** Learn and build proofs for the clause in the vector. Clauses in the vector should be in the order they were learned. *)
-
-  val assert_can_prove_unsat : clause -> unit
-  (** [assert_can_prove_unsat c] tries and prove the empty clause from [c]. [c] may be a learnt clause not yet proved.
-      @raise Insuficient_hyps if it is impossible. *)
-
   type proof_node = {
     conclusion : clause;
     step : step;
@@ -28,6 +22,31 @@ module type S = sig
     | Hypothesis
     | Lemma of lemma
     | Resolution of proof * proof * atom
+  (** Lazy type for proof trees. *)
+
+  (** {3 Resolution helpers} *)
+  val to_list : clause -> atom list
+  (** Returns the sorted list of atoms of a clause. *)
+
+  val merge : atom list -> atom list -> atom list
+  (** Merge two sorted atom list using a suitable comparison function. *)
+
+  val resolve : atom list -> atom list * atom list
+  (** Performs a "resolution step" on a sorted list of atoms.
+      [resolve (List.merge l1 l2)] where [l1] and [l2] are sorted atom lists should return the pair
+      [\[a\], l'], where [l'] is the result of the resolution of [l1] and [l2] over [a]. *)
+
+  (** {3 Proof building functions} *)
+
+  val is_proven : clause -> bool
+  (** Returns [true] if the clause has a derivation in the current proof graph, and [false] otherwise. *)
+
+  val learn : clause Vec.t -> unit
+  (** Learn and build proofs for the clause in the vector. Clauses in the vector should be in the order they were learned. *)
+
+  val assert_can_prove_unsat : clause -> unit
+  (** [assert_can_prove_unsat c] tries and prove the empty clause from [c]. [c] may be a learnt clause not yet proved.
+      @raise Insuficient_hyps if it is impossible. *)
 
   val prove_unsat : clause -> proof
   (** Given a conflict clause [c], returns a proof of the empty clause. Same as [assert_can_prove_unsat] but returns

util/either.ml

@@ -0,0 +1,11 @@
+
+type ('a, 'b) t =
+    | Left of 'a
+    | Right of 'b
+
+let mk_left a = Left a
+let mk_right b = Right b
+
+let destruct e f_left f_right = match e with
+    | Left a -> f_left a
+    | Right b -> f_right b

util/either.mli

@@ -0,0 +1,11 @@
+
+
+type ('a, 'b) t =
+    | Left of 'a
+    | Right of 'b
+
+val mk_left : 'a -> ('a, 'b) t
+val mk_right : 'b -> ('a, 'b) t
+
+val destruct : ('a, 'b) t ->
+    ('a -> 'c) -> ('b -> 'c) -> 'c