projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
temp commit.
[tatoo.git]
/
src
/
formula.mli
diff --git
a/src/formula.mli
b/src/formula.mli
index
e83bca1
..
52e38b7
100644
(file)
--- a/
src/formula.mli
+++ b/
src/formula.mli
@@
-14,30
+14,28
@@
(***********************************************************************)
(*
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-0
2-05 16:11:43 CE
T by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-0
4-04 18:41:24 CES
T by Kim Nguyen>
*)
*)
-module type
PREDICATE
=
+module type
ATOM
=
sig
type t
sig
type t
- type ctx
- val eval : ctx -> t -> bool
val neg : t -> t
include Hcons.Abstract with type t := t
val neg : t -> t
include Hcons.Abstract with type t := t
- include
Sigs.AUX
.Printable with type t := t
+ include
Common_sig
.Printable with type t := t
end
end
-type ('formula,'
pred
) expr =
+type ('formula,'
atom
) expr =
| False
| True
| Or of 'formula * 'formula
| And of 'formula * 'formula
| False
| True
| Or of 'formula * 'formula
| And of 'formula * 'formula
- | Atom of '
pred
+ | Atom of '
atom
(** View of the internal representation of a formula,
used for pattern matching *)
(** View of the internal representation of a formula,
used for pattern matching *)
-module Make(P :
PREDICATE
) :
+module Make(P :
ATOM
) :
sig
type t
sig
type t
@@
-53,7
+51,7
@@
sig
(** Equality over formulae *)
val expr : t -> (t,P.t) expr
(** Equality over formulae *)
val expr : t -> (t,P.t) expr
- (**
Equality over
formulae *)
+ (**
Return a view of the
formulae *)
val compare : t -> t -> int
(** Comparison of formulae *)
val compare : t -> t -> int
(** Comparison of formulae *)
@@
-77,15
+75,16
@@
sig
(** [atom_ dir b q] creates a down_left or down_right atom for state
[q]. The atom is positive if [b == true].
*)
(** [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 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 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 *)
+
+ val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
+ (** [fold f phi acc] folds [f] over the formula structure *)
+
end
end