-g: set default candidate queue capacity to 50 (for each worker thread)

Author: xamidi

README.html

@@ -426,10 +426,10 @@ <h4 id="usage">Usage</h4>
        -d: default system ; ignore all other arguments except '-e'
 
 Composable:
-  -g &lt;limit or -1&gt; [-u] [-q &lt;limit&gt;] [-l &lt;limit or -1&gt;] [-k &lt;limit or -1&gt;] [-b] [-v] [-s]
+  -g &lt;limit or -1&gt; [-u] [-q &lt;limit or -1&gt;] [-l &lt;limit or -1&gt;] [-k &lt;limit or -1&gt;] [-b] [-v] [-s]
      Generate proof files ; at ./data/[&lt;hash&gt;/]/dProofs-withConclusions/ when '-s' unspecified ; otherwise at ./data/[&lt;hash&gt;/]/dProofs-withoutConclusions/
        -u: unfiltered (significantly faster, but generates redundant proofs)
-       -q: limit number of proof candidate strings queued per worker thread (may lower memory requirements for systems with low acceptance rates)
+       -q: limit number of proof candidate strings queued per worker thread (may lower memory requirements for systems with low acceptance rates) ; default: 50
        -l: limit symbolic length of generated conclusions to at most the given number ; works only in extracted environments ; recommended to use in combination with '-q' to save memory
        -k: similar to '-l' ; limit symbolic length of consequents in generated conclusions, i.e. antecedents in conditionals are not limited (but non-conditionals are limited in full length)
        -b: brief parsing ; refer to conclusion strings for D-proof processing and use them for rule evaluation (collects faster, but requires more memory) ; used only when '-v' unspecified

README.md

@@ -51,10 +51,10 @@ Some more – and very special – proof systems are illustrated [further down b
            -d: default system ; ignore all other arguments except '-e'
 
     Composable:
-      -g <limit or -1> [-u] [-q <limit>] [-l <limit or -1>] [-k <limit or -1>] [-b] [-v] [-s]
+      -g <limit or -1> [-u] [-q <limit or -1>] [-l <limit or -1>] [-k <limit or -1>] [-b] [-v] [-s]
          Generate proof files ; at ./data/[<hash>/]/dProofs-withConclusions/ when '-s' unspecified ; otherwise at ./data/[<hash>/]/dProofs-withoutConclusions/
            -u: unfiltered (significantly faster, but generates redundant proofs)
-           -q: limit number of proof candidate strings queued per worker thread (may lower memory requirements for systems with low acceptance rates)
+           -q: limit number of proof candidate strings queued per worker thread (may lower memory requirements for systems with low acceptance rates) ; default: 50
            -l: limit symbolic length of generated conclusions to at most the given number ; works only in extracted environments ; recommended to use in combination with '-q' to save memory
            -k: similar to '-l' ; limit symbolic length of consequents in generated conclusions, i.e. antecedents in conditionals are not limited (but non-conditionals are limited in full length)
            -b: brief parsing ; refer to conclusion strings for D-proof processing and use them for rule evaluation (collects faster, but requires more memory) ; used only when '-v' unspecified

logic/DlProofEnumerator.cpp

@@ -1631,6 +1631,12 @@ void DlProofEnumerator::generateDProofRepresentativeFiles(uint32_t limit, bool r
 	chrono::time_point<chrono::steady_clock> startTime;
 	if (useConclusionStrings || useConclusionTrees)
 		withConclusions = true; // need conclusions in these modes
+	size_t defaultQC = 50;
+	if (candidateQueueCapacities) {
+		if (*candidateQueueCapacities == SIZE_MAX)
+			candidateQueueCapacities = nullptr;
+	} else
+		candidateQueueCapacities = &defaultQC;
 
 	// 1. Load representative D-proof strings.
 	auto myInfo = [&]() -> string {

main.cpp

@@ -63,10 +63,10 @@ static const map<Task, string>& cmdInfo() {
 				"         -e: specify extracted system with the given identifier\n"
 				"         -d: default system ; ignore all other arguments except '-e'\n";
 		_[Task::Generate] =
-				"    -g <limit or -1> [-u] [-q <limit>] [-l <limit or -1>] [-k <limit or -1>] [-b] [-v] [-s]\n"
+				"    -g <limit or -1> [-u] [-q <limit or -1>] [-l <limit or -1>] [-k <limit or -1>] [-b] [-v] [-s]\n"
 				"       Generate proof files ; at ./data/[<hash>/]/dProofs-withConclusions/ when '-s' unspecified ; otherwise at ./data/[<hash>/]/dProofs-withoutConclusions/\n"
 				"         -u: unfiltered (significantly faster, but generates redundant proofs)\n"
-				"         -q: limit number of proof candidate strings queued per worker thread (may lower memory requirements for systems with low acceptance rates)\n"
+				"         -q: limit number of proof candidate strings queued per worker thread (may lower memory requirements for systems with low acceptance rates) ; default: 50\n"
 				"         -l: limit symbolic length of generated conclusions to at most the given number ; works only in extracted environments ; recommended to use in combination with '-q' to save memory\n"
 				"         -k: similar to '-l' ; limit symbolic length of consequents in generated conclusions, i.e. antecedents in conditionals are not limited (but non-conditionals are limited in full length)\n"
 				"         -b: brief parsing ; refer to conclusion strings for D-proof processing and use them for rule evaluation (collects faster, but requires more memory) ; used only when '-v' unspecified\n"