X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fauto%2Fformula.ml;fp=src%2Fauto%2Fformula.ml;h=7128ba4194648d6f1779130f43425fcbf67e031c;hb=35c32fbd2543a399cc6939f21317bebf37172646;hp=a27ffc6ecf0b73448a355a5cddc2befa45f29e18;hpb=cd87d0f43eb81563fd303875ff4c83fe382ea99f;p=tatoo.git

diff --git a/src/auto/formula.ml b/src/auto/formula.ml
index a27ffc6..7128ba4 100644
--- 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