Explicit status for local assumption clauses

Proofs require local assumptions to be recognisable.
Keeping the reason of local assumptions as Bcp simplfies
the code, since a proof is a clause, and allows to not have
to recreate the local unit clause that effectively propagates
the local assumptions.

With this fix, simplification of clauses is not required aymore for
levels between 0 (excluded) and base_level, so the partition function
can be simplified accordingly.

src/core/internal.ml

@@ -292,8 +292,8 @@ module Make
 
      Clauses that propagated false lits are remembered to reconstruct resolution proofs.
   *)
-  let partition root atoms : atom list * clause list =
+  let partition atoms : atom list * clause list =
-    let rec partition_aux root trues unassigned falses history i =
+    let rec partition_aux trues unassigned falses history i =
       if i >= Array.length atoms then
         trues @ unassigned @ falses, history
       else begin
@@ -307,30 +307,28 @@ module Make
             (arr_to_list atoms (i + 1)), history
         else if a.neg.is_true then
           let l = a.var.v_level in
-          if 0 <= l && l <= root then begin
+          if l = 0 then begin
             match a.var.reason with
-            | None | Some Decision -> assert false
-            (* The var must have a reason, and it cannot be a decision/assumption,
-               its level is below root level. *)
             | Some (Bcp cl) ->
-              partition_aux root trues unassigned falses (cl :: history) (i + 1)
+              partition_aux trues unassigned falses (cl :: history) (i + 1)
             (* A var false at level 0 can be eliminated from the clause,
                but we need to kepp in mind that we used another clause to simplify it. *)
-            | Some (Semantic n) when 0 <= n && n <= root ->
+            | Some (Semantic 0) ->
-              partition_aux root trues unassigned falses history (i + 1)
+              partition_aux trues unassigned falses history (i + 1)
             (* Semantic propagations at level 0 are, well not easy to deal with,
                this shouldn't really happen actually (because semantic propagations
                at level 0 should come with a proof). *)
             (* TODO: get a proof of the propagation. *)
-            | _ -> assert false
+            | None | Some (Decision | Semantic _ ) -> assert false
+            (* The var must have a reason, and it cannot be a decision/assumption,
+               since its level is 0. *)
           end else
-            partition_aux root trues unassigned (a::falses) history (i + 1)
+            partition_aux trues unassigned (a::falses) history (i + 1)
         else
-          partition_aux root trues (a::unassigned) falses history (i + 1)
+          partition_aux trues (a::unassigned) falses history (i + 1)
       end
     in
-    assert (0 <= root);
+    partition_aux [] [] [] [] 0
-    partition_aux root [] [] [] [] 0
 
 
   (* Making a decision.
@@ -445,7 +443,7 @@ module Make
      be able to build a correct proof at the end of proof search. *)
   let simpl_reason : reason -> reason = function
     | (Bcp cl) as r ->
-      let l, history = partition env.base_level cl.atoms in
+      let l, history = partition cl.atoms in
       begin match l with
         | [ a ] ->
           if history = [] then r
@@ -471,7 +469,7 @@ module Make
     if not a.is_true then begin
       assert (a.var.v_level < 0 && a.var.reason = None && lvl >= 0);
       let reason =
-        if lvl > env.base_level then reason
+        if lvl > 0 then reason
         else simpl_reason reason
       in
       a.is_true <- true;
@@ -596,7 +594,7 @@ module Make
                     c := res
                   | _ -> assert false
                 end
-              | None | Some Decision | Some Semantic _ -> ()
+              | None | Some (Decision | Semantic _ ) -> ()
             end
       done; assert false
     with Exit ->
@@ -636,7 +634,7 @@ module Make
     while !cond do
       begin match !c.cpremise with
         | History _ -> clause_bump_activity !c
-        | Hyp | Lemma _ -> ()
+        | Hyp | Local | Lemma _ -> ()
       end;
       history := !c :: !history;
       (* visit the current predecessors *)
@@ -751,10 +749,10 @@ module Make
     let vec = match init.cpremise with
       | Hyp -> env.clauses_hyps
       | Lemma _ -> env.clauses_learnt
-      | History _ -> assert false
+      | Local | History _ -> assert false
     in
     try
-      let atoms, history = partition 0 init.atoms in
+      let atoms, history = partition init.atoms in
       let clause =
         if history = [] then init
         else make_clause ?tag:init.tag (fresh_name ()) atoms (History (init :: history))
@@ -1147,15 +1145,15 @@ module Make
       Log.debugf 10 "local assumption: @[%a@]" (fun k->k pp_atom a);
       assert (decision_level () = env.base_level);
       if a.is_true then ()
-      else if a.neg.is_true then begin
+      else
-        (* conflict between assumptions: UNSAT *)
+        let c = make_clause (fresh_hname ()) [a] Local in
-        let c = make_clause (fresh_hname ()) [a] Hyp in
+        if a.neg.is_true then begin
-        report_unsat c;
+          (* conflict between assumptions: UNSAT *)
-      end else begin
+          report_unsat c;
-        (* make a decision, propagate *)
+        end else begin
-        let level = decision_level() in
+          (* make a decision, propagate *)
-        let c = make_clause (fresh_hname ()) [a] Hyp in
+          let level = decision_level() in
-        enqueue_bool a ~level (Bcp c);
+          enqueue_bool a ~level (Bcp c);
       end
     in
     assert (env.base_level > 0);

src/core/res.ml

@@ -83,23 +83,44 @@ module Make(St : Solver_types.S) = struct
     assert St.(conclusion.cpremise <> History []);
     conclusion
 
-  let prove_unsat c =
+  let rec set_atom_proof a =
-    let l = Array.to_list c.St.atoms in
+    let aux acc b =
-    let l = List.map (fun a ->
+      if equal_atoms a.St.neg b then acc
-        match St.(a.var.reason) with
+      else set_atom_proof b :: acc
-        | Some St.Bcp d -> d
-        | _ -> assert false) l
     in
-    St.make_clause (fresh_pcl_name ()) [] (St.History (c :: l))
+    assert St.(a.var.v_level >= 0);
+    match St.(a.var.reason) with
+    | Some St.Bcp c ->
+      Log.debugf 50 "Analysing: @[%a@ %a@]"
+        (fun k -> k St.pp_atom a St.pp_clause c);
+      if Array.length c.St.atoms = 1 then begin
+        Log.debugf 30 "Old reason: @[%a@]" (fun k -> k St.pp_atom a);
+        c
+      end else begin
+        assert (a.St.neg.St.is_true);
+        let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in
+        let c' = St.make_clause (fresh_pcl_name ()) [a.St.neg] r in
+        a.St.var.St.reason <- Some St.(Bcp c');
+        Log.debugf 30 "New reason: @[%a@ %a@]"
+          (fun k -> k St.pp_atom a St.pp_clause c');
+        c'
+      end
+    | _ -> assert false
+
+  let prove_unsat conflict =
+    if Array.length conflict.St.atoms = 0 then conflict
+    else begin
+      Log.debugf 3 "Proving unsat from: @[%a@]" (fun k -> k St.pp_clause conflict);
+      let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in
+      let res = St.make_clause (fresh_pcl_name ()) [] (St.History (conflict :: l)) in
+      Log.debugf 5 "Proof found: @[%a@]" (fun k -> k St.pp_clause res);
+      res
+    end
 
   let prove_atom a =
-    if St.(a.is_true && a.var.v_level = 0) then begin
+    if St.(a.is_true && a.var.v_level = 0) then
-      match St.(a.var.reason) with
+      Some (set_atom_proof a)
-      | Some St.Bcp c ->
+    else
-        assert (Array.length St.(c.atoms) = 1 && equal_atoms a St.(c.atoms).(0));
-        Some c
-      | _ -> assert false
-    end else
       None
 
   (* Interface exposed *)
@@ -110,6 +131,7 @@ module Make(St : Solver_types.S) = struct
   }
   and step =
     | Hypothesis
+    | Assumption
     | Lemma of lemma
     | Resolution of proof * proof * atom
 
@@ -119,15 +141,15 @@ module Make(St : Solver_types.S) = struct
         (fun k -> k St.pp_clause c St.pp_clause d);
       let dl = to_list d in
       begin match resolve (merge cl dl) with
-      | [ a ], l ->
+        | [ a ], l ->
-        begin match r with
+          begin match r with
-          | [] -> (l, c, d, a)
+            | [] -> (l, c, d, a)
-          | _ ->
+            | _ ->
-            let new_clause = St.make_clause (fresh_pcl_name ())
+              let new_clause = St.make_clause (fresh_pcl_name ())
-                l (St.History [c; d]) in
+                  l (St.History [c; d]) in
-            chain_res (new_clause, l) r
+              chain_res (new_clause, l) r
-        end
+          end
-      | _ -> assert false
+        | _ -> assert false
       end
     | _ -> assert false
 
@@ -138,6 +160,8 @@ module Make(St : Solver_types.S) = struct
       {conclusion; step = Lemma l; }
     | St.Hyp ->
       { conclusion; step = Hypothesis; }
+    | St.Local ->
+      { conclusion; step = Assumption; }
     | St.History [] ->
       assert false
     | St.History [ c ] ->
@@ -163,11 +187,11 @@ module Make(St : Solver_types.S) = struct
         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.Hyp | St.Local | St.Lemma _ -> aux (c :: res) acc r
-            | St.History h ->
+          | St.History h ->
-              let l = List.fold_left (fun acc c ->
+            let l = List.fold_left (fun acc c ->
-                  if not c.St.visited then c :: acc else acc) r h in
+                if not c.St.visited then c :: acc else acc) r h in
-              aux res (c :: acc) l
+            aux res (c :: acc) l
         end else
           aux res acc r
     in

src/core/res_intf.ml

@@ -27,6 +27,7 @@ module type S = sig
   }
   and step =
     | Hypothesis
+    | Assumption
     | Lemma of lemma
     | Resolution of proof * proof * atom
   (** Lazy type for proof trees. Proofs are persistent objects, and can be

src/core/solver_types.ml

@@ -72,6 +72,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
 
   and premise =
     | Hyp
+    | Local
     | Lemma of proof
     | History of clause list
 
@@ -277,6 +278,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
 
   let pp_premise out = function
     | Hyp -> Format.fprintf out "hyp"
+    | Local -> Format.fprintf out "local"
     | Lemma _ -> Format.fprintf out "th_lemma"
     | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@ " name) v
 

src/core/solver_types_intf.ml

@@ -67,6 +67,7 @@ module type S = sig
 
   and premise =
     | Hyp
+    | Local
     | Lemma of proof
     | History of clause list