updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
--- a/src/Tools/Metis/src/Active.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Active.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Active =
--- a/src/Tools/Metis/src/Active.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Active.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Active :> Active =
--- a/src/Tools/Metis/src/Atom.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Atom.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Atom =
--- a/src/Tools/Metis/src/Atom.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Atom.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Atom :> Atom =
--- a/src/Tools/Metis/src/AtomNet.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/AtomNet.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature AtomNet =
--- a/src/Tools/Metis/src/AtomNet.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/AtomNet.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure AtomNet :> AtomNet =
--- a/src/Tools/Metis/src/Clause.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Clause.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Clause =
--- a/src/Tools/Metis/src/Clause.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Clause.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Clause :> Clause =
--- a/src/Tools/Metis/src/ElementSet.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/ElementSet.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature ElementSet =
--- a/src/Tools/Metis/src/ElementSet.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/ElementSet.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
functor ElementSet (KM : KeyMap) :> ElementSet
--- a/src/Tools/Metis/src/Formula.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Formula.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Formula =
--- a/src/Tools/Metis/src/Formula.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Formula.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Formula :> Formula =
--- a/src/Tools/Metis/src/Heap.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Heap.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Heap =
--- a/src/Tools/Metis/src/Heap.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Heap.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Heap :> Heap =
--- a/src/Tools/Metis/src/KeyMap.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/KeyMap.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature KeyMap =
--- a/src/Tools/Metis/src/KeyMap.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/KeyMap.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
--- a/src/Tools/Metis/src/KnuthBendixOrder.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE KNUTH-BENDIX TERM ORDERING *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature KnuthBendixOrder =
--- a/src/Tools/Metis/src/KnuthBendixOrder.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure KnuthBendixOrder :> KnuthBendixOrder =
--- a/src/Tools/Metis/src/Lazy.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Lazy.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Lazy =
--- a/src/Tools/Metis/src/Lazy.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Lazy.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Lazy :> Lazy =
--- a/src/Tools/Metis/src/Literal.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Literal.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Literal =
--- a/src/Tools/Metis/src/Literal.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Literal.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Literal :> Literal =
--- a/src/Tools/Metis/src/LiteralNet.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/LiteralNet.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature LiteralNet =
--- a/src/Tools/Metis/src/LiteralNet.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/LiteralNet.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure LiteralNet :> LiteralNet =
--- a/src/Tools/Metis/src/Map.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Map.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Map =
--- a/src/Tools/Metis/src/Map.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Map.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Map :> Map =
--- a/src/Tools/Metis/src/Model.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Model.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Model =
--- a/src/Tools/Metis/src/Model.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Model.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Model :> Model =
--- a/src/Tools/Metis/src/Name.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Name.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAMES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Name =
--- a/src/Tools/Metis/src/Name.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Name.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAMES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Name :> Name =
--- a/src/Tools/Metis/src/NameArity.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/NameArity.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature NameArity =
--- a/src/Tools/Metis/src/NameArity.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/NameArity.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure NameArity :> NameArity =
--- a/src/Tools/Metis/src/Normalize.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Normalize.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Normalize =
--- a/src/Tools/Metis/src/Normalize.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Normalize.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Normalize :> Normalize =
@@ -685,24 +685,23 @@
(* Basic conjunctive normal form. *)
(* ------------------------------------------------------------------------- *)
-val newSkolemFunction =
- let
- val counter : int StringMap.map ref = ref (StringMap.new ())
+local
+ val counter : int StringMap.map ref = ref (StringMap.new ());
- fun new n () =
- let
- val ref m = counter
- val s = Name.toString n
- val i = Option.getOpt (StringMap.peek m s, 0)
- val () = counter := StringMap.insert m (s, i + 1)
- val i = if i = 0 then "" else "_" ^ Int.toString i
- val s = skolemPrefix ^ "_" ^ s ^ i
- in
- Name.fromString s
- end
- in
- fn n => Portable.critical (new n) ()
- end;
+ fun new n () =
+ let
+ val ref m = counter
+ val s = Name.toString n
+ val i = Option.getOpt (StringMap.peek m s, 0)
+ val () = counter := StringMap.insert m (s, i + 1)
+ val i = if i = 0 then "" else "_" ^ Int.toString i
+ val s = skolemPrefix ^ "_" ^ s ^ i
+ in
+ Name.fromString s
+ end;
+in
+ fun newSkolemFunction n = Portable.critical (new n) ();
+end;
fun skolemize fv bv fm =
let
@@ -1241,18 +1240,19 @@
(* Definitions. *)
(* ------------------------------------------------------------------------- *)
-val newDefinitionRelation =
- let
- val counter : int ref = ref 0
- in
- fn () => Portable.critical (fn () =>
- let
- val ref i = counter
- val () = counter := i + 1
- in
- definitionPrefix ^ "_" ^ Int.toString i
- end) ()
- end;
+local
+ val counter : int ref = ref 0;
+
+ fun new () =
+ let
+ val ref i = counter
+ val () = counter := i + 1
+ in
+ definitionPrefix ^ "_" ^ Int.toString i
+ end;
+in
+ fun newDefinitionRelation () = Portable.critical new ();
+end;
fun newDefinition def =
let
--- a/src/Tools/Metis/src/Options.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Options.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROCESSING COMMAND LINE OPTIONS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Options =
--- a/src/Tools/Metis/src/Options.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Options.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROCESSING COMMAND LINE OPTIONS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Options :> Options =
--- a/src/Tools/Metis/src/Ordered.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Ordered.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Ordered =
--- a/src/Tools/Metis/src/Ordered.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Ordered.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure IntOrdered =
--- a/src/Tools/Metis/src/Parse.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Parse.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PARSING *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Parse =
--- a/src/Tools/Metis/src/Parse.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Parse.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PARSING *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Parse :> Parse =
--- a/src/Tools/Metis/src/Portable.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Portable.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ML COMPILER SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Portable =
--- a/src/Tools/Metis/src/PortableMlton.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/PortableMlton.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MLTON SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Portable :> Portable =
--- a/src/Tools/Metis/src/PortableMosml.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/PortableMosml.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MOSCOW ML SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Portable :> Portable =
--- a/src/Tools/Metis/src/PortablePolyml.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/PortablePolyml.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* POLY/ML SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Portable :> Portable =
--- a/src/Tools/Metis/src/Print.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Print.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Print =
--- a/src/Tools/Metis/src/Print.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Print.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Print :> Print =
--- a/src/Tools/Metis/src/Problem.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Problem.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Problem =
--- a/src/Tools/Metis/src/Problem.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Problem.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Problem :> Problem =
--- a/src/Tools/Metis/src/Proof.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Proof.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Proof =
--- a/src/Tools/Metis/src/Proof.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Proof.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Proof :> Proof =
--- a/src/Tools/Metis/src/Resolution.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Resolution.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Resolution =
--- a/src/Tools/Metis/src/Resolution.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Resolution.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Resolution :> Resolution =
--- a/src/Tools/Metis/src/Rewrite.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Rewrite.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Rewrite =
--- a/src/Tools/Metis/src/Rewrite.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Rewrite.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Rewrite :> Rewrite =
--- a/src/Tools/Metis/src/Rule.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Rule.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Rule =
--- a/src/Tools/Metis/src/Rule.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Rule.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Rule :> Rule =
--- a/src/Tools/Metis/src/Set.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Set.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Set =
--- a/src/Tools/Metis/src/Set.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Set.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Set :> Set =
--- a/src/Tools/Metis/src/Sharing.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Sharing.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Sharing =
--- a/src/Tools/Metis/src/Sharing.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Sharing.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Sharing :> Sharing =
--- a/src/Tools/Metis/src/Stream.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Stream.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Stream =
--- a/src/Tools/Metis/src/Stream.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Stream.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Stream :> Stream =
--- a/src/Tools/Metis/src/Subst.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Subst.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Subst =
--- a/src/Tools/Metis/src/Subst.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Subst.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Subst :> Subst =
--- a/src/Tools/Metis/src/Subsume.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Subsume.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Subsume =
--- a/src/Tools/Metis/src/Subsume.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Subsume.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Subsume :> Subsume =
--- a/src/Tools/Metis/src/Term.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Term.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Term =
--- a/src/Tools/Metis/src/Term.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Term.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Term :> Term =
--- a/src/Tools/Metis/src/TermNet.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/TermNet.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature TermNet =
--- a/src/Tools/Metis/src/TermNet.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/TermNet.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure TermNet :> TermNet =
--- a/src/Tools/Metis/src/Thm.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Thm.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Thm =
--- a/src/Tools/Metis/src/Thm.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Thm.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Thm :> Thm =
--- a/src/Tools/Metis/src/Tptp.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Tptp.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE TPTP PROBLEM FILE FORMAT *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Tptp =
--- a/src/Tools/Metis/src/Tptp.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Tptp.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE TPTP PROBLEM FILE FORMAT *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Tptp :> Tptp =
--- a/src/Tools/Metis/src/Units.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Units.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Units =
--- a/src/Tools/Metis/src/Units.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Units.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Units :> Units =
--- a/src/Tools/Metis/src/Useful.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Useful =
--- a/src/Tools/Metis/src/Useful.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Useful :> Useful =
@@ -462,50 +462,33 @@
end;
local
- fun calcPrimes ps n i =
- if List.exists (fn p => divides p i) ps then calcPrimes ps n (i + 1)
+ fun calcPrimes mode ps i n =
+ if n = 0 then ps
+ else if List.exists (fn p => divides p i) ps then
+ let
+ val i = i + 1
+ and n = if mode then n else n - 1
+ in
+ calcPrimes mode ps i n
+ end
else
let
val ps = ps @ [i]
+ and i = i + 1
and n = n - 1
in
- if n = 0 then ps else calcPrimes ps n (i + 1)
+ calcPrimes mode ps i n
end;
-
- val primesList = ref [2];
in
- fun primes n = Portable.critical (fn () =>
- let
- val ref ps = primesList
-
- val k = n - length ps
- in
- if k <= 0 then List.take (ps,n)
- else
- let
- val ps = calcPrimes ps k (List.last ps + 1)
+ fun primes n =
+ if n <= 0 then []
+ else calcPrimes true [2] 3 (n - 1);
- val () = primesList := ps
- in
- ps
- end
- end) ();
+ fun primesUpTo n =
+ if n < 2 then []
+ else calcPrimes false [2] 3 (n - 2);
end;
-fun primesUpTo n = Portable.critical (fn () =>
- let
- fun f k =
- let
- val l = primes k
-
- val p = List.last l
- in
- if p < n then f (2 * k) else takeWhile (fn j => j <= n) l
- end
- in
- f 8
- end) ();
-
(* ------------------------------------------------------------------------- *)
(* Strings. *)
(* ------------------------------------------------------------------------- *)
@@ -723,23 +706,30 @@
local
val generator = ref 0
-in
- fun newInt () = Portable.critical (fn () =>
+
+ fun newIntThunk () =
let
val n = !generator
+
val () = generator := n + 1
in
n
- end) ();
+ end;
- fun newInts 0 = []
- | newInts k = Portable.critical (fn () =>
+ fun newIntsThunk k () =
let
val n = !generator
+
val () = generator := n + k
in
interval n k
- end) ();
+ end;
+in
+ fun newInt () = Portable.critical newIntThunk ();
+
+ fun newInts k =
+ if k <= 0 then []
+ else Portable.critical (newIntsThunk k) ();
end;
fun withRef (r,new) f x =
--- a/src/Tools/Metis/src/Waiting.sig Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Waiting.sig Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Waiting =
--- a/src/Tools/Metis/src/Waiting.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Waiting.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Waiting :> Waiting =
--- a/src/Tools/Metis/src/metis.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/metis.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* METIS FIRST ORDER PROVER *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
open Useful;
@@ -13,7 +13,7 @@
val VERSION = "2.3";
-val versionString = PROGRAM^" "^VERSION^" (release 20100915)"^"\n";
+val versionString = PROGRAM^" "^VERSION^" (release 20100916)"^"\n";
(* ------------------------------------------------------------------------- *)
(* Program options. *)
--- a/src/Tools/Metis/src/problems.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/problems.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
(* ========================================================================= *)
--- a/src/Tools/Metis/src/problems2tptp.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/problems2tptp.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
open Useful;
--- a/src/Tools/Metis/src/selftest.sml Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/selftest.sml Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* METIS TESTS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)