new feature '--unite': create union of proof summary files

Author: xamidi

README.html

@@ -491,7 +491,7 @@ <h4 id="usage">Usage</h4>
        -e: keep expanded proof strings ; show fully detailed condensed detachment proofs rather than allowing them to contain references
        -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)
-       -b: duplicate conclusion removal ; replace each given subproof that has a redundant conclusion with its first shortest alternative and remove duplicates ; beneficial in preparing '-z'
+       -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
@@ -514,6 +514,12 @@ <h4 id="usage">Usage</h4>
        -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
+  --unite &lt;input files&gt; [-n] [-b] [-o &lt;output file&gt;] [-d]
+     Unite proof summary files of the same system which are given by a comma-separated list of paths ; targets and prints all used conclusions ; ignores configured system (proof summaries provide their own axioms)
+       -n: specify and print formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
+       -b: duplicate conclusion removal ; replace each given subproof that has a redundant conclusion with its first shortest alternative and remove duplicates
+       -o: redirect the result's output to the specified file
+       -d: print debug information
   --ndconvert &lt;input file&gt; [-b &lt;base file&gt;] [-n] [-u] [-h] [-k] [-o &lt;output file&gt;] [-d]
      Convert proof from Fitch-style natural deduction to condensed detachment in a user-definable Hilbert system and print its proof summary (usable via '--transform' and '--unfold') ; ignores configured system
      Input file must contain propositional FitchFX proof without premises, as exportable from https://mrieppel.github.io/FitchFX/ ; supported rules: 'Assumption','IP','~I','~E','&gt;I','&gt;E','&I','&E','vI','vE','&lt;&gt;I','&lt;&gt;E','Reit'
@@ -589,6 +595,8 @@ <h4 id="usage">Usage</h4>
 pmGenerator --unfold CpCqp=1,CCpCqrCCpqCpr=2,CCNpNqCqp=3,[0]CCpCNqNrCpCrq:D2D13,[1]Cpp:DD211,[2]NCCppNCqq:DD3DD2DD2D[0]D[0]11D1[1][1] -n -t CNNpp,NCCppNCqq
 pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -p -2 -d
 pmGenerator --transform "CCCpqrCCrpCsp=1,[0]=DDDD1D1D1D1DDDD1D1D11111111,[1]=D1DD[0]1[0],[2]=DDDD1DD[1][1]1111" -n -w -t _
+pmGenerator --unite data/w1.txt,data/w1-m.txt,data/w1-w2.txt,data/w1-w3.txt,data/w1-w4.txt,data/w1-w5.txt,data/w1-w6.txt -n -b -o data/w1-minax-full.txt
+pmGenerator --ndconvert data/m_ffx.txt -n -b data/w1.txt -o data/w1-m.txt
 pmGenerator --ndconvert data/m_ffx.txt -n -b data/w1.txt -u
 pmGenerator -c -s CCCCC0.1CN2N3.2.4CC4.0C3.0 -g 35 --plot -s -t -x 50 -y 100 -o data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/plot_data_x50_y100.txt
 pmGenerator -c -n -s CCCCCpqCNrNsrtCCtpCsp --search CpCqp,CCpCqrCCpqCpr,CCNpNqCqp -n

README.md

@@ -123,7 +123,7 @@ Some more – and very special – proof systems are illustrated [further down b
            -e: keep expanded proof strings ; show fully detailed condensed detachment proofs rather than allowing them to contain references
            -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)
-           -b: duplicate conclusion removal ; replace each given subproof that has a redundant conclusion with its first shortest alternative and remove duplicates ; beneficial in preparing '-z'
+           -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
@@ -146,6 +146,12 @@ Some more – and very special – proof systems are illustrated [further down b
            -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
+      --unite <input files> [-n] [-b] [-o <output file>] [-d]
+         Unite proof summary files of the same system which are given by a comma-separated list of paths ; targets and prints all used conclusions ; ignores configured system (proof summaries provide their own axioms)
+           -n: specify and print formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
+           -b: duplicate conclusion removal ; replace each given subproof that has a redundant conclusion with its first shortest alternative and remove duplicates
+           -o: redirect the result's output to the specified file
+           -d: print debug information
       --ndconvert <input file> [-b <base file>] [-n] [-u] [-h] [-k] [-o <output file>] [-d]
          Convert proof from Fitch-style natural deduction to condensed detachment in a user-definable Hilbert system and print its proof summary (usable via '--transform' and '--unfold') ; ignores configured system
          Input file must contain propositional FitchFX proof without premises, as exportable from https://mrieppel.github.io/FitchFX/ ; supported rules: 'Assumption','IP','~I','~E','>I','>E','&I','&E','vI','vE','<>I','<>E','Reit'
@@ -222,6 +228,8 @@ Some more – and very special – proof systems are illustrated [further down b
     pmGenerator --unfold CpCqp=1,CCpCqrCCpqCpr=2,CCNpNqCqp=3,[0]CCpCNqNrCpCrq:D2D13,[1]Cpp:DD211,[2]NCCppNCqq:DD3DD2DD2D[0]D[0]11D1[1][1] -n -t CNNpp,NCCppNCqq
     pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -p -2 -d
     pmGenerator --transform "CCCpqrCCrpCsp=1,[0]=DDDD1D1D1D1DDDD1D1D11111111,[1]=D1DD[0]1[0],[2]=DDDD1DD[1][1]1111" -n -w -t _
+    pmGenerator --unite data/w1.txt,data/w1-m.txt,data/w1-w2.txt,data/w1-w3.txt,data/w1-w4.txt,data/w1-w5.txt,data/w1-w6.txt -n -b -o data/w1-minax-full.txt
+    pmGenerator --ndconvert data/m_ffx.txt -n -b data/w1.txt -o data/w1-m.txt
     pmGenerator --ndconvert data/m_ffx.txt -n -b data/w1.txt -u
     pmGenerator -c -s CCCCC0.1CN2N3.2.4CC4.0C3.0 -g 35 --plot -s -t -x 50 -y 100 -o data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/plot_data_x50_y100.txt
     pmGenerator -c -n -s CCCCCpqCNrNsrtCCtpCsp --search CpCqp,CCpCqrCCpqCpr,CCNpNqCqp -n

logic/DlProofEnumerator.cpp

@@ -33,6 +33,52 @@ inline string myTime() {
 	time_t time = chrono::system_clock::to_time_t(chrono::system_clock::now());
 	return strtok(ctime(&time), "\n");
 }
+inline void switchRefs(char& c, bool& inReference, unsigned& refIndex, const auto& inRefAction, const auto& outRefAction) {
+	if (inReference)
+		switch (c) {
+		case '0':
+			refIndex = 10 * refIndex;
+			break;
+		case '1':
+			refIndex = 10 * refIndex + 1;
+			break;
+		case '2':
+			refIndex = 10 * refIndex + 2;
+			break;
+		case '3':
+			refIndex = 10 * refIndex + 3;
+			break;
+		case '4':
+			refIndex = 10 * refIndex + 4;
+			break;
+		case '5':
+			refIndex = 10 * refIndex + 5;
+			break;
+		case '6':
+			refIndex = 10 * refIndex + 6;
+			break;
+		case '7':
+			refIndex = 10 * refIndex + 7;
+			break;
+		case '8':
+			refIndex = 10 * refIndex + 8;
+			break;
+		case '9':
+			refIndex = 10 * refIndex + 9;
+			break;
+		case ']':
+			inRefAction();
+			refIndex = 0;
+			inReference = false;
+			break;
+		default:
+			throw invalid_argument("DlProofEnumerator::switchRefs(): Invalid character '" + string { c } + "': Not part of a proof reference.");
+		}
+	else if (c == '[')
+		inReference = true;
+	else
+		outRefAction();
+}
 }
 
 const vector<const vector<string>*>& DlProofEnumerator::builtinRepresentatives() {
@@ -1146,6 +1192,67 @@ void DlProofEnumerator::unfoldProofSummary(const string& input, bool useInputFil
 	}
 }
 
+void DlProofEnumerator::uniteProofSummary(const string& input, bool normalPolishNotation, bool removeDuplicateConclusions, const string* outputFile, bool debug) {
+	chrono::time_point<chrono::steady_clock> startTime;
+	vector<string> paths = FctHelper::stringSplit(input, ",");
+	vector<DRuleParser::AxiomInfo> targetAxioms;
+	vector<string> abstractDProof;
+	vector<shared_ptr<DlFormula>> conclusions;
+	for (const string& path : paths) {
+		vector<DRuleParser::AxiomInfo> targetAxioms_part;
+		vector<string> abstractDProof_part;
+		DlProofEnumerator::convertProofSummaryToAbstractDProof(path, &targetAxioms_part, &abstractDProof_part, nullptr, true, normalPolishNotation, false, debug);
+		size_t shift = abstractDProof.size();
+		if (targetAxioms.empty()) {
+			targetAxioms = targetAxioms_part;
+			abstractDProof = abstractDProof_part;
+		} else if (targetAxioms.size() != targetAxioms_part.size())
+			throw invalid_argument("Cannot unite proof summaries with different axioms.");
+		else {
+			for (size_t i = 0; i < targetAxioms.size(); i++)
+				if (*targetAxioms[i].refinedAxiom != *targetAxioms_part[i].refinedAxiom)
+					throw invalid_argument("Cannot unite proof summaries with different axioms.");
+			auto translate = [&](const string& s) -> string {
+				string result;
+				bool inReference = false;
+				unsigned refIndex = 0;
+				for (char c : s) {
+					switchRefs(c, inReference, refIndex, [&]() {
+						result += "[" + to_string(refIndex + shift) + "]";
+					}, [&]() { result += string { c }; });
+				}
+				if (inReference)
+					throw invalid_argument("DlProofEnumerator::uniteProofSummary(): Missing character ']' after '['.");
+				return result;
+			};
+			for (const string& s : abstractDProof_part)
+				abstractDProof.push_back(translate(s));
+		}
+		if (debug)
+			cout << "Appended " << abstractDProof.size() << " abstract D-proofs from \"" << path << "\"." << endl;
+	}
+	abstractDProof = DRuleParser::recombineAbstractDProof(abstractDProof, conclusions, &targetAxioms, true, nullptr, nullptr, 1, nullptr, debug, SIZE_MAX, true, SIZE_MAX, SIZE_MAX, removeDuplicateConclusions);
+	if (debug)
+		startTime = chrono::steady_clock::now();
+	if (outputFile) { // Not using FctHelper::writeToFile() in order to write huge files without huge string acquisition.
+		filesystem::path file = filesystem::u8path(*outputFile);
+		while (!filesystem::exists(file) && !FctHelper::ensureDirExists(file.string()))
+			cerr << "Failed to create file at \"" << file.string() << "\", trying again." << endl;
+		string::size_type bytes;
+		{
+			ofstream fout(file, fstream::out | fstream::binary);
+			bytes = DlProofEnumerator::printProofSummary(fout, targetAxioms, abstractDProof, conclusions, normalPolishNotation);
+		}
+		if (debug)
+			cout << FctHelper::durationStringMs(chrono::duration_cast<chrono::microseconds>(chrono::steady_clock::now() - startTime)) << " taken to print and save " << bytes << " bytes to " << file.string() << "." << endl;
+	} else {
+		string::size_type bytes = DlProofEnumerator::printProofSummary(cout, targetAxioms, abstractDProof, conclusions, normalPolishNotation);
+		cout << flush;
+		if (debug)
+			cout << FctHelper::durationStringMs(chrono::duration_cast<chrono::microseconds>(chrono::steady_clock::now() - startTime)) << " taken to print " << bytes << " bytes." << endl;
+	}
+}
+
 bool DlProofEnumerator::loadDProofRepresentatives(vector<vector<string>>& allRepresentatives, vector<vector<string>>* optOut_allConclusions, uint64_t* optOut_allRepresentativesCount, map<uint32_t, uint64_t>* optOut_representativeCounts, uint32_t* optOut_firstMissingIndex, bool debug, const string& filePrefix, const string& filePostfix, bool initFresh, uint32_t limit, const uint32_t* proofLenStepSize) {
 	const uint32_t c = proofLenStepSize ? *proofLenStepSize : _necessitationLimit ? 1 : 2;
 	chrono::time_point<chrono::steady_clock> startTime;

logic/DlProofEnumerator.h

@@ -77,6 +77,7 @@ struct DlProofEnumerator {
 	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 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);
 
 	// Data prediction
 	static void printGenerationExpenditures(bool redundantSchemaRemoval = true, bool withConclusions = true, bool debug = false);