[bugfix] Eliminate duplicates in input clauses

When adding clauses that conatins duplicates, the checking
of some proof would fail because there would sometime be multiple
littrals to resolve over. This fixes that problem.

_tags

@@ -29,6 +29,7 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 <src/smt/type_smt.*>: package(dolmen)
 
 # more warnings
+<src/**/*.ml>: warn_error(+8)
 <src/**/*.ml>: warn_K, warn_Y, warn_X
 <src/**/*.ml>: short_paths, safe_string, strict_sequence
 <src/**/*.cm*>: debug

src/backend/dot.ml

@@ -72,10 +72,18 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm
     | S.Hypothesis ->
       print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Hypothesis" "LIGHTBLUE"
         [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))];
+    | S.Assumption ->
+      print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Assumption" "LIGHTBLUE"
+        [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))];
     | S.Lemma lemma ->
       let rule, color, l = A.lemma_info lemma in
       let color = match color with None -> "YELLOW" | Some c -> c in
       print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
+    | S.Duplicate (p, l) ->
+      print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Duplicate" "GREY"
+        ((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) ::
+        List.map (ttify A.print_atom) l);
+      print_edge fmt (node_id n) (node_id (S.expand p))
     | S.Resolution (_, _, a) ->
       print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY"
         [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))];

src/backend/dot.mli

@@ -28,7 +28,7 @@ module type Arg = sig
 
   val print_atom : Format.formatter -> atom -> unit
   (** Print the contents of the given atomic formulas.
-      WARNING: this function should take care to esapce and/or not output special
+      WARNING: this function should take care to escape and/or not output special
       reserved characters for the dot format (such as quotes and so on). *)
 
   val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list

src/core/internal.ml

@@ -318,6 +318,20 @@ module Make
     if i >= Array.length arr then []
     else Array.to_list (Array.sub arr i (Array.length arr - i))
 
+  (* Eliminates atom doublons in clauses *)
+  let eliminate_doublons clause : clause =
+    let duplicates = ref [] in
+    let res = ref [] in
+    Array.iter (fun a ->
+        if a.var.seen then duplicates := a :: !duplicates
+        else (a.var.seen <- true; res := a :: !res)
+      ) clause.atoms;
+    List.iter (fun a -> a.var.seen <- false) !res;
+    if !duplicates = [] then
+      clause
+    else
+      make_clause (fresh_lname ()) !res (History [clause])
+
   (* Partition literals for new clauses, into:
      - true literals (maybe makes the clause trivial if the lit is proved true at level 0)
      - unassigned literals, yet to be decided
@@ -734,15 +748,18 @@ module Make
     cancel_until (max cr.cr_backtrack_lvl (base_level ()));
     record_learnt_clause confl cr
 
+  (* Get the correct vector to insert a clause in. *)
+  let rec clause_vector c =
+    match c.cpremise with
+      | Hyp -> env.clauses_hyps
+      | Local -> env.clauses_temp
+      | Lemma _ | History _ -> env.clauses_learnt
+
   (* Add a new clause, simplifying, propagating, and backtracking if
      the clause is false in the current trail *)
   let add_clause (init:clause) : unit =
     Log.debugf debug "Adding clause: @[<hov>%a@]" (fun k -> k St.pp_clause init);
-    let vec = match init.cpremise with
-      | Hyp -> env.clauses_hyps
-      | Local -> env.clauses_temp
-      | History _ | Lemma _ -> env.clauses_learnt
-    in
+    let vec = clause_vector init in
     try
       let atoms, history = partition init.atoms in
       let clause =
@@ -921,9 +938,7 @@ module Make
     let atoms = List.rev_map create_atom l in
     let c = make_clause (fresh_tname ()) atoms (Lemma lemma) in
     Log.debugf info "Pushing clause %a" (fun k->k St.pp_clause c);
-    (* do not add the clause yet, wait for the theory propagation to
-       be done *)
-    Stack.push c env.clauses_to_add
+    Stack.push (eliminate_doublons c) env.clauses_to_add
 
   let slice_propagate f = function
     | Plugin_intf.Eval l ->
@@ -937,7 +952,7 @@ module Make
             (p :: List.map (fun a -> a.neg) l) (Lemma proof) in
         if p.is_true then ()
         else if p.neg.is_true then
-          Stack.push c env.clauses_to_add
+          Stack.push (eliminate_doublons c) env.clauses_to_add
         else begin
           Iheap.grow_to_at_least env.order (St.nb_elt ());
           insert_subterms_order p.var;
@@ -1153,7 +1168,7 @@ module Make
                 let atoms = List.rev_map create_atom l in
                 let c = make_clause (fresh_tname ()) atoms (Lemma p) in
                 Log.debugf info "Theory conflict clause: %a" (fun k -> k St.pp_clause c);
-                Stack.push c env.clauses_to_add
+                Stack.push (eliminate_doublons c) env.clauses_to_add
             end;
             if Stack.is_empty env.clauses_to_add then raise Sat
         end
@@ -1165,7 +1180,10 @@ module Make
       (fun l ->
          let atoms = List.rev_map atom l in
          let c = make_clause ?tag (fresh_hname ()) atoms Hyp in
-         Stack.push c env.clauses_to_add)
+         Log.debugf debug "Assuming clause: @[<hov 2>%a@]" (fun k -> k pp_clause c);
+         let c' = eliminate_doublons c in
+         Log.debugf debug "Inserting clause: @[<hov 2>%a@]" (fun k -> k pp_clause c');
+         Stack.push c' env.clauses_to_add)
       cnf
 
   (* create a factice decision level for local assumptions *)

src/core/res.ml

@@ -34,6 +34,7 @@ module Make(St : Solver_types.S) = struct
   let merge = List.merge compare_atoms
 
   let _c = ref 0
+  let fresh_dpl_name () = incr _c; "D" ^ (string_of_int !_c)
   let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c)
 
   (* Compute resolution of 2 clauses *)
@@ -52,22 +53,44 @@ module Make(St : Solver_types.S) = struct
     let resolved, new_clause = aux [] [] l in
     resolved, List.rev new_clause
 
-  (* List.sort_uniq is only since 4.02.0 *)
-  let sort_uniq compare l =
-    let rec aux = function
-      | x :: ((y :: _) as r) -> if compare x y = 0 then aux r else x :: aux r
-      | l -> l
+  (* Compute the set of doublons of a clause *)
+  let list c = List.sort compare_atoms (Array.to_list St.(c.atoms))
+
+  let analyze cl =
+    let rec aux duplicates free = function
+      | [] -> duplicates, free
+      | [ x ] -> duplicates, x :: free
+      | x :: ((y :: r) as l) ->
+        if equal_atoms x y then
+          count duplicates (x :: free) x [y] r
+        else
+          aux duplicates (x :: free) l
+    and count duplicates free x acc = function
+      | (y :: r) when equal_atoms x y ->
+        count duplicates free x (y :: acc) r
+      | l ->
+        aux (acc :: duplicates) free l
     in
-    aux (List.sort compare l)
+    let doublons, acc = aux [] [] cl in
+    doublons, List.rev acc
 
   let to_list c =
-    let v = St.(c.atoms) in
-    let l = Array.to_list v in
-    let res = sort_uniq compare_atoms l in
-    let l, _ = resolve res in
-    if l <> [] then
-      Log.debug 3 "Input clause is a tautology";
-    res
+    let cl = list c in
+    let doublons, l = analyze cl in
+    let conflicts, _ = resolve l in
+    if doublons <> [] then
+      Log.debug warn "Input clause has redundancies";
+    if conflicts <> [] then
+      Log.debug warn "Input clause is a tautology";
+    cl
+
+  let rec pp_cl fmt l =
+    let rec aux fmt = function
+      | [] -> ()
+      | a :: r ->
+        Format.fprintf fmt "%a@,%a" St.pp_atom a aux r
+    in
+    Format.fprintf fmt "@[<v>%a@]" aux l
 
   (* Comparison of clauses *)
   let cmp_cl c d =
@@ -139,6 +162,7 @@ module Make(St : Solver_types.S) = struct
     | Hypothesis
     | Assumption
     | Lemma of lemma
+    | Duplicate of proof * atom list
     | Resolution of proof * proof * atom
 
   let rec chain_res (c, cl) = function
@@ -171,8 +195,9 @@ module Make(St : Solver_types.S) = struct
     | St.History [] ->
       assert false
     | St.History [ c ] ->
-      assert (cmp c conclusion = 0);
-      expand c
+      let duplicates, res = analyze (list c) in
+      assert (cmp_cl res (list conclusion) = 0);
+      { conclusion; step = Duplicate (c, List.concat duplicates) }
     | St.History ( c :: ([d] as r)) ->
       let (l, c', d', a) = chain_res (c, to_list c) r in
       assert (cmp_cl l (to_list conclusion) = 0);
@@ -231,10 +256,12 @@ module Make(St : Solver_types.S) = struct
         Stack.push (Leaving c) s;
         let node = expand c in
         begin match node.step with
+          | Duplicate (p1, _) ->
+            Stack.push (Enter p1) s
           | Resolution (p1, p2, _) ->
             Stack.push (Enter p2) s;
             Stack.push (Enter p1) s
-          | _ -> ()
+          | Hypothesis | Assumption | Lemma _ -> ()
         end
       end;
       fold_aux s h f acc

src/core/res_intf.ml

@@ -36,7 +36,10 @@ module type S = sig
     | Assumption
       (** The conclusion has been locally assumed by the user *)
     | Lemma of lemma
-      (** The conclusion is a tautology provided by the theory, with associated proof *)
+    (** The conclusion is a tautology provided by the theory, with associated proof *)
+    | Duplicate of proof * atom list
+    (** The conclusion is obtained by eliminating multiple occurences of the atom in
+        the conclusion of the provided proof. *)
     | Resolution of proof * proof * atom
       (** The conclusion can be deduced by performing a resolution between the conclusions
           of the two given proofs. The atom on which to perform the resolution is also given. *)

src/core/solver_types.ml

@@ -298,7 +298,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     | 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
+    | History v -> List.iter (fun { name; _ } -> Format.fprintf out "%s,@ " name) v
 
   let pp_assign fmt v =
     match v.assigned with
@@ -312,11 +312,11 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       (v.lid+1) pp_assign v E.Term.print v.term
 
   let pp_atom out a =
-    Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]@ "
+    Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]"
       (sign a) (a.var.vid+1) pp_value a E.Formula.print a.lit
 
   let pp_atoms_vec out vec =
-    Array.iter (fun a -> pp_atom out a) vec
+    Array.iter (fun a -> Format.fprintf out "%a@ " pp_atom a) vec
 
   let pp_clause out {name=name; atoms=arr; cpremise=cp; } =
     Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"

src/core/solver_types_intf.ml

@@ -98,7 +98,10 @@ module type S = sig
     | Lemma of proof          (** The clause is a theory-provided tautology, with
                                   the given proof. *)
     | History of clause list  (** The clause can be obtained by resolution of the clauses
-                                  in the list. For a premise [History [a_1 :: ... :: a_n]]
+                                  in the list. If the list has a single element [c] , then
+                                  the clause can be obtained by simplifying [c] (i.e
+                                  eliminating doublons in its atom list).
+                                  For a premise [History [a_1 :: ... :: a_n]] ([n > 0])
                                   the clause is obtained by performing resolution of
                                   [a_1] with [a_2], and then performing a resolution step between
                                   the result and [a_3], etc...

src/main.ml

@@ -11,8 +11,8 @@ exception Out_of_space
 let file = ref ""
 let p_cnf = ref false
 let p_check = ref false
+let p_dot_proof = ref ""
 let p_proof_print = ref false
-let p_unsat_core = ref false
 let time_limit = ref 300.
 let size_limit = ref 1000_000_000.
 
@@ -27,7 +27,14 @@ end
 module Make
     (S : External.S)
     (T : Type.S with type atom := S.atom)
-= struct
+  : sig
+    val do_task : Dolmen.Statement.t -> unit
+  end = struct
+
+  module D = Dot.Make(S.Proof)(struct
+      let print_atom = S.St.print_atom
+      let lemma_info _ = "<>", None, []
+    end)
 
   let hyps = ref []
 
@@ -57,6 +64,10 @@ module Make
           if !p_check then begin
             let p = state.Solver_intf.get_proof () in
             S.Proof.check p;
+            if !p_dot_proof <> "" then begin
+              let fmt = Format.formatter_of_out_channel (open_out !p_dot_proof) in
+              D.print fmt p
+            end
           end;
           let t' = Sys.time () -. t in
           Format.printf "Unsat (%f/%f)@." t t'
@@ -128,6 +139,8 @@ let argspec = Arg.align [
     " Prints the cnf used.";
     "-check", Arg.Set p_check,
     " Build, check and print the proof (if output is set), if unsat";
+    "-dot", Arg.Set_string p_dot_proof,
+    " If provided, print the dot proof in the given file";
     "-gc", Arg.Unit setup_gc_stat,
     " Outputs statistics about the GC";
     "-s", Arg.String set_solver,
@@ -136,8 +149,6 @@ let argspec = Arg.align [
     "<s>[kMGT] Sets the size limit for the sat solver";
     "-time", Arg.String (int_arg time_limit),
     "<t>[smhd] Sets the time limit for the sat solver";
-    "-u", Arg.Set p_unsat_core,
-    " Prints the unsat-core explanation of the unsat proof (if used with -check)";
     "-v", Arg.Int (fun i -> Log.set_debug i),
     "<lvl> Sets the debug verbose level";
   ]

tests/bugs/double_atom.cnf

@@ -0,0 +1,10 @@
+p cnf 2 3
+c Local assumptions
+
+c Hypotheses
+-2 -2 -1 -1 0
+1 0
+2 0
+c Lemmas
+
+

tests/unsat/bug-01.cnf

@@ -0,0 +1 @@
+../bugs/double_atom.cnf