Fix the build script.
[tatoo.git] / src / auto / formula.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 (*
17   Time-stamp: <Last modified on 2013-03-09 11:16:45 CET by Kim Nguyen>
18 *)
19
20 module type ATOM =
21 sig
22   type t
23   val neg : t -> t
24   include Utils.Hcons.Abstract with type t := t
25   include Utils.Common_sig.Printable with type t := t
26 end
27
28 type ('formula,'atom) expr =
29   | False
30   | True
31   | Or of 'formula * 'formula
32   | And of 'formula * 'formula
33   | Atom of 'atom
34
35 (** View of the internal representation of a formula,
36     used for pattern matching *)
37
38 module Make(P : ATOM) :
39 sig
40   type t
41
42   (** Abstract type representing hashconsed formulae *)
43
44   val hash : t -> int
45   (** Hash function for formulae *)
46
47   val uid : t -> Utils.Uid.t
48   (** Returns a unique ID for formulae *)
49
50   val equal : t -> t -> bool
51   (** Equality over formulae *)
52
53   val expr : t -> (t,P.t) expr
54   (** Return a view of the formulae *)
55
56   val compare : t -> t -> int
57   (** Comparison of formulae *)
58
59   val print : Format.formatter -> t -> unit
60   (** Pretty printer *)
61
62   val is_true : t -> bool
63   (** [is_true f] tests whether the formula is the atom True *)
64
65   val is_false : t -> bool
66   (** [is_false f] tests whether the formula is the atom False *)
67
68   val true_ : t
69   (** Atom True *)
70
71   val false_ : t
72   (** Atom False *)
73
74   val atom_ : P.t -> t
75   (** [atom_ dir b q] creates a down_left or down_right atom for state
76       [q]. The atom is positive if [b == true].
77   *)
78
79   val not_ : t -> t
80   val or_ : t -> t -> t
81   val and_ : t -> t -> t
82   (** Boolean connective *)
83
84   val of_bool : bool -> t
85   (** Convert an ocaml Boolean value to a formula *)
86
87   val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
88   (** [fold f phi acc] folds [f] over the formula structure *)
89
90 end