--parse: show index origins whenever modified + code style improvements

Author: xamidi

__dependency_graph.dot

@@ -1,8 +1,8 @@
 digraph {
+	sha2 -> "(cstring)" [color=blue]
 	sha2 -> "(iomanip)" [color=blue]
 	sha2 -> "(iostream)" [color=blue]
 	sha2 -> "(sstream)" [color=blue]
-	sha2 -> "(cstring)" [color=blue]
 	sha2 -> "(cstdint)" [color=red]
 	sha2 -> "(string)" [color=red]
 	subgraph "cluster_D:/Dropbox/eclipse/pmGenerator\cryptography" {
@@ -19,8 +19,8 @@ digraph {
 		CfgGrammar
 		CfgGrammar
 	}
-	FctHelper -> "(iostream)" [color=blue]
 	FctHelper -> "(cmath)" [color=blue]
+	FctHelper -> "(iostream)" [color=blue]
 	FctHelper -> "(algorithm)" [color=red]
 	FctHelper -> "(array)" [color=red]
 	FctHelper -> "(charconv)" [color=red]

cryptography/sha2.cpp

@@ -1,9 +1,9 @@
 #include "sha2.h"
 
+#include <cstring>
 #include <iomanip>
 #include <iostream>
 #include <sstream>
-#include <cstring>
 
 using namespace std;
 

grammar/CfgGrammar.cpp

@@ -25,7 +25,7 @@ CfgGrammar::CfgGrammar(const string& startSymbolString, const string& grammarStr
 		const vector<string>& ruleElements = FctHelper::stringSplit(grammarLine, " ");
 		if (!FctHelper::vectorContains(nonterminals, ruleElements[0]))
 			nonterminals.push_back(ruleElements[0]);
-		const vector<string>& splitGrammarLine = FctHelper::stringSplit(grammarLine, " -> ");
+		const vector<string>& splitGrammarLine = FctHelper::stringSplit(grammarLine, " ::= ");
 
 		vector<string> grammarRule;
 		if (splitGrammarLine[1].find('|') != string::npos) { // multiple rules
@@ -59,7 +59,7 @@ CfgGrammar::CfgGrammar(const string& startSymbolString, const string& grammarStr
 	while (getline(reader2, grammarLine)) {
 		const vector<string>& ruleElements = FctHelper::stringSplit(grammarLine, " ");
 		for (size_t i = 1; i < ruleElements.size(); i++)
-			if (!FctHelper::vectorContains(nonterminals, ruleElements[i]) && !FctHelper::vectorContains(terminals, ruleElements[i]) && (ruleElements[i] != "->") && (ruleElements[i] != "|"))
+			if (!FctHelper::vectorContains(nonterminals, ruleElements[i]) && !FctHelper::vectorContains(terminals, ruleElements[i]) && (ruleElements[i] != "::=") && (ruleElements[i] != "|"))
 				terminals.push_back(ruleElements[i]);
 	}
 

grammar/CfgGrammar.h

@@ -11,8 +11,7 @@ namespace xamidi {
 namespace grammar {
 
 // Represents a context-free grammar
-struct CfgGrammar: public helper::IPrintable {
-private:
+class CfgGrammar: public helper::IPrintable {
 	std::uint32_t _elementCounter;
 	std::string _startSymbolString;
 	std::string _grammarString;
@@ -30,39 +29,31 @@ struct CfgGrammar: public helper::IPrintable {
 	CfgGrammar(const std::string& startSymbolString, const std::string& grammarString);
 
 	const std::string& startSymbolString() const;
-
 	std::uint32_t startSymbolId() const;
 
 	const std::string& grammarString() const;
 
 	const std::vector<std::uint32_t>& nonterminalIds() const;
-
 	const std::vector<std::uint32_t>& terminalIds() const;
 
 	const std::vector<std::string>& nonterminalStrings() const;
-
 	const std::vector<std::string>& terminalStrings() const;
 
 	const std::unordered_map<std::uint32_t, const std::string>& nonterminalStringLookup() const;
-
 	const std::unordered_map<std::uint32_t, const std::string>& terminalStringLookup() const;
 
 	const std::string& stringOf(std::uint32_t id) const;
-
 	std::vector<std::string> stringsOf(const std::vector<std::uint32_t>& ids) const;
-
 	std::string symbolSequenceOf(const std::vector<std::uint32_t>& ids) const;
 
 	const std::unordered_map<std::uint32_t, std::vector<std::vector<std::uint32_t>>>& productionRules() const;
 
 	std::uint32_t maybeStoreNonterminal(const std::string&);
-
 	std::uint32_t maybeStoreTerminal(const std::string&);
 
 	std::uint32_t idLookup(const std::string&) const;
 
 	std::string productionString() const;
-
 	virtual std::string toString() const override;
 };
 

helper/FctHelper.cpp

@@ -1,7 +1,7 @@
 #include "FctHelper.h"
 
-#include <iostream>
 #include <cmath>
+#include <iostream>
 
 using namespace std;
 

helper/ProgressData.h

@@ -10,7 +10,7 @@
 namespace xamidi {
 namespace helper {
 
-struct ProgressData { // Note: Displays only integer percentage values, which might be generously rounded up, but less so for larger data sets (i.e. higher 'maximum'). 'percentageStepSize' must be a divisor of 100.
+struct ProgressData { // NOTE: Displays only integer percentage values, which might be generously rounded up, but less so for larger data sets (i.e. higher 'maximum'). 'percentageStepSize' must be a divisor of 100.
 	unsigned percentageStepSize = 0;
 	std::uint64_t maximum = 0;
 	bool maximumEstimated = false;

logic/DlCore.cpp

@@ -1352,7 +1352,7 @@ string::size_type DlCore::traverseFormulas_polishNotation_noRename_numVars(const
 }
 
 string DlCore::substitutionRepresentation_traverse(const map<string, shared_ptr<DlFormula>>& substitutions) {
-	return FctHelper::mapStringF(substitutions, [](const pair<string, shared_ptr<DlFormula>>& pair) { return "\u3008" + pair.first + ", " + formulaRepresentation_traverse(pair.second) + "\u3009"; }, { }, { });
+	return FctHelper::mapStringF(substitutions, [](const pair<const string, shared_ptr<DlFormula>>& pair) { return "\u3008" + pair.first + ", " + formulaRepresentation_traverse(pair.second) + "\u3009"; }, { }, { });
 }
 
 shared_ptr<DlFormula> DlCore::substitute(const shared_ptr<DlFormula>& formula, const map<string, shared_ptr<DlFormula>>& substitutions) {

logic/DlCore.h

@@ -15,7 +15,7 @@
 namespace xamidi {
 namespace helper { struct String; }
 namespace tree { template<typename T> class TreeNode; }
-namespace grammar { struct CfgGrammar; }
+namespace grammar { class CfgGrammar; }
 
 namespace logic {
 
@@ -138,7 +138,7 @@ struct DlCore {
 	// Note that the unifier for trees can be exponential in size w.r.t. the input, e.g. formulas { a\orz\ory\orx\orw, w\or(x\or(y\or(z\ora))) } [n := 5 variables each] result in
 	// unifier 〈w, a\ora\or(a\ora)\or(a\ora\or(a\ora))〉, 〈x, a\ora\or(a\ora)〉, 〈y, a\ora〉, 〈z, a〉 [15 variables, generally 2^(n-2) + ... + 2^1 + 2^0 = sum_(k=0)^(n-2)2^k = 2^(n-1)-1].
 	// Their unified formula is thereby a\ora\or(a\ora)\or(a\ora\or(a\ora))\or(a\ora\or(a\ora)\or(a\ora\or(a\ora))) [16 variables, generally 2^(n-1)].
-	static bool tryUnifyTrees(const std::shared_ptr<logic::DlFormula>& formulaA, const std::shared_ptr<logic::DlFormula>& formulaB, std::map<std::string, std::shared_ptr<logic::DlFormula>>* optOut_substitutions = nullptr, bool debug = false);
+	static bool tryUnifyTrees(const std::shared_ptr<DlFormula>& formulaA, const std::shared_ptr<DlFormula>& formulaB, std::map<std::string, std::shared_ptr<DlFormula>>* optOut_substitutions = nullptr, bool debug = false);
 
 	// A standard formula representation, except that topmost binary operators are not surrounded by parentheses.
 	static std::string formulaRepresentation_traverse(const std::shared_ptr<DlFormula>& formula);
@@ -203,7 +203,7 @@ struct DlCore {
 private:
 	// Helper functions
 	static bool _isSchemaOf(const std::shared_ptr<DlFormula>& potentialSchema, const std::shared_ptr<DlFormula>& formula, std::map<std::string, std::shared_ptr<DlFormula>>& substitutions);
-	static bool _tryUnifyTrees(const std::shared_ptr<logic::DlFormula>& formulaA, const std::shared_ptr<logic::DlFormula>& formulaB, std::map<std::string, std::shared_ptr<logic::DlFormula>>& substitutions, bool debug);
+	static bool _tryUnifyTrees(const std::shared_ptr<DlFormula>& formulaA, const std::shared_ptr<DlFormula>& formulaB, std::map<std::string, std::shared_ptr<DlFormula>>& substitutions, bool debug);
 	static void _toBasicDlFormula(const std::shared_ptr<DlFormula>& destinationNode, const std::shared_ptr<DlFormula>& formula, std::unordered_map<std::shared_ptr<DlFormula>, std::shared_ptr<DlFormula>>* optOut_originals, bool calculateMeanings);
 	static void _substitute(const std::shared_ptr<DlFormula>& destinationNode, const std::shared_ptr<DlFormula>& formula, const std::map<std::string, std::shared_ptr<DlFormula>>& substitutions);
 };

logic/DlProofEnumerator.cpp

@@ -761,7 +761,7 @@ void DlProofEnumerator::sampleCombinations() {
 		cerr << "Some tests failed." << endl;
 }
 
-void DlProofEnumerator::printProofs(const vector<string>& dProofs, DlFormulaStyle outputNotation, bool conclusionsOnly, bool summaryMode, unsigned minUseAmountToCreateHelperProof, bool abstractProofStrings, const string* inputFile, const string* outputFile, bool debug) {
+void DlProofEnumerator::printProofs(const vector<string>& dProofs, DlFormulaStyle outputNotation, bool conclusionsOnly, bool summaryMode, unsigned minUseAmountToCreateHelperProof, bool abstractProofStrings, const string* inputFile, const string* outputFile, bool debug, string* optOut_result, unordered_map<size_t, size_t>* optOut_indexOrigins) {
 	chrono::time_point<chrono::steady_clock> startTime;
 	vector<string> dProofsFromFile;
 	if (inputFile) {
@@ -869,20 +869,40 @@ void DlProofEnumerator::printProofs(const vector<string>& dProofs, DlFormulaStyl
 			}
 		}
 	}
-	if (!outputFile)
-		cout << ss.str() << flush;
-	else {
+	if (optOut_result)
+		*optOut_result = ss.str();
+	if (optOut_indexOrigins)
+		*optOut_indexOrigins = indexOrigins;
+	if (outputFile) {
 		if (debug)
 			startTime = chrono::steady_clock::now();
 		if (!FctHelper::writeToFile(*outputFile, ss.str()))
 			throw runtime_error("Failed to write to file at \"" + *outputFile + "\".");
 		if (debug)
 			cout << FctHelper::durationStringMs(chrono::duration_cast<chrono::microseconds>(chrono::steady_clock::now() - startTime)) << " taken to save " << ss.str().length() << " bytes to \"" << *outputFile << "\"." << endl;
-	}
-	if (!conclusionsOnly && (_dProofs.size() != rawParseData.size() || !duplicates.empty()))
+	} else if (!optOut_result)
+		cout << ss.str() << flush;
+	if (!conclusionsOnly && (_dProofs.size() != rawParseData.size() || !duplicates.empty() || any_of(indexOrigins.begin(), indexOrigins.end(), [](const pair<const size_t, size_t>& p) { return p.first != p.second; })))
 		cout << "Index correspondences (out,in) are " << FctHelper::mapString(map<size_t, size_t>(indexOrigins.begin(), indexOrigins.end())) << "." << endl;
 }
 
+string::size_type DlProofEnumerator::printProofSummary(ostream& mout, const vector<DRuleParser::AxiomInfo>& axioms, const vector<string>& abstractDProof, const vector<shared_ptr<DlFormula>>& conclusions, bool normalPolishNotation, bool printInfixUnicode) {
+	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; };
+	string::size_type bytes = 0;
+	for (const DRuleParser::AxiomInfo& ax : axioms) {
+		string f = printInfixUnicode ? infixUnicode(ax.refinedAxiom) : normalPolishNotation ? DlCore::toPolishNotation(ax.refinedAxiom) : DlCore::toPolishNotation_noRename(ax.refinedAxiom);
+		mout << "    " << f << " = " << ax.name << "\n";
+		bytes += 9 + f.length();
+	}
+	for (size_t i = 0; i < abstractDProof.size(); i++) {
+		string f = printInfixUnicode ? infixUnicode(conclusions[i]) : normalPolishNotation ? DlCore::toPolishNotation(conclusions[i]) : DlCore::toPolishNotation_noRename(conclusions[i]);
+		const string& p = abstractDProof[i];
+		mout << "[" << i << "] " << f << " = " << p << "\n";
+		bytes += 7 + FctHelper::digitsNum_uint64(i) + f.length() + p.length();
+	}
+	return bytes;
+}
+
 void DlProofEnumerator::convertProofSummaryToAbstractDProof(const string& input, vector<DRuleParser::AxiomInfo>* optOut_customAxioms, vector<string>* optOut_abstractDProof, vector<DRuleParser::AxiomInfo>* optOut_requiredIntermediateResults, bool useInputFile, bool normalPolishNotation, bool noInputConclusions, bool debug) {
 	vector<string> summaryLines;
 	{
@@ -942,7 +962,7 @@ void DlProofEnumerator::convertProofSummaryToAbstractDProof(const string& input,
 				throw invalid_argument("Missing axiom name in \"" + line + "\".");
 			string axName = line.substr(pos);
 			if (axName.length() != 1 || ((axName[0] < '1' || axName[0] > '9') && (axName[0] < 'a' || axName[0] > 'z')))
-				throw invalid_argument("Invalid axiom name in \"" + line + "\".");
+				throw invalid_argument("Invalid axiom name (\"" + axName + "\") in \"" + line + "\".");
 			size_t num = axName[0] >= '1' && axName[0] <= '9' ? axName[0] - '1' : 10 + axName[0] - 'a' - 1;
 			if (num != axiomIndex++)
 				throw invalid_argument("[axiomIndex = " + to_string(axiomIndex - 1) + ", char = " + to_string(axiomIndex - 10 + 'a') + "] Invalid axiom number in \"" + line + "\". Should be " + (axiomIndex <= 9 ? string { char(axiomIndex + '0') } : string { char(axiomIndex - 10 + 'a') }) + ".");
@@ -1013,22 +1033,6 @@ void DlProofEnumerator::recombineProofSummary(const string& input, bool useInput
 	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);
 
-	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; };
-		string::size_type bytes = 0;
-		for (const DRuleParser::AxiomInfo& ax : customAxioms) {
-			string f = printInfixUnicode ? infixUnicode(ax.refinedAxiom) : normalPolishNotation ? DlCore::toPolishNotation(ax.refinedAxiom) : DlCore::toPolishNotation_noRename(ax.refinedAxiom);
-			mout << "    " << f << " = " << ax.name << "\n";
-			bytes += 9 + f.length();
-		}
-		for (size_t i = 0; i < abstractDProof.size(); i++) {
-			string f = printInfixUnicode ? infixUnicode(conclusions[i]) : normalPolishNotation ? DlCore::toPolishNotation(conclusions[i]) : DlCore::toPolishNotation_noRename(conclusions[i]);
-			const string& p = abstractDProof[i];
-			mout << "[" << i << "] " << f << " = " << p << "\n";
-			bytes += 7 + FctHelper::digitsNum_uint64(i) + f.length() + p.length();
-		}
-		return bytes;
-	};
 	chrono::time_point<chrono::steady_clock> startTime;
 	if (debug)
 		startTime = chrono::steady_clock::now();
@@ -1039,12 +1043,12 @@ void DlProofEnumerator::recombineProofSummary(const string& input, bool useInput
 		string::size_type bytes;
 		{
 			ofstream fout(file, fstream::out | fstream::binary);
-			bytes = print(fout);
+			bytes = printProofSummary(fout, customAxioms, abstractDProof, conclusions, normalPolishNotation, printInfixUnicode);
 		}
 		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 = print(cout);
+		string::size_type bytes = printProofSummary(cout, customAxioms, abstractDProof, conclusions, normalPolishNotation, printInfixUnicode);
 		cout << flush;
 		if (debug)
 			cout << FctHelper::durationStringMs(chrono::duration_cast<chrono::microseconds>(chrono::steady_clock::now() - startTime)) << " taken to print " << bytes << " bytes." << endl;
@@ -4063,9 +4067,9 @@ void DlProofEnumerator::printConclusionLengthPlotData(bool measureSymbolicLength
 								++it;
 						}
 					if (table)
-						ss << FctHelper::mapStringF(allAmounts, [](const pair<size_t, size_t>& p) { return to_string(p.first) + "\t" + to_string(p.second); }, { }, "\n", "\n") << "\n";
+						ss << FctHelper::mapStringF(allAmounts, [](const pair<const size_t, size_t>& p) { return to_string(p.first) + "\t" + to_string(p.second); }, { }, "\n", "\n") << "\n";
 					else
-						ss << FctHelper::mapStringF(allAmounts, [](const pair<size_t, size_t>& p) { return to_string(p.first) + " " + to_string(p.second); }, { }, "\n", " ") << "\n";
+						ss << FctHelper::mapStringF(allAmounts, [](const pair<const size_t, size_t>& p) { return to_string(p.first) + " " + to_string(p.second); }, { }, "\n", " ") << "\n";
 				} else
 					ss << "\n";
 				// formula representation lengths: ([1,1000] data) [x <= 500] https://www.desmos.com/calculator/b9qvvkinal, https://i.imgur.com/IMFY84S.png ; [x,y <= 1000] https://www.desmos.com/calculator/tjej0cpyju, https://i.imgur.com/1Z4WjJa.png ; [x <= 1000, y <= 100] https://www.desmos.com/calculator/zpe5zw41cm, https://i.imgur.com/6aCR6iq.png