From 510a8aaa34c3e7f3b9161763c2a6d1d8773e4cc9 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Sat, 9 Jul 2016 03:06:21 +0200
Subject: [PATCH 1/7] [bugfix] Clause level now computed at creation

Apart from new assumptions, clause level can always
be computed from the histoy of the clause, so it is
better to do it in Solver_types when creating clauses.
Aditionally, it seems there was an error in the manual
computing of clause level somewhere, this fixes the bug.
---
 solver/internal.ml          | 68 ++++++++++++++++++-------------------
 solver/res.ml               |  3 +-
 solver/solver_types.ml      | 13 +++++--
 solver/solver_types_intf.ml |  4 +--
 4 files changed, 46 insertions(+), 42 deletions(-)

diff --git a/solver/internal.ml b/solver/internal.ml
index 9a98b2bb..8dc7fa79 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -281,51 +281,51 @@ module Make
   (* Simplify clauses *)
   exception Trivial
 
-  let simplify_zero atoms level0 =
+  let simplify_zero atoms =
     (* Eliminates dead litterals from clauses when at decision level 0 *)
     assert (decision_level () = 0);
-    let aux (atoms, history, lvl) a =
+    let aux (atoms, history) a =
       if a.is_true then raise Trivial;
       if a.neg.is_true then begin
         match a.var.reason with
         | None | Some Decision -> assert false
-        | Some (Bcp cl) -> atoms, cl :: history, max lvl cl.c_level
-        | Some (Semantic 0) -> atoms, history, lvl
+        | Some (Bcp cl) -> atoms, cl :: history
+        | Some (Semantic 0) -> atoms, history
         | Some (Semantic _) ->
           Log.debugf 0 "Unexpected semantic propagation at level 0: %a"
             (fun k->k St.pp_atom a);
           assert false
       end else
-        a::atoms, history, lvl
+        a::atoms, history
     in
-    let atoms, init, lvl = List.fold_left aux ([], [], level0) atoms in
-    List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init, lvl
+    let atoms, init = List.fold_left aux ([], []) atoms in
+    List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init
 
-  let partition atoms init0 =
+  let partition atoms =
     (* Parittion litterals for new clauses *)
-    let rec partition_aux trues unassigned falses history lvl = function
-      | [] -> trues @ unassigned @ falses, history, lvl
+    let rec partition_aux trues unassigned falses history = function
+      | [] -> trues @ unassigned @ falses, history
       | a :: r ->
         if a.is_true then
           if a.var.v_level = 0 then raise Trivial
-          else (a::trues) @ unassigned @ falses @ r, history, lvl
+          else (a::trues) @ unassigned @ falses @ r, history
         else if a.neg.is_true then
           if a.var.v_level = 0 then begin
             match a.var.reason with
             | Some (Bcp cl) ->
-              partition_aux trues unassigned falses (cl :: history) (max lvl cl.c_level) r
+              partition_aux trues unassigned falses (cl :: history) r
             | Some (Semantic 0) ->
-              partition_aux trues unassigned falses history lvl r
+              partition_aux trues unassigned falses history r
             | _ -> assert false
           end else
-            partition_aux trues unassigned (a::falses) history lvl r
+            partition_aux trues unassigned (a::falses) history r
         else
-          partition_aux trues (a::unassigned) falses history lvl r
+          partition_aux trues (a::unassigned) falses history r
     in
     if decision_level () = 0 then
-      simplify_zero atoms init0
+      simplify_zero atoms
     else
-      partition_aux [] [] [] [] init0 atoms
+      partition_aux [] [] [] [] atoms
 
   (* Compute a progess estimate *)
   let progress_estimate () =
@@ -413,12 +413,12 @@ module Make
 
   let simpl_reason = function
     | (Bcp cl) as r ->
-      let l, history, c_lvl = partition (Vec.to_list cl.atoms) 0 in
+      let l, history = partition (Vec.to_list cl.atoms) in
       begin match l with
         | [ a ] ->
           if history = [] then r
           else
-            let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) c_lvl in
+            let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) in
             Bcp tmp_cl
         | _ -> assert false
       end
@@ -478,7 +478,6 @@ module Make
     let is_uip  = ref false in
     let c       = ref (Proof.to_list c_clause) in
     let history = ref [c_clause] in
-    let c_level = ref 0 in
     clause_bump_activity c_clause;
     let is_semantic a = match a.var.reason with
       | Some Semantic _ -> true
@@ -505,7 +504,6 @@ module Make
                 begin match tmp with
                   | [] -> ()
                   | [b] when b == a.var.pa ->
-                    c_level := max !c_level d.c_level;
                     clause_bump_activity d;
                     var_bump_activity a.var;
                     history := d :: !history;
@@ -518,7 +516,7 @@ module Make
     with Exit ->
       let learnt = List.sort (fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in
       let blevel = backtrack_lvl !is_uip learnt in
-      blevel, learnt, List.rev !history, !is_uip, !c_level
+      blevel, learnt, List.rev !history, !is_uip
 
   let get_atom i =
     match Vec.get env.elt_queue i with
@@ -534,7 +532,6 @@ module Make
     let tr_ind = ref (Vec.size env.elt_queue - 1) in
     let size   = ref 1 in
     let history = ref [] in
-    let c_level = ref 0 in
     assert (decision_level () > 0);
     while !cond do
       if !c.learnt then clause_bump_activity !c;
@@ -575,12 +572,11 @@ module Make
         cond := false;
         learnt := p.neg :: (List.rev !learnt)
       | n, Some Bcp cl ->
-        c_level := max !c_level cl.c_level;
         c := cl
       | n, _ -> assert false
     done;
     List.iter (fun q -> q.var.seen <- false) !seen;
-    !blevel, !learnt, List.rev !history, true, !c_level
+    !blevel, !learnt, List.rev !history, true
 
   let analyze c_clause =
     if St.mcsat then
@@ -588,7 +584,7 @@ module Make
     else
       analyze_sat c_clause
 
-  let record_learnt_clause confl blevel learnt history is_uip lvl =
+  let record_learnt_clause confl blevel learnt history is_uip =
     begin match learnt with
       | [] -> assert false
       | [fuip] ->
@@ -597,13 +593,13 @@ module Make
           report_unsat confl
         else begin
           let name = fresh_lname () in
-          let uclause = make_clause name learnt (List.length learnt) true history lvl in
+          let uclause = make_clause name learnt (List.length learnt) true history in
           Vec.push env.clauses_learnt uclause;
           enqueue_bool fuip 0 (Bcp uclause)
         end
       | fuip :: _ ->
         let name = fresh_lname () in
-        let lclause = make_clause name learnt (List.length learnt) true history lvl in
+        let lclause = make_clause name learnt (List.length learnt) true history in
         Vec.push env.clauses_learnt lclause;
         attach_clause lclause;
         clause_bump_activity lclause;
@@ -621,19 +617,20 @@ module Make
     env.conflicts <- env.conflicts + 1;
     if decision_level() = 0 || Vec.for_all (fun a -> a.var.v_level = 0) confl.atoms then
       report_unsat confl; (* Top-level conflict *)
-    let blevel, learnt, history, is_uip, lvl = analyze confl in
+    let blevel, learnt, history, is_uip = analyze confl in
     cancel_until blevel;
-    record_learnt_clause confl blevel learnt (History history) is_uip lvl
+    record_learnt_clause confl blevel learnt (History history) is_uip
 
   (* Add a new clause *)
   let add_clause ?(force=false) init0 =
+    Log.debugf 90 "Adding clause:@[<hov>%a@]" (fun k -> k St.pp_clause init0);
     let vec = match init0.cpremise with
       | Lemma _ -> env.clauses_learnt
       | History [] -> env.clauses_hyps
       | History _ -> assert false
     in
     try
-      let atoms, history, level = partition (Vec.to_list init0.atoms) init0.c_level in
+      let atoms, history = partition (Vec.to_list init0.atoms) in
       let size = List.length atoms in
       match atoms with
       | [] ->
@@ -642,7 +639,7 @@ module Make
       | a::b::_ ->
         let clause =
           if history = [] then init0
-          else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History (init0 :: history)) level
+          else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History (init0 :: history))
         in
         Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause);
         attach_clause clause;
@@ -737,7 +734,7 @@ module Make
     let atoms = List.rev_map (fun x -> new_atom x) l in
     Iheap.grow_to_by_double env.order (St.nb_elt ());
     List.iter (fun a -> insert_var_order (elt_of_var a.var)) atoms;
-    let c = make_clause (fresh_tname ()) atoms (List.length atoms) true (Lemma lemma) base_level in
+    let c = make_clause (fresh_tname ()) atoms (List.length atoms) true (Lemma lemma) in
     add_clause c
 
   let slice_propagate f lvl =
@@ -775,7 +772,7 @@ module Make
         let l = List.rev_map new_atom l in
         Iheap.grow_to_by_double env.order (St.nb_elt ());
         List.iter (fun a -> insert_var_order (elt_of_var a.var)) l;
-        let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) base_level in
+        let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) in
         Some c
     end
 
@@ -956,7 +953,8 @@ module Make
 
   let add_clauses ?tag cnf =
     let aux cl =
-      let c = make_clause ?tag (fresh_hname ()) cl (List.length cl) false (History []) (current_level ()) in
+      let c = make_clause ?tag ~lvl:(current_level ())
+          (fresh_hname ()) cl (List.length cl) false (History []) in
       add_clause c;
       (* Clauses can be added after search has begun (and thus we are not at level 0,
          so better not do anything at this point.
diff --git a/solver/res.ml b/solver/res.ml
index d97595aa..1c14667c 100644
--- a/solver/res.ml
+++ b/solver/res.ml
@@ -94,7 +94,6 @@ module Make(St : Solver_types.S) = struct
         | _ -> assert false) l
     in
     St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l))
-      (List.fold_left (fun i c -> max i c.St.c_level) 0 l)
 
   let prove_atom a =
     if St.(a.is_true && a.var.v_level = 0) then begin
@@ -128,7 +127,7 @@ module Make(St : Solver_types.S) = struct
           | [] -> (l, c, d, a)
           | _ ->
             let new_clause = St.make_clause (fresh_pcl_name ()) l (List.length l) true
-                (St.History [c; d]) (max c.St.c_level d.St.c_level) in
+                (St.History [c; d]) in
             chain_res (new_clause, l) r
         end
       | _ -> assert false
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 297cbdc6..34baa3ba 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -179,18 +179,25 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     let var, negated = make_boolean_var lit in
     if negated then var.na else var.pa
 
-  let make_clause ?tag name ali sz_ali is_learnt premise lvl =
+  let make_clause ?tag ?lvl name ali sz_ali is_learnt premise =
     let atoms = Vec.from_list ali sz_ali dummy_atom in
+    let level =
+      match lvl, premise with
+      | Some lvl, History [] -> lvl
+      | Some _, _ -> assert false
+      | None, History l -> List.fold_left (fun lvl c -> max lvl c.c_level) 0 l
+      | None, Lemma _ -> 0
+    in
     { name  = name;
       tag = tag;
       atoms = atoms;
       removed = false;
       learnt = is_learnt;
-      c_level = lvl;
+      c_level = level;
       activity = 0.;
       cpremise = premise}
 
-  let empty_clause = make_clause "Empty" [] 0 false (History []) 0
+  let empty_clause = make_clause "Empty" [] 0 false (History [])
 
   (* Decisions & propagations *)
   type t = (lit, atom) Either.t
diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml
index 1be6c9d4..a09ce96b 100644
--- a/solver/solver_types_intf.ml
+++ b/solver/solver_types_intf.ml
@@ -115,8 +115,8 @@ module type S = sig
 
   val empty_clause : clause
   (** The empty clause *)
-  val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> int -> clause
-  (** [make_clause name atoms size learnt premise level] creates a clause with the given attributes. *)
+  val make_clause : ?tag:int -> ?lvl:int -> string -> atom list -> int -> bool -> premise -> clause
+  (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *)
 
   (** {2 Clause names} *)
 

From 245941efdb87306f7f5d0b9cd48bcf1e5fa93a49 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 13 Jul 2016 16:23:34 +0200
Subject: [PATCH 2/7] Remember more added clauses

---
 _tags                       |  1 -
 solver/internal.ml          | 91 ++++++++++++++++++++-----------------
 solver/solver_types.ml      |  6 +--
 solver/solver_types_intf.ml |  2 +-
 4 files changed, 54 insertions(+), 46 deletions(-)

diff --git a/_tags b/_tags
index 2ea41d17..4a5fd955 100644
--- a/_tags
+++ b/_tags
@@ -1,5 +1,4 @@
 <util/*.cmx>: for-pack(Msat)
-#<util/*.native>: 
 <smt/*.cmx>: for-pack(Msat)
 <sat/*.cmx>: for-pack(Msat)
 <solver/*.cmx>: for-pack(Msat)
diff --git a/solver/internal.ml b/solver/internal.ml
index 8dc7fa79..aa6a6681 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -351,24 +351,29 @@ module Make
 
   (* Adding/removing clauses *)
   let attach_clause c =
-    Vec.push (Vec.get c.atoms 0).neg.watched c;
-    Vec.push (Vec.get c.atoms 1).neg.watched c;
-    if c.learnt then
-      env.learnts_literals <- env.learnts_literals + Vec.size c.atoms
-    else
-      env.clauses_literals <- env.clauses_literals + Vec.size c.atoms
+    if not c.attached then begin
+      c.attached <- true;
+      Vec.push (Vec.get c.atoms 0).neg.watched c;
+      Vec.push (Vec.get c.atoms 1).neg.watched c;
+      if c.learnt then
+        env.learnts_literals <- env.learnts_literals + Vec.size c.atoms
+      else
+        env.clauses_literals <- env.clauses_literals + Vec.size c.atoms
+    end
 
   let detach_clause c =
-    Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c);
-    c.removed <- true;
-    (* Not necessary, cleanup is done during propagation
-       Vec.remove (Vec.get c.atoms 0).neg.watched c;
-       Vec.remove (Vec.get c.atoms 1).neg.watched c;
-    *)
-    if c.learnt then
-      env.learnts_literals <- env.learnts_literals - Vec.size c.atoms
-    else
-      env.clauses_literals <- env.clauses_literals - Vec.size c.atoms
+    if c.attached then begin
+      c.attached <- false;
+      Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c);
+      (* Not necessary, cleanup is done during propagation
+         Vec.remove (Vec.get c.atoms 0).neg.watched c;
+         Vec.remove (Vec.get c.atoms 1).neg.watched c;
+      *)
+      if c.learnt then
+        env.learnts_literals <- env.learnts_literals - Vec.size c.atoms
+      else
+        env.clauses_literals <- env.clauses_literals - Vec.size c.atoms
+    end
 
   let remove_clause c = detach_clause c
 
@@ -413,13 +418,16 @@ module Make
 
   let simpl_reason = function
     | (Bcp cl) as r ->
-      let l, history = partition (Vec.to_list cl.atoms) in
+      Log.debugf 90 "Simplifying reason: %a" (fun k -> k St.pp_clause cl);
+      let atoms = Vec.to_list cl.atoms in
+      let l, history = partition atoms in
       begin match l with
         | [ a ] ->
           if history = [] then r
-          else
+          else begin
             let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) in
             Bcp tmp_cl
+          end
         | _ -> assert false
       end
     | r -> r
@@ -605,7 +613,7 @@ module Make
         clause_bump_activity lclause;
         if is_uip then
           enqueue_bool fuip blevel (Bcp lclause)
-      else begin
+        else begin
           env.next_decision <- Some fuip.neg
         end
     end;
@@ -622,28 +630,28 @@ module Make
     record_learnt_clause confl blevel learnt (History history) is_uip
 
   (* Add a new clause *)
-  let add_clause ?(force=false) init0 =
-    Log.debugf 90 "Adding clause:@[<hov>%a@]" (fun k -> k St.pp_clause init0);
-    let vec = match init0.cpremise with
-      | Lemma _ -> env.clauses_learnt
+  let add_clause ?(force=false) init =
+    Log.debugf 90 "Adding clause:@[<hov>%a@]" (fun k -> k St.pp_clause init);
+    let vec = match init.cpremise with
+      | Lemma _ -> env.clauses_theory
       | History [] -> env.clauses_hyps
       | History _ -> assert false
     in
     try
-      let atoms, history = partition (Vec.to_list init0.atoms) in
+      let atoms, history = partition (Vec.to_list init.atoms) in
       let size = List.length atoms in
+      let clause =
+        if history = [] then init
+        else make_clause ?tag:init.tag (fresh_name ())
+            atoms size true (History (init :: history))
+      in
+      Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause);
+      Vec.push vec clause;
       match atoms with
       | [] ->
-        Log.debugf 1 "New clause (unsat) :@ @[%a@]" (fun k->k St.pp_clause init0);
-        report_unsat init0
+        report_unsat clause
       | a::b::_ ->
-        let clause =
-          if history = [] then init0
-          else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History (init0 :: history))
-        in
-        Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause);
         attach_clause clause;
-        Vec.push vec clause;
         if a.neg.is_true then begin
           let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in
           cancel_until lvl;
@@ -656,9 +664,10 @@ module Make
       | [a]   ->
         Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a);
         cancel_until 0;
-        enqueue_bool a 0 (Bcp  init0)
+        enqueue_bool a 0 (Bcp clause)
     with Trivial ->
-      Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init0)
+      Vec.push vec init;
+      Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init)
 
   let propagate_in_clause a c i watched new_sz =
     let atoms = c.atoms in
@@ -709,7 +718,7 @@ module Make
       try
         for i = 0 to Vec.size watched - 1 do
           let c = Vec.get watched i in
-          if not c.removed then propagate_in_clause a c i watched new_sz_w
+          if c.attached then propagate_in_clause a c i watched new_sz_w
         done;
       with Conflict c ->
         assert (!res = None);
@@ -786,10 +795,10 @@ module Make
       let res = ref None in
       while env.elt_head < Vec.size env.elt_queue do
         begin match Vec.get env.elt_queue env.elt_head with
-        | Either.Left _ -> ()
-        | Either.Right a ->
-             incr num_props;
-             propagate_atom a res
+          | Either.Left _ -> ()
+          | Either.Right a ->
+            incr num_props;
+            propagate_atom a res
         end;
         env.elt_head <- env.elt_head + 1;
       done;
@@ -958,8 +967,8 @@ module Make
       add_clause c;
       (* Clauses can be added after search has begun (and thus we are not at level 0,
          so better not do anything at this point.
-      match propagate () with
-      | None -> () | Some confl -> report_unsat confl
+         match propagate () with
+         | None -> () | Some confl -> report_unsat confl
       *)
     in
     List.iter aux cnf
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 34baa3ba..01e39816 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -62,7 +62,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     c_level : int;
     mutable cpremise : premise;
     mutable activity : float;
-    mutable removed : bool;
+    mutable attached : bool;
   }
 
   and reason =
@@ -102,7 +102,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       tag = None;
       atoms = Vec.make_empty dummy_atom;
       activity = -1.;
-      removed = false;
+      attached = false;
       c_level = -1;
       learnt = false;
       cpremise = History [] }
@@ -191,7 +191,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     { name  = name;
       tag = tag;
       atoms = atoms;
-      removed = false;
+      attached = false;
       learnt = is_learnt;
       c_level = level;
       activity = 0.;
diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml
index a09ce96b..b755fb8c 100644
--- a/solver/solver_types_intf.ml
+++ b/solver/solver_types_intf.ml
@@ -57,7 +57,7 @@ module type S = sig
     c_level : int;
     mutable cpremise : premise;
     mutable activity : float;
-    mutable removed : bool;
+    mutable attached : bool;
   }
 
   and reason =

From c159a60d9be0e4a408c4015e5929f10993ea075f Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 13 Jul 2016 16:43:01 +0200
Subject: [PATCH 3/7] Better premises for clauses

---
 solver/internal.ml          |  9 +++++----
 solver/res.ml               |  6 ++++--
 solver/solver_types.ml      | 15 ++++++++-------
 solver/solver_types_intf.ml |  3 ++-
 4 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/solver/internal.ml b/solver/internal.ml
index aa6a6681..8a79bea4 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -633,8 +633,8 @@ module Make
   let add_clause ?(force=false) init =
     Log.debugf 90 "Adding clause:@[<hov>%a@]" (fun k -> k St.pp_clause init);
     let vec = match init.cpremise with
-      | Lemma _ -> env.clauses_theory
-      | History [] -> env.clauses_hyps
+      | Hyp _ -> env.clauses_hyps
+      | Lemma _ -> env.clauses_learnt
       | History _ -> assert false
     in
     try
@@ -962,8 +962,8 @@ module Make
 
   let add_clauses ?tag cnf =
     let aux cl =
-      let c = make_clause ?tag ~lvl:(current_level ())
-          (fresh_hname ()) cl (List.length cl) false (History []) in
+      let c = make_clause ?tag (fresh_hname ())
+          cl (List.length cl) false (Hyp (current_level ())) in
       add_clause c;
       (* Clauses can be added after search has begun (and thus we are not at level 0,
          so better not do anything at this point.
@@ -1124,6 +1124,7 @@ module Make
         if c.c_level > l then begin
           remove_clause c;
           match c.cpremise with
+          | Lemma _ -> Stack.push c s
           | History ({ cpremise = Lemma _ } as c' :: _ ) -> Stack.push c' s
           | _ -> () (* Only simplified clauses can have a level > 0 *)
         end else begin
diff --git a/solver/res.ml b/solver/res.ml
index 1c14667c..2663dcb5 100644
--- a/solver/res.ml
+++ b/solver/res.ml
@@ -139,9 +139,11 @@ module Make(St : Solver_types.S) = struct
     match conclusion.St.cpremise with
     | St.Lemma l ->
       {conclusion; step = Lemma l; }
-    | St.History [] ->
+    | St.Hyp _ ->
       assert (not conclusion.St.learnt);
       { conclusion; step = Hypothesis; }
+    | St.History [] ->
+      assert false
     | St.History [ c ] ->
       assert (cmp c conclusion = 0);
       expand c
@@ -163,7 +165,7 @@ module Make(St : Solver_types.S) = struct
       | [] -> acc
       | c :: r ->
         begin match c.St.cpremise with
-          | St.History [] | St.Lemma _ -> aux (c :: acc) r
+          | St.Hyp _ | St.Lemma _ -> aux (c :: acc) r
           | St.History l -> aux acc (l @ r)
         end
     in
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 01e39816..4faebc70 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -71,6 +71,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     | Semantic of int
 
   and premise =
+    | Hyp of int
     | Lemma of proof
     | History of clause list
 
@@ -179,14 +180,13 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     let var, negated = make_boolean_var lit in
     if negated then var.na else var.pa
 
-  let make_clause ?tag ?lvl name ali sz_ali is_learnt premise =
+  let make_clause ?tag name ali sz_ali is_learnt premise =
     let atoms = Vec.from_list ali sz_ali dummy_atom in
     let level =
-      match lvl, premise with
-      | Some lvl, History [] -> lvl
-      | Some _, _ -> assert false
-      | None, History l -> List.fold_left (fun lvl c -> max lvl c.c_level) 0 l
-      | None, Lemma _ -> 0
+      match premise with
+      | Hyp lvl -> lvl
+      | Lemma _ -> 0
+      | History l -> List.fold_left (fun lvl c -> max lvl c.c_level) 0 l
     in
     { name  = name;
       tag = tag;
@@ -276,8 +276,9 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     else "[]"
 
   let pp_premise out = function
-    | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@," name) v
+    | Hyp _ -> Format.fprintf out "hyp"
     | Lemma _ -> Format.fprintf out "th_lemma"
+    | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@," name) v
 
   let pp_assign out = function
     | None -> ()
diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml
index b755fb8c..cb14fd89 100644
--- a/solver/solver_types_intf.ml
+++ b/solver/solver_types_intf.ml
@@ -66,6 +66,7 @@ module type S = sig
     | Semantic of int
 
   and premise =
+    | Hyp of int
     | Lemma of proof
     | History of clause list
 
@@ -115,7 +116,7 @@ module type S = sig
 
   val empty_clause : clause
   (** The empty clause *)
-  val make_clause : ?tag:int -> ?lvl:int -> string -> atom list -> int -> bool -> premise -> clause
+  val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause
   (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *)
 
   (** {2 Clause names} *)

From ef49d5eaaa2e0d9c3cba8febf5cc8f1f80d1dd8c Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 13 Jul 2016 17:07:03 +0200
Subject: [PATCH 4/7] Slightly better formatting for clause printing

---
 solver/solver_types.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 4faebc70..f6cdaa37 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -278,25 +278,25 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
   let pp_premise out = function
     | Hyp _ -> Format.fprintf out "hyp"
     | Lemma _ -> Format.fprintf out "th_lemma"
-    | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@," name) v
+    | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@ " name) v
 
   let pp_assign out = function
     | None -> ()
-    | Some t -> Format.fprintf out "[assignment: %a]" E.Term.print t
+    | Some t -> Format.fprintf out " ->@ %a" E.Term.print t
 
   let pp_lit out v =
-    Format.fprintf out "%d [lit:%a]%a"
+    Format.fprintf out "%d [lit:%a%a]"
       (v.lid+1) E.Term.print v.term pp_assign v.assigned
 
   let pp_atom out a =
-    Format.fprintf out "%s%d%s[lit:%a]"
+    Format.fprintf out "%s%d%s[atom:%a]"
       (sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
 
   let pp_atoms_vec out vec =
-    Vec.print ~sep:"; " pp_atom out vec
+    Vec.print ~sep:"@ " pp_atom out vec
 
   let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
-    Format.fprintf out "%s%s{ %a} cpremise={{%a}}"
+    Format.fprintf out "@[<hov 2>%s%s{@[<hov 2>%a@]}@ cpremise={@[<hov2>%a@]}@]"
       name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
 
 end

From 2ff1279f266b7814473090f9fb5d748a0bcb2c94 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 13 Jul 2016 17:44:04 +0200
Subject: [PATCH 5/7] Better perfs for unsat_core

---
 solver/res.ml               | 27 ++++++++++++++++++---------
 solver/solver_types.ml      |  3 +++
 solver/solver_types_intf.ml |  1 +
 3 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/solver/res.ml b/solver/res.ml
index 2663dcb5..2195ef0d 100644
--- a/solver/res.ml
+++ b/solver/res.ml
@@ -158,18 +158,27 @@ module Make(St : Solver_types.S) = struct
       { conclusion; step = Resolution (c', d', a); }
 
   (* Compute unsat-core
-     TODO: the uniq sort at the end may be costly, maybe remove it,
-           or compare the clauses faster ? *)
+     TODO: replace visited bool by a int unique to each call
+     of unsat_core, so that the cleanup can be removed ? *)
   let unsat_core proof =
-    let rec aux acc = function
-      | [] -> acc
+    let rec aux res acc = function
+      | [] -> res, acc
       | c :: r ->
-        begin match c.St.cpremise with
-          | St.Hyp _ | St.Lemma _ -> aux (c :: acc) r
-          | St.History l -> aux acc (l @ r)
-        end
+        if not c.St.visited then begin
+          c.St.visited <- true;
+          match c.St.cpremise with
+            | St.Hyp _ | St.Lemma _ -> aux (c :: res) acc r
+            | St.History h ->
+              let l = List.fold_left (fun acc c ->
+                  if not c.St.visited then c :: acc else acc) r h in
+              aux res (c :: acc) l
+        end else
+          aux res acc r
     in
-    sort_uniq cmp (aux [] [proof])
+    let res, tmp = aux [] [] [proof] in
+    List.iter (fun c -> c.St.visited <- false) res;
+    List.iter (fun c -> c.St.visited <- false) tmp;
+    res
 
   (* Iter on proofs *)
   module H = Hashtbl.Make(struct
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index f6cdaa37..414648ae 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -63,6 +63,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     mutable cpremise : premise;
     mutable activity : float;
     mutable attached : bool;
+    mutable visited : bool;
   }
 
   and reason =
@@ -106,6 +107,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       attached = false;
       c_level = -1;
       learnt = false;
+      visited = false;
       cpremise = History [] }
 
   let () =
@@ -192,6 +194,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       tag = tag;
       atoms = atoms;
       attached = false;
+      visited = false;
       learnt = is_learnt;
       c_level = level;
       activity = 0.;
diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml
index cb14fd89..740ee05d 100644
--- a/solver/solver_types_intf.ml
+++ b/solver/solver_types_intf.ml
@@ -58,6 +58,7 @@ module type S = sig
     mutable cpremise : premise;
     mutable activity : float;
     mutable attached : bool;
+    mutable visited : bool;
   }
 
   and reason =

From 1acecc0815d940df166928b983ce34b4e76d2824 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 13 Jul 2016 18:14:23 +0200
Subject: [PATCH 6/7] Small printing upgrades

---
 solver/solver_types.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 414648ae..524d08f6 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -263,7 +263,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     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 sign a = if a == a.var.pa then "+" else "-"
 
   let level a =
     match a.var.v_level, a.var.reason with
@@ -292,14 +292,14 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       (v.lid+1) E.Term.print v.term pp_assign v.assigned
 
   let pp_atom out a =
-    Format.fprintf out "%s%d%s[atom:%a]"
+    Format.fprintf out "%s%d%s[atom:%a]@ "
       (sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
 
   let pp_atoms_vec out vec =
-    Vec.print ~sep:"@ " pp_atom out vec
+    Vec.print ~sep:"" pp_atom out vec
 
   let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
-    Format.fprintf out "@[<hov 2>%s%s{@[<hov 2>%a@]}@ cpremise={@[<hov2>%a@]}@]"
+    Format.fprintf out "%s%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
       name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
 
 end

From 9dadb67fc97c84334019c345d776d3a1c219ab8f Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Sat, 16 Jul 2016 15:55:26 +0200
Subject: [PATCH 7/7] [bugfix] Sort false atoms by levels in new clauses

When a new clauses is added and it is a conflict (i.e all atoms
are false), one must take care of which literals to watch.
In order to work, the watched literals must be those with the higher
decision levels, or else the watched literals might not react when
needed. This is fixed by sorting the literals in decreasing order of
decision level when adding a new clause which happens to be false in the
current trail.
---
 solver/internal.ml          | 67 ++++++++++++++++++-------------------
 solver/res.ml               |  9 +++--
 solver/solver_types.ml      | 13 +++----
 solver/solver_types_intf.ml |  3 +-
 4 files changed, 42 insertions(+), 50 deletions(-)

diff --git a/solver/internal.ml b/solver/internal.ml
index 8a79bea4..716581b6 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -304,7 +304,8 @@ module Make
   let partition atoms =
     (* Parittion litterals for new clauses *)
     let rec partition_aux trues unassigned falses history = function
-      | [] -> trues @ unassigned @ falses, history
+      | [] ->
+        trues @ unassigned @ falses, history
       | a :: r ->
         if a.is_true then
           if a.var.v_level = 0 then raise Trivial
@@ -352,27 +353,18 @@ module Make
   (* Adding/removing clauses *)
   let attach_clause c =
     if not c.attached then begin
+      Log.debugf 60 "Attaching %a" (fun k -> k St.pp_clause c);
       c.attached <- true;
       Vec.push (Vec.get c.atoms 0).neg.watched c;
       Vec.push (Vec.get c.atoms 1).neg.watched c;
-      if c.learnt then
-        env.learnts_literals <- env.learnts_literals + Vec.size c.atoms
-      else
-        env.clauses_literals <- env.clauses_literals + Vec.size c.atoms
     end
 
   let detach_clause c =
     if c.attached then begin
       c.attached <- false;
       Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c);
-      (* Not necessary, cleanup is done during propagation
-         Vec.remove (Vec.get c.atoms 0).neg.watched c;
-         Vec.remove (Vec.get c.atoms 1).neg.watched c;
-      *)
-      if c.learnt then
-        env.learnts_literals <- env.learnts_literals - Vec.size c.atoms
-      else
-        env.clauses_literals <- env.clauses_literals - Vec.size c.atoms
+      Vec.remove (Vec.get c.atoms 0).neg.watched c;
+      Vec.remove (Vec.get c.atoms 1).neg.watched c;
     end
 
   let remove_clause c = detach_clause c
@@ -383,6 +375,7 @@ module Make
   (* cancel down to [lvl] excluded *)
   let cancel_until lvl =
     if decision_level () > lvl then begin
+      Log.debugf 5 "Backtracking to lvl %d" (fun k -> k lvl);
       env.elt_head <- Vec.get env.elt_levels lvl;
       env.th_head <- env.elt_head;
       for c = env.elt_head to Vec.size env.elt_queue - 1 do
@@ -424,10 +417,8 @@ module Make
       begin match l with
         | [ a ] ->
           if history = [] then r
-          else begin
-            let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) in
-            Bcp tmp_cl
-          end
+          else
+            Bcp (make_clause (fresh_tname ()) l 1 (History (cl :: history)))
         | _ -> assert false
       end
     | r -> r
@@ -522,7 +513,8 @@ module Make
             end
       done; assert false
     with Exit ->
-      let learnt = List.sort (fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in
+      let learnt = List.fast_sort (
+          fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in
       let blevel = backtrack_lvl !is_uip learnt in
       blevel, learnt, List.rev !history, !is_uip
 
@@ -542,7 +534,10 @@ module Make
     let history = ref [] in
     assert (decision_level () > 0);
     while !cond do
-      if !c.learnt then clause_bump_activity !c;
+      begin match !c.cpremise with
+        | History _ -> clause_bump_activity !c
+        | Hyp _ | Lemma _ -> ()
+      end;
       history := !c :: !history;
       (* visit the current predecessors *)
       for j = 0 to Vec.size !c.atoms - 1 do
@@ -601,13 +596,13 @@ module Make
           report_unsat confl
         else begin
           let name = fresh_lname () in
-          let uclause = make_clause name learnt (List.length learnt) true history in
+          let uclause = make_clause name learnt (List.length learnt) history in
           Vec.push env.clauses_learnt uclause;
           enqueue_bool fuip 0 (Bcp uclause)
         end
       | fuip :: _ ->
         let name = fresh_lname () in
-        let lclause = make_clause name learnt (List.length learnt) true history in
+        let lclause = make_clause name learnt (List.length learnt) history in
         Vec.push env.clauses_learnt lclause;
         attach_clause lclause;
         clause_bump_activity lclause;
@@ -643,7 +638,7 @@ module Make
       let clause =
         if history = [] then init
         else make_clause ?tag:init.tag (fresh_name ())
-            atoms size true (History (init :: history))
+          atoms size (History (init :: history))
       in
       Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause);
       Vec.push vec clause;
@@ -651,15 +646,18 @@ module Make
       | [] ->
         report_unsat clause
       | a::b::_ ->
-        attach_clause clause;
         if a.neg.is_true then begin
-          let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in
-          cancel_until lvl;
-          add_boolean_conflict clause
-        end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin
-          let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in
-          cancel_until lvl;
-          enqueue_bool a lvl (Bcp clause)
+          Vec.sort clause.atoms (fun a b ->
+              compare b.var.v_level a.var.v_level);
+          attach_clause clause;
+          add_boolean_conflict init
+        end else begin
+          attach_clause clause;
+          if b.neg.is_true && not a.is_true && not a.neg.is_true then begin
+            let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in
+            cancel_until lvl;
+            enqueue_bool a lvl (Bcp clause)
+          end
         end
       | [a]   ->
         Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a);
@@ -681,8 +679,7 @@ module Make
       (* true clause, keep it in watched *)
       Vec.set watched !new_sz c;
       incr new_sz;
-    end
-    else
+    end else
       try (* look for another watch lit *)
         for k = 2 to Vec.size atoms - 1 do
           let ak = Vec.get atoms k in
@@ -743,7 +740,7 @@ module Make
     let atoms = List.rev_map (fun x -> new_atom x) l in
     Iheap.grow_to_by_double env.order (St.nb_elt ());
     List.iter (fun a -> insert_var_order (elt_of_var a.var)) atoms;
-    let c = make_clause (fresh_tname ()) atoms (List.length atoms) true (Lemma lemma) in
+    let c = make_clause (fresh_tname ()) atoms (List.length atoms) (Lemma lemma) in
     add_clause c
 
   let slice_propagate f lvl =
@@ -781,7 +778,7 @@ module Make
         let l = List.rev_map new_atom l in
         Iheap.grow_to_by_double env.order (St.nb_elt ());
         List.iter (fun a -> insert_var_order (elt_of_var a.var)) l;
-        let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) in
+        let c = St.make_clause (St.fresh_tname ()) l (List.length l) (Lemma p) in
         Some c
     end
 
@@ -963,7 +960,7 @@ module Make
   let add_clauses ?tag cnf =
     let aux cl =
       let c = make_clause ?tag (fresh_hname ())
-          cl (List.length cl) false (Hyp (current_level ())) in
+          cl (List.length cl) (Hyp (current_level ())) in
       add_clause c;
       (* Clauses can be added after search has begun (and thus we are not at level 0,
          so better not do anything at this point.
diff --git a/solver/res.ml b/solver/res.ml
index 2195ef0d..b74a0cc9 100644
--- a/solver/res.ml
+++ b/solver/res.ml
@@ -83,7 +83,7 @@ module Make(St : Solver_types.S) = struct
     cmp_cl (to_list c) (to_list d)
 
   let prove conclusion =
-    assert St.(conclusion.learnt || conclusion.cpremise <> History []);
+    assert St.(conclusion.cpremise <> History []);
     conclusion
 
   let prove_unsat c =
@@ -93,7 +93,7 @@ module Make(St : Solver_types.S) = struct
         | Some St.Bcp d -> d
         | _ -> assert false) l
     in
-    St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l))
+    St.make_clause (fresh_pcl_name ()) [] 0 (St.History (c :: l))
 
   let prove_atom a =
     if St.(a.is_true && a.var.v_level = 0) then begin
@@ -126,8 +126,8 @@ module Make(St : Solver_types.S) = struct
         begin match r with
           | [] -> (l, c, d, a)
           | _ ->
-            let new_clause = St.make_clause (fresh_pcl_name ()) l (List.length l) true
-                (St.History [c; d]) in
+            let new_clause = St.make_clause (fresh_pcl_name ())
+                l (List.length l) (St.History [c; d]) in
             chain_res (new_clause, l) r
         end
       | _ -> assert false
@@ -140,7 +140,6 @@ module Make(St : Solver_types.S) = struct
     | St.Lemma l ->
       {conclusion; step = Lemma l; }
     | St.Hyp _ ->
-      assert (not conclusion.St.learnt);
       { conclusion; step = Hypothesis; }
     | St.History [] ->
       assert false
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 524d08f6..76894b3a 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -58,7 +58,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     name : string;
     tag : int option;
     atoms : atom Vec.t;
-    learnt : bool;
     c_level : int;
     mutable cpremise : premise;
     mutable activity : float;
@@ -106,7 +105,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       activity = -1.;
       attached = false;
       c_level = -1;
-      learnt = false;
       visited = false;
       cpremise = History [] }
 
@@ -182,7 +180,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     let var, negated = make_boolean_var lit in
     if negated then var.na else var.pa
 
-  let make_clause ?tag name ali sz_ali is_learnt premise =
+  let make_clause ?tag name ali sz_ali premise =
     let atoms = Vec.from_list ali sz_ali dummy_atom in
     let level =
       match premise with
@@ -195,12 +193,11 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       atoms = atoms;
       attached = false;
       visited = false;
-      learnt = is_learnt;
       c_level = level;
       activity = 0.;
       cpremise = premise}
 
-  let empty_clause = make_clause "Empty" [] 0 false (History [])
+  let empty_clause = make_clause "Empty" [] 0 (History [])
 
   (* Decisions & propagations *)
   type t = (lit, atom) Either.t
@@ -298,9 +295,9 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
   let pp_atoms_vec out vec =
     Vec.print ~sep:"" pp_atom out vec
 
-  let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
-    Format.fprintf out "%s%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
-      name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
+  let pp_clause out {name=name; atoms=arr; cpremise=cp; } =
+    Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
+      name pp_atoms_vec arr pp_premise cp
 
 end
 
diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml
index 740ee05d..619558f4 100644
--- a/solver/solver_types_intf.ml
+++ b/solver/solver_types_intf.ml
@@ -53,7 +53,6 @@ module type S = sig
     name : string;
     tag : int option;
     atoms : atom Vec.t;
-    learnt : bool;
     c_level : int;
     mutable cpremise : premise;
     mutable activity : float;
@@ -117,7 +116,7 @@ module type S = sig
 
   val empty_clause : clause
   (** The empty clause *)
-  val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause
+  val make_clause : ?tag:int -> string -> atom list -> int -> premise -> clause
   (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *)
 
   (** {2 Clause names} *)