A bit of cleanup of dead code

solver/mcproof.ml

@@ -39,7 +39,6 @@ module Make(St : Mcsolver_types.S) = struct
       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)
@@ -84,33 +83,10 @@ module Make(St : Mcsolver_types.S) = struct
     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
+    else if not St.(c.learnt) then begin
       H.add proof cl Assumption;
       true
     end else match St.(c.cpremise) with
@@ -148,12 +124,6 @@ module Make(St : Mcsolver_types.S) = struct
 
   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")
 
@@ -209,9 +179,6 @@ module Make(St : Mcsolver_types.S) = struct
       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;
@@ -273,14 +240,14 @@ module Make(St : Mcsolver_types.S) = struct
     aux (to_list c, to_list d)
 
   let unsat_core proof =
-    let rec aux proof =
+    let rec aux acc proof =
       let p = proof () in
       match p.step with
-      | Hypothesis | Lemma _ -> [p.conclusion]
+      | Hypothesis | Lemma _ -> p.conclusion :: acc
       | Resolution (proof1, proof2, _) ->
-        List.rev_append (aux proof1) (aux proof2)
+        aux (aux acc proof1) proof2
     in
-    List.sort_uniq compare_cl (aux proof)
+    List.sort_uniq compare_cl (aux [] proof)
 
   (* Print proof graph *)
   let _i = ref 0

solver/mcsolver.ml

@@ -273,7 +273,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
               a.neg.is_true <- false;
               a.var.level <- -1;
               a.var.tag.reason <- Bcp None;
-              a.var.tag.vpremise <- History [];
               insert_var_order (Either.mk_right a.var)
             end)
       done;
@@ -427,7 +426,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
         if fuip.neg.is_true then
             report_unsat confl
         else begin
-          fuip.var.tag.vpremise <- history;
           let name = fresh_lname () in
           let uclause = make_clause name learnt (List.length learnt) true history in
           L.debug 1 "Unit clause learnt : %a" St.pp_clause uclause;
@@ -469,13 +467,11 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
       let aux (atoms, init) a =
           if a.is_true then raise Trivial;
           if a.neg.is_true then
-              match a.var.tag.vpremise with
+              atoms, false
-              | History v -> atoms, [init0]
-              | Lemma p -> assert false
           else
               a::atoms, init
       in
-      let atoms, init = List.fold_left aux ([], []) atoms in
+      let atoms, init = List.fold_left aux ([], true) atoms in
       List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init
 
   let partition atoms init0 =
@@ -486,37 +482,35 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
           if a.var.level = 0 then raise Trivial
           else (a::trues) @ unassigned @ falses @ r, init
         else if a.neg.is_true then
-          if a.var.level = 0 then match a.var.tag.vpremise with
+          if a.var.level = 0 then
-          | History v ->
+            partition_aux trues unassigned falses false r
-            partition_aux trues unassigned falses [init0] r
-          | Lemma _ -> assert false
           else
             partition_aux trues unassigned (a::falses) init r
-        else partition_aux trues (a::unassigned) falses init r
+        else
+          partition_aux trues (a::unassigned) falses init r
     in
     if decision_level () = 0 then
         simplify_zero atoms init0
     else
-        partition_aux [] [] [] [] atoms
+        partition_aux [] [] [] true atoms
 
-  let add_clause ~cnumber atoms history =
+  let add_clause name atoms history =
     if env.is_unsat then raise Unsat;
-    let init_name = string_of_int cnumber in
+    let init_name = name in
     let init0 = make_clause init_name atoms (List.length atoms) (history <> History []) history in
     L.debug 10 "Adding clause : %a" St.pp_clause init0;
     try
       let atoms, init = partition atoms init0 in
-      let history = match init with
-      | [] -> history
-      | l -> History l
-      in
       let size = List.length atoms in
       match atoms with
       | [] ->
         report_unsat init0;
       | a::b::_ ->
         let name = fresh_name () in
-        let clause = make_clause name atoms size (history <> History []) history in
+        let clause =
+            if init then init0
+            else make_clause name atoms size true (History [init0])
+        in
         L.debug 1 "New clause : %a" St.pp_clause init0;
         attach_clause clause;
         Vec.push env.clauses clause;
@@ -531,8 +525,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
         end
       | [a]   ->
         cancel_until 0;
-        a.var.tag.vpremise <- history;
+        enqueue_bool a 0 (Bcp (Some init0))
-        enqueue_bool a 0 (Bcp (match init with [init0] -> Some init0 | _ -> None))
     with Trivial -> ()
 
 
@@ -620,18 +613,15 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
       ignore (th_eval a);
       a
 
-  let _th_cnumber = ref 0
-
   let slice_get i = Either.destruct (Vec.get env.trail i)
       (function {level; tag={term; assigned = Some v}} -> Th.Assign (term, v), level | _ -> assert false)
       (fun a -> Th.Lit a.lit, a.var.level)
 
   let slice_push l lemma =
-    decr _th_cnumber;
     let atoms = List.rev_map (fun x -> new_atom x) l in
     Iheap.grow_to_by_double env.order (St.nb_vars ());
     List.iter (fun a -> insert_var_order (Either.mk_right a.var)) atoms;
-    add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma)
+    add_clause "lemma" atoms (Lemma lemma)
 
   let slice_propagate f lvl =
     let a = add_atom f in
@@ -830,7 +820,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
 
   let add_clauses cnf ~cnumber =
     let aux cl =
-        add_clause ~cnumber cl (History []);
+        add_clause "hyp" cl (History []);
         match propagate () with
         | None -> () | Some confl -> report_unsat confl
     in

solver/mcsolver_types.ml

@@ -37,9 +37,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
   type boolean = {
     pa : atom;
     na : atom;
-    mutable seen : bool;
     mutable reason : reason;
-    mutable vpremise : premise
   }
 
   and atom =
@@ -78,9 +76,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
       tag = {
         pa = dummy_atom;
         na = dummy_atom;
-        reason = Bcp None;
+        reason = Bcp None; };
-        seen = false;
-        vpremise = History []; };
     }
   and dummy_atom =
     { var = dummy_var;
@@ -145,9 +141,7 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
             tag = {
               pa = pa;
               na = na;
-              reason = Bcp None;
+              reason = Bcp None;};
-              seen = false;
-              vpremise = History [];};
           }
         and pa =
           { var = var;
@@ -263,9 +257,8 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
       (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}}"
+    bprintf b "%s%d%s[lit:%s]"
       (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit)
-      pp_premise a.var.tag.vpremise
 
   let pp_atoms_vec b vec =
     for i = 0 to Vec.size vec - 1 do

solver/mcsolver_types_intf.ml

@@ -31,9 +31,7 @@ module type S = sig
   type boolean = {
     pa : atom;
     na : atom;
-    mutable seen : bool;
     mutable reason : reason;
-    mutable vpremise : premise
   }
 
   and atom = {

solver/res.ml

@@ -79,7 +79,7 @@ module Make(St : Solver_types.S) = struct
     done;
     let l, res = resolve (List.sort_uniq compare_atoms !l) in
     if l <> [] then
-      raise (Resolution_error "Input cause is a tautology");
+      raise (Resolution_error "Input clause is a tautology");
     res
 
   (* Adding hyptoheses *)