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

Clause atoms are now in an array instead of a vec

Browse source
This commit is contained in:
Guillaume Bury 2016-07-18 18:42:15 +02:00
parent 933943c4e3
commit 38b4fde5c1
5 changed files with 52 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/backend/dot.ml
View file

@ -20,12 +20,12 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm
let print_clause fmt c =
let v = c.S.St.atoms in
if Vec.is_empty v then
if Array.length v = 0 then
Format.fprintf fmt "⊥"
else
let n = Vec.size v in
let n = Array.length v in
for i = 0 to n - 1 do
Format.fprintf fmt "%a" A.print_atom (Vec.get v i);
Format.fprintf fmt "%a" A.print_atom v.(i);
if i < n - 1 then
Format.fprintf fmt ", "
done

61
src/core/internal.ml
View file

@ -414,20 +414,20 @@ module Make
if not c.attached then begin
Log.debugf 60 "Attaching %a" (fun k -> k St.pp_clause c);
c.attached <- true;
Vec.push (Vec.get c.atoms 0).neg.watched c;
Vec.push (Vec.get c.atoms 1).neg.watched c;
Vec.push c.atoms.(0).neg.watched c;
Vec.push c.atoms.(1).neg.watched c;
end
let detach_clause c =
if c.attached then begin
c.attached <- false;
Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c);
Vec.remove (Vec.get c.atoms 0).neg.watched c;
Vec.remove (Vec.get c.atoms 1).neg.watched c;
Vec.remove c.atoms.(0).neg.watched c;
Vec.remove c.atoms.(1).neg.watched c;
end
(* Is a clause satisfied ? *)
let satisfied c = Vec.exists (fun atom -> atom.is_true) c.atoms
let satisfied c = Array.exists (fun atom -> atom.is_true) c.atoms
(* Backtracking.
Used to backtrack, i.e cancel down to [lvl] excluded,
@ -494,7 +494,7 @@ module Make
be able to build a correct proof at the end of proof search. *)
let simpl_reason = function
| (Bcp cl) as r ->
let atoms = Vec.to_list cl.atoms in
let atoms = Array.to_list cl.atoms in
let l, history = partition atoms in
begin match l with
| [ a ] ->
@ -506,7 +506,7 @@ module Make
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
rebuild the whole resolution tree when we want to prove [a]. *)
Bcp (make_clause (fresh_tname ()) l 1 (History (cl :: history)))
Bcp (make_clause (fresh_tname ()) l (History (cl :: history)))
| _ -> assert false
end
| r -> r
@ -630,8 +630,8 @@ module Make
end;
history := !c :: !history;
(* visit the current predecessors *)
for j = 0 to Vec.size !c.atoms - 1 do
let q = Vec.get !c.atoms j in
for j = 0 to Array.length !c.atoms - 1 do
let q = !c.atoms.(j) in
assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* Pas sur *)
if q.var.v_level = 0 then begin
assert (q.neg.is_true);
@ -686,13 +686,13 @@ module Make
report_unsat confl
else begin
let name = fresh_lname () in
let uclause = make_clause name learnt (List.length learnt) history in
let uclause = make_clause name learnt history in
Vec.push env.clauses_learnt uclause;
enqueue_bool fuip 0 (Bcp uclause)
end
| fuip :: _ ->
let name = fresh_lname () in
let lclause = make_clause name learnt (List.length learnt) history in
let lclause = make_clause name learnt history in
Vec.push env.clauses_learnt lclause;
attach_clause lclause;
clause_bump_activity lclause;
@ -708,7 +708,7 @@ module Make
let add_boolean_conflict confl =
env.next_decision <- None;
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 || Array.for_all (fun a -> a.var.v_level = 0) confl.atoms then
report_unsat confl; (* Top-level conflict *)
let blevel, learnt, history, is_uip = analyze confl in
cancel_until blevel;
@ -723,12 +723,10 @@ module Make
| History _ -> assert false
in
try
let atoms, history = partition (Vec.to_list init.atoms) in
let size = List.length atoms in
let atoms, history = partition (Array.to_list init.atoms) in
let clause =
if history = [] then init
else make_clause ?tag:init.tag (fresh_name ())
atoms size (History (init :: history))
else make_clause ?tag:init.tag (fresh_name ()) atoms (History (init :: history))
in
Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause);
Vec.push vec clause;
@ -737,8 +735,8 @@ module Make
report_unsat clause
| a::b::_ ->
if a.neg.is_true then begin
Vec.sort clause.atoms (fun a b ->
compare b.var.v_level a.var.v_level);
Array.sort (fun a b ->
compare b.var.v_level a.var.v_level) clause.atoms;
attach_clause clause;
add_boolean_conflict init
end else begin
@ -759,24 +757,24 @@ module Make
let propagate_in_clause a c i watched new_sz =
let atoms = c.atoms in
let first = Vec.get atoms 0 in
let first = atoms.(0) in
if first == a.neg then begin (* false lit must be at index 1 *)
Vec.set atoms 0 (Vec.get atoms 1);
Vec.set atoms 1 first
atoms.(0) <- atoms.(1);
atoms.(1) <- first
end;
let first = Vec.get atoms 0 in
let first = atoms.(0) in
if first.is_true then begin
(* true clause, keep it in watched *)
Vec.set watched !new_sz c;
incr new_sz;
end else
try (* look for another watch lit *)
for k = 2 to Vec.size atoms - 1 do
let ak = Vec.get atoms k in
for k = 2 to Array.length atoms - 1 do
let ak = atoms.(k) in
if not (ak.neg.is_true) then begin
(* watch lit found: update and exit *)
Vec.set atoms 1 ak;
Vec.set atoms k a.neg;
atoms.(1) <- ak;
atoms.(k) <- a.neg;
Vec.push ak.neg.watched c;
raise Exit
end
@ -832,7 +830,7 @@ module Make
let atoms = List.rev_map (fun x -> new_atom x) l in
Iheap.grow_to_by_double env.order (St.nb_elt ());
List.iter (fun a -> insert_var_order (elt_of_var a.var)) atoms;
let c = make_clause (fresh_tname ()) atoms (List.length atoms) (Lemma lemma) in
let c = make_clause (fresh_tname ()) atoms (Lemma lemma) in
Log.debugf 10 "Pushing clause %a" (fun k->k St.pp_clause c);
Stack.push c env.clauses_pushed
@ -871,7 +869,7 @@ module Make
let l = List.rev_map new_atom l in
Iheap.grow_to_by_double env.order (St.nb_elt ());
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) (Lemma p) in
let c = St.make_clause (St.fresh_tname ()) l (Lemma p) in
Some c
end
@ -1046,9 +1044,8 @@ module Make
let check_clause c =
let b = ref false in
let atoms = c.atoms in
for i = 0 to Vec.size atoms - 1 do
let a = Vec.get atoms i in
b := !b || a.is_true
for i = 0 to Array.length atoms - 1 do
b := !b || atoms.(i).is_true
done;
assert (!b)
@ -1058,7 +1055,7 @@ module Make
let add_clauses ?tag cnf =
let aux cl =
let c = make_clause ?tag (fresh_hname ())
cl (List.length cl) (Hyp (current_level ())) in
cl (Hyp (current_level ())) in
add_clause c;
(* Clauses can be added after search has begun (and thus we are not at level 0,
so better not do anything at this point.

17
src/core/res.ml
View file

@ -56,11 +56,8 @@ module Make(St : Solver_types.S) = struct
let to_list c =
let v = St.(c.atoms) in
let l = ref [] in
for i = 0 to Vec.size v - 1 do
l := (Vec.get v i) :: !l
done;
let res = sort_uniq compare_atoms !l 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";
@ -87,19 +84,19 @@ module Make(St : Solver_types.S) = struct
conclusion
let prove_unsat c =
let l = Vec.to_list c.St.atoms in
let l = Array.to_list c.St.atoms in
let l = List.map (fun a ->
match St.(a.var.reason) with
| Some St.Bcp d -> d
| _ -> assert false) l
in
St.make_clause (fresh_pcl_name ()) [] 0 (St.History (c :: l))
St.make_clause (fresh_pcl_name ()) [] (St.History (c :: l))
let prove_atom a =
if St.(a.is_true && a.var.v_level = 0) then begin
match St.(a.var.reason) with
| Some St.Bcp c ->
assert (Vec.size St.(c.atoms) = 1 && equal_atoms a (Vec.get St.(c.atoms) 0));
assert (Array.length St.(c.atoms) = 1 && equal_atoms a St.(c.atoms).(0));
Some c
| _ -> assert false
end else
@ -127,7 +124,7 @@ module Make(St : Solver_types.S) = struct
| [] -> (l, c, d, a)
| _ ->
let new_clause = St.make_clause (fresh_pcl_name ())
l (List.length l) (St.History [c; d]) in
l (St.History [c; d]) in
chain_res (new_clause, l) r
end
| _ -> assert false
@ -183,7 +180,7 @@ module Make(St : Solver_types.S) = struct
module H = Hashtbl.Make(struct
type t = clause
let hash cl =
Vec.fold (fun i a -> Hashtbl.hash St.(a.aid, i)) 0 cl.St.atoms
Array.fold_left (fun i a -> Hashtbl.hash St.(a.aid, i)) 0 cl.St.atoms
let equal = (==)
end)

22
src/core/solver_types.ml
View file

@ -57,7 +57,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
and clause = {
name : string;
tag : int option;
atoms : atom Vec.t;
atoms : atom array;
c_level : int;
mutable cpremise : premise;
mutable activity : float;
@ -101,7 +101,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
let dummy_clause =
{ name = "";
tag = None;
atoms = Vec.make_empty dummy_atom;
atoms = [| |];
activity = -1.;
attached = false;
c_level = -1;
@ -183,8 +183,8 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
| Formula_intf.Negated -> var.na
| Formula_intf.Same_sign -> var.pa
let make_clause ?tag name ali sz_ali premise =
let atoms = Vec.from_list ali sz_ali dummy_atom in
let make_clause ?tag name ali premise =
let atoms = Array.of_list ali in
let level =
match premise with
| Hyp lvl -> lvl
@ -200,7 +200,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
activity = 0.;
cpremise = premise}
let empty_clause = make_clause "Empty" [] 0 (History [])
let empty_clause = make_clause "Empty" [] (History [])
(* Decisions & propagations *)
type t = (lit, atom) Either.t
@ -248,13 +248,13 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
let print_atom fmt a = E.Formula.print fmt a.lit
let print_atoms fmt v =
if Vec.size v = 0 then
if Array.length v = 0 then
Format.fprintf fmt "∅"
else begin
print_atom fmt (Vec.get v 0);
if (Vec.size v) > 1 then begin
for i = 1 to (Vec.size v) - 1 do
Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i)
print_atom fmt v.(0);
if (Array.length v) > 1 then begin
for i = 1 to (Array.length v) - 1 do
Format.fprintf fmt " ∨ %a" print_atom v.(i)
done
end
end
@ -296,7 +296,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
(sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
let pp_atoms_vec out vec =
Vec.print ~sep:"" pp_atom out vec
Array.iter (fun a -> pp_atom out a) vec
let pp_clause out {name=name; atoms=arr; cpremise=cp; } =
Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"

4
src/core/solver_types_intf.ml
View file

@ -52,7 +52,7 @@ module type S = sig
and clause = {
name : string;
tag : int option;
atoms : atom Vec.t;
atoms : atom array;
c_level : int;
mutable cpremise : premise;
mutable activity : float;
@ -116,7 +116,7 @@ module type S = sig
val empty_clause : clause
(** The empty clause *)
val make_clause : ?tag:int -> string -> atom list -> int -> premise -> clause
val make_clause : ?tag:int -> string -> atom list -> premise -> clause
(** [make_clause name atoms size premise] creates a clause with the given attributes. *)
(** {2 Clause names} *)