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