src/boolean.mli

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                     Kim Nguyen, LRI UMR8623                         *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   8 (*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
   9 (*  Recherche Scientifique. All rights reserved.  This file is         *)
  10 (*  distributed under the terms of the GNU Lesser General Public       *)
  11 (*  License, with the special exception on linking described in file   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  16 type ('formula,'atom) expr =
  17   | False
  18   | True
  19   | Or of 'formula * 'formula
  20   | And of 'formula * 'formula
  21   | Atom of 'atom * bool
  22
  23 (** View of the internal representation of a formula,
  24     used for pattern matching *)
  25
  26 module Make(A : sig
  27   include Hcons.S
  28   include Common_sig.Printable with type t := t
  29 end) :
  30 sig
  31   type t
  32
  33   (** Abstract type representing hashconsed formulae *)
  34
  35   val hash : t -> int
  36   (** Hash function for formulae *)
  37
  38   val uid : t -> Uid.t
  39   (** Returns a unique ID for formulae *)
  40
  41   val equal : t -> t -> bool
  42   (** Equality over formulae *)
  43
  44   val expr : t -> (t,A.t) expr
  45   (** Return a view of the formulae *)
  46
  47   val compare : t -> t -> int
  48   (** Comparison of formulae *)
  49
  50   val print : Format.formatter -> t -> unit
  51   (** Pretty printer *)
  52
  53   val is_true : t -> bool
  54   (** [is_true f] tests whether the formula is the atom True *)
  55
  56   val is_false : t -> bool
  57   (** [is_false f] tests whether the formula is the atom False *)
  58
  59   val true_ : t
  60   (** Atom True *)
  61
  62   val false_ : t
  63   (** Atom False *)
  64
  65   val atom_ : A.t -> t
  66   (** [atom_ a] creates a new formula consisting of the atome a.
  67   *)
  68
  69   val not_ : t -> t
  70   val or_ : t -> t -> t
  71   val and_ : t -> t -> t
  72   (** Boolean connective *)
  73
  74   val of_bool : bool -> t
  75   (** Convert an ocaml Boolean value to a formula *)
  76
  77   val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
  78   (** [fold f phi acc] folds [f] over the formula structure *)
  79
  80 end