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 dcc410c8a0
commit 9be4c66911
4 changed files with 46 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

68
src/core/internal.ml
View file

@ -315,10 +315,10 @@ module Make
*) *)
exception Trivial exception Trivial
let simplify_zero atoms level0 = let simplify_zero atoms =
(* Eliminates dead litterals from clauses when at decision level 0 (see above) *) (* Eliminates dead litterals from clauses when at decision level 0 (see above) *)
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 variable is true at level 0, then the clause is always satisfied *) (* If a variable is true at level 0, then the clause is always satisfied *)
if a.neg.is_true then begin if a.neg.is_true then begin
@ -327,10 +327,10 @@ module Make
| None | Some Decision -> assert false | None | Some Decision -> assert false
(* The var must have a reason, and it cannot be a decision, since we are (* The var must have a reason, and it cannot be a decision, since we are
at level 0. *) at level 0. *)
| Some (Bcp cl) -> atoms, cl :: history, max lvl cl.c_level | Some (Bcp cl) -> atoms, cl :: history
(* The variable has been set to false because of another clause, (* The variable has been set to false because of another clause,
we then need to keep track of the assumption level used. *) we then need to keep track of the assumption level used. *)
| Some (Semantic 0) -> atoms, history, lvl | Some (Semantic 0) -> atoms, history
(* Semantic propagations at level 0 are, well not easy to deal with, (* Semantic propagations at level 0 are, well not easy to deal with,
this shouldn't really happen actually (because semantic propagations this shouldn't really happen actually (because semantic propagations
at level 0 currently lack a proof). *) at level 0 currently lack a proof). *)
@ -339,43 +339,43 @@ module Make
(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
(* General case, we do not know the truth value of a, just let it be. *) (* General case, we do not know the truth value of a, just let it be. *)
in in
let atoms, init, lvl = List.fold_left aux ([], [], level0) atoms in let atoms, init = List.fold_left aux ([], []) atoms in
(* TODO: Why do we sort the atoms here ? *) (* TODO: Why do we sort the atoms here ? *)
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
(* Same as before, a var true at level 0 gives a trivially true clause *) (* Same as before, a var true at level 0 gives a trivially true clause *)
else (a::trues) @ unassigned @ falses @ r, history, lvl else (a::trues) @ unassigned @ falses @ r, history
(* A var true at level > 0 does not change anything, but is unlikely (* A var true at level > 0 does not change anything, but is unlikely
to be watched, so we put prefer to put them at the end. *) to be watched, so we put prefer to put them at the end. *)
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
(* Same as before, a var false at level 0 can be eliminated from the clause, (* Same as before, a var false at level 0 can be eliminated from the clause,
but we need to kepp in mind that we used another clause to simplify it. *) but we need to kepp in mind that we used another clause to simplify it. *)
| 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.
TODO: remove it or use it ? *) TODO: remove it or use it ? *)
@ -494,7 +494,7 @@ module Make
be able to build a correct proof at the end of proof search. *) be able to build a correct proof at the end of proof search. *)
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
@ -505,7 +505,7 @@ module Make
with only one formula (which is [a]). So we explicitly create that clause with only one formula (which is [a]). So we explicitly create that clause
and set it as the cause for the propagation of [a], that way we can and set it as the cause for the propagation of [a], that way we can
rebuild the whole resolution tree when we want to prove [a]. *) rebuild the whole resolution tree when we want to prove [a]. *)
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
@ -567,7 +567,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
@ -594,7 +593,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;
@ -607,7 +605,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
@ -623,7 +621,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;
@ -664,12 +661,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
@ -677,7 +673,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] ->
@ -686,13 +682,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;
@ -710,19 +706,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
| [] -> | [] ->
@ -731,7 +728,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;
@ -828,7 +825,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
Log.debugf 10 "Pushing clause %a" (fun k->k St.pp_clause c); Log.debugf 10 "Pushing clause %a" (fun k->k St.pp_clause c);
Stack.push c env.clauses_pushed Stack.push c env.clauses_pushed
@ -867,7 +864,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
@ -1053,7 +1050,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
src/core/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
src/core/solver_types.ml
View file

@ -182,18 +182,25 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
| Formula_intf.Negated -> var.na | Formula_intf.Negated -> var.na
| Formula_intf.Same_sign -> var.pa | Formula_intf.Same_sign -> 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
src/core/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} *)