new version of the Metis files
authorblanchet
Mon, 13 Sep 2010 21:09:43 +0200
changeset 39348 6f9c9899f99f
parent 39347 50dec19e682b
child 39349 2d0a4361c3ef
new version of the Metis files
src/Tools/Metis/src/Active.sig
src/Tools/Metis/src/Active.sml
src/Tools/Metis/src/Atom.sig
src/Tools/Metis/src/Atom.sml
src/Tools/Metis/src/AtomNet.sig
src/Tools/Metis/src/AtomNet.sml
src/Tools/Metis/src/Clause.sig
src/Tools/Metis/src/Clause.sml
src/Tools/Metis/src/ElementSet.sig
src/Tools/Metis/src/ElementSet.sml
src/Tools/Metis/src/FILES
src/Tools/Metis/src/Formula.sig
src/Tools/Metis/src/Formula.sml
src/Tools/Metis/src/Heap.sig
src/Tools/Metis/src/Heap.sml
src/Tools/Metis/src/KeyMap.sig
src/Tools/Metis/src/KeyMap.sml
src/Tools/Metis/src/KnuthBendixOrder.sig
src/Tools/Metis/src/KnuthBendixOrder.sml
src/Tools/Metis/src/Lazy.sig
src/Tools/Metis/src/Lazy.sml
src/Tools/Metis/src/Literal.sig
src/Tools/Metis/src/Literal.sml
src/Tools/Metis/src/LiteralNet.sig
src/Tools/Metis/src/LiteralNet.sml
src/Tools/Metis/src/Map.sig
src/Tools/Metis/src/Map.sml
src/Tools/Metis/src/Model.sig
src/Tools/Metis/src/Model.sml
src/Tools/Metis/src/Name.sig
src/Tools/Metis/src/Name.sml
src/Tools/Metis/src/NameArity.sig
src/Tools/Metis/src/NameArity.sml
src/Tools/Metis/src/Normalize.sig
src/Tools/Metis/src/Normalize.sml
src/Tools/Metis/src/Options.sig
src/Tools/Metis/src/Options.sml
src/Tools/Metis/src/Ordered.sig
src/Tools/Metis/src/Ordered.sml
src/Tools/Metis/src/Parse.sig
src/Tools/Metis/src/Parse.sml
src/Tools/Metis/src/Portable.sig
src/Tools/Metis/src/PortableMlton.sml
src/Tools/Metis/src/PortableMosml.sml
src/Tools/Metis/src/PortablePolyml.sml
src/Tools/Metis/src/Print.sig
src/Tools/Metis/src/Print.sml
src/Tools/Metis/src/Problem.sig
src/Tools/Metis/src/Problem.sml
src/Tools/Metis/src/Proof.sig
src/Tools/Metis/src/Proof.sml
src/Tools/Metis/src/Random.sig
src/Tools/Metis/src/Random.sml
src/Tools/Metis/src/Resolution.sig
src/Tools/Metis/src/Resolution.sml
src/Tools/Metis/src/Rewrite.sig
src/Tools/Metis/src/Rewrite.sml
src/Tools/Metis/src/Rule.sig
src/Tools/Metis/src/Rule.sml
src/Tools/Metis/src/Set.sig
src/Tools/Metis/src/Set.sml
src/Tools/Metis/src/Sharing.sig
src/Tools/Metis/src/Sharing.sml
src/Tools/Metis/src/Stream.sig
src/Tools/Metis/src/Stream.sml
src/Tools/Metis/src/Subst.sig
src/Tools/Metis/src/Subst.sml
src/Tools/Metis/src/Subsume.sig
src/Tools/Metis/src/Subsume.sml
src/Tools/Metis/src/Term.sig
src/Tools/Metis/src/Term.sml
src/Tools/Metis/src/TermNet.sig
src/Tools/Metis/src/TermNet.sml
src/Tools/Metis/src/Thm.sig
src/Tools/Metis/src/Thm.sml
src/Tools/Metis/src/Tptp.sig
src/Tools/Metis/src/Tptp.sml
src/Tools/Metis/src/Units.sig
src/Tools/Metis/src/Units.sml
src/Tools/Metis/src/Useful.sig
src/Tools/Metis/src/Useful.sml
src/Tools/Metis/src/Waiting.sig
src/Tools/Metis/src/Waiting.sml
src/Tools/Metis/src/metis.sml
src/Tools/Metis/src/problems.sml
src/Tools/Metis/src/problems2tptp.sml
src/Tools/Metis/src/selftest.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Active.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,55 @@
+(* ========================================================================= *)
+(* THE ACTIVE SET OF CLAUSES                                                 *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Active =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of active clause sets.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+type simplify =
+     {subsume : bool,
+      reduce : bool,
+      rewrite : bool}
+
+type parameters =
+     {clause : Clause.parameters,
+      prefactor : simplify,
+      postfactor : simplify}
+
+type active
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val default : parameters
+
+val size : active -> int
+
+val saturation : active -> Clause.clause list
+
+(* ------------------------------------------------------------------------- *)
+(* Create a new active clause set and initialize clauses.                    *)
+(* ------------------------------------------------------------------------- *)
+
+val new :
+    parameters -> {axioms : Thm.thm list, conjecture : Thm.thm list} ->
+    active * {axioms : Clause.clause list, conjecture : Clause.clause list}
+
+(* ------------------------------------------------------------------------- *)
+(* Add a clause into the active set and deduce all consequences.             *)
+(* ------------------------------------------------------------------------- *)
+
+val add : active -> Clause.clause -> active * Clause.clause list
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : active Print.pp
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Active.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,911 @@
+(* ========================================================================= *)
+(* THE ACTIVE SET OF CLAUSES                                                 *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Active :> Active =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+(*MetisDebug
+local
+  fun mkRewrite ordering =
+      let
+        fun add (cl,rw) =
+            let
+              val {id, thm = th, ...} = Clause.dest cl
+            in
+              case total Thm.destUnitEq th of
+                SOME l_r => Rewrite.add rw (id,(l_r,th))
+              | NONE => rw
+            end
+      in
+        foldl add (Rewrite.new (KnuthBendixOrder.compare ordering))
+      end;
+
+  fun allFactors red =
+      let
+        fun allClause cl =
+            List.all red (cl :: Clause.factor cl) orelse
+            let
+              val () = Print.trace Clause.pp
+                         "Active.isSaturated.allFactors: cl" cl
+            in
+              false
+            end
+      in
+        List.all allClause
+      end;
+
+  fun allResolutions red =
+      let
+        fun allClause2 cl_lit cl =
+            let
+              fun allLiteral2 lit =
+                  case total (Clause.resolve cl_lit) (cl,lit) of
+                    NONE => true
+                  | SOME cl => allFactors red [cl]
+            in
+              LiteralSet.all allLiteral2 (Clause.literals cl)
+            end orelse
+            let
+              val () = Print.trace Clause.pp
+                         "Active.isSaturated.allResolutions: cl2" cl
+            in
+              false
+            end
+
+        fun allClause1 allCls cl =
+            let
+              val cl = Clause.freshVars cl
+
+              fun allLiteral1 lit = List.all (allClause2 (cl,lit)) allCls
+            in
+              LiteralSet.all allLiteral1 (Clause.literals cl)
+            end orelse
+            let
+              val () = Print.trace Clause.pp
+                         "Active.isSaturated.allResolutions: cl1" cl
+            in
+              false
+            end
+
+      in
+        fn [] => true
+         | allCls as cl :: cls =>
+           allClause1 allCls cl andalso allResolutions red cls
+      end;
+
+  fun allParamodulations red cls =
+      let
+        fun allClause2 cl_lit_ort_tm cl =
+            let
+              fun allLiteral2 lit =
+                  let
+                    val para = Clause.paramodulate cl_lit_ort_tm
+
+                    fun allSubterms (path,tm) =
+                        case total para (cl,lit,path,tm) of
+                          NONE => true
+                        | SOME cl => allFactors red [cl]
+                  in
+                    List.all allSubterms (Literal.nonVarTypedSubterms lit)
+                  end orelse
+                  let
+                    val () = Print.trace Literal.pp
+                               "Active.isSaturated.allParamodulations: lit2" lit
+                  in
+                    false
+                  end
+            in
+              LiteralSet.all allLiteral2 (Clause.literals cl)
+            end orelse
+            let
+              val () = Print.trace Clause.pp
+                         "Active.isSaturated.allParamodulations: cl2" cl
+              val (_,_,ort,_) = cl_lit_ort_tm
+              val () = Print.trace Rewrite.ppOrient
+                         "Active.isSaturated.allParamodulations: ort1" ort
+            in
+              false
+            end
+
+        fun allClause1 cl =
+            let
+              val cl = Clause.freshVars cl
+
+              fun allLiteral1 lit =
+                  let
+                    fun allCl2 x = List.all (allClause2 x) cls
+                  in
+                    case total Literal.destEq lit of
+                      NONE => true
+                    | SOME (l,r) =>
+                      allCl2 (cl,lit,Rewrite.LeftToRight,l) andalso
+                      allCl2 (cl,lit,Rewrite.RightToLeft,r)
+                  end orelse
+                  let
+                    val () = Print.trace Literal.pp
+                               "Active.isSaturated.allParamodulations: lit1" lit
+                  in
+                    false
+                  end
+            in
+              LiteralSet.all allLiteral1 (Clause.literals cl)
+            end orelse
+            let
+              val () = Print.trace Clause.pp
+                         "Active.isSaturated.allParamodulations: cl1" cl
+            in
+              false
+            end
+      in
+        List.all allClause1 cls
+      end;
+
+  fun redundant {subsume,reduce,rewrite} =
+      let
+        fun simp cl =
+            case Clause.simplify cl of
+              NONE => true
+            | SOME cl =>
+              Subsume.isStrictlySubsumed subsume (Clause.literals cl) orelse
+              let
+                val cl' = cl
+                val cl' = Clause.reduce reduce cl'
+                val cl' = Clause.rewrite rewrite cl'
+              in
+                not (Clause.equalThms cl cl') andalso
+                (simp cl' orelse
+                 let
+                   val () = Print.trace Clause.pp
+                              "Active.isSaturated.redundant: cl'" cl'
+                 in
+                   false
+                 end)
+              end
+      in
+        fn cl =>
+           simp cl orelse
+           let
+             val () = Print.trace Clause.pp
+                        "Active.isSaturated.redundant: cl" cl
+           in
+             false
+           end
+      end;
+in
+  fun isSaturated ordering subs cls =
+      let
+        val rd = Units.empty
+        val rw = mkRewrite ordering cls
+        val red = redundant {subsume = subs, reduce = rd, rewrite = rw}
+      in
+        (allFactors red cls andalso
+         allResolutions red cls andalso
+         allParamodulations red cls) orelse
+        let
+          val () = Print.trace Rewrite.pp "Active.isSaturated: rw" rw
+          val () = Print.trace (Print.ppList Clause.pp)
+                     "Active.isSaturated: clauses" cls
+        in
+          false
+        end
+      end;
+end;
+
+fun checkSaturated ordering subs cls =
+    if isSaturated ordering subs cls then ()
+    else raise Bug "Active.checkSaturated";
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* A type of active clause sets.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+type simplify = {subsume : bool, reduce : bool, rewrite : bool};
+
+type parameters =
+     {clause : Clause.parameters,
+      prefactor : simplify,
+      postfactor : simplify};
+
+datatype active =
+    Active of
+      {parameters : parameters,
+       clauses : Clause.clause IntMap.map,
+       units : Units.units,
+       rewrite : Rewrite.rewrite,
+       subsume : Clause.clause Subsume.subsume,
+       literals : (Clause.clause * Literal.literal) LiteralNet.literalNet,
+       equations :
+         (Clause.clause * Literal.literal * Rewrite.orient * Term.term)
+         TermNet.termNet,
+       subterms :
+         (Clause.clause * Literal.literal * Term.path * Term.term)
+         TermNet.termNet,
+       allSubterms : (Clause.clause * Term.term) TermNet.termNet};
+
+fun getSubsume (Active {subsume = s, ...}) = s;
+
+fun setRewrite active rewrite =
+    let
+      val Active
+            {parameters,clauses,units,subsume,literals,equations,
+             subterms,allSubterms,...} = active
+    in
+      Active
+        {parameters = parameters, clauses = clauses, units = units,
+         rewrite = rewrite, subsume = subsume, literals = literals,
+         equations = equations, subterms = subterms, allSubterms = allSubterms}
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val maxSimplify : simplify = {subsume = true, reduce = true, rewrite = true};
+
+val default : parameters =
+    {clause = Clause.default,
+     prefactor = maxSimplify,
+     postfactor = maxSimplify};
+
+fun empty parameters =
+    let
+      val {clause,...} = parameters
+      val {ordering,...} = clause
+    in
+      Active
+        {parameters = parameters,
+         clauses = IntMap.new (),
+         units = Units.empty,
+         rewrite = Rewrite.new (KnuthBendixOrder.compare ordering),
+         subsume = Subsume.new (),
+         literals = LiteralNet.new {fifo = false},
+         equations = TermNet.new {fifo = false},
+         subterms = TermNet.new {fifo = false},
+         allSubterms = TermNet.new {fifo = false}}
+    end;
+
+fun size (Active {clauses,...}) = IntMap.size clauses;
+
+fun clauses (Active {clauses = cls, ...}) =
+    let
+      fun add (_,cl,acc) = cl :: acc
+    in
+      IntMap.foldr add [] cls
+    end;
+
+fun saturation active =
+    let
+      fun remove (cl,(cls,subs)) =
+          let
+            val lits = Clause.literals cl
+          in
+            if Subsume.isStrictlySubsumed subs lits then (cls,subs)
+            else (cl :: cls, Subsume.insert subs (lits,()))
+          end
+
+      val cls = clauses active
+      val (cls,_) = foldl remove ([], Subsume.new ()) cls
+      val (cls,subs) = foldl remove ([], Subsume.new ()) cls
+
+(*MetisDebug
+      val Active {parameters,...} = active
+      val {clause,...} = parameters
+      val {ordering,...} = clause
+      val () = checkSaturated ordering subs cls
+*)
+    in
+      cls
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val pp =
+    let
+      fun toStr active = "Active{" ^ Int.toString (size active) ^ "}"
+    in
+      Print.ppMap toStr Print.ppString
+    end;
+
+(*MetisDebug
+local
+  fun ppField f ppA a =
+      Print.blockProgram Print.Inconsistent 2
+        [Print.addString (f ^ " ="),
+         Print.addBreak 1,
+         ppA a];
+
+  val ppClauses =
+      ppField "clauses"
+        (Print.ppMap IntMap.toList
+           (Print.ppList (Print.ppPair Print.ppInt Clause.pp)));
+
+  val ppRewrite = ppField "rewrite" Rewrite.pp;
+
+  val ppSubterms =
+      ppField "subterms"
+        (TermNet.pp
+           (Print.ppMap (fn (c,l,p,t) => ((Clause.id c, l, p), t))
+              (Print.ppPair
+                 (Print.ppTriple Print.ppInt Literal.pp Term.ppPath)
+                 Term.pp)));
+in
+  fun pp (Active {clauses,rewrite,subterms,...}) =
+      Print.blockProgram Print.Inconsistent 2
+        [Print.addString "Active",
+         Print.addBreak 1,
+         Print.blockProgram Print.Inconsistent 1
+           [Print.addString "{",
+            ppClauses clauses,
+            Print.addString ",",
+            Print.addBreak 1,
+            ppRewrite rewrite,
+(*MetisTrace5
+            Print.addString ",",
+            Print.addBreak 1,
+            ppSubterms subterms,
+*)
+            Print.skip],
+         Print.addString "}"];
+end;
+*)
+
+val toString = Print.toString pp;
+
+(* ------------------------------------------------------------------------- *)
+(* Simplify clauses.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun simplify simp units rewr subs =
+    let
+      val {subsume = s, reduce = r, rewrite = w} = simp
+
+      fun rewrite cl =
+          let
+            val cl' = Clause.rewrite rewr cl
+          in
+            if Clause.equalThms cl cl' then SOME cl else Clause.simplify cl'
+          end
+    in
+      fn cl =>
+         case Clause.simplify cl of
+           NONE => NONE
+         | SOME cl =>
+           case (if w then rewrite cl else SOME cl) of
+             NONE => NONE
+           | SOME cl =>
+             let
+               val cl = if r then Clause.reduce units cl else cl
+             in
+               if s andalso Clause.subsumes subs cl then NONE else SOME cl
+             end
+    end;
+
+(*MetisDebug
+val simplify = fn simp => fn units => fn rewr => fn subs => fn cl =>
+    let
+      fun traceCl s = Print.trace Clause.pp ("Active.simplify: " ^ s)
+(*MetisTrace4
+      val ppClOpt = Print.ppOption Clause.pp
+      val () = traceCl "cl" cl
+*)
+      val cl' = simplify simp units rewr subs cl
+(*MetisTrace4
+      val () = Print.trace ppClOpt "Active.simplify: cl'" cl'
+*)
+      val () =
+          case cl' of
+            NONE => ()
+          | SOME cl' =>
+            case
+              (case simplify simp units rewr subs cl' of
+                 NONE => SOME ("away", K ())
+               | SOME cl'' =>
+                 if Clause.equalThms cl' cl'' then NONE
+                 else SOME ("further", fn () => traceCl "cl''" cl'')) of
+              NONE => ()
+            | SOME (e,f) =>
+              let
+                val () = traceCl "cl" cl
+                val () = traceCl "cl'" cl'
+                val () = f ()
+              in
+                raise
+                  Bug
+                    ("Active.simplify: clause should have been simplified "^e)
+              end
+    in
+      cl'
+    end;
+*)
+
+fun simplifyActive simp active =
+    let
+      val Active {units,rewrite,subsume,...} = active
+    in
+      simplify simp units rewrite subsume
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Add a clause into the active set.                                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun addUnit units cl =
+    let
+      val th = Clause.thm cl
+    in
+      case total Thm.destUnit th of
+        SOME lit => Units.add units (lit,th)
+      | NONE => units
+    end;
+
+fun addRewrite rewrite cl =
+    let
+      val th = Clause.thm cl
+    in
+      case total Thm.destUnitEq th of
+        SOME l_r => Rewrite.add rewrite (Clause.id cl, (l_r,th))
+      | NONE => rewrite
+    end;
+
+fun addSubsume subsume cl = Subsume.insert subsume (Clause.literals cl, cl);
+
+fun addLiterals literals cl =
+    let
+      fun add (lit as (_,atm), literals) =
+          if Atom.isEq atm then literals
+          else LiteralNet.insert literals (lit,(cl,lit))
+    in
+      LiteralSet.foldl add literals (Clause.largestLiterals cl)
+    end;
+
+fun addEquations equations cl =
+    let
+      fun add ((lit,ort,tm),equations) =
+          TermNet.insert equations (tm,(cl,lit,ort,tm))
+    in
+      foldl add equations (Clause.largestEquations cl)
+    end;
+
+fun addSubterms subterms cl =
+    let
+      fun add ((lit,path,tm),subterms) =
+          TermNet.insert subterms (tm,(cl,lit,path,tm))
+    in
+      foldl add subterms (Clause.largestSubterms cl)
+    end;
+
+fun addAllSubterms allSubterms cl =
+    let
+      fun add ((_,_,tm),allSubterms) =
+          TermNet.insert allSubterms (tm,(cl,tm))
+    in
+      foldl add allSubterms (Clause.allSubterms cl)
+    end;
+
+fun addClause active cl =
+    let
+      val Active
+            {parameters,clauses,units,rewrite,subsume,literals,
+             equations,subterms,allSubterms} = active
+      val clauses = IntMap.insert clauses (Clause.id cl, cl)
+      and subsume = addSubsume subsume cl
+      and literals = addLiterals literals cl
+      and equations = addEquations equations cl
+      and subterms = addSubterms subterms cl
+      and allSubterms = addAllSubterms allSubterms cl
+    in
+      Active
+        {parameters = parameters, clauses = clauses, units = units,
+         rewrite = rewrite, subsume = subsume, literals = literals,
+         equations = equations, subterms = subterms,
+         allSubterms = allSubterms}
+    end;
+
+fun addFactorClause active cl =
+    let
+      val Active
+            {parameters,clauses,units,rewrite,subsume,literals,
+             equations,subterms,allSubterms} = active
+      val units = addUnit units cl
+      and rewrite = addRewrite rewrite cl
+    in
+      Active
+        {parameters = parameters, clauses = clauses, units = units,
+         rewrite = rewrite, subsume = subsume, literals = literals,
+         equations = equations, subterms = subterms, allSubterms = allSubterms}
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Derive (unfactored) consequences of a clause.                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun deduceResolution literals cl (lit as (_,atm), acc) =
+    let
+      fun resolve (cl_lit,acc) =
+          case total (Clause.resolve cl_lit) (cl,lit) of
+            SOME cl' => cl' :: acc
+          | NONE => acc
+(*MetisTrace4
+      val () = Print.trace Literal.pp "Active.deduceResolution: lit" lit
+*)
+    in
+      if Atom.isEq atm then acc
+      else foldl resolve acc (LiteralNet.unify literals (Literal.negate lit))
+    end;
+
+fun deduceParamodulationWith subterms cl ((lit,ort,tm),acc) =
+    let
+      fun para (cl_lit_path_tm,acc) =
+          case total (Clause.paramodulate (cl,lit,ort,tm)) cl_lit_path_tm of
+            SOME cl' => cl' :: acc
+          | NONE => acc
+    in
+      foldl para acc (TermNet.unify subterms tm)
+    end;
+
+fun deduceParamodulationInto equations cl ((lit,path,tm),acc) =
+    let
+      fun para (cl_lit_ort_tm,acc) =
+          case total (Clause.paramodulate cl_lit_ort_tm) (cl,lit,path,tm) of
+            SOME cl' => cl' :: acc
+          | NONE => acc
+    in
+      foldl para acc (TermNet.unify equations tm)
+    end;
+
+fun deduce active cl =
+    let
+      val Active {parameters,literals,equations,subterms,...} = active
+
+      val lits = Clause.largestLiterals cl
+      val eqns = Clause.largestEquations cl
+      val subtms =
+          if TermNet.null equations then [] else Clause.largestSubterms cl
+(*MetisTrace5
+      val () = Print.trace LiteralSet.pp "Active.deduce: lits" lits
+      val () = Print.trace
+                 (Print.ppList
+                    (Print.ppMap (fn (lit,ort,_) => (lit,ort))
+                      (Print.ppPair Literal.pp Rewrite.ppOrient)))
+                 "Active.deduce: eqns" eqns
+      val () = Print.trace
+                 (Print.ppList
+                    (Print.ppTriple Literal.pp Term.ppPath Term.pp))
+                 "Active.deduce: subtms" subtms
+*)
+
+      val acc = []
+      val acc = LiteralSet.foldl (deduceResolution literals cl) acc lits
+      val acc = foldl (deduceParamodulationWith subterms cl) acc eqns
+      val acc = foldl (deduceParamodulationInto equations cl) acc subtms
+      val acc = rev acc
+
+(*MetisTrace5
+      val () = Print.trace (Print.ppList Clause.pp) "Active.deduce: acc" acc
+*)
+    in
+      acc
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Extract clauses from the active set that can be simplified.               *)
+(* ------------------------------------------------------------------------- *)
+
+local
+  fun clause_rewritables active =
+      let
+        val Active {clauses,rewrite,...} = active
+
+        fun rewr (id,cl,ids) =
+            let
+              val cl' = Clause.rewrite rewrite cl
+            in
+              if Clause.equalThms cl cl' then ids else IntSet.add ids id
+            end
+      in
+        IntMap.foldr rewr IntSet.empty clauses
+      end;
+
+  fun orderedRedexResidues (((l,r),_),ort) =
+      case ort of
+        NONE => []
+      | SOME Rewrite.LeftToRight => [(l,r,true)]
+      | SOME Rewrite.RightToLeft => [(r,l,true)];
+
+  fun unorderedRedexResidues (((l,r),_),ort) =
+      case ort of
+        NONE => [(l,r,false),(r,l,false)]
+      | SOME _ => [];
+
+  fun rewrite_rewritables active rewr_ids =
+      let
+        val Active {parameters,rewrite,clauses,allSubterms,...} = active
+        val {clause = {ordering,...}, ...} = parameters
+        val order = KnuthBendixOrder.compare ordering
+
+        fun addRewr (id,acc) =
+            if IntMap.inDomain id clauses then IntSet.add acc id else acc
+
+        fun addReduce ((l,r,ord),acc) =
+            let
+              fun isValidRewr tm =
+                  case total (Subst.match Subst.empty l) tm of
+                    NONE => false
+                  | SOME sub =>
+                    ord orelse
+                    let
+                      val tm' = Subst.subst (Subst.normalize sub) r
+                    in
+                      order (tm,tm') = SOME GREATER
+                    end
+
+              fun addRed ((cl,tm),acc) =
+                  let
+(*MetisTrace5
+                    val () = Print.trace Clause.pp "Active.addRed: cl" cl
+                    val () = Print.trace Term.pp "Active.addRed: tm" tm
+*)
+                    val id = Clause.id cl
+                  in
+                    if IntSet.member id acc then acc
+                    else if not (isValidRewr tm) then acc
+                    else IntSet.add acc id
+                  end
+
+(*MetisTrace5
+              val () = Print.trace Term.pp "Active.addReduce: l" l
+              val () = Print.trace Term.pp "Active.addReduce: r" r
+              val () = Print.trace Print.ppBool "Active.addReduce: ord" ord
+*)
+            in
+              List.foldl addRed acc (TermNet.matched allSubterms l)
+            end
+
+        fun addEquation redexResidues (id,acc) =
+            case Rewrite.peek rewrite id of
+              NONE => acc
+            | SOME eqn_ort => List.foldl addReduce acc (redexResidues eqn_ort)
+
+        val addOrdered = addEquation orderedRedexResidues
+
+        val addUnordered = addEquation unorderedRedexResidues
+
+        val ids = IntSet.empty
+        val ids = List.foldl addRewr ids rewr_ids
+        val ids = List.foldl addOrdered ids rewr_ids
+        val ids = List.foldl addUnordered ids rewr_ids
+      in
+        ids
+      end;
+
+  fun choose_clause_rewritables active ids = size active <= length ids
+
+  fun rewritables active ids =
+      if choose_clause_rewritables active ids then clause_rewritables active
+      else rewrite_rewritables active ids;
+
+(*MetisDebug
+  val rewritables = fn active => fn ids =>
+      let
+        val clause_ids = clause_rewritables active
+        val rewrite_ids = rewrite_rewritables active ids
+
+        val () =
+            if IntSet.equal rewrite_ids clause_ids then ()
+            else
+              let
+                val ppIdl = Print.ppList Print.ppInt
+                val ppIds = Print.ppMap IntSet.toList ppIdl
+                val () = Print.trace pp "Active.rewritables: active" active
+                val () = Print.trace ppIdl "Active.rewritables: ids" ids
+                val () = Print.trace ppIds
+                           "Active.rewritables: clause_ids" clause_ids
+                val () = Print.trace ppIds
+                           "Active.rewritables: rewrite_ids" rewrite_ids
+              in
+                raise Bug "Active.rewritables: ~(rewrite_ids SUBSET clause_ids)"
+              end
+      in
+        if choose_clause_rewritables active ids then clause_ids else rewrite_ids
+      end;
+*)
+
+  fun delete active ids =
+      if IntSet.null ids then active
+      else
+        let
+          fun idPred id = not (IntSet.member id ids)
+
+          fun clausePred cl = idPred (Clause.id cl)
+
+          val Active
+                {parameters,
+                 clauses,
+                 units,
+                 rewrite,
+                 subsume,
+                 literals,
+                 equations,
+                 subterms,
+                 allSubterms} = active
+
+          val clauses = IntMap.filter (idPred o fst) clauses
+          and subsume = Subsume.filter clausePred subsume
+          and literals = LiteralNet.filter (clausePred o #1) literals
+          and equations = TermNet.filter (clausePred o #1) equations
+          and subterms = TermNet.filter (clausePred o #1) subterms
+          and allSubterms = TermNet.filter (clausePred o fst) allSubterms
+        in
+          Active
+            {parameters = parameters,
+             clauses = clauses,
+             units = units,
+             rewrite = rewrite,
+             subsume = subsume,
+             literals = literals,
+             equations = equations,
+             subterms = subterms,
+             allSubterms = allSubterms}
+        end;
+in
+  fun extract_rewritables (active as Active {clauses,rewrite,...}) =
+      if Rewrite.isReduced rewrite then (active,[])
+      else
+        let
+(*MetisTrace3
+          val () = trace "Active.extract_rewritables: inter-reducing\n"
+*)
+          val (rewrite,ids) = Rewrite.reduce' rewrite
+          val active = setRewrite active rewrite
+          val ids = rewritables active ids
+          val cls = IntSet.transform (IntMap.get clauses) ids
+(*MetisTrace3
+          val ppCls = Print.ppList Clause.pp
+          val () = Print.trace ppCls "Active.extract_rewritables: cls" cls
+*)
+        in
+          (delete active ids, cls)
+        end
+(*MetisDebug
+        handle Error err =>
+          raise Bug ("Active.extract_rewritables: shouldn't fail\n" ^ err);
+*)
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Factor clauses.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+local
+  fun prefactor_simplify active subsume =
+      let
+        val Active {parameters,units,rewrite,...} = active
+        val {prefactor,...} = parameters
+      in
+        simplify prefactor units rewrite subsume
+      end;
+
+  fun postfactor_simplify active subsume =
+      let
+        val Active {parameters,units,rewrite,...} = active
+        val {postfactor,...} = parameters
+      in
+        simplify postfactor units rewrite subsume
+      end;
+
+  val sort_utilitywise =
+      let
+        fun utility cl =
+            case LiteralSet.size (Clause.literals cl) of
+              0 => ~1
+            | 1 => if Thm.isUnitEq (Clause.thm cl) then 0 else 1
+            | n => n
+      in
+        sortMap utility Int.compare
+      end;
+
+  fun factor_add (cl, active_subsume_acc as (active,subsume,acc)) =
+      case postfactor_simplify active subsume cl of
+        NONE => active_subsume_acc
+      | SOME cl =>
+        let
+          val active = addFactorClause active cl
+          and subsume = addSubsume subsume cl
+          and acc = cl :: acc
+        in
+          (active,subsume,acc)
+        end;
+
+  fun factor1 (cl, active_subsume_acc as (active,subsume,_)) =
+      case prefactor_simplify active subsume cl of
+        NONE => active_subsume_acc
+      | SOME cl =>
+        let
+          val cls = sort_utilitywise (cl :: Clause.factor cl)
+        in
+          foldl factor_add active_subsume_acc cls
+        end;
+
+  fun factor' active acc [] = (active, rev acc)
+    | factor' active acc cls =
+      let
+        val cls = sort_utilitywise cls
+        val subsume = getSubsume active
+        val (active,_,acc) = foldl factor1 (active,subsume,acc) cls
+        val (active,cls) = extract_rewritables active
+      in
+        factor' active acc cls
+      end;
+in
+  fun factor active cls = factor' active [] cls;
+end;
+
+(*MetisTrace4
+val factor = fn active => fn cls =>
+    let
+      val ppCls = Print.ppList Clause.pp
+      val () = Print.trace ppCls "Active.factor: cls" cls
+      val (active,cls') = factor active cls
+      val () = Print.trace ppCls "Active.factor: cls'" cls'
+    in
+      (active,cls')
+    end;
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Create a new active clause set and initialize clauses.                    *)
+(* ------------------------------------------------------------------------- *)
+
+fun new parameters {axioms,conjecture} =
+    let
+      val {clause,...} = parameters
+
+      fun mk_clause th =
+          Clause.mk {parameters = clause, id = Clause.newId (), thm = th}
+
+      val active = empty parameters
+      val (active,axioms) = factor active (map mk_clause axioms)
+      val (active,conjecture) = factor active (map mk_clause conjecture)
+    in
+      (active, {axioms = axioms, conjecture = conjecture})
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Add a clause into the active set and deduce all consequences.             *)
+(* ------------------------------------------------------------------------- *)
+
+fun add active cl =
+    case simplifyActive maxSimplify active cl of
+      NONE => (active,[])
+    | SOME cl' =>
+      if Clause.isContradiction cl' then (active,[cl'])
+      else if not (Clause.equalThms cl cl') then factor active [cl']
+      else
+        let
+(*MetisTrace2
+          val () = Print.trace Clause.pp "Active.add: cl" cl
+*)
+          val active = addClause active cl
+          val cl = Clause.freshVars cl
+          val cls = deduce active cl
+          val (active,cls) = factor active cls
+(*MetisTrace2
+          val ppCls = Print.ppList Clause.pp
+          val () = Print.trace ppCls "Active.add: cls" cls
+*)
+        in
+          (active,cls)
+        end;
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Atom.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,141 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC ATOMS                                                   *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Atom =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic atoms.                               *)
+(* ------------------------------------------------------------------------- *)
+
+type relationName = Name.name
+
+type relation = relationName * int
+
+type atom = relationName * Term.term list
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val name : atom -> relationName
+
+val arguments : atom -> Term.term list
+
+val arity : atom -> int
+
+val relation : atom -> relation
+
+val functions : atom -> NameAritySet.set
+
+val functionNames : atom -> NameSet.set
+
+(* Binary relations *)
+
+val mkBinop : relationName -> Term.term * Term.term -> atom
+
+val destBinop : relationName -> atom -> Term.term * Term.term
+
+val isBinop : relationName -> atom -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* The size of an atom in symbols.                                           *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : atom -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for atoms.                                    *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : atom * atom -> order
+
+val equal : atom -> atom -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val subterm : atom -> Term.path -> Term.term
+
+val subterms : atom -> (Term.path * Term.term) list
+
+val replace : atom -> Term.path * Term.term -> atom
+
+val find : (Term.term -> bool) -> atom -> Term.path option
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Term.var -> atom -> bool
+
+val freeVars : atom -> NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions.                                                            *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Subst.subst -> atom -> atom
+
+(* ------------------------------------------------------------------------- *)
+(* Matching.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val match : Subst.subst -> atom -> atom -> Subst.subst  (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* Unification.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val unify : Subst.subst -> atom -> atom -> Subst.subst  (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+val eqRelationName : relationName
+
+val eqRelation : relation
+
+val mkEq : Term.term * Term.term -> atom
+
+val destEq : atom -> Term.term * Term.term
+
+val isEq : atom -> bool
+
+val mkRefl : Term.term -> atom
+
+val destRefl : atom -> Term.term
+
+val isRefl : atom -> bool
+
+val sym : atom -> atom  (* raises Error if given a refl *)
+
+val lhs : atom -> Term.term
+
+val rhs : atom -> Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations.                          *)
+(* ------------------------------------------------------------------------- *)
+
+val typedSymbols : atom -> int
+
+val nonVarTypedSubterms : atom -> (Term.path * Term.term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : atom Print.pp
+
+val toString : atom -> string
+
+val fromString : string -> atom
+
+val parse : Term.term Parse.quotation -> atom
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Atom.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,247 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC ATOMS                                                   *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Atom :> Atom =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic atoms.                               *)
+(* ------------------------------------------------------------------------- *)
+
+type relationName = Name.name;
+
+type relation = relationName * int;
+
+type atom = relationName * Term.term list;
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun name ((rel,_) : atom) = rel;
+
+fun arguments ((_,args) : atom) = args;
+
+fun arity atm = length (arguments atm);
+
+fun relation atm = (name atm, arity atm);
+
+val functions =
+    let
+      fun f (tm,acc) = NameAritySet.union (Term.functions tm) acc
+    in
+      fn atm => foldl f NameAritySet.empty (arguments atm)
+    end;
+
+val functionNames =
+    let
+      fun f (tm,acc) = NameSet.union (Term.functionNames tm) acc
+    in
+      fn atm => foldl f NameSet.empty (arguments atm)
+    end;
+
+(* Binary relations *)
+
+fun mkBinop p (a,b) : atom = (p,[a,b]);
+
+fun destBinop p (x,[a,b]) =
+    if Name.equal x p then (a,b) else raise Error "Atom.destBinop: wrong binop"
+  | destBinop _ _ = raise Error "Atom.destBinop: not a binop";
+
+fun isBinop p = can (destBinop p);
+
+(* ------------------------------------------------------------------------- *)
+(* The size of an atom in symbols.                                           *)
+(* ------------------------------------------------------------------------- *)
+
+fun symbols atm = foldl (fn (tm,z) => Term.symbols tm + z) 1 (arguments atm);
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for atoms.                                    *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare ((p1,tms1),(p2,tms2)) =
+    case Name.compare (p1,p2) of
+      LESS => LESS
+    | EQUAL => lexCompare Term.compare (tms1,tms2)
+    | GREATER => GREATER;
+
+fun equal atm1 atm2 = compare (atm1,atm2) = EQUAL;
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun subterm _ [] = raise Bug "Atom.subterm: empty path"
+  | subterm ((_,tms) : atom) (h :: t) =
+    if h >= length tms then raise Error "Atom.subterm: bad path"
+    else Term.subterm (List.nth (tms,h)) t;
+
+fun subterms ((_,tms) : atom) =
+    let
+      fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
+    in
+      foldl f [] (enumerate tms)
+    end;
+
+fun replace _ ([],_) = raise Bug "Atom.replace: empty path"
+  | replace (atm as (rel,tms)) (h :: t, res) : atom =
+    if h >= length tms then raise Error "Atom.replace: bad path"
+    else
+      let
+        val tm = List.nth (tms,h)
+        val tm' = Term.replace tm (t,res)
+      in
+        if Portable.pointerEqual (tm,tm') then atm
+        else (rel, updateNth (h,tm') tms)
+      end;
+
+fun find pred =
+    let
+      fun f (i,tm) =
+          case Term.find pred tm of
+            SOME path => SOME (i :: path)
+          | NONE => NONE
+    in
+      fn (_,tms) : atom => first f (enumerate tms)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+fun freeIn v atm = List.exists (Term.freeIn v) (arguments atm);
+
+val freeVars =
+    let
+      fun f (tm,acc) = NameSet.union (Term.freeVars tm) acc
+    in
+      fn atm => foldl f NameSet.empty (arguments atm)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions.                                                            *)
+(* ------------------------------------------------------------------------- *)
+
+fun subst sub (atm as (p,tms)) : atom =
+    let
+      val tms' = Sharing.map (Subst.subst sub) tms
+    in
+      if Portable.pointerEqual (tms',tms) then atm else (p,tms')
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Matching.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+local
+  fun matchArg ((tm1,tm2),sub) = Subst.match sub tm1 tm2;
+in
+  fun match sub (p1,tms1) (p2,tms2) =
+      let
+        val _ = (Name.equal p1 p2 andalso length tms1 = length tms2) orelse
+                raise Error "Atom.match"
+      in
+        foldl matchArg sub (zip tms1 tms2)
+      end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Unification.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+local
+  fun unifyArg ((tm1,tm2),sub) = Subst.unify sub tm1 tm2;
+in
+  fun unify sub (p1,tms1) (p2,tms2) =
+      let
+        val _ = (Name.equal p1 p2 andalso length tms1 = length tms2) orelse
+                raise Error "Atom.unify"
+      in
+        foldl unifyArg sub (zip tms1 tms2)
+      end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+val eqRelationName = Name.fromString "=";
+
+val eqRelationArity = 2;
+
+val eqRelation = (eqRelationName,eqRelationArity);
+
+val mkEq = mkBinop eqRelationName;
+
+fun destEq x = destBinop eqRelationName x;
+
+fun isEq x = isBinop eqRelationName x;
+
+fun mkRefl tm = mkEq (tm,tm);
+
+fun destRefl atm =
+    let
+      val (l,r) = destEq atm
+      val _ = Term.equal l r orelse raise Error "Atom.destRefl"
+    in
+      l
+    end;
+
+fun isRefl x = can destRefl x;
+
+fun sym atm =
+    let
+      val (l,r) = destEq atm
+      val _ = not (Term.equal l r) orelse raise Error "Atom.sym: refl"
+    in
+      mkEq (r,l)
+    end;
+
+fun lhs atm = fst (destEq atm);
+
+fun rhs atm = snd (destEq atm);
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations.                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun typedSymbols ((_,tms) : atom) =
+    foldl (fn (tm,z) => Term.typedSymbols tm + z) 1 tms;
+
+fun nonVarTypedSubterms (_,tms) =
+    let
+      fun addArg ((n,arg),acc) =
+          let
+            fun addTm ((path,tm),acc) = (n :: path, tm) :: acc
+          in
+            foldl addTm acc (Term.nonVarTypedSubterms arg)
+          end
+    in
+      foldl addArg [] (enumerate tms)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val pp = Print.ppMap Term.Fn Term.pp;
+
+val toString = Print.toString pp;
+
+fun fromString s = Term.destFn (Term.fromString s);
+
+val parse = Parse.parseQuotation Term.toString fromString;
+
+end
+
+structure AtomOrdered =
+struct type t = Atom.atom val compare = Atom.compare end
+
+structure AtomMap = KeyMap (AtomOrdered);
+
+structure AtomSet = ElementSet (AtomMap);
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/AtomNet.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,48 @@
+(* ========================================================================= *)
+(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS              *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature AtomNet =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of atom sets that can be efficiently matched and unified.          *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = {fifo : bool}
+
+type 'a atomNet
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val new : parameters -> 'a atomNet
+
+val size : 'a atomNet -> int
+
+val insert : 'a atomNet -> Atom.atom * 'a -> 'a atomNet
+
+val fromList : parameters -> (Atom.atom * 'a) list -> 'a atomNet
+
+val filter : ('a -> bool) -> 'a atomNet -> 'a atomNet
+
+val toString : 'a atomNet -> string
+
+val pp : 'a Print.pp -> 'a atomNet Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* Matching and unification queries.                                         *)
+(*                                                                           *)
+(* These function return OVER-APPROXIMATIONS!                                *)
+(* Filter afterwards to get the precise set of satisfying values.            *)
+(* ------------------------------------------------------------------------- *)
+
+val match : 'a atomNet -> Atom.atom -> 'a list
+
+val matched : 'a atomNet -> Atom.atom -> 'a list
+
+val unify : 'a atomNet -> Atom.atom -> 'a list
+
+end
--- /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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Clause.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,107 @@
+(* ========================================================================= *)
+(* CLAUSE = ID + THEOREM                                                     *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Clause =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of clause.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+datatype literalOrder =
+    NoLiteralOrder
+  | UnsignedLiteralOrder
+  | PositiveLiteralOrder
+
+type parameters =
+     {ordering : KnuthBendixOrder.kbo,
+      orderLiterals : literalOrder,
+      orderTerms : bool}
+
+type clauseId = int
+
+type clauseInfo = {parameters : parameters, id : clauseId, thm : Thm.thm}
+
+type clause
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val default : parameters
+
+val newId : unit -> clauseId
+
+val mk : clauseInfo -> clause
+
+val dest : clause -> clauseInfo
+
+val id : clause -> clauseId
+
+val thm : clause -> Thm.thm
+
+val equalThms : clause -> clause -> bool
+
+val literals : clause -> Thm.clause
+
+val isTautology : clause -> bool
+
+val isContradiction : clause -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* The term ordering is used to cut down inferences.                         *)
+(* ------------------------------------------------------------------------- *)
+
+val largestLiterals : clause -> LiteralSet.set
+
+val largestEquations :
+    clause -> (Literal.literal * Rewrite.orient * Term.term) list
+
+val largestSubterms :
+    clause -> (Literal.literal * Term.path * Term.term) list
+
+val allSubterms : clause -> (Literal.literal * Term.path * Term.term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Subsumption.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val subsumes : clause Subsume.subsume -> clause -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Simplifying rules: these preserve the clause id.                          *)
+(* ------------------------------------------------------------------------- *)
+
+val freshVars : clause -> clause
+
+val simplify : clause -> clause option
+
+val reduce : Units.units -> clause -> clause
+
+val rewrite : Rewrite.rewrite -> clause -> clause
+
+(* ------------------------------------------------------------------------- *)
+(* Inference rules: these generate new clause ids.                           *)
+(* ------------------------------------------------------------------------- *)
+
+val factor : clause -> clause list
+
+val resolve : clause * Literal.literal -> clause * Literal.literal -> clause
+
+val paramodulate :
+    clause * Literal.literal * Rewrite.orient * Term.term ->
+    clause * Literal.literal * Term.path * Term.term -> clause
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val showId : bool ref
+
+val pp : clause Print.pp
+
+val toString : clause -> string
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Clause.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,360 @@
+(* ========================================================================= *)
+(* CLAUSE = ID + THEOREM                                                     *)
+(* Copyright (c) 2002-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Clause :> Clause =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val newId =
+    let
+      val r = ref 0
+    in
+      fn () => case r of ref n => let val () = r := n + 1 in n end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of clause.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+datatype literalOrder =
+    NoLiteralOrder
+  | UnsignedLiteralOrder
+  | PositiveLiteralOrder;
+
+type parameters =
+     {ordering : KnuthBendixOrder.kbo,
+      orderLiterals : literalOrder,
+      orderTerms : bool};
+
+type clauseId = int;
+
+type clauseInfo = {parameters : parameters, id : clauseId, thm : Thm.thm};
+
+datatype clause = Clause of clauseInfo;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val showId = ref false;
+
+local
+  val ppIdThm = Print.ppPair Print.ppInt Thm.pp;
+in
+  fun pp (Clause {id,thm,...}) =
+      if !showId then ppIdThm (id,thm) else Thm.pp thm;
+end;
+
+fun toString cl = Print.toString pp cl;
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val default : parameters =
+    {ordering = KnuthBendixOrder.default,
+     orderLiterals = PositiveLiteralOrder,
+     orderTerms = true};
+
+fun mk info = Clause info
+
+fun dest (Clause info) = info;
+
+fun id (Clause {id = i, ...}) = i;
+
+fun thm (Clause {thm = th, ...}) = th;
+
+fun equalThms cl cl' = Thm.equal (thm cl) (thm cl');
+
+fun new parameters thm =
+    Clause {parameters = parameters, id = newId (), thm = thm};
+
+fun literals cl = Thm.clause (thm cl);
+
+fun isTautology (Clause {thm,...}) = Thm.isTautology thm;
+
+fun isContradiction (Clause {thm,...}) = Thm.isContradiction thm;
+
+(* ------------------------------------------------------------------------- *)
+(* The term ordering is used to cut down inferences.                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun strictlyLess ordering x_y =
+    case KnuthBendixOrder.compare ordering x_y of
+      SOME LESS => true
+    | _ => false;
+
+fun isLargerTerm ({ordering,orderTerms,...} : parameters) l_r =
+    not orderTerms orelse not (strictlyLess ordering l_r);
+
+local
+  fun atomToTerms atm =
+      case total Atom.destEq atm of
+        NONE => [Term.Fn atm]
+      | SOME (l,r) => [l,r];
+
+  fun notStrictlyLess ordering (xs,ys) =
+      let
+        fun less x = List.exists (fn y => strictlyLess ordering (x,y)) ys
+      in
+        not (List.all less xs)
+      end;
+in
+  fun isLargerLiteral ({ordering,orderLiterals,...} : parameters) lits =
+      case orderLiterals of
+        NoLiteralOrder => K true
+      | UnsignedLiteralOrder =>
+        let
+          fun addLit ((_,atm),acc) = atomToTerms atm @ acc
+
+          val tms = LiteralSet.foldl addLit [] lits
+        in
+          fn (_,atm') => notStrictlyLess ordering (atomToTerms atm', tms)
+        end
+      | PositiveLiteralOrder =>
+        case LiteralSet.findl (K true) lits of
+          NONE => K true
+        | SOME (pol,_) =>
+          let
+            fun addLit ((p,atm),acc) =
+                if p = pol then atomToTerms atm @ acc else acc
+
+            val tms = LiteralSet.foldl addLit [] lits
+          in
+            fn (pol',atm') =>
+               if pol <> pol' then pol
+               else notStrictlyLess ordering (atomToTerms atm', tms)
+          end;
+end;
+
+fun largestLiterals (Clause {parameters,thm,...}) =
+    let
+      val litSet = Thm.clause thm
+      val isLarger = isLargerLiteral parameters litSet
+      fun addLit (lit,s) = if isLarger lit then LiteralSet.add s lit else s
+    in
+      LiteralSet.foldr addLit LiteralSet.empty litSet
+    end;
+
+(*MetisTrace6
+val largestLiterals = fn cl =>
+    let
+      val ppResult = LiteralSet.pp
+      val () = Print.trace pp "Clause.largestLiterals: cl" cl
+      val result = largestLiterals cl
+      val () = Print.trace ppResult "Clause.largestLiterals: result" result
+    in
+      result
+    end;
+*)
+
+fun largestEquations (cl as Clause {parameters,...}) =
+    let
+      fun addEq lit ort (l_r as (l,_)) acc =
+          if isLargerTerm parameters l_r then (lit,ort,l) :: acc else acc
+
+      fun addLit (lit,acc) =
+          case total Literal.destEq lit of
+            NONE => acc
+          | SOME (l,r) =>
+            let
+              val acc = addEq lit Rewrite.RightToLeft (r,l) acc
+              val acc = addEq lit Rewrite.LeftToRight (l,r) acc
+            in
+              acc
+            end
+    in
+      LiteralSet.foldr addLit [] (largestLiterals cl)
+    end;
+
+local
+  fun addLit (lit,acc) =
+      let
+        fun addTm ((path,tm),acc) = (lit,path,tm) :: acc
+      in
+        foldl addTm acc (Literal.nonVarTypedSubterms lit)
+      end;
+in
+  fun largestSubterms cl = LiteralSet.foldl addLit [] (largestLiterals cl);
+
+  fun allSubterms cl = LiteralSet.foldl addLit [] (literals cl);
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Subsumption.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun subsumes (subs : clause Subsume.subsume) cl =
+    Subsume.isStrictlySubsumed subs (literals cl);
+
+(* ------------------------------------------------------------------------- *)
+(* Simplifying rules: these preserve the clause id.                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun freshVars (Clause {parameters,id,thm}) =
+    Clause {parameters = parameters, id = id, thm = Rule.freshVars thm};
+
+fun simplify (Clause {parameters,id,thm}) =
+    case Rule.simplify thm of
+      NONE => NONE
+    | SOME thm => SOME (Clause {parameters = parameters, id = id, thm = thm});
+
+fun reduce units (Clause {parameters,id,thm}) =
+    Clause {parameters = parameters, id = id, thm = Units.reduce units thm};
+
+fun rewrite rewr (cl as Clause {parameters,id,thm}) =
+    let
+      fun simp th =
+          let
+            val {ordering,...} = parameters
+            val cmp = KnuthBendixOrder.compare ordering
+          in
+            Rewrite.rewriteIdRule rewr cmp id th
+          end
+
+(*MetisTrace4
+      val () = Print.trace Rewrite.pp "Clause.rewrite: rewr" rewr
+      val () = Print.trace Print.ppInt "Clause.rewrite: id" id
+      val () = Print.trace pp "Clause.rewrite: cl" cl
+*)
+
+      val thm =
+          case Rewrite.peek rewr id of
+            NONE => simp thm
+          | SOME ((_,thm),_) => if Rewrite.isReduced rewr then thm else simp thm
+
+      val result = Clause {parameters = parameters, id = id, thm = thm}
+
+(*MetisTrace4
+      val () = Print.trace pp "Clause.rewrite: result" result
+*)
+    in
+      result
+    end
+(*MetisDebug
+    handle Error err => raise Error ("Clause.rewrite:\n" ^ err);
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Inference rules: these generate new clause ids.                           *)
+(* ------------------------------------------------------------------------- *)
+
+fun factor (cl as Clause {parameters,thm,...}) =
+    let
+      val lits = largestLiterals cl
+
+      fun apply sub = new parameters (Thm.subst sub thm)
+    in
+      map apply (Rule.factor' lits)
+    end;
+
+(*MetisTrace5
+val factor = fn cl =>
+    let
+      val () = Print.trace pp "Clause.factor: cl" cl
+      val result = factor cl
+      val () = Print.trace (Print.ppList pp) "Clause.factor: result" result
+    in
+      result
+    end;
+*)
+
+fun resolve (cl1,lit1) (cl2,lit2) =
+    let
+(*MetisTrace5
+      val () = Print.trace pp "Clause.resolve: cl1" cl1
+      val () = Print.trace Literal.pp "Clause.resolve: lit1" lit1
+      val () = Print.trace pp "Clause.resolve: cl2" cl2
+      val () = Print.trace Literal.pp "Clause.resolve: lit2" lit2
+*)
+      val Clause {parameters, thm = th1, ...} = cl1
+      and Clause {thm = th2, ...} = cl2
+      val sub = Literal.unify Subst.empty lit1 (Literal.negate lit2)
+(*MetisTrace5
+      val () = Print.trace Subst.pp "Clause.resolve: sub" sub
+*)
+      val lit1 = Literal.subst sub lit1
+      val lit2 = Literal.negate lit1
+      val th1 = Thm.subst sub th1
+      and th2 = Thm.subst sub th2
+      val _ = isLargerLiteral parameters (Thm.clause th1) lit1 orelse
+(*MetisTrace5
+              (trace "Clause.resolve: th1 violates ordering\n"; false) orelse
+*)
+              raise Error "resolve: clause1: ordering constraints"
+      val _ = isLargerLiteral parameters (Thm.clause th2) lit2 orelse
+(*MetisTrace5
+              (trace "Clause.resolve: th2 violates ordering\n"; false) orelse
+*)
+              raise Error "resolve: clause2: ordering constraints"
+      val th = Thm.resolve lit1 th1 th2
+(*MetisTrace5
+      val () = Print.trace Thm.pp "Clause.resolve: th" th
+*)
+      val cl = Clause {parameters = parameters, id = newId (), thm = th}
+(*MetisTrace5
+      val () = Print.trace pp "Clause.resolve: cl" cl
+*)
+    in
+      cl
+    end;
+
+fun paramodulate (cl1,lit1,ort1,tm1) (cl2,lit2,path2,tm2) =
+    let
+(*MetisTrace5
+      val () = Print.trace pp "Clause.paramodulate: cl1" cl1
+      val () = Print.trace Literal.pp "Clause.paramodulate: lit1" lit1
+      val () = Print.trace Rewrite.ppOrient "Clause.paramodulate: ort1" ort1
+      val () = Print.trace Term.pp "Clause.paramodulate: tm1" tm1
+      val () = Print.trace pp "Clause.paramodulate: cl2" cl2
+      val () = Print.trace Literal.pp "Clause.paramodulate: lit2" lit2
+      val () = Print.trace Term.ppPath "Clause.paramodulate: path2" path2
+      val () = Print.trace Term.pp "Clause.paramodulate: tm2" tm2
+*)
+      val Clause {parameters, thm = th1, ...} = cl1
+      and Clause {thm = th2, ...} = cl2
+      val sub = Subst.unify Subst.empty tm1 tm2
+      val lit1 = Literal.subst sub lit1
+      and lit2 = Literal.subst sub lit2
+      and th1 = Thm.subst sub th1
+      and th2 = Thm.subst sub th2
+
+      val _ = isLargerLiteral parameters (Thm.clause th1) lit1 orelse
+              raise Error "Clause.paramodulate: with clause: ordering"
+      val _ = isLargerLiteral parameters (Thm.clause th2) lit2 orelse
+              raise Error "Clause.paramodulate: into clause: ordering"
+
+      val eqn = (Literal.destEq lit1, th1)
+      val eqn as (l_r,_) =
+          case ort1 of
+            Rewrite.LeftToRight => eqn
+          | Rewrite.RightToLeft => Rule.symEqn eqn
+(*MetisTrace6
+      val () = Print.trace Rule.ppEquation "Clause.paramodulate: eqn" eqn
+*)
+      val _ = isLargerTerm parameters l_r orelse
+              raise Error "Clause.paramodulate: equation: ordering constraints"
+      val th = Rule.rewrRule eqn lit2 path2 th2
+(*MetisTrace5
+      val () = Print.trace Thm.pp "Clause.paramodulate: th" th
+*)
+    in
+      Clause {parameters = parameters, id = newId (), thm = th}
+    end
+(*MetisTrace5
+    handle Error err =>
+      let
+        val () = trace ("Clause.paramodulate: failed: " ^ err ^ "\n")
+      in
+        raise Error err
+      end;
+*)
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/ElementSet.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,175 @@
+(* ========================================================================= *)
+(* FINITE SETS WITH A FIXED ELEMENT TYPE                                     *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+signature ElementSet =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of set elements.                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+type element
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite sets.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+type set
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors.                                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val empty : set
+
+val singleton : element -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Set size.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val null : set -> bool
+
+val size : set -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Querying.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val peek : set -> element -> element option
+
+val member : element -> set -> bool
+
+val pick : set -> element  (* an arbitrary element *)
+
+val nth : set -> int -> element  (* in the range [0,size-1] *)
+
+val random : set -> element
+
+(* ------------------------------------------------------------------------- *)
+(* Adding.                                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+val add : set -> element -> set
+
+val addList : set -> element list -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Removing.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val delete : set -> element -> set  (* must be present *)
+
+val remove : set -> element -> set
+
+val deletePick : set -> element * set
+
+val deleteNth : set -> int -> element * set
+
+val deleteRandom : set -> element * set
+
+(* ------------------------------------------------------------------------- *)
+(* Joining.                                                                  *)
+(* ------------------------------------------------------------------------- *)
+
+val union : set -> set -> set
+
+val unionList : set list -> set
+
+val intersect : set -> set -> set
+
+val intersectList : set list -> set
+
+val difference : set -> set -> set
+
+val symmetricDifference : set -> set -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+val filter : (element -> bool) -> set -> set
+
+val partition : (element -> bool) -> set -> set * set
+
+val app : (element -> unit) -> set -> unit
+
+val foldl : (element * 's -> 's) -> 's -> set -> 's
+
+val foldr : (element * 's -> 's) -> 's -> set -> 's
+
+(* ------------------------------------------------------------------------- *)
+(* Searching.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val findl : (element -> bool) -> set -> element option
+
+val findr : (element -> bool) -> set -> element option
+
+val firstl : (element -> 'a option) -> set -> 'a option
+
+val firstr : (element -> 'a option) -> set -> 'a option
+
+val exists : (element -> bool) -> set -> bool
+
+val all : (element -> bool) -> set -> bool
+
+val count : (element -> bool) -> set -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : set * set -> order
+
+val equal : set -> set -> bool
+
+val subset : set -> set -> bool
+
+val disjoint : set -> set -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val transform : (element -> 'a) -> set -> 'a list
+
+val toList : set -> element list
+
+val fromList : element list -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from maps.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a map
+
+val mapPartial : (element -> 'a option) -> set -> 'a map
+
+val map : (element -> 'a) -> set -> 'a map
+
+val domain : 'a map -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val toString : set -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over sets                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+type iterator
+
+val mkIterator : set -> iterator option
+
+val mkRevIterator : set -> iterator option
+
+val readIterator : iterator -> element
+
+val advanceIterator : iterator -> iterator option
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/ElementSet.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,347 @@
+(* ========================================================================= *)
+(* FINITE SETS WITH A FIXED ELEMENT TYPE                                     *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+functor ElementSet (KM : KeyMap) :> ElementSet
+where type element = KM.key and type 'a map = 'a KM.map =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* A type of set elements.                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+type element = KM.key;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite sets.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a map = 'a KM.map;
+
+datatype set = Set of unit map;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from maps.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun dest (Set m) = m;
+
+fun mapPartial f =
+    let
+      fun mf (elt,()) = f elt
+    in
+      fn Set m => KM.mapPartial mf m
+    end;
+
+fun map f =
+    let
+      fun mf (elt,()) = f elt
+    in
+      fn Set m => KM.map mf m
+    end;
+
+fun domain m = Set (KM.transform (fn _ => ()) m);
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors.                                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val empty = Set (KM.new ());
+
+fun singleton elt = Set (KM.singleton (elt,()));
+
+(* ------------------------------------------------------------------------- *)
+(* Set size.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun null (Set m) = KM.null m;
+
+fun size (Set m) = KM.size m;
+
+(* ------------------------------------------------------------------------- *)
+(* Querying.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun peek (Set m) elt =
+    case KM.peekKey m elt of
+      SOME (elt,()) => SOME elt
+    | NONE => NONE;
+
+fun member elt (Set m) = KM.inDomain elt m;
+
+fun pick (Set m) =
+    let
+      val (elt,_) = KM.pick m
+    in
+      elt
+    end;
+
+fun nth (Set m) n =
+    let
+      val (elt,_) = KM.nth m n
+    in
+      elt
+    end;
+
+fun random (Set m) =
+    let
+      val (elt,_) = KM.random m
+    in
+      elt
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Adding.                                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+fun add (Set m) elt =
+    let
+      val m = KM.insert m (elt,())
+    in
+      Set m
+    end;
+
+local
+  fun uncurriedAdd (elt,set) = add set elt;
+in
+  fun addList set = List.foldl uncurriedAdd set;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun delete (Set m) elt =
+    let
+      val m = KM.delete m elt
+    in
+      Set m
+    end;
+
+fun remove (Set m) elt =
+    let
+      val m = KM.remove m elt
+    in
+      Set m
+    end;
+
+fun deletePick (Set m) =
+    let
+      val ((elt,()),m) = KM.deletePick m
+    in
+      (elt, Set m)
+    end;
+
+fun deleteNth (Set m) n =
+    let
+      val ((elt,()),m) = KM.deleteNth m n
+    in
+      (elt, Set m)
+    end;
+
+fun deleteRandom (Set m) =
+    let
+      val ((elt,()),m) = KM.deleteRandom m
+    in
+      (elt, Set m)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Joining.                                                                  *)
+(* ------------------------------------------------------------------------- *)
+
+fun union (Set m1) (Set m2) = Set (KM.unionDomain m1 m2);
+
+fun unionList sets =
+    let
+      val ms = List.map dest sets
+    in
+      Set (KM.unionListDomain ms)
+    end;
+
+fun intersect (Set m1) (Set m2) = Set (KM.intersectDomain m1 m2);
+
+fun intersectList sets =
+    let
+      val ms = List.map dest sets
+    in
+      Set (KM.intersectListDomain ms)
+    end;
+
+fun difference (Set m1) (Set m2) =
+    Set (KM.differenceDomain m1 m2);
+
+fun symmetricDifference (Set m1) (Set m2) =
+    Set (KM.symmetricDifferenceDomain m1 m2);
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+fun filter pred =
+    let
+      fun mpred (elt,()) = pred elt
+    in
+      fn Set m => Set (KM.filter mpred m)
+    end;
+
+fun partition pred =
+    let
+      fun mpred (elt,()) = pred elt
+    in
+      fn Set m =>
+         let
+           val (m1,m2) = KM.partition mpred m
+         in
+           (Set m1, Set m2)
+         end
+    end;
+
+fun app f =
+    let
+      fun mf (elt,()) = f elt
+    in
+      fn Set m => KM.app mf m
+    end;
+
+fun foldl f =
+    let
+      fun mf (elt,(),acc) = f (elt,acc)
+    in
+      fn acc => fn Set m => KM.foldl mf acc m
+    end;
+
+fun foldr f =
+    let
+      fun mf (elt,(),acc) = f (elt,acc)
+    in
+      fn acc => fn Set m => KM.foldr mf acc m
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+fun findl p =
+    let
+      fun mp (elt,()) = p elt
+    in
+      fn Set m =>
+         case KM.findl mp m of
+           SOME (elt,()) => SOME elt
+         | NONE => NONE
+    end;
+
+fun findr p =
+    let
+      fun mp (elt,()) = p elt
+    in
+      fn Set m =>
+         case KM.findr mp m of
+           SOME (elt,()) => SOME elt
+         | NONE => NONE
+    end;
+
+fun firstl f =
+    let
+      fun mf (elt,()) = f elt
+    in
+      fn Set m => KM.firstl mf m
+    end;
+
+fun firstr f =
+    let
+      fun mf (elt,()) = f elt
+    in
+      fn Set m => KM.firstr mf m
+    end;
+
+fun exists p =
+    let
+      fun mp (elt,()) = p elt
+    in
+      fn Set m => KM.exists mp m
+    end;
+
+fun all p =
+    let
+      fun mp (elt,()) = p elt
+    in
+      fn Set m => KM.all mp m
+    end;
+
+fun count p =
+    let
+      fun mp (elt,()) = p elt
+    in
+      fn Set m => KM.count mp m
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+fun compareValue ((),()) = EQUAL;
+
+fun equalValue () () = true;
+
+fun compare (Set m1, Set m2) = KM.compare compareValue (m1,m2);
+
+fun equal (Set m1) (Set m2) = KM.equal equalValue m1 m2;
+
+fun subset (Set m1) (Set m2) = KM.subsetDomain m1 m2;
+
+fun disjoint (Set m1) (Set m2) = KM.disjointDomain m1 m2;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun transform f =
+    let
+      fun inc (x,l) = f x :: l
+    in
+      foldr inc []
+    end;
+
+fun toList (Set m) = KM.keys m;
+
+fun fromList elts = addList empty elts;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun toString set =
+    "{" ^ (if null set then "" else Int.toString (size set)) ^ "}";
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over sets                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+type iterator = unit KM.iterator;
+
+fun mkIterator (Set m) = KM.mkIterator m;
+
+fun mkRevIterator (Set m) = KM.mkRevIterator m;
+
+fun readIterator iter =
+    let
+      val (elt,()) = KM.readIterator iter
+    in
+      elt
+    end;
+
+fun advanceIterator iter = KM.advanceIterator iter;
+
+end
+
+structure IntSet =
+ElementSet (IntMap);
+
+structure IntPairSet =
+ElementSet (IntPairMap);
+
+structure StringSet =
+ElementSet (StringMap);
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/FILES	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,40 @@
+Random.sig Random.sml
+Portable.sig PortablePolyml.sml
+Useful.sig Useful.sml
+Lazy.sig Lazy.sml
+Stream.sig Stream.sml
+Ordered.sig Ordered.sml
+Map.sig Map.sml
+KeyMap.sig KeyMap.sml
+Set.sig Set.sml
+ElementSet.sig ElementSet.sml
+Sharing.sig Sharing.sml
+Heap.sig Heap.sml
+Print.sig Print.sml
+Parse.sig Parse.sml
+Options.sig Options.sml
+Name.sig Name.sml
+NameArity.sig NameArity.sml
+Term.sig Term.sml
+Subst.sig Subst.sml
+Atom.sig Atom.sml
+Formula.sig Formula.sml
+Literal.sig Literal.sml
+Thm.sig Thm.sml
+Proof.sig Proof.sml
+Rule.sig Rule.sml
+Normalize.sig Normalize.sml
+Model.sig Model.sml
+Problem.sig Problem.sml
+TermNet.sig TermNet.sml
+AtomNet.sig AtomNet.sml
+LiteralNet.sig LiteralNet.sml
+Subsume.sig Subsume.sml
+KnuthBendixOrder.sig KnuthBendixOrder.sml
+Rewrite.sig Rewrite.sml
+Units.sig Units.sml
+Clause.sig Clause.sml
+Active.sig Active.sml
+Waiting.sig Waiting.sml
+Resolution.sig Resolution.sml
+Tptp.sig Tptp.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Formula.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,197 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC FORMULAS                                                *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Formula =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic formulas.                                     *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formula =
+    True
+  | False
+  | Atom of Atom.atom
+  | Not of formula
+  | And of formula * formula
+  | Or of formula * formula
+  | Imp of formula * formula
+  | Iff of formula * formula
+  | Forall of Term.var * formula
+  | Exists of Term.var * formula
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+(* Booleans *)
+
+val mkBoolean : bool -> formula
+
+val destBoolean : formula -> bool
+
+val isBoolean : formula -> bool
+
+val isTrue : formula -> bool
+
+val isFalse : formula -> bool
+
+(* Functions *)
+
+val functions : formula -> NameAritySet.set
+
+val functionNames : formula -> NameSet.set
+
+(* Relations *)
+
+val relations : formula -> NameAritySet.set
+
+val relationNames : formula -> NameSet.set
+
+(* Atoms *)
+
+val destAtom : formula -> Atom.atom
+
+val isAtom : formula -> bool
+
+(* Negations *)
+
+val destNeg : formula -> formula
+
+val isNeg : formula -> bool
+
+val stripNeg : formula -> int * formula
+
+(* Conjunctions *)
+
+val listMkConj : formula list -> formula
+
+val stripConj : formula -> formula list
+
+val flattenConj : formula -> formula list
+
+(* Disjunctions *)
+
+val listMkDisj : formula list -> formula
+
+val stripDisj : formula -> formula list
+
+val flattenDisj : formula -> formula list
+
+(* Equivalences *)
+
+val listMkEquiv : formula list -> formula
+
+val stripEquiv : formula -> formula list
+
+val flattenEquiv : formula -> formula list
+
+(* Universal quantification *)
+
+val destForall : formula -> Term.var * formula
+
+val isForall : formula -> bool
+
+val listMkForall : Term.var list * formula -> formula
+
+val setMkForall : NameSet.set * formula -> formula
+
+val stripForall : formula -> Term.var list * formula
+
+(* Existential quantification *)
+
+val destExists : formula -> Term.var * formula
+
+val isExists : formula -> bool
+
+val listMkExists : Term.var list * formula -> formula
+
+val setMkExists : NameSet.set * formula -> formula
+
+val stripExists : formula -> Term.var list * formula
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a formula in symbols.                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : formula -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for formulas.                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : formula * formula -> order
+
+val equal : formula -> formula -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Term.var -> formula -> bool
+
+val freeVars : formula -> NameSet.set
+
+val freeVarsList : formula list -> NameSet.set
+
+val specialize : formula -> formula
+
+val generalize : formula -> formula
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions.                                                            *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Subst.subst -> formula -> formula
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+val mkEq : Term.term * Term.term -> formula
+
+val destEq : formula -> Term.term * Term.term
+
+val isEq : formula -> bool
+
+val mkNeq : Term.term * Term.term -> formula
+
+val destNeq : formula -> Term.term * Term.term
+
+val isNeq : formula -> bool
+
+val mkRefl : Term.term -> formula
+
+val destRefl : formula -> Term.term
+
+val isRefl : formula -> bool
+
+val sym : formula -> formula  (* raises Error if given a refl *)
+
+val lhs : formula -> Term.term
+
+val rhs : formula -> Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Splitting goals.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val splitGoal : formula -> formula list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+type quotation = formula Parse.quotation
+
+val pp : formula Print.pp
+
+val toString : formula -> string
+
+val fromString : string -> formula
+
+val parse : quotation -> formula
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Formula.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,601 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC FORMULAS                                                *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Formula :> Formula =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic formulas.                                     *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formula =
+    True
+  | False
+  | Atom of Atom.atom
+  | Not of formula
+  | And of formula * formula
+  | Or of formula * formula
+  | Imp of formula * formula
+  | Iff of formula * formula
+  | Forall of Term.var * formula
+  | Exists of Term.var * formula;
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+(* Booleans *)
+
+fun mkBoolean true = True
+  | mkBoolean false = False;
+
+fun destBoolean True = true
+  | destBoolean False = false
+  | destBoolean _ = raise Error "destBoolean";
+
+val isBoolean = can destBoolean;
+
+fun isTrue fm =
+    case fm of
+      True => true
+    | _ => false;
+
+fun isFalse fm =
+    case fm of
+      False => true
+    | _ => false;
+
+(* Functions *)
+
+local
+  fun funcs fs [] = fs
+    | funcs fs (True :: fms) = funcs fs fms
+    | funcs fs (False :: fms) = funcs fs fms
+    | funcs fs (Atom atm :: fms) =
+      funcs (NameAritySet.union (Atom.functions atm) fs) fms
+    | funcs fs (Not p :: fms) = funcs fs (p :: fms)
+    | funcs fs (And (p,q) :: fms) = funcs fs (p :: q :: fms)
+    | funcs fs (Or (p,q) :: fms) = funcs fs (p :: q :: fms)
+    | funcs fs (Imp (p,q) :: fms) = funcs fs (p :: q :: fms)
+    | funcs fs (Iff (p,q) :: fms) = funcs fs (p :: q :: fms)
+    | funcs fs (Forall (_,p) :: fms) = funcs fs (p :: fms)
+    | funcs fs (Exists (_,p) :: fms) = funcs fs (p :: fms);
+in
+  fun functions fm = funcs NameAritySet.empty [fm];
+end;
+
+local
+  fun funcs fs [] = fs
+    | funcs fs (True :: fms) = funcs fs fms
+    | funcs fs (False :: fms) = funcs fs fms
+    | funcs fs (Atom atm :: fms) =
+      funcs (NameSet.union (Atom.functionNames atm) fs) fms
+    | funcs fs (Not p :: fms) = funcs fs (p :: fms)
+    | funcs fs (And (p,q) :: fms) = funcs fs (p :: q :: fms)
+    | funcs fs (Or (p,q) :: fms) = funcs fs (p :: q :: fms)
+    | funcs fs (Imp (p,q) :: fms) = funcs fs (p :: q :: fms)
+    | funcs fs (Iff (p,q) :: fms) = funcs fs (p :: q :: fms)
+    | funcs fs (Forall (_,p) :: fms) = funcs fs (p :: fms)
+    | funcs fs (Exists (_,p) :: fms) = funcs fs (p :: fms);
+in
+  fun functionNames fm = funcs NameSet.empty [fm];
+end;
+
+(* Relations *)
+
+local
+  fun rels fs [] = fs
+    | rels fs (True :: fms) = rels fs fms
+    | rels fs (False :: fms) = rels fs fms
+    | rels fs (Atom atm :: fms) =
+      rels (NameAritySet.add fs (Atom.relation atm)) fms
+    | rels fs (Not p :: fms) = rels fs (p :: fms)
+    | rels fs (And (p,q) :: fms) = rels fs (p :: q :: fms)
+    | rels fs (Or (p,q) :: fms) = rels fs (p :: q :: fms)
+    | rels fs (Imp (p,q) :: fms) = rels fs (p :: q :: fms)
+    | rels fs (Iff (p,q) :: fms) = rels fs (p :: q :: fms)
+    | rels fs (Forall (_,p) :: fms) = rels fs (p :: fms)
+    | rels fs (Exists (_,p) :: fms) = rels fs (p :: fms);
+in
+  fun relations fm = rels NameAritySet.empty [fm];
+end;
+
+local
+  fun rels fs [] = fs
+    | rels fs (True :: fms) = rels fs fms
+    | rels fs (False :: fms) = rels fs fms
+    | rels fs (Atom atm :: fms) = rels (NameSet.add fs (Atom.name atm)) fms
+    | rels fs (Not p :: fms) = rels fs (p :: fms)
+    | rels fs (And (p,q) :: fms) = rels fs (p :: q :: fms)
+    | rels fs (Or (p,q) :: fms) = rels fs (p :: q :: fms)
+    | rels fs (Imp (p,q) :: fms) = rels fs (p :: q :: fms)
+    | rels fs (Iff (p,q) :: fms) = rels fs (p :: q :: fms)
+    | rels fs (Forall (_,p) :: fms) = rels fs (p :: fms)
+    | rels fs (Exists (_,p) :: fms) = rels fs (p :: fms);
+in
+  fun relationNames fm = rels NameSet.empty [fm];
+end;
+
+(* Atoms *)
+
+fun destAtom (Atom atm) = atm
+  | destAtom _ = raise Error "Formula.destAtom";
+
+val isAtom = can destAtom;
+
+(* Negations *)
+
+fun destNeg (Not p) = p
+  | destNeg _ = raise Error "Formula.destNeg";
+
+val isNeg = can destNeg;
+
+val stripNeg =
+    let
+      fun strip n (Not fm) = strip (n + 1) fm
+        | strip n fm = (n,fm)
+    in
+      strip 0
+    end;
+
+(* Conjunctions *)
+
+fun listMkConj fms =
+    case rev fms of [] => True | fm :: fms => foldl And fm fms;
+
+local
+  fun strip cs (And (p,q)) = strip (p :: cs) q
+    | strip cs fm = rev (fm :: cs);
+in
+  fun stripConj True = []
+    | stripConj fm = strip [] fm;
+end;
+
+val flattenConj =
+    let
+      fun flat acc [] = acc
+        | flat acc (And (p,q) :: fms) = flat acc (q :: p :: fms)
+        | flat acc (True :: fms) = flat acc fms
+        | flat acc (fm :: fms) = flat (fm :: acc) fms
+    in
+      fn fm => flat [] [fm]
+    end;
+
+(* Disjunctions *)
+
+fun listMkDisj fms =
+    case rev fms of [] => False | fm :: fms => foldl Or fm fms;
+
+local
+  fun strip cs (Or (p,q)) = strip (p :: cs) q
+    | strip cs fm = rev (fm :: cs);
+in
+  fun stripDisj False = []
+    | stripDisj fm = strip [] fm;
+end;
+
+val flattenDisj =
+    let
+      fun flat acc [] = acc
+        | flat acc (Or (p,q) :: fms) = flat acc (q :: p :: fms)
+        | flat acc (False :: fms) = flat acc fms
+        | flat acc (fm :: fms) = flat (fm :: acc) fms
+    in
+      fn fm => flat [] [fm]
+    end;
+
+(* Equivalences *)
+
+fun listMkEquiv fms =
+    case rev fms of [] => True | fm :: fms => foldl Iff fm fms;
+
+local
+  fun strip cs (Iff (p,q)) = strip (p :: cs) q
+    | strip cs fm = rev (fm :: cs);
+in
+  fun stripEquiv True = []
+    | stripEquiv fm = strip [] fm;
+end;
+
+val flattenEquiv =
+    let
+      fun flat acc [] = acc
+        | flat acc (Iff (p,q) :: fms) = flat acc (q :: p :: fms)
+        | flat acc (True :: fms) = flat acc fms
+        | flat acc (fm :: fms) = flat (fm :: acc) fms
+    in
+      fn fm => flat [] [fm]
+    end;
+
+(* Universal quantifiers *)
+
+fun destForall (Forall v_f) = v_f
+  | destForall _ = raise Error "destForall";
+
+val isForall = can destForall;
+
+fun listMkForall ([],body) = body
+  | listMkForall (v :: vs, body) = Forall (v, listMkForall (vs,body));
+
+fun setMkForall (vs,body) = NameSet.foldr Forall body vs;
+
+local
+  fun strip vs (Forall (v,b)) = strip (v :: vs) b
+    | strip vs tm = (rev vs, tm);
+in
+  val stripForall = strip [];
+end;
+
+(* Existential quantifiers *)
+
+fun destExists (Exists v_f) = v_f
+  | destExists _ = raise Error "destExists";
+
+val isExists = can destExists;
+
+fun listMkExists ([],body) = body
+  | listMkExists (v :: vs, body) = Exists (v, listMkExists (vs,body));
+
+fun setMkExists (vs,body) = NameSet.foldr Exists body vs;
+
+local
+  fun strip vs (Exists (v,b)) = strip (v :: vs) b
+    | strip vs tm = (rev vs, tm);
+in
+  val stripExists = strip [];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a formula in symbols.                                         *)
+(* ------------------------------------------------------------------------- *)
+
+local
+  fun sz n [] = n
+    | sz n (True :: fms) = sz (n + 1) fms
+    | sz n (False :: fms) = sz (n + 1) fms
+    | sz n (Atom atm :: fms) = sz (n + Atom.symbols atm) fms
+    | sz n (Not p :: fms) = sz (n + 1) (p :: fms)
+    | sz n (And (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+    | sz n (Or (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+    | sz n (Imp (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+    | sz n (Iff (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+    | sz n (Forall (_,p) :: fms) = sz (n + 1) (p :: fms)
+    | sz n (Exists (_,p) :: fms) = sz (n + 1) (p :: fms);
+in
+  fun symbols fm = sz 0 [fm];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for formulas.                                 *)
+(* ------------------------------------------------------------------------- *)
+
+local
+  fun cmp [] = EQUAL
+    | cmp (f1_f2 :: fs) =
+      if Portable.pointerEqual f1_f2 then cmp fs
+      else
+        case f1_f2 of
+          (True,True) => cmp fs
+        | (True,_) => LESS
+        | (_,True) => GREATER
+        | (False,False) => cmp fs
+        | (False,_) => LESS
+        | (_,False) => GREATER
+        | (Atom atm1, Atom atm2) =>
+          (case Atom.compare (atm1,atm2) of
+             LESS => LESS
+           | EQUAL => cmp fs
+           | GREATER => GREATER)
+        | (Atom _, _) => LESS
+        | (_, Atom _) => GREATER
+        | (Not p1, Not p2) => cmp ((p1,p2) :: fs)
+        | (Not _, _) => LESS
+        | (_, Not _) => GREATER
+        | (And (p1,q1), And (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
+        | (And _, _) => LESS
+        | (_, And _) => GREATER
+        | (Or (p1,q1), Or (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
+        | (Or _, _) => LESS
+        | (_, Or _) => GREATER
+        | (Imp (p1,q1), Imp (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
+        | (Imp _, _) => LESS
+        | (_, Imp _) => GREATER
+        | (Iff (p1,q1), Iff (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
+        | (Iff _, _) => LESS
+        | (_, Iff _) => GREATER
+        | (Forall (v1,p1), Forall (v2,p2)) =>
+          (case Name.compare (v1,v2) of
+             LESS => LESS
+           | EQUAL => cmp ((p1,p2) :: fs)
+           | GREATER => GREATER)
+        | (Forall _, Exists _) => LESS
+        | (Exists _, Forall _) => GREATER
+        | (Exists (v1,p1), Exists (v2,p2)) =>
+          (case Name.compare (v1,v2) of
+             LESS => LESS
+           | EQUAL => cmp ((p1,p2) :: fs)
+           | GREATER => GREATER);
+in
+  fun compare fm1_fm2 = cmp [fm1_fm2];
+end;
+
+fun equal fm1 fm2 = compare (fm1,fm2) = EQUAL;
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+fun freeIn v =
+    let
+      fun f [] = false
+        | f (True :: fms) = f fms
+        | f (False :: fms) = f fms
+        | f (Atom atm :: fms) = Atom.freeIn v atm orelse f fms
+        | f (Not p :: fms) = f (p :: fms)
+        | f (And (p,q) :: fms) = f (p :: q :: fms)
+        | f (Or (p,q) :: fms) = f (p :: q :: fms)
+        | f (Imp (p,q) :: fms) = f (p :: q :: fms)
+        | f (Iff (p,q) :: fms) = f (p :: q :: fms)
+        | f (Forall (w,p) :: fms) =
+          if Name.equal v w then f fms else f (p :: fms)
+        | f (Exists (w,p) :: fms) =
+          if Name.equal v w then f fms else f (p :: fms)
+    in
+      fn fm => f [fm]
+    end;
+
+local
+  fun fv vs [] = vs
+    | fv vs ((_,True) :: fms) = fv vs fms
+    | fv vs ((_,False) :: fms) = fv vs fms
+    | fv vs ((bv, Atom atm) :: fms) =
+      fv (NameSet.union vs (NameSet.difference (Atom.freeVars atm) bv)) fms
+    | fv vs ((bv, Not p) :: fms) = fv vs ((bv,p) :: fms)
+    | fv vs ((bv, And (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+    | fv vs ((bv, Or (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+    | fv vs ((bv, Imp (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+    | fv vs ((bv, Iff (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+    | fv vs ((bv, Forall (v,p)) :: fms) = fv vs ((NameSet.add bv v, p) :: fms)
+    | fv vs ((bv, Exists (v,p)) :: fms) = fv vs ((NameSet.add bv v, p) :: fms);
+
+  fun add (fm,vs) = fv vs [(NameSet.empty,fm)];
+in
+  fun freeVars fm = add (fm,NameSet.empty);
+
+  fun freeVarsList fms = List.foldl add NameSet.empty fms;
+end;
+
+fun specialize fm = snd (stripForall fm);
+
+fun generalize fm = listMkForall (NameSet.toList (freeVars fm), fm);
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions.                                                            *)
+(* ------------------------------------------------------------------------- *)
+
+local
+  fun substCheck sub fm = if Subst.null sub then fm else substFm sub fm
+
+  and substFm sub fm =
+      case fm of
+        True => fm
+      | False => fm
+      | Atom (p,tms) =>
+        let
+          val tms' = Sharing.map (Subst.subst sub) tms
+        in
+          if Portable.pointerEqual (tms,tms') then fm else Atom (p,tms')
+        end
+      | Not p =>
+        let
+          val p' = substFm sub p
+        in
+          if Portable.pointerEqual (p,p') then fm else Not p'
+        end
+      | And (p,q) => substConn sub fm And p q
+      | Or (p,q) => substConn sub fm Or p q
+      | Imp (p,q) => substConn sub fm Imp p q
+      | Iff (p,q) => substConn sub fm Iff p q
+      | Forall (v,p) => substQuant sub fm Forall v p
+      | Exists (v,p) => substQuant sub fm Exists v p
+
+  and substConn sub fm conn p q =
+      let
+        val p' = substFm sub p
+        and q' = substFm sub q
+      in
+        if Portable.pointerEqual (p,p') andalso
+           Portable.pointerEqual (q,q')
+        then fm
+        else conn (p',q')
+      end
+
+  and substQuant sub fm quant v p =
+      let
+        val v' =
+            let
+              fun f (w,s) =
+                  if Name.equal w v then s
+                  else
+                    case Subst.peek sub w of
+                      NONE => NameSet.add s w
+                    | SOME tm => NameSet.union s (Term.freeVars tm)
+
+              val vars = freeVars p
+              val vars = NameSet.foldl f NameSet.empty vars
+            in
+              Term.variantPrime vars v
+            end
+
+        val sub =
+            if Name.equal v v' then Subst.remove sub (NameSet.singleton v)
+            else Subst.insert sub (v, Term.Var v')
+
+        val p' = substCheck sub p
+      in
+        if Name.equal v v' andalso Portable.pointerEqual (p,p') then fm
+        else quant (v',p')
+      end;
+in
+  val subst = substCheck;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkEq a_b = Atom (Atom.mkEq a_b);
+
+fun destEq fm = Atom.destEq (destAtom fm);
+
+val isEq = can destEq;
+
+fun mkNeq a_b = Not (mkEq a_b);
+
+fun destNeq (Not fm) = destEq fm
+  | destNeq _ = raise Error "Formula.destNeq";
+
+val isNeq = can destNeq;
+
+fun mkRefl tm = Atom (Atom.mkRefl tm);
+
+fun destRefl fm = Atom.destRefl (destAtom fm);
+
+val isRefl = can destRefl;
+
+fun sym fm = Atom (Atom.sym (destAtom fm));
+
+fun lhs fm = fst (destEq fm);
+
+fun rhs fm = snd (destEq fm);
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+type quotation = formula Parse.quotation;
+
+val truthName = Name.fromString "T"
+and falsityName = Name.fromString "F"
+and conjunctionName = Name.fromString "/\\"
+and disjunctionName = Name.fromString "\\/"
+and implicationName = Name.fromString "==>"
+and equivalenceName = Name.fromString "<=>"
+and universalName = Name.fromString "!"
+and existentialName = Name.fromString "?";
+
+local
+  fun demote True = Term.Fn (truthName,[])
+    | demote False = Term.Fn (falsityName,[])
+    | demote (Atom (p,tms)) = Term.Fn (p,tms)
+    | demote (Not p) =
+      let
+        val ref s = Term.negation
+      in
+        Term.Fn (Name.fromString s, [demote p])
+      end
+    | demote (And (p,q)) = Term.Fn (conjunctionName, [demote p, demote q])
+    | demote (Or (p,q)) = Term.Fn (disjunctionName, [demote p, demote q])
+    | demote (Imp (p,q)) = Term.Fn (implicationName, [demote p, demote q])
+    | demote (Iff (p,q)) = Term.Fn (equivalenceName, [demote p, demote q])
+    | demote (Forall (v,b)) = Term.Fn (universalName, [Term.Var v, demote b])
+    | demote (Exists (v,b)) =
+      Term.Fn (existentialName, [Term.Var v, demote b]);
+in
+  fun pp fm = Term.pp (demote fm);
+end;
+
+val toString = Print.toString pp;
+
+local
+  fun isQuant [Term.Var _, _] = true
+    | isQuant _ = false;
+
+  fun promote (Term.Var v) = Atom (v,[])
+    | promote (Term.Fn (f,tms)) =
+      if Name.equal f truthName andalso null tms then
+        True
+      else if Name.equal f falsityName andalso null tms then
+        False
+      else if Name.toString f = !Term.negation andalso length tms = 1 then
+        Not (promote (hd tms))
+      else if Name.equal f conjunctionName andalso length tms = 2 then
+        And (promote (hd tms), promote (List.nth (tms,1)))
+      else if Name.equal f disjunctionName andalso length tms = 2 then
+        Or (promote (hd tms), promote (List.nth (tms,1)))
+      else if Name.equal f implicationName andalso length tms = 2 then
+        Imp (promote (hd tms), promote (List.nth (tms,1)))
+      else if Name.equal f equivalenceName andalso length tms = 2 then
+        Iff (promote (hd tms), promote (List.nth (tms,1)))
+      else if Name.equal f universalName andalso isQuant tms then
+        Forall (Term.destVar (hd tms), promote (List.nth (tms,1)))
+      else if Name.equal f existentialName andalso isQuant tms then
+        Exists (Term.destVar (hd tms), promote (List.nth (tms,1)))
+      else
+        Atom (f,tms);
+in
+  fun fromString s = promote (Term.fromString s);
+end;
+
+val parse = Parse.parseQuotation toString fromString;
+
+(* ------------------------------------------------------------------------- *)
+(* Splitting goals.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+local
+  fun add_asms asms goal =
+      if null asms then goal else Imp (listMkConj (rev asms), goal);
+
+  fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
+
+  fun split asms pol fm =
+      case (pol,fm) of
+        (* Positive splittables *)
+        (true,True) => []
+      | (true, Not f) => split asms false f
+      | (true, And (f1,f2)) => split asms true f1 @ split (f1 :: asms) true f2
+      | (true, Or (f1,f2)) => split (Not f1 :: asms) true f2
+      | (true, Imp (f1,f2)) => split (f1 :: asms) true f2
+      | (true, Iff (f1,f2)) =>
+        split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
+      | (true, Forall (v,f)) => map (add_var_asms asms v) (split [] true f)
+        (* Negative splittables *)
+      | (false,False) => []
+      | (false, Not f) => split asms true f
+      | (false, And (f1,f2)) => split (f1 :: asms) false f2
+      | (false, Or (f1,f2)) =>
+        split asms false f1 @ split (Not f1 :: asms) false f2
+      | (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
+      | (false, Iff (f1,f2)) =>
+        split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
+      | (false, Exists (v,f)) => map (add_var_asms asms v) (split [] false f)
+        (* Unsplittables *)
+      | _ => [add_asms asms (if pol then fm else Not fm)];
+in
+  fun splitGoal fm = split [] true fm;
+end;
+
+(*MetisTrace3
+val splitGoal = fn fm =>
+    let
+      val result = splitGoal fm
+      val () = Print.trace pp "Formula.splitGoal: fm" fm
+      val () = Print.trace (Print.ppList pp) "Formula.splitGoal: result" result
+    in
+      result
+    end;
+*)
+
+end
+
+structure FormulaOrdered =
+struct type t = Formula.formula val compare = Formula.compare end
+
+structure FormulaMap = KeyMap (FormulaOrdered);
+
+structure FormulaSet = ElementSet (FormulaMap);
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Heap.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,31 @@
+(* ========================================================================= *)
+(* A HEAP DATATYPE FOR ML                                                    *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Heap =
+sig
+
+type 'a heap
+
+val new : ('a * 'a -> order) -> 'a heap
+
+val add : 'a heap -> 'a -> 'a heap
+
+val null : 'a heap -> bool
+
+val top : 'a heap -> 'a  (* raises Empty *)
+
+val remove : 'a heap -> 'a * 'a heap  (* raises Empty *)
+
+val size : 'a heap -> int
+
+val app : ('a -> unit) -> 'a heap -> unit
+
+val toList : 'a heap -> 'a list
+
+val toStream : 'a heap -> 'a Stream.stream
+
+val toString : 'a heap -> string
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Heap.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,77 @@
+(* ========================================================================= *)
+(* A HEAP DATATYPE FOR ML                                                    *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Heap :> Heap =
+struct
+
+(* Leftist heaps as in Purely Functional Data Structures, by Chris Okasaki *)
+
+datatype 'a node = E | T of int * 'a * 'a node * 'a node;
+
+datatype 'a heap = Heap of ('a * 'a -> order) * int * 'a node;
+
+fun rank E = 0
+  | rank (T (r,_,_,_)) = r;
+
+fun makeT (x,a,b) =
+  if rank a >= rank b then T (rank b + 1, x, a, b) else T (rank a + 1, x, b, a);
+
+fun merge cmp =
+    let
+      fun mrg (h,E) = h
+        | mrg (E,h) = h
+        | mrg (h1 as T (_,x,a1,b1), h2 as T (_,y,a2,b2)) =
+          case cmp (x,y) of
+            GREATER => makeT (y, a2, mrg (h1,b2))
+          | _ => makeT (x, a1, mrg (b1,h2))
+    in
+      mrg
+    end;
+
+fun new cmp = Heap (cmp,0,E);
+
+fun add (Heap (f,n,a)) x = Heap (f, n + 1, merge f (T (1,x,E,E), a));
+
+fun size (Heap (_, n, _)) = n;
+
+fun null h = size h = 0;
+
+fun top (Heap (_,_,E)) = raise Empty
+  | top (Heap (_, _, T (_,x,_,_))) = x;
+
+fun remove (Heap (_,_,E)) = raise Empty
+  | remove (Heap (f, n, T (_,x,a,b))) = (x, Heap (f, n - 1, merge f (a,b)));
+
+fun app f =
+    let
+      fun ap [] = ()
+        | ap (E :: rest) = ap rest
+        | ap (T (_,d,a,b) :: rest) = (f d; ap (a :: b :: rest))
+    in
+      fn Heap (_,_,a) => ap [a]
+    end;
+
+fun toList h =
+    if null h then []
+    else
+      let
+        val (x,h) = remove h
+      in
+        x :: toList h
+      end;
+
+fun toStream h =
+    if null h then Stream.Nil
+    else
+      let
+        val (x,h) = remove h
+      in
+        Stream.Cons (x, fn () => toStream h)
+      end;
+
+fun toString h =
+    "Heap[" ^ (if null h then "" else Int.toString (size h)) ^ "]";
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/KeyMap.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,196 @@
+(* ========================================================================= *)
+(* FINITE MAPS WITH A FIXED KEY TYPE                                         *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+signature KeyMap =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of map keys.                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+type key
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite maps.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors.                                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val new : unit -> 'a map
+
+val singleton : key * 'a -> 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Map size.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val null : 'a map -> bool
+
+val size : 'a map -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Querying.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val peekKey : 'a map -> key -> (key * 'a) option
+
+val peek : 'a map -> key -> 'a option
+
+val get : 'a map -> key -> 'a  (* raises Error *)
+
+val pick : 'a map -> key * 'a  (* an arbitrary key/value pair *)
+
+val nth : 'a map -> int -> key * 'a  (* in the range [0,size-1] *)
+
+val random : 'a map -> key * 'a
+
+(* ------------------------------------------------------------------------- *)
+(* Adding.                                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+val insert : 'a map -> key * 'a -> 'a map
+
+val insertList : 'a map -> (key * 'a) list -> 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Removing.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val delete : 'a map -> key -> 'a map  (* must be present *)
+
+val remove : 'a map -> key -> 'a map
+
+val deletePick : 'a map -> (key * 'a) * 'a map
+
+val deleteNth : 'a map -> int -> (key * 'a) * 'a map
+
+val deleteRandom : 'a map -> (key * 'a) * 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Joining (all join operations prefer keys in the second map).              *)
+(* ------------------------------------------------------------------------- *)
+
+val merge :
+    {first : key * 'a -> 'c option,
+     second : key * 'b -> 'c option,
+     both : (key * 'a) * (key * 'b) -> 'c option} ->
+    'a map -> 'b map -> 'c map
+
+val union :
+    ((key * 'a) * (key * 'a) -> 'a option) ->
+    'a map -> 'a map -> 'a map
+
+val intersect :
+    ((key * 'a) * (key * 'b) -> 'c option) ->
+    'a map -> 'b map -> 'c map
+
+(* ------------------------------------------------------------------------- *)
+(* Set operations on the domain.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val inDomain : key -> 'a map -> bool
+
+val unionDomain : 'a map -> 'a map -> 'a map
+
+val unionListDomain : 'a map list -> 'a map
+
+val intersectDomain : 'a map -> 'a map -> 'a map
+
+val intersectListDomain : 'a map list -> 'a map
+
+val differenceDomain : 'a map -> 'a map -> 'a map
+
+val symmetricDifferenceDomain : 'a map -> 'a map -> 'a map
+
+val equalDomain : 'a map -> 'a map -> bool
+
+val subsetDomain : 'a map -> 'a map -> bool
+
+val disjointDomain : 'a map -> 'a map -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+val mapPartial : (key * 'a -> 'b option) -> 'a map -> 'b map
+
+val map : (key * 'a -> 'b) -> 'a map -> 'b map
+
+val app : (key * 'a -> unit) -> 'a map -> unit
+
+val transform : ('a -> 'b) -> 'a map -> 'b map
+
+val filter : (key * 'a -> bool) -> 'a map -> 'a map
+
+val partition :
+    (key * 'a -> bool) -> 'a map -> 'a map * 'a map
+
+val foldl : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
+
+val foldr : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
+
+(* ------------------------------------------------------------------------- *)
+(* Searching.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val findl : (key * 'a -> bool) -> 'a map -> (key * 'a) option
+
+val findr : (key * 'a -> bool) -> 'a map -> (key * 'a) option
+
+val firstl : (key * 'a -> 'b option) -> 'a map -> 'b option
+
+val firstr : (key * 'a -> 'b option) -> 'a map -> 'b option
+
+val exists : (key * 'a -> bool) -> 'a map -> bool
+
+val all : (key * 'a -> bool) -> 'a map -> bool
+
+val count : (key * 'a -> bool) -> 'a map -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : ('a * 'a -> order) -> 'a map * 'a map -> order
+
+val equal : ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val keys : 'a map -> key list
+
+val values : 'a map -> 'a list
+
+val toList : 'a map -> (key * 'a) list
+
+val fromList : (key * 'a) list -> 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val toString : 'a map -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over maps.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a iterator
+
+val mkIterator : 'a map -> 'a iterator option
+
+val mkRevIterator : 'a map -> 'a iterator option
+
+val readIterator : 'a iterator -> key * 'a
+
+val advanceIterator : 'a iterator -> 'a iterator option
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/KeyMap.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,1442 @@
+(* ========================================================================= *)
+(* FINITE MAPS WITH A FIXED KEY TYPE                                         *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* Importing from the input signature.                                       *)
+(* ------------------------------------------------------------------------- *)
+
+type key = Key.t;
+
+val compareKey = Key.compare;
+
+(* ------------------------------------------------------------------------- *)
+(* Importing useful functionality.                                           *)
+(* ------------------------------------------------------------------------- *)
+
+exception Bug = Useful.Bug;
+
+exception Error = Useful.Error;
+
+val pointerEqual = Portable.pointerEqual;
+
+val K = Useful.K;
+
+val randomInt = Portable.randomInt;
+
+val randomWord = Portable.randomWord;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting a comparison function to an equality function.                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun equalKey key1 key2 = compareKey (key1,key2) = EQUAL;
+
+(* ------------------------------------------------------------------------- *)
+(* Priorities.                                                               *)
+(* ------------------------------------------------------------------------- *)
+
+type priority = Word.word;
+
+val randomPriority = randomWord;
+
+val comparePriority = Word.compare;
+
+(* ------------------------------------------------------------------------- *)
+(* Priority search trees.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+datatype 'value tree =
+    E
+  | T of 'value node
+
+and 'value node =
+    Node of
+      {size : int,
+       priority : priority,
+       left : 'value tree,
+       key : key,
+       value : 'value,
+       right : 'value tree};
+
+fun lowerPriorityNode node1 node2 =
+    let
+      val Node {priority = p1, ...} = node1
+      and Node {priority = p2, ...} = node2
+    in
+      comparePriority (p1,p2) = LESS
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Tree debugging functions.                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+local
+  fun checkSizes tree =
+      case tree of
+        E => 0
+      | T (Node {size,left,right,...}) =>
+        let
+          val l = checkSizes left
+          and r = checkSizes right
+
+          val () = if l + 1 + r = size then () else raise Bug "wrong size"
+        in
+          size
+        end;
+
+  fun checkSorted x tree =
+      case tree of
+        E => x
+      | T (Node {left,key,right,...}) =>
+        let
+          val x = checkSorted x left
+
+          val () =
+              case x of
+                NONE => ()
+              | SOME k =>
+                case compareKey (k,key) of
+                  LESS => ()
+                | EQUAL => raise Bug "duplicate keys"
+                | GREATER => raise Bug "unsorted"
+
+          val x = SOME key
+        in
+          checkSorted x right
+        end;
+
+  fun checkPriorities tree =
+      case tree of
+        E => NONE
+      | T node =>
+        let
+          val Node {left,right,...} = node
+
+          val () =
+              case checkPriorities left of
+                NONE => ()
+              | SOME lnode =>
+                if not (lowerPriorityNode node lnode) then ()
+                else raise Bug "left child has greater priority"
+
+          val () =
+              case checkPriorities right of
+                NONE => ()
+              | SOME rnode =>
+                if not (lowerPriorityNode node rnode) then ()
+                else raise Bug "right child has greater priority"
+        in
+          SOME node
+        end;
+in
+  fun treeCheckInvariants tree =
+      let
+        val _ = checkSizes tree
+
+        val _ = checkSorted NONE tree
+
+        val _ = checkPriorities tree
+      in
+        tree
+      end
+      handle Error err => raise Bug err;
+end;
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Tree operations.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeNew () = E;
+
+fun nodeSize (Node {size = x, ...}) = x;
+
+fun treeSize tree =
+    case tree of
+      E => 0
+    | T x => nodeSize x;
+
+fun mkNode priority left key value right =
+    let
+      val size = treeSize left + 1 + treeSize right
+    in
+      Node
+        {size = size,
+         priority = priority,
+         left = left,
+         key = key,
+         value = value,
+         right = right}
+    end;
+
+fun mkTree priority left key value right =
+    let
+      val node = mkNode priority left key value right
+    in
+      T node
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Extracting the left and right spines of a tree.                           *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeLeftSpine acc tree =
+    case tree of
+      E => acc
+    | T node => nodeLeftSpine acc node
+
+and nodeLeftSpine acc node =
+    let
+      val Node {left,...} = node
+    in
+      treeLeftSpine (node :: acc) left
+    end;
+
+fun treeRightSpine acc tree =
+    case tree of
+      E => acc
+    | T node => nodeRightSpine acc node
+
+and nodeRightSpine acc node =
+    let
+      val Node {right,...} = node
+    in
+      treeRightSpine (node :: acc) right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Singleton trees.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkNodeSingleton priority key value =
+    let
+      val size = 1
+      and left = E
+      and right = E
+    in
+      Node
+        {size = size,
+         priority = priority,
+         left = left,
+         key = key,
+         value = value,
+         right = right}
+    end;
+
+fun nodeSingleton (key,value) =
+    let
+      val priority = randomPriority ()
+    in
+      mkNodeSingleton priority key value
+    end;
+
+fun treeSingleton key_value =
+    let
+      val node = nodeSingleton key_value
+    in
+      T node
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Appending two trees, where every element of the first tree is less than   *)
+(* every element of the second tree.                                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeAppend tree1 tree2 =
+    case tree1 of
+      E => tree2
+    | T node1 =>
+      case tree2 of
+        E => tree1
+      | T node2 =>
+        if lowerPriorityNode node1 node2 then
+          let
+            val Node {priority,left,key,value,right,...} = node2
+
+            val left = treeAppend tree1 left
+          in
+            mkTree priority left key value right
+          end
+        else
+          let
+            val Node {priority,left,key,value,right,...} = node1
+
+            val right = treeAppend right tree2
+          in
+            mkTree priority left key value right
+          end;
+
+(* ------------------------------------------------------------------------- *)
+(* Appending two trees and a node, where every element of the first tree is  *)
+(* less than the node, which in turn is less than every element of the       *)
+(* second tree.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeCombine left node right =
+    let
+      val left_node = treeAppend left (T node)
+    in
+      treeAppend left_node right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching a tree for a value.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun treePeek pkey tree =
+    case tree of
+      E => NONE
+    | T node => nodePeek pkey node
+
+and nodePeek pkey node =
+    let
+      val Node {left,key,value,right,...} = node
+    in
+      case compareKey (pkey,key) of
+        LESS => treePeek pkey left
+      | EQUAL => SOME value
+      | GREATER => treePeek pkey right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Tree paths.                                                               *)
+(* ------------------------------------------------------------------------- *)
+
+(* Generating a path by searching a tree for a key/value pair *)
+
+fun treePeekPath pkey path tree =
+    case tree of
+      E => (path,NONE)
+    | T node => nodePeekPath pkey path node
+
+and nodePeekPath pkey path node =
+    let
+      val Node {left,key,right,...} = node
+    in
+      case compareKey (pkey,key) of
+        LESS => treePeekPath pkey ((true,node) :: path) left
+      | EQUAL => (path, SOME node)
+      | GREATER => treePeekPath pkey ((false,node) :: path) right
+    end;
+
+(* A path splits a tree into left/right components *)
+
+fun addSidePath ((wentLeft,node),(leftTree,rightTree)) =
+    let
+      val Node {priority,left,key,value,right,...} = node
+    in
+      if wentLeft then (leftTree, mkTree priority rightTree key value right)
+      else (mkTree priority left key value leftTree, rightTree)
+    end;
+
+fun addSidesPath left_right = List.foldl addSidePath left_right;
+
+fun mkSidesPath path = addSidesPath (E,E) path;
+
+(* Updating the subtree at a path *)
+
+local
+  fun updateTree ((wentLeft,node),tree) =
+      let
+        val Node {priority,left,key,value,right,...} = node
+      in
+        if wentLeft then mkTree priority tree key value right
+        else mkTree priority left key value tree
+      end;
+in
+  fun updateTreePath tree = List.foldl updateTree tree;
+end;
+
+(* Inserting a new node at a path position *)
+
+fun insertNodePath node =
+    let
+      fun insert left_right path =
+          case path of
+            [] =>
+            let
+              val (left,right) = left_right
+            in
+              treeCombine left node right
+            end
+          | (step as (_,snode)) :: rest =>
+            if lowerPriorityNode snode node then
+              let
+                val left_right = addSidePath (step,left_right)
+              in
+                insert left_right rest
+              end
+            else
+              let
+                val (left,right) = left_right
+
+                val tree = treeCombine left node right
+              in
+                updateTreePath tree path
+              end
+    in
+      insert (E,E)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Using a key to split a node into three components: the keys comparing     *)
+(* less than the supplied key, an optional equal key, and the keys comparing *)
+(* greater.                                                                  *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodePartition pkey node =
+    let
+      val (path,pnode) = nodePeekPath pkey [] node
+    in
+      case pnode of
+        NONE =>
+        let
+          val (left,right) = mkSidesPath path
+        in
+          (left,NONE,right)
+        end
+      | SOME node =>
+        let
+          val Node {left,key,value,right,...} = node
+
+          val (left,right) = addSidesPath (left,right) path
+        in
+          (left, SOME (key,value), right)
+        end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching a tree for a key/value pair.                                    *)
+(* ------------------------------------------------------------------------- *)
+
+fun treePeekKey pkey tree =
+    case tree of
+      E => NONE
+    | T node => nodePeekKey pkey node
+
+and nodePeekKey pkey node =
+    let
+      val Node {left,key,value,right,...} = node
+    in
+      case compareKey (pkey,key) of
+        LESS => treePeekKey pkey left
+      | EQUAL => SOME (key,value)
+      | GREATER => treePeekKey pkey right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Inserting new key/values into the tree.                                   *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeInsert key_value tree =
+    let
+      val (key,value) = key_value
+
+      val (path,inode) = treePeekPath key [] tree
+    in
+      case inode of
+        NONE =>
+        let
+          val node = nodeSingleton (key,value)
+        in
+          insertNodePath node path
+        end
+      | SOME node =>
+        let
+          val Node {size,priority,left,right,...} = node
+
+          val node =
+              Node
+                {size = size,
+                 priority = priority,
+                 left = left,
+                 key = key,
+                 value = value,
+                 right = right}
+        in
+          updateTreePath (T node) path
+        end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Deleting key/value pairs: it raises an exception if the supplied key is   *)
+(* not present.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDelete dkey tree =
+    case tree of
+      E => raise Bug "KeyMap.delete: element not found"
+    | T node => nodeDelete dkey node
+
+and nodeDelete dkey node =
+    let
+      val Node {size,priority,left,key,value,right} = node
+    in
+      case compareKey (dkey,key) of
+        LESS =>
+        let
+          val size = size - 1
+          and left = treeDelete dkey left
+
+          val node =
+              Node
+                {size = size,
+                 priority = priority,
+                 left = left,
+                 key = key,
+                 value = value,
+                 right = right}
+        in
+          T node
+        end
+      | EQUAL => treeAppend left right
+      | GREATER =>
+        let
+          val size = size - 1
+          and right = treeDelete dkey right
+
+          val node =
+              Node
+                {size = size,
+                 priority = priority,
+                 left = left,
+                 key = key,
+                 value = value,
+                 right = right}
+        in
+          T node
+        end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Partial map is the basic operation for preserving tree structure.         *)
+(* It applies its argument function to the elements *in order*.              *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMapPartial f tree =
+    case tree of
+      E => E
+    | T node => nodeMapPartial f node
+
+and nodeMapPartial f (Node {priority,left,key,value,right,...}) =
+    let
+      val left = treeMapPartial f left
+      and vo = f (key,value)
+      and right = treeMapPartial f right
+    in
+      case vo of
+        NONE => treeAppend left right
+      | SOME value => mkTree priority left key value right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping tree values.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMap f tree =
+    case tree of
+      E => E
+    | T node => T (nodeMap f node)
+
+and nodeMap f node =
+    let
+      val Node {size,priority,left,key,value,right} = node
+
+      val left = treeMap f left
+      and value = f (key,value)
+      and right = treeMap f right
+    in
+      Node
+        {size = size,
+         priority = priority,
+         left = left,
+         key = key,
+         value = value,
+         right = right}
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Merge is the basic operation for joining two trees. Note that the merged  *)
+(* key is always the one from the second map.                                *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMerge f1 f2 fb tree1 tree2 =
+    case tree1 of
+      E => treeMapPartial f2 tree2
+    | T node1 =>
+      case tree2 of
+        E => treeMapPartial f1 tree1
+      | T node2 => nodeMerge f1 f2 fb node1 node2
+
+and nodeMerge f1 f2 fb node1 node2 =
+    let
+      val Node {priority,left,key,value,right,...} = node2
+
+      val (l,kvo,r) = nodePartition key node1
+
+      val left = treeMerge f1 f2 fb l left
+      and right = treeMerge f1 f2 fb r right
+
+      val vo =
+          case kvo of
+            NONE => f2 (key,value)
+          | SOME kv => fb (kv,(key,value))
+    in
+      case vo of
+        NONE => treeAppend left right
+      | SOME value =>
+        let
+          val node = mkNodeSingleton priority key value
+        in
+          treeCombine left node right
+        end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* A union operation on trees.                                               *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeUnion f f2 tree1 tree2 =
+    case tree1 of
+      E => tree2
+    | T node1 =>
+      case tree2 of
+        E => tree1
+      | T node2 => nodeUnion f f2 node1 node2
+
+and nodeUnion f f2 node1 node2 =
+    if pointerEqual (node1,node2) then nodeMapPartial f2 node1
+    else
+      let
+        val Node {priority,left,key,value,right,...} = node2
+
+        val (l,kvo,r) = nodePartition key node1
+
+        val left = treeUnion f f2 l left
+        and right = treeUnion f f2 r right
+
+        val vo =
+            case kvo of
+              NONE => SOME value
+            | SOME kv => f (kv,(key,value))
+      in
+        case vo of
+          NONE => treeAppend left right
+        | SOME value =>
+          let
+            val node = mkNodeSingleton priority key value
+          in
+            treeCombine left node right
+          end
+      end;
+
+(* ------------------------------------------------------------------------- *)
+(* An intersect operation on trees.                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeIntersect f t1 t2 =
+    case t1 of
+      E => E
+    | T n1 =>
+      case t2 of
+        E => E
+      | T n2 => nodeIntersect f n1 n2
+
+and nodeIntersect f n1 n2 =
+    let
+      val Node {priority,left,key,value,right,...} = n2
+
+      val (l,kvo,r) = nodePartition key n1
+
+      val left = treeIntersect f l left
+      and right = treeIntersect f r right
+
+      val vo =
+          case kvo of
+            NONE => NONE
+          | SOME kv => f (kv,(key,value))
+    in
+      case vo of
+        NONE => treeAppend left right
+      | SOME value => mkTree priority left key value right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* A union operation on trees which simply chooses the second value.         *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeUnionDomain tree1 tree2 =
+    case tree1 of
+      E => tree2
+    | T node1 =>
+      case tree2 of
+        E => tree1
+      | T node2 =>
+        if pointerEqual (node1,node2) then tree2
+        else nodeUnionDomain node1 node2
+
+and nodeUnionDomain node1 node2 =
+    let
+      val Node {priority,left,key,value,right,...} = node2
+
+      val (l,_,r) = nodePartition key node1
+
+      val left = treeUnionDomain l left
+      and right = treeUnionDomain r right
+
+      val node = mkNodeSingleton priority key value
+    in
+      treeCombine left node right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* An intersect operation on trees which simply chooses the second value.    *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeIntersectDomain tree1 tree2 =
+    case tree1 of
+      E => E
+    | T node1 =>
+      case tree2 of
+        E => E
+      | T node2 =>
+        if pointerEqual (node1,node2) then tree2
+        else nodeIntersectDomain node1 node2
+
+and nodeIntersectDomain node1 node2 =
+    let
+      val Node {priority,left,key,value,right,...} = node2
+
+      val (l,kvo,r) = nodePartition key node1
+
+      val left = treeIntersectDomain l left
+      and right = treeIntersectDomain r right
+    in
+      if Option.isSome kvo then mkTree priority left key value right
+      else treeAppend left right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* A difference operation on trees.                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDifferenceDomain t1 t2 =
+    case t1 of
+      E => E
+    | T n1 =>
+      case t2 of
+        E => t1
+      | T n2 => nodeDifferenceDomain n1 n2
+
+and nodeDifferenceDomain n1 n2 =
+    if pointerEqual (n1,n2) then E
+    else
+      let
+        val Node {priority,left,key,value,right,...} = n1
+
+        val (l,kvo,r) = nodePartition key n2
+
+        val left = treeDifferenceDomain left l
+        and right = treeDifferenceDomain right r
+      in
+        if Option.isSome kvo then treeAppend left right
+        else mkTree priority left key value right
+      end;
+
+(* ------------------------------------------------------------------------- *)
+(* A subset operation on trees.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeSubsetDomain tree1 tree2 =
+    case tree1 of
+      E => true
+    | T node1 =>
+      case tree2 of
+        E => false
+      | T node2 => nodeSubsetDomain node1 node2
+
+and nodeSubsetDomain node1 node2 =
+    pointerEqual (node1,node2) orelse
+    let
+      val Node {size,left,key,right,...} = node1
+    in
+      size <= nodeSize node2 andalso
+      let
+        val (l,kvo,r) = nodePartition key node2
+      in
+        Option.isSome kvo andalso
+        treeSubsetDomain left l andalso
+        treeSubsetDomain right r
+      end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Picking an arbitrary key/value pair from a tree.                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodePick node =
+    let
+      val Node {key,value,...} = node
+    in
+      (key,value)
+    end;
+
+fun treePick tree =
+    case tree of
+      E => raise Bug "KeyMap.treePick"
+    | T node => nodePick node;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing an arbitrary key/value pair from a tree.                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodeDeletePick node =
+    let
+      val Node {left,key,value,right,...} = node
+    in
+      ((key,value), treeAppend left right)
+    end;
+
+fun treeDeletePick tree =
+    case tree of
+      E => raise Bug "KeyMap.treeDeletePick"
+    | T node => nodeDeletePick node;
+
+(* ------------------------------------------------------------------------- *)
+(* Finding the nth smallest key/value (counting from 0).                     *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeNth n tree =
+    case tree of
+      E => raise Bug "KeyMap.treeNth"
+    | T node => nodeNth n node
+
+and nodeNth n node =
+    let
+      val Node {left,key,value,right,...} = node
+
+      val k = treeSize left
+    in
+      if n = k then (key,value)
+      else if n < k then treeNth n left
+      else treeNth (n - (k + 1)) right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing the nth smallest key/value (counting from 0).                    *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDeleteNth n tree =
+    case tree of
+      E => raise Bug "KeyMap.treeDeleteNth"
+    | T node => nodeDeleteNth n node
+
+and nodeDeleteNth n node =
+    let
+      val Node {size,priority,left,key,value,right} = node
+
+      val k = treeSize left
+    in
+      if n = k then ((key,value), treeAppend left right)
+      else if n < k then
+        let
+          val (key_value,left) = treeDeleteNth n left
+
+          val size = size - 1
+
+          val node =
+              Node
+                {size = size,
+                 priority = priority,
+                 left = left,
+                 key = key,
+                 value = value,
+                 right = right}
+        in
+          (key_value, T node)
+        end
+      else
+        let
+          val n = n - (k + 1)
+
+          val (key_value,right) = treeDeleteNth n right
+
+          val size = size - 1
+
+          val node =
+              Node
+                {size = size,
+                 priority = priority,
+                 left = left,
+                 key = key,
+                 value = value,
+                 right = right}
+        in
+          (key_value, T node)
+        end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+datatype 'value iterator =
+    LR of (key * 'value) * 'value tree * 'value node list
+  | RL of (key * 'value) * 'value tree * 'value node list;
+
+fun fromSpineLR nodes =
+    case nodes of
+      [] => NONE
+    | Node {key,value,right,...} :: nodes =>
+      SOME (LR ((key,value),right,nodes));
+
+fun fromSpineRL nodes =
+    case nodes of
+      [] => NONE
+    | Node {key,value,left,...} :: nodes =>
+      SOME (RL ((key,value),left,nodes));
+
+fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
+
+fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
+
+fun treeMkIterator tree = addLR [] tree;
+
+fun treeMkRevIterator tree = addRL [] tree;
+
+fun readIterator iter =
+    case iter of
+      LR (key_value,_,_) => key_value
+    | RL (key_value,_,_) => key_value;
+
+fun advanceIterator iter =
+    case iter of
+      LR (_,tree,nodes) => addLR nodes tree
+    | RL (_,tree,nodes) => addRL nodes tree;
+
+fun foldIterator f acc io =
+    case io of
+      NONE => acc
+    | SOME iter =>
+      let
+        val (key,value) = readIterator iter
+      in
+        foldIterator f (f (key,value,acc)) (advanceIterator iter)
+      end;
+
+fun findIterator pred io =
+    case io of
+      NONE => NONE
+    | SOME iter =>
+      let
+        val key_value = readIterator iter
+      in
+        if pred key_value then SOME key_value
+        else findIterator pred (advanceIterator iter)
+      end;
+
+fun firstIterator f io =
+    case io of
+      NONE => NONE
+    | SOME iter =>
+      let
+        val key_value = readIterator iter
+      in
+        case f key_value of
+          NONE => firstIterator f (advanceIterator iter)
+        | s => s
+      end;
+
+fun compareIterator compareValue io1 io2 =
+    case (io1,io2) of
+      (NONE,NONE) => EQUAL
+    | (NONE, SOME _) => LESS
+    | (SOME _, NONE) => GREATER
+    | (SOME i1, SOME i2) =>
+      let
+        val (k1,v1) = readIterator i1
+        and (k2,v2) = readIterator i2
+      in
+        case compareKey (k1,k2) of
+          LESS => LESS
+        | EQUAL =>
+          (case compareValue (v1,v2) of
+             LESS => LESS
+           | EQUAL =>
+             let
+               val io1 = advanceIterator i1
+               and io2 = advanceIterator i2
+             in
+               compareIterator compareValue io1 io2
+             end
+           | GREATER => GREATER)
+        | GREATER => GREATER
+      end;
+
+fun equalIterator equalValue io1 io2 =
+    case (io1,io2) of
+      (NONE,NONE) => true
+    | (NONE, SOME _) => false
+    | (SOME _, NONE) => false
+    | (SOME i1, SOME i2) =>
+      let
+        val (k1,v1) = readIterator i1
+        and (k2,v2) = readIterator i2
+      in
+        equalKey k1 k2 andalso
+        equalValue v1 v2 andalso
+        let
+          val io1 = advanceIterator i1
+          and io2 = advanceIterator i2
+        in
+          equalIterator equalValue io1 io2
+        end
+      end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite maps.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+datatype 'value map =
+    Map of 'value tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Map debugging functions.                                                  *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+fun checkInvariants s m =
+    let
+      val Map tree = m
+
+      val _ = treeCheckInvariants tree
+    in
+      m
+    end
+    handle Bug bug => raise Bug (s ^ "\n" ^ "KeyMap.checkInvariants: " ^ bug);
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors.                                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun new () =
+    let
+      val tree = treeNew ()
+    in
+      Map tree
+    end;
+
+fun singleton key_value =
+    let
+      val tree = treeSingleton key_value
+    in
+      Map tree
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Map size.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun size (Map tree) = treeSize tree;
+
+fun null m = size m = 0;
+
+(* ------------------------------------------------------------------------- *)
+(* Querying.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun peekKey (Map tree) key = treePeekKey key tree;
+
+fun peek (Map tree) key = treePeek key tree;
+
+fun inDomain key m = Option.isSome (peek m key);
+
+fun get m key =
+    case peek m key of
+      NONE => raise Error "KeyMap.get: element not found"
+    | SOME value => value;
+
+fun pick (Map tree) = treePick tree;
+
+fun nth (Map tree) n = treeNth n tree;
+
+fun random m =
+    let
+      val n = size m
+    in
+      if n = 0 then raise Bug "KeyMap.random: empty"
+      else nth m (randomInt n)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Adding.                                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+fun insert (Map tree) key_value =
+    let
+      val tree = treeInsert key_value tree
+    in
+      Map tree
+    end;
+
+(*BasicDebug
+val insert = fn m => fn kv =>
+    checkInvariants "KeyMap.insert: result"
+      (insert (checkInvariants "KeyMap.insert: input" m) kv);
+*)
+
+fun insertList m =
+    let
+      fun ins (key_value,acc) = insert acc key_value
+    in
+      List.foldl ins m
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun delete (Map tree) dkey =
+    let
+      val tree = treeDelete dkey tree
+    in
+      Map tree
+    end;
+
+(*BasicDebug
+val delete = fn m => fn k =>
+    checkInvariants "KeyMap.delete: result"
+      (delete (checkInvariants "KeyMap.delete: input" m) k);
+*)
+
+fun remove m key = if inDomain key m then delete m key else m;
+
+fun deletePick (Map tree) =
+    let
+      val (key_value,tree) = treeDeletePick tree
+    in
+      (key_value, Map tree)
+    end;
+
+(*BasicDebug
+val deletePick = fn m =>
+    let
+      val (kv,m) = deletePick (checkInvariants "KeyMap.deletePick: input" m)
+    in
+      (kv, checkInvariants "KeyMap.deletePick: result" m)
+    end;
+*)
+
+fun deleteNth (Map tree) n =
+    let
+      val (key_value,tree) = treeDeleteNth n tree
+    in
+      (key_value, Map tree)
+    end;
+
+(*BasicDebug
+val deleteNth = fn m => fn n =>
+    let
+      val (kv,m) = deleteNth (checkInvariants "KeyMap.deleteNth: input" m) n
+    in
+      (kv, checkInvariants "KeyMap.deleteNth: result" m)
+    end;
+*)
+
+fun deleteRandom m =
+    let
+      val n = size m
+    in
+      if n = 0 then raise Bug "KeyMap.deleteRandom: empty"
+      else deleteNth m (randomInt n)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Joining (all join operations prefer keys in the second map).              *)
+(* ------------------------------------------------------------------------- *)
+
+fun merge {first,second,both} (Map tree1) (Map tree2) =
+    let
+      val tree = treeMerge first second both tree1 tree2
+    in
+      Map tree
+    end;
+
+(*BasicDebug
+val merge = fn f => fn m1 => fn m2 =>
+    checkInvariants "KeyMap.merge: result"
+      (merge f
+         (checkInvariants "KeyMap.merge: input 1" m1)
+         (checkInvariants "KeyMap.merge: input 2" m2));
+*)
+
+fun union f (Map tree1) (Map tree2) =
+    let
+      fun f2 kv = f (kv,kv)
+
+      val tree = treeUnion f f2 tree1 tree2
+    in
+      Map tree
+    end;
+
+(*BasicDebug
+val union = fn f => fn m1 => fn m2 =>
+    checkInvariants "KeyMap.union: result"
+      (union f
+         (checkInvariants "KeyMap.union: input 1" m1)
+         (checkInvariants "KeyMap.union: input 2" m2));
+*)
+
+fun intersect f (Map tree1) (Map tree2) =
+    let
+      val tree = treeIntersect f tree1 tree2
+    in
+      Map tree
+    end;
+
+(*BasicDebug
+val intersect = fn f => fn m1 => fn m2 =>
+    checkInvariants "KeyMap.intersect: result"
+      (intersect f
+         (checkInvariants "KeyMap.intersect: input 1" m1)
+         (checkInvariants "KeyMap.intersect: input 2" m2));
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over maps.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkIterator (Map tree) = treeMkIterator tree;
+
+fun mkRevIterator (Map tree) = treeMkRevIterator tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+fun mapPartial f (Map tree) =
+    let
+      val tree = treeMapPartial f tree
+    in
+      Map tree
+    end;
+
+(*BasicDebug
+val mapPartial = fn f => fn m =>
+    checkInvariants "KeyMap.mapPartial: result"
+      (mapPartial f (checkInvariants "KeyMap.mapPartial: input" m));
+*)
+
+fun map f (Map tree) =
+    let
+      val tree = treeMap f tree
+    in
+      Map tree
+    end;
+
+(*BasicDebug
+val map = fn f => fn m =>
+    checkInvariants "KeyMap.map: result"
+      (map f (checkInvariants "KeyMap.map: input" m));
+*)
+
+fun transform f = map (fn (_,value) => f value);
+
+fun filter pred =
+    let
+      fun f (key_value as (_,value)) =
+          if pred key_value then SOME value else NONE
+    in
+      mapPartial f
+    end;
+
+fun partition p =
+    let
+      fun np x = not (p x)
+    in
+      fn m => (filter p m, filter np m)
+    end;
+
+fun foldl f b m = foldIterator f b (mkIterator m);
+
+fun foldr f b m = foldIterator f b (mkRevIterator m);
+
+fun app f m = foldl (fn (key,value,()) => f (key,value)) () m;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+fun findl p m = findIterator p (mkIterator m);
+
+fun findr p m = findIterator p (mkRevIterator m);
+
+fun firstl f m = firstIterator f (mkIterator m);
+
+fun firstr f m = firstIterator f (mkRevIterator m);
+
+fun exists p m = Option.isSome (findl p m);
+
+fun all p =
+    let
+      fun np x = not (p x)
+    in
+      fn m => not (exists np m)
+    end;
+
+fun count pred =
+    let
+      fun f (k,v,acc) = if pred (k,v) then acc + 1 else acc
+    in
+      foldl f 0
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare compareValue (m1,m2) =
+    if pointerEqual (m1,m2) then EQUAL
+    else
+      case Int.compare (size m1, size m2) of
+        LESS => LESS
+      | EQUAL =>
+        let
+          val Map _ = m1
+
+          val io1 = mkIterator m1
+          and io2 = mkIterator m2
+        in
+          compareIterator compareValue io1 io2
+        end
+      | GREATER => GREATER;
+
+fun equal equalValue m1 m2 =
+    pointerEqual (m1,m2) orelse
+    (size m1 = size m2 andalso
+     let
+       val Map _ = m1
+
+       val io1 = mkIterator m1
+       and io2 = mkIterator m2
+     in
+       equalIterator equalValue io1 io2
+     end);
+
+(* ------------------------------------------------------------------------- *)
+(* Set operations on the domain.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun unionDomain (Map tree1) (Map tree2) =
+    let
+      val tree = treeUnionDomain tree1 tree2
+    in
+      Map tree
+    end;
+
+(*BasicDebug
+val unionDomain = fn m1 => fn m2 =>
+    checkInvariants "KeyMap.unionDomain: result"
+      (unionDomain
+         (checkInvariants "KeyMap.unionDomain: input 1" m1)
+         (checkInvariants "KeyMap.unionDomain: input 2" m2));
+*)
+
+local
+  fun uncurriedUnionDomain (m,acc) = unionDomain acc m;
+in
+  fun unionListDomain ms =
+      case ms of
+        [] => raise Bug "KeyMap.unionListDomain: no sets"
+      | m :: ms => List.foldl uncurriedUnionDomain m ms;
+end;
+
+fun intersectDomain (Map tree1) (Map tree2) =
+    let
+      val tree = treeIntersectDomain tree1 tree2
+    in
+      Map tree
+    end;
+
+(*BasicDebug
+val intersectDomain = fn m1 => fn m2 =>
+    checkInvariants "KeyMap.intersectDomain: result"
+      (intersectDomain
+         (checkInvariants "KeyMap.intersectDomain: input 1" m1)
+         (checkInvariants "KeyMap.intersectDomain: input 2" m2));
+*)
+
+local
+  fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m;
+in
+  fun intersectListDomain ms =
+      case ms of
+        [] => raise Bug "KeyMap.intersectListDomain: no sets"
+      | m :: ms => List.foldl uncurriedIntersectDomain m ms;
+end;
+
+fun differenceDomain (Map tree1) (Map tree2) =
+    let
+      val tree = treeDifferenceDomain tree1 tree2
+    in
+      Map tree
+    end;
+
+(*BasicDebug
+val differenceDomain = fn m1 => fn m2 =>
+    checkInvariants "KeyMap.differenceDomain: result"
+      (differenceDomain
+         (checkInvariants "KeyMap.differenceDomain: input 1" m1)
+         (checkInvariants "KeyMap.differenceDomain: input 2" m2));
+*)
+
+fun symmetricDifferenceDomain m1 m2 =
+    unionDomain (differenceDomain m1 m2) (differenceDomain m2 m1);
+
+fun equalDomain m1 m2 = equal (K (K true)) m1 m2;
+
+fun subsetDomain (Map tree1) (Map tree2) =
+    treeSubsetDomain tree1 tree2;
+
+fun disjointDomain m1 m2 = null (intersectDomain m1 m2);
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun keys m = foldr (fn (key,_,l) => key :: l) [] m;
+
+fun values m = foldr (fn (_,value,l) => value :: l) [] m;
+
+fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
+
+fun fromList l =
+    let
+      val m = new ()
+    in
+      insertList m l
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";
+
+end
+
+structure IntMap =
+KeyMap (IntOrdered);
+
+structure IntPairMap =
+KeyMap (IntPairOrdered);
+
+structure StringMap =
+KeyMap (StringOrdered);
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,22 @@
+(* ========================================================================= *)
+(* THE KNUTH-BENDIX TERM ORDERING                                            *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature KnuthBendixOrder =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* The weight of all constants must be at least 1, and there must be at most *)
+(* one unary function with weight 0.                                         *)
+(* ------------------------------------------------------------------------- *)
+
+type kbo =
+     {weight : Term.function -> int,
+      precedence : Term.function * Term.function -> order}
+
+val default : kbo
+
+val compare : kbo -> Term.term * Term.term -> order option
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,199 @@
+(* ========================================================================= *)
+(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS                                    *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure KnuthBendixOrder :> KnuthBendixOrder =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun notEqualTerm (x,y) = not (Term.equal x y);
+
+fun firstNotEqualTerm f l =
+    case List.find notEqualTerm l of
+      SOME (x,y) => f x y
+    | NONE => raise Bug "firstNotEqualTerm";
+
+(* ------------------------------------------------------------------------- *)
+(* The weight of all constants must be at least 1, and there must be at most *)
+(* one unary function with weight 0.                                         *)
+(* ------------------------------------------------------------------------- *)
+
+type kbo =
+     {weight : Term.function -> int,
+      precedence : Term.function * Term.function -> order};
+
+(* Default weight = uniform *)
+
+val uniformWeight : Term.function -> int = K 1;
+
+(* Default precedence = by arity *)
+
+val arityPrecedence : Term.function * Term.function -> order =
+    fn ((f1,n1),(f2,n2)) =>
+       case Int.compare (n1,n2) of
+         LESS => LESS
+       | EQUAL => Name.compare (f1,f2)
+       | GREATER => GREATER;
+
+(* The default order *)
+
+val default = {weight = uniformWeight, precedence = arityPrecedence};
+
+(* ------------------------------------------------------------------------- *)
+(* Term weight-1 represented as a linear function of the weight-1 of the     *)
+(* variables in the term (plus a constant).                                  *)
+(*                                                                           *)
+(* Note that the conditions on weight functions ensure that all weights are  *)
+(* at least 1, so all weight-1s are at least 0.                              *)
+(* ------------------------------------------------------------------------- *)
+
+datatype weight = Weight of int NameMap.map * int;
+
+val weightEmpty : int NameMap.map = NameMap.new ();
+
+val weightZero = Weight (weightEmpty,0);
+
+fun weightIsZero (Weight (m,c)) = c = 0 andalso NameMap.null m;
+
+fun weightNeg (Weight (m,c)) = Weight (NameMap.transform ~ m, ~c);
+
+local
+  fun add ((_,n1),(_,n2)) =
+      let
+        val n = n1 + n2
+      in
+        if n = 0 then NONE else SOME n
+      end;
+in
+  fun weightAdd (Weight (m1,c1)) (Weight (m2,c2)) =
+      Weight (NameMap.union add m1 m2, c1 + c2);
+end;
+
+fun weightSubtract w1 w2 = weightAdd w1 (weightNeg w2);
+
+fun weightTerm weight =
+    let
+      fun wt m c [] = Weight (m,c)
+        | wt m c (Term.Var v :: tms) =
+          let
+            val n = Option.getOpt (NameMap.peek m v, 0)
+          in
+            wt (NameMap.insert m (v, n + 1)) (c + 1) tms
+          end
+        | wt m c (Term.Fn (f,a) :: tms) =
+          wt m (c + weight (f, length a)) (a @ tms)
+    in
+      fn tm => wt weightEmpty ~1 [tm]
+    end;
+
+fun weightLowerBound (w as Weight (m,c)) =
+    if NameMap.exists (fn (_,n) => n < 0) m then NONE else SOME c;
+
+(*MetisDebug
+val ppWeightList =
+    let
+      fun ppCoeff n =
+          if n < 0 then Print.sequence (Print.addString "~") (ppCoeff (~n))
+          else if n = 1 then Print.skip
+          else Print.ppInt n
+
+      fun pp_tm (NONE,n) = Print.ppInt n
+        | pp_tm (SOME v, n) = Print.sequence (ppCoeff n) (Name.pp v)
+    in
+      fn [] => Print.ppInt 0
+       | tms => Print.ppOpList " +" pp_tm tms
+    end;
+
+fun ppWeight (Weight (m,c)) =
+    let
+      val l = NameMap.toList m
+      val l = map (fn (v,n) => (SOME v, n)) l
+      val l = if c = 0 then l else l @ [(NONE,c)]
+    in
+      ppWeightList l
+    end;
+
+val weightToString = Print.toString ppWeight;
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* The Knuth-Bendix term order.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare {weight,precedence} =
+    let
+      fun weightDifference tm1 tm2 =
+          let
+            val w1 = weightTerm weight tm1
+            and w2 = weightTerm weight tm2
+          in
+            weightSubtract w2 w1
+          end
+
+      fun weightLess tm1 tm2 =
+          let
+            val w = weightDifference tm1 tm2
+          in
+            if weightIsZero w then precedenceLess tm1 tm2
+            else weightDiffLess w tm1 tm2
+          end
+
+      and weightDiffLess w tm1 tm2 =
+          case weightLowerBound w of
+            NONE => false
+          | SOME 0 => precedenceLess tm1 tm2
+          | SOME n => n > 0
+
+      and precedenceLess (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) =
+          (case precedence ((f1, length a1), (f2, length a2)) of
+             LESS => true
+           | EQUAL => firstNotEqualTerm weightLess (zip a1 a2)
+           | GREATER => false)
+        | precedenceLess _ _ = false
+
+      fun weightDiffGreater w tm1 tm2 = weightDiffLess (weightNeg w) tm2 tm1
+
+      fun weightCmp tm1 tm2 =
+          let
+            val w = weightDifference tm1 tm2
+          in
+            if weightIsZero w then precedenceCmp tm1 tm2
+            else if weightDiffLess w tm1 tm2 then SOME LESS
+            else if weightDiffGreater w tm1 tm2 then SOME GREATER
+            else NONE
+          end
+
+      and precedenceCmp (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) =
+          (case precedence ((f1, length a1), (f2, length a2)) of
+             LESS => SOME LESS
+           | EQUAL => firstNotEqualTerm weightCmp (zip a1 a2)
+           | GREATER => SOME GREATER)
+        | precedenceCmp _ _ = raise Bug "kboOrder.precendenceCmp"
+    in
+      fn (tm1,tm2) =>
+         if Term.equal tm1 tm2 then SOME EQUAL else weightCmp tm1 tm2
+    end;
+
+(*MetisTrace7
+val compare = fn kbo => fn (tm1,tm2) =>
+    let
+      val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm1" tm1
+      val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm2" tm2
+      val result = compare kbo (tm1,tm2)
+      val () =
+          case result of
+            NONE => trace "KnuthBendixOrder.compare: result = Incomparable\n"
+          | SOME x =>
+            Print.trace Print.ppOrder "KnuthBendixOrder.compare: result" x
+    in
+      result
+    end;
+*)
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Lazy.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,19 @@
+(* ========================================================================= *)
+(* SUPPORT FOR LAZY EVALUATION                                               *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+signature Lazy =
+sig
+
+type 'a lazy
+
+val quickly : 'a -> 'a lazy
+
+val delay : (unit -> 'a) -> 'a lazy
+
+val force : 'a lazy -> 'a
+
+val memoize : (unit -> 'a) -> unit -> 'a
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Lazy.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,38 @@
+(* ========================================================================= *)
+(* SUPPORT FOR LAZY EVALUATION                                               *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+structure Lazy :> Lazy =
+struct
+
+datatype 'a thunk =
+    Value of 'a
+  | Thunk of unit -> 'a;
+
+datatype 'a lazy = Lazy of 'a thunk ref;
+
+fun quickly v = Lazy (ref (Value v));
+
+fun delay f = Lazy (ref (Thunk f));
+
+fun force (Lazy s) =
+    case !s of
+      Value v => v
+    | Thunk f =>
+      let
+        val v = f ()
+
+        val () = s := Value v
+      in
+        v
+      end;
+
+fun memoize f =
+    let
+      val t = delay f
+    in
+      fn () => force t
+    end;
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Literal.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,165 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC LITERALS                                                *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Literal =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic literals.                            *)
+(* ------------------------------------------------------------------------- *)
+
+type polarity = bool
+
+type literal = polarity * Atom.atom
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val polarity : literal -> polarity
+
+val atom : literal -> Atom.atom
+
+val name : literal -> Atom.relationName
+
+val arguments : literal -> Term.term list
+
+val arity : literal -> int
+
+val positive : literal -> bool
+
+val negative : literal -> bool
+
+val negate : literal -> literal
+
+val relation : literal -> Atom.relation
+
+val functions : literal -> NameAritySet.set
+
+val functionNames : literal -> NameSet.set
+
+(* Binary relations *)
+
+val mkBinop : Atom.relationName -> polarity * Term.term * Term.term -> literal
+
+val destBinop : Atom.relationName -> literal -> polarity * Term.term * Term.term
+
+val isBinop : Atom.relationName -> literal -> bool
+
+(* Formulas *)
+
+val toFormula : literal -> Formula.formula
+
+val fromFormula : Formula.formula -> literal
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a literal in symbols.                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : literal -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for literals.                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : literal * literal -> order  (* negative < positive *)
+
+val equal : literal -> literal -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val subterm : literal -> Term.path -> Term.term
+
+val subterms : literal -> (Term.path * Term.term) list
+
+val replace : literal -> Term.path * Term.term -> literal
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Term.var -> literal -> bool
+
+val freeVars : literal -> NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions.                                                            *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Subst.subst -> literal -> literal
+
+(* ------------------------------------------------------------------------- *)
+(* Matching.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val match :  (* raises Error *)
+    Subst.subst -> literal -> literal -> Subst.subst
+
+(* ------------------------------------------------------------------------- *)
+(* Unification.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val unify :  (* raises Error *)
+    Subst.subst -> literal -> literal -> Subst.subst
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+val mkEq : Term.term * Term.term -> literal
+
+val destEq : literal -> Term.term * Term.term
+
+val isEq : literal -> bool
+
+val mkNeq : Term.term * Term.term -> literal
+
+val destNeq : literal -> Term.term * Term.term
+
+val isNeq : literal -> bool
+
+val mkRefl : Term.term -> literal
+
+val destRefl : literal -> Term.term
+
+val isRefl : literal -> bool
+
+val mkIrrefl : Term.term -> literal
+
+val destIrrefl : literal -> Term.term
+
+val isIrrefl : literal -> bool
+
+(* The following work with both equalities and disequalities *)
+
+val sym : literal -> literal  (* raises Error if given a refl or irrefl *)
+
+val lhs : literal -> Term.term
+
+val rhs : literal -> Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations.                          *)
+(* ------------------------------------------------------------------------- *)
+
+val typedSymbols : literal -> int
+
+val nonVarTypedSubterms : literal -> (Term.path * Term.term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : literal Print.pp
+
+val toString : literal -> string
+
+val fromString : string -> literal
+
+val parse : Term.term Parse.quotation -> literal
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Literal.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,293 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC LITERALS                                                *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Literal :> Literal =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic literals.                            *)
+(* ------------------------------------------------------------------------- *)
+
+type polarity = bool;
+
+type literal = polarity * Atom.atom;
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun polarity ((pol,_) : literal) = pol;
+
+fun atom ((_,atm) : literal) = atm;
+
+fun name lit = Atom.name (atom lit);
+
+fun arguments lit = Atom.arguments (atom lit);
+
+fun arity lit = Atom.arity (atom lit);
+
+fun positive lit = polarity lit;
+
+fun negative lit = not (polarity lit);
+
+fun negate (pol,atm) : literal = (not pol, atm)
+
+fun relation lit = Atom.relation (atom lit);
+
+fun functions lit = Atom.functions (atom lit);
+
+fun functionNames lit = Atom.functionNames (atom lit);
+
+(* Binary relations *)
+
+fun mkBinop rel (pol,a,b) : literal = (pol, Atom.mkBinop rel (a,b));
+
+fun destBinop rel ((pol,atm) : literal) =
+    case Atom.destBinop rel atm of (a,b) => (pol,a,b);
+
+fun isBinop rel = can (destBinop rel);
+
+(* Formulas *)
+
+fun toFormula (true,atm) = Formula.Atom atm
+  | toFormula (false,atm) = Formula.Not (Formula.Atom atm);
+
+fun fromFormula (Formula.Atom atm) = (true,atm)
+  | fromFormula (Formula.Not (Formula.Atom atm)) = (false,atm)
+  | fromFormula _ = raise Error "Literal.fromFormula";
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a literal in symbols.                                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun symbols ((_,atm) : literal) = Atom.symbols atm;
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for literals.                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val compare = prodCompare boolCompare Atom.compare;
+
+fun equal (p1,atm1) (p2,atm2) = p1 = p2 andalso Atom.equal atm1 atm2;
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun subterm lit path = Atom.subterm (atom lit) path;
+
+fun subterms lit = Atom.subterms (atom lit);
+
+fun replace (lit as (pol,atm)) path_tm =
+    let
+      val atm' = Atom.replace atm path_tm
+    in
+      if Portable.pointerEqual (atm,atm') then lit else (pol,atm')
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+fun freeIn v lit = Atom.freeIn v (atom lit);
+
+fun freeVars lit = Atom.freeVars (atom lit);
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions.                                                            *)
+(* ------------------------------------------------------------------------- *)
+
+fun subst sub (lit as (pol,atm)) : literal =
+    let
+      val atm' = Atom.subst sub atm
+    in
+      if Portable.pointerEqual (atm',atm) then lit else (pol,atm')
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Matching.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun match sub ((pol1,atm1) : literal) (pol2,atm2) =
+    let
+      val _ = pol1 = pol2 orelse raise Error "Literal.match"
+    in
+      Atom.match sub atm1 atm2
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Unification.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun unify sub ((pol1,atm1) : literal) (pol2,atm2) =
+    let
+      val _ = pol1 = pol2 orelse raise Error "Literal.unify"
+    in
+      Atom.unify sub atm1 atm2
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkEq l_r : literal = (true, Atom.mkEq l_r);
+
+fun destEq ((true,atm) : literal) = Atom.destEq atm
+  | destEq (false,_) = raise Error "Literal.destEq";
+
+val isEq = can destEq;
+
+fun mkNeq l_r : literal = (false, Atom.mkEq l_r);
+
+fun destNeq ((false,atm) : literal) = Atom.destEq atm
+  | destNeq (true,_) = raise Error "Literal.destNeq";
+
+val isNeq = can destNeq;
+
+fun mkRefl tm = (true, Atom.mkRefl tm);
+
+fun destRefl (true,atm) = Atom.destRefl atm
+  | destRefl (false,_) = raise Error "Literal.destRefl";
+
+val isRefl = can destRefl;
+
+fun mkIrrefl tm = (false, Atom.mkRefl tm);
+
+fun destIrrefl (true,_) = raise Error "Literal.destIrrefl"
+  | destIrrefl (false,atm) = Atom.destRefl atm;
+
+val isIrrefl = can destIrrefl;
+
+fun sym (pol,atm) : literal = (pol, Atom.sym atm);
+
+fun lhs ((_,atm) : literal) = Atom.lhs atm;
+
+fun rhs ((_,atm) : literal) = Atom.rhs atm;
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations.                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun typedSymbols ((_,atm) : literal) = Atom.typedSymbols atm;
+
+fun nonVarTypedSubterms ((_,atm) : literal) = Atom.nonVarTypedSubterms atm;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val pp = Print.ppMap toFormula Formula.pp;
+
+val toString = Print.toString pp;
+
+fun fromString s = fromFormula (Formula.fromString s);
+
+val parse = Parse.parseQuotation Term.toString fromString;
+
+end
+
+structure LiteralOrdered =
+struct type t = Literal.literal val compare = Literal.compare end
+
+structure LiteralMap = KeyMap (LiteralOrdered);
+
+structure LiteralSet =
+struct
+
+  local
+    structure S = ElementSet (LiteralMap);
+  in
+    open S;
+  end;
+
+  fun negateMember lit set = member (Literal.negate lit) set;
+
+  val negate =
+      let
+        fun f (lit,set) = add set (Literal.negate lit)
+      in
+        foldl f empty
+      end;
+
+  val relations =
+      let
+        fun f (lit,set) = NameAritySet.add set (Literal.relation lit)
+      in
+        foldl f NameAritySet.empty
+      end;
+
+  val functions =
+      let
+        fun f (lit,set) = NameAritySet.union set (Literal.functions lit)
+      in
+        foldl f NameAritySet.empty
+      end;
+
+  fun freeIn v = exists (Literal.freeIn v);
+
+  val freeVars =
+      let
+        fun f (lit,set) = NameSet.union set (Literal.freeVars lit)
+      in
+        foldl f NameSet.empty
+      end;
+
+  val freeVarsList =
+      let
+        fun f (lits,set) = NameSet.union set (freeVars lits)
+      in
+        List.foldl f NameSet.empty
+      end;
+
+  val symbols =
+      let
+        fun f (lit,z) = Literal.symbols lit + z
+      in
+        foldl f 0
+      end;
+
+  val typedSymbols =
+      let
+        fun f (lit,z) = Literal.typedSymbols lit + z
+      in
+        foldl f 0
+      end;
+
+  fun subst sub lits =
+      let
+        fun substLit (lit,(eq,lits')) =
+            let
+              val lit' = Literal.subst sub lit
+              val eq = eq andalso Portable.pointerEqual (lit,lit')
+            in
+              (eq, add lits' lit')
+            end
+
+        val (eq,lits') = foldl substLit (true,empty) lits
+      in
+        if eq then lits else lits'
+      end;
+
+  fun conjoin set =
+      Formula.listMkConj (List.map Literal.toFormula (toList set));
+
+  fun disjoin set =
+      Formula.listMkDisj (List.map Literal.toFormula (toList set));
+
+  val pp =
+      Print.ppMap
+        toList
+        (Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp));
+
+end
+
+structure LiteralSetOrdered =
+struct type t = LiteralSet.set val compare = LiteralSet.compare end
+
+structure LiteralSetMap = KeyMap (LiteralSetOrdered);
+
+structure LiteralSetSet = ElementSet (LiteralSetMap);
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/LiteralNet.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,50 @@
+(* ========================================================================= *)
+(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS           *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature LiteralNet =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of literal sets that can be efficiently matched and unified.       *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = {fifo : bool}
+
+type 'a literalNet
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val new : parameters -> 'a literalNet
+
+val size : 'a literalNet -> int
+
+val profile : 'a literalNet -> {positive : int, negative : int}
+
+val insert : 'a literalNet -> Literal.literal * 'a -> 'a literalNet
+
+val fromList : parameters -> (Literal.literal * 'a) list -> 'a literalNet
+
+val filter : ('a -> bool) -> 'a literalNet -> 'a literalNet
+
+val toString : 'a literalNet -> string
+
+val pp : 'a Print.pp -> 'a literalNet Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* Matching and unification queries.                                         *)
+(*                                                                           *)
+(* These function return OVER-APPROXIMATIONS!                                *)
+(* Filter afterwards to get the precise set of satisfying values.            *)
+(* ------------------------------------------------------------------------- *)
+
+val match : 'a literalNet -> Literal.literal -> 'a list
+
+val matched : 'a literalNet -> Literal.literal -> 'a list
+
+val unify : 'a literalNet -> Literal.literal -> 'a list
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/LiteralNet.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,74 @@
+(* ========================================================================= *)
+(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS           *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure LiteralNet :> LiteralNet =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of literal sets that can be efficiently matched and unified.       *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = AtomNet.parameters;
+
+type 'a literalNet =
+    {positive : 'a AtomNet.atomNet,
+     negative : 'a AtomNet.atomNet};
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun new parm = {positive = AtomNet.new parm, negative = AtomNet.new parm};
+
+local
+  fun pos ({positive,...} : 'a literalNet) = AtomNet.size positive;
+
+  fun neg ({negative,...} : 'a literalNet) = AtomNet.size negative;
+in
+  fun size net = pos net + neg net;
+
+  fun profile net = {positive = pos net, negative = neg net};
+end;
+
+fun insert {positive,negative} ((true,atm),a) =
+    {positive = AtomNet.insert positive (atm,a), negative = negative}
+  | insert {positive,negative} ((false,atm),a) =
+    {positive = positive, negative = AtomNet.insert negative (atm,a)};
+
+fun fromList parm l = foldl (fn (lit_a,n) => insert n lit_a) (new parm) l;
+
+fun filter pred {positive,negative} =
+    {positive = AtomNet.filter pred positive,
+     negative = AtomNet.filter pred negative};
+
+fun toString net = "LiteralNet[" ^ Int.toString (size net) ^ "]";
+
+fun pp ppA =
+    Print.ppMap
+      (fn {positive,negative} => (positive,negative))
+      (Print.ppOp2 " + NEGATIVE" (AtomNet.pp ppA) (AtomNet.pp ppA));
+
+(* ------------------------------------------------------------------------- *)
+(* Matching and unification queries.                                         *)
+(*                                                                           *)
+(* These function return OVER-APPROXIMATIONS!                                *)
+(* Filter afterwards to get the precise set of satisfying values.            *)
+(* ------------------------------------------------------------------------- *)
+
+fun match ({positive,...} : 'a literalNet) (true,atm) =
+    AtomNet.match positive atm
+  | match {negative,...} (false,atm) = AtomNet.match negative atm;
+
+fun matched ({positive,...} : 'a literalNet) (true,atm) =
+    AtomNet.matched positive atm
+  | matched {negative,...} (false,atm) = AtomNet.matched negative atm;
+
+fun unify ({positive,...} : 'a literalNet) (true,atm) =
+    AtomNet.unify positive atm
+  | unify {negative,...} (false,atm) = AtomNet.unify negative atm;
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Map.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,190 @@
+(* ========================================================================= *)
+(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+signature Map =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite maps.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+type ('key,'a) map
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors.                                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val new : ('key * 'key -> order) -> ('key,'a) map
+
+val singleton : ('key * 'key -> order) -> 'key * 'a -> ('key,'a) map
+
+(* ------------------------------------------------------------------------- *)
+(* Map size.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val null : ('key,'a) map -> bool
+
+val size : ('key,'a) map -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Querying.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val peekKey : ('key,'a) map -> 'key -> ('key * 'a) option
+
+val peek : ('key,'a) map -> 'key -> 'a option
+
+val get : ('key,'a) map -> 'key -> 'a  (* raises Error *)
+
+val pick : ('key,'a) map -> 'key * 'a  (* an arbitrary key/value pair *)
+
+val nth : ('key,'a) map -> int -> 'key * 'a  (* in the range [0,size-1] *)
+
+val random : ('key,'a) map -> 'key * 'a
+
+(* ------------------------------------------------------------------------- *)
+(* Adding.                                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+val insert : ('key,'a) map -> 'key * 'a -> ('key,'a) map
+
+val insertList : ('key,'a) map -> ('key * 'a) list -> ('key,'a) map
+
+(* ------------------------------------------------------------------------- *)
+(* Removing.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val delete : ('key,'a) map -> 'key -> ('key,'a) map  (* must be present *)
+
+val remove : ('key,'a) map -> 'key -> ('key,'a) map
+
+val deletePick : ('key,'a) map -> ('key * 'a) * ('key,'a) map
+
+val deleteNth : ('key,'a) map -> int -> ('key * 'a) * ('key,'a) map
+
+val deleteRandom : ('key,'a) map -> ('key * 'a) * ('key,'a) map
+
+(* ------------------------------------------------------------------------- *)
+(* Joining (all join operations prefer keys in the second map).              *)
+(* ------------------------------------------------------------------------- *)
+
+val merge :
+    {first : 'key * 'a -> 'c option,
+     second : 'key * 'b -> 'c option,
+     both : ('key * 'a) * ('key * 'b) -> 'c option} ->
+    ('key,'a) map -> ('key,'b) map -> ('key,'c) map
+
+val union :
+    (('key * 'a) * ('key * 'a) -> 'a option) ->
+    ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+
+val intersect :
+    (('key * 'a) * ('key * 'b) -> 'c option) ->
+    ('key,'a) map -> ('key,'b) map -> ('key,'c) map
+
+(* ------------------------------------------------------------------------- *)
+(* Set operations on the domain.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val inDomain : 'key -> ('key,'a) map -> bool
+
+val unionDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+
+val unionListDomain : ('key,'a) map list -> ('key,'a) map
+
+val intersectDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+
+val intersectListDomain : ('key,'a) map list -> ('key,'a) map
+
+val differenceDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+
+val symmetricDifferenceDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+
+val equalDomain : ('key,'a) map -> ('key,'a) map -> bool
+
+val subsetDomain : ('key,'a) map -> ('key,'a) map -> bool
+
+val disjointDomain : ('key,'a) map -> ('key,'a) map -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+val mapPartial : ('key * 'a -> 'b option) -> ('key,'a) map -> ('key,'b) map
+
+val map : ('key * 'a -> 'b) -> ('key,'a) map -> ('key,'b) map
+
+val app : ('key * 'a -> unit) -> ('key,'a) map -> unit
+
+val transform : ('a -> 'b) -> ('key,'a) map -> ('key,'b) map
+
+val filter : ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map
+
+val partition :
+    ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map * ('key,'a) map
+
+val foldl : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
+
+val foldr : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
+
+(* ------------------------------------------------------------------------- *)
+(* Searching.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val findl : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
+
+val findr : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
+
+val firstl : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
+
+val firstr : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
+
+val exists : ('key * 'a -> bool) -> ('key,'a) map -> bool
+
+val all : ('key * 'a -> bool) -> ('key,'a) map -> bool
+
+val count : ('key * 'a -> bool) -> ('key,'a) map -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : ('a * 'a -> order) -> ('key,'a) map * ('key,'a) map -> order
+
+val equal : ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+val keys : ('key,'a) map -> 'key list
+
+val values : ('key,'a) map -> 'a list
+
+val toList : ('key,'a) map -> ('key * 'a) list
+
+val fromList : ('key * 'key -> order) -> ('key * 'a) list -> ('key,'a) map
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val toString : ('key,'a) map -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over maps.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+type ('key,'a) iterator
+
+val mkIterator : ('key,'a) map -> ('key,'a) iterator option
+
+val mkRevIterator : ('key,'a) map -> ('key,'a) iterator option
+
+val readIterator : ('key,'a) iterator -> 'key * 'a
+
+val advanceIterator : ('key,'a) iterator -> ('key,'a) iterator option
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Map.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,1425 @@
+(* ========================================================================= *)
+(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+structure Map :> Map =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* Importing useful functionality.                                           *)
+(* ------------------------------------------------------------------------- *)
+
+exception Bug = Useful.Bug;
+
+exception Error = Useful.Error;
+
+val pointerEqual = Portable.pointerEqual;
+
+val K = Useful.K;
+
+val randomInt = Portable.randomInt;
+
+val randomWord = Portable.randomWord;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting a comparison function to an equality function.                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun equalKey compareKey key1 key2 = compareKey (key1,key2) = EQUAL;
+
+(* ------------------------------------------------------------------------- *)
+(* Priorities.                                                               *)
+(* ------------------------------------------------------------------------- *)
+
+type priority = Word.word;
+
+val randomPriority = randomWord;
+
+val comparePriority = Word.compare;
+
+(* ------------------------------------------------------------------------- *)
+(* Priority search trees.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ('key,'value) tree =
+    E
+  | T of ('key,'value) node
+
+and ('key,'value) node =
+    Node of
+      {size : int,
+       priority : priority,
+       left : ('key,'value) tree,
+       key : 'key,
+       value : 'value,
+       right : ('key,'value) tree};
+
+fun lowerPriorityNode node1 node2 =
+    let
+      val Node {priority = p1, ...} = node1
+      and Node {priority = p2, ...} = node2
+    in
+      comparePriority (p1,p2) = LESS
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Tree debugging functions.                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+local
+  fun checkSizes tree =
+      case tree of
+        E => 0
+      | T (Node {size,left,right,...}) =>
+        let
+          val l = checkSizes left
+          and r = checkSizes right
+
+          val () = if l + 1 + r = size then () else raise Bug "wrong size"
+        in
+          size
+        end;
+
+  fun checkSorted compareKey x tree =
+      case tree of
+        E => x
+      | T (Node {left,key,right,...}) =>
+        let
+          val x = checkSorted compareKey x left
+
+          val () =
+              case x of
+                NONE => ()
+              | SOME k =>
+                case compareKey (k,key) of
+                  LESS => ()
+                | EQUAL => raise Bug "duplicate keys"
+                | GREATER => raise Bug "unsorted"
+
+          val x = SOME key
+        in
+          checkSorted compareKey x right
+        end;
+
+  fun checkPriorities compareKey tree =
+      case tree of
+        E => NONE
+      | T node =>
+        let
+          val Node {left,right,...} = node
+
+          val () =
+              case checkPriorities compareKey left of
+                NONE => ()
+              | SOME lnode =>
+                if not (lowerPriorityNode node lnode) then ()
+                else raise Bug "left child has greater priority"
+
+          val () =
+              case checkPriorities compareKey right of
+                NONE => ()
+              | SOME rnode =>
+                if not (lowerPriorityNode node rnode) then ()
+                else raise Bug "right child has greater priority"
+        in
+          SOME node
+        end;
+in
+  fun treeCheckInvariants compareKey tree =
+      let
+        val _ = checkSizes tree
+
+        val _ = checkSorted compareKey NONE tree
+
+        val _ = checkPriorities compareKey tree
+      in
+        tree
+      end
+      handle Error err => raise Bug err;
+end;
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Tree operations.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeNew () = E;
+
+fun nodeSize (Node {size = x, ...}) = x;
+
+fun treeSize tree =
+    case tree of
+      E => 0
+    | T x => nodeSize x;
+
+fun mkNode priority left key value right =
+    let
+      val size = treeSize left + 1 + treeSize right
+    in
+      Node
+        {size = size,
+         priority = priority,
+         left = left,
+         key = key,
+         value = value,
+         right = right}
+    end;
+
+fun mkTree priority left key value right =
+    let
+      val node = mkNode priority left key value right
+    in
+      T node
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Extracting the left and right spines of a tree.                           *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeLeftSpine acc tree =
+    case tree of
+      E => acc
+    | T node => nodeLeftSpine acc node
+
+and nodeLeftSpine acc node =
+    let
+      val Node {left,...} = node
+    in
+      treeLeftSpine (node :: acc) left
+    end;
+
+fun treeRightSpine acc tree =
+    case tree of
+      E => acc
+    | T node => nodeRightSpine acc node
+
+and nodeRightSpine acc node =
+    let
+      val Node {right,...} = node
+    in
+      treeRightSpine (node :: acc) right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Singleton trees.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkNodeSingleton priority key value =
+    let
+      val size = 1
+      and left = E
+      and right = E
+    in
+      Node
+        {size = size,
+         priority = priority,
+         left = left,
+         key = key,
+         value = value,
+         right = right}
+    end;
+
+fun nodeSingleton (key,value) =
+    let
+      val priority = randomPriority ()
+    in
+      mkNodeSingleton priority key value
+    end;
+
+fun treeSingleton key_value =
+    let
+      val node = nodeSingleton key_value
+    in
+      T node
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Appending two trees, where every element of the first tree is less than   *)
+(* every element of the second tree.                                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeAppend tree1 tree2 =
+    case tree1 of
+      E => tree2
+    | T node1 =>
+      case tree2 of
+        E => tree1
+      | T node2 =>
+        if lowerPriorityNode node1 node2 then
+          let
+            val Node {priority,left,key,value,right,...} = node2
+
+            val left = treeAppend tree1 left
+          in
+            mkTree priority left key value right
+          end
+        else
+          let
+            val Node {priority,left,key,value,right,...} = node1
+
+            val right = treeAppend right tree2
+          in
+            mkTree priority left key value right
+          end;
+
+(* ------------------------------------------------------------------------- *)
+(* Appending two trees and a node, where every element of the first tree is  *)
+(* less than the node, which in turn is less than every element of the       *)
+(* second tree.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeCombine left node right =
+    let
+      val left_node = treeAppend left (T node)
+    in
+      treeAppend left_node right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching a tree for a value.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun treePeek compareKey pkey tree =
+    case tree of
+      E => NONE
+    | T node => nodePeek compareKey pkey node
+
+and nodePeek compareKey pkey node =
+    let
+      val Node {left,key,value,right,...} = node
+    in
+      case compareKey (pkey,key) of
+        LESS => treePeek compareKey pkey left
+      | EQUAL => SOME value
+      | GREATER => treePeek compareKey pkey right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Tree paths.                                                               *)
+(* ------------------------------------------------------------------------- *)
+
+(* Generating a path by searching a tree for a key/value pair *)
+
+fun treePeekPath compareKey pkey path tree =
+    case tree of
+      E => (path,NONE)
+    | T node => nodePeekPath compareKey pkey path node
+
+and nodePeekPath compareKey pkey path node =
+    let
+      val Node {left,key,right,...} = node
+    in
+      case compareKey (pkey,key) of
+        LESS => treePeekPath compareKey pkey ((true,node) :: path) left
+      | EQUAL => (path, SOME node)
+      | GREATER => treePeekPath compareKey pkey ((false,node) :: path) right
+    end;
+
+(* A path splits a tree into left/right components *)
+
+fun addSidePath ((wentLeft,node),(leftTree,rightTree)) =
+    let
+      val Node {priority,left,key,value,right,...} = node
+    in
+      if wentLeft then (leftTree, mkTree priority rightTree key value right)
+      else (mkTree priority left key value leftTree, rightTree)
+    end;
+
+fun addSidesPath left_right = List.foldl addSidePath left_right;
+
+fun mkSidesPath path = addSidesPath (E,E) path;
+
+(* Updating the subtree at a path *)
+
+local
+  fun updateTree ((wentLeft,node),tree) =
+      let
+        val Node {priority,left,key,value,right,...} = node
+      in
+        if wentLeft then mkTree priority tree key value right
+        else mkTree priority left key value tree
+      end;
+in
+  fun updateTreePath tree = List.foldl updateTree tree;
+end;
+
+(* Inserting a new node at a path position *)
+
+fun insertNodePath node =
+    let
+      fun insert left_right path =
+          case path of
+            [] =>
+            let
+              val (left,right) = left_right
+            in
+              treeCombine left node right
+            end
+          | (step as (_,snode)) :: rest =>
+            if lowerPriorityNode snode node then
+              let
+                val left_right = addSidePath (step,left_right)
+              in
+                insert left_right rest
+              end
+            else
+              let
+                val (left,right) = left_right
+
+                val tree = treeCombine left node right
+              in
+                updateTreePath tree path
+              end
+    in
+      insert (E,E)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Using a key to split a node into three components: the keys comparing     *)
+(* less than the supplied key, an optional equal key, and the keys comparing *)
+(* greater.                                                                  *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodePartition compareKey pkey node =
+    let
+      val (path,pnode) = nodePeekPath compareKey pkey [] node
+    in
+      case pnode of
+        NONE =>
+        let
+          val (left,right) = mkSidesPath path
+        in
+          (left,NONE,right)
+        end
+      | SOME node =>
+        let
+          val Node {left,key,value,right,...} = node
+
+          val (left,right) = addSidesPath (left,right) path
+        in
+          (left, SOME (key,value), right)
+        end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching a tree for a key/value pair.                                    *)
+(* ------------------------------------------------------------------------- *)
+
+fun treePeekKey compareKey pkey tree =
+    case tree of
+      E => NONE
+    | T node => nodePeekKey compareKey pkey node
+
+and nodePeekKey compareKey pkey node =
+    let
+      val Node {left,key,value,right,...} = node
+    in
+      case compareKey (pkey,key) of
+        LESS => treePeekKey compareKey pkey left
+      | EQUAL => SOME (key,value)
+      | GREATER => treePeekKey compareKey pkey right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Inserting new key/values into the tree.                                   *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeInsert compareKey key_value tree =
+    let
+      val (key,value) = key_value
+
+      val (path,inode) = treePeekPath compareKey key [] tree
+    in
+      case inode of
+        NONE =>
+        let
+          val node = nodeSingleton (key,value)
+        in
+          insertNodePath node path
+        end
+      | SOME node =>
+        let
+          val Node {size,priority,left,right,...} = node
+
+          val node =
+              Node
+                {size = size,
+                 priority = priority,
+                 left = left,
+                 key = key,
+                 value = value,
+                 right = right}
+        in
+          updateTreePath (T node) path
+        end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Deleting key/value pairs: it raises an exception if the supplied key is   *)
+(* not present.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDelete compareKey dkey tree =
+    case tree of
+      E => raise Bug "Map.delete: element not found"
+    | T node => nodeDelete compareKey dkey node
+
+and nodeDelete compareKey dkey node =
+    let
+      val Node {size,priority,left,key,value,right} = node
+    in
+      case compareKey (dkey,key) of
+        LESS =>
+        let
+          val size = size - 1
+          and left = treeDelete compareKey dkey left
+
+          val node =
+              Node
+                {size = size,
+                 priority = priority,
+                 left = left,
+                 key = key,
+                 value = value,
+                 right = right}
+        in
+          T node
+        end
+      | EQUAL => treeAppend left right
+      | GREATER =>
+        let
+          val size = size - 1
+          and right = treeDelete compareKey dkey right
+
+          val node =
+              Node
+                {size = size,
+                 priority = priority,
+                 left = left,
+                 key = key,
+                 value = value,
+                 right = right}
+        in
+          T node
+        end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Partial map is the basic operation for preserving tree structure.         *)
+(* It applies its argument function to the elements *in order*.              *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMapPartial f tree =
+    case tree of
+      E => E
+    | T node => nodeMapPartial f node
+
+and nodeMapPartial f (Node {priority,left,key,value,right,...}) =
+    let
+      val left = treeMapPartial f left
+      and vo = f (key,value)
+      and right = treeMapPartial f right
+    in
+      case vo of
+        NONE => treeAppend left right
+      | SOME value => mkTree priority left key value right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping tree values.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMap f tree =
+    case tree of
+      E => E
+    | T node => T (nodeMap f node)
+
+and nodeMap f node =
+    let
+      val Node {size,priority,left,key,value,right} = node
+
+      val left = treeMap f left
+      and value = f (key,value)
+      and right = treeMap f right
+    in
+      Node
+        {size = size,
+         priority = priority,
+         left = left,
+         key = key,
+         value = value,
+         right = right}
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Merge is the basic operation for joining two trees. Note that the merged  *)
+(* key is always the one from the second map.                                *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMerge compareKey f1 f2 fb tree1 tree2 =
+    case tree1 of
+      E => treeMapPartial f2 tree2
+    | T node1 =>
+      case tree2 of
+        E => treeMapPartial f1 tree1
+      | T node2 => nodeMerge compareKey f1 f2 fb node1 node2
+
+and nodeMerge compareKey f1 f2 fb node1 node2 =
+    let
+      val Node {priority,left,key,value,right,...} = node2
+
+      val (l,kvo,r) = nodePartition compareKey key node1
+
+      val left = treeMerge compareKey f1 f2 fb l left
+      and right = treeMerge compareKey f1 f2 fb r right
+
+      val vo =
+          case kvo of
+            NONE => f2 (key,value)
+          | SOME kv => fb (kv,(key,value))
+    in
+      case vo of
+        NONE => treeAppend left right
+      | SOME value =>
+        let
+          val node = mkNodeSingleton priority key value
+        in
+          treeCombine left node right
+        end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* A union operation on trees.                                               *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeUnion compareKey f f2 tree1 tree2 =
+    case tree1 of
+      E => tree2
+    | T node1 =>
+      case tree2 of
+        E => tree1
+      | T node2 => nodeUnion compareKey f f2 node1 node2
+
+and nodeUnion compareKey f f2 node1 node2 =
+    if pointerEqual (node1,node2) then nodeMapPartial f2 node1
+    else
+      let
+        val Node {priority,left,key,value,right,...} = node2
+
+        val (l,kvo,r) = nodePartition compareKey key node1
+
+        val left = treeUnion compareKey f f2 l left
+        and right = treeUnion compareKey f f2 r right
+
+        val vo =
+            case kvo of
+              NONE => SOME value
+            | SOME kv => f (kv,(key,value))
+      in
+        case vo of
+          NONE => treeAppend left right
+        | SOME value =>
+          let
+            val node = mkNodeSingleton priority key value
+          in
+            treeCombine left node right
+          end
+      end;
+
+(* ------------------------------------------------------------------------- *)
+(* An intersect operation on trees.                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeIntersect compareKey f t1 t2 =
+    case t1 of
+      E => E
+    | T n1 =>
+      case t2 of
+        E => E
+      | T n2 => nodeIntersect compareKey f n1 n2
+
+and nodeIntersect compareKey f n1 n2 =
+    let
+      val Node {priority,left,key,value,right,...} = n2
+
+      val (l,kvo,r) = nodePartition compareKey key n1
+
+      val left = treeIntersect compareKey f l left
+      and right = treeIntersect compareKey f r right
+
+      val vo =
+          case kvo of
+            NONE => NONE
+          | SOME kv => f (kv,(key,value))
+    in
+      case vo of
+        NONE => treeAppend left right
+      | SOME value => mkTree priority left key value right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* A union operation on trees which simply chooses the second value.         *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeUnionDomain compareKey tree1 tree2 =
+    case tree1 of
+      E => tree2
+    | T node1 =>
+      case tree2 of
+        E => tree1
+      | T node2 =>
+        if pointerEqual (node1,node2) then tree2
+        else nodeUnionDomain compareKey node1 node2
+
+and nodeUnionDomain compareKey node1 node2 =
+    let
+      val Node {priority,left,key,value,right,...} = node2
+
+      val (l,_,r) = nodePartition compareKey key node1
+
+      val left = treeUnionDomain compareKey l left
+      and right = treeUnionDomain compareKey r right
+
+      val node = mkNodeSingleton priority key value
+    in
+      treeCombine left node right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* An intersect operation on trees which simply chooses the second value.    *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeIntersectDomain compareKey tree1 tree2 =
+    case tree1 of
+      E => E
+    | T node1 =>
+      case tree2 of
+        E => E
+      | T node2 =>
+        if pointerEqual (node1,node2) then tree2
+        else nodeIntersectDomain compareKey node1 node2
+
+and nodeIntersectDomain compareKey node1 node2 =
+    let
+      val Node {priority,left,key,value,right,...} = node2
+
+      val (l,kvo,r) = nodePartition compareKey key node1
+
+      val left = treeIntersectDomain compareKey l left
+      and right = treeIntersectDomain compareKey r right
+    in
+      if Option.isSome kvo then mkTree priority left key value right
+      else treeAppend left right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* A difference operation on trees.                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDifferenceDomain compareKey t1 t2 =
+    case t1 of
+      E => E
+    | T n1 =>
+      case t2 of
+        E => t1
+      | T n2 => nodeDifferenceDomain compareKey n1 n2
+
+and nodeDifferenceDomain compareKey n1 n2 =
+    if pointerEqual (n1,n2) then E
+    else
+      let
+        val Node {priority,left,key,value,right,...} = n1
+
+        val (l,kvo,r) = nodePartition compareKey key n2
+
+        val left = treeDifferenceDomain compareKey left l
+        and right = treeDifferenceDomain compareKey right r
+      in
+        if Option.isSome kvo then treeAppend left right
+        else mkTree priority left key value right
+      end;
+
+(* ------------------------------------------------------------------------- *)
+(* A subset operation on trees.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeSubsetDomain compareKey tree1 tree2 =
+    case tree1 of
+      E => true
+    | T node1 =>
+      case tree2 of
+        E => false
+      | T node2 => nodeSubsetDomain compareKey node1 node2
+
+and nodeSubsetDomain compareKey node1 node2 =
+    pointerEqual (node1,node2) orelse
+    let
+      val Node {size,left,key,right,...} = node1
+    in
+      size <= nodeSize node2 andalso
+      let
+        val (l,kvo,r) = nodePartition compareKey key node2
+      in
+        Option.isSome kvo andalso
+        treeSubsetDomain compareKey left l andalso
+        treeSubsetDomain compareKey right r
+      end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Picking an arbitrary key/value pair from a tree.                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodePick node =
+    let
+      val Node {key,value,...} = node
+    in
+      (key,value)
+    end;
+
+fun treePick tree =
+    case tree of
+      E => raise Bug "Map.treePick"
+    | T node => nodePick node;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing an arbitrary key/value pair from a tree.                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodeDeletePick node =
+    let
+      val Node {left,key,value,right,...} = node
+    in
+      ((key,value), treeAppend left right)
+    end;
+
+fun treeDeletePick tree =
+    case tree of
+      E => raise Bug "Map.treeDeletePick"
+    | T node => nodeDeletePick node;
+
+(* ------------------------------------------------------------------------- *)
+(* Finding the nth smallest key/value (counting from 0).                     *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeNth n tree =
+    case tree of
+      E => raise Bug "Map.treeNth"
+    | T node => nodeNth n node
+
+and nodeNth n node =
+    let
+      val Node {left,key,value,right,...} = node
+
+      val k = treeSize left
+    in
+      if n = k then (key,value)
+      else if n < k then treeNth n left
+      else treeNth (n - (k + 1)) right
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing the nth smallest key/value (counting from 0).                    *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDeleteNth n tree =
+    case tree of
+      E => raise Bug "Map.treeDeleteNth"
+    | T node => nodeDeleteNth n node
+
+and nodeDeleteNth n node =
+    let
+      val Node {size,priority,left,key,value,right} = node
+
+      val k = treeSize left
+    in
+      if n = k then ((key,value), treeAppend left right)
+      else if n < k then
+        let
+          val (key_value,left) = treeDeleteNth n left
+
+          val size = size - 1
+
+          val node =
+              Node
+                {size = size,
+                 priority = priority,
+                 left = left,
+                 key = key,
+                 value = value,
+                 right = right}
+        in
+          (key_value, T node)
+        end
+      else
+        let
+          val n = n - (k + 1)
+
+          val (key_value,right) = treeDeleteNth n right
+
+          val size = size - 1
+
+          val node =
+              Node
+                {size = size,
+                 priority = priority,
+                 left = left,
+                 key = key,
+                 value = value,
+                 right = right}
+        in
+          (key_value, T node)
+        end
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ('key,'value) iterator =
+    LR of ('key * 'value) * ('key,'value) tree * ('key,'value) node list
+  | RL of ('key * 'value) * ('key,'value) tree * ('key,'value) node list;
+
+fun fromSpineLR nodes =
+    case nodes of
+      [] => NONE
+    | Node {key,value,right,...} :: nodes =>
+      SOME (LR ((key,value),right,nodes));
+
+fun fromSpineRL nodes =
+    case nodes of
+      [] => NONE
+    | Node {key,value,left,...} :: nodes =>
+      SOME (RL ((key,value),left,nodes));
+
+fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
+
+fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
+
+fun treeMkIterator tree = addLR [] tree;
+
+fun treeMkRevIterator tree = addRL [] tree;
+
+fun readIterator iter =
+    case iter of
+      LR (key_value,_,_) => key_value
+    | RL (key_value,_,_) => key_value;
+
+fun advanceIterator iter =
+    case iter of
+      LR (_,tree,nodes) => addLR nodes tree
+    | RL (_,tree,nodes) => addRL nodes tree;
+
+fun foldIterator f acc io =
+    case io of
+      NONE => acc
+    | SOME iter =>
+      let
+        val (key,value) = readIterator iter
+      in
+        foldIterator f (f (key,value,acc)) (advanceIterator iter)
+      end;
+
+fun findIterator pred io =
+    case io of
+      NONE => NONE
+    | SOME iter =>
+      let
+        val key_value = readIterator iter
+      in
+        if pred key_value then SOME key_value
+        else findIterator pred (advanceIterator iter)
+      end;
+
+fun firstIterator f io =
+    case io of
+      NONE => NONE
+    | SOME iter =>
+      let
+        val key_value = readIterator iter
+      in
+        case f key_value of
+          NONE => firstIterator f (advanceIterator iter)
+        | s => s
+      end;
+
+fun compareIterator compareKey compareValue io1 io2 =
+    case (io1,io2) of
+      (NONE,NONE) => EQUAL
+    | (NONE, SOME _) => LESS
+    | (SOME _, NONE) => GREATER
+    | (SOME i1, SOME i2) =>
+      let
+        val (k1,v1) = readIterator i1
+        and (k2,v2) = readIterator i2
+      in
+        case compareKey (k1,k2) of
+          LESS => LESS
+        | EQUAL =>
+          (case compareValue (v1,v2) of
+             LESS => LESS
+           | EQUAL =>
+             let
+               val io1 = advanceIterator i1
+               and io2 = advanceIterator i2
+             in
+               compareIterator compareKey compareValue io1 io2
+             end
+           | GREATER => GREATER)
+        | GREATER => GREATER
+      end;
+
+fun equalIterator equalKey equalValue io1 io2 =
+    case (io1,io2) of
+      (NONE,NONE) => true
+    | (NONE, SOME _) => false
+    | (SOME _, NONE) => false
+    | (SOME i1, SOME i2) =>
+      let
+        val (k1,v1) = readIterator i1
+        and (k2,v2) = readIterator i2
+      in
+        equalKey k1 k2 andalso
+        equalValue v1 v2 andalso
+        let
+          val io1 = advanceIterator i1
+          and io2 = advanceIterator i2
+        in
+          equalIterator equalKey equalValue io1 io2
+        end
+      end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite maps.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ('key,'value) map =
+    Map of ('key * 'key -> order) * ('key,'value) tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Map debugging functions.                                                  *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+fun checkInvariants s m =
+    let
+      val Map (compareKey,tree) = m
+
+      val _ = treeCheckInvariants compareKey tree
+    in
+      m
+    end
+    handle Bug bug => raise Bug (s ^ "\n" ^ "Map.checkInvariants: " ^ bug);
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors.                                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun new compareKey =
+    let
+      val tree = treeNew ()
+    in
+      Map (compareKey,tree)
+    end;
+
+fun singleton compareKey key_value =
+    let
+      val tree = treeSingleton key_value
+    in
+      Map (compareKey,tree)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Map size.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun size (Map (_,tree)) = treeSize tree;
+
+fun null m = size m = 0;
+
+(* ------------------------------------------------------------------------- *)
+(* Querying.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun peekKey (Map (compareKey,tree)) key = treePeekKey compareKey key tree;
+
+fun peek (Map (compareKey,tree)) key = treePeek compareKey key tree;
+
+fun inDomain key m = Option.isSome (peek m key);
+
+fun get m key =
+    case peek m key of
+      NONE => raise Error "Map.get: element not found"
+    | SOME value => value;
+
+fun pick (Map (_,tree)) = treePick tree;
+
+fun nth (Map (_,tree)) n = treeNth n tree;
+
+fun random m =
+    let
+      val n = size m
+    in
+      if n = 0 then raise Bug "Map.random: empty"
+      else nth m (randomInt n)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Adding.                                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+fun insert (Map (compareKey,tree)) key_value =
+    let
+      val tree = treeInsert compareKey key_value tree
+    in
+      Map (compareKey,tree)
+    end;
+
+(*BasicDebug
+val insert = fn m => fn kv =>
+    checkInvariants "Map.insert: result"
+      (insert (checkInvariants "Map.insert: input" m) kv);
+*)
+
+fun insertList m =
+    let
+      fun ins (key_value,acc) = insert acc key_value
+    in
+      List.foldl ins m
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing.                                                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun delete (Map (compareKey,tree)) dkey =
+    let
+      val tree = treeDelete compareKey dkey tree
+    in
+      Map (compareKey,tree)
+    end;
+
+(*BasicDebug
+val delete = fn m => fn k =>
+    checkInvariants "Map.delete: result"
+      (delete (checkInvariants "Map.delete: input" m) k);
+*)
+
+fun remove m key = if inDomain key m then delete m key else m;
+
+fun deletePick (Map (compareKey,tree)) =
+    let
+      val (key_value,tree) = treeDeletePick tree
+    in
+      (key_value, Map (compareKey,tree))
+    end;
+
+(*BasicDebug
+val deletePick = fn m =>
+    let
+      val (kv,m) = deletePick (checkInvariants "Map.deletePick: input" m)
+    in
+      (kv, checkInvariants "Map.deletePick: result" m)
+    end;
+*)
+
+fun deleteNth (Map (compareKey,tree)) n =
+    let
+      val (key_value,tree) = treeDeleteNth n tree
+    in
+      (key_value, Map (compareKey,tree))
+    end;
+
+(*BasicDebug
+val deleteNth = fn m => fn n =>
+    let
+      val (kv,m) = deleteNth (checkInvariants "Map.deleteNth: input" m) n
+    in
+      (kv, checkInvariants "Map.deleteNth: result" m)
+    end;
+*)
+
+fun deleteRandom m =
+    let
+      val n = size m
+    in
+      if n = 0 then raise Bug "Map.deleteRandom: empty"
+      else deleteNth m (randomInt n)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Joining (all join operations prefer keys in the second map).              *)
+(* ------------------------------------------------------------------------- *)
+
+fun merge {first,second,both} (Map (compareKey,tree1)) (Map (_,tree2)) =
+    let
+      val tree = treeMerge compareKey first second both tree1 tree2
+    in
+      Map (compareKey,tree)
+    end;
+
+(*BasicDebug
+val merge = fn f => fn m1 => fn m2 =>
+    checkInvariants "Map.merge: result"
+      (merge f
+         (checkInvariants "Map.merge: input 1" m1)
+         (checkInvariants "Map.merge: input 2" m2));
+*)
+
+fun union f (Map (compareKey,tree1)) (Map (_,tree2)) =
+    let
+      fun f2 kv = f (kv,kv)
+
+      val tree = treeUnion compareKey f f2 tree1 tree2
+    in
+      Map (compareKey,tree)
+    end;
+
+(*BasicDebug
+val union = fn f => fn m1 => fn m2 =>
+    checkInvariants "Map.union: result"
+      (union f
+         (checkInvariants "Map.union: input 1" m1)
+         (checkInvariants "Map.union: input 2" m2));
+*)
+
+fun intersect f (Map (compareKey,tree1)) (Map (_,tree2)) =
+    let
+      val tree = treeIntersect compareKey f tree1 tree2
+    in
+      Map (compareKey,tree)
+    end;
+
+(*BasicDebug
+val intersect = fn f => fn m1 => fn m2 =>
+    checkInvariants "Map.intersect: result"
+      (intersect f
+         (checkInvariants "Map.intersect: input 1" m1)
+         (checkInvariants "Map.intersect: input 2" m2));
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over maps.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkIterator (Map (_,tree)) = treeMkIterator tree;
+
+fun mkRevIterator (Map (_,tree)) = treeMkRevIterator tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+fun mapPartial f (Map (compareKey,tree)) =
+    let
+      val tree = treeMapPartial f tree
+    in
+      Map (compareKey,tree)
+    end;
+
+(*BasicDebug
+val mapPartial = fn f => fn m =>
+    checkInvariants "Map.mapPartial: result"
+      (mapPartial f (checkInvariants "Map.mapPartial: input" m));
+*)
+
+fun map f (Map (compareKey,tree)) =
+    let
+      val tree = treeMap f tree
+    in
+      Map (compareKey,tree)
+    end;
+
+(*BasicDebug
+val map = fn f => fn m =>
+    checkInvariants "Map.map: result"
+      (map f (checkInvariants "Map.map: input" m));
+*)
+
+fun transform f = map (fn (_,value) => f value);
+
+fun filter pred =
+    let
+      fun f (key_value as (_,value)) =
+          if pred key_value then SOME value else NONE
+    in
+      mapPartial f
+    end;
+
+fun partition p =
+    let
+      fun np x = not (p x)
+    in
+      fn m => (filter p m, filter np m)
+    end;
+
+fun foldl f b m = foldIterator f b (mkIterator m);
+
+fun foldr f b m = foldIterator f b (mkRevIterator m);
+
+fun app f m = foldl (fn (key,value,()) => f (key,value)) () m;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+fun findl p m = findIterator p (mkIterator m);
+
+fun findr p m = findIterator p (mkRevIterator m);
+
+fun firstl f m = firstIterator f (mkIterator m);
+
+fun firstr f m = firstIterator f (mkRevIterator m);
+
+fun exists p m = Option.isSome (findl p m);
+
+fun all p =
+    let
+      fun np x = not (p x)
+    in
+      fn m => not (exists np m)
+    end;
+
+fun count pred =
+    let
+      fun f (k,v,acc) = if pred (k,v) then acc + 1 else acc
+    in
+      foldl f 0
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare compareValue (m1,m2) =
+    if pointerEqual (m1,m2) then EQUAL
+    else
+      case Int.compare (size m1, size m2) of
+        LESS => LESS
+      | EQUAL =>
+        let
+          val Map (compareKey,_) = m1
+
+          val io1 = mkIterator m1
+          and io2 = mkIterator m2
+        in
+          compareIterator compareKey compareValue io1 io2
+        end
+      | GREATER => GREATER;
+
+fun equal equalValue m1 m2 =
+    pointerEqual (m1,m2) orelse
+    (size m1 = size m2 andalso
+     let
+       val Map (compareKey,_) = m1
+
+       val io1 = mkIterator m1
+       and io2 = mkIterator m2
+     in
+       equalIterator (equalKey compareKey) equalValue io1 io2
+     end);
+
+(* ------------------------------------------------------------------------- *)
+(* Set operations on the domain.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun unionDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+    let
+      val tree = treeUnionDomain compareKey tree1 tree2
+    in
+      Map (compareKey,tree)
+    end;
+
+(*BasicDebug
+val unionDomain = fn m1 => fn m2 =>
+    checkInvariants "Map.unionDomain: result"
+      (unionDomain
+         (checkInvariants "Map.unionDomain: input 1" m1)
+         (checkInvariants "Map.unionDomain: input 2" m2));
+*)
+
+local
+  fun uncurriedUnionDomain (m,acc) = unionDomain acc m;
+in
+  fun unionListDomain ms =
+      case ms of
+        [] => raise Bug "Map.unionListDomain: no sets"
+      | m :: ms => List.foldl uncurriedUnionDomain m ms;
+end;
+
+fun intersectDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+    let
+      val tree = treeIntersectDomain compareKey tree1 tree2
+    in
+      Map (compareKey,tree)
+    end;
+
+(*BasicDebug
+val intersectDomain = fn m1 => fn m2 =>
+    checkInvariants "Map.intersectDomain: result"
+      (intersectDomain
+         (checkInvariants "Map.intersectDomain: input 1" m1)
+         (checkInvariants "Map.intersectDomain: input 2" m2));
+*)
+
+local
+  fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m;
+in
+  fun intersectListDomain ms =
+      case ms of
+        [] => raise Bug "Map.intersectListDomain: no sets"
+      | m :: ms => List.foldl uncurriedIntersectDomain m ms;
+end;
+
+fun differenceDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+    let
+      val tree = treeDifferenceDomain compareKey tree1 tree2
+    in
+      Map (compareKey,tree)
+    end;
+
+(*BasicDebug
+val differenceDomain = fn m1 => fn m2 =>
+    checkInvariants "Map.differenceDomain: result"
+      (differenceDomain
+         (checkInvariants "Map.differenceDomain: input 1" m1)
+         (checkInvariants "Map.differenceDomain: input 2" m2));
+*)
+
+fun symmetricDifferenceDomain m1 m2 =
+    unionDomain (differenceDomain m1 m2) (differenceDomain m2 m1);
+
+fun equalDomain m1 m2 = equal (K (K true)) m1 m2;
+
+fun subsetDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+    treeSubsetDomain compareKey tree1 tree2;
+
+fun disjointDomain m1 m2 = null (intersectDomain m1 m2);
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun keys m = foldr (fn (key,_,l) => key :: l) [] m;
+
+fun values m = foldr (fn (_,value,l) => value :: l) [] m;
+
+fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
+
+fun fromList compareKey l =
+    let
+      val m = new compareKey
+    in
+      insertList m l
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Model.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,277 @@
+(* ========================================================================= *)
+(* RANDOM FINITE MODELS                                                      *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+signature Model =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* Model size.                                                               *)
+(* ------------------------------------------------------------------------- *)
+
+type size = {size : int}
+
+(* ------------------------------------------------------------------------- *)
+(* A model of size N has integer elements 0...N-1.                           *)
+(* ------------------------------------------------------------------------- *)
+
+type element = int
+
+val zeroElement : element
+
+val incrementElement : size -> element -> element option
+
+(* ------------------------------------------------------------------------- *)
+(* The parts of the model that are fixed.                                    *)
+(* ------------------------------------------------------------------------- *)
+
+type fixedFunction = size -> element list -> element option
+
+type fixedRelation = size -> element list -> bool option
+
+datatype fixed =
+    Fixed of
+      {functions : fixedFunction NameArityMap.map,
+       relations : fixedRelation NameArityMap.map}
+
+val emptyFixed : fixed
+
+val unionFixed : fixed -> fixed -> fixed
+
+val getFunctionFixed : fixed -> NameArity.nameArity -> fixedFunction
+
+val getRelationFixed : fixed -> NameArity.nameArity -> fixedRelation
+
+val insertFunctionFixed : fixed -> NameArity.nameArity * fixedFunction -> fixed
+
+val insertRelationFixed : fixed -> NameArity.nameArity * fixedRelation -> fixed
+
+val unionListFixed : fixed list -> fixed
+
+val basicFixed : fixed  (* interprets equality and hasType *)
+
+(* ------------------------------------------------------------------------- *)
+(* Renaming fixed model parts.                                               *)
+(* ------------------------------------------------------------------------- *)
+
+type fixedMap =
+     {functionMap : Name.name NameArityMap.map,
+      relationMap : Name.name NameArityMap.map}
+
+val mapFixed : fixedMap -> fixed -> fixed
+
+val ppFixedMap : fixedMap Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* Standard fixed model parts.                                               *)
+(* ------------------------------------------------------------------------- *)
+
+(* Projections *)
+
+val projectionMin : int
+
+val projectionMax : int
+
+val projectionName : int -> Name.name
+
+val projectionFixed : fixed
+
+(* Arithmetic *)
+
+val numeralMin : int
+
+val numeralMax : int
+
+val numeralName : int -> Name.name
+
+val addName : Name.name
+
+val divName : Name.name
+
+val dividesName : Name.name
+
+val evenName : Name.name
+
+val expName : Name.name
+
+val geName : Name.name
+
+val gtName : Name.name
+
+val isZeroName : Name.name
+
+val leName : Name.name
+
+val ltName : Name.name
+
+val modName : Name.name
+
+val multName : Name.name
+
+val negName : Name.name
+
+val oddName : Name.name
+
+val preName : Name.name
+
+val subName : Name.name
+
+val sucName : Name.name
+
+val modularFixed : fixed
+
+val overflowFixed : fixed
+
+(* Sets *)
+
+val cardName : Name.name
+
+val complementName : Name.name
+
+val differenceName : Name.name
+
+val emptyName : Name.name
+
+val memberName : Name.name
+
+val insertName : Name.name
+
+val intersectName : Name.name
+
+val singletonName : Name.name
+
+val subsetName : Name.name
+
+val symmetricDifferenceName : Name.name
+
+val unionName : Name.name
+
+val universeName : Name.name
+
+val setFixed : fixed
+
+(* Lists *)
+
+val appendName : Name.name
+
+val consName : Name.name
+
+val lengthName : Name.name
+
+val nilName : Name.name
+
+val nullName : Name.name
+
+val tailName : Name.name
+
+val listFixed : fixed
+
+(* ------------------------------------------------------------------------- *)
+(* Valuations.                                                               *)
+(* ------------------------------------------------------------------------- *)
+
+type valuation
+
+val emptyValuation : valuation
+
+val zeroValuation : NameSet.set -> valuation
+
+val constantValuation : element -> NameSet.set -> valuation
+
+val peekValuation : valuation -> Name.name -> element option
+
+val getValuation : valuation -> Name.name -> element
+
+val insertValuation : valuation -> Name.name * element -> valuation
+
+val randomValuation : {size : int} -> NameSet.set -> valuation
+
+val incrementValuation :
+    {size : int} -> NameSet.set -> valuation -> valuation option
+
+val foldValuation :
+    {size : int} -> NameSet.set -> (valuation * 'a -> 'a) -> 'a -> 'a
+
+(* ------------------------------------------------------------------------- *)
+(* A type of random finite models.                                           *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = {size : int, fixed : fixed}
+
+type model
+
+val default : parameters
+
+val new : parameters -> model
+
+val size : model -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Interpreting terms and formulas in the model.                             *)
+(* ------------------------------------------------------------------------- *)
+
+val interpretFunction : model -> Term.functionName * element list -> element
+
+val interpretRelation : model -> Atom.relationName * element list -> bool
+
+val interpretTerm : model -> valuation -> Term.term -> element
+
+val interpretAtom : model -> valuation -> Atom.atom -> bool
+
+val interpretFormula : model -> valuation -> Formula.formula -> bool
+
+val interpretLiteral : model -> valuation -> Literal.literal -> bool
+
+val interpretClause : model -> valuation -> Thm.clause -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Check whether random groundings of a formula are true in the model.       *)
+(* Note: if it's cheaper, a systematic check will be performed instead.      *)
+(* ------------------------------------------------------------------------- *)
+
+val check :
+    (model -> valuation -> 'a -> bool) -> {maxChecks : int option} -> model ->
+    NameSet.set -> 'a -> {T : int, F : int}
+
+val checkAtom :
+    {maxChecks : int option} -> model -> Atom.atom -> {T : int, F : int}
+
+val checkFormula :
+    {maxChecks : int option} -> model -> Formula.formula -> {T : int, F : int}
+
+val checkLiteral :
+    {maxChecks : int option} -> model -> Literal.literal -> {T : int, F : int}
+
+val checkClause :
+    {maxChecks : int option} -> model -> Thm.clause -> {T : int, F : int}
+
+(* ------------------------------------------------------------------------- *)
+(* Updating the model.                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+val updateFunction :
+    model -> (Term.functionName * element list) * element -> unit
+
+val updateRelation :
+    model -> (Atom.relationName * element list) * bool -> unit
+
+(* ------------------------------------------------------------------------- *)
+(* Choosing a random perturbation to make a formula true in the model.       *)
+(* ------------------------------------------------------------------------- *)
+
+val perturbTerm : model -> valuation -> Term.term * element list -> unit
+
+val perturbAtom : model -> valuation -> Atom.atom * bool -> unit
+
+val perturbLiteral : model -> valuation -> Literal.literal -> unit
+
+val perturbClause : model -> valuation -> Thm.clause -> unit
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : model Print.pp
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Model.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,1278 @@
+(* ========================================================================= *)
+(* RANDOM FINITE MODELS                                                      *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+structure Model :> Model =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Constants.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val maxSpace = 1000;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val multInt =
+    case Int.maxInt of
+      NONE => (fn x => fn y => SOME (x * y))
+    | SOME m =>
+      let
+        val m = Real.floor (Math.sqrt (Real.fromInt m))
+      in
+        fn x => fn y => if x <= m andalso y <= m then SOME (x * y) else NONE
+      end;
+
+local
+  fun iexp x y acc =
+      if y mod 2 = 0 then iexp' x y acc
+      else
+        case multInt acc x of
+          SOME acc => iexp' x y acc
+        | NONE => NONE
+
+  and iexp' x y acc =
+      if y = 1 then SOME acc
+      else
+        let
+          val y = y div 2
+        in
+          case multInt x x of
+            SOME x => iexp x y acc
+          | NONE => NONE
+        end;
+in
+  fun expInt x y =
+      if y <= 1 then
+        if y = 0 then SOME 1
+        else if y = 1 then SOME x
+        else raise Bug "expInt: negative exponent"
+      else if x <= 1 then
+        if 0 <= x then SOME x
+        else raise Bug "expInt: negative exponand"
+      else iexp x y 1;
+end;
+
+fun boolToInt true = 1
+  | boolToInt false = 0;
+
+fun intToBool 1 = true
+  | intToBool 0 = false
+  | intToBool _ = raise Bug "Model.intToBool";
+
+fun minMaxInterval i j = interval i (1 + j - i);
+
+(* ------------------------------------------------------------------------- *)
+(* Model size.                                                               *)
+(* ------------------------------------------------------------------------- *)
+
+type size = {size : int};
+
+(* ------------------------------------------------------------------------- *)
+(* A model of size N has integer elements 0...N-1.                           *)
+(* ------------------------------------------------------------------------- *)
+
+type element = int;
+
+val zeroElement = 0;
+
+fun incrementElement {size = N} i =
+    let
+      val i = i + 1
+    in
+      if i = N then NONE else SOME i
+    end;
+
+fun elementListSpace {size = N} arity =
+    case expInt N arity of
+      NONE => NONE
+    | s as SOME m => if m <= maxSpace then s else NONE;
+
+fun elementListIndex {size = N} =
+    let
+      fun f acc elts =
+          case elts of
+            [] => acc
+          | elt :: elts => f (N * acc + elt) elts
+    in
+      f 0
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* The parts of the model that are fixed.                                    *)
+(* ------------------------------------------------------------------------- *)
+
+type fixedFunction = size -> element list -> element option;
+
+type fixedRelation = size -> element list -> bool option;
+
+datatype fixed =
+    Fixed of
+      {functions : fixedFunction NameArityMap.map,
+       relations : fixedRelation NameArityMap.map};
+
+val uselessFixedFunction : fixedFunction = K (K NONE);
+
+val uselessFixedRelation : fixedRelation = K (K NONE);
+
+val emptyFunctions : fixedFunction NameArityMap.map = NameArityMap.new ();
+
+val emptyRelations : fixedRelation NameArityMap.map = NameArityMap.new ();
+
+fun fixed0 f sz elts =
+    case elts of
+      [] => f sz
+    | _ => raise Bug "Model.fixed0: wrong arity";
+
+fun fixed1 f sz elts =
+    case elts of
+      [x] => f sz x
+    | _ => raise Bug "Model.fixed1: wrong arity";
+
+fun fixed2 f sz elts =
+    case elts of
+      [x,y] => f sz x y
+    | _ => raise Bug "Model.fixed2: wrong arity";
+
+val emptyFixed =
+    let
+      val fns = emptyFunctions
+      and rels = emptyRelations
+    in
+      Fixed
+        {functions = fns,
+         relations = rels}
+    end;
+
+fun peekFunctionFixed fix name_arity =
+    let
+      val Fixed {functions = fns, ...} = fix
+    in
+      NameArityMap.peek fns name_arity
+    end;
+
+fun peekRelationFixed fix name_arity =
+    let
+      val Fixed {relations = rels, ...} = fix
+    in
+      NameArityMap.peek rels name_arity
+    end;
+
+fun getFunctionFixed fix name_arity =
+    case peekFunctionFixed fix name_arity of
+      SOME f => f
+    | NONE => uselessFixedFunction;
+
+fun getRelationFixed fix name_arity =
+    case peekRelationFixed fix name_arity of
+      SOME rel => rel
+    | NONE => uselessFixedRelation;
+
+fun insertFunctionFixed fix name_arity_fn =
+    let
+      val Fixed {functions = fns, relations = rels} = fix
+
+      val fns = NameArityMap.insert fns name_arity_fn
+    in
+      Fixed
+        {functions = fns,
+         relations = rels}
+    end;
+
+fun insertRelationFixed fix name_arity_rel =
+    let
+      val Fixed {functions = fns, relations = rels} = fix
+
+      val rels = NameArityMap.insert rels name_arity_rel
+    in
+      Fixed
+        {functions = fns,
+         relations = rels}
+    end;
+
+local
+  fun union _ = raise Bug "Model.unionFixed: nameArity clash";
+in
+  fun unionFixed fix1 fix2 =
+      let
+        val Fixed {functions = fns1, relations = rels1} = fix1
+        and Fixed {functions = fns2, relations = rels2} = fix2
+
+        val fns = NameArityMap.union union fns1 fns2
+
+        val rels = NameArityMap.union union rels1 rels2
+      in
+        Fixed
+          {functions = fns,
+           relations = rels}
+      end;
+end;
+
+val unionListFixed =
+    let
+      fun union (fix,acc) = unionFixed acc fix
+    in
+      List.foldl union emptyFixed
+    end;
+
+local
+  fun hasTypeFn _ elts =
+      case elts of
+        [x,_] => SOME x
+      | _ => raise Bug "Model.hasTypeFn: wrong arity";
+
+  fun eqRel _ elts =
+      case elts of
+        [x,y] => SOME (x = y)
+      | _ => raise Bug "Model.eqRel: wrong arity";
+in
+  val basicFixed =
+      let
+        val fns = NameArityMap.singleton (Term.hasTypeFunction,hasTypeFn)
+
+        val rels = NameArityMap.singleton (Atom.eqRelation,eqRel)
+      in
+        Fixed
+          {functions = fns,
+           relations = rels}
+      end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Renaming fixed model parts.                                               *)
+(* ------------------------------------------------------------------------- *)
+
+type fixedMap =
+     {functionMap : Name.name NameArityMap.map,
+      relationMap : Name.name NameArityMap.map};
+
+fun mapFixed fixMap fix =
+    let
+      val {functionMap = fnMap, relationMap = relMap} = fixMap
+      and Fixed {functions = fns, relations = rels} = fix
+
+      val fns = NameArityMap.compose fnMap fns
+
+      val rels = NameArityMap.compose relMap rels
+    in
+      Fixed
+        {functions = fns,
+         relations = rels}
+    end;
+
+local
+  fun mkEntry tag (na,n) = (tag,na,n);
+
+  fun mkList tag m = map (mkEntry tag) (NameArityMap.toList m);
+
+  fun ppEntry (tag,source_arity,target) =
+      Print.blockProgram Print.Inconsistent 2
+        [Print.addString tag,
+         Print.addBreak 1,
+         NameArity.pp source_arity,
+         Print.addString " ->",
+         Print.addBreak 1,
+         Name.pp target];
+in
+  fun ppFixedMap fixMap =
+      let
+        val {functionMap = fnMap, relationMap = relMap} = fixMap
+      in
+        case mkList "function" fnMap @ mkList "relation" relMap of
+          [] => Print.skip
+        | entry :: entries =>
+          Print.blockProgram Print.Consistent 0
+            (ppEntry entry ::
+             map (Print.sequence Print.addNewline o ppEntry) entries)
+      end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Standard fixed model parts.                                               *)
+(* ------------------------------------------------------------------------- *)
+
+(* Projections *)
+
+val projectionMin = 1
+and projectionMax = 9;
+
+val projectionList = minMaxInterval projectionMin projectionMax;
+
+fun projectionName i =
+    let
+      val _ = projectionMin <= i orelse
+              raise Bug "Model.projectionName: less than projectionMin"
+
+      val _ = i <= projectionMax orelse
+              raise Bug "Model.projectionName: greater than projectionMax"
+    in
+      Name.fromString ("project" ^ Int.toString i)
+    end;
+
+fun projectionFn i _ elts = SOME (List.nth (elts, i - 1));
+
+fun arityProjectionFixed arity =
+    let
+      fun mkProj i = ((projectionName i, arity), projectionFn i)
+
+      fun addProj i acc =
+          if i > arity then acc
+          else addProj (i + 1) (NameArityMap.insert acc (mkProj i))
+
+      val fns = addProj projectionMin emptyFunctions
+
+      val rels = emptyRelations
+    in
+      Fixed
+        {functions = fns,
+         relations = rels}
+    end;
+
+val projectionFixed =
+    unionListFixed (map arityProjectionFixed projectionList);
+
+(* Arithmetic *)
+
+val numeralMin = ~100
+and numeralMax = 100;
+
+val numeralList = minMaxInterval numeralMin numeralMax;
+
+fun numeralName i =
+    let
+      val _ = numeralMin <= i orelse
+              raise Bug "Model.numeralName: less than numeralMin"
+
+      val _ = i <= numeralMax orelse
+              raise Bug "Model.numeralName: greater than numeralMax"
+
+      val s = if i < 0 then "negative" ^ Int.toString (~i) else Int.toString i
+    in
+      Name.fromString s
+    end;
+
+val addName = Name.fromString "+"
+and divName = Name.fromString "div"
+and dividesName = Name.fromString "divides"
+and evenName = Name.fromString "even"
+and expName = Name.fromString "exp"
+and geName = Name.fromString ">="
+and gtName = Name.fromString ">"
+and isZeroName = Name.fromString "isZero"
+and leName = Name.fromString "<="
+and ltName = Name.fromString "<"
+and modName = Name.fromString "mod"
+and multName = Name.fromString "*"
+and negName = Name.fromString "~"
+and oddName = Name.fromString "odd"
+and preName = Name.fromString "pre"
+and subName = Name.fromString "-"
+and sucName = Name.fromString "suc";
+
+local
+  (* Support *)
+
+  fun modN {size = N} x = x mod N;
+
+  fun oneN sz = modN sz 1;
+
+  fun multN sz (x,y) = modN sz (x * y);
+
+  (* Functions *)
+
+  fun numeralFn i sz = SOME (modN sz i);
+
+  fun addFn sz x y = SOME (modN sz (x + y));
+
+  fun divFn {size = N} x y =
+      let
+        val y = if y = 0 then N else y
+      in
+        SOME (x div y)
+      end;
+
+  fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
+
+  fun modFn {size = N} x y =
+      let
+        val y = if y = 0 then N else y
+      in
+        SOME (x mod y)
+      end;
+
+  fun multFn sz x y = SOME (multN sz (x,y));
+
+  fun negFn {size = N} x = SOME (if x = 0 then 0 else N - x);
+
+  fun preFn {size = N} x = SOME (if x = 0 then N - 1 else x - 1);
+
+  fun subFn {size = N} x y = SOME (if x < y then N + x - y else x - y);
+
+  fun sucFn {size = N} x = SOME (if x = N - 1 then 0 else x + 1);
+
+  (* Relations *)
+
+  fun dividesRel _ x y = SOME (divides x y);
+
+  fun evenRel _ x = SOME (x mod 2 = 0);
+
+  fun geRel _ x y = SOME (x >= y);
+
+  fun gtRel _ x y = SOME (x > y);
+
+  fun isZeroRel _ x = SOME (x = 0);
+
+  fun leRel _ x y = SOME (x <= y);
+
+  fun ltRel _ x y = SOME (x < y);
+
+  fun oddRel _ x = SOME (x mod 2 = 1);
+in
+  val modularFixed =
+      let
+        val fns =
+            NameArityMap.fromList
+              (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+                 numeralList @
+               [((addName,2), fixed2 addFn),
+                ((divName,2), fixed2 divFn),
+                ((expName,2), fixed2 expFn),
+                ((modName,2), fixed2 modFn),
+                ((multName,2), fixed2 multFn),
+                ((negName,1), fixed1 negFn),
+                ((preName,1), fixed1 preFn),
+                ((subName,2), fixed2 subFn),
+                ((sucName,1), fixed1 sucFn)])
+
+        val rels =
+            NameArityMap.fromList
+              [((dividesName,2), fixed2 dividesRel),
+               ((evenName,1), fixed1 evenRel),
+               ((geName,2), fixed2 geRel),
+               ((gtName,2), fixed2 gtRel),
+               ((isZeroName,1), fixed1 isZeroRel),
+               ((leName,2), fixed2 leRel),
+               ((ltName,2), fixed2 ltRel),
+               ((oddName,1), fixed1 oddRel)]
+      in
+        Fixed
+          {functions = fns,
+           relations = rels}
+      end;
+end;
+
+local
+  (* Support *)
+
+  fun cutN {size = N} x = if x >= N then N - 1 else x;
+
+  fun oneN sz = cutN sz 1;
+
+  fun multN sz (x,y) = cutN sz (x * y);
+
+  (* Functions *)
+
+  fun numeralFn i sz = if i < 0 then NONE else SOME (cutN sz i);
+
+  fun addFn sz x y = SOME (cutN sz (x + y));
+
+  fun divFn _ x y = if y = 0 then NONE else SOME (x div y);
+
+  fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
+
+  fun modFn {size = N} x y =
+      if y = 0 orelse x = N - 1 then NONE else SOME (x mod y);
+
+  fun multFn sz x y = SOME (multN sz (x,y));
+
+  fun negFn _ x = if x = 0 then SOME 0 else NONE;
+
+  fun preFn _ x = if x = 0 then NONE else SOME (x - 1);
+
+  fun subFn {size = N} x y =
+      if y = 0 then SOME x
+      else if x = N - 1 orelse x < y then NONE
+      else SOME (x - y);
+
+  fun sucFn sz x = SOME (cutN sz (x + 1));
+
+  (* Relations *)
+
+  fun dividesRel {size = N} x y =
+      if x = 1 orelse y = 0 then SOME true
+      else if x = 0 then SOME false
+      else if y = N - 1 then NONE
+      else SOME (divides x y);
+
+  fun evenRel {size = N} x =
+      if x = N - 1 then NONE else SOME (x mod 2 = 0);
+
+  fun geRel {size = N} y x =
+      if x = N - 1 then if y = N - 1 then NONE else SOME false
+      else if y = N - 1 then SOME true else SOME (x <= y);
+
+  fun gtRel {size = N} y x =
+      if x = N - 1 then if y = N - 1 then NONE else SOME false
+      else if y = N - 1 then SOME true else SOME (x < y);
+
+  fun isZeroRel _ x = SOME (x = 0);
+
+  fun leRel {size = N} x y =
+      if x = N - 1 then if y = N - 1 then NONE else SOME false
+      else if y = N - 1 then SOME true else SOME (x <= y);
+
+  fun ltRel {size = N} x y =
+      if x = N - 1 then if y = N - 1 then NONE else SOME false
+      else if y = N - 1 then SOME true else SOME (x < y);
+
+  fun oddRel {size = N} x =
+      if x = N - 1 then NONE else SOME (x mod 2 = 1);
+in
+  val overflowFixed =
+      let
+        val fns =
+            NameArityMap.fromList
+              (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+                 numeralList @
+               [((addName,2), fixed2 addFn),
+                ((divName,2), fixed2 divFn),
+                ((expName,2), fixed2 expFn),
+                ((modName,2), fixed2 modFn),
+                ((multName,2), fixed2 multFn),
+                ((negName,1), fixed1 negFn),
+                ((preName,1), fixed1 preFn),
+                ((subName,2), fixed2 subFn),
+                ((sucName,1), fixed1 sucFn)])
+
+        val rels =
+            NameArityMap.fromList
+              [((dividesName,2), fixed2 dividesRel),
+               ((evenName,1), fixed1 evenRel),
+               ((geName,2), fixed2 geRel),
+               ((gtName,2), fixed2 gtRel),
+               ((isZeroName,1), fixed1 isZeroRel),
+               ((leName,2), fixed2 leRel),
+               ((ltName,2), fixed2 ltRel),
+               ((oddName,1), fixed1 oddRel)]
+      in
+        Fixed
+          {functions = fns,
+           relations = rels}
+      end;
+end;
+
+(* Sets *)
+
+val cardName = Name.fromString "card"
+and complementName = Name.fromString "complement"
+and differenceName = Name.fromString "difference"
+and emptyName = Name.fromString "empty"
+and memberName = Name.fromString "member"
+and insertName = Name.fromString "insert"
+and intersectName = Name.fromString "intersect"
+and singletonName = Name.fromString "singleton"
+and subsetName = Name.fromString "subset"
+and symmetricDifferenceName = Name.fromString "symmetricDifference"
+and unionName = Name.fromString "union"
+and universeName = Name.fromString "universe";
+
+local
+  (* Support *)
+
+  fun eltN {size = N} =
+      let
+        fun f 0 acc = acc
+          | f x acc = f (x div 2) (acc + 1)
+      in
+        f N ~1
+      end;
+
+  fun posN i = Word.<< (0w1, Word.fromInt i);
+
+  fun univN sz = Word.- (posN (eltN sz), 0w1);
+
+  fun setN sz x = Word.andb (Word.fromInt x, univN sz);
+
+  (* Functions *)
+
+  fun cardFn sz x =
+      let
+        fun f 0w0 acc = acc
+          | f s acc =
+            let
+              val acc = if Word.andb (s,0w1) = 0w0 then acc else acc + 1
+            in
+              f (Word.>> (s,0w1)) acc
+            end
+      in
+        SOME (f (setN sz x) 0)
+      end;
+
+  fun complementFn sz x = SOME (Word.toInt (Word.xorb (univN sz, setN sz x)));
+
+  fun differenceFn sz x y =
+      let
+        val x = setN sz x
+        and y = setN sz y
+      in
+        SOME (Word.toInt (Word.andb (x, Word.notb y)))
+      end;
+
+  fun emptyFn _ = SOME 0;
+
+  fun insertFn sz x y =
+      let
+        val x = x mod eltN sz
+        and y = setN sz y
+      in
+        SOME (Word.toInt (Word.orb (posN x, y)))
+      end;
+
+  fun intersectFn sz x y =
+      SOME (Word.toInt (Word.andb (setN sz x, setN sz y)));
+
+  fun singletonFn sz x =
+      let
+        val x = x mod eltN sz
+      in
+        SOME (Word.toInt (posN x))
+      end;
+
+  fun symmetricDifferenceFn sz x y =
+      let
+        val x = setN sz x
+        and y = setN sz y
+      in
+        SOME (Word.toInt (Word.xorb (x,y)))
+      end;
+
+  fun unionFn sz x y =
+      SOME (Word.toInt (Word.orb (setN sz x, setN sz y)));
+
+  fun universeFn sz = SOME (Word.toInt (univN sz));
+
+  (* Relations *)
+
+  fun memberRel sz x y =
+      let
+        val x = x mod eltN sz
+        and y = setN sz y
+      in
+        SOME (Word.andb (posN x, y) <> 0w0)
+      end;
+
+  fun subsetRel sz x y =
+      let
+        val x = setN sz x
+        and y = setN sz y
+      in
+        SOME (Word.andb (x, Word.notb y) = 0w0)
+      end;
+in
+  val setFixed =
+      let
+        val fns =
+            NameArityMap.fromList
+              [((cardName,1), fixed1 cardFn),
+               ((complementName,1), fixed1 complementFn),
+               ((differenceName,2), fixed2 differenceFn),
+               ((emptyName,0), fixed0 emptyFn),
+               ((insertName,2), fixed2 insertFn),
+               ((intersectName,2), fixed2 intersectFn),
+               ((singletonName,1), fixed1 singletonFn),
+               ((symmetricDifferenceName,2), fixed2 symmetricDifferenceFn),
+               ((unionName,2), fixed2 unionFn),
+               ((universeName,0), fixed0 universeFn)]
+
+        val rels =
+            NameArityMap.fromList
+              [((memberName,2), fixed2 memberRel),
+               ((subsetName,2), fixed2 subsetRel)]
+      in
+        Fixed
+          {functions = fns,
+           relations = rels}
+      end;
+end;
+
+(* Lists *)
+
+val appendName = Name.fromString "@"
+and consName = Name.fromString "::"
+and lengthName = Name.fromString "length"
+and nilName = Name.fromString "nil"
+and nullName = Name.fromString "null"
+and tailName = Name.fromString "tail";
+
+local
+  val baseFix =
+      let
+        val fix = unionFixed projectionFixed overflowFixed
+
+        val sucFn = getFunctionFixed fix (sucName,1)
+
+        fun suc2Fn sz _ x = sucFn sz [x]
+      in
+        insertFunctionFixed fix ((sucName,2), fixed2 suc2Fn)
+      end;
+
+  val fixMap =
+      {functionMap = NameArityMap.fromList
+                       [((appendName,2),addName),
+                        ((consName,2),sucName),
+                        ((lengthName,1), projectionName 1),
+                        ((nilName,0), numeralName 0),
+                        ((tailName,1),preName)],
+       relationMap = NameArityMap.fromList
+                       [((nullName,1),isZeroName)]};
+
+in
+  val listFixed = mapFixed fixMap baseFix;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Valuations.                                                               *)
+(* ------------------------------------------------------------------------- *)
+
+datatype valuation = Valuation of element NameMap.map;
+
+val emptyValuation = Valuation (NameMap.new ());
+
+fun insertValuation (Valuation m) v_i = Valuation (NameMap.insert m v_i);
+
+fun peekValuation (Valuation m) v = NameMap.peek m v;
+
+fun constantValuation i =
+    let
+      fun add (v,V) = insertValuation V (v,i)
+    in
+      NameSet.foldl add emptyValuation
+    end;
+
+val zeroValuation = constantValuation zeroElement;
+
+fun getValuation V v =
+    case peekValuation V v of
+      SOME i => i
+    | NONE => raise Error "Model.getValuation: incomplete valuation";
+
+fun randomValuation {size = N} vs =
+    let
+      fun f (v,V) = insertValuation V (v, Portable.randomInt N)
+    in
+      NameSet.foldl f emptyValuation vs
+    end;
+
+fun incrementValuation N vars =
+    let
+      fun inc vs V =
+          case vs of
+            [] => NONE
+          | v :: vs =>
+            let
+              val (carry,i) =
+                  case incrementElement N (getValuation V v) of
+                    SOME i => (false,i)
+                  | NONE => (true,zeroElement)
+
+              val V = insertValuation V (v,i)
+            in
+              if carry then inc vs V else SOME V
+            end
+    in
+      inc (NameSet.toList vars)
+    end;
+
+fun foldValuation N vars f =
+    let
+      val inc = incrementValuation N vars
+
+      fun fold V acc =
+          let
+            val acc = f (V,acc)
+          in
+            case inc V of
+              NONE => acc
+            | SOME V => fold V acc
+          end
+
+      val zero = zeroValuation vars
+    in
+      fold zero
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of random finite mapping Z^n -> Z.                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val UNKNOWN = ~1;
+
+datatype table =
+    ForgetfulTable
+  | ArrayTable of int Array.array;
+
+fun newTable N arity =
+    case elementListSpace {size = N} arity of
+      NONE => ForgetfulTable
+    | SOME space => ArrayTable (Array.array (space,UNKNOWN));
+
+local
+  fun randomResult R = Portable.randomInt R;
+in
+  fun lookupTable N R table elts =
+      case table of
+        ForgetfulTable => randomResult R
+      | ArrayTable a =>
+        let
+          val i = elementListIndex {size = N} elts
+
+          val r = Array.sub (a,i)
+        in
+          if r <> UNKNOWN then r
+          else
+            let
+              val r = randomResult R
+
+              val () = Array.update (a,i,r)
+            in
+              r
+            end
+        end;
+end;
+
+fun updateTable N table (elts,r) =
+    case table of
+      ForgetfulTable => ()
+    | ArrayTable a =>
+      let
+        val i = elementListIndex {size = N} elts
+
+        val () = Array.update (a,i,r)
+      in
+        ()
+      end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of random finite mappings name * arity -> Z^arity -> Z.            *)
+(* ------------------------------------------------------------------------- *)
+
+datatype tables =
+    Tables of
+      {domainSize : int,
+       rangeSize : int,
+       tableMap : table NameArityMap.map ref};
+
+fun newTables N R =
+    Tables
+      {domainSize = N,
+       rangeSize = R,
+       tableMap = ref (NameArityMap.new ())};
+
+fun getTables tables n_a =
+    let
+      val Tables {domainSize = N, rangeSize = _, tableMap = tm} = tables
+
+      val ref m = tm
+    in
+      case NameArityMap.peek m n_a of
+        SOME t => t
+      | NONE =>
+        let
+          val (_,a) = n_a
+
+          val t = newTable N a
+
+          val m = NameArityMap.insert m (n_a,t)
+
+          val () = tm := m
+        in
+          t
+        end
+    end;
+
+fun lookupTables tables (n,elts) =
+    let
+      val Tables {domainSize = N, rangeSize = R, ...} = tables
+
+      val a = length elts
+
+      val table = getTables tables (n,a)
+    in
+      lookupTable N R table elts
+    end;
+
+fun updateTables tables ((n,elts),r) =
+    let
+      val Tables {domainSize = N, ...} = tables
+
+      val a = length elts
+
+      val table = getTables tables (n,a)
+    in
+      updateTable N table (elts,r)
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of random finite models.                                           *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = {size : int, fixed : fixed};
+
+datatype model =
+    Model of
+      {size : int,
+       fixedFunctions : (element list -> element option) NameArityMap.map,
+       fixedRelations : (element list -> bool option) NameArityMap.map,
+       randomFunctions : tables,
+       randomRelations : tables};
+
+fun new {size = N, fixed} =
+    let
+      val Fixed {functions = fns, relations = rels} = fixed
+
+      val fixFns = NameArityMap.transform (fn f => f {size = N}) fns
+      and fixRels = NameArityMap.transform (fn r => r {size = N}) rels
+
+      val rndFns = newTables N N
+      and rndRels = newTables N 2
+    in
+      Model
+        {size = N,
+         fixedFunctions = fixFns,
+         fixedRelations = fixRels,
+         randomFunctions = rndFns,
+         randomRelations = rndRels}
+    end;
+
+fun size (Model {size = N, ...}) = N;
+
+fun peekFixedFunction M (n,elts) =
+    let
+      val Model {fixedFunctions = fixFns, ...} = M
+    in
+      case NameArityMap.peek fixFns (n, length elts) of
+        NONE => NONE
+      | SOME fixFn => fixFn elts
+    end;
+
+fun isFixedFunction M n_elts = Option.isSome (peekFixedFunction M n_elts);
+
+fun peekFixedRelation M (n,elts) =
+    let
+      val Model {fixedRelations = fixRels, ...} = M
+    in
+      case NameArityMap.peek fixRels (n, length elts) of
+        NONE => NONE
+      | SOME fixRel => fixRel elts
+    end;
+
+fun isFixedRelation M n_elts = Option.isSome (peekFixedRelation M n_elts);
+
+(* A default model *)
+
+val defaultSize = 8;
+
+val defaultFixed =
+    unionListFixed
+      [basicFixed,
+       projectionFixed,
+       modularFixed,
+       setFixed,
+       listFixed];
+
+val default = {size = defaultSize, fixed = defaultFixed};
+
+(* ------------------------------------------------------------------------- *)
+(* Taking apart terms to interpret them.                                     *)
+(* ------------------------------------------------------------------------- *)
+
+fun destTerm tm =
+    case tm of
+      Term.Var _ => tm
+    | Term.Fn f_tms =>
+      case Term.stripApp tm of
+        (_,[]) => tm
+      | (v as Term.Var _, tms) => Term.Fn (Term.appName, v :: tms)
+      | (Term.Fn (f,tms), tms') => Term.Fn (f, tms @ tms');
+
+(* ------------------------------------------------------------------------- *)
+(* Interpreting terms and formulas in the model.                             *)
+(* ------------------------------------------------------------------------- *)
+
+fun interpretFunction M n_elts =
+    case peekFixedFunction M n_elts of
+      SOME r => r
+    | NONE =>
+      let
+        val Model {randomFunctions = rndFns, ...} = M
+      in
+        lookupTables rndFns n_elts
+      end;
+
+fun interpretRelation M n_elts =
+    case peekFixedRelation M n_elts of
+      SOME r => r
+    | NONE =>
+      let
+        val Model {randomRelations = rndRels, ...} = M
+      in
+        intToBool (lookupTables rndRels n_elts)
+      end;
+
+fun interpretTerm M V =
+    let
+      fun interpret tm =
+          case destTerm tm of
+            Term.Var v => getValuation V v
+          | Term.Fn (f,tms) => interpretFunction M (f, map interpret tms)
+    in
+      interpret
+    end;
+
+fun interpretAtom M V (r,tms) =
+    interpretRelation M (r, map (interpretTerm M V) tms);
+
+fun interpretFormula M =
+    let
+      val N = size M
+
+      fun interpret V fm =
+          case fm of
+            Formula.True => true
+          | Formula.False => false
+          | Formula.Atom atm => interpretAtom M V atm
+          | Formula.Not p => not (interpret V p)
+          | Formula.Or (p,q) => interpret V p orelse interpret V q
+          | Formula.And (p,q) => interpret V p andalso interpret V q
+          | Formula.Imp (p,q) => interpret V (Formula.Or (Formula.Not p, q))
+          | Formula.Iff (p,q) => interpret V p = interpret V q
+          | Formula.Forall (v,p) => interpret' V p v N
+          | Formula.Exists (v,p) =>
+            interpret V (Formula.Not (Formula.Forall (v, Formula.Not p)))
+
+      and interpret' V fm v i =
+          i = 0 orelse
+          let
+            val i = i - 1
+            val V' = insertValuation V (v,i)
+          in
+            interpret V' fm andalso interpret' V fm v i
+          end
+    in
+      interpret
+    end;
+
+fun interpretLiteral M V (pol,atm) =
+    let
+      val b = interpretAtom M V atm
+    in
+      if pol then b else not b
+    end;
+
+fun interpretClause M V cl = LiteralSet.exists (interpretLiteral M V) cl;
+
+(* ------------------------------------------------------------------------- *)
+(* Check whether random groundings of a formula are true in the model.       *)
+(* Note: if it's cheaper, a systematic check will be performed instead.      *)
+(* ------------------------------------------------------------------------- *)
+
+fun check interpret {maxChecks} M fv x =
+    let
+      val N = size M
+
+      fun score (V,{T,F}) =
+          if interpret M V x then {T = T + 1, F = F} else {T = T, F = F + 1}
+
+      fun randomCheck acc = score (randomValuation {size = N} fv, acc)
+
+      val maxChecks =
+          case maxChecks of
+            NONE => maxChecks
+          | SOME m =>
+            case expInt N (NameSet.size fv) of
+              SOME n => if n <= m then NONE else maxChecks
+            | NONE => maxChecks
+    in
+      case maxChecks of
+        SOME m => funpow m randomCheck {T = 0, F = 0}
+      | NONE => foldValuation {size = N} fv score {T = 0, F = 0}
+    end;
+
+fun checkAtom maxChecks M atm =
+    check interpretAtom maxChecks M (Atom.freeVars atm) atm;
+
+fun checkFormula maxChecks M fm =
+    check interpretFormula maxChecks M (Formula.freeVars fm) fm;
+
+fun checkLiteral maxChecks M lit =
+    check interpretLiteral maxChecks M (Literal.freeVars lit) lit;
+
+fun checkClause maxChecks M cl =
+    check interpretClause maxChecks M (LiteralSet.freeVars cl) cl;
+
+(* ------------------------------------------------------------------------- *)
+(* Updating the model.                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+fun updateFunction M func_elts_elt =
+    let
+      val Model {randomFunctions = rndFns, ...} = M
+
+      val () = updateTables rndFns func_elts_elt
+    in
+      ()
+    end;
+
+fun updateRelation M (rel_elts,pol) =
+    let
+      val Model {randomRelations = rndRels, ...} = M
+
+      val () = updateTables rndRels (rel_elts, boolToInt pol)
+    in
+      ()
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of terms with interpretations embedded in the subterms.            *)
+(* ------------------------------------------------------------------------- *)
+
+datatype modelTerm =
+    ModelVar
+  | ModelFn of Term.functionName * modelTerm list * int list;
+
+fun modelTerm M V =
+    let
+      fun modelTm tm =
+          case destTerm tm of
+            Term.Var v => (ModelVar, getValuation V v)
+          | Term.Fn (f,tms) =>
+            let
+              val (tms,xs) = unzip (map modelTm tms)
+            in
+              (ModelFn (f,tms,xs), interpretFunction M (f,xs))
+            end
+    in
+      modelTm
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Perturbing the model.                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+datatype perturbation =
+    FunctionPerturbation of (Term.functionName * element list) * element
+  | RelationPerturbation of (Atom.relationName * element list) * bool;
+
+fun perturb M pert =
+    case pert of
+      FunctionPerturbation func_elts_elt => updateFunction M func_elts_elt
+    | RelationPerturbation rel_elts_pol => updateRelation M rel_elts_pol;
+
+local
+  fun pertTerm _ [] _ acc = acc
+    | pertTerm M target tm acc =
+      case tm of
+        ModelVar => acc
+      | ModelFn (func,tms,xs) =>
+        let
+          fun onTarget ys = mem (interpretFunction M (func,ys)) target
+
+          val func_xs = (func,xs)
+
+          val acc =
+              if isFixedFunction M func_xs then acc
+              else
+                let
+                  fun add (y,acc) = FunctionPerturbation (func_xs,y) :: acc
+                in
+                  foldl add acc target
+                end
+        in
+          pertTerms M onTarget tms xs acc
+        end
+
+  and pertTerms M onTarget =
+      let
+        val N = size M
+
+        fun filterElements pred =
+            let
+              fun filt 0 acc = acc
+                | filt i acc =
+                  let
+                    val i = i - 1
+                    val acc = if pred i then i :: acc else acc
+                  in
+                    filt i acc
+                  end
+            in
+              filt N []
+            end
+
+        fun pert _ [] [] acc = acc
+          | pert ys (tm :: tms) (x :: xs) acc =
+            let
+              fun pred y =
+                  y <> x andalso onTarget (List.revAppend (ys, y :: xs))
+
+              val target = filterElements pred
+
+              val acc = pertTerm M target tm acc
+            in
+              pert (x :: ys) tms xs acc
+            end
+          | pert _ _ _ _ = raise Bug "Model.pertTerms.pert"
+      in
+        pert []
+      end;
+
+  fun pertAtom M V target (rel,tms) acc =
+      let
+        fun onTarget ys = interpretRelation M (rel,ys) = target
+
+        val (tms,xs) = unzip (map (modelTerm M V) tms)
+
+        val rel_xs = (rel,xs)
+
+        val acc =
+            if isFixedRelation M rel_xs then acc
+            else RelationPerturbation (rel_xs,target) :: acc
+      in
+        pertTerms M onTarget tms xs acc
+      end;
+
+  fun pertLiteral M V ((pol,atm),acc) = pertAtom M V pol atm acc;
+
+  fun pertClause M V cl acc = LiteralSet.foldl (pertLiteral M V) acc cl;
+
+  fun pickPerturb M perts =
+      if null perts then ()
+      else perturb M (List.nth (perts, Portable.randomInt (length perts)));
+in
+  fun perturbTerm M V (tm,target) =
+      pickPerturb M (pertTerm M target (fst (modelTerm M V tm)) []);
+
+  fun perturbAtom M V (atm,target) =
+      pickPerturb M (pertAtom M V target atm []);
+
+  fun perturbLiteral M V lit = pickPerturb M (pertLiteral M V (lit,[]));
+
+  fun perturbClause M V cl = pickPerturb M (pertClause M V cl []);
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun pp M =
+    Print.program
+      [Print.addString "Model{",
+       Print.ppInt (size M),
+       Print.addString "}"];
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Name.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,45 @@
+(* ========================================================================= *)
+(* NAMES                                                                     *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+signature Name =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of names.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+type name
+
+(* ------------------------------------------------------------------------- *)
+(* A total ordering.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : name * name -> order
+
+val equal : name -> name -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Fresh names.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val newName : unit -> name
+
+val newNames : int -> name list
+
+val variantPrime : (name -> bool) -> name -> name
+
+val variantNum : (name -> bool) -> name -> name
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : name Print.pp
+
+val toString : name -> string
+
+val fromString : string -> name
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Name.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,98 @@
+(* ========================================================================= *)
+(* NAMES                                                                     *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2      *)
+(* ========================================================================= *)
+
+structure Name :> Name =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of names.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+type name = string;
+
+(* ------------------------------------------------------------------------- *)
+(* A total ordering.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val compare = String.compare;
+
+fun equal n1 n2 = n1 = n2;
+
+(* ------------------------------------------------------------------------- *)
+(* Fresh variables.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+local
+  val prefix  = "_";
+
+  fun numName i = mkPrefix prefix (Int.toString i);
+in
+  fun newName () = numName (newInt ());
+
+  fun newNames n = map numName (newInts n);
+end;
+
+fun variantPrime acceptable =
+    let
+      fun variant n = if acceptable n then n else variant (n ^ "'")
+    in
+      variant
+    end;
+
+local
+  fun isDigitOrPrime #"'" = true
+    | isDigitOrPrime c = Char.isDigit c;
+in
+  fun variantNum acceptable n =
+      if acceptable n then n
+      else
+        let
+          val n = stripSuffix isDigitOrPrime n
+
+          fun variant i =
+              let
+                val n_i = n ^ Int.toString i
+              in
+                if acceptable n_i then n_i else variant (i + 1)
+              end
+        in
+          variant 0
+        end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val pp = Print.ppString;
+
+fun toString s : string = s;
+
+fun fromString s : name = s;
+
+end
+
+structure NameOrdered =
+struct type t = Name.name val compare = Name.compare end
+
+structure NameMap = KeyMap (NameOrdered);
+
+structure NameSet =
+struct
+
+  local
+    structure S = ElementSet (NameMap);
+  in
+    open S;
+  end;
+
+  val pp =
+      Print.ppMap
+        toList
+        (Print.ppBracket "{" "}" (Print.ppOpList "," Name.pp));
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/NameArity.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,47 @@
+(* ========================================================================= *)
+(* NAME/ARITY PAIRS                                                          *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature NameArity =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of name/arity pairs.                                               *)
+(* ------------------------------------------------------------------------- *)
+
+type nameArity = Name.name * int
+
+val name : nameArity -> Name.name
+
+val arity : nameArity -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Testing for different arities.                                            *)
+(* ------------------------------------------------------------------------- *)
+
+val nary : int -> nameArity -> bool
+
+val nullary : nameArity -> bool
+
+val unary : nameArity -> bool
+
+val binary : nameArity -> bool
+
+val ternary : nameArity -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* A total ordering.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : nameArity * nameArity -> order
+
+val equal : nameArity -> nameArity -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : nameArity Print.pp
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/NameArity.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,91 @@
+(* ========================================================================= *)
+(* NAME/ARITY PAIRS                                                          *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure NameArity :> NameArity =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* A type of name/arity pairs.                                               *)
+(* ------------------------------------------------------------------------- *)
+
+type nameArity = Name.name * int;
+
+fun name ((n,_) : nameArity) = n;
+
+fun arity ((_,i) : nameArity) = i;
+
+(* ------------------------------------------------------------------------- *)
+(* Testing for different arities.                                            *)
+(* ------------------------------------------------------------------------- *)
+
+fun nary i n_i = arity n_i = i;
+
+val nullary = nary 0
+and unary = nary 1
+and binary = nary 2
+and ternary = nary 3;
+
+(* ------------------------------------------------------------------------- *)
+(* A total ordering.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare ((n1,i1),(n2,i2)) =
+    case Name.compare (n1,n2) of
+      LESS => LESS
+    | EQUAL => Int.compare (i1,i2)
+    | GREATER => GREATER;
+
+fun equal (n1,i1) (n2,i2) = i1 = i2 andalso Name.equal n1 n2;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing.                                              *)
+(* ------------------------------------------------------------------------- *)
+
+fun pp (n,i) =
+    Print.blockProgram Print.Inconsistent 0
+      [Name.pp n,
+       Print.addString "/",
+       Print.ppInt i];
+
+end
+
+structure NameArityOrdered =
+struct type t = NameArity.nameArity val compare = NameArity.compare end
+
+structure NameArityMap =
+struct
+
+  local
+    structure S = KeyMap (NameArityOrdered);
+  in
+    open S;
+  end;
+
+  fun compose m1 m2 =
+      let
+        fun pk ((_,a),n) = peek m2 (n,a)
+      in
+        mapPartial pk m1
+      end;
+
+end
+
+structure NameAritySet =
+struct
+
+  local
+    structure S = ElementSet (NameArityMap);
+  in
+    open S;
+  end;
+
+  val allNullary = all NameArity.nullary;
+
+  val pp =
+      Print.ppMap
+        toList
+        (Print.ppBracket "{" "}" (Print.ppOpList "," NameArity.pp));
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Normalize.sig	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,55 @@
+(* ========================================================================= *)
+(* NORMALIZING FORMULAS                                                      *)
+(* Copyright (c) 2001-2009 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Normalize =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* Negation normal form.                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+val nnf : Formula.formula -> Formula.formula
+
+(* ------------------------------------------------------------------------- *)
+(* Conjunctive normal form derivations.                                      *)
+(* ------------------------------------------------------------------------- *)
+
+type thm
+
+datatype inference =
+    Axiom of Formula.formula
+  | Definition of string * Formula.formula
+  | Simplify of thm * thm list
+  | Conjunct of thm
+  | Specialize of thm
+  | Skolemize of thm
+  | Clausify of thm
+
+val mkAxiom : Formula.formula -> thm
+
+val destThm : thm -> Formula.formula * inference
+
+val proveThms :
+    thm list -> (Formula.formula * inference * Formula.formula list) list
+
+val toStringInference : inference -> string
+
+val ppInference : inference Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* Conjunctive normal form.                                                  *)
+(* ------------------------------------------------------------------------- *)
+
+type cnf
+
+val initialCnf : cnf
+
+val addCnf : thm -> cnf -> (Thm.clause * thm) list * cnf
+
+val proveCnf : thm list -> (Thm.clause * thm) list
+
+val cnf : Formula.formula -> Thm.clause list
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Normalize.sml	Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,1386 @@
+(* ========================================================================= *)
+(* NORMALIZING FORMULAS                                                      *)
+(* Copyright (c) 2001-2007 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Normalize :> Normalize =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Constants.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val prefix = "FOFtoCNF";
+
+val skolemPrefix = "skolem" ^ prefix;
+
+val definitionPrefix = "definition" ^ prefix;
+
+(* ------------------------------------------------------------------------- *)
+(* Storing huge real numbers as their log.                                   *)
+(* ------------------------------------------------------------------------- *)
+
+datatype logReal = LogReal of real;
+
+fun compareLogReal (LogReal logX, LogReal logY) =
+    Real.compare (logX,logY);
+
+val zeroLogReal = LogReal ~1.0;
+
+val oneLogReal = LogReal 0.0;
+
+local
+  fun isZero logX = logX < 0.0;
+
+  (* Assume logX >= logY >= 0.0 *)
+  fun add logX logY = logX + Math.ln (1.0 + Math.exp (logY - logX));
+in
+  fun isZeroLogReal (LogReal logX) = isZero logX;
+
+  fun multiplyLogReal (LogReal logX) (LogReal logY) =
+      if isZero logX orelse isZero logY then zeroLogReal
+      else LogReal (logX + logY);
+
+  fun addLogReal (lx as LogReal logX) (ly as LogReal logY) =
+      if isZero logX then ly
+      else if isZero logY then lx
+      else if logX < logY then LogReal (add logY logX)
+      else LogReal (add logX logY);
+
+  fun withinRelativeLogReal logDelta (LogReal logX) (LogReal logY) =
+      isZero logX orelse
+      (not (isZero logY) andalso logX < logY + logDelta);
+end;
+
+fun toStringLogReal (LogReal logX) = Real.toString logX;
+
+(* ------------------------------------------------------------------------- *)
+(* Counting the clauses that would be generated by conjunctive normal form.  *)
+(* ------------------------------------------------------------------------- *)
+
+val countLogDelta = 0.01;
+
+datatype count = Count of {positive : logReal, negative : logReal};
+
+fun countCompare (count1,count2) =
+    let
+      val Count {positive = p1, negative = _} = count1
+      and Count {positive = p2, negative = _} = count2
+    in
+      compareLogReal (p1,p2)
+    end;
+
+fun countNegate (Count {positive = p, negative = n}) =
+    Count {positive = n, negative = p};
+
+fun countLeqish count1 count2 =
+    let
+      val Count {positive = p1, negative = _} = count1
+      and Count {positive = p2, negative = _} = count2
+    in
+      withinRelativeLogReal countLogDelta p1 p2
+    end;
+
+(*MetisDebug
+fun countEqualish count1 count2 =
+    countLeqish count1 count2 andalso
+    countLeqish count2 count1;
+
+fun countEquivish count1 count2 =
+    countEqualish count1 count2 andalso
+    countEqualish (countNegate count1) (countNegate count2);
+*)
+
+val countTrue = Count {positive = zeroLogReal, negative = oneLogReal};
+
+val countFalse = Count {positive = oneLogReal, negative = zeroLogReal};
+
+val countLiteral = Count {positive = oneLogReal, negative = oneLogReal};
+
+fun countAnd2 (count1,count2) =
+    let
+      val Count {positive = p1, negative = n1} = count1
+      and Count {positive = p2, negative = n2} = count2
+      val p = addLogReal p1 p2
+      and n = multiplyLogReal n1 n2
+    in
+      Count {positive = p, negative = n}
+    end;
+
+fun countOr2 (count1,count2) =
+    let
+      val Count {positive = p1, negative = n1} = count1
+      and Count {positive = p2, negative = n2} = count2
+      val p = multiplyLogReal p1 p2
+      and n = addLogReal n1 n2
+    in
+      Count {positive = p, negative = n}
+    end;
+
+(* Whether countXor2 is associative or not is an open question. *)
+
+fun countXor2 (count1,count2) =
+    let
+      val Count {positive = p1, negative = n1} = count1
+      and Count {positive = p2, negative = n2} = count2
+      val p = addLogReal (multiplyLogReal p1 p2) (multiplyLogReal n1 n2)
+      and n = addLogReal (multiplyLogReal p1 n2) (multiplyLogReal n1 p2)
+    in
+      Count {positive = p, negative = n}
+    end;
+
+fun countDefinition body_count = countXor2 (countLiteral,body_count);
+
+val countToString =
+    let
+      val rToS = toStringLogReal
+    in
+      fn Count {positive = p, negative = n} =>
+         "(+" ^ rToS p ^ ",-" ^ rToS n ^ ")"
+    end;
+
+val ppCount = Print.ppMap countToString Print.ppString;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of normalized formula.                                             *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formula =
+    True
+  | False
+  | Literal of NameSet.set * Literal.literal
+  | And of NameSet.set * count * formula Set.set
+  | Or of NameSet.set * count * formula Set.set
+  | Xor of NameSet.set * count * bool * formula Set.set
+  | Exists of NameSet.set * count * NameSet.set * formula
+  | Forall of NameSet.set * count * NameSet.set * formula;
+
+fun compare f1_f2 =
+    if Portable.pointerEqual f1_f2 then EQUAL
+    else
+      case f1_f2 of
+        (True,True) => EQUAL
+      | (True,_) => LESS
+      | (_,True) => GREATER
+      | (False,False) => EQUAL
+      | (False,_) => LESS
+      | (_,False) => GREATER
+      | (Literal (_,l1), Literal (_,l2)) => Literal.compare (l1,l2)
+      | (Literal _, _) => LESS
+      | (_, Literal _) => GREATER
+      | (And (_,_,s1), And (_,_,s2)) => Set.compare (s1,s2)
+      | (And _, _) => LESS
+      | (_, And _) => GREATER
+      | (Or (_,_,s1), Or (_,_,s2)) => Set.compare (s1,s2)
+      | (Or _, _) => LESS
+      | (_, Or _) => GREATER
+      | (Xor (_,_,p1,s1), Xor (_,_,p2,s2)) =>
+        (case boolCompare (p1,p2) of
+           LESS => LESS
+         | EQUAL => Set.compare (s1,s2)
+         | GREATER => GREATER)
+      | (Xor _, _) => LESS
+      | (_, Xor _) => GREATER
+      | (Exists (_,_,n1,f1), Exists (_,_,n2,f2)) =>
+        (case NameSet.compare (n1,n2) of
+           LESS => LESS
+         | EQUAL => compare (f1,f2)
+         | GREATER => GREATER)
+      | (Exists _, _) => LESS
+      | (_, Exists _) => GREATER
+      | (Forall (_,_,n1,f1), Forall (_,_,n2,f2)) =>
+        (case NameSet.compare (n1,n2) of
+           LESS => LESS
+         | EQUAL => compare (f1,f2)
+         | GREATER => GREATER);
+
+val empty = Set.empty compare;
+
+val singleton = Set.singleton compare;
+
+local
+  fun neg True = False
+    | neg False = True
+    | neg (Literal (fv,lit)) = Literal (fv, Literal.negate lit)
+    | neg (And (fv,c,s)) = Or (fv, countNegate c, neg_set s)
+    | neg (Or (fv,c,s)) = And (fv, countNegate c, neg_set s)
+    | neg (Xor (fv,c,p,s)) = Xor (fv, c, not p, s)
+    | neg (Exists (fv,c,n,f)) = Forall (fv, countNegate c, n, neg f)
+    | neg (Forall (fv,c,n,f)) = Exists (fv, countNegate c, n, neg f)
+
+  and neg_set s = Set.foldl neg_elt empty s
+
+  and neg_elt (f,s) = Set.add s (neg f);
+in
+  val negate = neg;
+
+  val negateSet = neg_set;
+end;
+
+fun negateMember x s = Set.member (negate x) s;
+
+local
+  fun member s x = negateMember x s;
+in
+  fun negateDisjoint s1 s2 =
+      if Set.size s1 < Set.size s2 then not (Set.exists (member s2) s1)
+      else not (Set.exists (member s1) s2);
+end;
+
+fun polarity True = true
+  | polarity False = false
+  | polarity (Literal (_,(pol,_))) = not pol
+  | polarity (And _) = true
+  | polarity (Or _) = false
+  | polar