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

debug msg

Browse source
This commit is contained in:
Simon Cruanes 2021-03-18 13:27:21 -04:00
parent 2312da883c
commit 380efa816f
1 changed files with 20 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -136,10 +136,16 @@ module Make(A : ARG) : S with module A = A = struct
| B_eq _ | B_neq _ -> None | B_eq _ | B_neq _ -> None
| B_atom _ -> None | B_atom _ -> None
let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty let fresh_term self ~for_ ~pre ty =
let fresh_lit (self:state) ~mk_lit ~pre : Lit.t = let u = A.Gensym.fresh_term self.gensym ~pre ty in
let t = fresh_term ~pre self (Ty.bool self.ty_st) in Log.debugf 20
mk_lit t (fun k->k "(@[sidekick.bool.proxy@ :t %a@ :for %a@])"
T.pp u T.pp for_);
u
let fresh_lit (self:state) ~for_ ~mk_lit ~pre : Lit.t =
let proxy = fresh_term ~for_ ~pre self (Ty.bool self.ty_st) in
mk_lit proxy
(* preprocess "ite" away *) (* preprocess "ite" away *)
let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : T.t option = let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : T.t option =
@ -150,7 +156,7 @@ module Make(A : ARG) : S with module A = A = struct
| B_bool true -> Some b | B_bool true -> Some b
| B_bool false -> Some c | B_bool false -> Some c
| _ -> | _ ->
let t_a = fresh_term self ~pre:"ite" (T.ty b) in let t_a = fresh_term self ~for_:t ~pre:"ite" (T.ty b) in
let lit_a = mk_lit a in let lit_a = mk_lit a in
add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_a b)]; add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_a b)];
add_clause [lit_a; mk_lit (eq self.tst t_a c)]; add_clause [lit_a; mk_lit (eq self.tst t_a c)];
@ -170,16 +176,19 @@ module Make(A : ARG) : S with module A = A = struct
let lit = get_lit_uncached t_abs in let lit = get_lit_uncached t_abs in
if not (T.equal (Lit.term lit) t_abs) then ( if not (T.equal (Lit.term lit) t_abs) then (
T.Tbl.add self.cnf t_abs lit; T.Tbl.add self.cnf t_abs lit;
Log.debugf 20
(fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])"
Lit.pp lit T.pp t_abs);
); );
lit lit
in in
if t_sign then lit else Lit.neg lit if t_sign then lit else Lit.neg lit
and equiv_ ~is_xor a b : Lit.t = and equiv_ ~is_xor ~for_ a b : Lit.t =
let a = get_lit a in let a = get_lit a in
let b = get_lit b in let b = get_lit b in
let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *) let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
let proxy = fresh_lit ~mk_lit ~pre:"equiv_" self in let proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in
(* proxy => a<=> b, (* proxy => a<=> b,
¬proxy => a xor b *) ¬proxy => a xor b *)
add_clause [Lit.neg proxy; Lit.neg a; b]; add_clause [Lit.neg proxy; Lit.neg a; b];
@ -197,14 +206,14 @@ module Make(A : ARG) : S with module A = A = struct
Lit.neg lit Lit.neg lit
| B_and l -> | B_and l ->
let subs = l |> Iter.map get_lit |> Iter.to_list in let subs = l |> Iter.map get_lit |> Iter.to_list in
let proxy = fresh_lit ~mk_lit ~pre:"and_" self in let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"and_" self in
(* add clauses *) (* add clauses *)
List.iter (fun u -> add_clause [Lit.neg proxy; u]) subs; List.iter (fun u -> add_clause [Lit.neg proxy; u]) subs;
add_clause (proxy :: List.map Lit.neg subs); add_clause (proxy :: List.map Lit.neg subs);
proxy proxy
| B_or l -> | B_or l ->
let subs = l |> Iter.map get_lit |> Iter.to_list in let subs = l |> Iter.map get_lit |> Iter.to_list in
let proxy = fresh_lit ~mk_lit ~pre:"or_" self in let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in
(* add clauses *) (* add clauses *)
List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs; List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs;
add_clause (Lit.neg proxy :: subs); add_clause (Lit.neg proxy :: subs);
@ -217,8 +226,8 @@ module Make(A : ARG) : S with module A = A = struct
or_a self.tst @@ IArray.append args (IArray.singleton u) in or_a self.tst @@ IArray.append args (IArray.singleton u) in
get_lit t' get_lit t'
| B_ite _ | B_eq _ | B_neq _ -> mk_lit t | B_ite _ | B_eq _ | B_neq _ -> mk_lit t
| B_equiv (a,b) -> equiv_ ~is_xor:false a b | B_equiv (a,b) -> equiv_ ~for_:t ~is_xor:false a b
| B_xor (a,b) -> equiv_ ~is_xor:true a b | B_xor (a,b) -> equiv_ ~for_:t ~is_xor:true a b
| B_atom u -> mk_lit u | B_atom u -> mk_lit u
in in
let lit = get_lit t in let lit = get_lit t in