From 83e456ef8a0d110d0c09e9e8af65fd19c54f5b00 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 30 Jul 2022 21:17:37 -0400 Subject: [PATCH] remove sidekick_lit functor --- src/lit/Sidekick_lit.ml | 44 ----------------------------------------- src/lit/dune | 6 ------ 2 files changed, 50 deletions(-) delete mode 100644 src/lit/Sidekick_lit.ml delete mode 100644 src/lit/dune diff --git a/src/lit/Sidekick_lit.ml b/src/lit/Sidekick_lit.ml deleted file mode 100644 index 64fb360f..00000000 --- a/src/lit/Sidekick_lit.ml +++ /dev/null @@ -1,44 +0,0 @@ -(** Implementation of literals from terms *) - -module Make (T : Sidekick_core.TERM) : Sidekick_core.LIT with module T = T = -struct - module T = T - - type term = T.Term.t - type t = { lit_term: term; lit_sign: bool } - - let[@inline] neg l = { l with lit_sign = not l.lit_sign } - let[@inline] sign t = t.lit_sign - let[@inline] abs t = { t with lit_sign = true } - let[@inline] term (t : t) : term = t.lit_term - let[@inline] signed_term t = term t, sign t - let make ~sign t = { lit_sign = sign; lit_term = t } - - let atom ?(sign = true) tst (t : term) : t = - let t, sign' = T.Term.abs tst t in - let sign = - if not sign' then - not sign - else - sign - in - make ~sign t - - let equal a b = a.lit_sign = b.lit_sign && T.Term.equal a.lit_term b.lit_term - - let hash a = - let sign = a.lit_sign in - CCHash.combine3 2 (CCHash.bool sign) (T.Term.hash a.lit_term) - - let pp out l = - if l.lit_sign then - T.Term.pp out l.lit_term - else - Format.fprintf out "(@[@<1>¬@ %a@])" T.Term.pp l.lit_term - - let norm_sign l = - if l.lit_sign then - l, true - else - neg l, false -end diff --git a/src/lit/dune b/src/lit/dune deleted file mode 100644 index dbfc89b0..00000000 --- a/src/lit/dune +++ /dev/null @@ -1,6 +0,0 @@ -(library - (name sidekick_lit) - (public_name sidekick.lit) - (synopsis "Implementation of literals for Sidekick") - (libraries containers sidekick.core sidekick.util) - (flags :standard -warn-error -a+8 -open Sidekick_util))