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

basic renaming

Browse source
This commit is contained in:
Simon Cruanes 2021-03-20 23:55:31 -04:00
parent 3aadb055b6
commit 7bf6b18bc0
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -153,11 +153,11 @@ module Make(A : ARG) : S with module A = A = struct
| B_bool true -> Some b
| B_bool false -> Some c
| _ ->
let t_a = fresh_term self ~for_:t ~pre:"ite" (T.ty b) in
let t_ite = fresh_term self ~for_:t ~pre:"ite" (T.ty b) 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_a; mk_lit (eq self.tst t_a c)];
Some t_a
add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)];
add_clause [lit_a; mk_lit (eq self.tst t_ite c)];
Some t_ite
end
| _ -> None