Source file bool_lit.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76

(* This file is free software, part of Zipperposition. See file "license" for more details. *)

(** {1 Boolean Literal} *)

open Logtk

module type S = Bool_lit_intf.S

module type PAYLOAD = sig
  type t
  val dummy : t
end

let stat_num_lit = Util.mk_stat "msat.num_lits"

module Make(Payload : PAYLOAD)
  : S with type payload = Payload.t
= struct
  type t = {
    id: int; (* sign = sign of literal *)
    payload: Payload.t;
    neg: t; (* negation *)
  }
  type lit = t
  type payload = Payload.t

  let rec dummy = { id=0; neg=dummy; payload=Payload.dummy; }

  let fresh_id =
    let n = ref 1 in
    fun () ->
      Util.incr_stat stat_num_lit;
      let id = !n in
      incr n;
      id

  (* factory for literals *)
  let make =
    fun payload ->
    let id = fresh_id () in
    let rec pos = {
      id;
      payload;
      neg;
    } and neg = {
        id= -id;
        payload;
        neg=pos;
      } in
    pos

  let hash i = Hash.int i.id
  let equal i j = i.id = j.id
  let compare i j = CCInt.compare i.id j.id
  let neg i = i.neg
  let sign i = i.id > 0
  let abs i = if i.id > 0 then i else i.neg
  let norm i = abs i, i.id < 0
  let set_sign b i = if b then abs i else (abs i).neg
  let apply_sign b i = if b then i else i.neg
  let payload i = i.payload
  let to_int i = i.id
  let pp out i =
    Format.fprintf out "%s%d" (if sign i then "" else "¬") (abs i).id

  module AsKey = struct
    type t = lit
    let compare = compare
    let hash = hash
    let equal = equal
  end

  module Set = CCSet.Make(AsKey)
  module Tbl = CCHashtbl.Make(AsKey)
end