--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/AtomNet.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,59 @@
+(* ========================================================================= *)
+(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure AtomNet :> AtomNet =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun atomToTerm atom = Term.Fn atom;
+
+fun termToAtom (Term.Var _) = raise Bug "AtomNet.termToAtom"
+ | termToAtom (Term.Fn atom) = atom;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of atom sets that can be efficiently matched and unified. *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = TermNet.parameters;
+
+type 'a atomNet = 'a TermNet.termNet;
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val new = TermNet.new;
+
+val size = TermNet.size;
+
+fun insert net (atm,a) = TermNet.insert net (atomToTerm atm, a);
+
+fun fromList parm l = foldl (fn (atm_a,n) => insert n atm_a) (new parm) l;
+
+val filter = TermNet.filter;
+
+fun toString net = "AtomNet[" ^ Int.toString (size net) ^ "]";
+
+val pp = TermNet.pp;
+
+(* ------------------------------------------------------------------------- *)
+(* Matching and unification queries. *)
+(* *)
+(* These function return OVER-APPROXIMATIONS! *)
+(* Filter afterwards to get the precise set of satisfying values. *)
+(* ------------------------------------------------------------------------- *)
+
+fun match net atm = TermNet.match net (atomToTerm atm);
+
+fun matched net atm = TermNet.matched net (atomToTerm atm);
+
+fun unify net atm = TermNet.unify net (atomToTerm atm);
+
+end