Better premises for clauses

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

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

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

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