From 1edf9e337401ad9a2e70da425cd5d7db47631aae Mon Sep 17 00:00:00 2001 From: Reviewer Date: Sun, 17 Jul 2022 18:42:14 +0700 Subject: [PATCH 1/2] Improve minimize * speed. See issue #10. --- src/metamath.c | 119 ++++++++++++++++++++++++++++++++++++------------- 1 file changed, 89 insertions(+), 30 deletions(-) diff --git a/src/metamath.c b/src/metamath.c index ed7c206d..e357404d 100644 --- a/src/metamath.c +++ b/src/metamath.c @@ -5150,6 +5150,92 @@ void command(int argc, char *argv[]) { print2("Bytes refer to compressed proof size, " "steps to uncompressed length.\n"); + /* Clear tmp for all math tokens */ + for (k = 0; k < g_mathTokens; k++) + g_MathToken[k].tmp = 0; + + long step, mlen; + nmbrString *mString; + + /* Set tmp to 1 for math tokens present in the proof */ + m = nmbrLen(g_ProofInProgress.proof); + for (step = 0; step < m; step++) { + mString = (g_ProofInProgress.target)[step]; + mlen = nmbrLen(mString); + + for (i = 0; i < mlen; i++) { + g_MathToken[mString[i]].tmp = 1; + } + } + + /* usefulStatements is a boolean array, where usefulStatements[k] == 1 + iff statement k might be useful in minimization */ + char *usefulStatements; + usefulStatements = poolMalloc(g_proveStatement*sizeof(char)); + long usefulCount = 0; + + /* Fill the usefulStatements array */ + for (k = 1; k < g_proveStatement; k++) { + usefulStatements[k] = 1; + + if (!mathboxFlag && k >= g_mathboxStmt && k < thisMathboxStartStmt) { + usefulStatements[k] = 0; + continue; + } + + if (g_Statement[k].type != (char)p_ && g_Statement[k].type != (char)a_) { + usefulStatements[k] = 0; + continue; + } + if (!matchesList(g_Statement[k].labelName, g_fullArg[1], '*', '?')) { + usefulStatements[k] = 0; + continue; + } + + if (exceptPos != 0) { + /* Skip any match to the EXCEPT argument */ + if (matchesList(g_Statement[k].labelName, g_fullArg[exceptPos + 1], + '*', '?')) { + usefulStatements[k] = 0; + continue; + } + } + + if (forbidMatchList[0]) { /* User provided a /FORBID list */ + /* First, we check to make sure we're not trying a statement + in the forbidMatchList directly (traceProof() won't find + this) */ + if (matchesList(g_Statement[k].labelName, forbidMatchList, '*', '?')) { + usefulStatements[k] = 0; + continue; + } + } + + /* Check to see if statement comment specified a usage + restriction */ + if (!overrideFlag) { + if (getMarkupFlag(k, USAGE_DISCOURAGED)) { + usefulStatements[k] = 0; + continue; + } + } + + /* Check if all math constants used in statement k are present + in the minimized proof. Hypotheses are not checked. */ + mString = g_Statement[k].mathString; + mlen = nmbrLen(mString); + + for (i = 0; i < mlen; i++) { + if (g_MathToken[mString[i]].tokenType == (char)con_) { + if (!g_MathToken[mString[i]].tmp) + usefulStatements[k] = 0; + } + } + usefulCount += usefulStatements[k]; + } + if (verboseMode) + print2("Found %ld potentially useful theorems.\n", usefulCount); + /* Scan forward, then reverse, then pick best result */ for (forwRevPass = 1; forwRevPass <= 2; forwRevPass++) { @@ -5182,38 +5268,9 @@ void command(int argc, char *argv[]) { for (k = forwFlag ? 1 : (g_proveStatement - 1); k * (forwFlag ? 1 : -1) < (forwFlag ? g_proveStatement : 0); k = k + (forwFlag ? 1 : -1)) { - if (!mathboxFlag && k >= g_mathboxStmt && k < thisMathboxStartStmt) { - continue; - } - - if (g_Statement[k].type != (char)p_ && g_Statement[k].type != (char)a_) - continue; - if (!matchesList(g_Statement[k].labelName, g_fullArg[1], '*', '?')) + if(!usefulStatements[k]) continue; - if (exceptPos != 0) { - /* Skip any match to the EXCEPT argument */ - if (matchesList(g_Statement[k].labelName, g_fullArg[exceptPos + 1], - '*', '?')) - continue; - } - - if (forbidMatchList[0]) { /* User provided a /FORBID list */ - /* First, we check to make sure we're not trying a statement - in the forbidMatchList directly (traceProof() won't find - this) */ - if (matchesList(g_Statement[k].labelName, forbidMatchList, '*', '?')) - continue; - } - - /* Check to see if statement comment specified a usage - restriction */ - if (!overrideFlag) { - if (getMarkupFlag(k, USAGE_DISCOURAGED)) { - continue; - } - } - /* Print individual labels */ if (prntStatus == 0) prntStatus = 1; /* Matched at least one */ @@ -5565,6 +5622,8 @@ void command(int argc, char *argv[]) { g_Statement[g_proveStatement].labelName); } + poolFree(usefulStatements); /* Deallocate memory */ + free_vstring(str1); /* Deallocate memory */ free_nmbrString(nmbrSaveProof); /* Deallocate memory */ From 5b796eee2be87495f5b016ab8256f1e87051dbc5 Mon Sep 17 00:00:00 2001 From: Reviewer Date: Mon, 18 Jul 2022 18:59:35 +0700 Subject: [PATCH 2/2] Preset usefulStatements to 0 at the start of the loop. --- src/metamath.c | 32 +++++++++++++------------------- 1 file changed, 13 insertions(+), 19 deletions(-) diff --git a/src/metamath.c b/src/metamath.c index e357404d..ff36abc8 100644 --- a/src/metamath.c +++ b/src/metamath.c @@ -5176,48 +5176,37 @@ void command(int argc, char *argv[]) { /* Fill the usefulStatements array */ for (k = 1; k < g_proveStatement; k++) { - usefulStatements[k] = 1; + usefulStatements[k] = 0; - if (!mathboxFlag && k >= g_mathboxStmt && k < thisMathboxStartStmt) { - usefulStatements[k] = 0; + if (!mathboxFlag && k >= g_mathboxStmt && k < thisMathboxStartStmt) continue; - } - if (g_Statement[k].type != (char)p_ && g_Statement[k].type != (char)a_) { - usefulStatements[k] = 0; + if (g_Statement[k].type != (char)p_ && g_Statement[k].type != (char)a_) continue; - } - if (!matchesList(g_Statement[k].labelName, g_fullArg[1], '*', '?')) { - usefulStatements[k] = 0; + + if (!matchesList(g_Statement[k].labelName, g_fullArg[1], '*', '?')) continue; - } if (exceptPos != 0) { /* Skip any match to the EXCEPT argument */ if (matchesList(g_Statement[k].labelName, g_fullArg[exceptPos + 1], - '*', '?')) { - usefulStatements[k] = 0; + '*', '?')) continue; - } } if (forbidMatchList[0]) { /* User provided a /FORBID list */ /* First, we check to make sure we're not trying a statement in the forbidMatchList directly (traceProof() won't find this) */ - if (matchesList(g_Statement[k].labelName, forbidMatchList, '*', '?')) { - usefulStatements[k] = 0; + if (matchesList(g_Statement[k].labelName, forbidMatchList, '*', '?')) continue; - } } /* Check to see if statement comment specified a usage restriction */ if (!overrideFlag) { - if (getMarkupFlag(k, USAGE_DISCOURAGED)) { - usefulStatements[k] = 0; + if (getMarkupFlag(k, USAGE_DISCOURAGED)) continue; - } } /* Check if all math constants used in statement k are present @@ -5225,12 +5214,17 @@ void command(int argc, char *argv[]) { mString = g_Statement[k].mathString; mlen = nmbrLen(mString); + usefulStatements[k] = 1; for (i = 0; i < mlen; i++) { if (g_MathToken[mString[i]].tokenType == (char)con_) { if (!g_MathToken[mString[i]].tmp) + { usefulStatements[k] = 0; + break; + } } } + usefulCount += usefulStatements[k]; } if (verboseMode)