--transform -z: avoid duplicate registrations of evaluation indices

- fixes that duplicate empty rules would be generated upon compression
+ make steps in w3.txt well-ordered (according to fix; [43] called [52])
  - files were previously generated without 'indexEvalSequence'
    rebuilding, of which files other than w3.txt were not affected

Author: xamidi

data/w3.txt

@@ -7,7 +7,7 @@
 % Full summary: pmGenerator --transform data/w3.txt -f -n -t . -j 1
 % Step counting: pmGenerator --transform data/w3.txt -f -n -t . -p -2 -d
 %                pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
-% Compact (1970 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw,CCCCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqpyCCyzCaz,CCCpCqrsCCqrs,CCCpqrCqr,CCCNpqrCpr,CCNppCqp,CCCCNpqCrqpCsp,CpCCpqCrq,CCCNCNpqrsCps,CpCqCrp,CCCCCpqrCsrtCqt,CNNCpqCrCpq,CCNCCpCqpNrsCrs,CCpNpCqNp,CCpCqNpCrCqNp,CCCpqrCNpr,CCNpqCNCrpq,CCpqCNCprq,CCNpqCNCrCspq,CCpqCCNppq,CCNCpqrCCrqCpq,CCpCpqCpq,CCCCpqCrqsCps,CCpqCNCprq,CCpCqrCqCpr
+% Compact (1951 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw,CCCCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqpyCCyzCaz,CCCpCqrsCCqrs,CCCpqrCqr,CCCNpqrCpr,CCNppCqp,CCCCNpqCrqpCsp,CpCCpqCrq,CCCNCNpqrsCps,CpCqCrp,CCCCCpqrCsrtCqt,CNNCpqCrCpq,CCNCCpCqpNrsCrs,CCpNpCqNp,CCpCqNpCrCqNp,CCCpqrCNpr,CCNpqCNCrpq,CCpqCNCprq,CCNpqCNCrCspq,CCpqCCNppq,CCNCpqrCCrqCpq,CCpCpqCpq,CCCCpqCrqsCps,CCpCqrCqCpr
 % Concrete (296514 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
 
     CpCCNqCCNrsCptCCtqCrq = 1
@@ -65,25 +65,25 @@
 [41] CCNppp = D[33]DDD[0]D[18]DDD1[6]1[16][36]1
 
 [42] CCNpqCNCrpq = D[7]D[0]D[18]DD[7]D[0]D[33]D[18][16]D[18][40]
-[43] CNCpqCrCsp = D[52][27]
-[44] CCNpqCNCrCspq = D[7]D[0]D[18]DD[7]D[0]DD[7][34][20]D[18]D[13][40]
-[45] CCpCpqCrCpq = D[0][43]
-[46] CCpqCCNppq = D[7]D[0]D[39]D[0]DD[23]D[17]D[18][36]1
-[47] CCNCpqrCCrqCpq = DD[46]DD1[21]DDD[3]D[3]D1[7][6][13]D[44]1
-[48] CCpCpqCpq = DD[45][45]1
-[49] CCCCpqCrqsCps = DD[13]D1D[6]D[3]DD[15]11D[46]D[28][48]
-[50] CCpqCCNqpq = D[0]D[49][46]
-[51] CpCCpqq = D[49][48]
-[52] CCpqCNCprq = D[7]D[0]DDD[0]D[28]D[17]D[19]D[14]D[19][32]DDD[13]D1DDD[15]D[3]D[3]D1[11]1[0]1DD[3][11][37]1
+[43] CCpqCNCprq = D[7]D[0]DDD[0]D[28]D[17]D[19]D[14]D[19][32]DDD[13]D1DDD[15]D[3]D[3]D1[11]1[0]1DD[3][11][37]1
+[44] CNCpqCrCsp = D[43][27]
+[45] CCNpqCNCrCspq = D[7]D[0]D[18]DD[7]D[0]DD[7][34][20]D[18]D[13][40]
+[46] CCpCpqCrCpq = D[0][44]
+[47] CCpqCCNppq = D[7]D[0]D[39]D[0]DD[23]D[17]D[18][36]1
+[48] CCNCpqrCCrqCpq = DD[47]DD1[21]DDD[3]D[3]D1[7][6][13]D[45]1
+[49] CCpCpqCpq = DD[46][46]1
+[50] CCCCpqCrqsCps = DD[13]D1D[6]D[3]DD[15]11D[47]D[28][49]
+[51] CCpqCCNqpq = D[0]D[50][47]
+[52] CpCCpqq = D[50][49]
 
 % Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 16469 steps
-[53] CCpqCCqrCpr = DDD1[52]D[26]D[46][51][47]
+[53] CCpqCCqrCpr = DDD1[43]D[26]D[47][52][48]
 
 % Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 23321 steps
-[54] CCNpNqCqp = DD[7][37]DD[48]D[0]D[42][43]DD[50]D[18]D[19][33]D[42]D[48]DD[7]D[0]D[25][38][44]
+[54] CCNpNqCqp = DD[7][37]DD[49]D[0]D[42][44]DD[51]D[18]D[19][33]D[42]D[49]DD[7]D[0]D[25][38][45]
 
 [55] CCCCpqCrqsCCrps = D[53][53]
-[56] CCpCqrCqCpr = D[55]D[53][51]
+[56] CCpCqrCqCpr = D[55]D[53][52]
 
 % Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 254925 steps
-[57] CCpCqrCCpqCpr = D[56]D[55]D[47]DD[56]D[39][50]D[56]D[55][39]
+[57] CCpCqrCCpqCpr = D[56]D[55]D[48]DD[56]D[39][51]D[56]D[55][39]

metamath/DRuleParser.cpp

@@ -2164,8 +2164,12 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
 	// 6. Rebuild 'indexEvalSequence' (if some rules changed).
 	if (modified) {
 		vector<size_t> newIndexEvalSequence;
+		set<size_t> registered;
 		set<size_t> explored;
-		auto explore = [&](const string& rule, size_t i, const auto& me) -> void { // similar to 'auto parse' in DRuleParser::parseAbstractDProof(), but everything is parsed already
+
+		// Similar to 'auto parse' in DRuleParser::parseAbstractDProof(), but everything is parsed already.
+		// Additionally, need to avoid duplicate registration of evaluation indices, which here could occur due to non-orderliness of the input.
+		auto explore = [&](const string& rule, size_t i, const auto& me) -> void {
 			vector<DProofInfo> rawParseData;
 			string::size_type pos = rule.find('[');
 			if (pos != string::npos) {
@@ -2185,7 +2189,10 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
 						me(num < retractedDProof.size() ? retractedDProof[num] : helperRules[num - retractedDProof.size()], num, me);
 						explored.emplace(num);
 					}
-					newIndexEvalSequence.push_back(i);
+					if (!registered.count(i)) {
+						newIndexEvalSequence.push_back(i);
+						registered.emplace(i);
+					}
 					return;
 				} else {
 					bool refLhs = pos == 1;
@@ -2221,8 +2228,10 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
 					}
 				}
 			}
-			newIndexEvalSequence.push_back(i);
-			return;
+			if (!registered.count(i)) {
+				newIndexEvalSequence.push_back(i);
+				registered.emplace(i);
+			}
 		};
 		for (size_t i = 0; i < retractedDProof.size(); i++)
 			explore(retractedDProof[i], i, explore);