Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Improve minimize performance #94

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Improve minimize performance #94

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1edf9e3
Improve minimize * speed. See issue #10.
savask Jul 17, 2022
5b796ee
Preset usefulStatements to 0 at the start of the loop.
savask Jul 18, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
113 changes: 83 additions & 30 deletions src/metamath.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5150,6 +5150,86 @@ 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));
Comment on lines +5171 to +5174
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not use bool, true, false as advised in #17 (comment) ? Then a few statements below have minor modifications, e.g., usefulCount += usefulStatements[k]; has to be replaced by something like if (usefulStatements[k]) {usefulCount += 1}

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think originally I used char for consistency, for example, the .tmp field uses 0 and 1 instead of bool. As a positive side effect, usefulCount can be updated without branching (although I don't think it makes any great difference in this case).

long usefulCount = 0;

/* Fill the usefulStatements array */
for (k = 1; k < g_proveStatement; k++) {
usefulStatements[k] = 0;

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], '*', '?'))
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;
}

/* 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);

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;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be followed by a break; instruction

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

break;
}
}
}

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++) {

Expand Down Expand Up @@ -5182,38 +5262,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 */

Expand Down Expand Up @@ -5565,6 +5616,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 */

Expand Down