src/hconsed_run.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                   Lucca Hirschi, LRI UMR8623                        *)
   4 (*                   Université Paris-Sud & CNRS                       *)
   5 (*                                                                     *)
   6 (*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
   7 (*  Recherche Scientifique. All rights reserved.  This file is         *)
   8 (*  distributed under the terms of the GNU Lesser General Public       *)
   9 (*  License, with the special exception on linking described in file   *)
  10 (*  ../LICENSE.                                                        *)
  11 (*                                                                     *)
  12 (***********************************************************************)
  13
  14 INCLUDE "utils.ml"
  15
  16
  17 (* Hash Consign modules *)
  18
  19 module type Oracle_fixpoint =
  20 sig
  21   type t = StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
  22   val equal : t -> t -> bool
  23   val hash : t -> int
  24 end
  25
  26 type dStateS = StateSet.t*StateSet.t
  27 module type Run_fixpoint =
  28 sig
  29   type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
  30   val equal : t -> t -> bool
  31   val hash : t -> int
  32 end
  33
  34 module Oracle_fixpoint : Oracle_fixpoint = struct
  35   type t =
  36       StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
  37   let equal (s,l,r,list,t) (s',l',r',list',t') = StateSet.equal s s' &&
  38     StateSet.equal l l' && StateSet.equal r r' && QName.equal t t'
  39   let hash (s,l,r,list,t) =
  40     HASHINT4(StateSet.hash s, StateSet.hash l, StateSet.hash r, QName.hash t)
  41 end
  42
  43 let dequal (x,y) (x',y') = StateSet.equal x x' && StateSet.equal y y'
  44 let dhash (x,y) = HASHINT2(StateSet.hash x, StateSet.hash y)
  45 module Run_fixpoint : Run_fixpoint = struct
  46   type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
  47   let equal (s,l,r,list,t) (s',l',r',list',t') = dequal s s' &&
  48     dequal l l' && dequal r r' && QName.equal t t'
  49   let hash (s,l,r,list,t) =
  50     HASHINT4(dhash s, dhash l, dhash r, QName.hash t)
  51 end