--- a/CONTRIBUTORS Wed Jul 08 16:35:23 2020 +0200
+++ b/CONTRIBUTORS Thu Jul 09 11:39:16 2020 +0200
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* July 2020: Martin Desharnais
+ Integration of Metis 2.4.
+
* June 2020: Makarius Wenzel
System option pide_session is enabled by default, notably for standard
"isabelle build" to invoke Scala from ML.
--- a/NEWS Wed Jul 08 16:35:23 2020 +0200
+++ b/NEWS Thu Jul 09 11:39:16 2020 +0200
@@ -48,6 +48,10 @@
* For the natural numbers, Sup {} = 0.
+* Updated the Metis prover underlying the "metis" proof method to
+ version 2.4 (release 20180810). The new version fixes one soundness
+ defect and two incompleteness defects. Very slight INCOMPATIBILITY.
+
* Library theory "Bit_Operations" with generic bit operations.
* Session HOL-Word: Type word is restricted to bit strings consisting
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy Wed Jul 08 16:35:23 2020 +0200
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Thu Jul 09 11:39:16 2020 +0200
@@ -950,7 +950,7 @@
from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
by simp
then obtain a b where p: "p = [ a, b ]"
- by (metis length_0_conv length_Suc_conv)
+ by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
with \<open>p \<in> carrier (K[X])\<close> show ?thesis
using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
subfield.subfield_Units[OF assms(1)]
--- a/src/Tools/Metis/Makefile Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/Makefile Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
###############################################################################
# METIS MAKEFILE
-# Copyright (c) 2001 Joe Hurd, distributed under the BSD License
+# Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License
###############################################################################
.SUFFIXES:
@@ -10,26 +10,27 @@
###############################################################################
.PHONY: default
-default: mosml
+default:
+ @if command -v mlton > /dev/null ; then $(MAKE) mlton ; else if command -v polyc > /dev/null ; then $(MAKE) polyml ; else if command -v mosmlc > /dev/null ; then $(MAKE) mosml ; else echo "ERROR: No ML found on path: install either MLton, Poly/ML or Moscow ML." ; exit 1 ; fi ; fi ; fi
###############################################################################
# Cleaning temporary files.
###############################################################################
TEMP = \
- $(MOSML_TARGETS) \
- bin/mosml/*.sml bin/mosml/*.ui bin/mosml/*.uo bin/mosml/a.out \
$(MLTON_TARGETS) \
bin/mlton/*.sml bin/mlton/*.mlb \
$(POLYML_TARGETS) \
- bin/polyml/*.sml bin/polyml/*.log bin/polyml/*.o
+ bin/polyml/*.sml bin/polyml/*.log \
+ $(MOSML_TARGETS) \
+ bin/mosml/*.sml bin/mosml/*.ui bin/mosml/*.uo bin/mosml/a.out
.PHONY: clean
clean:
@echo
- @echo '********************'
- @echo '* Clean everything *'
- @echo '********************'
+ @echo '+------------------+'
+ @echo '| Clean everything |'
+ @echo '+------------------+'
@echo
rm -f $(TEMP)
$(MAKE) -C test $@
@@ -98,6 +99,97 @@
MLPP_OPTS =
###############################################################################
+# Building using MLton.
+###############################################################################
+
+MLTON = mlton
+
+MLTON_OPTS = -runtime 'ram-slop 0.4'
+
+MLTON_SRC = \
+ src/Portable.sig src/PortableMlton.sml \
+ $(SRC)
+
+MLTON_TARGETS = \
+ bin/mlton/selftest \
+ bin/mlton/metis \
+ bin/mlton/problems2tptp
+
+bin/mlton/%.sml: $(MLTON_SRC) src/%.sml
+ @$(MLPP) $(MLPP_OPTS) -c mlton $^ > $@
+
+bin/mlton/%.mlb: bin/mlton/%.sml
+ echo '$$(SML_LIB)/basis/basis.mlb $$(SML_LIB)/basis/mlton.mlb $(notdir $<)' > $@
+
+bin/mlton/%: bin/mlton/%.mlb
+ @echo
+ @echo '+-------------------------+'
+ @echo '| Compile a MLton program |'
+ @echo '+-------------------------+'
+ @echo
+ @echo $@
+ cd bin/mlton ; $(MLTON) $(MLTON_OPTS) $(notdir $<)
+ @echo
+
+.PHONY: mlton-info
+mlton-info:
+ @echo
+ @echo '+-----------------------------------+'
+ @echo '| Build and test the MLton programs |'
+ @echo '+-----------------------------------+'
+ @echo
+
+.PHONY: mlton
+mlton: mlton-info $(MLTON_TARGETS)
+ $(MAKE) -C test mlton
+
+###############################################################################
+# Building using Poly/ML.
+###############################################################################
+
+POLYML = polyc
+
+POLYML_OPTS =
+
+POLYML_SRC = \
+ src/Random.sig src/Random.sml \
+ src/Portable.sig src/PortablePolyml.sml \
+ $(SRC)
+
+POLYML_TARGETS = \
+ bin/polyml/selftest \
+ bin/polyml/problems2tptp \
+ bin/polyml/metis
+
+bin/polyml/%.sml: src/%.sml $(POLYML_SRC)
+ @$(MLPP) $(MLPP_OPTS) -c polyml $(POLYML_SRC) > $@
+ @echo 'fun main () = let' >> $@
+ @$(MLPP) $(MLPP_OPTS) -c polyml $< >> $@
+ @echo "in () end handle e => (TextIO.output (TextIO.stdErr, \"FATAL EXCEPTION:\\\\n\"^ exnMessage e); OS.Process.exit OS.Process.failure);" >> $@
+
+bin/polyml/%: bin/polyml/%.sml
+ @echo
+ @echo '+---------------------------+'
+ @echo '| Compile a Poly/ML program |'
+ @echo '+---------------------------+'
+ @echo
+ @echo $@
+ cd bin/polyml && $(POLYML) $(POLYML_OPTS) -o $(notdir $@) $(notdir $<)
+ @echo
+
+.PHONY: polyml-info
+polyml-info:
+ @echo
+ @echo '+-------------------------------------+'
+ @echo '| Build and test the Poly/ML programs |'
+ @echo '+-------------------------------------+'
+ @echo
+
+.PHONY: polyml
+polyml: polyml-info $(POLYML_TARGETS)
+ $(MAKE) -C test polyml
+
+###############################################################################
# Building using Moscow ML.
###############################################################################
@@ -116,120 +208,15 @@
.PHONY: mosml-info
mosml-info:
@echo
- @echo '*****************************************'
- @echo '* Build and test the Moscow ML programs *'
- @echo '*****************************************'
+ @echo '+---------------------------------------+'
+ @echo '| Build and test the Moscow ML programs |'
+ @echo '+---------------------------------------+'
@echo
.PHONY: mosml
mosml: mosml-info $(MOSML_OBJ) $(MOSML_TARGETS) test
###############################################################################
-# Building using MLton.
-###############################################################################
-
-MLTON = mlton
-
-MLTON_OPTS = -runtime 'ram-slop 0.4'
-
-MLTON_SRC = \
- src/Portable.sig src/PortableMlton.sml \
- $(SRC)
-
-METIS = bin/mlton/metis
-
-PROBLEMS2TPTP = bin/mlton/problems2tptp
-
-MLTON_TARGETS = \
- bin/mlton/selftest \
- $(METIS) \
- $(PROBLEMS2TPTP)
-
-bin/mlton/%.sml: $(MLTON_SRC) src/%.sml
- @$(MLPP) $(MLPP_OPTS) -c mlton $^ > $@
-
-bin/mlton/%.mlb: bin/mlton/%.sml
- echo '$$(SML_LIB)/basis/basis.mlb $$(SML_LIB)/basis/mlton.mlb $(notdir $<)' > $@
-
-bin/mlton/%: bin/mlton/%.mlb
- @echo
- @echo '***************************'
- @echo '* Compile a MLton program *'
- @echo '***************************'
- @echo
- @echo $@
- cd bin/mlton ; $(MLTON) $(MLTON_OPTS) $(notdir $<)
- @echo
-
-.PHONY: mlton-info
-mlton-info:
- @echo
- @echo '*************************************'
- @echo '* Build and test the MLton programs *'
- @echo '*************************************'
- @echo
-
-.PHONY: mlton
-mlton: mlton-info $(MLTON_TARGETS)
- $(MAKE) -C test mlton
-
-###############################################################################
-# Building using Poly/ML.
-###############################################################################
-
-POLYML = poly
-
-POLYML_OPTS =
-
-ifeq ($(shell uname), Darwin)
- POLYML_LINK_OPTS = -lpolymain -lpolyml -segprot POLY rwx rwx
-else
- POLYML_LINK_OPTS = -lpolymain -lpolyml
-endif
-
-POLYML_SRC = \
- src/Random.sig src/Random.sml \
- src/Portable.sig src/PortablePolyml.sml \
- $(SRC)
-
-POLYML_TARGETS = \
- bin/polyml/selftest \
- bin/polyml/problems2tptp \
- bin/polyml/metis
-
-bin/polyml/%.sml: src/%.sml $(POLYML_SRC)
- @$(MLPP) $(MLPP_OPTS) -c polyml $(POLYML_SRC) > $@
- @echo 'fun main () = let' >> $@
- @$(MLPP) $(MLPP_OPTS) -c polyml $< >> $@
- @echo "in () end; PolyML.export(\"$(basename $(notdir $<))\", main);" >> $@
-
-bin/polyml/%.o: bin/polyml/%.sml
- cd bin/polyml ; echo "use \"$(notdir $<)\";" | $(POLYML) $(POLYML_OPTS) > $(basename $(notdir $<)).log
- @if test $@ -nt $< ; then echo 'compiled $@' ; else cat bin/polyml/$(basename $(notdir $<)).log ; exit 1 ; fi
-
-bin/polyml/%: bin/polyml/%.o
- @echo
- @echo '*****************************'
- @echo '* Compile a Poly/ML program *'
- @echo '*****************************'
- @echo
- @echo $@
- cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) $(POLYML_LINK_OPTS)
- @echo
-
-.PHONY: polyml-info
-polyml-info:
- @echo
- @echo '***************************************'
- @echo '* Build and test the Poly/ML programs *'
- @echo '***************************************'
- @echo
-
-.PHONY: polyml
-polyml: polyml-info $(POLYML_TARGETS)
- $(MAKE) -C test polyml
-
-###############################################################################
# Development.
##############################################################################
--- a/src/Tools/Metis/README Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/README Thu Jul 09 11:39:16 2020 +0200
@@ -4,15 +4,16 @@
for Metis with the latest Metis package.
1. The files "Makefile" and "script/mlpp" and the directory "src/"
- must reflect the corresponding files in Joe Hurd's official Metis
- package. The package that was used when these notes where written
- was Metis 2.3 (release 20110926).
+ must reflect the corresponding files in Joe Leslie-Hurd's official
+ Metis package. The package that was used when these notes where
+ written was Metis 2.3 (release 20110926). The package was later
+ updated to Metis 2.4 (release 20180810).
2. The license in each source file will probably not be something we
can use in Isabelle. The "fix_metis_license" script can be run to
replace all occurrences of "MIT license" with "BSD License". In a
- 13 Sept. 2010 email to Gerwin Klein, Joe Hurd, the sole copyright
- holder of Metis, wrote:
+ 13 Sept. 2010 email to Gerwin Klein, Joe Leslie-Hurd, the sole
+ copyright holder of Metis, wrote:
I hereby give permission to the Isabelle team to release Metis
as part of Isabelle, with the Metis code covered under the
@@ -46,5 +47,11 @@
Good luck!
+
Jasmin Blanchette
1 December 2011
+
+Updated by
+
+ Martin Desharnais
+ 9 July 2020
--- a/src/Tools/Metis/make_metis Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/make_metis Thu Jul 09 11:39:16 2020 +0200
@@ -14,8 +14,8 @@
cat <<EOF
(*
This file was generated by the "make_metis" script. The BSD License is used
- with Joe Hurd's kind permission. Extract from a September 13, 2010 email
- written by Joe Hurd:
+ with Joe Leslie-Hurd's kind permission. Extract from a September 13, 2010
+ email written by him:
I hereby give permission to the Isabelle team to release Metis as part
of Isabelle, with the Metis code covered under the Isabelle BSD
--- a/src/Tools/Metis/metis.ML Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/metis.ML Thu Jul 09 11:39:16 2020 +0200
@@ -1,7 +1,7 @@
(*
This file was generated by the "make_metis" script. The BSD License is used
- with Joe Hurd's kind permission. Extract from a September 13, 2010 email
- written by Joe Hurd:
+ with Joe Leslie-Hurd's kind permission. Extract from a September 13, 2010
+ email written by him:
I hereby give permission to the Isabelle team to release Metis as part
of Isabelle, with the Metis code covered under the Isabelle BSD
@@ -93,7 +93,7 @@
(* ========================================================================= *)
(* ML COMPILER SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Portable =
@@ -174,7 +174,7 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Useful =
@@ -377,6 +377,20 @@
val gcd : int -> int -> int
+(* Primes *)
+
+type sieve
+
+val initSieve : sieve
+
+val maxSieve : sieve -> int
+
+val primesSieve : sieve -> int list
+
+val incSieve : sieve -> bool * sieve
+
+val nextSieve : sieve -> int * sieve
+
val primes : int -> int list
val primesUpTo : int -> int list
@@ -507,7 +521,7 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Useful :> Metis_Useful =
@@ -981,33 +995,99 @@
end;
end;
-local
- 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
- calcPrimes mode ps i n
- end;
-in
- fun primes n =
- if n <= 0 then []
- else calcPrimes true [2] 3 (n - 1);
-
- fun primesUpTo n =
- if n < 2 then []
- else calcPrimes false [2] 3 (n - 2);
-end;
+(* Primes *)
+
+datatype sieve =
+ Sieve of
+ {max : int,
+ primes : (int * (int * int)) list};
+
+val initSieve =
+ let
+ val n = 1
+ and ps = []
+ in
+ Sieve
+ {max = n,
+ primes = ps}
+ end;
+
+fun maxSieve (Sieve {max = n, ...}) = n;
+
+fun primesSieve (Sieve {primes = ps, ...}) = List.map fst ps;
+
+fun incSieve sieve =
+ let
+ val n = maxSieve sieve + 1
+
+ fun add i ps =
+ case ps of
+ [] => (true,[(n,(0,0))])
+ | (p,(k,j)) :: ps =>
+ let
+ val k = (k + i) mod p
+
+ val j = j + i
+ in
+ if k = 0 then (false, (p,(k,j)) :: ps)
+ else
+ let
+ val (b,ps) = add j ps
+ in
+ (b, (p,(k,0)) :: ps)
+ end
+ end
+
+ val Sieve {primes = ps, ...} = sieve
+
+ val (b,ps) = add 1 ps
+
+ val sieve =
+ Sieve
+ {max = n,
+ primes = ps}
+ in
+ (b,sieve)
+ end;
+
+fun nextSieve sieve =
+ let
+ val (b,sieve) = incSieve sieve
+ in
+ if b then (maxSieve sieve, sieve)
+ else nextSieve sieve
+ end;
+
+local
+ fun inc s =
+ let
+ val (_,s) = incSieve s
+ in
+ s
+ end;
+in
+ fun primesUpTo m =
+ if m <= 1 then []
+ else primesSieve (funpow (m - 1) inc initSieve);
+end;
+
+val primes =
+ let
+ fun next s n =
+ if n <= 0 then []
+ else
+ let
+ val (p,s) = nextSieve s
+
+ val n = n - 1
+
+ val ps = next s n
+ in
+ p :: ps
+ end
+ in
+ next initSieve
+ end;
(* ------------------------------------------------------------------------- *)
(* Strings. *)
@@ -1354,7 +1434,9 @@
fun timed f a =
let
val tmr = Timer.startCPUTimer ()
+
val res = f a
+
val {usr,sys,...} = Timer.checkCPUTimer tmr
in
(Time.toReal usr + Time.toReal sys, res)
@@ -1388,7 +1470,7 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Lazy =
@@ -1410,7 +1492,7 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Lazy :> Metis_Lazy =
@@ -1451,7 +1533,7 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Ordered =
@@ -1487,7 +1569,7 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_IntOrdered =
@@ -1513,7 +1595,7 @@
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Map =
@@ -1706,7 +1788,7 @@
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Map :> Metis_Map =
@@ -3136,7 +3218,7 @@
(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_KeyMap =
@@ -3339,7 +3421,7 @@
(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
functor Metis_KeyMap (Key : Metis_Ordered) :> Metis_KeyMap where type key = Key.t =
@@ -4786,7 +4868,7 @@
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Set =
@@ -4958,7 +5040,7 @@
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Set :> Metis_Set =
@@ -5292,7 +5374,7 @@
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_ElementSet =
@@ -5427,8 +5509,10 @@
val disjoint : set -> set -> bool
(* ------------------------------------------------------------------------- *)
-(* Closing under an operation. *)
-(* ------------------------------------------------------------------------- *)
+(* Pointwise operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val lift : (element -> set) -> set -> set
val closedAdd : (element -> set) -> set -> set -> set
@@ -5457,6 +5541,34 @@
val domain : 'a map -> set
(* ------------------------------------------------------------------------- *)
+(* Depth-first search. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ordering =
+ Linear of element list
+ | Cycle of element list
+
+val preOrder : (element -> set) -> set -> ordering
+
+val postOrder : (element -> set) -> set -> ordering
+
+val preOrdered : (element -> set) -> element list -> bool
+
+val postOrdered : (element -> set) -> element list -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Strongly connected components. *)
+(* ------------------------------------------------------------------------- *)
+
+val preOrderSCC : (element -> set) -> set -> set list
+
+val postOrderSCC : (element -> set) -> set -> set list
+
+val preOrderedSCC : (element -> set) -> set list -> bool
+
+val postOrderedSCC : (element -> set) -> set list -> bool
+
+(* ------------------------------------------------------------------------- *)
(* Pretty-printing. *)
(* ------------------------------------------------------------------------- *)
@@ -5482,7 +5594,7 @@
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
functor Metis_ElementSet (
@@ -5784,8 +5896,15 @@
fun disjoint (Metis_Set m1) (Metis_Set m2) = KM.disjointDomain m1 m2;
(* ------------------------------------------------------------------------- *)
-(* Closing under an operation. *)
-(* ------------------------------------------------------------------------- *)
+(* Pointwise operations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun lift f =
+ let
+ fun inc (elt,set) = union set (f elt)
+ in
+ foldl inc empty
+ end;
fun closedAdd f =
let
@@ -5818,6 +5937,324 @@
fun fromList elts = addList empty elts;
(* ------------------------------------------------------------------------- *)
+(* Depth-first search. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ordering =
+ Linear of element list
+ | Cycle of element list;
+
+fun postOrdered children =
+ let
+ fun check acc elts =
+ case elts of
+ [] => true
+ | elt :: elts =>
+ not (member elt acc) andalso
+ let
+ val acc = closedAdd children acc (singleton elt)
+ in
+ check acc elts
+ end
+ in
+ check empty
+ end;
+
+fun preOrdered children elts = postOrdered children (List.rev elts);
+
+local
+ fun takeStackset elt =
+ let
+ fun notElement (e,_,_) = not (equalElement e elt)
+ in
+ Metis_Useful.takeWhile notElement
+ end;
+
+ fun consElement ((e,_,_),el) = e :: el;
+
+ fun depthFirstSearch children =
+ let
+ fun traverse (dealt,dealtset) (stack,stackset) work =
+ case work of
+ [] =>
+ (case stack of
+ [] => Linear dealt
+ | (elt,work,stackset) :: stack =>
+ let
+ val dealt = elt :: dealt
+
+ val dealtset = add dealtset elt
+ in
+ traverse (dealt,dealtset) (stack,stackset) work
+ end)
+ | elt :: work =>
+ if member elt dealtset then
+ traverse (dealt,dealtset) (stack,stackset) work
+ else if member elt stackset then
+ let
+ val cycle = takeStackset elt stack
+
+ val cycle = elt :: List.foldl consElement [elt] cycle
+ in
+ Cycle cycle
+ end
+ else
+ let
+ val stack = (elt,work,stackset) :: stack
+
+ val stackset = add stackset elt
+
+ val work = toList (children elt)
+ in
+ traverse (dealt,dealtset) (stack,stackset) work
+ end
+
+ val dealt = []
+ and dealtset = empty
+ and stack = []
+ and stackset = empty
+ in
+ traverse (dealt,dealtset) (stack,stackset)
+ end;
+in
+ fun preOrder children roots =
+ let
+ val result = depthFirstSearch children (toList roots)
+
+(*BasicDebug
+ val () =
+ case result of
+ Cycle _ => ()
+ | Linear l =>
+ let
+ val () =
+ if subset roots (fromList l) then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.preOrder: missing roots"
+
+ val () =
+ if preOrdered children l then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.preOrder: bad ordering"
+ in
+ ()
+ end
+*)
+ in
+ result
+ end;
+
+ fun postOrder children roots =
+ case depthFirstSearch children (toList roots) of
+ Linear l =>
+ let
+ val l = List.rev l
+
+(*BasicDebug
+ val () =
+ if subset roots (fromList l) then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.postOrder: missing roots"
+
+ val () =
+ if postOrdered children l then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.postOrder: bad ordering"
+*)
+ in
+ Linear l
+ end
+ | cycle => cycle;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Strongly connected components. *)
+(* ------------------------------------------------------------------------- *)
+
+fun postOrderedSCC children =
+ let
+ fun check acc eltsl =
+ case eltsl of
+ [] => true
+ | elts :: eltsl =>
+ not (null elts) andalso
+ disjoint elts acc andalso
+ let
+ fun addElt elt = closedAdd children acc (singleton elt)
+
+ val (root,elts) = deletePick elts
+
+ fun checkElt elt = member root (addElt elt)
+ in
+ all checkElt elts andalso
+ let
+ val acc = addElt root
+ in
+ subset elts acc andalso
+ check acc eltsl
+ end
+ end
+ in
+ check empty
+ end;
+
+fun preOrderedSCC children eltsl = postOrderedSCC children (List.rev eltsl);
+
+(* An implementation of Tarjan's algorithm: *)
+
+(* http://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm *)
+
+local
+ datatype stackSCC = StackSCC of set * (element * set) list;
+
+ val emptyStack = StackSCC (empty,[]);
+
+ fun pushStack (StackSCC (elts,eltl)) elt =
+ StackSCC (add elts elt, (elt,elts) :: eltl);
+
+ fun inStack elt (StackSCC (elts,_)) = member elt elts;
+
+ fun popStack root =
+ let
+ fun pop scc eltl =
+ case eltl of
+ [] => raise Metis_Useful.Bug "Metis_ElementSet.popStack"
+ | (elt,elts) :: eltl =>
+ let
+ val scc = add scc elt
+ in
+ if equalElement elt root then (scc, StackSCC (elts,eltl))
+ else pop scc eltl
+ end
+ in
+ fn sccs => fn StackSCC (_,eltl) =>
+ let
+ val (scc,stack) = pop empty eltl
+ in
+ (scc :: sccs, stack)
+ end
+ end;
+
+ fun getIndex indices e : int =
+ case KM.peek indices e of
+ SOME i => i
+ | NONE => raise Metis_Useful.Bug "Metis_ElementSet.getIndex";
+
+ fun isRoot indices lows e = getIndex indices e = getIndex lows e;
+
+ fun reduceIndex indices (e,i) =
+ let
+ val j = getIndex indices e
+ in
+ if j <= i then indices else KM.insert indices (e,i)
+ end;
+
+ fun tarjan children =
+ let
+ fun dfsVertex sccs callstack index indices lows stack elt =
+ let
+ val indices = KM.insert indices (elt,index)
+ and lows = KM.insert lows (elt,index)
+
+ val index = index + 1
+
+ val stack = pushStack stack elt
+
+ val chil = toList (children elt)
+ in
+ dfsSuccessors sccs callstack index indices lows stack elt chil
+ end
+
+ and dfsSuccessors sccs callstack index indices lows stack elt chil =
+ case chil of
+ [] =>
+ let
+ val (sccs,stack) =
+ if isRoot indices lows elt then popStack elt sccs stack
+ else (sccs,stack)
+ in
+ case callstack of
+ [] => (sccs,index,indices,lows)
+ | (p,elts) :: callstack =>
+ let
+ val lows = reduceIndex lows (p, getIndex lows elt)
+ in
+ dfsSuccessors sccs callstack index indices lows stack p elts
+ end
+ end
+ | c :: chil =>
+ case KM.peek indices c of
+ NONE =>
+ let
+ val callstack = (elt,chil) :: callstack
+ in
+ dfsVertex sccs callstack index indices lows stack c
+ end
+ | SOME cind =>
+ let
+ val lows =
+ if inStack c stack then reduceIndex lows (elt,cind)
+ else lows
+ in
+ dfsSuccessors sccs callstack index indices lows stack elt chil
+ end
+
+ fun dfsRoots sccs index indices lows elts =
+ case elts of
+ [] => sccs
+ | elt :: elts =>
+ if KM.inDomain elt indices then
+ dfsRoots sccs index indices lows elts
+ else
+ let
+ val callstack = []
+
+ val (sccs,index,indices,lows) =
+ dfsVertex sccs callstack index indices lows emptyStack elt
+ in
+ dfsRoots sccs index indices lows elts
+ end
+
+ val sccs = []
+ and index = 0
+ and indices = KM.new ()
+ and lows = KM.new ()
+ in
+ dfsRoots sccs index indices lows
+ end;
+in
+ fun preOrderSCC children roots =
+ let
+ val result = tarjan children (toList roots)
+
+(*BasicDebug
+ val () =
+ if subset roots (unionList result) then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.preOrderSCC: missing roots"
+
+ val () =
+ if preOrderedSCC children result then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.preOrderSCC: bad ordering"
+*)
+ in
+ result
+ end;
+
+ fun postOrderSCC children roots =
+ let
+ val result = List.rev (tarjan children (toList roots))
+
+(*BasicDebug
+ val () =
+ if subset roots (unionList result) then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.postOrderSCC: missing roots"
+
+ val () =
+ if postOrderedSCC children result then ()
+ else raise Metis_Useful.Bug "Metis_ElementSet.postOrderSCC: bad ordering"
+*)
+ in
+ result
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
(* Pretty-printing. *)
(* ------------------------------------------------------------------------- *)
@@ -5858,7 +6295,7 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Sharing =
@@ -5906,7 +6343,7 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Sharing :> Metis_Sharing =
@@ -6067,7 +6504,7 @@
(* ========================================================================= *)
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Stream =
@@ -6123,6 +6560,8 @@
val drop : int -> 'a stream -> 'a stream (* raises Subscript *)
+val unfold : ('b -> ('a * 'b) option) -> 'b -> 'a stream
+
(* ------------------------------------------------------------------------- *)
(* Metis_Stream versions of standard list operations: these might not terminate. *)
(* ------------------------------------------------------------------------- *)
@@ -6155,6 +6594,8 @@
(* Metis_Stream operations. *)
(* ------------------------------------------------------------------------- *)
+val primes : int stream
+
val memoize : 'a stream -> 'a stream
val listConcat : 'a list stream -> 'a stream
@@ -6179,7 +6620,7 @@
(* ========================================================================= *)
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Stream :> Metis_Stream =
@@ -6271,6 +6712,16 @@
fun drop n s = funpow n tl s handle Empty => raise Subscript;
+fun unfold f =
+ let
+ fun next b () =
+ case f b of
+ NONE => Nil
+ | SOME (a,b) => Cons (a, next b)
+ in
+ fn b => next b ()
+ end;
+
(* ------------------------------------------------------------------------- *)
(* Metis_Stream versions of standard list operations: these might not terminate. *)
(* ------------------------------------------------------------------------- *)
@@ -6360,6 +6811,13 @@
(* Metis_Stream operations. *)
(* ------------------------------------------------------------------------- *)
+val primes =
+ let
+ fun next s = SOME (Metis_Useful.nextSieve s)
+ in
+ unfold next Metis_Useful.initSieve
+ end;
+
fun memoize Nil = Nil
| memoize (Cons (h,t)) = Cons (h, Metis_Lazy.memoize (fn () => memoize (t ())));
@@ -6416,7 +6874,7 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Heap =
@@ -6450,7 +6908,7 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Heap :> Metis_Heap =
@@ -6530,7 +6988,7 @@
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Print =
@@ -6737,7 +7195,7 @@
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Print :> Metis_Print =
@@ -8285,12 +8743,17 @@
toStreamWithLineLength len ppA a
end;
-local
- val sep = mkWord " =";
-in
- fun trace ppX nameX x =
- Metis_Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
-end;
+fun trace ppX nameX =
+ let
+ fun ppNameX x =
+ consistentBlock 2
+ [ppString nameX,
+ ppString " =",
+ break,
+ ppX x]
+ in
+ fn x => Metis_Useful.trace (toString ppNameX x ^ "\n")
+ end;
end
@@ -8298,7 +8761,7 @@
(* ========================================================================= *)
(* PARSING *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Parse =
@@ -8415,7 +8878,7 @@
(* ========================================================================= *)
(* PARSING *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Parse :> Metis_Parse =
@@ -8689,7 +9152,7 @@
(* ========================================================================= *)
(* NAMES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Name =
@@ -8737,7 +9200,7 @@
(* ========================================================================= *)
(* NAMES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Name :> Metis_Name =
@@ -8837,7 +9300,7 @@
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_NameArity =
@@ -8887,7 +9350,7 @@
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_NameArity :> Metis_NameArity =
@@ -8982,7 +9445,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Term =
@@ -9172,7 +9635,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Term :> Metis_Term =
@@ -9913,7 +10376,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Subst =
@@ -10035,7 +10498,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Subst :> Metis_Subst =
@@ -10287,7 +10750,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Atom =
@@ -10431,7 +10894,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Atom :> Metis_Atom =
@@ -10682,7 +11145,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Formula =
@@ -10882,7 +11345,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Formula :> Metis_Formula =
@@ -11454,7 +11917,7 @@
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
+ split (f1 :: asms) false f2 @ split (Not f2 :: asms) true f1
| (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
(* Unsplittables *)
| _ => [add_asms asms (if pol then fm else Not fm)];
@@ -11486,7 +11949,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Literal =
@@ -11654,7 +12117,7 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Literal :> Metis_Literal =
@@ -11950,7 +12413,7 @@
(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Thm =
@@ -12101,7 +12564,7 @@
(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Thm :> Metis_Thm =
@@ -12318,7 +12781,7 @@
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Proof =
@@ -12382,7 +12845,7 @@
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Proof :> Metis_Proof =
@@ -12836,7 +13299,7 @@
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Rule =
@@ -13113,7 +13576,7 @@
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Rule :> Metis_Rule =
@@ -13891,7 +14354,7 @@
fun factor th =
let
- fun fact sub = removeSym (Metis_Thm.subst sub th)
+ fun fact sub = removeIrrefl (removeSym (Metis_Thm.subst sub th))
in
List.map fact (factor' (Metis_Thm.clause th))
end;
@@ -13902,7 +14365,7 @@
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Normalize =
@@ -13960,7 +14423,7 @@
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Normalize :> Metis_Normalize =
@@ -14608,14 +15071,24 @@
| Metis_Literal (_,lit) => Metis_Literal.toFormula lit
| And (_,_,s) => Metis_Formula.listMkConj (Metis_Set.transform form s)
| Or (_,_,s) => Metis_Formula.listMkDisj (Metis_Set.transform form s)
- | Xor (_,_,p,s) =>
- let
- val s = if p then negateLastElt s else s
- in
- Metis_Formula.listMkEquiv (Metis_Set.transform form s)
- end
+ | Xor (_,_,p,s) => xorForm p s
| Exists (_,_,n,f) => Metis_Formula.listMkExists (Metis_NameSet.toList n, form f)
- | Forall (_,_,n,f) => Metis_Formula.listMkForall (Metis_NameSet.toList n, form f);
+ | Forall (_,_,n,f) => Metis_Formula.listMkForall (Metis_NameSet.toList n, form f)
+
+ (* To convert a Xor set to an Iff list we need to know *)
+ (* whether the size of the set is even or odd: *)
+ (* *)
+ (* b XOR a = b <=> ~a *)
+ (* c XOR b XOR a = c <=> b <=> a *)
+ (* d XOR c XOR b XOR a = d <=> c <=> b <=> ~a *)
+ (* e XOR d XOR c XOR b XOR a = e <=> d <=> c <=> b <=> a *)
+ and xorForm p s =
+ let
+ val p = if Metis_Set.size s mod 2 = 0 then not p else p
+ val s = if p then s else negateLastElt s
+ in
+ Metis_Formula.listMkEquiv (Metis_Set.transform form s)
+ end;
in
val toFormula = form;
end;
@@ -15351,7 +15824,7 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Model =
@@ -15631,7 +16104,7 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Model :> Metis_Model =
@@ -16912,7 +17385,7 @@
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Problem =
@@ -16978,7 +17451,7 @@
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Problem :> Metis_Problem =
@@ -17141,7 +17614,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_TermNet =
@@ -17194,7 +17667,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_TermNet :> Metis_TermNet =
@@ -17652,7 +18125,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_AtomNet =
@@ -17703,7 +18176,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_AtomNet :> Metis_AtomNet =
@@ -17765,7 +18238,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_LiteralNet =
@@ -17818,7 +18291,7 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_LiteralNet :> Metis_LiteralNet =
@@ -17895,7 +18368,7 @@
(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Subsume =
@@ -17949,7 +18422,7 @@
(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Subsume :> Metis_Subsume =
@@ -18046,7 +18519,7 @@
fun size (Metis_Subsume {empty, unit, nonunit = {clauses,...}}) =
length empty + Metis_LiteralNet.size unit + Metis_IntMap.size clauses;
-
+
fun insert (Metis_Subsume {empty,unit,nonunit}) (cl',a) =
case sortClause cl' of
[] =>
@@ -18286,7 +18759,7 @@
(* ========================================================================= *)
(* THE KNUTH-BENDIX TERM ORDERING *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_KnuthBendixOrder =
@@ -18311,7 +18784,7 @@
(* ========================================================================= *)
(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_KnuthBendixOrder :> Metis_KnuthBendixOrder =
@@ -18513,7 +18986,7 @@
(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Rewrite =
@@ -18615,7 +19088,7 @@
(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Rewrite :> Metis_Rewrite =
@@ -18834,7 +19307,7 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Rewriting (the order must be a refinement of the rewrite order). *)
+(* Rewriting (the supplied order must be a refinement of the rewrite order). *)
(* ------------------------------------------------------------------------- *)
local
@@ -18904,34 +19377,35 @@
end
end;
-datatype neqConvs = NeqConvs of Metis_Rule.conv Metis_LiteralMap.map;
-
-val neqConvsEmpty = NeqConvs (Metis_LiteralMap.new ());
-
-fun neqConvsNull (NeqConvs m) = Metis_LiteralMap.null m;
-
-fun neqConvsAdd order (neq as NeqConvs m) lit =
+datatype neqConvs = NeqConvs of Metis_Rule.conv list;
+
+val neqConvsEmpty = NeqConvs [];
+
+fun neqConvsNull (NeqConvs l) = List.null l;
+
+fun neqConvsAdd order (neq as NeqConvs l) lit =
case total (mkNeqConv order) lit of
- NONE => NONE
- | SOME conv => SOME (NeqConvs (Metis_LiteralMap.insert m (lit,conv)));
+ NONE => neq
+ | SOME conv => NeqConvs (conv :: l);
fun mkNeqConvs order =
let
- fun add (lit,(neq,lits)) =
- case neqConvsAdd order neq lit of
- SOME neq => (neq,lits)
- | NONE => (neq, Metis_LiteralSet.add lits lit)
- in
- Metis_LiteralSet.foldl add (neqConvsEmpty,Metis_LiteralSet.empty)
- end;
-
-fun neqConvsDelete (NeqConvs m) lit = NeqConvs (Metis_LiteralMap.delete m lit);
-
-fun neqConvsToConv (NeqConvs m) =
- Metis_Rule.firstConv (Metis_LiteralMap.foldr (fn (_,c,l) => c :: l) [] m);
-
-fun neqConvsFoldl f b (NeqConvs m) =
- Metis_LiteralMap.foldl (fn (l,_,z) => f (l,z)) b m;
+ fun add (lit,neq) = neqConvsAdd order neq lit
+ in
+ Metis_LiteralSet.foldl add neqConvsEmpty
+ end;
+
+fun buildNeqConvs order lits =
+ let
+ fun add (lit,(neq,neqs)) = (neqConvsAdd order neq lit, (lit,neq) :: neqs)
+ in
+ snd (Metis_LiteralSet.foldl add (neqConvsEmpty,[]) lits)
+ end;
+
+fun neqConvsToConv (NeqConvs l) = Metis_Rule.firstConv l;
+
+fun neqConvsUnion (NeqConvs l1) (NeqConvs l2) =
+ NeqConvs (List.revAppend (l1,l2));
fun neqConvsRewrIdLiterule order known redexes id neq =
if Metis_IntMap.null known andalso neqConvsNull neq then Metis_Rule.allLiterule
@@ -18947,7 +19421,7 @@
fun rewriteIdEqn' order known redexes id (eqn as (l_r,th)) =
let
- val (neq,_) = mkNeqConvs order (Metis_Thm.clause th)
+ val neq = mkNeqConvs order (Metis_Thm.clause th)
val literule = neqConvsRewrIdLiterule order known redexes id neq
val (strongEqn,lit) =
case Metis_Rule.equationLiteral eqn of
@@ -18970,40 +19444,39 @@
let
val mk_literule = neqConvsRewrIdLiterule order known redexes id
- fun rewr_neq_lit (lit, acc as (changed,neq,lits,th)) =
- let
- val neq = neqConvsDelete neq lit
+ fun rewr_neq_lit ((lit,rneq),(changed,lneq,lits,th)) =
+ let
+ val neq = neqConvsUnion lneq rneq
val (lit',litTh) = mk_literule neq lit
- in
- if Metis_Literal.equal lit lit' then acc
- else
- let
- val th = Metis_Thm.resolve lit th litTh
- in
- case neqConvsAdd order neq lit' of
- SOME neq => (true,neq,lits,th)
- | NONE => (changed, neq, Metis_LiteralSet.add lits lit', th)
- end
- end
-
- fun rewr_neq_lits neq lits th =
- let
+ val lneq = neqConvsAdd order lneq lit'
+ val lits = Metis_LiteralSet.add lits lit'
+ in
+ if Metis_Literal.equal lit lit' then (changed,lneq,lits,th)
+ else (true, lneq, lits, Metis_Thm.resolve lit th litTh)
+ end
+
+ fun rewr_neq_lits lits th =
+ let
+ val neqs = buildNeqConvs order lits
+
+ val neq = neqConvsEmpty
+ val lits = Metis_LiteralSet.empty
+
val (changed,neq,lits,th) =
- neqConvsFoldl rewr_neq_lit (false,neq,lits,th) neq
- in
- if changed then rewr_neq_lits neq lits th
- else (neq,lits,th)
- end
-
- val (neq,lits) = mkNeqConvs order lits
-
- val (neq,lits,th) = rewr_neq_lits neq lits th
+ List.foldl rewr_neq_lit (false,neq,lits,th) neqs
+ in
+ if changed then rewr_neq_lits lits th else (neq,th)
+ end
+
+ val (neq,lits) = Metis_LiteralSet.partition Metis_Literal.isNeq lits
+
+ val (neq,th) = rewr_neq_lits neq th
val rewr_literule = mk_literule neq
fun rewr_lit (lit,th) =
- if Metis_Thm.member lit th then Metis_Rule.literalRule rewr_literule lit th
- else th
+ if not (Metis_Thm.member lit th) then th
+ else Metis_Rule.literalRule rewr_literule lit th
in
Metis_LiteralSet.foldl rewr_lit th lits
end;
@@ -19021,12 +19494,12 @@
(*MetisTrace6
val () = Metis_Print.trace Metis_Thm.pp "Metis_Rewrite.rewriteIdRule': result" result
*)
- val _ = not (thmReducible order known id result) orelse
- raise Bug "rewriteIdRule: should be normalized"
+ val () = if not (thmReducible order known id result) then ()
+ else raise Bug "Metis_Rewrite.rewriteIdRule': should be normalized"
in
result
end
- handle Error err => raise Error ("Metis_Rewrite.rewriteIdRule:\n" ^ err);
+ handle Error err => raise Error ("Metis_Rewrite.rewriteIdRule':\n" ^ err);
*)
fun rewrIdConv (Metis_Rewrite {known,redexes,...}) order =
@@ -19048,6 +19521,30 @@
fun rewriteIdRule (Metis_Rewrite {known,redexes,...}) order =
rewriteIdRule' order known redexes;
+(*MetisDebug
+val rewriteIdRule = fn rewr => fn order => fn id => fn th =>
+ let
+ val result = rewriteIdRule rewr order id th
+
+ val th' = rewriteIdRule rewr order id result
+
+ val () = if Metis_Thm.equal th' result then ()
+ else
+ let
+ fun trace p s = Metis_Print.trace p ("Metis_Rewrite.rewriteIdRule: "^s)
+ val () = trace pp "rewr" rewr
+ val () = trace Metis_Thm.pp "th" th
+ val () = trace Metis_Thm.pp "result" result
+ val () = trace Metis_Thm.pp "th'" th'
+ in
+ raise Bug "Metis_Rewrite.rewriteIdRule: should be idempotent"
+ end
+ in
+ result
+ end
+ handle Error err => raise Error ("Metis_Rewrite.rewriteIdRule:\n" ^ err);
+*)
+
fun rewriteRule rewrite order = rewriteIdRule rewrite order ~1;
(* ------------------------------------------------------------------------- *)
@@ -19303,7 +19800,7 @@
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Units =
@@ -19355,7 +19852,7 @@
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Units :> Metis_Units =
@@ -19464,7 +19961,7 @@
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Clause =
@@ -19574,7 +20071,7 @@
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Clause :> Metis_Clause =
@@ -19792,38 +20289,43 @@
fun reduce units (Metis_Clause {parameters,id,thm}) =
Metis_Clause {parameters = parameters, id = id, thm = Metis_Units.reduce units thm};
-fun rewrite rewr (cl as Metis_Clause {parameters,id,thm}) =
- let
- fun simp th =
- let
- val {ordering,...} = parameters
- val cmp = Metis_KnuthBendixOrder.compare ordering
- in
- Metis_Rewrite.rewriteIdRule rewr cmp id th
- end
+local
+ fun simp rewr (parm : parameters) id th =
+ let
+ val {ordering,...} = parm
+ val cmp = Metis_KnuthBendixOrder.compare ordering
+ in
+ Metis_Rewrite.rewriteIdRule rewr cmp id th
+ end;
+in
+ fun rewrite rewr cl =
+ let
+ val Metis_Clause {parameters = parm, id, thm = th} = cl
(*MetisTrace4
- val () = Metis_Print.trace Metis_Rewrite.pp "Metis_Clause.rewrite: rewr" rewr
- val () = Metis_Print.trace Metis_Print.ppInt "Metis_Clause.rewrite: id" id
- val () = Metis_Print.trace pp "Metis_Clause.rewrite: cl" cl
-*)
-
- val thm =
- case Metis_Rewrite.peek rewr id of
- NONE => simp thm
- | SOME ((_,thm),_) => if Metis_Rewrite.isReduced rewr then thm else simp thm
-
- val result = Metis_Clause {parameters = parameters, id = id, thm = thm}
+ val () = Metis_Print.trace Metis_Rewrite.pp "Metis_Clause.rewrite: rewr" rewr
+ val () = Metis_Print.trace Metis_Print.ppInt "Metis_Clause.rewrite: id" id
+ val () = Metis_Print.trace pp "Metis_Clause.rewrite: cl" cl
+*)
+
+ val th =
+ case Metis_Rewrite.peek rewr id of
+ NONE => simp rewr parm id th
+ | SOME ((_,th),_) =>
+ if Metis_Rewrite.isReduced rewr then th else simp rewr parm id th
+
+ val result = Metis_Clause {parameters = parm, id = id, thm = th}
(*MetisTrace4
- val () = Metis_Print.trace pp "Metis_Clause.rewrite: result" result
-*)
- in
- result
- end
+ val () = Metis_Print.trace pp "Metis_Clause.rewrite: result" result
+*)
+ in
+ result
+ end
(*MetisDebug
- handle Error err => raise Error ("Metis_Clause.rewrite:\n" ^ err);
-*)
+ handle Error err => raise Error ("Metis_Clause.rewrite:\n" ^ err);
+*)
+end;
(* ------------------------------------------------------------------------- *)
(* Inference rules: these generate new clause ids. *)
@@ -19946,7 +20448,7 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Active =
@@ -20004,7 +20506,7 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Active :> Metis_Active =
@@ -20156,9 +20658,9 @@
let
fun simp cl =
case Metis_Clause.simplify cl of
- NONE => true
+ NONE => true (* tautology case *)
| SOME cl =>
- Metis_Subsume.isStrictlySubsumed subsume (Metis_Clause.literals cl) orelse
+ Metis_Subsume.isSubsumed subsume (Metis_Clause.literals cl) orelse
let
val cl' = cl
val cl' = Metis_Clause.reduce reduce cl'
@@ -20398,9 +20900,11 @@
(*MetisDebug
val simplify = fn simp => fn units => fn rewr => fn subs => fn cl =>
let
- fun traceCl s = Metis_Print.trace Metis_Clause.pp ("Metis_Active.simplify: " ^ s)
+ val ppClOpt = Metis_Print.ppOption Metis_Clause.pp
+ fun trace pp s = Metis_Print.trace pp ("Metis_Active.simplify: " ^ s)
+ val traceCl = trace Metis_Clause.pp
+ val traceClOpt = trace ppClOpt
(*MetisTrace4
- val ppClOpt = Metis_Print.ppOption Metis_Clause.pp
val () = traceCl "cl" cl
*)
val cl' = simplify simp units rewr subs cl
@@ -20420,8 +20924,14 @@
NONE => ()
| SOME (e,f) =>
let
+ val () = Metis_Print.trace Metis_Rewrite.pp "Metis_Active.simplify: rewr" rewr
+ val () = Metis_Print.trace Metis_Units.pp "Metis_Active.simplify: units" units
+ val () = Metis_Print.trace Metis_Subsume.pp "Metis_Active.simplify: subs" subs
val () = traceCl "cl" cl
val () = traceCl "cl'" cl'
+ val () = traceClOpt "simplify cl'" (Metis_Clause.simplify cl')
+ val () = traceCl "rewrite cl'" (Metis_Clause.rewrite rewr cl')
+ val () = traceCl "reduce cl'" (Metis_Clause.reduce units cl')
val () = f ()
in
raise
@@ -20820,34 +21330,42 @@
sortMap utility Int.compare
end;
- fun factor_add (cl, active_subsume_acc as (active,subsume,acc)) =
+ fun post_factor (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,_)) =
+ | SOME cl' =>
+ if Metis_Clause.equalThms cl' cl then
+ let
+ val active = addFactorClause active cl
+ and subsume = addSubsume subsume cl
+ and acc = cl :: acc
+ in
+ (active,subsume,acc)
+ end
+ else
+ (* If the clause was changed in the post-factor simplification *)
+ (* step, then it may have altered the set of largest literals *)
+ (* in the clause. The safest thing to do is to factor again. *)
+ factor1 cl' active_subsume_acc
+
+ and factor1 cl active_subsume_acc =
+ let
+ val cls = sort_utilitywise (cl :: Metis_Clause.factor cl)
+ in
+ List.foldl post_factor active_subsume_acc cls
+ end;
+
+ fun pre_factor (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 :: Metis_Clause.factor cl)
- in
- List.foldl factor_add active_subsume_acc cls
- end;
+ | SOME cl => factor1 cl active_subsume_acc;
fun factor' active acc [] = (active, List.rev acc)
| factor' active acc cls =
let
val cls = sort_utilitywise cls
val subsume = getSubsume active
- val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls
+ val (active,_,acc) = List.foldl pre_factor (active,subsume,acc) cls
val (active,cls) = extract_rewritables active
in
factor' active acc cls
@@ -20919,7 +21437,7 @@
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Waiting =
@@ -20999,7 +21517,7 @@
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Waiting :> Metis_Waiting =
@@ -21293,7 +21811,7 @@
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Resolution =
@@ -21347,7 +21865,7 @@
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Resolution :> Metis_Resolution =
--- a/src/Tools/Metis/scripts/mlpp Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/scripts/mlpp Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
#!/usr/bin/perl
-# Copyright (c) 2006 Joe Hurd, distributed under the BSD License
+# Copyright (c) 2006 Joe Leslie-Hurd, distributed under the BSD License
use strict;
use warnings;
@@ -72,19 +72,7 @@
my $text = shift @_;
if ($opt_c eq "mosml") {
- $text =~ s/Array\.copy/Array_copy/g;
- $text =~ s/Array\.foldli/Array_foldli/g;
- $text =~ s/Array\.foldri/Array_foldri/g;
- $text =~ s/Array\.modifyi/Array_modifyi/g;
- $text =~ s/OS\.Process\.isSuccess/OS_Process_isSuccess/g;
- $text =~ s/PP\.ppstream/ppstream/g;
- $text =~ s/String\.concatWith/String_concatWith/g;
- $text =~ s/String\.isSubstring/String_isSubstring/g;
- $text =~ s/String\.isSuffix/String_isSuffix/g;
- $text =~ s/Substring\.full/Substring_full/g;
- $text =~ s/TextIO\.inputLine/TextIO_inputLine/g;
- $text =~ s/Vector\.foldli/Vector_foldli/g;
- $text =~ s/Vector\.mapi/Vector_mapi/g;
+ $text =~ s/Real\.isFinite/Real_isFinite/g;
}
print STDOUT $text;
@@ -300,7 +288,7 @@
=head1 AUTHORS
-Joe Hurd <joe@gilith.com>
+Joe Leslie-Hurd <joe@gilith.com>
=head1 SEE ALSO
--- a/src/Tools/Metis/src/Active.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Active.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Active =
--- a/src/Tools/Metis/src/Active.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Active.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Active :> Active =
@@ -152,9 +152,9 @@
let
fun simp cl =
case Clause.simplify cl of
- NONE => true
+ NONE => true (* tautology case *)
| SOME cl =>
- Subsume.isStrictlySubsumed subsume (Clause.literals cl) orelse
+ Subsume.isSubsumed subsume (Clause.literals cl) orelse
let
val cl' = cl
val cl' = Clause.reduce reduce cl'
@@ -394,9 +394,11 @@
(*MetisDebug
val simplify = fn simp => fn units => fn rewr => fn subs => fn cl =>
let
- fun traceCl s = Print.trace Clause.pp ("Active.simplify: " ^ s)
+ val ppClOpt = Print.ppOption Clause.pp
+ fun trace pp s = Print.trace pp ("Active.simplify: " ^ s)
+ val traceCl = trace Clause.pp
+ val traceClOpt = trace ppClOpt
(*MetisTrace4
- val ppClOpt = Print.ppOption Clause.pp
val () = traceCl "cl" cl
*)
val cl' = simplify simp units rewr subs cl
@@ -416,8 +418,14 @@
NONE => ()
| SOME (e,f) =>
let
+ val () = Print.trace Rewrite.pp "Active.simplify: rewr" rewr
+ val () = Print.trace Units.pp "Active.simplify: units" units
+ val () = Print.trace Subsume.pp "Active.simplify: subs" subs
val () = traceCl "cl" cl
val () = traceCl "cl'" cl'
+ val () = traceClOpt "simplify cl'" (Clause.simplify cl')
+ val () = traceCl "rewrite cl'" (Clause.rewrite rewr cl')
+ val () = traceCl "reduce cl'" (Clause.reduce units cl')
val () = f ()
in
raise
@@ -816,34 +824,42 @@
sortMap utility Int.compare
end;
- fun factor_add (cl, active_subsume_acc as (active,subsume,acc)) =
+ fun post_factor (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;
+ | SOME cl' =>
+ if Clause.equalThms cl' cl then
+ let
+ val active = addFactorClause active cl
+ and subsume = addSubsume subsume cl
+ and acc = cl :: acc
+ in
+ (active,subsume,acc)
+ end
+ else
+ (* If the clause was changed in the post-factor simplification *)
+ (* step, then it may have altered the set of largest literals *)
+ (* in the clause. The safest thing to do is to factor again. *)
+ factor1 cl' active_subsume_acc
- fun factor1 (cl, active_subsume_acc as (active,subsume,_)) =
+ and factor1 cl active_subsume_acc =
+ let
+ val cls = sort_utilitywise (cl :: Clause.factor cl)
+ in
+ List.foldl post_factor active_subsume_acc cls
+ end;
+
+ fun pre_factor (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
- List.foldl factor_add active_subsume_acc cls
- end;
+ | SOME cl => factor1 cl active_subsume_acc;
fun factor' active acc [] = (active, List.rev acc)
| factor' active acc cls =
let
val cls = sort_utilitywise cls
val subsume = getSubsume active
- val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls
+ val (active,_,acc) = List.foldl pre_factor (active,subsume,acc) cls
val (active,cls) = extract_rewritables active
in
factor' active acc cls
--- a/src/Tools/Metis/src/Atom.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Atom.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Atom =
--- a/src/Tools/Metis/src/Atom.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Atom.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Atom :> Atom =
--- a/src/Tools/Metis/src/AtomNet.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/AtomNet.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature AtomNet =
--- a/src/Tools/Metis/src/AtomNet.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/AtomNet.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure AtomNet :> AtomNet =
--- a/src/Tools/Metis/src/Clause.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Clause.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Clause =
--- a/src/Tools/Metis/src/Clause.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Clause.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Clause :> Clause =
@@ -218,38 +218,43 @@
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
+local
+ fun simp rewr (parm : parameters) id th =
+ let
+ val {ordering,...} = parm
+ val cmp = KnuthBendixOrder.compare ordering
+ in
+ Rewrite.rewriteIdRule rewr cmp id th
+ end;
+in
+ fun rewrite rewr cl =
+ let
+ val Clause {parameters = parm, id, thm = th} = cl
(*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 () = 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 th =
+ case Rewrite.peek rewr id of
+ NONE => simp rewr parm id th
+ | SOME ((_,th),_) =>
+ if Rewrite.isReduced rewr then th else simp rewr parm id th
- val result = Clause {parameters = parameters, id = id, thm = thm}
+ val result = Clause {parameters = parm, id = id, thm = th}
(*MetisTrace4
- val () = Print.trace pp "Clause.rewrite: result" result
+ val () = Print.trace pp "Clause.rewrite: result" result
*)
- in
- result
- end
+ in
+ result
+ end
(*MetisDebug
- handle Error err => raise Error ("Clause.rewrite:\n" ^ err);
+ handle Error err => raise Error ("Clause.rewrite:\n" ^ err);
*)
+end;
(* ------------------------------------------------------------------------- *)
(* Inference rules: these generate new clause ids. *)
--- a/src/Tools/Metis/src/ElementSet.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/ElementSet.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature ElementSet =
@@ -135,9 +135,11 @@
val disjoint : set -> set -> bool
(* ------------------------------------------------------------------------- *)
-(* Closing under an operation. *)
+(* Pointwise operations. *)
(* ------------------------------------------------------------------------- *)
+val lift : (element -> set) -> set -> set
+
val closedAdd : (element -> set) -> set -> set -> set
val close : (element -> set) -> set -> set
@@ -165,6 +167,34 @@
val domain : 'a map -> set
(* ------------------------------------------------------------------------- *)
+(* Depth-first search. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ordering =
+ Linear of element list
+ | Cycle of element list
+
+val preOrder : (element -> set) -> set -> ordering
+
+val postOrder : (element -> set) -> set -> ordering
+
+val preOrdered : (element -> set) -> element list -> bool
+
+val postOrdered : (element -> set) -> element list -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Strongly connected components. *)
+(* ------------------------------------------------------------------------- *)
+
+val preOrderSCC : (element -> set) -> set -> set list
+
+val postOrderSCC : (element -> set) -> set -> set list
+
+val preOrderedSCC : (element -> set) -> set list -> bool
+
+val postOrderedSCC : (element -> set) -> set list -> bool
+
+(* ------------------------------------------------------------------------- *)
(* Pretty-printing. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/ElementSet.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/ElementSet.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
functor ElementSet (
@@ -302,9 +302,16 @@
fun disjoint (Set m1) (Set m2) = KM.disjointDomain m1 m2;
(* ------------------------------------------------------------------------- *)
-(* Closing under an operation. *)
+(* Pointwise operations. *)
(* ------------------------------------------------------------------------- *)
+fun lift f =
+ let
+ fun inc (elt,set) = union set (f elt)
+ in
+ foldl inc empty
+ end;
+
fun closedAdd f =
let
fun adds acc set = foldl check acc set
@@ -336,6 +343,324 @@
fun fromList elts = addList empty elts;
(* ------------------------------------------------------------------------- *)
+(* Depth-first search. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ordering =
+ Linear of element list
+ | Cycle of element list;
+
+fun postOrdered children =
+ let
+ fun check acc elts =
+ case elts of
+ [] => true
+ | elt :: elts =>
+ not (member elt acc) andalso
+ let
+ val acc = closedAdd children acc (singleton elt)
+ in
+ check acc elts
+ end
+ in
+ check empty
+ end;
+
+fun preOrdered children elts = postOrdered children (List.rev elts);
+
+local
+ fun takeStackset elt =
+ let
+ fun notElement (e,_,_) = not (equalElement e elt)
+ in
+ Useful.takeWhile notElement
+ end;
+
+ fun consElement ((e,_,_),el) = e :: el;
+
+ fun depthFirstSearch children =
+ let
+ fun traverse (dealt,dealtset) (stack,stackset) work =
+ case work of
+ [] =>
+ (case stack of
+ [] => Linear dealt
+ | (elt,work,stackset) :: stack =>
+ let
+ val dealt = elt :: dealt
+
+ val dealtset = add dealtset elt
+ in
+ traverse (dealt,dealtset) (stack,stackset) work
+ end)
+ | elt :: work =>
+ if member elt dealtset then
+ traverse (dealt,dealtset) (stack,stackset) work
+ else if member elt stackset then
+ let
+ val cycle = takeStackset elt stack
+
+ val cycle = elt :: List.foldl consElement [elt] cycle
+ in
+ Cycle cycle
+ end
+ else
+ let
+ val stack = (elt,work,stackset) :: stack
+
+ val stackset = add stackset elt
+
+ val work = toList (children elt)
+ in
+ traverse (dealt,dealtset) (stack,stackset) work
+ end
+
+ val dealt = []
+ and dealtset = empty
+ and stack = []
+ and stackset = empty
+ in
+ traverse (dealt,dealtset) (stack,stackset)
+ end;
+in
+ fun preOrder children roots =
+ let
+ val result = depthFirstSearch children (toList roots)
+
+(*BasicDebug
+ val () =
+ case result of
+ Cycle _ => ()
+ | Linear l =>
+ let
+ val () =
+ if subset roots (fromList l) then ()
+ else raise Useful.Bug "ElementSet.preOrder: missing roots"
+
+ val () =
+ if preOrdered children l then ()
+ else raise Useful.Bug "ElementSet.preOrder: bad ordering"
+ in
+ ()
+ end
+*)
+ in
+ result
+ end;
+
+ fun postOrder children roots =
+ case depthFirstSearch children (toList roots) of
+ Linear l =>
+ let
+ val l = List.rev l
+
+(*BasicDebug
+ val () =
+ if subset roots (fromList l) then ()
+ else raise Useful.Bug "ElementSet.postOrder: missing roots"
+
+ val () =
+ if postOrdered children l then ()
+ else raise Useful.Bug "ElementSet.postOrder: bad ordering"
+*)
+ in
+ Linear l
+ end
+ | cycle => cycle;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Strongly connected components. *)
+(* ------------------------------------------------------------------------- *)
+
+fun postOrderedSCC children =
+ let
+ fun check acc eltsl =
+ case eltsl of
+ [] => true
+ | elts :: eltsl =>
+ not (null elts) andalso
+ disjoint elts acc andalso
+ let
+ fun addElt elt = closedAdd children acc (singleton elt)
+
+ val (root,elts) = deletePick elts
+
+ fun checkElt elt = member root (addElt elt)
+ in
+ all checkElt elts andalso
+ let
+ val acc = addElt root
+ in
+ subset elts acc andalso
+ check acc eltsl
+ end
+ end
+ in
+ check empty
+ end;
+
+fun preOrderedSCC children eltsl = postOrderedSCC children (List.rev eltsl);
+
+(* An implementation of Tarjan's algorithm: *)
+
+(* http://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm *)
+
+local
+ datatype stackSCC = StackSCC of set * (element * set) list;
+
+ val emptyStack = StackSCC (empty,[]);
+
+ fun pushStack (StackSCC (elts,eltl)) elt =
+ StackSCC (add elts elt, (elt,elts) :: eltl);
+
+ fun inStack elt (StackSCC (elts,_)) = member elt elts;
+
+ fun popStack root =
+ let
+ fun pop scc eltl =
+ case eltl of
+ [] => raise Useful.Bug "ElementSet.popStack"
+ | (elt,elts) :: eltl =>
+ let
+ val scc = add scc elt
+ in
+ if equalElement elt root then (scc, StackSCC (elts,eltl))
+ else pop scc eltl
+ end
+ in
+ fn sccs => fn StackSCC (_,eltl) =>
+ let
+ val (scc,stack) = pop empty eltl
+ in
+ (scc :: sccs, stack)
+ end
+ end;
+
+ fun getIndex indices e : int =
+ case KM.peek indices e of
+ SOME i => i
+ | NONE => raise Useful.Bug "ElementSet.getIndex";
+
+ fun isRoot indices lows e = getIndex indices e = getIndex lows e;
+
+ fun reduceIndex indices (e,i) =
+ let
+ val j = getIndex indices e
+ in
+ if j <= i then indices else KM.insert indices (e,i)
+ end;
+
+ fun tarjan children =
+ let
+ fun dfsVertex sccs callstack index indices lows stack elt =
+ let
+ val indices = KM.insert indices (elt,index)
+ and lows = KM.insert lows (elt,index)
+
+ val index = index + 1
+
+ val stack = pushStack stack elt
+
+ val chil = toList (children elt)
+ in
+ dfsSuccessors sccs callstack index indices lows stack elt chil
+ end
+
+ and dfsSuccessors sccs callstack index indices lows stack elt chil =
+ case chil of
+ [] =>
+ let
+ val (sccs,stack) =
+ if isRoot indices lows elt then popStack elt sccs stack
+ else (sccs,stack)
+ in
+ case callstack of
+ [] => (sccs,index,indices,lows)
+ | (p,elts) :: callstack =>
+ let
+ val lows = reduceIndex lows (p, getIndex lows elt)
+ in
+ dfsSuccessors sccs callstack index indices lows stack p elts
+ end
+ end
+ | c :: chil =>
+ case KM.peek indices c of
+ NONE =>
+ let
+ val callstack = (elt,chil) :: callstack
+ in
+ dfsVertex sccs callstack index indices lows stack c
+ end
+ | SOME cind =>
+ let
+ val lows =
+ if inStack c stack then reduceIndex lows (elt,cind)
+ else lows
+ in
+ dfsSuccessors sccs callstack index indices lows stack elt chil
+ end
+
+ fun dfsRoots sccs index indices lows elts =
+ case elts of
+ [] => sccs
+ | elt :: elts =>
+ if KM.inDomain elt indices then
+ dfsRoots sccs index indices lows elts
+ else
+ let
+ val callstack = []
+
+ val (sccs,index,indices,lows) =
+ dfsVertex sccs callstack index indices lows emptyStack elt
+ in
+ dfsRoots sccs index indices lows elts
+ end
+
+ val sccs = []
+ and index = 0
+ and indices = KM.new ()
+ and lows = KM.new ()
+ in
+ dfsRoots sccs index indices lows
+ end;
+in
+ fun preOrderSCC children roots =
+ let
+ val result = tarjan children (toList roots)
+
+(*BasicDebug
+ val () =
+ if subset roots (unionList result) then ()
+ else raise Useful.Bug "ElementSet.preOrderSCC: missing roots"
+
+ val () =
+ if preOrderedSCC children result then ()
+ else raise Useful.Bug "ElementSet.preOrderSCC: bad ordering"
+*)
+ in
+ result
+ end;
+
+ fun postOrderSCC children roots =
+ let
+ val result = List.rev (tarjan children (toList roots))
+
+(*BasicDebug
+ val () =
+ if subset roots (unionList result) then ()
+ else raise Useful.Bug "ElementSet.postOrderSCC: missing roots"
+
+ val () =
+ if postOrderedSCC children result then ()
+ else raise Useful.Bug "ElementSet.postOrderSCC: bad ordering"
+*)
+ in
+ result
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
(* Pretty-printing. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Formula.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Formula.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Formula =
--- a/src/Tools/Metis/src/Formula.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Formula.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Formula :> Formula =
@@ -572,7 +572,7 @@
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
+ split (f1 :: asms) false f2 @ split (Not f2 :: asms) true f1
| (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
(* Unsplittables *)
| _ => [add_asms asms (if pol then fm else Not fm)];
--- a/src/Tools/Metis/src/Heap.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Heap.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Heap =
--- a/src/Tools/Metis/src/Heap.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Heap.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Heap :> Heap =
--- a/src/Tools/Metis/src/KeyMap.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/KeyMap.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature KeyMap =
--- a/src/Tools/Metis/src/KeyMap.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/KeyMap.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
--- a/src/Tools/Metis/src/KnuthBendixOrder.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE KNUTH-BENDIX TERM ORDERING *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature KnuthBendixOrder =
--- a/src/Tools/Metis/src/KnuthBendixOrder.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure KnuthBendixOrder :> KnuthBendixOrder =
--- a/src/Tools/Metis/src/Lazy.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Lazy.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Lazy =
--- a/src/Tools/Metis/src/Lazy.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Lazy.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Lazy :> Lazy =
--- a/src/Tools/Metis/src/Literal.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Literal.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Literal =
--- a/src/Tools/Metis/src/Literal.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Literal.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Literal :> Literal =
--- a/src/Tools/Metis/src/LiteralNet.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/LiteralNet.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature LiteralNet =
--- a/src/Tools/Metis/src/LiteralNet.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/LiteralNet.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure LiteralNet :> LiteralNet =
--- a/src/Tools/Metis/src/Map.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Map.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Map =
--- a/src/Tools/Metis/src/Map.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Map.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Map :> Map =
--- a/src/Tools/Metis/src/Model.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Model.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Model =
--- a/src/Tools/Metis/src/Model.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Model.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Model :> Model =
--- a/src/Tools/Metis/src/Name.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Name.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAMES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Name =
--- a/src/Tools/Metis/src/Name.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Name.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAMES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Name :> Name =
--- a/src/Tools/Metis/src/NameArity.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/NameArity.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature NameArity =
--- a/src/Tools/Metis/src/NameArity.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/NameArity.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure NameArity :> NameArity =
--- a/src/Tools/Metis/src/Normalize.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Normalize.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Normalize =
--- a/src/Tools/Metis/src/Normalize.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Normalize.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Normalize :> Normalize =
@@ -648,14 +648,24 @@
| Literal (_,lit) => Literal.toFormula lit
| And (_,_,s) => Formula.listMkConj (Set.transform form s)
| Or (_,_,s) => Formula.listMkDisj (Set.transform form s)
- | Xor (_,_,p,s) =>
- let
- val s = if p then negateLastElt s else s
- in
- Formula.listMkEquiv (Set.transform form s)
- end
+ | Xor (_,_,p,s) => xorForm p s
| Exists (_,_,n,f) => Formula.listMkExists (NameSet.toList n, form f)
- | Forall (_,_,n,f) => Formula.listMkForall (NameSet.toList n, form f);
+ | Forall (_,_,n,f) => Formula.listMkForall (NameSet.toList n, form f)
+
+ (* To convert a Xor set to an Iff list we need to know *)
+ (* whether the size of the set is even or odd: *)
+ (* *)
+ (* b XOR a = b <=> ~a *)
+ (* c XOR b XOR a = c <=> b <=> a *)
+ (* d XOR c XOR b XOR a = d <=> c <=> b <=> ~a *)
+ (* e XOR d XOR c XOR b XOR a = e <=> d <=> c <=> b <=> a *)
+ and xorForm p s =
+ let
+ val p = if Set.size s mod 2 = 0 then not p else p
+ val s = if p then s else negateLastElt s
+ in
+ Formula.listMkEquiv (Set.transform form s)
+ end;
in
val toFormula = form;
end;
--- a/src/Tools/Metis/src/Options.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Options.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROCESSING COMMAND LINE OPTIONS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Options =
--- a/src/Tools/Metis/src/Options.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Options.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROCESSING COMMAND LINE OPTIONS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Options :> Options =
--- a/src/Tools/Metis/src/Ordered.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Ordered.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Ordered =
--- a/src/Tools/Metis/src/Ordered.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Ordered.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure IntOrdered =
--- a/src/Tools/Metis/src/Parse.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Parse.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PARSING *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Parse =
--- a/src/Tools/Metis/src/Parse.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Parse.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PARSING *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Parse :> Parse =
--- a/src/Tools/Metis/src/Portable.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Portable.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ML COMPILER SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Portable =
--- a/src/Tools/Metis/src/PortableMlton.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/PortableMlton.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MLTON SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Portable :> Portable =
--- a/src/Tools/Metis/src/PortableMosml.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/PortableMosml.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MOSCOW ML SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Portable :> Portable =
@@ -85,99 +85,4 @@
(* Ad-hoc upgrading of the Moscow ML basis library. *)
(* ------------------------------------------------------------------------- *)
-fun Array_copy {src,dst,di} =
- let
- open Array
- in
- copy {src = src, si = 0, len = NONE, dst = dst, di = di}
- end;
-
-fun Array_foldli f b v =
- let
- open Array
- in
- foldli f b (v,0,NONE)
- end;
-
-fun Array_foldri f b v =
- let
- open Array
- in
- foldri f b (v,0,NONE)
- end;
-
-fun Array_modifyi f a =
- let
- open Array
- in
- modifyi f (a,0,NONE)
- end;
-
-fun OS_Process_isSuccess s = s = OS.Process.success;
-
-fun String_concatWith s =
- let
- fun add (x,l) = s :: x :: l
- in
- fn [] => ""
- | x :: xs =>
- let
- val xs = List.foldl add [] (List.rev xs)
- in
- String.concat (x :: xs)
- end
- end;
-
-fun String_isSubstring p s =
- let
- val sizeP = size p
- and sizeS = size s
- in
- if sizeP > sizeS then false
- else if sizeP = sizeS then p = s
- else
- let
- fun check i = String.substring (s,i,sizeP) = p
-
- fun checkn i = check i orelse (i > 0 andalso checkn (i - 1))
- in
- checkn (sizeS - sizeP)
- end
- end;
-
-fun String_isSuffix p s =
- let
- val sizeP = size p
- and sizeS = size s
- in
- sizeP <= sizeS andalso
- String.extract (s, sizeS - sizeP, NONE) = p
- end;
-
-fun Substring_full s =
- let
- open Substring
- in
- all s
- end;
-
-fun TextIO_inputLine h =
- let
- open TextIO
- in
- case inputLine h of "" => NONE | s => SOME s
- end;
-
-fun Vector_foldli f b v =
- let
- open Vector
- in
- foldli f b (v,0,NONE)
- end;
-
-fun Vector_mapi f v =
- let
- open Vector
- in
- mapi f (v,0,NONE)
- end;
+fun Real_isFinite (_ : real) = true;
--- a/src/Tools/Metis/src/PortablePolyml.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/PortablePolyml.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* POLY/ML SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Portable :> Portable =
--- a/src/Tools/Metis/src/Print.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Print.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Print =
--- a/src/Tools/Metis/src/Print.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Print.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Print :> Print =
@@ -1548,11 +1548,16 @@
toStreamWithLineLength len ppA a
end;
-local
- val sep = mkWord " =";
-in
- fun trace ppX nameX x =
- Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
-end;
+fun trace ppX nameX =
+ let
+ fun ppNameX x =
+ consistentBlock 2
+ [ppString nameX,
+ ppString " =",
+ break,
+ ppX x]
+ in
+ fn x => Useful.trace (toString ppNameX x ^ "\n")
+ end;
end
--- a/src/Tools/Metis/src/Problem.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Problem.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Problem =
--- a/src/Tools/Metis/src/Problem.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Problem.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Problem :> Problem =
--- a/src/Tools/Metis/src/Proof.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Proof.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Proof =
--- a/src/Tools/Metis/src/Proof.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Proof.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Proof :> Proof =
--- a/src/Tools/Metis/src/Resolution.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Resolution.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Resolution =
--- a/src/Tools/Metis/src/Resolution.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Resolution.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Resolution :> Resolution =
--- a/src/Tools/Metis/src/Rewrite.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Rewrite.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Rewrite =
--- a/src/Tools/Metis/src/Rewrite.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Rewrite.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Rewrite :> Rewrite =
@@ -219,7 +219,7 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Rewriting (the order must be a refinement of the rewrite order). *)
+(* Rewriting (the supplied order must be a refinement of the rewrite order). *)
(* ------------------------------------------------------------------------- *)
local
@@ -289,34 +289,35 @@
end
end;
-datatype neqConvs = NeqConvs of Rule.conv LiteralMap.map;
+datatype neqConvs = NeqConvs of Rule.conv list;
-val neqConvsEmpty = NeqConvs (LiteralMap.new ());
+val neqConvsEmpty = NeqConvs [];
-fun neqConvsNull (NeqConvs m) = LiteralMap.null m;
+fun neqConvsNull (NeqConvs l) = List.null l;
-fun neqConvsAdd order (neq as NeqConvs m) lit =
+fun neqConvsAdd order (neq as NeqConvs l) lit =
case total (mkNeqConv order) lit of
- NONE => NONE
- | SOME conv => SOME (NeqConvs (LiteralMap.insert m (lit,conv)));
+ NONE => neq
+ | SOME conv => NeqConvs (conv :: l);
fun mkNeqConvs order =
let
- fun add (lit,(neq,lits)) =
- case neqConvsAdd order neq lit of
- SOME neq => (neq,lits)
- | NONE => (neq, LiteralSet.add lits lit)
+ fun add (lit,neq) = neqConvsAdd order neq lit
in
- LiteralSet.foldl add (neqConvsEmpty,LiteralSet.empty)
+ LiteralSet.foldl add neqConvsEmpty
end;
-fun neqConvsDelete (NeqConvs m) lit = NeqConvs (LiteralMap.delete m lit);
+fun buildNeqConvs order lits =
+ let
+ fun add (lit,(neq,neqs)) = (neqConvsAdd order neq lit, (lit,neq) :: neqs)
+ in
+ snd (LiteralSet.foldl add (neqConvsEmpty,[]) lits)
+ end;
-fun neqConvsToConv (NeqConvs m) =
- Rule.firstConv (LiteralMap.foldr (fn (_,c,l) => c :: l) [] m);
+fun neqConvsToConv (NeqConvs l) = Rule.firstConv l;
-fun neqConvsFoldl f b (NeqConvs m) =
- LiteralMap.foldl (fn (l,_,z) => f (l,z)) b m;
+fun neqConvsUnion (NeqConvs l1) (NeqConvs l2) =
+ NeqConvs (List.revAppend (l1,l2));
fun neqConvsRewrIdLiterule order known redexes id neq =
if IntMap.null known andalso neqConvsNull neq then Rule.allLiterule
@@ -332,7 +333,7 @@
fun rewriteIdEqn' order known redexes id (eqn as (l_r,th)) =
let
- val (neq,_) = mkNeqConvs order (Thm.clause th)
+ val neq = mkNeqConvs order (Thm.clause th)
val literule = neqConvsRewrIdLiterule order known redexes id neq
val (strongEqn,lit) =
case Rule.equationLiteral eqn of
@@ -355,40 +356,39 @@
let
val mk_literule = neqConvsRewrIdLiterule order known redexes id
- fun rewr_neq_lit (lit, acc as (changed,neq,lits,th)) =
+ fun rewr_neq_lit ((lit,rneq),(changed,lneq,lits,th)) =
let
- val neq = neqConvsDelete neq lit
+ val neq = neqConvsUnion lneq rneq
val (lit',litTh) = mk_literule neq lit
+ val lneq = neqConvsAdd order lneq lit'
+ val lits = LiteralSet.add lits lit'
in
- if Literal.equal lit lit' then acc
- else
- let
- val th = Thm.resolve lit th litTh
- in
- case neqConvsAdd order neq lit' of
- SOME neq => (true,neq,lits,th)
- | NONE => (changed, neq, LiteralSet.add lits lit', th)
- end
+ if Literal.equal lit lit' then (changed,lneq,lits,th)
+ else (true, lneq, lits, Thm.resolve lit th litTh)
end
- fun rewr_neq_lits neq lits th =
+ fun rewr_neq_lits lits th =
let
+ val neqs = buildNeqConvs order lits
+
+ val neq = neqConvsEmpty
+ val lits = LiteralSet.empty
+
val (changed,neq,lits,th) =
- neqConvsFoldl rewr_neq_lit (false,neq,lits,th) neq
+ List.foldl rewr_neq_lit (false,neq,lits,th) neqs
in
- if changed then rewr_neq_lits neq lits th
- else (neq,lits,th)
+ if changed then rewr_neq_lits lits th else (neq,th)
end
- val (neq,lits) = mkNeqConvs order lits
+ val (neq,lits) = LiteralSet.partition Literal.isNeq lits
- val (neq,lits,th) = rewr_neq_lits neq lits th
+ val (neq,th) = rewr_neq_lits neq th
val rewr_literule = mk_literule neq
fun rewr_lit (lit,th) =
- if Thm.member lit th then Rule.literalRule rewr_literule lit th
- else th
+ if not (Thm.member lit th) then th
+ else Rule.literalRule rewr_literule lit th
in
LiteralSet.foldl rewr_lit th lits
end;
@@ -406,12 +406,12 @@
(*MetisTrace6
val () = Print.trace Thm.pp "Rewrite.rewriteIdRule': result" result
*)
- val _ = not (thmReducible order known id result) orelse
- raise Bug "rewriteIdRule: should be normalized"
+ val () = if not (thmReducible order known id result) then ()
+ else raise Bug "Rewrite.rewriteIdRule': should be normalized"
in
result
end
- handle Error err => raise Error ("Rewrite.rewriteIdRule:\n" ^ err);
+ handle Error err => raise Error ("Rewrite.rewriteIdRule':\n" ^ err);
*)
fun rewrIdConv (Rewrite {known,redexes,...}) order =
@@ -433,6 +433,30 @@
fun rewriteIdRule (Rewrite {known,redexes,...}) order =
rewriteIdRule' order known redexes;
+(*MetisDebug
+val rewriteIdRule = fn rewr => fn order => fn id => fn th =>
+ let
+ val result = rewriteIdRule rewr order id th
+
+ val th' = rewriteIdRule rewr order id result
+
+ val () = if Thm.equal th' result then ()
+ else
+ let
+ fun trace p s = Print.trace p ("Rewrite.rewriteIdRule: "^s)
+ val () = trace pp "rewr" rewr
+ val () = trace Thm.pp "th" th
+ val () = trace Thm.pp "result" result
+ val () = trace Thm.pp "th'" th'
+ in
+ raise Bug "Rewrite.rewriteIdRule: should be idempotent"
+ end
+ in
+ result
+ end
+ handle Error err => raise Error ("Rewrite.rewriteIdRule:\n" ^ err);
+*)
+
fun rewriteRule rewrite order = rewriteIdRule rewrite order ~1;
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Rule.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Rule.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Rule =
--- a/src/Tools/Metis/src/Rule.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Rule.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Rule :> Rule =
@@ -778,7 +778,7 @@
fun factor th =
let
- fun fact sub = removeSym (Thm.subst sub th)
+ fun fact sub = removeIrrefl (removeSym (Thm.subst sub th))
in
List.map fact (factor' (Thm.clause th))
end;
--- a/src/Tools/Metis/src/Set.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Set.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Set =
--- a/src/Tools/Metis/src/Set.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Set.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Set :> Set =
--- a/src/Tools/Metis/src/Sharing.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Sharing.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Sharing =
--- a/src/Tools/Metis/src/Sharing.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Sharing.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Sharing :> Sharing =
--- a/src/Tools/Metis/src/Stream.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Stream.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Stream =
@@ -56,6 +56,8 @@
val drop : int -> 'a stream -> 'a stream (* raises Subscript *)
+val unfold : ('b -> ('a * 'b) option) -> 'b -> 'a stream
+
(* ------------------------------------------------------------------------- *)
(* Stream versions of standard list operations: these might not terminate. *)
(* ------------------------------------------------------------------------- *)
@@ -88,6 +90,8 @@
(* Stream operations. *)
(* ------------------------------------------------------------------------- *)
+val primes : int stream
+
val memoize : 'a stream -> 'a stream
val listConcat : 'a list stream -> 'a stream
--- a/src/Tools/Metis/src/Stream.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Stream.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Stream :> Stream =
@@ -92,6 +92,16 @@
fun drop n s = funpow n tl s handle Empty => raise Subscript;
+fun unfold f =
+ let
+ fun next b () =
+ case f b of
+ NONE => Nil
+ | SOME (a,b) => Cons (a, next b)
+ in
+ fn b => next b ()
+ end;
+
(* ------------------------------------------------------------------------- *)
(* Stream versions of standard list operations: these might not terminate. *)
(* ------------------------------------------------------------------------- *)
@@ -181,6 +191,13 @@
(* Stream operations. *)
(* ------------------------------------------------------------------------- *)
+val primes =
+ let
+ fun next s = SOME (Useful.nextSieve s)
+ in
+ unfold next Useful.initSieve
+ end;
+
fun memoize Nil = Nil
| memoize (Cons (h,t)) = Cons (h, Lazy.memoize (fn () => memoize (t ())));
--- a/src/Tools/Metis/src/Subst.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Subst.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Subst =
--- a/src/Tools/Metis/src/Subst.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Subst.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Subst :> Subst =
--- a/src/Tools/Metis/src/Subsume.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Subsume.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Subsume =
--- a/src/Tools/Metis/src/Subsume.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Subsume.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Subsume :> Subsume =
@@ -97,7 +97,7 @@
fun size (Subsume {empty, unit, nonunit = {clauses,...}}) =
length empty + LiteralNet.size unit + IntMap.size clauses;
-
+
fun insert (Subsume {empty,unit,nonunit}) (cl',a) =
case sortClause cl' of
[] =>
--- a/src/Tools/Metis/src/Term.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Term.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Term =
--- a/src/Tools/Metis/src/Term.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Term.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Term :> Term =
--- a/src/Tools/Metis/src/TermNet.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/TermNet.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature TermNet =
--- a/src/Tools/Metis/src/TermNet.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/TermNet.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure TermNet :> TermNet =
--- a/src/Tools/Metis/src/Thm.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Thm.sig Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Thm =
--- a/src/Tools/Metis/src/Thm.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Thm.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Thm :> Thm =
--- a/src/Tools/Metis/src/Tptp.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Tptp.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE TPTP PROBLEM FILE FORMAT *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Tptp =
@@ -103,13 +103,23 @@
| FofFormulaBody of Formula.formula
(* ------------------------------------------------------------------------- *)
+(* Extra TPTP inferences. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype inference =
+ StripInference
+ | NegateInference
+
+val nameInference : inference -> string
+
+(* ------------------------------------------------------------------------- *)
(* TPTP formula sources. *)
(* ------------------------------------------------------------------------- *)
datatype formulaSource =
NoFormulaSource
| StripFormulaSource of
- {inference : string,
+ {inference : inference,
parents : formulaName list}
| NormalizeFormulaSource of
{inference : Normalize.inference,
--- a/src/Tools/Metis/src/Tptp.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Tptp.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE TPTP PROBLEM FILE FORMAT *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Tptp :> Tptp =
@@ -886,13 +886,26 @@
| FofFormulaBody fm => ppFof mapping (Formula.generalize fm);
(* ------------------------------------------------------------------------- *)
+(* Extra TPTP inferences. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype inference =
+ StripInference
+ | NegateInference;
+
+fun nameInference inf =
+ case inf of
+ StripInference => "strip"
+ | NegateInference => "negate";
+
+(* ------------------------------------------------------------------------- *)
(* TPTP formula sources. *)
(* ------------------------------------------------------------------------- *)
datatype formulaSource =
NoFormulaSource
| StripFormulaSource of
- {inference : string,
+ {inference : inference,
parents : formulaName list}
| NormalizeFormulaSource of
{inference : Normalize.inference,
@@ -983,8 +996,6 @@
val GEN_INFERENCE = "inference"
and GEN_INTRODUCED = "introduced";
- fun nameStrip inf = inf;
-
fun ppStrip mapping inf = Print.skip;
fun nameNormalize inf =
@@ -1075,7 +1086,7 @@
let
val gen = GEN_INFERENCE
- val name = nameStrip inference
+ val name = nameInference inference
in
Print.inconsistentBlock (size gen + 1)
[Print.ppString gen,
@@ -1315,7 +1326,7 @@
(fn ((),((),s)) => "$$" ^ s);
val nameParser =
- (stringParser || numberParser || quoteParser) >> FormulaName;
+ (lowerParser || numberParser || quoteParser) >> FormulaName;
val roleParser = lowerParser >> fromStringRole;
@@ -2043,46 +2054,79 @@
end;
local
- datatype blockComment =
- OutsideBlockComment
+ datatype comment =
+ NoComment
+ | EnteringLineComment
+ | InsideLineComment
| EnteringBlockComment
| InsideBlockComment
- | LeavingBlockComment;
-
- fun stripLineComments acc strm =
+ | LeavingBlockComment
+ | InsideSingleQuoteComment
+ | EscapedSingleQuoteComment;
+
+ fun stripInitialLineComments acc strm =
case strm of
Stream.Nil => (List.rev acc, Stream.Nil)
| Stream.Cons (line,rest) =>
case total destLineComment line of
- SOME s => stripLineComments (s :: acc) (rest ())
- | NONE => (List.rev acc, Stream.filter (not o isLineComment) strm);
-
- fun advanceBlockComment c state =
+ SOME s => stripInitialLineComments (s :: acc) (rest ())
+ | NONE => (List.rev acc, strm);
+
+ fun advanceComment c state =
case state of
- OutsideBlockComment =>
- if c = #"/" then (Stream.Nil, EnteringBlockComment)
- else (Stream.singleton c, OutsideBlockComment)
+ NoComment =>
+ (case c of
+ #"\n" => (Stream.Nil, EnteringLineComment)
+ | #"/" => (Stream.Nil, EnteringBlockComment)
+ | #"'" => (Stream.singleton #"'", InsideSingleQuoteComment)
+ | _ => (Stream.singleton c, NoComment))
+ | EnteringLineComment =>
+ (case c of
+ #"%" => (Stream.singleton #"\n", InsideLineComment)
+ | #"\n" => (Stream.singleton #"\n", EnteringLineComment)
+ | #"/" => (Stream.singleton #"\n", EnteringBlockComment)
+ | #"'" => (Stream.fromList [#"\n",#"'"], InsideSingleQuoteComment)
+ | _ => (Stream.fromList [#"\n",c], NoComment))
+ | InsideLineComment =>
+ (case c of
+ #"\n" => (Stream.Nil, EnteringLineComment)
+ | _ => (Stream.Nil, InsideLineComment))
| EnteringBlockComment =>
- if c = #"*" then (Stream.Nil, InsideBlockComment)
- else if c = #"/" then (Stream.singleton #"/", EnteringBlockComment)
- else (Stream.fromList [#"/",c], OutsideBlockComment)
+ (case c of
+ #"*" => (Stream.Nil, InsideBlockComment)
+ | #"\n" => (Stream.singleton #"/", EnteringLineComment)
+ | #"/" => (Stream.singleton #"/", EnteringBlockComment)
+ | #"'" => (Stream.fromList [#"/",#"'"], InsideSingleQuoteComment)
+ | _ => (Stream.fromList [#"/",c], NoComment))
| InsideBlockComment =>
- if c = #"*" then (Stream.Nil, LeavingBlockComment)
- else (Stream.Nil, InsideBlockComment)
+ (case c of
+ #"*" => (Stream.Nil, LeavingBlockComment)
+ | _ => (Stream.Nil, InsideBlockComment))
| LeavingBlockComment =>
- if c = #"/" then (Stream.Nil, OutsideBlockComment)
- else if c = #"*" then (Stream.Nil, LeavingBlockComment)
- else (Stream.Nil, InsideBlockComment);
-
- fun eofBlockComment state =
+ (case c of
+ #"/" => (Stream.Nil, NoComment)
+ | #"*" => (Stream.Nil, LeavingBlockComment)
+ | _ => (Stream.Nil, InsideBlockComment))
+ | InsideSingleQuoteComment =>
+ (case c of
+ #"'" => (Stream.singleton #"'", NoComment)
+ | #"\\" => (Stream.singleton #"\\", EscapedSingleQuoteComment)
+ | _ => (Stream.singleton c, InsideSingleQuoteComment))
+ | EscapedSingleQuoteComment =>
+ (Stream.singleton c, InsideSingleQuoteComment);
+
+ fun eofComment state =
case state of
- OutsideBlockComment => Stream.Nil
+ NoComment => Stream.Nil
+ | EnteringLineComment => Stream.singleton #"\n"
+ | InsideLineComment => Stream.Nil
| EnteringBlockComment => Stream.singleton #"/"
- | _ => raise Error "EOF inside a block comment";
-
- val stripBlockComments =
- Stream.mapsConcat advanceBlockComment eofBlockComment
- OutsideBlockComment;
+ | InsideBlockComment => raise Error "EOF inside a block comment"
+ | LeavingBlockComment => raise Error "EOF inside a block comment"
+ | InsideSingleQuoteComment => raise Error "EOF inside a single quote"
+ | EscapedSingleQuoteComment => raise Error "EOF inside a single quote";
+
+ val stripComments = Stream.mapsConcat advanceComment eofComment NoComment;
in
fun read {mapping,filename} =
let
@@ -2095,11 +2139,11 @@
(let
(* The character stream *)
- val (comments,chars) = stripLineComments [] chars
+ val (comments,chars) = stripInitialLineComments [] chars
val chars = Parse.everything Parse.any chars
- val chars = stripBlockComments chars
+ val chars = stripComments chars
(* The declaration stream *)
@@ -2347,7 +2391,7 @@
val source =
StripFormulaSource
- {inference = "strip",
+ {inference = StripInference,
parents = pars}
val formula =
@@ -2487,7 +2531,7 @@
let
val source =
StripFormulaSource
- {inference = "negate",
+ {inference = NegateInference,
parents = [name]}
val prefix = "negate_" ^ Int.toString number ^ "_"
--- a/src/Tools/Metis/src/Units.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Units.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Units =
--- a/src/Tools/Metis/src/Units.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Units.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Units :> Units =
--- a/src/Tools/Metis/src/Useful.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Useful.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Useful =
@@ -203,6 +203,20 @@
val gcd : int -> int -> int
+(* Primes *)
+
+type sieve
+
+val initSieve : sieve
+
+val maxSieve : sieve -> int
+
+val primesSieve : sieve -> int list
+
+val incSieve : sieve -> bool * sieve
+
+val nextSieve : sieve -> int * sieve
+
val primes : int -> int list
val primesUpTo : int -> int list
--- a/src/Tools/Metis/src/Useful.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Useful.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Useful :> Useful =
@@ -474,33 +474,99 @@
end;
end;
+(* Primes *)
+
+datatype sieve =
+ Sieve of
+ {max : int,
+ primes : (int * (int * int)) list};
+
+val initSieve =
+ let
+ val n = 1
+ and ps = []
+ in
+ Sieve
+ {max = n,
+ primes = ps}
+ end;
+
+fun maxSieve (Sieve {max = n, ...}) = n;
+
+fun primesSieve (Sieve {primes = ps, ...}) = List.map fst ps;
+
+fun incSieve sieve =
+ let
+ val n = maxSieve sieve + 1
+
+ fun add i ps =
+ case ps of
+ [] => (true,[(n,(0,0))])
+ | (p,(k,j)) :: ps =>
+ let
+ val k = (k + i) mod p
+
+ val j = j + i
+ in
+ if k = 0 then (false, (p,(k,j)) :: ps)
+ else
+ let
+ val (b,ps) = add j ps
+ in
+ (b, (p,(k,0)) :: ps)
+ end
+ end
+
+ val Sieve {primes = ps, ...} = sieve
+
+ val (b,ps) = add 1 ps
+
+ val sieve =
+ Sieve
+ {max = n,
+ primes = ps}
+ in
+ (b,sieve)
+ end;
+
+fun nextSieve sieve =
+ let
+ val (b,sieve) = incSieve sieve
+ in
+ if b then (maxSieve sieve, sieve)
+ else nextSieve sieve
+ end;
+
local
- 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
- calcPrimes mode ps i n
- end;
+ fun inc s =
+ let
+ val (_,s) = incSieve s
+ in
+ s
+ end;
in
- fun primes n =
- if n <= 0 then []
- else calcPrimes true [2] 3 (n - 1);
+ fun primesUpTo m =
+ if m <= 1 then []
+ else primesSieve (funpow (m - 1) inc initSieve);
+end;
- fun primesUpTo n =
- if n < 2 then []
- else calcPrimes false [2] 3 (n - 2);
-end;
+val primes =
+ let
+ fun next s n =
+ if n <= 0 then []
+ else
+ let
+ val (p,s) = nextSieve s
+
+ val n = n - 1
+
+ val ps = next s n
+ in
+ p :: ps
+ end
+ in
+ next initSieve
+ end;
(* ------------------------------------------------------------------------- *)
(* Strings. *)
@@ -847,7 +913,9 @@
fun timed f a =
let
val tmr = Timer.startCPUTimer ()
+
val res = f a
+
val {usr,sys,...} = Timer.checkCPUTimer tmr
in
(Time.toReal usr + Time.toReal sys, res)
--- a/src/Tools/Metis/src/Waiting.sig Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Waiting.sig Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Waiting =
--- a/src/Tools/Metis/src/Waiting.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Waiting.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Waiting :> Waiting =
--- a/src/Tools/Metis/src/metis.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/metis.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* METIS FIRST ORDER PROVER *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
open Useful;
@@ -11,9 +11,9 @@
val PROGRAM = "metis";
-val VERSION = "2.3";
+val VERSION = "2.4";
-val versionString = PROGRAM^" "^VERSION^" (release 20110926)"^"\n";
+val versionString = PROGRAM^" "^VERSION^" (release 20180810)"^"\n";
(* ------------------------------------------------------------------------- *)
(* Program options. *)
@@ -157,7 +157,7 @@
local
fun display_sep () =
if notshowing_any () then ()
- else TextIO.print (nChars #"-" (!Print.lineLength) ^ "\n");
+ else TextIO.print (nChars #"%" (!Print.lineLength) ^ "\n");
fun display_name filename =
if notshowing "name" then ()
@@ -204,7 +204,7 @@
local
fun display_proof_start filename =
- TextIO.print ("\nSZS output start CNFRefutation for " ^ filename ^ "\n");
+ TextIO.print ("\n% SZS output start CNFRefutation for " ^ filename ^ "\n");
fun display_proof_body problem proofs =
let
@@ -235,7 +235,7 @@
end;
fun display_proof_end filename =
- TextIO.print ("SZS output end CNFRefutation for " ^ filename ^ "\n\n");
+ TextIO.print ("% SZS output end CNFRefutation for " ^ filename ^ "\n\n");
in
fun display_proof filename problem proofs =
if notshowing "proof" then ()
@@ -291,7 +291,7 @@
fun display_status filename status =
if notshowing "status" then ()
else
- TextIO.print ("SZS status " ^ Tptp.toStringStatus status ^
+ TextIO.print ("% SZS status " ^ Tptp.toStringStatus status ^
" for " ^ filename ^ "\n");
fun display_problem filename cls =
--- a/src/Tools/Metis/src/problems.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/problems.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
(* ========================================================================= *)
@@ -218,7 +218,7 @@
{name = "SPLIT_NOT_IFF",
comments = ["A way to split a goal that looks like ~(p <=> q)"],
goal = `
-~(p <=> q) <=> (p ==> ~q) /\ (q ==> ~p)`},
+~(p <=> q) <=> (p ==> ~q) /\ (~q ==> p)`},
(* ------------------------------------------------------------------------- *)
(* Monadic Predicate Logic. *)
--- a/src/Tools/Metis/src/problems2tptp.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/problems2tptp.sml Thu Jul 09 11:39:16 2020 +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 Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
open Useful;
--- a/src/Tools/Metis/src/selftest.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/selftest.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* METIS TESTS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)
@@ -65,6 +65,7 @@
and pvFm = printval Formula.pp
and pvFms = printval (Print.ppList Formula.pp)
and pvThm = printval Thm.pp
+and pvThms = printval (Print.ppList Thm.pp)
and pvEqn : Rule.equation -> Rule.equation = printval (Print.ppMap snd Thm.pp)
and pvNet = printval (LiteralNet.pp Print.ppInt)
and pvRw = printval Rewrite.pp
@@ -483,6 +484,27 @@
val ax = pvThm (AX [`~(a = b)`, `~(b = c)`, `~(c = d)`, `a = d`]);
val th = pvThm (try (Rewrite.orderedRewrite kboCmp []) ax);
+(* Bug discovered by Michael Farber *)
+
+val eqns = [Q`f $x = c`];
+val ax = pvThm (AX [`~(f $y = g a b)`,`p (g a b)`]);
+val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax);
+
+val eqns = [Q`even (numeral c) = d`,
+ Q`f (numeral c) $x = $x`];
+val ax = pvThm
+ (AX [`~(even (numeral c) = even $y)`,
+ `p (even (f (numeral c) $y))`]);
+val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax);
+
+val eqns = [Q`even (numeral c) = d`,
+ Q`f (numeral c) $x = $x`,
+ Q`g a b = numeral c`];
+val ax = pvThm
+ (AX [`~(even (numeral c) = even $y)`,
+ `p (even (f (g a b) $y))`]);
+val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax);
+
(* ------------------------------------------------------------------------- *)
val () = SAY "Unit cache";
(* ------------------------------------------------------------------------- *)
@@ -500,6 +522,11 @@
val _ = pvFm (nnf (F`p /\ ~p`));
val _ = pvFm (nnf (F`(!x. P x) ==> ((?y. Q y) <=> (?z. P z /\ Q z))`));
val _ = pvFm (nnf (F`~(~(p <=> q) <=> r) <=> ~(p <=> ~(q <=> r))`));
+val _ = pvFm (nnf (F`~((((p <=> q) <=> r) /\ (q <=> r)) ==> p)`));
+val _ = pvFm (nnf (F`p <=> q`));
+val _ = pvFm (nnf (F`p <=> q <=> r`));
+val _ = pvFm (nnf (F`p <=> q <=> r <=> s`));
+val _ = pvFm (nnf (F`p <=> q <=> r <=> s <=> t`));
(* ------------------------------------------------------------------------- *)
val () = SAY "Conjunctive normal form";
@@ -1064,6 +1091,27 @@
`$y <= exp $x`]);
val _ = pvLits (Clause.largestLiterals cl);
+(* Bug discovered by Michael Farber *)
+
+local
+ fun activeFactor th =
+ let
+ val (_,{axioms,conjecture}) =
+ Active.new Active.default {axioms = [], conjecture = [th]}
+ in
+ List.map Clause.thm (axioms @ conjecture)
+ end;
+in
+ val th = pvThm (AX[`c4 (c5 (c6 c7 c8) $y) $z = c3`,
+ `c4 (c5 (c6 c7 c8) $t) $u = c3`]);
+ val _ = pvThms (activeFactor th);
+
+ val th = pvThm (AX[`~(c4 (c5 (c6 c7 c8) c28) c29 = c4 (c5 (c6 c7 c8) c28) $x)`,
+ `c4 (c5 (c6 c7 c8) $y) $z = c3`,
+ `c4 (c5 (c6 c7 c8) $t) $u = c3`]);
+ val _ = pvThms (activeFactor th);
+end;
+
(* ------------------------------------------------------------------------- *)
val () = SAY "Syntax checking the problem sets";
(* ------------------------------------------------------------------------- *)