From 8076c060475f715d13fc3737d8c6767668fa8cef Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 14 Feb 2017 19:21:07 +0100 Subject: [PATCH] [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 | 1 + src/backend/dot.ml | 8 +++++ src/backend/dot.mli | 2 +- src/core/internal.ml | 40 +++++++++++++++++------- src/core/res.ml | 59 +++++++++++++++++++++++++---------- src/core/res_intf.ml | 5 ++- src/core/solver_types.ml | 6 ++-- src/core/solver_types_intf.ml | 5 ++- src/main.ml | 19 ++++++++--- tests/bugs/double_atom.cnf | 10 ++++++ tests/unsat/bug-01.cnf | 1 + 11 files changed, 119 insertions(+), 37 deletions(-) create mode 100644 tests/bugs/double_atom.cnf create mode 120000 tests/unsat/bug-01.cnf diff --git a/_tags b/_tags index 31793d6e..2edeeba1 100644 --- a/_tags +++ b/_tags @@ -29,6 +29,7 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20) : package(dolmen) # more warnings +: warn_error(+8) : warn_K, warn_Y, warn_X : short_paths, safe_string, strict_sequence : debug diff --git a/src/backend/dot.ml b/src/backend/dot.ml index f8338a2e..fdfec48f 100644 --- a/src/backend/dot.ml +++ b/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)))]; diff --git a/src/backend/dot.mli b/src/backend/dot.mli index e66665f1..d47271a2 100644 --- a/src/backend/dot.mli +++ b/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 diff --git a/src/core/internal.ml b/src/core/internal.ml index 7f12532a..ea07e2bd 100644 --- a/src/core/internal.ml +++ b/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: @[%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: @[%a@]" (fun k -> k pp_clause c); + let c' = eliminate_doublons c in + Log.debugf debug "Inserting clause: @[%a@]" (fun k -> k pp_clause c'); + Stack.push c' env.clauses_to_add) cnf (* create a factice decision level for local assumptions *) diff --git a/src/core/res.ml b/src/core/res.ml index df4a6229..4545f633 100644 --- a/src/core/res.ml +++ b/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 "@[%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 diff --git a/src/core/res_intf.ml b/src/core/res_intf.ml index 4630cae7..3260baec 100644 --- a/src/core/res_intf.ml +++ b/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. *) diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml index 70b3ead6..0b2849ef 100644 --- a/src/core/solver_types.ml +++ b/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:@[%a@]]@ " + Format.fprintf out "%s%d[%a][atom:@[%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@[{@[%a@]}@ cpremise={@[%a@]}@]" diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml index 57b47e7c..059f70fb 100644 --- a/src/core/solver_types_intf.ml +++ b/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... diff --git a/src/main.ml b/src/main.ml index bc40bb32..86d35d7f 100644 --- a/src/main.ml +++ b/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 [ "[kMGT] Sets the size limit for the sat solver"; "-time", Arg.String (int_arg time_limit), "[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), " Sets the debug verbose level"; ] diff --git a/tests/bugs/double_atom.cnf b/tests/bugs/double_atom.cnf new file mode 100644 index 00000000..3c9abc3d --- /dev/null +++ b/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 + + diff --git a/tests/unsat/bug-01.cnf b/tests/unsat/bug-01.cnf new file mode 120000 index 00000000..5a72ddaf --- /dev/null +++ b/tests/unsat/bug-01.cnf @@ -0,0 +1 @@ +../bugs/double_atom.cnf \ No newline at end of file