diff --git a/README.html b/README.html index 08137c1..d6e60dc 100644 --- a/README.html +++ b/README.html @@ -444,12 +444,13 @@

Usage

-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] [-t <string>] [-e] [-i <limit or -1>] [-l <limit or -1>] [-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>] [-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 -p: only keep subproofs with primitive lengths not exceeding the given limit ; default: -1 -n: specify and print formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0") + -u: print formulas in infix notation with operators as Unicode characters ; does not affect input format (for which '-n' can still be specified) -t: only transform proofs of specified theorems (proven by subsequences of the input), given by a comma-separated string ; "." to keep all conclusions ; default: final theorem only -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 diff --git a/README.md b/README.md index 13fa16e..e0a84b4 100644 --- a/README.md +++ b/README.md @@ -73,12 +73,13 @@ 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 [-s ] [-j ] [-p ] [-n] [-t ] [-e] [-i ] [-l ] [-f] [-o ] [-d] + --transform [-s ] [-j ] [-p ] [-n] [-u] [-t ] [-e] [-i ] [-l ] [-f] [-o ] [-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 -p: only keep subproofs with primitive lengths not exceeding the given limit ; default: -1 -n: specify and print formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0") + -u: print formulas in infix notation with operators as Unicode characters ; does not affect input format (for which '-n' can still be specified) -t: only transform proofs of specified theorems (proven by subsequences of the input), given by a comma-separated string ; "." to keep all conclusions ; default: final theorem only -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 diff --git a/data/w3.txt b/data/w3.txt index 66dcc98..70aebcc 100644 --- a/data/w3.txt +++ b/data/w3.txt @@ -7,8 +7,8 @@ % 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 (2367 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCpCqrsCCqrs,CCCCCpqrCqrsCts,CCCpqrCqr,CCCNpqrCpr,CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp,CCCCNpqCrqpCsp,CpCCpqCrq,CpCqCrp,CCCCCCpqCrqsNttCut,CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy,CCCCCpqrCsrtCqt,CCCpCqrsCrs,CCpNCCqCrqpCsNCCqCrqp,CCNCCpCqpNrsCrs,CCCpqCNprCsCNpr,CpCCNCqrrCqr,CCpqCNNpq,CCNNpqCpq,CCNpqCNCrpq,CCNpqCNCrCspq,CCpNCNppCqNCNpp,CNCpqCrCsp,CCpCpqCpq,CCpqCNCprq,CCCpqrCNpr,CCpqCCNppq,CpCCpqq,CCpqCCNqpq,CCpCqrCqCpr -% Concrete (5271958 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e +% Compact (2509 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCCCpCCqrCsrtCCCqrCsrtuCvu,CCCpCqrsCCqrs,CCCCCpqrCqrsCts,CCpqCCCpqrCsr,CCCpqrCqr,CCCNpqrCpr,CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp,CCNppCqp,CCCCNpqCrqpCsp,CCCNpqCCrCsCtsqCCquCpu,CpCCpqCrq,CpCqCrp,CCCCCCpqCrqsNttCut,CCCCCNpqrCsrtCpt,CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy,CCCCCpqrCsrtCqt,CCCpCqrsCrs,CNNCpqCrCpq,CCNCCpCqpNrsCrs,CCCpqCNprCsCNpr,CpCCNCqrrCqr,CCpNpCqNp,CCpqCNNpq,CCCpqrCNpr,CCpNCNppCqNCNpp,CpCqCrNNp,CCNpqCNCrpq,CCNpqCNCrCspq,CCpqCCNppq,CNCpqCrCsp,CCpCpqCpq,CCpqCCNqpq,CpCCpqq,CCpCqrCqCpr +% Concrete (3128030 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e CpCCNqCCNrsCptCCtqCrq = 1 [0] CCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqp = D11 @@ -27,76 +27,80 @@ [13] CCCpCqrsCCqrs = DD1[10]1 [14] CCCCCpCCqrCsrtCCCqrCsrtCuCCCqrCsrtCCCuCCCqrCsrtvCwv = D[3]D[3][4] [15] CCCCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpwCxCCqwCpwCCCxCCqwCpwyCzy = D[3]D[3]D1[7] -[16] CCCCCpqrCqrsCts = DD[13][0]1 -[17] CCCCCCpqCrqsCtsuCqu = DD[13]DD[3]111 -[18] CCCNpqCCCCrstCstqCCquCpu = D[3]DD[16]11 -[19] CCpqCrCpq = D[13][10] +[16] CCCpqCrqCCCCpqCrqsCts = D[3][11] +[17] CCCCCpqrCqrsCts = DD[13][0]1 +[18] CCCCCCpqCrqsCtsuCqu = DD[13]DD[3]111 +[19] CCCNpqCCCCrstCstqCCquCpu = D[3]DD[17]11 [20] CCpqCCCpqrCsr = D[13][11] -[21] CCCpqrCqr = DDD[16]D[3][2]1[0] +[21] CCCpqrCqr = DDD[17]D[3][2]1[0] [22] CCCNpqrCpr = D[0]D[12][13] -[23] CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp = D1D[6][18] -[24] CCNppCqp = D[0]D[22][0] -[25] CpCqCrq = DD[16][16]1 -[26] CCNpCCNqrCCsCtCutvCCvpCqp = D1[25] +[23] CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp = D1D[6][19] +[24] CpCCqpCrp = D[22][0] +[25] CCNppCqp = D[0][24] +[26] CpCqCrq = DD[17][17]1 +[27] CCNpCCNqrCCsCtCutvCCvpCqp = D1[26] % Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 67 steps -[27] CpCqp = D[25]1 +[28] CpCqp = D[26]1 -[28] CCNpCCNqrCCsCtsuCCupCqp = D1[27] -[29] CCCCNpqCrqpCsp = D[0]D[17]DD[3][8][3] -[30] CCCNpqCCrCsCtsqCCquCpu = D[3][26] -[31] CpCCpqCrq = DD[1]DDD[3]D[3]D1[8][3][13][0] -[32] CpCqCrp = D[21][19] -[33] CCCCCCpqCrqsNttCut = D[0]D[21]DDD1[6]1D[6][10] -[34] CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy = D[13]D1D[13][28] -[35] CCCCCpqrCsrtCqt = DD[13]DD[3]D[13]1[24]1 +[29] CCNpCCNqrCCsCtsuCCupCqp = D1[28] +[30] CCCCNpqCrqpCsp = D[0]D[18]DD[3][8][3] +[31] CCCNpqCCrCsCtsqCCquCpu = D[3][27] +[32] CpCCpqCrq = DD[1]DDD[3]D[3]D1[8][3][13][0] +[33] CCCNpqCCrCsCtsuCCuvCpv = D[13][27] +[34] CpCqCrp = D[21]D[13][10] +[35] CCCCCCpqCrqsNttCut = D[0]D[21]DDD1[6]1D[6][10] +[36] CCCCCNpqrCsrtCpt = DD[13]D1DDD[17]D[3]D[3]D1[11]1[0]1 +[37] CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy = D[13]D1D[13][29] +[38] CCCCCpqrCsrtCqt = DD[13]DD[3]D[13]1[25]1 % Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 127 steps -[36] CpCNpq = D[22]D[7][24] +[39] CpCNpq = D[22]D[7][25] -[37] CCCpCqrsCrs = DD1[24]DD[15][6][13] +[40] CCCpCqrsCrs = DD1[25]DD[15][6][13] % Identity principle (Cpp), i.e. 0→0 ; 135 steps -[38] Cpp = DD[22]D[0][31]1 +[41] Cpp = DD[22]D[0][32]1 -[39] CCNpCCNqrCCsstCCtpCqp = D1[38] -[40] CCpNCCqCrqpCsNCCqCrqp = D[28]DD[29]DD[6]D[3]D1[13]D[29]D[1]DD[0]D[12]D[0]DD[14][5][13]DD[0]DDD[3]D[3]D1D[6][3][13][13][12]1 -[41] CCNCCpCqpNrsCrs = D[18][40] -[42] CpCqCrNCCsCtsNp = D[41][32] -[43] CCCpqCNprCsCNpr = D[23]D[35]D[20]D[22]DD[13][26]D[22][40] -[44] CpCCNCqrrCqr = DD[39]D[21]DDD[13]D1DDD[16]D[3]D[3]D1[11]1[0]1DD[3][11][41][29] -[45] CCpqCCCrrpq = D[39][44] -[46] CCpqCNNpq = DD[33]DD[30]D[39]D[22]D[13][42][31]1 -[47] CCNNpqCpq = D[34]D[23]D[35]D[20]DD[22]D[39]D[41][31]1 -[48] CpCqCrNNp = D[47][32] -[49] CpCqCrNNCNps = D[22][48] +[42] CCNpCCNqrCCsstCCtpCqp = D1[41] +[43] CNNCpqCrCpq = DD[30]DD[6]D[3]D1[13]D[30]D[1]DD[0]D[12]D[0]DD[14][5][13]DD[0]DDD[3]D[3]D1D[6][3][13][13][12]1 +[44] CCpNCCqCrqpCsNCCqCrqp = D[29][43] +[45] CCNCCpCqpNrsCrs = D[19][44] +[46] CpCqCrNCCsCtsNp = D[45][34] +[47] CCCpqCNprCsCNpr = D[23]D[38]D[20]D[22]D[33]D[22][44] +[48] CpCCNCqrrCqr = DD[42]D[21]D[36]D[16][45][30] +[49] CCCpCqpNCNNCNrrsCtr = DD[31]D[42]D[22][46][25] +[50] CCpNpCqNp = D[23]D[38]D[20]DD[22]D[42]D[45][32]1 +[51] CCpqCNNpq = DD[35]DD[31]D[42]D[22]D[13][46][32]1 +[52] CCNNpqCpq = D[31][50] +[53] CCCpqrCNpr = DDD[42]D[38]D[20]D[22]D[33]D[13]D[22]D[42][43][20]1 +[54] CCpNCNppCqNCNpp = D[23]DD[30]D[20]D[21][49]1 +[55] CpCqCrNNp = D[22]D[42]D[21]DD[31]D[42]D[21][46][24] +[56] CpCqCrNNCNps = D[22][55] -% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 2225 steps -[50] CCNppp = D[47]DD[33]DD[30]D[39]D[22][42][24]1 +% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 2177 steps +[57] CCNppp = D[52]DD[35][49]1 -[51] CCNpqCNCrpq = D[34]D[23]D[46]D[21][48] -[52] CCNpqCNCrCspq = D[34]D[23]D[46]D[37][48] -[53] CCpNCNppCqNCNpp = D[23]D[46]D[35]D[31]D[45][50] -[54] CNCpqCrCsp = DDD[45][47]DD[23]DD[34]D[23]D[46][49][32]D[46]D[23]D[51][32]D[52]DD[43]DD[0]DD[14][6][13][12]1 -[55] CCpCpqCrCpq = D[23][54] -[56] CpCCqCqrCqr = D[55][55] -[57] CCpCpqCpq = D[56][56] -[58] CCpqCNCprq = D[34]D[23]DD[57][43]D[47]D[21]D[13][19] -[59] CCCpqrCNpr = D[34]D[23]D[58][48] -[60] CCpqCCNppq = DD[13]D1[1]D[23]DD[34]DD[34]D[23]D[46]DD[34][53][32]D[59][53][32] -[61] CCpCqCprCqCpr = D[57]D[23]D[51][54] -[62] CCNCpqrCCrqCpq = DD[60][37]D[52]1 -[63] CpCCpqq = DD[61]D[17][15]DD[28][44][57] -[64] CCpqCCNqpq = D[23]DDD[13][23]D[60]D[35][57][60] +[58] CCNpqCNCrpq = D[37]D[23]D[51]D[21][55] +[59] CCNpqCNCrCspq = D[37]D[23]D[51]D[40][55] +[60] CCpqCCNppq = DD[13]D1[1]D[23]DD[37]DD[37]D[23]D[51]DD[37][54][34]D[53][54][34] +[61] CCNCpqrCCrqCpq = DD[60][40]D[59]1 +[62] CNCpqCrCsp = DDDD[42][48][52]DD[23]DD[37]D[23]D[51][56][34]D[51]D[23]D[58][34]D[59]DD[47]DD[0]DD[14][6][13][12]1 +[63] CCpCpqCrCpq = D[23][62] +[64] CpCCqCqrCqr = D[63][63] +[65] CCpCpqCpq = D[64][64] +[66] CCpqCCNqpq = D[23]DDD[13][23]D[60]D[38][65][60] +[67] CCpCqCprCqCpr = D[65]D[23]D[58][62] +[68] CpCCpqq = DD[67]D[18][15]DD[29][48][65] -% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 303787 steps -[65] CCpqCCqrCpr = DDD1[58]D[27]D[60][63][62] +% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 180451 steps +[69] CCpqCCqrCpr = DDD1D[37]D[23]DD[65][47]D[36]D[16][50]D[28]D[60][68][61] -% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 306275 steps -[66] CCNpNqCqp = D[47]D[61]DD[64]D[21]D[22][41]D[51]D[57]DD[34]D[23][49][52] +% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 182879 steps +[70] CCNpNqCqp = D[52]D[67]DD[66]D[21]D[22][45]D[58]D[65]DD[37]D[23][56][59] -[67] CCCCpqCrqsCCrps = D[65][65] -[68] CCpCqrCqCpr = D[67]D[65][63] +[71] CCCCpqCrqsCCrps = D[69][69] +[72] CCpCqrCqCpr = D[71]D[69][68] -% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 4659203 steps -[69] CCpCqrCCpqCpr = D[68]D[67]D[62]DD[68]D[59][64]D[68]D[67][59] +% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 2762055 steps +[73] CCpCqrCCpqCpr = D[72]D[71]D[61]DD[72]D[53][66]D[72]D[71][53] diff --git a/logic/DlProofEnumerator.cpp b/logic/DlProofEnumerator.cpp index 8cb1376..028c3d4 100644 --- a/logic/DlProofEnumerator.cpp +++ b/logic/DlProofEnumerator.cpp @@ -981,7 +981,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, const string* filterForTheorems, bool abstractProofStrings, size_t storeIntermediateUnfoldingLimit, size_t maxLengthToComputeDProof, const string* outputFile, bool debug) { +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, const string* outputFile, bool debug) { vector customAxioms; vector abstractDProof_input; vector requiredIntermediateResults; @@ -1009,14 +1009,15 @@ void DlProofEnumerator::recombineProofSummary(const string& input, bool useInput const vector abstractDProof = DRuleParser::recombineAbstractDProof(abstractDProof_input, conclusions, &customAxioms, filterForTheorems ? *filterForTheorems != "." ? &filterForTheorems_axInfo : &requiredIntermediateResults : nullptr, conclusionsWithHelperProofs ? &conclusionsWithHelperProofs_axInfo : nullptr, minUseAmountToCreateHelperProof, &requiredIntermediateResults, debug, maxLengthToKeepProof, abstractProofStrings, storeIntermediateUnfoldingLimit, maxLengthToComputeDProof); auto print = [&](ostream& mout) -> string::size_type { + auto infixUnicode = [](const shared_ptr& 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 = normalPolishNotation ? DlCore::toPolishNotation(ax.refinedAxiom) : DlCore::toPolishNotation_noRename(ax.refinedAxiom); + 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 = normalPolishNotation ? DlCore::toPolishNotation(conclusions[i]) : DlCore::toPolishNotation_noRename(conclusions[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(); diff --git a/logic/DlProofEnumerator.h b/logic/DlProofEnumerator.h index 37b0e54..17b2157 100644 --- a/logic/DlProofEnumerator.h +++ b/logic/DlProofEnumerator.h @@ -69,7 +69,7 @@ struct DlProofEnumerator { static void sampleCombinations(); static void printProofs(const std::vector& 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); static void convertProofSummaryToAbstractDProof(const std::string& input, std::vector& out_customAxioms, std::vector& out_abstractDProof, std::vector* optOut_requiredIntermediateResults = nullptr, bool useInputFile = false, bool normalPolishNotation = 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, const std::string* filterForTheorems = nullptr, bool abstractProofStrings = true, std::size_t storeIntermediateUnfoldingLimit = SIZE_MAX, std::size_t maxLengthToComputeDProof = 134217728, const std::string* outputFile = nullptr, bool debug = 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, const std::string* outputFile = nullptr, bool debug = 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, const std::string* outputFile = nullptr, bool debug = false); // Data prediction diff --git a/main.cpp b/main.cpp index a4a5cbc..1988db0 100644 --- a/main.cpp +++ b/main.cpp @@ -96,12 +96,13 @@ static const map& cmdInfo() { " -o: redirect the result's output to the specified file\n" " -d: print debug information\n"; _[Task::TransformProofSummary] = - " --transform [-s ] [-j ] [-p ] [-n] [-t ] [-e] [-i ] [-l ] [-f] [-o ] [-d]\n" + " --transform [-s ] [-j ] [-p ] [-n] [-u] [-t ] [-e] [-i ] [-l ] [-f] [-o ] [-d]\n" " Transform proof summary (as by '--parse [...] -s') into recombined variant ; ignores configured system (proof summaries provide their own axioms) ; \",\" represents LF\n" " -s: list a subproof with its conclusion if it occurs in the given comma-separated list of conclusions\n" " -j: join common subproofs together when they are used at least a given amount of times ; default: 2\n" " -p: only keep subproofs with primitive lengths not exceeding the given limit ; default: -1\n" " -n: specify and print formulas in normal Polish notation (e.g. \"CpCqp\"), not with numeric variables (e.g. \"C0C1.0\")\n" + " -u: print formulas in infix notation with operators as Unicode characters ; does not affect input format (for which '-n' can still be specified)\n" " -t: only transform proofs of specified theorems (proven by subsequences of the input), given by a comma-separated string ; \".\" to keep all conclusions ; default: final theorem only\n" " -e: keep expanded proof strings ; show fully detailed condensed detachment proofs rather than allowing them to contain references\n" " -i: decrease memory requirements but increase time consumption by not storing intermediate unfoldings that exceed a certain length ; default: -1\n" @@ -371,10 +372,10 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { , , if (i + 1 >= argc) return printUsage("Missing parameter for \"--" + command + "\".", recent(command)); tasks.emplace_back(Task::ParseAndPrintProofs, map { { "string", argv[++i] }, { "outputFile", "" } }, map { { "minUseAmountToCreateHelperProof", 2 } }, map { { "useInputFile", false }, { "useOutputFile", false }, { "normalPolishNotation", false }, { "unicodeInfixNotation", false }, { "conclusionsOnly", false }, { "summaryMode", false }, { "abstractProofStrings", true }, { "debug", false }, { "whether -j was called", false } }); - } else if (command == "transform") { // --transform [-s ] [-j ] [-p ] [-n] [-t ] [-e] [-i ] [-l ] [-f] [-o ] [-d] + } else if (command == "transform") { // --transform [-s ] [-j ] [-p ] [-n] [-u] [-t ] [-e] [-i ] [-l ] [-f] [-o ] [-d] if (i + 1 >= argc) return printUsage("Missing parameter for \"--" + command + "\".", recent(command)); - tasks.emplace_back(Task::TransformProofSummary, map { { "string", argv[++i] }, { "conclusionsWithHelperProofs", "" }, { "filterForTheorems", "" }, { "outputFile", "" } }, map { { "minUseAmountToCreateHelperProof", 2 }, { "maxLengthToKeepProof", -1 }, { "storeIntermediateUnfoldingLimit", -1 }, { "maxLengthToComputeDProof", 134217728 } }, map { { "useInputFile", false }, { "useOutputFile", false }, { "normalPolishNotation", false }, { "abstractProofStrings", true }, { "debug", false }, { "whether -s was called", false }, { "whether -t was called", false } }); + tasks.emplace_back(Task::TransformProofSummary, map { { "string", argv[++i] }, { "conclusionsWithHelperProofs", "" }, { "filterForTheorems", "" }, { "outputFile", "" } }, map { { "minUseAmountToCreateHelperProof", 2 }, { "maxLengthToKeepProof", -1 }, { "storeIntermediateUnfoldingLimit", -1 }, { "maxLengthToComputeDProof", 134217728 } }, map { { "useInputFile", false }, { "useOutputFile", false }, { "normalPolishNotation", false }, { "printInfixUnicode", false }, { "abstractProofStrings", true }, { "debug", false }, { "whether -s was called", false }, { "whether -t was called", false } }); } else if (command == "unfold") { // --unfold [-n] [-t ] [-i ] [-l ] [-w] [-f] [-o ] [-d] if (i + 1 >= argc) return printUsage("Missing parameter for \"--" + command + "\".", recent(command)); @@ -777,6 +778,9 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { , , case Task::ParseAndPrintProofs: // --parse -u (print formulas in infix notation with operators as Unicode characters) tasks.back().bln["unicodeInfixNotation"] = true; break; + case Task::TransformProofSummary: // --transform -u (print formulas in infix notation with operators as Unicode characters) + tasks.back().bln["printInfixUnicode"] = true; + break; case Task::ConclusionLengthPlot: // --plot -u (include unfiltered proof files) tasks.back().bln["includeUnfiltered"] = true; break; @@ -873,7 +877,7 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { , , ss << ++index << ". printProofs(" << (t.bln["useInputFile"] ? "{ }" : "\"" + t.str["string"] + "\"") << ", " << (t.bln["normalPolishNotation"] ? "DlFormulaStyle::PolishStandard" : t.bln["unicodeInfixNotation"] ? "DlFormulaStyle::InfixUnicode" : "DlFormulaStyle::PolishNumeric") << ", " << bstr(t.bln["conclusionsOnly"]) << ", " << bstr(t.bln["summaryMode"]) << ", " << (unsigned) t.num["minUseAmountToCreateHelperProof"] << ", " << bstr(t.bln["abstractProofStrings"]) << ", " << (t.bln["useInputFile"] ? "\"" + t.str["string"] + "\"" : "null") << ", " << (t.bln["useOutputFile"] ? "\"" + t.str["outputFile"] + "\"" : "null") << ", " << bstr(t.bln["debug"]) << ")\n"; break; case Task::TransformProofSummary: // --transform - ss << ++index << ". recombineProofSummary(\"" << t.str["string"] << "\", " << bstr(t.bln["useInputFile"]) << ", " << (t.bln["whether -s was called"] ? "\"" + t.str["conclusionsWithHelperProofs"] + "\"" : "null") << ", " << (unsigned) t.num["minUseAmountToCreateHelperProof"] << ", " << (size_t) t.num["maxLengthToKeepProof"] << ", " << bstr(t.bln["normalPolishNotation"]) << ", " << (t.bln["whether -t was called"] ? "\"" + t.str["filterForTheorems"] + "\"" : "null") << ", " << bstr(t.bln["abstractProofStrings"]) << ", " << (size_t) t.num["storeIntermediateUnfoldingLimit"] << ", " << (size_t) t.num["maxLengthToComputeDProof"] << ", " << (t.bln["useOutputFile"] ? "\"" + t.str["outputFile"] + "\"" : "null") << ", " << bstr(t.bln["debug"]) << ")\n"; + ss << ++index << ". recombineProofSummary(\"" << t.str["string"] << "\", " << bstr(t.bln["useInputFile"]) << ", " << (t.bln["whether -s was called"] ? "\"" + t.str["conclusionsWithHelperProofs"] + "\"" : "null") << ", " << (unsigned) t.num["minUseAmountToCreateHelperProof"] << ", " << (size_t) t.num["maxLengthToKeepProof"] << ", " << bstr(t.bln["normalPolishNotation"]) << ", " << bstr(t.bln["printInfixUnicode"]) << ", " << (t.bln["whether -t was called"] ? "\"" + t.str["filterForTheorems"] + "\"" : "null") << ", " << bstr(t.bln["abstractProofStrings"]) << ", " << (size_t) t.num["storeIntermediateUnfoldingLimit"] << ", " << (size_t) t.num["maxLengthToComputeDProof"] << ", " << (t.bln["useOutputFile"] ? "\"" + t.str["outputFile"] + "\"" : "null") << ", " << bstr(t.bln["debug"]) << ")\n"; break; case Task::UnfoldProofSummary: // --unfold ss << ++index << ". unfoldProofSummary(\"" << t.str["string"] << "\", " << bstr(t.bln["useInputFile"]) << ", " << bstr(t.bln["normalPolishNotation"]) << ", " << (t.bln["whether -t was called"] ? "\"" + t.str["filterForTheorems"] + "\"" : "null") << ", " << (size_t) t.num["storeIntermediateUnfoldingLimit"] << ", " << (size_t) t.num["maxLengthToComputeDProof"] << ", " << bstr(t.bln["wrap"]) << ", " << (t.bln["useOutputFile"] ? "\"" + t.str["outputFile"] + "\"" : "null") << ", " << bstr(t.bln["debug"]) << ")\n"; @@ -969,11 +973,11 @@ int main(int argc, char* argv[]) { // argc = 1 + N, argv = { , , cout << "[Main] Calling printProofs(" << (t.bln["useInputFile"] ? "{ }" : "\"" + t.str["string"] + "\"") << ", " << (t.bln["normalPolishNotation"] ? "DlFormulaStyle::PolishStandard" : t.bln["unicodeInfixNotation"] ? "DlFormulaStyle::InfixUnicode" : "DlFormulaStyle::PolishNumeric") << ", " << bstr(t.bln["conclusionsOnly"]) << ", " << bstr(t.bln["summaryMode"]) << ", " << (unsigned) t.num["minUseAmountToCreateHelperProof"] << ", " << bstr(t.bln["abstractProofStrings"]) << ", " << (t.bln["useInputFile"] ? "\"" + t.str["string"] + "\"" : "null") << ", " << (t.bln["useOutputFile"] ? "\"" + t.str["outputFile"] + "\"" : "null") << ", " << bstr(t.bln["debug"]) << ")." << endl; DlProofEnumerator::printProofs(t.bln["useInputFile"] ? vector { } : FctHelper::stringSplit(t.str["string"], ","), t.bln["normalPolishNotation"] ? DlFormulaStyle::PolishStandard : t.bln["unicodeInfixNotation"] ? DlFormulaStyle::InfixUnicode : DlFormulaStyle::PolishNumeric, t.bln["conclusionsOnly"], t.bln["summaryMode"], (unsigned) t.num["minUseAmountToCreateHelperProof"], t.bln["abstractProofStrings"], t.bln["useInputFile"] ? &t.str["string"] : nullptr, t.bln["useOutputFile"] ? &t.str["outputFile"] : nullptr, t.bln["debug"]); break; - case Task::TransformProofSummary: // --transform [-s ] [-j ] [-p ] [-n] [-t ] [-e] [-i ] [-l ] [-f] [-o ] [-d] - cout << "[Main] Calling recombineProofSummary(\"" << t.str["string"] << "\", " << bstr(t.bln["useInputFile"]) << ", " << (t.bln["whether -s was called"] ? "\"" + t.str["conclusionsWithHelperProofs"] + "\"" : "null") << ", " << (unsigned) t.num["minUseAmountToCreateHelperProof"] << ", " << (size_t) t.num["maxLengthToKeepProof"] << ", " << bstr(t.bln["normalPolishNotation"]) << ", " << (t.bln["whether -t was called"] ? "\"" + t.str["filterForTheorems"] + "\"" : "null") << ", " << bstr(t.bln["abstractProofStrings"]) << ", " << (size_t) t.num["storeIntermediateUnfoldingLimit"] << ", " << (size_t) t.num["maxLengthToComputeDProof"] << ", " << (t.bln["useOutputFile"] ? "\"" + t.str["outputFile"] + "\"" : "null") << ", " << bstr(t.bln["debug"]) << ")." << endl; + case Task::TransformProofSummary: // --transform [-s ] [-j ] [-p ] [-n] [-u] [-t ] [-e] [-i ] [-l ] [-f] [-o ] [-d] + cout << "[Main] Calling recombineProofSummary(\"" << t.str["string"] << "\", " << bstr(t.bln["useInputFile"]) << ", " << (t.bln["whether -s was called"] ? "\"" + t.str["conclusionsWithHelperProofs"] + "\"" : "null") << ", " << (unsigned) t.num["minUseAmountToCreateHelperProof"] << ", " << (size_t) t.num["maxLengthToKeepProof"] << ", " << bstr(t.bln["normalPolishNotation"]) << ", " << bstr(t.bln["printInfixUnicode"]) << ", " << (t.bln["whether -t was called"] ? "\"" + t.str["filterForTheorems"] + "\"" : "null") << ", " << bstr(t.bln["abstractProofStrings"]) << ", " << (size_t) t.num["storeIntermediateUnfoldingLimit"] << ", " << (size_t) t.num["maxLengthToComputeDProof"] << ", " << (t.bln["useOutputFile"] ? "\"" + t.str["outputFile"] + "\"" : "null") << ", " << bstr(t.bln["debug"]) << ")." << endl; if (!t.bln["useInputFile"]) boost::replace_all(t.str["string"], ",", "\n"); - DlProofEnumerator::recombineProofSummary(t.str["string"], t.bln["useInputFile"], t.bln["whether -s was called"] ? &t.str["conclusionsWithHelperProofs"] : nullptr, (unsigned) t.num["minUseAmountToCreateHelperProof"], t.num["maxLengthToKeepProof"], t.bln["normalPolishNotation"], t.bln["whether -t was called"] ? &t.str["filterForTheorems"] : nullptr, t.bln["abstractProofStrings"], t.num["storeIntermediateUnfoldingLimit"], t.num["maxLengthToComputeDProof"], t.bln["useOutputFile"] ? &t.str["outputFile"] : nullptr, t.bln["debug"]); + DlProofEnumerator::recombineProofSummary(t.str["string"], t.bln["useInputFile"], t.bln["whether -s was called"] ? &t.str["conclusionsWithHelperProofs"] : nullptr, (unsigned) t.num["minUseAmountToCreateHelperProof"], t.num["maxLengthToKeepProof"], t.bln["normalPolishNotation"], t.bln["printInfixUnicode"], t.bln["whether -t was called"] ? &t.str["filterForTheorems"] : nullptr, t.bln["abstractProofStrings"], t.num["storeIntermediateUnfoldingLimit"], t.num["maxLengthToComputeDProof"], t.bln["useOutputFile"] ? &t.str["outputFile"] : nullptr, t.bln["debug"]); break; case Task::UnfoldProofSummary: // --unfold [-n] [-t ] [-i ] [-l ] [-w] [-f] [-o ] [-d] cout << "[Main] Calling unfoldProofSummary(\"" << t.str["string"] << "\", " << bstr(t.bln["useInputFile"]) << ", " << bstr(t.bln["normalPolishNotation"]) << ", " << (t.bln["whether -t was called"] ? "\"" + t.str["filterForTheorems"] + "\"" : "null") << ", " << (size_t) t.num["storeIntermediateUnfoldingLimit"] << ", " << (size_t) t.num["maxLengthToComputeDProof"] << ", " << bstr(t.bln["wrap"]) << ", " << (t.bln["useOutputFile"] ? "\"" + t.str["outputFile"] + "\"" : "null") << ", " << bstr(t.bln["debug"]) << ")." << endl;