more in-depth proof iterator explanation + minor improvements

Author: xamidi

__dependency_graph.dot

@@ -9,7 +9,6 @@ digraph {
 		CfgGrammar
 		CfgGrammar
 	}
-	FctHelper -> Resources [color=blue]
 	FctHelper -> iostream [color=blue]
 	FctHelper -> math [color=blue]
 	FctHelper -> algorithm [color=red]
@@ -67,6 +66,7 @@ digraph {
 	main -> cstring [color=blue]
 	main -> ctime [color=blue]
 	main -> iostream [color=blue]
+	main -> unistd [color=blue]
 	subgraph "cluster_D:/Dropbox/eclipse/pmGenerator" {
 		main
 	}

helper/FctHelper.cpp

@@ -1,7 +1,5 @@
 #include "FctHelper.h"
 
-#include "Resources.h"
-
 #include <iostream>
 #include <math.h>
 

main.cpp

@@ -5,6 +5,7 @@
 #include <cstring>
 #include <ctime>
 #include <iostream>
+#include <unistd.h>
 
 using namespace std;
 using namespace xamid::helper;
@@ -14,11 +15,11 @@ using namespace xamid::nortmann;
 struct A {
 	A() {
 		time_t time = chrono::system_clock::to_time_t(chrono::system_clock::now());
-		cout << strtok(ctime(&time), "\n") << ": Process started." << endl;
+		cout << strtok(ctime(&time), "\n") << ": Process started. [pid: " << getpid() << ", tid:" << this_thread::get_id() << "]" << endl;
 	}
 	~A() {
 		time_t time = chrono::system_clock::to_time_t(chrono::system_clock::now());
-		cout << strtok(ctime(&time), "\n") << ": Process terminated." << endl;
+		cout << strtok(ctime(&time), "\n") << ": Process terminated. [pid: " << getpid() << ", tid:" << this_thread::get_id() << "]" << endl;
 	}
 } a;
 

nortmann/DlProofEnumerator.h

@@ -93,6 +93,17 @@ struct DlProofEnumerator {
 	}
 
 private:
+	// The idea, for an odd number n := 'knownLimit', is to implement a pushdown automaton for a context-free grammar
+	// with start symbol S, nonterminals {S, A} \cup {Nx | x > 0 odd, and x <= n}, and production rules
+	// S -> N1 | ... | Nn | A                     (S produces a superset of all representative proofs.)
+	// A -> <production generated by proofLengthCombinations(n)>, e.g. n = 5 => A -> D N1 N5 | D N5 N1 | D N3 N3 | D N3 N5 | D N5 N3 | D N1 A | D A N1 | D N5 N5 | D N3 A | D A N3 | D N5 A | D A N5 | D A A
+	// N1 -> {p | p is representative proof of length 1}
+	// ...
+	// Nn -> {p | p is representative proof of length n}.
+	// This grammar defines a superset of all condensed-detachment proofs on top of the already known proofs of lengths up to n, where A encodes those which have
+	// at least length n + 2. By starting the pushdown automaton with stack [A], only the new candidates are iterated, of which invalid candidates can be skipped
+	// after resulting in a parse error. When providing 'wordLengthLimit' := n + 2, this means to only iterate candidates of length n + 2 in an efficient way.
+	// [NOTE: Sequential non-generic variants (with explicit grammars given as comments) are available at https://github.com/deontic-logic/proof-tool/blob/29dd7dfab9f373d1dd387fb99c16e82c577ec21f/nortmann/DlProofEnumerator.h?ts=4#L167-L174 and below.]
 	static void _loadAndProcessQueuesConcurrently(unsigned concurrencyCount, std::vector<std::deque<std::string>>& queues, std::vector<std::mutex>& mtxs, const auto& loader, const auto& process);
 	static void _processCondensedDetachmentPlProofs_generic_seq(std::string& prefix, std::vector<std::uint32_t>& stack, std::uint32_t wordLengthLimit, std::uint32_t knownLimit, const std::vector<std::vector<std::string>>& allRepresentatives, const auto& fString);
 	static void _processCondensedDetachmentPlProofs_naive_seq(std::string& prefix, unsigned stackSize, std::uint32_t wordLengthLimit, const auto& fString);