Rework the formula predicates:

[tatoo.git] / src / auto / formula.ml

diff --git a/src/auto/formula.ml b/src/auto/formula.ml
index a27ffc6..7128ba4 100644 (file)
--- a/src/auto/formula.ml
+++ b/src/auto/formula.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-04 22:52:17 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-09 11:12:54 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -27,24 +27,22 @@ open Utils
 (** Implementation of hashconsed Boolean formulae *)
 
 *)
-module type PREDICATE =
+module type ATOM =
 sig
   type t
-  type ctx
-  val eval : ctx -> t -> bool
   val neg : t -> t
   include Hcons.Abstract with type t := t
   include Common_sig.Printable with type t := t
 end
 
-type ('formula,'pred) expr =
+type ('formula,'atom) expr =
   | False
   | True
   | Or of 'formula * 'formula
   | And of 'formula * 'formula
-  | Atom of 'pred
+  | Atom of 'atom
 
-module Make (P: PREDICATE) =
+module Make (P: ATOM) =
 struct
 
 
@@ -172,12 +170,4 @@ let and_ f1 f2 =
 
 let of_bool = function true -> true_ | false -> false_
 
-let rec eval ctx f =
-  match f.Node.node.pos with
-    True -> true
-  | False -> false
-  | Atom p -> P.eval ctx p
-  | And(f1, f2) -> eval ctx f1 && eval ctx f2
-  | Or(f1, f2) -> eval ctx f1 || eval ctx f2
-
 end