Skip to content

Commit 28699b3

Browse files
xamidixamidi
committed
release v1.0 final, last before using MPI
- polishing & preparation for MPI-based filtering - take dProofs37-unfiltered31+.txt into account; update pmproofs.txt - fix crashing DRuleReducer::createReplacementsFile(): bad std::copy - since 5ba7f16 - std::for_each cannot handle exceptions, use tbb::parallel_for instead - mention rwth computing time project and add abstract
1 parent 84ef5c2 commit 28699b3

13 files changed

+240
-1635
lines changed

‎.gitattributes

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,4 @@
88
*.gif -text
99
*.ico -text
1010
*.7z -text
11+
*.pdf -text

‎README.html

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -249,6 +249,12 @@ <h1 id="xamidi-pmgenerator">@xamidi/pmGenerator</h1>
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>
251251
</tr>
252+
<tr>
253+
<td><a href="https://mega.nz/file/6wUyDQzT#DQIJOLd5dCn-6V9sJWiJXeGRPUTUaA-7LqbGfLStjV0" title="113'174'356'461 bytes compressed into 4'897'020'927 bytes (ratio approx. 23.1109)">dProofs37‑unfiltered31+.txt</a><sup>✻</sup></td>
254+
<td style="text-align:right">155 138 491 321</td>
255+
<td style="text-align:right">485.12</td>
256+
<td style="text-align:right"><a href="https://www.wolframalpha.com/input?i=113174356461%2F30717801573" title="size(dProofs37-unfiltered31+.txt) / size(dProofs35-unfiltered31+.txt)">3.6843...</a></td>
257+
</tr>
252258
</tbody>
253259
</table>
254260
<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>
@@ -290,4 +296,5 @@ <h4 id="usage">Usage</h4>
290296
<li><a href="https://github.com/xamidi/pmGenerator/tree/c++11">C++11 branch</a></li>
291297
<li><a href="https://github.com/xamidi/pmGenerator/tree/master">C++20 branch</a></li>
292298
</ul>
299+
<p><sup>✻</sup><sub>Generation and utilization were performed with computing resources granted by RWTH Aachen University under project <a href="pdf/rwth1392_abstract.pdf" title="View rwth1392_abstract.pdf">rwth1392</a>.</sub></p>
293300
</div></div></body></html>

‎README.md

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,13 @@ Code extracted from [deontic-logic/proof-tool](https://github.com/deontic-logic/
66
Exemplary generated results are available at [xamidi/mmsolitaire](https://github.com/xamidi/mmsolitaire "GitHub repository"). Eligible for shared memory high-performance computing. If you have access to a powerful computer, please consider to use this tool to further contribute to our knowledge regarding minimal proofs.
77
The following table exemplary shows progress that has already been made.
88

9-
| Load Files up to.. | Size of Files (with conclusions) [B] | Required Memory (approx.) [GiB] | Recent Growth Factor |
10-
| -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------:| -------------------------------:| --------------------------------------------------------------------------------------------------------------------------------------------------:|
11-
| [dProofs29.txt](https://github.com/xamidi/pmGenerator/tree/master/data/dProofs-withConclusions "735'676'962 bytes compressed into 41'959'698 bytes (ratio approx. 17.5329)") | 735 676 962 | 2.68 | [3.3613...](https://www.wolframalpha.com/input?i=516720692%2F153725015 "size(dProofs29.txt) / size(dProofs27.txt)") |
12-
| [dProofs31&#x2011;unfiltered31+.txt](https://mega.nz/file/G18AWIpC#B04xOdtQj_2PJJP0yNQxbim7pOgd-hwv1i1EVU6ZsTM "2'161'632'450 bytes compressed into 112'364'583 bytes (ratio approx. 19.2377)") | 2 897 309 412 | 9.84 | [4.1833...](https://www.wolframalpha.com/input?i=2161632450%2F516720692 "size(dProofs31-unfiltered31+.txt) / size(dProofs29.txt)") |
13-
| [dProofs33&#x2011;unfiltered31+.txt](https://mega.nz/file/3gVQSIJL#Qfa9CoUwsHWYYNHXYaP1mg61QQSJ1NSl1CHudK4g7BA "8'349'023'875 bytes compressed into 402'886'507 bytes (ratio approx. 20.7230)") | 11 246 333 287 | 36.49 | [3.8623...](https://www.wolframalpha.com/input?i=8349023875%2F2161632450 "size(dProofs33-unfiltered31+.txt) / size(dProofs31-unfiltered31+.txt)") |
14-
| [dProofs35&#x2011;unfiltered31+.txt](https://mega.nz/file/2893yZ7S#JlCHv4uOajgBJPPE2W87F_LAPzkH0-FlF4_2OrccuC4 "30'717'801'573 bytes compressed into 1'400'853'331 bytes (ratio approx. 21.9279)") | 41 964 134 860 | 130.52 | [3.6792...](https://www.wolframalpha.com/input?i=30717801573%2F8349023875 "size(dProofs35-unfiltered31+.txt) / size(dProofs33-unfiltered31+.txt)") |
9+
| Load Files up to.. | Size of Files (with conclusions) [B] | Required Memory (approx.) [GiB] | Recent Growth Factor |
10+
| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------:| -------------------------------:| ----------------------------------------------------------------------------------------------------------------------------------------------------:|
11+
| [dProofs29.txt](https://github.com/xamidi/pmGenerator/tree/master/data/dProofs-withConclusions "735'676'962 bytes compressed into 41'959'698 bytes (ratio approx. 17.5329)") | 735 676 962 | 2.68 | [3.3613...](https://www.wolframalpha.com/input?i=516720692%2F153725015 "size(dProofs29.txt) / size(dProofs27.txt)") |
12+
| [dProofs31&#x2011;unfiltered31+.txt](https://mega.nz/file/G18AWIpC#B04xOdtQj_2PJJP0yNQxbim7pOgd-hwv1i1EVU6ZsTM "2'161'632'450 bytes compressed into 112'364'583 bytes (ratio approx. 19.2377)") | 2 897 309 412 | 9.84 | [4.1833...](https://www.wolframalpha.com/input?i=2161632450%2F516720692 "size(dProofs31-unfiltered31+.txt) / size(dProofs29.txt)") |
13+
| [dProofs33&#x2011;unfiltered31+.txt](https://mega.nz/file/3gVQSIJL#Qfa9CoUwsHWYYNHXYaP1mg61QQSJ1NSl1CHudK4g7BA "8'349'023'875 bytes compressed into 402'886'507 bytes (ratio approx. 20.7230)") | 11 246 333 287 | 36.49 | [3.8623...](https://www.wolframalpha.com/input?i=8349023875%2F2161632450 "size(dProofs33-unfiltered31+.txt) / size(dProofs31-unfiltered31+.txt)") |
14+
| [dProofs35&#x2011;unfiltered31+.txt](https://mega.nz/file/2893yZ7S#JlCHv4uOajgBJPPE2W87F_LAPzkH0-FlF4_2OrccuC4 "30'717'801'573 bytes compressed into 1'400'853'331 bytes (ratio approx. 21.9279)") | 41 964 134 860 | 130.52 | [3.6792...](https://www.wolframalpha.com/input?i=30717801573%2F8349023875 "size(dProofs35-unfiltered31+.txt) / size(dProofs33-unfiltered31+.txt)") |
15+
| [dProofs37&#x2011;unfiltered31+.txt](https://mega.nz/file/6wUyDQzT#DQIJOLd5dCn-6V9sJWiJXeGRPUTUaA-7LqbGfLStjV0 "113'174'356'461 bytes compressed into 4'897'020'927 bytes (ratio approx. 23.1109)")<sup>✻</sup> | 155 138 491 321 | 485.12 | [3.6843...](https://www.wolframalpha.com/input?i=113174356461%2F30717801573 "size(dProofs37-unfiltered31+.txt) / size(dProofs35-unfiltered31+.txt)") |
1516

1617
This tool has been [posted](https://groups.google.com/g/metamath/c/6DzIY33mthE/m/K0I6UNoiAgAJ) to the Metamath mailing list.
1718

@@ -53,3 +54,5 @@ This tool has been [posted](https://groups.google.com/g/metamath/c/6DzIY33mthE/m
5354
#### Navigation
5455
- [C++11 branch](https://github.com/xamidi/pmGenerator/tree/c++11)
5556
- [C++20 branch](https://github.com/xamidi/pmGenerator/tree/master)
57+
58+
<sup>✻</sup><sub>Generation and utilization were performed with computing resources granted by RWTH Aachen University under project [rwth1392](pdf/rwth1392_abstract.pdf "View rwth1392_abstract.pdf").</sub>

‎__dependency_graph.dot

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,6 @@ digraph {
9797
DRuleReducer -> concurrent_vector [color=blue]
9898
DRuleReducer -> parallel_for [color=blue]
9999
DRuleReducer -> "boost/algorithm/string" [color=blue]
100-
DRuleReducer -> execution [color=blue]
101100
DRuleReducer -> iostream [color=blue]
102101
DRuleReducer -> string [color=red]
103102
subgraph "cluster_D:/Dropbox/eclipse/pmGenerator\metamath" {
@@ -142,7 +141,6 @@ digraph {
142141
DlProofEnumerator -> concurrent_vector [color=blue]
143142
DlProofEnumerator -> parallel_for [color=blue]
144143
DlProofEnumerator -> cstring [color=blue]
145-
DlProofEnumerator -> execution [color=blue]
146144
DlProofEnumerator -> iostream [color=blue]
147145
DlProofEnumerator -> FwdTbb [color=red]
148146
DlProofEnumerator -> ProgressData [color=red]

0 commit comments

Comments
 (0)