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

feat(th-bool): flattening of and/or also removes neutral elts

Browse source
This commit is contained in:
Simon Cruanes 2019-02-01 21:42:44 -06:00
parent f76f6bb0d9
commit f2eecaa758
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/th-bool/Sidekick_th_bool.ml
View file

@ -108,22 +108,24 @@ let as_id id (t:Term.t) : Term.t IArray.t option =
| _ -> None
(* flatten terms of the given ID *)
let flatten_id id (l:Term.t list) : Term.t list =
let flatten_id op sign (l:Term.t list) : Term.t list =
CCList.flat_map
(fun t -> match as_id id t with
(fun t -> match as_id op t with
| Some args -> IArray.to_list args
| None when (sign && Term.is_true t) || (not sign && Term.is_false t) ->
[] (* idempotent *)
| None -> [t])
l
let and_l st l =
match flatten_id id_and l with
match flatten_id id_and true l with
| [] -> Term.true_ st
| l when List.exists Term.is_false l -> Term.false_ st
| [x] -> x
| args -> Term.app_cst st C.and_ (IArray.of_list args)
let or_l st l =
match flatten_id id_or l with
match flatten_id id_or false l with
| [] -> Term.false_ st
| l when List.exists Term.is_true l -> Term.true_ st
| [x] -> x
@ -133,8 +135,9 @@ let and_ st a b = and_l st [a;b]
let or_ st a b = or_l st [a;b]
let eq st a b =
if Term.equal a b then Term.true_ st
else (
if Term.equal a b then (
Term.true_ st
) else (
let a,b = if Term.id a > Term.id b then b, a else a, b in
Term.app_cst st C.eq (IArray.doubleton a b)
)