DlProofEnumerator: space optimality

- formulas are stored as strings rather than tree structures

Author: xamidi

README.html

@@ -216,14 +216,12 @@ <h1 id="xamidi-pmgenerator">@xamidi/pmGenerator</h1>
 <p>Code extracted from <a href="https://github.com/deontic-logic/proof-tool">deontic-logic/proof-tool</a> (still private; <a href="https://deontic-logic.github.io/readme.html">readme</a>). Can be used to generate improved versions of <a href="https://us.metamath.org/mmsolitaire/pmproofs.txt" title="us.metamath.org/mmsolitaire/pmproofs.txt">pmproofs.txt</a> of the <a href="https://us.metamath.org/mmsolitaire/mms.html" title="us.metamath.org/mmsolitaire/mms.html">mmsolitaire</a> project.<br>Exemplary generated results are available at <a href="https://github.com/xamidi/mmsolitaire" title="GitHub repository">xamidi/mmsolitaire</a>. Eligible for high-performance computing. If you have access to a supercomputer, please consider to use this tool to further contribute to our knowledge regarding minimal proofs.</p>
 <p>Some aspects of this tool were explicated in a <a href="https://groups.google.com/g/metamath/c/v0p86y5b-m0">proposal</a> at the Metamath mailing list.</p>
 <h4 id="usage">Usage</h4>
-<pre><code><span>pmGenerator</span> <span>(</span> <span>-g</span> <span>&lt;limit&gt;</span> <span>[-u]</span> <span>[-m]</span> <span>[-c]</span> <span>| -r &lt;pmproofs file&gt; &lt;output file&gt; [-i &lt;prefix&gt;] [-m] [-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] )+
+<pre><code><span>pmGenerator</span> <span>(</span> <span>-g</span> <span>&lt;limit&gt;</span> <span>[-u]</span> <span>[-c]</span> <span>| -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] )+
 </span><span>-g:</span> <span>Generate</span> <span>proof</span> <span>files</span>
-<span>    -u:</span> <span>unfiltered</span> <span>(significantly</span> <span>faster,</span> <span>but</span> <span>generates</span> <span>redundant</span> <span>proofs),</span> <span>leads</span> <span>to</span> <span>formulas</span> <span>being</span> <span>stored</span> <span>as</span> <span>strings</span> <span>rather</span> <span>than</span> <span>tree</span> <span>structures</span> <span>(vastly</span> <span>reduced</span> <span>RAM</span> <span>usage)</span> <span>;</span> <span>deprecates</span> <span>-m</span>
-<span>    -m:</span> <span>disable</span> <span>memory</span> <span>reduction</span> <span>(distributed</span> <span>formula</span> <span>lookup</span> <span>data,</span> <span>requires</span> <span>more</span> <span>RAM,</span> <span>faster</span> <span>collection,</span> <span>significantly</span> <span>slower</span> <span>filtering)</span>
+<span>    -u:</span> <span>unfiltered</span> <span>(significantly</span> <span>faster,</span> <span>but</span> <span>generates</span> <span>redundant</span> <span>proofs)</span>
 <span>    -c:</span> <span>proof</span> <span>files</span> <span>without</span> <span>conclusions,</span> <span>requires</span> <span>additional</span> <span>parsing</span>
 <span>-r:</span> <span>Replacements</span> <span>file</span> <span>creation</span> <span>based</span> <span>on</span> <span>proof</span> <span>files</span>
 <span>    -i:</span> <span>customize</span> <span>input</span> <span>file</span> <span>path</span> <span>prefix</span> <span>;</span> <span>default:</span> <span>"data/dProofs-withConclusions/dProofs"</span>
-<span>    -m:</span> <span>disable</span> <span>memory</span> <span>reduction</span> <span>(distributed</span> <span>formula</span> <span>lookup</span> <span>data,</span> <span>requires</span> <span>more</span> <span>RAM)</span>
 <span>    -c:</span> <span>proof</span> <span>files</span> <span>without</span> <span>conclusions,</span> <span>requires</span> <span>additional</span> <span>parsing</span> <span>;</span> <span>sets</span> <span>default</span> <span>input</span> <span>file</span> <span>path</span> <span>prefix</span> <span>to</span> <span>"data/dProofs-withoutConclusions/dProofs"</span>
 <span>    -d:</span> <span>print</span> <span>debug</span> <span>information</span>
 <span>-a:</span> <span>Apply</span> <span>replacements</span> <span>file</span>
@@ -244,7 +242,7 @@ <h4 id="usage">Usage</h4>
 <span>    -o:</span> <span>print</span> <span>to</span> <span>given</span> <span>output</span> <span>file</span>
 <span>    -d:</span> <span>print</span> <span>debug</span> <span>information</span>
 </code></pre><h4 id="examples">Examples</h4>
-<pre><code><span>pmGenerator</span> -g <span>19</span>
+<pre><code><span>pmGenerator</span> -g <span>-1</span>
 pmGenerator -r <span>"data/pmproofs.txt"</span> <span>"data/pmproofs-reducer.txt"</span> -i <span>"data/dProofs"</span> -c -d
 pmGenerator -a SD data/pmproofs-reducer.txt data/pmproofs.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d
 pmGenerator -g <span>19</span> -g <span>21</span> -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

README.md

@@ -8,14 +8,12 @@ Exemplary generated results are available at [xamidi/mmsolitaire](https://github
 Some aspects of this tool were explicated in a [proposal](https://groups.google.com/g/metamath/c/v0p86y5b-m0) at the Metamath mailing list.
 
 #### Usage
-    pmGenerator ( -g <limit> [-u] [-m] [-c] | -r <pmproofs file> <output file> [-i <prefix>] [-m] [-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] )+
+    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] )+
     -g: Generate proof files
-        -u: unfiltered (significantly faster, but generates redundant proofs), leads to formulas being stored as strings rather than tree structures (vastly reduced RAM usage) ; deprecates -m
-        -m: disable memory reduction (distributed formula lookup data, requires more RAM, faster collection, significantly slower filtering)
+        -u: unfiltered (significantly faster, but generates redundant proofs)
         -c: proof files without conclusions, requires additional parsing
     -r: Replacements file creation based on proof files
         -i: customize input file path prefix ; default: "data/dProofs-withConclusions/dProofs"
-        -m: disable memory reduction (distributed formula lookup data, requires more RAM)
         -c: proof files without conclusions, requires additional parsing ; sets default input file path prefix to "data/dProofs-withoutConclusions/dProofs"
         -d: print debug information
     -a: Apply replacements file
@@ -37,7 +35,7 @@ Some aspects of this tool were explicated in a [proposal](https://groups.google.
         -d: print debug information
 
 #### Examples
-    pmGenerator -g 19
+    pmGenerator -g -1
     pmGenerator -r "data/pmproofs.txt" "data/pmproofs-reducer.txt" -i "data/dProofs" -c -d
     pmGenerator -a SD data/pmproofs-reducer.txt data/pmproofs.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d
     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

__dependency_graph.dot

@@ -78,7 +78,6 @@ digraph {
 	DRuleReducer -> FctHelper [color=blue]
 	DRuleReducer -> TreeNode [color=blue]
 	DRuleReducer -> DlCore [color=blue]
-	DRuleReducer -> DlFormula [color=blue]
 	DRuleReducer -> DlProofEnumerator [color=blue]
 	DRuleReducer -> DRuleParser [color=blue]
 	DRuleReducer -> concurrent_map [color=blue]
@@ -110,6 +109,7 @@ digraph {
 	DlCore -> functional [color=red]
 	DlCore -> map [color=red]
 	DlCore -> memory [color=red]
+	DlCore -> string [color=red]
 	DlCore -> unordered_map [color=red]
 	DlCore -> unordered_set [color=red]
 	DlFormula -> TreeNode [color=blue]
@@ -122,21 +122,16 @@ digraph {
 	DlProofEnumerator -> DlCore [color=blue]
 	DlProofEnumerator -> DlFormula [color=blue]
 	DlProofEnumerator -> concurrent_map [color=blue]
-	DlProofEnumerator -> concurrent_set [color=blue]
 	DlProofEnumerator -> concurrent_vector [color=blue]
 	DlProofEnumerator -> parallel_for [color=blue]
 	DlProofEnumerator -> execution [color=blue]
 	DlProofEnumerator -> iostream [color=blue]
-	DlProofEnumerator -> Hashing [color=red]
 	DlProofEnumerator -> ProgressData [color=red]
 	DlProofEnumerator -> concurrent_unordered_map [color=red]
-	DlProofEnumerator -> concurrent_unordered_set [color=red]
-	DlProofEnumerator -> version [color=red]
 	DlProofEnumerator -> array [color=red]
 	DlProofEnumerator -> condition_variable [color=red]
 	DlProofEnumerator -> deque [color=red]
 	DlProofEnumerator -> map [color=red]
-	DlProofEnumerator -> memory [color=red]
 	DlProofEnumerator -> thread [color=red]
 	DlStructure -> CfgGrammar [color=blue]
 	DlStructure -> cstdint [color=red]