Skip to content

Commit 8e3a7db

Browse files
xamidixamidi
committed
readme & cli preparations
1 parent 0db0f8d commit 8e3a7db

File tree

5 files changed

+31
-24
lines changed

5 files changed

+31
-24
lines changed

‎README.html‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@
33
Update instructions:
44
1. Manually replace <body>[...]</body> with that of the updated version
55
2. RegEx replace-all: [FIND]class\=\"markdown-content\"[/FIND], [REPLACE]id\=\"readme\"[/REPLACE] (1 occurence)
6-
3. RegEx replace-all: [FIND] class\=\" *\b(?!\bmarkdown-container ltr\b)[^\"]*\b *\"[/FIND], [REPLACE][/REPLACE] (236 occurences)
6+
3. RegEx replace-all: [FIND] class\=\" *\b(?!\bmarkdown-container ltr\b)[^\"]*\b *\"[/FIND], [REPLACE][/REPLACE] (249 occurences)
77
4. RegEx replace-all: [FIND]<p><img src\=\"icon\/icon-readme\.png\" align\=\"left\"><\/p>[/FIND], [REPLACE]<img src\=\"icon\/icon-readme\.png\" align\=\"left\">[/REPLACE] (1 occurence)
88
5. RegEx replace-all: [FIND]id\=\"-xamidi-pmgenerator\"[/FIND], [REPLACE]id\=\"xamidi-pmgenerator\"[/REPLACE] (1 occurence)
9-
6. RegEx replace-all: [FIND]<(/|)span>[/FIND], [REPLACE][/REPLACE] (468 occurences)
9+
6. RegEx replace-all: [FIND]<(/|)span>[/FIND], [REPLACE][/REPLACE] (494 occurences)
1010
(NOTE: Use RegEx replacements to not invalidate these instructions. Further content may require more bugfixes as by steps 4, 5 and 6.)
1111
-->
1212
<html>
@@ -232,19 +232,19 @@ <h1 id="xamidi-pmgenerator">@xamidi/pmGenerator</h1>
232232
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=516720692%2F153725015" title="size(dProofs29.txt) / size(dProofs27.txt)">3.3613...</a></td>
233233
</tr>
234234
<tr>
235-
<td><a href="https://mega.nz/file/G18AWIpC#B04xOdtQj_2PJJP0yNQxbim7pOgd-hwv1i1EVU6ZsTM" title="2'161'632'450 bytes compressed into 112'364'583 bytes (ratio approx. 19.2377)">dProofs31&#x2011;unfiltered31+.txt</a></td>
235+
<td><a href="https://mega.nz/file/G18AWIpC#B04xOdtQj_2PJJP0yNQxbim7pOgd-hwv1i1EVU6ZsTM" title="2'161'632'450 bytes compressed into 112'364'583 bytes (ratio approx. 19.2377)">dProofs31‑unfiltered31+.txt</a></td>
236236
<td style="text-align:right">2 897 309 412</td>
237237
<td style="text-align:right">9.84</td>
238238
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=2161632450%2F516720692" title="size(dProofs31-unfiltered31+.txt) / size(dProofs29.txt)">4.1833...</a></td>
239239
</tr>
240240
<tr>
241-
<td><a href="https://mega.nz/file/3gVQSIJL#Qfa9CoUwsHWYYNHXYaP1mg61QQSJ1NSl1CHudK4g7BA" title="8'349'023'875 bytes compressed into 402'886'507 bytes (ratio approx. 20.7230)">dProofs33&#x2011;unfiltered31+.txt</a></td>
241+
<td><a href="https://mega.nz/file/3gVQSIJL#Qfa9CoUwsHWYYNHXYaP1mg61QQSJ1NSl1CHudK4g7BA" title="8'349'023'875 bytes compressed into 402'886'507 bytes (ratio approx. 20.7230)">dProofs33‑unfiltered31+.txt</a></td>
242242
<td style="text-align:right">11 246 333 287</td>
243243
<td style="text-align:right">36.49</td>
244244
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=8349023875%2F2161632450" title="size(dProofs33-unfiltered31+.txt) / size(dProofs31-unfiltered31+.txt)">3.8623...</a></td>
245245
</tr>
246246
<tr>
247-
<td><a href="https://mega.nz/file/2893yZ7S#JlCHv4uOajgBJPPE2W87F_LAPzkH0-FlF4_2OrccuC4" title="30'717'801'573 bytes compressed into 1'400'853'331 bytes (ratio approx. 21.9279)">dProofs35&#x2011;unfiltered31+.txt</a></td>
247+
<td><a href="https://mega.nz/file/2893yZ7S#JlCHv4uOajgBJPPE2W87F_LAPzkH0-FlF4_2OrccuC4" title="30'717'801'573 bytes compressed into 1'400'853'331 bytes (ratio approx. 21.9279)">dProofs35‑unfiltered31+.txt</a></td>
248248
<td style="text-align:right">41 964 134 860</td>
249249
<td style="text-align:right">130.52</td>
250250
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=30717801573%2F8349023875" title="size(dProofs35-unfiltered31+.txt) / size(dProofs33-unfiltered31+.txt)">3.6792...</a></td>
@@ -259,7 +259,7 @@ <h1 id="xamidi-pmgenerator">@xamidi/pmGenerator</h1>
259259
</table>
260260
<p>This tool has been <a href="https://groups.google.com/g/metamath/c/6DzIY33mthE/m/K0I6UNoiAgAJ">posted</a> to the Metamath mailing list.</p>
261261
<h4 id="usage">Usage</h4>
262-
<pre><code>pmGenerator ( -g &lt;limit&gt; [-u] [-c] | -r &lt;pmproofs file&gt; &lt;output file&gt; [-i &lt;prefix&gt;] [-c] [-d] | -a &lt;initials&gt; &lt;replacements file&gt; &lt;pmproofs file&gt; &lt;output file&gt; [-s] [-l] [-w] [-d] | -f ( 0 | 1 ) [-i &lt;prefix&gt;] [-o &lt;prefix&gt;] [-d] | -p [-i &lt;prefix&gt;] [-s] [-t] [-x &lt;limit&gt;] [-y &lt;limit&gt;] [-o &lt;output file&gt;] [-d] )+ | -m &lt;limit&gt;
262+
<pre><code>pmGenerator ( -g &lt;limit&gt; [-u] [-c] | -r &lt;pmproofs file&gt; &lt;output file&gt; [-i &lt;prefix&gt;] [-c] [-d] | -a &lt;initials&gt; &lt;replacements file&gt; &lt;pmproofs file&gt; &lt;output file&gt; [-s] [-l] [-w] [-d] | -f ( 0 | 1 ) [-i &lt;prefix&gt;] [-o &lt;prefix&gt;] [-d] | -p [-i &lt;prefix&gt;] [-s] [-t] [-x &lt;limit&gt;] [-y &lt;limit&gt;] [-o &lt;output file&gt;] [-d] )+ | -m &lt;limit&gt; [-s]
263263
-g: Generate proof files
264264
-u: unfiltered (significantly faster, but generates redundant proofs)
265265
-c: proof files without conclusions, requires additional parsing
@@ -286,14 +286,15 @@ <h4 id="usage">Usage</h4>
286286
-d: print debug information
287287
-m: MPI-based multi-node filtering (-m &lt;n&gt;) of a first unfiltered proof file (with conclusions) at ./data/dProofs-withConclusions/dProofs&lt;n&gt;-unfiltered&lt;n&gt;+.txt. Creates dProofs&lt;n&gt;.txt.
288288
Cannot be combined with further commands.
289+
-s: disable smooth progress mode (lowers memory requirements, but makes worse progress predictions)
289290
</code></pre><h4 id="examples">Examples</h4>
290291
<pre><code>pmGenerator -g -1
291292
pmGenerator -r "data/pmproofs.txt" "data/pmproofs-reducer.txt" -i "data/dProofs" -c -d
292293
pmGenerator -a SD data/pmproofs-reducer.txt data/pmproofs.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d
293294
pmGenerator -g 19 -g 21 -u -r data/pmproofs-old.txt data/pmproofs-reducer.txt -d -a SD data/pmproofs-reducer.txt data/pmproofs-old.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d
294295
pmGenerator -f 0 -o data/dProofs-withoutConclusions_ALL/dProofs -d
295296
pmGenerator -p -s -d -p -s -t -x 50 -y 100 -o data/plot_data_x50_y100.txt
296-
pmGenerator -m 17
297+
pmGenerator -m 17 -s
297298
</code></pre><h4 id="navigation">Navigation</h4>
298299
<ul>
299300
<li><a href="https://github.com/xamidi/pmGenerator/tree/c++11">C++11 branch</a></li>

‎README.md‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ The following table exemplary shows progress that has already been made.
1818
This tool has been [posted](https://groups.google.com/g/metamath/c/6DzIY33mthE/m/K0I6UNoiAgAJ) to the Metamath mailing list.
1919

2020
#### Usage
21-
pmGenerator ( -g <limit> [-u] [-c] | -r <pmproofs file> <output file> [-i <prefix>] [-c] [-d] | -a <initials> <replacements file> <pmproofs file> <output file> [-s] [-l] [-w] [-d] | -f ( 0 | 1 ) [-i <prefix>] [-o <prefix>] [-d] | -p [-i <prefix>] [-s] [-t] [-x <limit>] [-y <limit>] [-o <output file>] [-d] )+ | -m <limit>
21+
pmGenerator ( -g <limit> [-u] [-c] | -r <pmproofs file> <output file> [-i <prefix>] [-c] [-d] | -a <initials> <replacements file> <pmproofs file> <output file> [-s] [-l] [-w] [-d] | -f ( 0 | 1 ) [-i <prefix>] [-o <prefix>] [-d] | -p [-i <prefix>] [-s] [-t] [-x <limit>] [-y <limit>] [-o <output file>] [-d] )+ | -m <limit> [-s]
2222
-g: Generate proof files
2323
-u: unfiltered (significantly faster, but generates redundant proofs)
2424
-c: proof files without conclusions, requires additional parsing
@@ -45,6 +45,7 @@ This tool has been [posted](https://groups.google.com/g/metamath/c/6DzIY33mthE/m
4545
-d: print debug information
4646
-m: MPI-based multi-node filtering (-m <n>) of a first unfiltered proof file (with conclusions) at ./data/dProofs-withConclusions/dProofs<n>-unfiltered<n>+.txt. Creates dProofs<n>.txt.
4747
Cannot be combined with further commands.
48+
-s: disable smooth progress mode (lowers memory requirements, but makes worse progress predictions)
4849

4950
#### Examples
5051
pmGenerator -g -1
@@ -53,7 +54,7 @@ This tool has been [posted](https://groups.google.com/g/metamath/c/6DzIY33mthE/m
5354
pmGenerator -g 19 -g 21 -u -r data/pmproofs-old.txt data/pmproofs-reducer.txt -d -a SD data/pmproofs-reducer.txt data/pmproofs-old.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d
5455
pmGenerator -f 0 -o data/dProofs-withoutConclusions_ALL/dProofs -d
5556
pmGenerator -p -s -d -p -s -t -x 50 -y 100 -o data/plot_data_x50_y100.txt
56-
pmGenerator -m 17
57+
pmGenerator -m 17 -s
5758

5859
#### Navigation
5960
- [C++11 branch](https://github.com/xamidi/pmGenerator/tree/c++11)

‎main.cpp‎

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { <command>, <arg1>,
3030
if (!error.empty())
3131
cerr << error << endl;
3232
cout << "Usage:\n"
33-
" pmGenerator ( -g <limit> [-u] [-c] | -r <pmproofs file> <output file> [-i <prefix>] [-c] [-d] | -a <initials> <replacements file> <pmproofs file> <output file> [-s] [-l] [-w] [-d] | -f ( 0 | 1 ) [-i <prefix>] [-o <prefix>] [-d] | -p [-i <prefix>] [-s] [-t] [-x <limit>] [-y <limit>] [-o <output file>] [-d] )+ | -m <limit>\n"
33+
" pmGenerator ( -g <limit> [-u] [-c] | -r <pmproofs file> <output file> [-i <prefix>] [-c] [-d] | -a <initials> <replacements file> <pmproofs file> <output file> [-s] [-l] [-w] [-d] | -f ( 0 | 1 ) [-i <prefix>] [-o <prefix>] [-d] | -p [-i <prefix>] [-s] [-t] [-x <limit>] [-y <limit>] [-o <output file>] [-d] )+ | -m <limit> [-s]\n"
3434
" -g: Generate proof files\n"
3535
" -u: unfiltered (significantly faster, but generates redundant proofs)\n"
3636
" -c: proof files without conclusions, requires additional parsing\n"
@@ -57,13 +57,15 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { <command>, <arg1>,
5757
" -d: print debug information\n"
5858
" -m: MPI-based multi-node filtering (-m <n>) of a first unfiltered proof file (with conclusions) at ./data/dProofs-withConclusions/dProofs<n>-unfiltered<n>+.txt. Creates dProofs<n>.txt.\n"
5959
" Cannot be combined with further commands.\n"
60+
" -s: disable smooth progress mode (lowers memory requirements, but makes worse progress predictions)\n"
6061
"Examples:\n"
6162
" pmGenerator -g -1\n"
6263
" pmGenerator -r \"data/pmproofs.txt\" \"data/pmproofs-reducer.txt\" -i \"data/dProofs\" -c -d\n"
6364
" pmGenerator -a SD data/pmproofs-reducer.txt data/pmproofs.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d\n"
6465
" pmGenerator -g 19 -g 21 -u -r data/pmproofs-old.txt data/pmproofs-reducer.txt -d -a SD data/pmproofs-reducer.txt data/pmproofs-old.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d\n"
6566
" pmGenerator -f 0 -o data/dProofs-withoutConclusions_ALL/dProofs -d\n"
66-
" pmGenerator -p -s -d -p -s -t -x 50 -y 100 -o data/plot_data_x50_y100.txt" << endl;
67+
" pmGenerator -p -s -d -p -s -t -x 50 -y 100 -o data/plot_data_x50_y100.txt"
68+
" pmGenerator -m 17 -s" << endl;
6769
return 0;
6870
};
6971
#if 0 // default command
@@ -96,7 +98,7 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { <command>, <arg1>,
9698
ApplyReplacements, // get<6> = debug, get<7> = styleAll, get<8> = listAll, get<9> = wrap
9799
FileConversion, // get<2> = inputFilePrefix, get<3> = outputFilePrefix, get<6> = debug, get<7> ? createGeneratorFilesWithConclusions(...) : createGeneratorFilesWithoutConclusions(...)
98100
ConclusionLengthPlot, // get<2> = inputFilePrefix, get<3> = mout, get<6> = debug, get<7> = measureSymbolicLength, get<8> = table, get<10> = cutX, get<11> = cutY
99-
MpiFilter // get<1> = wordLengthLimit
101+
MpiFilter // get<1> = wordLengthLimit, get<6> = smoothProgress
100102
};
101103
vector<tuple<Task, unsigned, string, string, string, string, bool, bool, bool, bool, int64_t, int64_t>> tasks;
102104

@@ -155,9 +157,12 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { <command>, <arg1>,
155157
i += 4;
156158
break;
157159
case 's':
158-
if (tasks.empty() || (get<0>(tasks.back()) != Task::ApplyReplacements && get<0>(tasks.back()) != Task::ConclusionLengthPlot))
160+
if (tasks.empty() || (get<0>(tasks.back()) != Task::ApplyReplacements && get<0>(tasks.back()) != Task::ConclusionLengthPlot && get<0>(tasks.back()) != Task::MpiFilter))
159161
return printUsage("Invalid argument \"-s\".");
160-
get<7>(tasks.back()) = true; // styleAll := true, or measureSymbolicLength := true
162+
if (get<0>(tasks.back()) != Task::MpiFilter)
163+
get<7>(tasks.back()) = true; // styleAll := true, or measureSymbolicLength := true
164+
else
165+
get<6>(tasks.back()) = false; // smoothProgress := false
161166
break;
162167
case 'l':
163168
if (tasks.empty() || get<0>(tasks.back()) != Task::ApplyReplacements)
@@ -228,7 +233,7 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { <command>, <arg1>,
228233
from_chars_result result = FctHelper::toUInt(param, value);
229234
if (result.ec != errc())
230235
return printUsage("Invalid parameter \"" + param + "\" for \"-m\".");
231-
tasks.emplace_back(Task::MpiFilter, value, "", "", "", "", false, false, false, false, 0, 0);
236+
tasks.emplace_back(Task::MpiFilter, value, "", "", "", "", true, false, false, false, 0, 0);
232237
mpiArg = "-m";
233238
}
234239
break;
@@ -280,7 +285,7 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { <command>, <arg1>,
280285
ss << ++index << ". printConclusionLengthPlotData(" << bstr(get<7>(t)) << ", " << bstr(get<8>(t)) << ", " << get<10>(t) << ", " << get<11>(t) << ", \"" << get<2>(t) << "\", " << (get<3>(t).empty() ? "null" : "\"" + get<3>(t) + "\"") << ", " << bstr(get<6>(t)) << ")\n";
281286
break;
282287
case Task::MpiFilter:
283-
ss << ++index << ". mpi_filterDProofRepresentativeFile(" << get<1>(t) << ")\n";
288+
ss << ++index << ". mpi_filterDProofRepresentativeFile(" << get<1>(t) << ", " << bstr(get<6>(t)) << ")\n";
284289
break;
285290
}
286291
cout << "Tasks:\n" << ss.str() << endl;
@@ -324,9 +329,9 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { <command>, <arg1>,
324329
break;
325330
case Task::MpiFilter:
326331
stringstream ss;
327-
ss << "[Main; pid: " << getpid() << ", tid:" << this_thread::get_id() << ", rank " << mpi_rank << " (" << mpi_size << " proc" << (mpi_size == 1 ? "" : "s") << ")] Calling mpi_filterDProofRepresentativeFile(" << get<1>(t) << ").";
332+
ss << "[Main; pid: " << getpid() << ", tid:" << this_thread::get_id() << ", rank " << mpi_rank << " (" << mpi_size << " proc" << (mpi_size == 1 ? "" : "s") << ")] Calling mpi_filterDProofRepresentativeFile(" << get<1>(t) << ", " << bstr(get<6>(t)) << ").";
328333
cout << ss.str() << endl;
329-
DlProofEnumerator::mpi_filterDProofRepresentativeFile(get<1>(t));
334+
DlProofEnumerator::mpi_filterDProofRepresentativeFile(get<1>(t), get<6>(t));
330335
break;
331336
}
332337
} catch (exception& e) {

‎nortmann/DlProofEnumerator.cpp‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -735,7 +735,7 @@ void DlProofEnumerator::generateDProofRepresentativeFiles(uint32_t limit, bool r
735735
cout << strtok(ctime(&time), "\n") << ": Limited D-proof representative generator complete. [parallel ; " << thread::hardware_concurrency() << " hardware thread contexts" << (limit == UINT32_MAX ? "" : ", limit: " + to_string(limit)) << (redundantSchemaRemoval ? "" : ", unfiltered") << "]" << endl;
736736
}
737737

738-
void DlProofEnumerator::mpi_filterDProofRepresentativeFile(uint32_t wordLengthLimit) {
738+
void DlProofEnumerator::mpi_filterDProofRepresentativeFile(uint32_t wordLengthLimit, bool smoothProgress) {
739739
chrono::time_point<chrono::steady_clock> startTime;
740740

741741
// Obtain the process ID and the number of processes
@@ -818,7 +818,7 @@ void DlProofEnumerator::mpi_filterDProofRepresentativeFile(uint32_t wordLengthLi
818818
const vector<string>& recentConclusionSequence = allConclusions[wordLengthLimit];
819819
if (isMainProc)
820820
startTime = chrono::steady_clock::now();
821-
tbb::concurrent_unordered_set<string> redundant = _mpi_findRedundantConclusionsForProofsOfMaxLength(mpi_rank, mpi_size, wordLengthLimit, representativeProofs, recentConclusionSequence, isMainProc ? &removalProgress : nullptr);
821+
tbb::concurrent_unordered_set<string> redundant = _mpi_findRedundantConclusionsForProofsOfMaxLength(mpi_rank, mpi_size, wordLengthLimit, representativeProofs, recentConclusionSequence, isMainProc ? &removalProgress : nullptr, smoothProgress);
822822
if (isMainProc)
823823
cout << FctHelper::durationStringMs(chrono::duration_cast<chrono::microseconds>(chrono::steady_clock::now() - startTime)) + " taken to detect " + to_string(redundant.size()) + " conclusions for which there are more general variants proven in lower or equal amounts of steps." << endl;
824824

@@ -1253,7 +1253,7 @@ void DlProofEnumerator::_removeRedundantConclusionsForProofsOfMaxLength(const ui
12531253
//#cout << FctHelper::round(static_cast<long double>(chrono::duration_cast<chrono::microseconds>(chrono::steady_clock::now() - startTime).count()) / 1000.0, 2) << " ms taken for erasure of " << toErase.size() << " elements." << endl;
12541254
}
12551255

1256-
tbb::concurrent_unordered_set<string> DlProofEnumerator::_mpi_findRedundantConclusionsForProofsOfMaxLength(int mpi_rank, int mpi_size, const uint32_t maxLength, tbb::concurrent_unordered_map<string, string>& representativeProofs, const vector<string>& recentConclusionSequence, helper::ProgressData* const progressData) {
1256+
tbb::concurrent_unordered_set<string> DlProofEnumerator::_mpi_findRedundantConclusionsForProofsOfMaxLength(int mpi_rank, int mpi_size, const uint32_t maxLength, tbb::concurrent_unordered_map<string, string>& representativeProofs, const vector<string>& recentConclusionSequence, helper::ProgressData* const progressData, bool smoothProgress) {
12571257
bool isMainProc = mpi_rank == 0;
12581258
size_t n = recentConclusionSequence.size();
12591259

@@ -1289,7 +1289,7 @@ tbb::concurrent_unordered_set<string> DlProofEnumerator::_mpi_findRedundantConcl
12891289
tbb::concurrent_queue<string> toErase;
12901290
tbb::concurrent_unordered_set<string> toErase_mainProc;
12911291
mutex mtx;
1292-
unique_lock<std::mutex> condLock(mtx);
1292+
unique_lock<mutex> condLock(mtx);
12931293
condition_variable cond;
12941294
atomic<bool> communicate = true;
12951295
atomic<bool> workerDone = false;

0 commit comments

Comments
 (0)