simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

[bugfix] Clause level now computed at creation

Browse source 
Apart from new assumptions, clause level can always
be computed from the histoy of the clause, so it is
better to do it in Solver_types when creating clauses.
Aditionally, it seems there was an error in the manual
computing of clause level somewhere, this fixes the bug.
This commit is contained in:
Guillaume Bury 2016-07-09 03:06:21 +02:00
parent 1a0fc95147
commit 510a8aaa34
4 changed files with 46 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

68
solver/internal.ml
View file

@ -281,51 +281,51 @@ module Make
(* Simplify clauses *) (* Simplify clauses *)
exception Trivial exception Trivial
let simplify_zero atoms level0 = let simplify_zero atoms =
(* Eliminates dead litterals from clauses when at decision level 0 *) (* Eliminates dead litterals from clauses when at decision level 0 *)
assert (decision_level () = 0); assert (decision_level () = 0);
let aux (atoms, history, lvl) a = let aux (atoms, history) a =
if a.is_true then raise Trivial; if a.is_true then raise Trivial;
if a.neg.is_true then begin if a.neg.is_true then begin
match a.var.reason with match a.var.reason with
| None | Some Decision -> assert false | None | Some Decision -> assert false
| Some (Bcp cl) -> atoms, cl :: history, max lvl cl.c_level | Some (Bcp cl) -> atoms, cl :: history
| Some (Semantic 0) -> atoms, history, lvl | Some (Semantic 0) -> atoms, history
| Some (Semantic _) -> | Some (Semantic _) ->
Log.debugf 0 "Unexpected semantic propagation at level 0: %a" Log.debugf 0 "Unexpected semantic propagation at level 0: %a"
(fun k->k St.pp_atom a); (fun k->k St.pp_atom a);
assert false assert false
end else end else
a::atoms, history, lvl a::atoms, history
in in
let atoms, init, lvl = List.fold_left aux ([], [], level0) atoms in let atoms, init = List.fold_left aux ([], []) atoms in
List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init, lvl List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init
let partition atoms init0 = let partition atoms =
(* Parittion litterals for new clauses *) (* Parittion litterals for new clauses *)
let rec partition_aux trues unassigned falses history lvl = function let rec partition_aux trues unassigned falses history = function
| [] -> trues @ unassigned @ falses, history, lvl | [] -> trues @ unassigned @ falses, history
| a :: r -> | a :: r ->
if a.is_true then if a.is_true then
if a.var.v_level = 0 then raise Trivial if a.var.v_level = 0 then raise Trivial
else (a::trues) @ unassigned @ falses @ r, history, lvl else (a::trues) @ unassigned @ falses @ r, history
else if a.neg.is_true then else if a.neg.is_true then
if a.var.v_level = 0 then begin if a.var.v_level = 0 then begin
match a.var.reason with match a.var.reason with
| Some (Bcp cl) -> | Some (Bcp cl) ->
partition_aux trues unassigned falses (cl :: history) (max lvl cl.c_level) r partition_aux trues unassigned falses (cl :: history) r
| Some (Semantic 0) -> | Some (Semantic 0) ->
partition_aux trues unassigned falses history lvl r partition_aux trues unassigned falses history r
| _ -> assert false | _ -> assert false
end else end else
partition_aux trues unassigned (a::falses) history lvl r partition_aux trues unassigned (a::falses) history r
else else
partition_aux trues (a::unassigned) falses history lvl r partition_aux trues (a::unassigned) falses history r
in in
if decision_level () = 0 then if decision_level () = 0 then
simplify_zero atoms init0 simplify_zero atoms
else else
partition_aux [] [] [] [] init0 atoms partition_aux [] [] [] [] atoms
(* Compute a progess estimate *) (* Compute a progess estimate *)
let progress_estimate () = let progress_estimate () =
@ -413,12 +413,12 @@ module Make
let simpl_reason = function let simpl_reason = function
| (Bcp cl) as r -> | (Bcp cl) as r ->
let l, history, c_lvl = partition (Vec.to_list cl.atoms) 0 in let l, history = partition (Vec.to_list cl.atoms) in
begin match l with begin match l with
| [ a ] -> | [ a ] ->
if history = [] then r if history = [] then r
else else
let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) c_lvl in let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) in
Bcp tmp_cl Bcp tmp_cl
| _ -> assert false | _ -> assert false
end end
@ -478,7 +478,6 @@ module Make
let is_uip = ref false in let is_uip = ref false in
let c = ref (Proof.to_list c_clause) in let c = ref (Proof.to_list c_clause) in
let history = ref [c_clause] in let history = ref [c_clause] in
let c_level = ref 0 in
clause_bump_activity c_clause; clause_bump_activity c_clause;
let is_semantic a = match a.var.reason with let is_semantic a = match a.var.reason with
| Some Semantic _ -> true | Some Semantic _ -> true
@ -505,7 +504,6 @@ module Make
begin match tmp with begin match tmp with
| [] -> () | [] -> ()
| [b] when b == a.var.pa -> | [b] when b == a.var.pa ->
c_level := max !c_level d.c_level;
clause_bump_activity d; clause_bump_activity d;
var_bump_activity a.var; var_bump_activity a.var;
history := d :: !history; history := d :: !history;
@ -518,7 +516,7 @@ module Make
with Exit -> with Exit ->
let learnt = List.sort (fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in let learnt = List.sort (fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in
let blevel = backtrack_lvl !is_uip learnt in let blevel = backtrack_lvl !is_uip learnt in
blevel, learnt, List.rev !history, !is_uip, !c_level blevel, learnt, List.rev !history, !is_uip
let get_atom i = let get_atom i =
match Vec.get env.elt_queue i with match Vec.get env.elt_queue i with
@ -534,7 +532,6 @@ module Make
let tr_ind = ref (Vec.size env.elt_queue - 1) in let tr_ind = ref (Vec.size env.elt_queue - 1) in
let size = ref 1 in let size = ref 1 in
let history = ref [] in let history = ref [] in
let c_level = ref 0 in
assert (decision_level () > 0); assert (decision_level () > 0);
while !cond do while !cond do
if !c.learnt then clause_bump_activity !c; if !c.learnt then clause_bump_activity !c;
@ -575,12 +572,11 @@ module Make
cond := false; cond := false;
learnt := p.neg :: (List.rev !learnt) learnt := p.neg :: (List.rev !learnt)
| n, Some Bcp cl -> | n, Some Bcp cl ->
c_level := max !c_level cl.c_level;
c := cl c := cl
| n, _ -> assert false | n, _ -> assert false
done; done;
List.iter (fun q -> q.var.seen <- false) !seen; List.iter (fun q -> q.var.seen <- false) !seen;
!blevel, !learnt, List.rev !history, true, !c_level !blevel, !learnt, List.rev !history, true
let analyze c_clause = let analyze c_clause =
if St.mcsat then if St.mcsat then
@ -588,7 +584,7 @@ module Make
else else
analyze_sat c_clause analyze_sat c_clause
let record_learnt_clause confl blevel learnt history is_uip lvl = let record_learnt_clause confl blevel learnt history is_uip =
begin match learnt with begin match learnt with
| [] -> assert false | [] -> assert false
| [fuip] -> | [fuip] ->
@ -597,13 +593,13 @@ module Make
report_unsat confl report_unsat confl
else begin else begin
let name = fresh_lname () in let name = fresh_lname () in
let uclause = make_clause name learnt (List.length learnt) true history lvl in let uclause = make_clause name learnt (List.length learnt) true history in
Vec.push env.clauses_learnt uclause; Vec.push env.clauses_learnt uclause;
enqueue_bool fuip 0 (Bcp uclause) enqueue_bool fuip 0 (Bcp uclause)
end end
| fuip :: _ -> | fuip :: _ ->
let name = fresh_lname () in let name = fresh_lname () in
let lclause = make_clause name learnt (List.length learnt) true history lvl in let lclause = make_clause name learnt (List.length learnt) true history in
Vec.push env.clauses_learnt lclause; Vec.push env.clauses_learnt lclause;
attach_clause lclause; attach_clause lclause;
clause_bump_activity lclause; clause_bump_activity lclause;
@ -621,19 +617,20 @@ module Make
env.conflicts <- env.conflicts + 1; env.conflicts <- env.conflicts + 1;
if decision_level() = 0 || Vec.for_all (fun a -> a.var.v_level = 0) confl.atoms then if decision_level() = 0 || Vec.for_all (fun a -> a.var.v_level = 0) confl.atoms then
report_unsat confl; (* Top-level conflict *) report_unsat confl; (* Top-level conflict *)
let blevel, learnt, history, is_uip, lvl = analyze confl in let blevel, learnt, history, is_uip = analyze confl in
cancel_until blevel; cancel_until blevel;
record_learnt_clause confl blevel learnt (History history) is_uip lvl record_learnt_clause confl blevel learnt (History history) is_uip
(* Add a new clause *) (* Add a new clause *)
let add_clause ?(force=false) init0 = let add_clause ?(force=false) init0 =
Log.debugf 90 "Adding clause:@[<hov>%a@]" (fun k -> k St.pp_clause init0);
let vec = match init0.cpremise with let vec = match init0.cpremise with
| Lemma _ -> env.clauses_learnt | Lemma _ -> env.clauses_learnt
| History [] -> env.clauses_hyps | History [] -> env.clauses_hyps
| History _ -> assert false | History _ -> assert false
in in
try try
let atoms, history, level = partition (Vec.to_list init0.atoms) init0.c_level in let atoms, history = partition (Vec.to_list init0.atoms) in
let size = List.length atoms in let size = List.length atoms in
match atoms with match atoms with
| [] -> | [] ->
@ -642,7 +639,7 @@ module Make
| a::b::_ -> | a::b::_ ->
let clause = let clause =
if history = [] then init0 if history = [] then init0
else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History (init0 :: history)) level else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History (init0 :: history))
in in
Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause); Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause);
attach_clause clause; attach_clause clause;
@ -737,7 +734,7 @@ module Make
let atoms = List.rev_map (fun x -> new_atom x) l in let atoms = List.rev_map (fun x -> new_atom x) l in
Iheap.grow_to_by_double env.order (St.nb_elt ()); Iheap.grow_to_by_double env.order (St.nb_elt ());
List.iter (fun a -> insert_var_order (elt_of_var a.var)) atoms; List.iter (fun a -> insert_var_order (elt_of_var a.var)) atoms;
let c = make_clause (fresh_tname ()) atoms (List.length atoms) true (Lemma lemma) base_level in let c = make_clause (fresh_tname ()) atoms (List.length atoms) true (Lemma lemma) in
add_clause c add_clause c
let slice_propagate f lvl = let slice_propagate f lvl =
@ -775,7 +772,7 @@ module Make
let l = List.rev_map new_atom l in let l = List.rev_map new_atom l in
Iheap.grow_to_by_double env.order (St.nb_elt ()); Iheap.grow_to_by_double env.order (St.nb_elt ());
List.iter (fun a -> insert_var_order (elt_of_var a.var)) l; List.iter (fun a -> insert_var_order (elt_of_var a.var)) l;
let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) base_level in let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) in
Some c Some c
end end
@ -956,7 +953,8 @@ module Make
let add_clauses ?tag cnf = let add_clauses ?tag cnf =
let aux cl = let aux cl =
let c = make_clause ?tag (fresh_hname ()) cl (List.length cl) false (History []) (current_level ()) in let c = make_clause ?tag ~lvl:(current_level ())
(fresh_hname ()) cl (List.length cl) false (History []) in
add_clause c; add_clause c;
(* Clauses can be added after search has begun (and thus we are not at level 0, (* Clauses can be added after search has begun (and thus we are not at level 0,
so better not do anything at this point. so better not do anything at this point.

3
solver/res.ml
View file

@ -94,7 +94,6 @@ module Make(St : Solver_types.S) = struct
| _ -> assert false) l | _ -> assert false) l
in in
St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l)) St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l))
(List.fold_left (fun i c -> max i c.St.c_level) 0 l)
let prove_atom a = 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 begin
@ -128,7 +127,7 @@ module Make(St : Solver_types.S) = struct
| [] -> (l, c, d, a) | [] -> (l, c, d, a)
| _ -> | _ ->
let new_clause = St.make_clause (fresh_pcl_name ()) l (List.length l) true let new_clause = St.make_clause (fresh_pcl_name ()) l (List.length l) true
(St.History [c; d]) (max c.St.c_level d.St.c_level) in (St.History [c; d]) in
chain_res (new_clause, l) r chain_res (new_clause, l) r
end end
| _ -> assert false | _ -> assert false

13
solver/solver_types.ml
View file

@ -179,18 +179,25 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
let var, negated = make_boolean_var lit in let var, negated = make_boolean_var lit in
if negated then var.na else var.pa if negated then var.na else var.pa
let make_clause ?tag name ali sz_ali is_learnt premise lvl = let make_clause ?tag ?lvl name ali sz_ali is_learnt premise =
let atoms = Vec.from_list ali sz_ali dummy_atom in let atoms = Vec.from_list ali sz_ali dummy_atom in
let level =
match lvl, premise with
| Some lvl, History [] -> lvl
| Some _, _ -> assert false
| None, History l -> List.fold_left (fun lvl c -> max lvl c.c_level) 0 l
| None, Lemma _ -> 0
in
{ name = name; { name = name;
tag = tag; tag = tag;
atoms = atoms; atoms = atoms;
removed = false; removed = false;
learnt = is_learnt; learnt = is_learnt;
c_level = lvl; c_level = level;
activity = 0.; activity = 0.;
cpremise = premise} cpremise = premise}
let empty_clause = make_clause "Empty" [] 0 false (History []) 0 let empty_clause = make_clause "Empty" [] 0 false (History [])
(* Decisions & propagations *) (* Decisions & propagations *)
type t = (lit, atom) Either.t type t = (lit, atom) Either.t

4
solver/solver_types_intf.ml
View file

@ -115,8 +115,8 @@ module type S = sig
val empty_clause : clause val empty_clause : clause
(** The empty clause *) (** The empty clause *)
val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> int -> clause val make_clause : ?tag:int -> ?lvl:int -> string -> atom list -> int -> bool -> premise -> clause
(** [make_clause name atoms size learnt premise level] creates a clause with the given attributes. *) (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *)
(** {2 Clause names} *) (** {2 Clause names} *)