Skip to content

Commit 01a8982

Browse files
xamidixamidi
committed
DRuleParser::compressAbstractDProof(): remove test code
The local struct AbstractDProof would previously allow to store generated theorems as tree::TreeNode objects rather than as std::string objects, upon changing a Boolean constant (for testing purposes). Using trees rather than strings turned out terribly inefficient.
1 parent 60ceab6 commit 01a8982

File tree

1 file changed

+29
-76
lines changed

1 file changed

+29
-76
lines changed

‎metamath/DRuleParser.cpp

+29-76
Original file line numberDiff line numberDiff line change
@@ -1844,7 +1844,6 @@ vector<string> DRuleParser::unfoldAbstractDProof(const vector<string>& abstractD
18441844
}
18451845

18461846
void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector<shared_ptr<DlFormula>>& abstractDProofConclusions, vector<string>& helperRules, vector<shared_ptr<DlFormula>>& helperRulesConclusions, vector<size_t>& indexEvalSequence, vector<size_t>& targetIndices, const vector<AxiomInfo>* customAxioms, bool targetEverything, vector<AxiomInfo>* filterForTheorems, bool concurrentDRuleSearch, size_t modificationRange, bool keepMaxRules, const string* vaultFile, bool sureSaves, bool skipFirstPrep) {
1847-
constexpr bool lowMemoryCollection = true; //### TODO
18481847
if (modificationRange >= 3 && UINT16_MAX < modificationRange) {
18491848
cerr << "[Proof compression] ERROR Requested D-proofs of lengths up to " << modificationRange << " (exceeding 2^16 = " << UINT16_MAX + 1 << " required indices). Aborting." << endl;
18501849
exit(0);
@@ -1970,8 +1969,7 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
19701969
const vector<tbb::concurrent_vector<AbstractDProof>>& extraData;
19711970
atomic<bool> active = true;
19721971
array<int64_t, 2> dRule; // i >= 0: proofElements[i], -1 <= i <= -35: axioms[-i - 1], i <= -64 && (-i & 64): extraData[(-i >> 7) & UINT16_MAX][-i >> 23] (i.e. up to 2^(64-1-23)-1 = 2^40-1 = 1099511627775 entries for D-proofs of each length)
1973-
string sResult; // used in case lowMemoryCollection
1974-
shared_ptr<DlFormula> tResult; // used in case !lowMemoryCollection
1972+
string sResult;
19751973
size_t fundamentalLength;
19761974
int64_t improvedOriginal = -1;
19771975
int64_t improvedByExtra = 0;
@@ -1981,40 +1979,19 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
19811979
sResult = f;
19821980
fundamentalLength = funLen;
19831981
}
1984-
AbstractDProof(const vector<tbb::concurrent_vector<AbstractDProof>>& extraData, const array<int64_t, 2>& r, const shared_ptr<DlFormula>& f, size_t funLen) :
1985-
extraData(extraData) {
1986-
dRule = r;
1987-
tResult = f;
1988-
fundamentalLength = funLen;
1989-
}
19901982
bool clearIfInactive() { // to free memory without removing the element in order to not touch indices
1991-
if (!active) {
1992-
tResult.reset();
1993-
return true;
1994-
}
1995-
return false;
1996-
}
1997-
bool clearIfInactive_lowMem() { // to free memory without removing the element in order to not touch indices
19981983
if (!active) {
19991984
sResult.clear();
20001985
return true;
20011986
}
20021987
return false;
20031988
}
2004-
string formulaString_numVars(bool lowMemoryCollection) const {
2005-
if (!active)
2006-
return "[inactive]";
2007-
return lowMemoryCollection ? sResult : DlCore::toPolishNotation_numVars(tResult);
2008-
}
2009-
string formulaString(bool lowMemoryCollection) const {
1989+
string formulaString() const {
20101990
if (!active)
20111991
return "[inactive]";
2012-
if (lowMemoryCollection) {
2013-
shared_ptr<DlFormula> _f;
2014-
DlCore::fromPolishNotation_noRename(_f, sResult);
2015-
return DlCore::toPolishNotation(_f);
2016-
} else
2017-
return DlCore::toPolishNotation(tResult);
1992+
shared_ptr<DlFormula> _f;
1993+
DlCore::fromPolishNotation_noRename(_f, sResult);
1994+
return DlCore::toPolishNotation(_f);
20181995
}
20191996
string toString() const override {
20201997
stringstream ss;
@@ -2031,11 +2008,11 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
20312008
}
20322009
return ss.str();
20332010
}
2034-
string toConclusionString(bool lowMemoryCollection) const {
2035-
return toString() + (active ? " = " + formulaString(lowMemoryCollection) : " (inactive)");
2011+
string toConclusionString() const {
2012+
return toString() + (active ? " = " + formulaString() : " (inactive)");
20362013
}
2037-
string toDetailedString(bool lowMemoryCollection) const {
2038-
return toString() + (active ? " = " + formulaString(lowMemoryCollection) + " (" : " (inactive; ") + "fundamental length " + to_string(fundamentalLength) + ")";
2014+
string toDetailedString() const {
2015+
return toString() + (active ? " = " + formulaString() + " (" : " (inactive; ") + "fundamental length " + to_string(fundamentalLength) + ")";
20392016
}
20402017
};
20412018
vector<tbb::concurrent_vector<AbstractDProof>> extraData; // relative abstract D-proofs of length index
@@ -2393,17 +2370,7 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
23932370
map<string, shared_ptr<DlFormula>> substitutions;
23942371
if (DlCore::tryUnifyTrees(antecedent, conditional_children[0], &substitutions)) {
23952372
consequent = DlCore::substitute(conditional_children[1], substitutions);
2396-
if (lowMemoryCollection)
2397-
consequent_isomorph = DlCore::toPolishNotation_numVars(consequent);
2398-
else { // Obtain unique variables.
2399-
DlCore::fromPolishNotation_noRename(consequent, consequent_isomorph = DlCore::toPolishNotation_numVars(consequent));
2400-
vector<string> vars = DlCore::primitivesOfFormula_ordered(consequent);
2401-
map<string, shared_ptr<DlFormula>> substitutions;
2402-
string varId = to_string(lenA) + "_" + to_string(iA) + "_" + to_string(lenB) + "_" + to_string(iB) + "_";
2403-
for (const string& v : vars)
2404-
substitutions.emplace(v, make_shared<DlFormula>(make_shared<String>(varId + v)));
2405-
consequent = DlCore::substitute(consequent, substitutions);
2406-
}
2373+
consequent_isomorph = DlCore::toPolishNotation_numVars(consequent);
24072374
// NOTE: In the final iteration, the only potentially useful new proofs (which thus shall be memorized) are those towards known intermediate conclusions, except in
24082375
// cases where a longer relative abstract proof with lower fundamental length could later be used as an improving replacement for a subproof towards a new formula.
24092376
// However, only storing proofs towards known intermediate conclusions here effectively enables the user to run with the next higher modification range (i.e. increased by two)
@@ -2458,10 +2425,7 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
24582425
obtainedConclusions.find(wAcc, consequent_isomorph);
24592426
wAcc->second = obtainedConclusionVal; // update 'obtainedConclusions'
24602427
}
2461-
if (lowMemoryCollection)
2462-
output.emplace_back(extraData, dRule, consequent_isomorph, funLen);
2463-
else
2464-
output.emplace_back(extraData, dRule, consequent, funLen);
2428+
output.emplace_back(extraData, dRule, consequent_isomorph, funLen);
24652429
if (improvedFor >= 0) {
24662430
output.back().improvedOriginal = improvedFor;
24672431
stringstream ss;
@@ -2495,7 +2459,7 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
24952459
if (l < 0 && (-l & 64)) {
24962460
const AbstractDProof& proof = extraData[(-l >> 7) & UINT16_MAX][-l >> 23];
24972461
fL = proof.fundamentalLength;
2498-
return lowMemoryCollection ? [&]() { shared_ptr<DlFormula> f; DlCore::fromPolishNotation_noRename(f, proof.sResult); return f; }() : proof.tResult;
2462+
return [&]() { shared_ptr<DlFormula> f; DlCore::fromPolishNotation_noRename(f, proof.sResult); return f; }();
24992463
} else {
25002464
fL = i < numRules ? fundamentalLengths[i] : 1;
25012465
return proofElements[i].result;
@@ -2544,8 +2508,8 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
25442508
shared_ptr<DlFormula> consequent;
25452509
string consequent_isomorph;
25462510
if (isCandidate(antecedent, conditional_children, lenA, iA, lenB, iB, funLen, consequent, consequent_isomorph, finalLoop)) {
2547-
if (vault.at(p.first)[i].second != (lowMemoryCollection ? consequent_isomorph : DlCore::toPolishNotation_numVars(consequent))) {
2548-
cerr << "[Proof compression] ERROR Mismatching stored vault entry " << vault.at(p.first)[i].first << " = " << vault.at(p.first)[i].second << " != " << (lowMemoryCollection ? consequent_isomorph : DlCore::toPolishNotation_numVars(consequent)) << " = D(" << conditional_str << ")(" << antecedent_str << "). Aborting." << endl;
2511+
if (vault.at(p.first)[i].second != consequent_isomorph) {
2512+
cerr << "[Proof compression] ERROR Mismatching stored vault entry " << vault.at(p.first)[i].first << " = " << vault.at(p.first)[i].second << " != " << consequent_isomorph << " = D(" << conditional_str << ")(" << antecedent_str << "). Aborting." << endl;
25492513
exit(0);
25502514
}
25512515
array<int64_t, 2> dRule { conditional_loc, antecedent_loc };
@@ -2622,7 +2586,7 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
26222586
if (!eB.active)
26232587
return;
26242588
shared_ptr<DlFormula> _f;
2625-
const shared_ptr<DlFormula>& conditional = lowMemoryCollection ? [&]() { DlCore::fromPolishNotation_noRename(_f, eB.sResult); return _f; }() : eB.tResult;
2589+
const shared_ptr<DlFormula>& conditional = [&]() { DlCore::fromPolishNotation_noRename(_f, eB.sResult); return _f; }();
26262590
const vector<shared_ptr<DlFormula>>& conditional_children = conditional->getChildren();
26272591
if (conditional_children.size() != 2 || conditional->getValue()->value != DlCore::terminalStr_imply())
26282592
return; // 'conditional' is no conditional => skip already
@@ -2659,7 +2623,7 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
26592623
if (addFunLen_overflow(eA.fundamentalLength, funLen_known(eB, iB), &funLen))
26602624
continue; // skip results with fundamental lengths above SIZE_MAX
26612625
shared_ptr<DlFormula> _f;
2662-
const shared_ptr<DlFormula>& antecedent = lowMemoryCollection ? [&]() { DlCore::fromPolishNotation_noRename(_f, eA.sResult); return _f; }() : eA.tResult;
2626+
const shared_ptr<DlFormula>& antecedent = [&]() { DlCore::fromPolishNotation_noRename(_f, eA.sResult); return _f; }();
26632627
shared_ptr<DlFormula> consequent;
26642628
string consequent_isomorph;
26652629
if (isCandidate(antecedent, conditional_children, lenA, iA, lenB, iB, funLen, consequent, consequent_isomorph, finalLoop)) {
@@ -2679,7 +2643,7 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
26792643
if (!eB.active)
26802644
return;
26812645
shared_ptr<DlFormula> _f;
2682-
const shared_ptr<DlFormula>& conditional = lowMemoryCollection ? [&]() { DlCore::fromPolishNotation_noRename(_f, eB.sResult); return _f; }() : eB.tResult;
2646+
const shared_ptr<DlFormula>& conditional = [&]() { DlCore::fromPolishNotation_noRename(_f, eB.sResult); return _f; }();
26832647
const vector<shared_ptr<DlFormula>>& conditional_children = conditional->getChildren();
26842648
if (conditional_children.size() != 2 || conditional->getValue()->value != DlCore::terminalStr_imply())
26852649
return; // 'conditional' is no conditional => skip already
@@ -2701,7 +2665,7 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
27012665
_distinguishedFormula = DlCore::substitute(f, substitutions);
27022666
return _distinguishedFormula;
27032667
};
2704-
const shared_ptr<DlFormula>& antecedent = lowMemoryCollection ? distinguishVariables([&]() { DlCore::fromPolishNotation_noRename(_distinguishedFormula, eA.sResult); return _distinguishedFormula; }()) : (lenA == lenB && iA == iB ? distinguishVariables(eA.tResult) : eA.tResult);
2668+
const shared_ptr<DlFormula>& antecedent = distinguishVariables([&]() { DlCore::fromPolishNotation_noRename(_distinguishedFormula, eA.sResult); return _distinguishedFormula; }());
27052669
shared_ptr<DlFormula> consequent;
27062670
string consequent_isomorph;
27072671
if (isCandidate(antecedent, conditional_children, lenA, iA, lenB, iB, funLen, consequent, consequent_isomorph, finalLoop)) {
@@ -2724,22 +2688,13 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
27242688
if (!output.empty()) {
27252689
chrono::time_point<chrono::steady_clock> startTime = chrono::steady_clock::now();
27262690
atomic<size_t> c = 0, d = 0;
2727-
if (lowMemoryCollection)
2728-
tbb::parallel_for_each(output.begin(), output.end(), [&](AbstractDProof& proof) {
2729-
if (!proof.sResult.empty()) {
2730-
if (proof.clearIfInactive_lowMem())
2731-
c++;
2732-
} else
2733-
d++;
2734-
});
2735-
else
2736-
tbb::parallel_for_each(output.begin(), output.end(), [&](AbstractDProof& proof) {
2737-
if (proof.tResult.get()) {
2738-
if (proof.clearIfInactive())
2739-
c++;
2740-
} else
2741-
d++;
2742-
});
2691+
tbb::parallel_for_each(output.begin(), output.end(), [&](AbstractDProof& proof) {
2692+
if (!proof.sResult.empty()) {
2693+
if (proof.clearIfInactive())
2694+
c++;
2695+
} else
2696+
d++;
2697+
});
27432698
cout << FctHelper::round(static_cast<long double>(chrono::duration_cast<chrono::microseconds>(chrono::steady_clock::now() - startTime).count()) / 1000.0, 2) << " ms taken to clear " << c << " of " << output.size() << " proof" << (output.size() == 1 ? "" : "s") << " from extraData[" << len << "], " << output.size() - c - d << " remain active. (" << d << " already clear and skipped)" << endl;
27442699
}
27452700
}
@@ -2779,7 +2734,7 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
27792734
}
27802735
improvements.emplace(i, location);
27812736
const AbstractDProof& proof = extraData[(-location >> 7) & UINT16_MAX][-location >> 23];
2782-
cout << "[Summary] Rule [" << i << "] (fundamental length " << fundamentalLengths[i] << ") improved by: " << proof.toDetailedString(lowMemoryCollection) << endl;
2737+
cout << "[Summary] Rule [" << i << "] (fundamental length " << fundamentalLengths[i] << ") improved by: " << proof.toDetailedString() << endl;
27832738
auto obtainBestVariantString = [&](const AbstractDProof& proof, const auto& me) -> string {
27842739
stringstream ss;
27852740
ss << "D";
@@ -2808,8 +2763,6 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
28082763
size_t optimizedFunLen = measure(optimizedRule);
28092764
cout << "[Summary] Rule [" << i << "] " << string(24 + FctHelper::digitsNum_uint64(fundamentalLengths[i]), ' ') << "optimized: " << optimizedRule << " (fundamental length " << optimizedFunLen << ")" << endl;
28102765
}
2811-
if (proof.improvedByExtra)
2812-
cout << "[WARNING] Rule [" << i << "] improvement has proof.improvedByExtra = " << proof.improvedByExtra << endl; //### TODO Remove after testing.
28132766
}
28142767
}
28152768

@@ -2837,13 +2790,13 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
28372790
const AbstractDProof& current = extraData[(e >> 7) & UINT16_MAX][e >> 23];
28382791
int64_t best = e; // already negated
28392792
size_t minFunLen = measure(current.toString());
2840-
//#cout << "> Found funLen: " << minFunLen << " (of " << current.toConclusionString(lowMemoryCollection) << ") <initial>" << endl;
2793+
//#cout << "> Found funLen: " << minFunLen << " (of " << current.toConclusionString() << ") <initial>" << endl;
28412794
auto iterateImprovingExtras = [&](const AbstractDProof& p, const auto& me) -> const AbstractDProof& {
28422795
int64_t l = -p.improvedByExtra;
28432796
if (l) {
28442797
const AbstractDProof& next = extraData[(l >> 7) & UINT16_MAX][l >> 23];
28452798
size_t funLen = measure(next.toString());
2846-
//#cout << "> Found funLen: " << funLen << " (of " << next.toConclusionString(lowMemoryCollection) << ") <subsequent>" << endl;
2799+
//#cout << "> Found funLen: " << funLen << " (of " << next.toConclusionString() << ") <subsequent>" << endl;
28472800
if (funLen < minFunLen) {
28482801
best = l;
28492802
minFunLen = funLen;
@@ -2874,7 +2827,7 @@ void DRuleParser::compressAbstractDProof(vector<string>& retractedDProof, vector
28742827
const AbstractDProof& candidate = extraData[(location >> 7) & UINT16_MAX][location >> 23];
28752828
size_t funLen_candidate = measure(candidate.toString());
28762829
stringstream ss1;
2877-
ss1 << "[Summary] Step: (" << index << ", " << dProof << " -> " << candidate.toConclusionString(lowMemoryCollection) << "), fundamental lengths (" << funLen << ", " << funLen_candidate << ")" << endl;
2830+
ss1 << "[Summary] Step: (" << index << ", " << dProof << " -> " << candidate.toConclusionString() << "), fundamental lengths (" << funLen << ", " << funLen_candidate << ")" << endl;
28782831
cout << ss1.str() << flush;
28792832
if (vaultOutput)
28802833
ss << ss1.str();

0 commit comments

Comments
 (0)