+++ /dev/null
-(***********************************************************************)
-(* *)
-(* 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. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-02-05 16:11:43 CET by Kim Nguyen>
-*)
-
-module type PREDICATE =
-sig
- type t
- type ctx
- val eval : ctx -> t -> bool
- val neg : t -> t
- include Hcons.Abstract with type t := t
- include Sigs.AUX.Printable with type t := t
-end
-
-type ('formula,'pred) expr =
- | False
- | True
- | Or of 'formula * 'formula
- | And of 'formula * 'formula
- | Atom of 'pred
-
-(** View of the internal representation of a formula,
- used for pattern matching *)
-
-module Make(P : PREDICATE) :
-sig
- 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,P.t) expr
- (** Equality over formulae *)
-
- val compare : t -> t -> int
- (** Comparison of formulae *)
-
- 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_ : P.t -> 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 *)
-
- val eval : P.ctx -> t -> bool
- (** Evaluate a formula given a context for atomic predicates *)
-end