Skip to content

Commit

Permalink
make '--transform -z' multi-threaded (with single-threaded option)
Browse files Browse the repository at this point in the history
+ custom tool ./excludeLists
  • Loading branch information
xamidi committed Jul 31, 2024
1 parent d8ce4b7 commit 97de261
Show file tree
Hide file tree
Showing 8 changed files with 180 additions and 84 deletions.
5 changes: 3 additions & 2 deletions README.html
Original file line number Diff line number Diff line change
Expand Up @@ -458,7 +458,7 @@ <h4 id="usage">Usage</h4>
-f: proofs are given by input file path (where a comma-separated string is stored), ignoring all CR, LF, whitespace, and lines starting with '%'
-o: redirect the result's output to the specified file
-d: print debug information
--transform &lt;string&gt; [-s &lt;string&gt;] [-j &lt;limit or -1&gt;] [-p &lt;limit or -1&gt;] [-n] [-u] [-t &lt;string&gt;] [-e] [-i &lt;limit or -1&gt;] [-l &lt;limit or -1&gt;] [-z] [-f] [-o &lt;output file&gt;] [-d]
--transform &lt;string&gt; [-s &lt;string&gt;] [-j &lt;limit or -1&gt;] [-p &lt;limit or -1&gt;] [-n] [-u] [-t &lt;string&gt;] [-e] [-i &lt;limit or -1&gt;] [-l &lt;limit or -1&gt;] [-z] [-y] [-f] [-o &lt;output file&gt;] [-d]
Transform proof summary (as by '--parse [...] -s') into recombined variant ; ignores configured system (proof summaries provide their own axioms) ; "," represents LF
-s: list a subproof with its conclusion if it occurs in the given comma-separated list of conclusions
-j: join common subproofs together when they are used at least a given amount of times ; default: 2
Expand All @@ -470,6 +470,7 @@ <h4 id="usage">Usage</h4>
-i: decrease memory requirements but increase time consumption by not storing intermediate unfoldings that exceed a certain length ; default: -1
-l: abort computation when combined requested proof sequences exceed the given limit in bytes ; default: 134217728 (i.e. 128 MiB)
-z: proof compression ; find and remove internal redundancies (e.g. non-trivial parts not affecting intermediate theorems) by attempting to use shorter owned subproofs at all positions
-y: disable multi-threaded D-rule replacement search in case proof compression is performed (enables deterministic solution procedure)
-f: proof summary is given by input file path ; ignores lines that are empty or starting with '%'
-o: redirect the result's output to the specified file
-d: print debug information
Expand Down Expand Up @@ -552,7 +553,7 @@ <h4 id="usage">Usage</h4>
pmGenerator --variate 1 -s --extract -# 35 -d -c -d -e 0
pmGenerator -m 17 -s
</code></pre><h4 id="multi-node-computing">Multi-node Computing</h4>
<p>For MPI-based filtering, each spawned process is multithreaded and attempts to use as many threads as the hardware specifies as concurrent. Therefore, it is ideal to spawn the same amount of processes and nodes.<br>The following exemplary <a href="https://slurm.schedmd.com/documentation.html">Slurm</a> batch script has been used via <a href="https://slurm.schedmd.com/sbatch.html">sbatch</a> in order to reduce <code>dProofs31‑unfiltered31+.txt</code> to <code>dProofs31.txt</code>.</p>
<p>For MPI-based filtering, each spawned process is multi-threaded and attempts to use as many threads as the hardware specifies as concurrent. Therefore, it is ideal to spawn the same amount of processes and nodes.<br>The following exemplary <a href="https://slurm.schedmd.com/documentation.html">Slurm</a> batch script has been used via <a href="https://slurm.schedmd.com/sbatch.html">sbatch</a> in order to reduce <code>dProofs31‑unfiltered31+.txt</code> to <code>dProofs31.txt</code>.</p>
<pre><code>#!/bin/zsh
#SBATCH --job-name=pmGen-20
#SBATCH --output=output_%J.txt
Expand Down
5 changes: 3 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ Some more – and very special – proof systems are illustrated [further down b
-f: proofs are given by input file path (where a comma-separated string is stored), ignoring all CR, LF, whitespace, and lines starting with '%'
-o: redirect the result's output to the specified file
-d: print debug information
--transform <string> [-s <string>] [-j <limit or -1>] [-p <limit or -1>] [-n] [-u] [-t <string>] [-e] [-i <limit or -1>] [-l <limit or -1>] [-z] [-f] [-o <output file>] [-d]
--transform <string> [-s <string>] [-j <limit or -1>] [-p <limit or -1>] [-n] [-u] [-t <string>] [-e] [-i <limit or -1>] [-l <limit or -1>] [-z] [-y] [-f] [-o <output file>] [-d]
Transform proof summary (as by '--parse [...] -s') into recombined variant ; ignores configured system (proof summaries provide their own axioms) ; "," represents LF
-s: list a subproof with its conclusion if it occurs in the given comma-separated list of conclusions
-j: join common subproofs together when they are used at least a given amount of times ; default: 2
Expand All @@ -95,6 +95,7 @@ Some more – and very special – proof systems are illustrated [further down b
-i: decrease memory requirements but increase time consumption by not storing intermediate unfoldings that exceed a certain length ; default: -1
-l: abort computation when combined requested proof sequences exceed the given limit in bytes ; default: 134217728 (i.e. 128 MiB)
-z: proof compression ; find and remove internal redundancies (e.g. non-trivial parts not affecting intermediate theorems) by attempting to use shorter owned subproofs at all positions
-y: disable multi-threaded D-rule replacement search in case proof compression is performed (enables deterministic solution procedure)
-f: proof summary is given by input file path ; ignores lines that are empty or starting with '%'
-o: redirect the result's output to the specified file
-d: print debug information
Expand Down Expand Up @@ -179,7 +180,7 @@ Some more – and very special – proof systems are illustrated [further down b
pmGenerator -m 17 -s

#### Multi-node Computing
For MPI-based filtering, each spawned process is multithreaded and attempts to use as many threads as the hardware specifies as concurrent. Therefore, it is ideal to spawn the same amount of processes and nodes.
For MPI-based filtering, each spawned process is multi-threaded and attempts to use as many threads as the hardware specifies as concurrent. Therefore, it is ideal to spawn the same amount of processes and nodes.
The following exemplary [Slurm](https://slurm.schedmd.com/documentation.html) batch script has been used via [sbatch](https://slurm.schedmd.com/sbatch.html) in order to reduce `dProofs31‑unfiltered31+.txt` to `dProofs31.txt`.

#!/bin/zsh
Expand Down
1 change: 1 addition & 0 deletions __dependency_graph.dot
Original file line number Diff line number Diff line change
Expand Up @@ -160,6 +160,7 @@ digraph {
DRuleParser -> DlCore [color=blue]
DRuleParser -> DlFormula [color=blue]
DRuleParser -> "boost/algorithm/string" [color=blue]
DRuleParser -> parallel_for_each [color=blue]
DRuleParser -> "(iostream)" [color=blue]
DRuleParser -> "(numeric)" [color=blue]
DRuleParser -> "(cstddef)" [color=red]
Expand Down
4 changes: 2 additions & 2 deletions logic/DlProofEnumerator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -961,7 +961,7 @@ void DlProofEnumerator::convertProofSummaryToAbstractDProof(const string& input,
//#if (optOut_requiredIntermediateResults) cout << "requiredIntermediateResults = " << FctHelper::vectorStringF(*optOut_requiredIntermediateResults, [](const DRuleParser::AxiomInfo& ax) { return DlCore::formulaRepresentation_traverse(ax.refinedAxiom) + "[" + ax.name + "]"; }) << endl;
}

void DlProofEnumerator::recombineProofSummary(const string& input, bool useInputFile, const string* conclusionsWithHelperProofs, unsigned minUseAmountToCreateHelperProof, size_t maxLengthToKeepProof, bool normalPolishNotation, bool printInfixUnicode, const string* filterForTheorems, bool abstractProofStrings, size_t storeIntermediateUnfoldingLimit, size_t maxLengthToComputeDProof, bool compress, const string* outputFile, bool debug) {
void DlProofEnumerator::recombineProofSummary(const string& input, bool useInputFile, const string* conclusionsWithHelperProofs, unsigned minUseAmountToCreateHelperProof, size_t maxLengthToKeepProof, bool normalPolishNotation, bool printInfixUnicode, const string* filterForTheorems, bool abstractProofStrings, size_t storeIntermediateUnfoldingLimit, size_t maxLengthToComputeDProof, bool compress, const string* outputFile, bool debug, bool compress_concurrentDRuleSearch) {
vector<DRuleParser::AxiomInfo> customAxioms;
vector<string> abstractDProof_input;
vector<DRuleParser::AxiomInfo> requiredIntermediateResults;
Expand All @@ -986,7 +986,7 @@ void DlProofEnumerator::recombineProofSummary(const string& input, bool useInput
if (conclusionsWithHelperProofs)
toAxiomInfoVector(*conclusionsWithHelperProofs, conclusionsWithHelperProofs_axInfo);
vector<shared_ptr<DlFormula>> conclusions;
const vector<string> abstractDProof = DRuleParser::recombineAbstractDProof(abstractDProof_input, conclusions, &customAxioms, filterForTheorems ? *filterForTheorems != "." ? &filterForTheorems_axInfo : &requiredIntermediateResults : nullptr, conclusionsWithHelperProofs ? &conclusionsWithHelperProofs_axInfo : nullptr, minUseAmountToCreateHelperProof, &requiredIntermediateResults, debug, maxLengthToKeepProof, abstractProofStrings, storeIntermediateUnfoldingLimit, maxLengthToComputeDProof, compress);
const vector<string> abstractDProof = DRuleParser::recombineAbstractDProof(abstractDProof_input, conclusions, &customAxioms, filterForTheorems ? *filterForTheorems != "." ? &filterForTheorems_axInfo : &requiredIntermediateResults : nullptr, conclusionsWithHelperProofs ? &conclusionsWithHelperProofs_axInfo : nullptr, minUseAmountToCreateHelperProof, &requiredIntermediateResults, debug, maxLengthToKeepProof, abstractProofStrings, storeIntermediateUnfoldingLimit, maxLengthToComputeDProof, compress, compress_concurrentDRuleSearch);

auto print = [&](ostream& mout) -> string::size_type {
auto infixUnicode = [](const shared_ptr<DlFormula>& f) { string s = DlCore::formulaRepresentation_traverse(f); boost::replace_all(s, DlCore::terminalStr_and(), "∧"); boost::replace_all(s, DlCore::terminalStr_or(), "∨"); boost::replace_all(s, DlCore::terminalStr_nand(), "↑"); boost::replace_all(s, DlCore::terminalStr_nor(), "↓"); boost::replace_all(s, DlCore::terminalStr_imply(), "→"); boost::replace_all(s, DlCore::terminalStr_implied(), "←"); boost::replace_all(s, DlCore::terminalStr_nimply(), "↛"); boost::replace_all(s, DlCore::terminalStr_nimplied(), "↚"); boost::replace_all(s, DlCore::terminalStr_equiv(), "↔"); boost::replace_all(s, DlCore::terminalStr_xor(), "↮"); boost::replace_all(s, DlCore::terminalStr_com(), "↷"); boost::replace_all(s, DlCore::terminalStr_app(), "↝"); boost::replace_all(s, DlCore::terminalStr_not(), "¬"); boost::replace_all(s, DlCore::terminalStr_nece(), "□"); boost::replace_all(s, DlCore::terminalStr_poss(), "◇"); boost::replace_all(s, DlCore::terminalStr_obli(), "○"); boost::replace_all(s, DlCore::terminalStr_perm(), "⌔"); boost::replace_all(s, DlCore::terminalStr_top(), "⊤"); boost::replace_all(s, DlCore::terminalStr_bot(), "⊥"); return s; };
Expand Down
2 changes: 1 addition & 1 deletion logic/DlProofEnumerator.h
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ struct DlProofEnumerator {
static void sampleCombinations();
static void printProofs(const std::vector<std::string>& dProofs, DlFormulaStyle outputNotation = DlFormulaStyle::PolishNumeric, bool conclusionsOnly = false, bool summaryMode = false, unsigned minUseAmountToCreateHelperProof = 2, bool abstractProofStrings = false, const std::string* inputFile = nullptr, const std::string* outputFile = nullptr, bool debug = false);
static void convertProofSummaryToAbstractDProof(const std::string& input, std::vector<metamath::DRuleParser::AxiomInfo>* optOut_customAxioms = nullptr, std::vector<std::string>* optOut_abstractDProof = nullptr, std::vector<metamath::DRuleParser::AxiomInfo>* optOut_requiredIntermediateResults = nullptr, bool useInputFile = false, bool normalPolishNotation = false, bool debug = true);
static void recombineProofSummary(const std::string& input, bool useInputFile, const std::string* conclusionsWithHelperProofs = nullptr, unsigned minUseAmountToCreateHelperProof = 2, std::size_t maxLengthToKeepProof = SIZE_MAX, bool normalPolishNotation = false, bool printInfixUnicode = false, const std::string* filterForTheorems = nullptr, bool abstractProofStrings = true, std::size_t storeIntermediateUnfoldingLimit = SIZE_MAX, std::size_t maxLengthToComputeDProof = 134217728, bool compress = false, const std::string* outputFile = nullptr, bool debug = false);
static void recombineProofSummary(const std::string& input, bool useInputFile, const std::string* conclusionsWithHelperProofs = nullptr, unsigned minUseAmountToCreateHelperProof = 2, std::size_t maxLengthToKeepProof = SIZE_MAX, bool normalPolishNotation = false, bool printInfixUnicode = false, const std::string* filterForTheorems = nullptr, bool abstractProofStrings = true, std::size_t storeIntermediateUnfoldingLimit = SIZE_MAX, std::size_t maxLengthToComputeDProof = 134217728, bool compress = false, const std::string* outputFile = nullptr, bool debug = false, bool compress_concurrentDRuleSearch = true);
static void unfoldProofSummary(const std::string& input, bool useInputFile, bool normalPolishNotation, const std::string* filterForTheorems = nullptr, std::size_t storeIntermediateUnfoldingLimit = SIZE_MAX, std::size_t maxLengthToComputeDProof = 134217728, bool wrap = false, const std::string* outputFile = nullptr, bool debug = false);

// Data prediction
Expand Down
Loading

0 comments on commit 97de261

Please sign in to comment.