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

fix: do not preemptively simplify imply

Browse source
This commit is contained in:
Simon Cruanes 2021-03-18 18:20:39 -04:00
parent 9fea7462dc
commit ffc45b0db6
1 changed files with 3 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -105,13 +105,9 @@ module Make(A : ARG) : S with module A = A = struct
else if Iter.for_all is_false a then Some (T.bool tst false)
else None
| B_imply (args, u) ->
(* turn into a disjunction *)
let u =
let args =
args |> Iter.map (not_ tst) |> IArray.of_iter in
or_a tst @@ IArray.append args (IArray.singleton u)
in
Some u
if Iter.exists is_false args then Some (T.bool tst true)
else if is_true u then Some (T.bool tst true)
else None
| B_ite (a,b,c) ->
(* directly simplify [a] so that maybe we never will simplify one
of the branches *)