From 2613926ab15dc1bf7ca895e1a0653f4d99cc8cb6 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 21 Jan 2016 00:06:41 +0100 Subject: [PATCH] First changes for better persistent proofs This commit ensures that clauses now contain all necessary information to construct the proof graph (without relying on propagation reasons). --- solver/internal.ml | 104 ++++++++++++++++++++++-------------- solver/res.ml | 8 ++- solver/solver_types_intf.ml | 2 +- tests/run | 2 +- 4 files changed, 73 insertions(+), 43 deletions(-) diff --git a/solver/internal.ml b/solver/internal.ml index 194ec234..b68b44a7 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -261,46 +261,46 @@ module Make let simplify_zero atoms level0 = (* Eliminates dead litterals from clauses when at decision level 0 *) assert (decision_level () = 0); - let aux (atoms, init, lvl) a = + let aux (atoms, history, lvl) a = if a.is_true then raise Trivial; if a.neg.is_true then begin match a.var.reason with - | Bcp (Some cl) -> atoms, false, max lvl cl.c_level - | Semantic 0 -> atoms, init, lvl + | Bcp (Some cl) -> atoms, cl :: history, max lvl cl.c_level + | Semantic 0 -> atoms, history, lvl | _ -> L.debug 0 "Unexpected semantic propagation at level 0: %a" St.pp_atom a; assert false end else - a::atoms, init, lvl + a::atoms, history, lvl in - let atoms, init, lvl = List.fold_left aux ([], true, level0) atoms in + let atoms, init, lvl = List.fold_left aux ([], [], level0) atoms in List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init, lvl let partition atoms init0 = (* Parittion litterals for new clauses *) - let rec partition_aux trues unassigned falses init lvl = function - | [] -> trues @ unassigned @ falses, init, lvl + let rec partition_aux trues unassigned falses history lvl = function + | [] -> trues @ unassigned @ falses, history, lvl | a :: r -> if a.is_true then if a.var.level = 0 then raise Trivial - else (a::trues) @ unassigned @ falses @ r, init, lvl + else (a::trues) @ unassigned @ falses @ r, history, lvl else if a.neg.is_true then if a.var.level = 0 then begin match a.var.reason with | Bcp (Some cl) -> - partition_aux trues unassigned falses false (max lvl cl.c_level) r + partition_aux trues unassigned falses (cl :: history) (max lvl cl.c_level) r | Semantic 0 -> - partition_aux trues unassigned falses init lvl r + partition_aux trues unassigned falses history lvl r | _ -> assert false end else - partition_aux trues unassigned (a::falses) init lvl r + partition_aux trues unassigned (a::falses) history lvl r else - partition_aux trues (a::unassigned) falses init lvl r + partition_aux trues (a::unassigned) falses history lvl r in if decision_level () = 0 then simplify_zero atoms init0 else - partition_aux [] [] [] false init0 atoms + partition_aux [] [] [] [] init0 atoms (* Compute a progess estimate *) let progress_estimate () = @@ -386,6 +386,19 @@ module Make env.unsat_conflict <- Some confl; raise Unsat + let simpl_reason = function + | (Bcp Some cl) as r -> + let l, history, c_lvl = partition (Vec.to_list cl.atoms) 0 in + begin match l with + | [ a ] -> + if history = [] then r + else + let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (List.rev (cl :: history))) c_lvl in + Bcp (Some tmp_cl) + | _ -> assert false + end + | r -> r + let enqueue_bool a lvl reason = if a.neg.is_true then begin L.debug 0 "Trying to enqueue a false litteral: %a" St.pp_atom a; @@ -393,6 +406,10 @@ module Make end; if not a.is_true then begin assert (a.var.level < 0 && a.var.reason = Bcp None && lvl >= 0); + let reason = + if lvl > 0 then reason + else simpl_reason reason + in a.is_true <- true; a.var.level <- lvl; a.var.reason <- reason; @@ -490,6 +507,7 @@ module Make let size = ref 1 in let history = ref [] in let c_level = ref 0 in + assert (decision_level () > 0); while !cond do if !c.learnt then clause_bump_activity !c; history := !c :: !history; @@ -497,16 +515,24 @@ module Make for j = 0 to Vec.size !c.atoms - 1 do let q = Vec.get !c.atoms j in assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) - if not q.var.seen && q.var.level > 0 then begin - var_bump_activity q.var; + if q.var.level = 0 then begin + assert (q.neg.is_true); + match q.var.reason with + | Bcp Some cl -> history := cl :: !history + | _ -> assert false + end; + if not q.var.seen then begin q.var.seen <- true; seen := q :: !seen; - if q.var.level >= decision_level () then begin - incr pathC - end else begin - learnt := q :: !learnt; - incr size; - blevel := max !blevel q.var.level + if q.var.level > 0 then begin + var_bump_activity q.var; + if q.var.level >= decision_level () then begin + incr pathC + end else begin + learnt := q :: !learnt; + incr size; + blevel := max !blevel q.var.level + end end end done; @@ -589,8 +615,8 @@ module Make report_unsat init0 | a::b::_ -> let clause = - if init then init0 - else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History [init0]) level + if history = [] then init0 + else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History (init0 :: history)) level in L.debug 4 "New clause: %a" St.pp_clause clause; attach_clause clause; @@ -839,20 +865,20 @@ module Make | Some atom -> env.next_decision <- None; pick_branch_aux atom - | None -> - destruct_elt ( - St.get_elt @@ Iheap.remove_min f_weight env.order) - (fun v -> - if v.level >= 0 then - pick_branch_lit () - else begin - let value = Th.assign v.term in - env.decisions <- env.decisions + 1; - new_decision_level(); - let current_level = decision_level () in - enqueue_assign v value current_level - end) - (fun v -> pick_branch_aux v.pa) + | None -> + destruct_elt ( + St.get_elt @@ Iheap.remove_min f_weight env.order) + (fun v -> + if v.level >= 0 then + pick_branch_lit () + else begin + let value = Th.assign v.term in + env.decisions <- env.decisions + 1; + new_decision_level(); + let current_level = decision_level () in + enqueue_assign v value current_level + end) + (fun v -> pick_branch_aux v.pa) let search n_of_conflicts n_of_learnts = let conflictC = ref 0 in @@ -919,7 +945,7 @@ module Make Th.if_sat (full_slice ()); if is_unsat () then raise Unsat else if env.nb_init_clauses = nbc && - env.elt_head = Vec.size env.elt_queue then + env.elt_head = Vec.size env.elt_queue then raise Sat end done @@ -1044,7 +1070,7 @@ module Make (if i = ul.ul_elt_lvl then "*" else " ") (if i = ul.ul_th_lvl then "*" else " ") i (fun fmt e -> - destruct e (St.pp_lit fmt) (St.pp_atom fmt)) (Vec.get env.elt_queue i) + destruct e (St.pp_lit fmt) (St.pp_atom fmt)) (Vec.get env.elt_queue i) done; (* Clear hypothesis not valid anymore *) diff --git a/solver/res.ml b/solver/res.ml index d6d7b504..85f56aad 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -167,8 +167,11 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct | a :: r -> L.debug 5 "Resolving (with history) %a" St.pp_clause c; let temp_c, temp_cl = List.fold_left add_res a r in - L.debug 10 " Switching to unit resolutions"; - let new_c, new_cl = (ref temp_c, ref temp_cl) in + let tmp = diff_learnt [] cl temp_cl in + List.iter (fun a -> + L.debug 0 " -> %a" St.pp_atom a) tmp; + assert (equal_cl cl temp_cl) + (* while not (equal_cl cl !new_cl) do let unit_to_use = diff_learnt [] cl !new_cl in let unit_r = List.map (fun a -> clause_unit a) unit_to_use in @@ -177,6 +180,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct new_c := temp_c; new_cl := temp_cl; done + *) | _ -> assert false and do_clause = function diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml index 133a1ddc..d3b09ee0 100644 --- a/solver/solver_types_intf.ml +++ b/solver/solver_types_intf.ml @@ -119,7 +119,7 @@ module type S = sig val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> int -> clause (** [make_clause name atoms size learnt premise level] creates a clause with the given attributes. *) - (** {2 Proof management} *) + (** {2 Clause names} *) val fresh_name : unit -> string val fresh_lname : unit -> string diff --git a/tests/run b/tests/run index 18241eb1..99c4613b 100755 --- a/tests/run +++ b/tests/run @@ -7,7 +7,7 @@ solvertest () { for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'` do echo -ne "\r\033[KTesting $f..." - "$SOLVER" -s $3 -time 30s -size 1G $f | grep $2 + "$SOLVER" -s $3 -time 30s -size 1G -check $f | grep $2 RET=$? if [ $RET -ne 0 ]; then