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 module type ATOM =
  17 sig
  18   include Hcons.S
  19   include Common_sig.Printable with type t := t
  20 end
  21
  22 type ('formula,'atom) expr =
  23   | False
  24   | True
  25   | Or of 'formula * 'formula
  26   | And of 'formula * 'formula
  27   | Atom of 'atom * bool
  28
  29 (** View of the internal representation of a formula,
  30     used for pattern matching *)
  31
  32 module Make(A : ATOM) :
  33 sig
  34   type t
  35
  36   (** Abstract type representing hashconsed formulae *)
  37
  38   val hash : t -> int
  39   (** Hash function for formulae *)
  40
  41   val uid : t -> Uid.t
  42   (** Returns a unique ID for formulae *)
  43
  44   val equal : t -> t -> bool
  45   (** Equality over formulae *)
  46
  47   val expr : t -> (t,A.t) expr
  48   (** Return a view of the formulae *)
  49
  50   val compare : t -> t -> int
  51   (** Comparison of formulae *)
  52
  53   val print : Format.formatter -> t -> unit
  54   (** Pretty printer *)
  55
  56   val is_true : t -> bool
  57   (** [is_true f] tests whether the formula is the atom True *)
  58
  59   val is_false : t -> bool
  60   (** [is_false f] tests whether the formula is the atom False *)
  61
  62   val true_ : t
  63   (** Atom True *)
  64
  65   val false_ : t
  66   (** Atom False *)
  67
  68   val atom_ : A.t -> t
  69   (** [atom_ a] creates a new formula consisting of the atome a.
  70   *)
  71
  72   val not_ : t -> t
  73   val or_ : t -> t -> t
  74   val and_ : t -> t -> t
  75   (** Boolean connective *)
  76
  77   val of_bool : bool -> t
  78   (** Convert an ocaml Boolean value to a formula *)
  79
  80   val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
  81   (** [fold f phi acc] folds [f] over the formula structure *)
  82
  83 end