Lots of fixes for proof generation.

sat/res.ml

@@ -20,6 +20,7 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
     | 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 *)
@@ -38,7 +39,7 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
       let equal = equal_cl
     end)
   let proof : node H.t = H.create 1007;;
-  let unit_learnt : clause H.t = H.create 37;;
+  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)
@@ -47,14 +48,6 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
   let _c = ref 0
   let fresh_pcl_name () = incr _c; "P" ^ (string_of_int !_c)
 
-  let clause_unit a =
-    try
-      H.find unit_learnt [a]
-    with Not_found ->
-      let new_c = St.(make_clause (fresh_pcl_name ()) [a] 1 true a.var.vpremise) in
-      H.add unit_learnt [a] new_c;
-      new_c
-
   (* Printing functions *)
   let print_atom fmt a =
     Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "¬ ") St.(a.var.vid + 1)
@@ -96,6 +89,25 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
     | [a] -> St.(a.var.level = 0 && a.var.reason = None && a.var.vpremise <> [])
     | _ -> false
 
+  let make_unit_hyp a =
+    let aux a = St.(make_clause (fresh_name ()) [a] 1 false []) 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.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
@@ -112,7 +124,7 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
     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 (c, cl_d));
+    assert (is_proved (d, cl_d));
     let l = List.merge compare_atoms cl_c cl_d in
     let resolved, new_clause = resolve l in
     match resolved with
@@ -134,22 +146,31 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
         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.reason) with
+    | 0, Some c -> c, to_list c
+    | 0, 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 :: ((_ :: _) as 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 unit_to_use = diff_learnt [] cl temp_cl in
-      let unit_r = List.map St.(fun a -> clause_unit a.neg, [a.neg]) unit_to_use in
-      let new_c, new_cl = List.fold_left add_res (temp_c, temp_cl) unit_r in
-      if not (equal_cl cl new_cl) then begin
-        (* We didn't get the expected clause, raise an error *)
-        Log.debug 0 "Expected the following clauses to be equal :";
-        Log.debug 0 "expected : %s" (Log.on_fmt print_cl cl);
-        Log.debug 0 "found : %a" St.pp_clause new_c;
-        assert false
-      end
+      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 St.(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) =
@@ -186,7 +207,9 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = 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.reason) with
         | 0, Some d -> d
-        | 0, None -> clause_unit St.(a.neg)
+        | 0, 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;
@@ -199,11 +222,15 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
     with Exit ->
       false
 
-  exception Cannot
+  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 Cannot
+    if not (prove_unsat_cl (c, to_list c)) then
+      raise Insuficient_hyps
 
   (* Interface exposed *)
   type proof_node = {
@@ -279,6 +306,8 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
       (print_dot_edge id) (c_id p2)
 
   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 () =
@@ -305,6 +334,7 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
           (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 ();

sat/res_intf.ml

@@ -9,9 +9,12 @@ module type S = sig
   val is_proven : clause -> bool
   (** Returns [true] if the clause has a derivation in the current proof graph, and [false] otherwise. *)
 
-  exception Cannot
+  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
-  (** [prove_unsat c] tries and prove the empty clause from [c].
+  (** [prove_unsat c] tries and prove the empty clause from [c]. [c] may be a learnt clause not yet proved.
       @raise Cannot if it is impossible. *)
 
   type proof_node = {

sat/sat.ml

@@ -120,6 +120,7 @@ module Make(Dummy : sig end) = struct
   let eval = SatSolver.eval
 
   let get_proof () =
+    SatSolver.Proof.learn (SatSolver.history ());
     match SatSolver.unsat_conflict () with
     | None -> assert false
     | Some c -> SatSolver.Proof.prove_unsat c

sat/solver.ml

@@ -498,18 +498,10 @@ module Make (F : Formula_intf.S)
 
   (* remove from [vec] the clauses that are satisfied in the current trail *)
   let remove_satisfied vec =
-    let j = ref 0 in
-    let k = Vec.size vec - 1 in
-    for i = 0 to k do
+    for i = 0 to Vec.size vec - 1 do
       let c = Vec.get vec i in
       if satisfied c then remove_clause c
-      else begin
-        Vec.set vec !j (Vec.get vec i);
-        incr j
-      end
-    done;
-    Vec.shrink vec (k + 1 - !j)
-
+    done
 
   module HUC = Hashtbl.Make
       (struct type t = clause let equal = (==) let hash = Hashtbl.hash end)
@@ -548,11 +540,11 @@ module Make (F : Formula_intf.S)
       | [] -> assert false
       | [fuip] ->
         assert (blevel = 0);
+        fuip.var.vpremise <- history;
         let name = fresh_lname () in
         let uclause = make_clause name learnt size true history in
-        Log.debug 2 "Unit clause learnt : %a" St.pp_atom fuip;
+        Log.debug 2 "Unit clause learnt : %a" St.pp_clause uclause;
         Vec.push env.learnts uclause;
-        fuip.var.vpremise <- history;
         enqueue fuip 0 (Some uclause)
       | fuip :: _ ->
         let name = fresh_lname () in

tests/run

@@ -7,7 +7,7 @@ solvertest () {
     for f in `find -L $1 -name *.cnf -type f`
     do
         echo -ne "\r\033[KTesting $f..."
-        "$SOLVER" -t 30s -s 1G $f | grep $2 > /dev/null 2> /dev/null
+        "$SOLVER" -check -t 30s -s 1G $f | grep $2 > /dev/null 2> /dev/null
         RET=$?
         if [ $RET -ne 0 ];
         then