--- a/src/Tools/Metis/src/Clause.sml Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/Clause.sml Fri Aug 17 23:10:50 2007 +0200
@@ -16,7 +16,8 @@
let
val r = ref 0
in
- fn () => case r of ref n => let val () = r := n + 1 in n end
+ fn () => CRITICAL (fn () =>
+ case r of ref n => let val () = r := n + 1 in n end)
end;
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Normalize.sml Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/Normalize.sml Fri Aug 17 23:10:50 2007 +0200
@@ -795,14 +795,14 @@
let
val counter : int NameMap.map ref = ref (NameMap.new ())
in
- fn n =>
+ fn n => CRITICAL (fn () =>
let
val ref m = counter
val i = Option.getOpt (NameMap.peek m n, 0)
val () = counter := NameMap.insert m (n, i + 1)
in
"skolem_" ^ n ^ (if i = 0 then "" else "_" ^ Int.toString i)
- end
+ end)
end;
fun skolemize fv bv fm =
@@ -993,13 +993,13 @@
let
val counter : int ref = ref 0
in
- fn () =>
+ fn () => CRITICAL (fn () =>
let
val ref i = counter
val () = counter := i + 1
in
"defCNF_" ^ Int.toString i
- end
+ end)
end;
fun newDefinition def =
--- a/src/Tools/Metis/src/Portable.sig Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/Portable.sig Fri Aug 17 23:10:50 2007 +0200
@@ -24,4 +24,10 @@
val time : ('a -> 'b) -> 'a -> 'b
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+val CRITICAL: (unit -> 'a) -> 'a
+
end
--- a/src/Tools/Metis/src/PortableIsabelle.sml Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/PortableIsabelle.sml Fri Aug 17 23:10:50 2007 +0200
@@ -23,6 +23,12 @@
val time = timeap;
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+val CRITICAL = CRITICAL;
+
end
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/PortableMlton.sml Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/PortableMlton.sml Fri Aug 17 23:10:50 2007 +0200
@@ -56,6 +56,12 @@
y
end;
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+fun CRITICAL e = e (); (*dummy*)
+
end
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/PortableMosml.sml Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/PortableMosml.sml Fri Aug 17 23:10:50 2007 +0200
@@ -26,6 +26,12 @@
val time = Mosml.time;
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+fun CRITICAL e = e (); (*dummy*)
+
end
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/PortableSmlNJ.sml Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/PortableSmlNJ.sml Fri Aug 17 23:10:50 2007 +0200
@@ -52,6 +52,12 @@
y
end;
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing) *)
+(* ------------------------------------------------------------------------- *)
+
+fun CRITICAL e = e (); (*dummy*)
+
end
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Random.sml Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/Random.sml Fri Aug 17 23:10:50 2007 +0200
@@ -18,27 +18,29 @@
fun newgen () = newgenseed (Time.toReal (Time.now ()));
-fun random {seedref as ref seed} =
- (seedref := nextrand seed; seed / m);
+fun random {seedref} = CRITICAL (fn () =>
+ (seedref := nextrand (! seedref); ! seedref / m));
-fun randomlist (n, {seedref as ref seed0}) =
- let fun h 0 seed res = (seedref := seed; res)
+fun randomlist (n, {seedref}) = CRITICAL (fn () =>
+ let val seed0 = ! seedref
+ fun h 0 seed res = (seedref := seed; res)
| h i seed res = h (i-1) (nextrand seed) (seed / m :: res)
- in h n seed0 [] end;
+ in h n seed0 [] end);
fun range (min, max) =
if min > max then raise Fail "Random.range: empty range"
else
- fn {seedref as ref seed} =>
- (seedref := nextrand seed; min + (floor(real(max-min) * seed / m)));
+ fn {seedref} => CRITICAL (fn () =>
+ (seedref := nextrand (! seedref); min + (floor(real(max-min) * ! seedref / m))));
fun rangelist (min, max) =
if min > max then raise Fail "Random.rangelist: empty range"
else
- fn (n, {seedref as ref seed0}) =>
- let fun h 0 seed res = (seedref := seed; res)
+ fn (n, {seedref}) => CRITICAL (fn () =>
+ let val seed0 = ! seedref
+ fun h 0 seed res = (seedref := seed; res)
| h i seed res = h (i-1) (nextrand seed)
(min + floor(real(max-min) * seed / m) :: res)
- in h n seed0 [] end
+ in h n seed0 [] end)
end
--- a/src/Tools/Metis/src/Useful.sml Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/Useful.sml Fri Aug 17 23:10:50 2007 +0200
@@ -377,7 +377,7 @@
val primesList = ref (calcPrimes 10);
in
- fun primes n =
+ fun primes n = CRITICAL (fn () =>
if length (!primesList) <= n then List.take (!primesList,n)
else
let
@@ -385,9 +385,9 @@
val () = primesList := l
in
l
- end;
+ end);
- fun primesUpTo n =
+ fun primesUpTo n = CRITICAL (fn () =>
let
fun f k [] =
let
@@ -400,7 +400,7 @@
if p <= n then f (k + 1) ps else List.take (!primesList, k)
in
f 0 (!primesList)
- end;
+ end);
end;
(* ------------------------------------------------------------------------- *)
@@ -572,22 +572,22 @@
local
val generator = ref 0
in
- fun newInt () =
+ fun newInt () = CRITICAL (fn () =>
let
val n = !generator
val () = generator := n + 1
in
n
- end;
+ end);
fun newInts 0 = []
- | newInts k =
+ | newInts k = CRITICAL (fn () =>
let
val n = !generator
val () = generator := n + k
in
interval n k
- end;
+ end);
end;
local