Usable version:

[tatoo.git] / src / formula.mli

diff --git a/src/formula.mli b/src/formula.mli
new file mode 100644 (file)
index 0000000..46cbe65
--- /dev/null
+++ b/src/formula.mli
@@ -0,0 +1,92 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(** Implementation of hashconsed Boolean formulae *)
+
+type move = [ `Left |`Right ]
+(** Direction for automata predicates *)
+
+type 'hcons expr =
+    False
+    | True
+    | Or of 'hcons * 'hcons
+    | And of 'hcons * 'hcons
+    | Atom of (move * bool * State.t)
+
+(** Partial internal representation of a formula,
+    used for pattern matching *)
+
+type t
+(** Abstract type representing hashconsed formulae *)
+
+val hash : t -> int
+(** Hash function for formulae *)
+
+val uid : t -> Uid.t
+(** Returns a unique ID for formulae *)
+
+val equal : t -> t -> bool
+(** Equality over formulae *)
+
+val expr : t -> t expr
+(** Equality over formulae *)
+
+val st : t -> StateSet.t * StateSet.t
+(** states occuring left and right, positively or negatively *)
+
+val compare : t -> t -> int
+(** Comparison of formulae *)
+
+val size : t -> int
+(** Syntactic size of the formula *)
+
+val print : Format.formatter -> t -> unit
+(** Pretty printer *)
+
+val is_true : t -> bool
+(** [is_true f] tests whether the formula is the atom True *)
+
+val is_false : t -> bool
+(** [is_false f] tests whether the formula is the atom False *)
+
+val true_ : t
+(** Atom True *)
+
+val false_ : t
+(** Atom False *)
+
+val atom_ : move -> bool -> StateSet.elt -> t
+(** [atom_ dir b q] creates a down_left or down_right atom for state
+    [q]. The atom is positive if [b == true].
+*)
+
+val not_ : t -> t
+val or_ : t -> t -> t
+val and_ : t -> t -> t
+(** Boolean connective *)
+
+val of_bool : bool -> t
+(** Convert an ocaml Boolean value to a formula *)
+
+module Infix : sig
+  val ( +| ) : t -> t -> t
+  val ( *& ) : t -> t -> t
+  val ( *+ ) : move -> StateSet.elt -> t
+  val ( *- ) : move -> StateSet.elt -> t
+end
+(** Module to facilitate infix notations of formulae.
+    Just [open Formla.Infix] and write:
+    [let f = `Left *+ q1 +| `Right *+ q2 in ...]
+*)