increase efficiency of '--transform -x,-z' + "baby steps" option ('-#')

- as suggested in #2 (comment) (discussions)
- standard proof compression rounds essentially use '-x 3' until no more
  changes, instead of slower nested loop approach
- can still use N-loop (i.e. looking for N-rules as replacements), but
  nested D-loop was too inefficient
- no more '--transform -y' (single-threaded D-rule replacement search)
- baby steps ('--transform -#') progress slower, but may synthesize more
  theorems
+ fix bug where calling removeDuplicateConclusionsFromAbstractDProof()
  or compressAbstractDProof() with !filterForTheorems could cause the
  target theorem to deviate from the final conclusion of the input

Author: xamidi

README.html

@@ -480,7 +480,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;] [-b] [-w] [-z] [-x &lt;limit&gt;] [-y] [-k] [-v &lt;file&gt;] [-h] [-q] [-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;] [-b] [-w] [-z] [-x &lt;limit&gt;] [-#] [-k] [-v &lt;file&gt;] [-h] [-q] [-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
@@ -494,12 +494,12 @@ <h4 id="usage">Usage</h4>
        -b: duplicate conclusion removal ; replace each given subproof that has a redundant conclusion with its first shortest alternative and remove duplicates ; beneficial in preparing '-x' or '-z'
        -w: read input without conclusions given
        -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
-       -x: proof compression with extended modification range; before each round generate relative abstract proofs (D-rules only) with up to &lt;range&gt; steps, potentially improving rules with new formulas ; default: 0
-       -y: disable multi-threaded D-rule replacement search in case proof compression is performed (enables deterministic procedure) ; not affecting exhaustive generations via '-x', which remain nondeterministic
-       -k: store maximum-size proofs generated via 'x' also when they do not prove known intermediate theorems, so they can still be used as replacements for subproofs ; increases memory consumption significantly
-       -v: coordinate iteration phases for maximum-size proofs generated via 'x' with the specified vault file (to avoid repeating these computations over multiple runs) ; used only when '-k' unspecified
-       -h: save raw intermediate results in files before each proof compression round (and after productive rounds) ; after each preparation phase (exhaustive generation) in case '-x' is specified
-       -q: skip first round preparation for '-x' ; useful to continue working on intermediate results produced by an aborted computation using '-h'
+       -x: proof compression with extended modification range; for '-x 5' or higher: prepare each round with relative abstract proofs (D-rules only) of up to &lt;range&gt; steps, potentially improving rules with new formulas ; default: 0
+       -#: use smaller, less efficient proof compression steps ; increases the number of potential rounds and newly introduced intermediate conclusions, potentially leading to shorter proofs eventually
+       -k: store maximum-size proofs prepared via '-x' also when they do not prove known intermediate theorems, so they can still be used as replacements for subproofs ; increases memory consumption significantly
+       -v: coordinate preparation phases for maximum-size proofs generated via '-x' with the specified vault file (to avoid repeating these computations over multiple runs) ; used only when '-k' unspecified
+       -h: save raw intermediate results in files at the beginning of each proof compression round (and at the end of productive rounds) ; after each preparation phase in case '-x' is specified
+       -q: skip first round preparation for '-x' ; useful to eliminate inefficiencies before extensive preparations, or to continue working on intermediate results produced by an aborted computation using '-h'
        -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

README.md

@@ -118,7 +118,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>] [-b] [-w] [-z] [-x <limit>] [-y] [-k] [-v <file>] [-h] [-q] [-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>] [-b] [-w] [-z] [-x <limit>] [-#] [-k] [-v <file>] [-h] [-q] [-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
@@ -132,12 +132,12 @@ Some more – and very special – proof systems are illustrated [further down b
            -b: duplicate conclusion removal ; replace each given subproof that has a redundant conclusion with its first shortest alternative and remove duplicates ; beneficial in preparing '-x' or '-z'
            -w: read input without conclusions given
            -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
-           -x: proof compression with extended modification range; before each round generate relative abstract proofs (D-rules only) with up to <range> steps, potentially improving rules with new formulas ; default: 0
-           -y: disable multi-threaded D-rule replacement search in case proof compression is performed (enables deterministic procedure) ; not affecting exhaustive generations via '-x', which remain nondeterministic
-           -k: store maximum-size proofs generated via 'x' also when they do not prove known intermediate theorems, so they can still be used as replacements for subproofs ; increases memory consumption significantly
-           -v: coordinate iteration phases for maximum-size proofs generated via 'x' with the specified vault file (to avoid repeating these computations over multiple runs) ; used only when '-k' unspecified
-           -h: save raw intermediate results in files before each proof compression round (and after productive rounds) ; after each preparation phase (exhaustive generation) in case '-x' is specified
-           -q: skip first round preparation for '-x' ; useful to continue working on intermediate results produced by an aborted computation using '-h'
+           -x: proof compression with extended modification range; for '-x 5' or higher: prepare each round with relative abstract proofs (D-rules only) of up to <range> steps, potentially improving rules with new formulas ; default: 0
+           -#: use smaller, less efficient proof compression steps ; increases the number of potential rounds and newly introduced intermediate conclusions, potentially leading to shorter proofs eventually
+           -k: store maximum-size proofs prepared via '-x' also when they do not prove known intermediate theorems, so they can still be used as replacements for subproofs ; increases memory consumption significantly
+           -v: coordinate preparation phases for maximum-size proofs generated via '-x' with the specified vault file (to avoid repeating these computations over multiple runs) ; used only when '-k' unspecified
+           -h: save raw intermediate results in files at the beginning of each proof compression round (and at the end of productive rounds) ; after each preparation phase in case '-x' is specified
+           -q: skip first round preparation for '-x' ; useful to eliminate inefficiencies before extensive preparations, or to continue working on intermediate results produced by an aborted computation using '-h'
            -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

helper/FctHelper.cpp

@@ -358,7 +358,7 @@ string FctHelper::durationYearsToMs(const chrono::microseconds& dur, bool innerA
 			empty = false;
 	} else
 		appendRequestedBlankIndent(2 + sId.length());
-	if (milliseconds || empty) {
+	if (durationUs || empty) {
 		string ms = FctHelper::round(milliseconds, round);
 		ss << spaceIfNonEmpty() << requestedIndent(round ? 4 + round : 3, ms) << ms << msId;
 	} else

logic/DlProofEnumerator.cpp

@@ -1036,7 +1036,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 removeDuplicateConclusions, bool compress, bool noInputConclusions, const string* outputFile, bool debug, bool compress_concurrentDRuleSearch, size_t compress_modificationRange, bool compress_keepMaxRules, const string* compress_vaultFile, bool compress_sureSaves, bool compress_skipFirstPrep) {
+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 removeDuplicateConclusions, bool compress, bool noInputConclusions, const string* outputFile, bool debug, size_t compress_modificationRange, bool compress_keepMaxRules, const string* compress_vaultFile, bool compress_sureSaves, bool compress_skipFirstPrep, bool compress_babySteps) {
 	vector<DRuleParser::AxiomInfo> customAxioms;
 	vector<string> abstractDProof_input;
 	vector<DRuleParser::AxiomInfo> requiredIntermediateResults;
@@ -1074,7 +1074,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, targetEverything, filterForTheorems && !targetEverything ? *filterForTheorems != "." || noInputConclusions ? &filterForTheorems_axInfo : &requiredIntermediateResults : nullptr, conclusionsWithHelperProofs ? &conclusionsWithHelperProofs_axInfo : nullptr, minUseAmountToCreateHelperProof, noInputConclusions ? nullptr : &requiredIntermediateResults, debug, maxLengthToKeepProof, abstractProofStrings, storeIntermediateUnfoldingLimit, maxLengthToComputeDProof, removeDuplicateConclusions, compress, compress_concurrentDRuleSearch, compress_modificationRange, compress_keepMaxRules, compress_vaultFile, compress_sureSaves, compress_skipFirstPrep);
+	const vector<string> abstractDProof = DRuleParser::recombineAbstractDProof(abstractDProof_input, conclusions, &customAxioms, targetEverything, filterForTheorems && !targetEverything ? *filterForTheorems != "." || noInputConclusions ? &filterForTheorems_axInfo : &requiredIntermediateResults : nullptr, conclusionsWithHelperProofs ? &conclusionsWithHelperProofs_axInfo : nullptr, minUseAmountToCreateHelperProof, noInputConclusions ? nullptr : &requiredIntermediateResults, debug, maxLengthToKeepProof, abstractProofStrings, storeIntermediateUnfoldingLimit, maxLengthToComputeDProof, removeDuplicateConclusions, compress, compress_modificationRange, compress_keepMaxRules, compress_vaultFile, compress_sureSaves, compress_skipFirstPrep, compress_babySteps);
 
 	chrono::time_point<chrono::steady_clock> startTime;
 	if (debug)

logic/DlProofEnumerator.h

@@ -75,7 +75,7 @@ struct DlProofEnumerator {
 	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, std::string* optOut_result = nullptr, std::unordered_map<std::size_t, std::size_t>* optOut_indexOrigins = nullptr, bool silent = false);
 	static std::string::size_type printProofSummary(std::ostream& mout, const std::vector<metamath::DRuleParser::AxiomInfo>& axioms, const std::vector<std::string>& abstractDProof, const std::vector<std::shared_ptr<DlFormula>>& conclusions, bool normalPolishNotation = false, bool printInfixUnicode = 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 noInputConclusions = 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 removeDuplicateConclusions = false, bool compress = false, bool noInputConclusions = false, const std::string* outputFile = nullptr, bool debug = false, bool compress_concurrentDRuleSearch = true, std::size_t compress_modificationRange = 0, bool compress_keepMaxRules = false, const std::string* compress_vaultFile = nullptr, bool compress_sureSaves = false, bool compress_skipFirstPrep = 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 removeDuplicateConclusions = false, bool compress = false, bool noInputConclusions = false, const std::string* outputFile = nullptr, bool debug = false, std::size_t compress_modificationRange = 0, bool compress_keepMaxRules = false, const std::string* compress_vaultFile = nullptr, bool compress_sureSaves = false, bool compress_skipFirstPrep = false, bool compress_babySteps = false);
 	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, bool noInputConclusions = false, const std::string* outputFile = nullptr, bool debug = false);
 	static void uniteProofSummary(const std::string& input, bool normalPolishNotation, bool removeDuplicateConclusions = false, const std::string* outputFile = nullptr, bool debug = false);