--- a/src/Tools/Metis/README Wed Sep 22 22:28:56 2021 +0200
+++ b/src/Tools/Metis/README Thu Sep 23 11:30:49 2021 +0200
@@ -7,7 +7,8 @@
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).
+ updated to Metis 2.4 (release 20180810) and later again to Metis 2.4
+ (release 20200713).
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
@@ -55,3 +56,4 @@
Martin Desharnais
9 July 2020
+ 23 September 2021
--- a/src/Tools/Metis/metis.ML Wed Sep 22 22:28:56 2021 +0200
+++ b/src/Tools/Metis/metis.ML Thu Sep 23 11:30:49 2021 +0200
@@ -12742,7 +12742,11 @@
handle Error err =>
raise Error ("Metis_Thm.resolve:\nlit = " ^ Metis_Literal.toString lit ^
"\npos = " ^ toString pos ^
- "\nneg = " ^ toString neg ^ "\n" ^ err);
+ "\nneg = " ^ toString neg ^ "\n" ^ err)
+ | Bug bug =>
+ raise Bug ("Metis_Thm.resolve:\nlit = " ^ Metis_Literal.toString lit ^
+ "\npos = " ^ toString pos ^
+ "\nneg = " ^ toString neg ^ "\n" ^ bug);
*)
(* ------------------------------------------------------------------------- *)
@@ -19452,7 +19456,8 @@
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)
+ else (true, lneq, lits,
+ if Metis_Thm.member lit th then Metis_Thm.resolve lit th litTh else th)
end
fun rewr_neq_lits lits th =
@@ -19499,7 +19504,12 @@
in
result
end
- handle Error err => raise Error ("Metis_Rewrite.rewriteIdRule':\n" ^ err);
+ handle Error err =>
+ raise Error ("Metis_Rewrite.rewriteIdRule':\n" ^
+ "th = " ^ Metis_Thm.toString th ^ "\n" ^ err)
+ | Bug bug =>
+ raise Bug ("Metis_Rewrite.rewriteIdRule':\n" ^
+ "th = " ^ Metis_Thm.toString th ^ "\n" ^ bug);
*)
fun rewrIdConv (Metis_Rewrite {known,redexes,...}) order =
@@ -20880,7 +20890,26 @@
let
val cl' = Metis_Clause.rewrite rewr cl
in
- if Metis_Clause.equalThms cl cl' then SOME cl else Metis_Clause.simplify cl'
+ if Metis_Clause.equalThms cl cl' then SOME cl
+ else
+ case Metis_Clause.simplify cl' of
+ NONE => NONE
+ | SOME cl'' =>
+ (* *)
+ (* Post-rewrite simplification can enable more rewrites: *)
+ (* *)
+ (* ~(X = f(X)) \/ ~(g(Y) = f(X)) \/ ~(c = f(X)) *)
+ (* ---------------------------------------------- rewrite *)
+ (* ~(X = f(X)) \/ ~(g(Y) = X) \/ ~(c = X) *)
+ (* ---------------------------------------------- simplify *)
+ (* ~(g(Y) = f(g(Y))) \/ ~(c = g(Y)) *)
+ (* ---------------------------------------------- rewrite *)
+ (* ~(c = f(c)) \/ ~(c = g(Y)) *)
+ (* *)
+ (* This was first observed in a bug discovered by Martin *)
+ (* Desharnais and Jasmin Blanchett *)
+ (* *)
+ if Metis_Clause.equalThms cl' cl'' then SOME cl' else rewrite cl''
end
in
fn cl =>
--- a/src/Tools/Metis/src/Active.sml Wed Sep 22 22:28:56 2021 +0200
+++ b/src/Tools/Metis/src/Active.sml Thu Sep 23 11:30:49 2021 +0200
@@ -374,7 +374,26 @@
let
val cl' = Clause.rewrite rewr cl
in
- if Clause.equalThms cl cl' then SOME cl else Clause.simplify cl'
+ if Clause.equalThms cl cl' then SOME cl
+ else
+ case Clause.simplify cl' of
+ NONE => NONE
+ | SOME cl'' =>
+ (* *)
+ (* Post-rewrite simplification can enable more rewrites: *)
+ (* *)
+ (* ~(X = f(X)) \/ ~(g(Y) = f(X)) \/ ~(c = f(X)) *)
+ (* ---------------------------------------------- rewrite *)
+ (* ~(X = f(X)) \/ ~(g(Y) = X) \/ ~(c = X) *)
+ (* ---------------------------------------------- simplify *)
+ (* ~(g(Y) = f(g(Y))) \/ ~(c = g(Y)) *)
+ (* ---------------------------------------------- rewrite *)
+ (* ~(c = f(c)) \/ ~(c = g(Y)) *)
+ (* *)
+ (* This was first observed in a bug discovered by Martin *)
+ (* Desharnais and Jasmin Blanchett *)
+ (* *)
+ if Clause.equalThms cl' cl'' then SOME cl' else rewrite cl''
end
in
fn cl =>
--- a/src/Tools/Metis/src/Rewrite.sml Wed Sep 22 22:28:56 2021 +0200
+++ b/src/Tools/Metis/src/Rewrite.sml Thu Sep 23 11:30:49 2021 +0200
@@ -364,7 +364,8 @@
val lits = LiteralSet.add lits lit'
in
if Literal.equal lit lit' then (changed,lneq,lits,th)
- else (true, lneq, lits, Thm.resolve lit th litTh)
+ else (true, lneq, lits,
+ if Thm.member lit th then Thm.resolve lit th litTh else th)
end
fun rewr_neq_lits lits th =
@@ -411,7 +412,12 @@
in
result
end
- handle Error err => raise Error ("Rewrite.rewriteIdRule':\n" ^ err);
+ handle Error err =>
+ raise Error ("Rewrite.rewriteIdRule':\n" ^
+ "th = " ^ Thm.toString th ^ "\n" ^ err)
+ | Bug bug =>
+ raise Bug ("Rewrite.rewriteIdRule':\n" ^
+ "th = " ^ Thm.toString th ^ "\n" ^ bug);
*)
fun rewrIdConv (Rewrite {known,redexes,...}) order =
--- a/src/Tools/Metis/src/Thm.sml Wed Sep 22 22:28:56 2021 +0200
+++ b/src/Tools/Metis/src/Thm.sml Thu Sep 23 11:30:49 2021 +0200
@@ -178,7 +178,11 @@
handle Error err =>
raise Error ("Thm.resolve:\nlit = " ^ Literal.toString lit ^
"\npos = " ^ toString pos ^
- "\nneg = " ^ toString neg ^ "\n" ^ err);
+ "\nneg = " ^ toString neg ^ "\n" ^ err)
+ | Bug bug =>
+ raise Bug ("Thm.resolve:\nlit = " ^ Literal.toString lit ^
+ "\npos = " ^ toString pos ^
+ "\nneg = " ^ toString neg ^ "\n" ^ bug);
*)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/metis.sml Wed Sep 22 22:28:56 2021 +0200
+++ b/src/Tools/Metis/src/metis.sml Thu Sep 23 11:30:49 2021 +0200
@@ -13,7 +13,7 @@
val VERSION = "2.4";
-val versionString = PROGRAM^" "^VERSION^" (release 20180810)"^"\n";
+val versionString = PROGRAM^" "^VERSION^" (release 20200713)"^"\n";
(* ------------------------------------------------------------------------- *)
(* Program options. *)
--- a/src/Tools/Metis/src/selftest.sml Wed Sep 22 22:28:56 2021 +0200
+++ b/src/Tools/Metis/src/selftest.sml Thu Sep 23 11:30:49 2021 +0200
@@ -505,6 +505,16 @@
`p (even (f (g a b) $y))`]);
val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax);
+(* Bug discovered by Martin Desharnais and Jasmin Blanchett *)
+
+val eqns = [];
+val ax = pvThm (AX [`~(a = f (g b))`,
+ `~(f a = f $x)`,
+ `~(f (g b) = g c)`,
+ `~(g c = f $x)`,
+ `~(g c = f a)`]);
+val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax);
+
(* ------------------------------------------------------------------------- *)
val () = SAY "Unit cache";
(* ------------------------------------------------------------------------- *)