# HG changeset patch # User desharna # Date 1632389449 -7200 # Node ID 6ab3116a251a51880bd74feeb37cee656ab98961 # Parent 41d009462d3cbafc13805e485cbb0853585cc62c updated to Metis 2.4 (release 20200713) diff -r 41d009462d3c -r 6ab3116a251a src/Tools/Metis/README --- 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 diff -r 41d009462d3c -r 6ab3116a251a src/Tools/Metis/metis.ML --- 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 => diff -r 41d009462d3c -r 6ab3116a251a src/Tools/Metis/src/Active.sml --- 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 => diff -r 41d009462d3c -r 6ab3116a251a src/Tools/Metis/src/Rewrite.sml --- 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 = diff -r 41d009462d3c -r 6ab3116a251a src/Tools/Metis/src/Thm.sml --- 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); *) (* ------------------------------------------------------------------------- *) diff -r 41d009462d3c -r 6ab3116a251a src/Tools/Metis/src/metis.sml --- 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. *) diff -r 41d009462d3c -r 6ab3116a251a src/Tools/Metis/src/selftest.sml --- 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"; (* ------------------------------------------------------------------------- *)