simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 19:55:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: cleanup SAT

Browse source
This commit is contained in:
Simon Cruanes 2018-05-25 21:32:29 -05:00
parent 9b8c21513a
commit 0b42a34a20
1 changed files with 46 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

90
src/sat/Internal.ml
View file

@ -22,9 +22,9 @@ module Make (Th : Theory_intf.S) = struct
type lemma = Th.proof type lemma = Th.proof
type var = { type var = {
vid : int; v_id : int;
pa : atom; v_pa : atom;
na : atom; v_na : atom;
mutable v_fields : Var_fields.t; mutable v_fields : Var_fields.t;
mutable v_level : int; mutable v_level : int;
mutable v_idx: int; (** position in heap *) mutable v_idx: int; (** position in heap *)
@ -33,7 +33,7 @@ module Make (Th : Theory_intf.S) = struct
} }
and atom = { and atom = {
aid : int; a_id : int;
var : var; var : var;
neg : atom; neg : atom;
lit : formula; lit : formula;
@ -64,9 +64,9 @@ module Make (Th : Theory_intf.S) = struct
type proof = clause type proof = clause
let rec dummy_var = let rec dummy_var =
{ vid = -101; { v_id = -101;
pa = dummy_atom; v_pa = dummy_atom;
na = dummy_atom; v_na = dummy_atom;
v_fields = Var_fields.empty; v_fields = Var_fields.empty;
v_level = -1; v_level = -1;
v_weight = -1.; v_weight = -1.;
@ -81,7 +81,7 @@ module Make (Th : Theory_intf.S) = struct
but we have to break the cycle *) but we have to break the cycle *)
neg = dummy_atom; neg = dummy_atom;
is_true = false; is_true = false;
aid = -102; a_id = -102;
} }
let dummy_clause = let dummy_clause =
{ name = -1; { name = -1;
@ -237,12 +237,12 @@ module Make (Th : Theory_intf.S) = struct
type t = var type t = var
let dummy = dummy_var let dummy = dummy_var
let[@inline] level v = v.v_level let[@inline] level v = v.v_level
let[@inline] pos v = v.pa let[@inline] pos v = v.v_pa
let[@inline] neg v = v.na let[@inline] neg v = v.v_na
let[@inline] reason v = v.reason let[@inline] reason v = v.reason
let[@inline] weight v = v.v_weight let[@inline] weight v = v.v_weight
let[@inline] id v = v.vid let[@inline] id v = v.v_id
let[@inline] level v = v.v_level let[@inline] level v = v.v_level
let[@inline] idx v = v.v_idx let[@inline] idx v = v.v_idx
@ -259,29 +259,29 @@ module Make (Th : Theory_intf.S) = struct
with Not_found -> with Not_found ->
let cpt_double = st.cpt_mk_var lsl 1 in let cpt_double = st.cpt_mk_var lsl 1 in
let rec var = let rec var =
{ vid = st.cpt_mk_var; { v_id = st.cpt_mk_var;
pa = pa; v_pa = v_pa;
na = na; v_na = v_na;
v_fields = Var_fields.empty; v_fields = Var_fields.empty;
v_level = -1; v_level = -1;
v_idx= -1; v_idx= -1;
v_weight = 0.; v_weight = 0.;
reason = None; reason = None;
} }
and pa = and v_pa =
{ var = var; { var = var;
lit = lit; lit = lit;
watched = Vec.make 10 dummy_clause; watched = Vec.make 10 dummy_clause;
neg = na; neg = v_na;
is_true = false; is_true = false;
aid = cpt_double (* aid = vid*2 *) } a_id = cpt_double (* a_id = v_id*2 *) }
and na = and v_na =
{ var = var; { var = var;
lit = Th.Form.neg lit; lit = Th.Form.neg lit;
watched = Vec.make 10 dummy_clause; watched = Vec.make 10 dummy_clause;
neg = pa; neg = v_pa;
is_true = false; is_true = false;
aid = cpt_double + 1 (* aid = vid*2+1 *) } in a_id = cpt_double + 1 (* a_id = v_id*2+1 *) } in
MF.add st.f_map lit var; MF.add st.f_map lit var;
st.cpt_mk_var <- st.cpt_mk_var + 1; st.cpt_mk_var <- st.cpt_mk_var + 1;
Vec.push st.vars var; Vec.push st.vars var;
@ -295,7 +295,7 @@ module Make (Th : Theory_intf.S) = struct
Var_fields.get v_field_seen_pos v.v_fields && Var_fields.get v_field_seen_pos v.v_fields &&
Var_fields.get v_field_seen_neg v.v_fields Var_fields.get v_field_seen_neg v.v_fields
let pp out (v:t) = Th.Form.print out v.pa.lit let pp out (v:t) = Th.Form.print out v.v_pa.lit
end end
module Atom = struct module Atom = struct
@ -304,13 +304,13 @@ module Make (Th : Theory_intf.S) = struct
let[@inline] level a = a.var.v_level let[@inline] level a = a.var.v_level
let[@inline] var a = a.var let[@inline] var a = a.var
let[@inline] neg a = a.neg let[@inline] neg a = a.neg
let[@inline] abs a = a.var.pa let[@inline] abs a = a.var.v_pa
let[@inline] get_formula a = a.lit let[@inline] get_formula a = a.lit
let[@inline] equal a b = a == b let[@inline] equal a b = a == b
let[@inline] is_pos a = a == abs a let[@inline] is_pos a = a == abs a
let[@inline] compare a b = Pervasives.compare a.aid b.aid let[@inline] compare a b = Pervasives.compare a.a_id b.a_id
let[@inline] reason a = Var.reason a.var let[@inline] reason a = Var.reason a.var
let[@inline] id a = a.aid let[@inline] id a = a.a_id
let[@inline] is_true a = a.is_true let[@inline] is_true a = a.is_true
let[@inline] is_false a = a.neg.is_true let[@inline] is_false a = a.neg.is_true
@ -329,8 +329,8 @@ module Make (Th : Theory_intf.S) = struct
let[@inline] make st lit = let[@inline] make st lit =
let var, negated = Var.make st lit in let var, negated = Var.make st lit in
match negated with match negated with
| Theory_intf.Negated -> var.na | Theory_intf.Negated -> var.v_na
| Theory_intf.Same_sign -> var.pa | Theory_intf.Same_sign -> var.v_pa
let pp fmt a = Th.Form.print fmt a.lit let pp fmt a = Th.Form.print fmt a.lit
@ -347,7 +347,7 @@ module Make (Th : Theory_intf.S) = struct
) )
(* Complete debug printing *) (* Complete debug printing *)
let sign a = if a == a.var.pa then "+" else "-" let sign a = if a == a.var.v_pa then "+" else "-"
let debug_reason fmt = function let debug_reason fmt = function
| n, _ when n < 0 -> | n, _ when n < 0 ->
@ -407,7 +407,7 @@ module Make (Th : Theory_intf.S) = struct
let[@inline] atoms c = c.atoms let[@inline] atoms c = c.atoms
let[@inline] atoms_l c = Array.to_list c.atoms let[@inline] atoms_l c = Array.to_list c.atoms
let[@inline] tag c = c.tag let[@inline] tag c = c.tag
let hash cl = Array.fold_left (fun i a -> Hashtbl.hash (a.aid, i)) 0 cl.atoms let hash cl = Array.fold_left (fun i a -> Hashtbl.hash (a.a_id, i)) 0 cl.atoms
let[@inline] premise c = c.c_premise let[@inline] premise c = c.c_premise
let[@inline] set_premise c p = c.c_premise <- p let[@inline] set_premise c p = c.c_premise <- p
@ -456,8 +456,8 @@ module Make (Th : Theory_intf.S) = struct
let aux fmt a = let aux fmt a =
Array.iter (fun p -> Array.iter (fun p ->
Format.fprintf fmt "%s%d " Format.fprintf fmt "%s%d "
(if p == p.var.pa then "-" else "") (if p == p.var.v_pa then "-" else "")
(p.var.vid+1) (p.var.v_id+1)
) a ) a
in in
Format.fprintf fmt "%a0" aux atoms Format.fprintf fmt "%a0" aux atoms
@ -493,7 +493,7 @@ module Make (Th : Theory_intf.S) = struct
if equal_atoms a b then if equal_atoms a b then
aux resolved (a :: acc) r aux resolved (a :: acc) r
else if equal_atoms (a.neg) b then else if equal_atoms (a.neg) b then
aux ((a.var.pa) :: resolved) acc r aux ((a.var.v_pa) :: resolved) acc r
else else
aux resolved (a :: acc) (b :: r) aux resolved (a :: acc) (b :: r)
in in
@ -767,8 +767,10 @@ module Make (Th : Theory_intf.S) = struct
*) *)
let insert_var_order st (v:var) : unit = let insert_var_order st (v:var) : unit =
if not (Var.in_heap v) && Var.level v < 0 then ( if not (Var.in_heap v) && Var.level v < 0 then (
(* new variable that is not assigned, add to heap. *) (* new variable that is not assigned, add to heap and to theory. *)
H.insert st.order v; H.insert st.order v;
Th.add_formula (Lazy.force st.th) v.v_pa.lit;
Th.add_formula (Lazy.force st.th) v.v_na.lit;
) )
(* attach an atom by deciding on its variable, if needed *) (* attach an atom by deciding on its variable, if needed *)
@ -845,7 +847,7 @@ module Make (Th : Theory_intf.S) = struct
- false literals (not suitable to watch) - false literals (not suitable to watch)
*) *)
let sort_lits_by_level atoms : atom list = let sort_lits_by_level atoms : atom list =
let rec partition_aux trues unassigned falses i = let rec aux trues unassigned falses i =
if i >= Array.length atoms then ( if i >= Array.length atoms then (
trues @ unassigned @ falses trues @ unassigned @ falses
) else ( ) else (
@ -857,13 +859,13 @@ module Make (Th : Theory_intf.S) = struct
else else
(a :: trues) @ unassigned @ falses @ (array_slice_to_list atoms (i + 1)) (a :: trues) @ unassigned @ falses @ (array_slice_to_list atoms (i + 1))
) else if a.neg.is_true then ( ) else if a.neg.is_true then (
partition_aux trues unassigned (a::falses) (i + 1) aux trues unassigned (a::falses) (i + 1)
) else ( ) else (
partition_aux trues (a::unassigned) falses (i + 1) aux trues (a::unassigned) falses (i + 1)
) )
) )
in in
try partition_aux [] [] [] 0 try aux [] [] [] 0
with Trivial -> Array.to_list atoms with Trivial -> Array.to_list atoms
(* Making a decision. (* Making a decision.
@ -1057,7 +1059,7 @@ module Make (Th : Theory_intf.S) = struct
except we look the the Last UIP (TODO: check ?), and do it in an imperative except we look the the Last UIP (TODO: check ?), and do it in an imperative
and efficient manner. *) and efficient manner. *)
let analyze_sat st c_clause : conflict_res = let analyze_sat st c_clause : conflict_res =
let pathC = ref 0 in let path_c = ref 0 in
let learnt = ref [] in let learnt = ref [] in
let cond = ref true in let cond = ref true in
let blevel = ref 0 in let blevel = ref 0 in
@ -1097,7 +1099,7 @@ module Make (Th : Theory_intf.S) = struct
if q.var.v_level > 0 then ( if q.var.v_level > 0 then (
var_bump_activity st q.var; var_bump_activity st q.var;
if q.var.v_level >= conflict_level then ( if q.var.v_level >= conflict_level then (
incr pathC; incr path_c;
) else ( ) else (
learnt := q :: !learnt; learnt := q :: !learnt;
blevel := max !blevel q.var.v_level blevel := max !blevel q.var.v_level
@ -1115,9 +1117,9 @@ module Make (Th : Theory_intf.S) = struct
decr tr_ind; decr tr_ind;
done; done;
let p = get_atom st !tr_ind in let p = get_atom st !tr_ind in
decr pathC; decr path_c;
decr tr_ind; decr tr_ind;
match !pathC, p.var.reason with match !path_c, p.var.reason with
| 0, _ -> | 0, _ ->
cond := false; cond := false;
learnt := p.neg :: (List.rev !learnt) learnt := p.neg :: (List.rev !learnt)
@ -1444,7 +1446,7 @@ module Make (Th : Theory_intf.S) = struct
let rec pick_branch_aux st atom : unit = let rec pick_branch_aux st atom : unit =
let v = atom.var in let v = atom.var in
if v.v_level >= 0 then ( if v.v_level >= 0 then (
assert (v.pa.is_true || v.na.is_true); assert (v.v_pa.is_true || v.v_na.is_true);
pick_branch_lit st pick_branch_lit st
) else ( ) else (
new_decision_level st; new_decision_level st;
@ -1458,7 +1460,7 @@ module Make (Th : Theory_intf.S) = struct
pick_branch_aux st atom pick_branch_aux st atom
| None -> | None ->
begin match H.remove_min st.order with begin match H.remove_min st.order with
| v -> pick_branch_aux st v.pa | v -> pick_branch_aux st v.v_pa
| exception Not_found -> raise Sat | exception Not_found -> raise Sat
end end
@ -1492,10 +1494,10 @@ module Make (Th : Theory_intf.S) = struct
let eval_level (st:t) lit = let eval_level (st:t) lit =
let var, negated = Var.make st lit in let var, negated = Var.make st lit in
if not var.pa.is_true && not var.na.is_true if not var.v_pa.is_true && not var.v_na.is_true
then raise UndecidedLit then raise UndecidedLit
else assert (var.v_level >= 0); else assert (var.v_level >= 0);
let truth = var.pa.is_true in let truth = var.v_pa.is_true in
let value = match negated with let value = match negated with
| Theory_intf.Negated -> not truth | Theory_intf.Negated -> not truth
| Theory_intf.Same_sign -> truth | Theory_intf.Same_sign -> truth