From 9465b2af95a146f514fc1e0b2d31bc3d9a233fb7 Mon Sep 17 00:00:00 2001
From: KrystalDelusion <krystinedawn@yosyshq.com>
Date: Wed, 24 Aug 2022 10:28:27 +1200
Subject: Fitting help messages to 80 character width

Uses the regex below to search (using vscode):
	^\t\tlog\("(.{10,}(?<!\\n)|.{81,}\\n)"\);

Finds any log messages double indented (which help messages are)
and checks if *either* there are is no newline character at the end,
*or* the number of characters before the newline is more than 80.
---
 passes/sat/qbfsat.cc | 45 ++++++++++++++++++++++++---------------------
 passes/sat/sim.cc    |  7 ++++---
 2 files changed, 28 insertions(+), 24 deletions(-)

(limited to 'passes/sat')

diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index 1302b3383..4580f194e 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -508,11 +508,11 @@ struct QbfSatPass : public Pass {
 		log("\n");
 		log("    qbfsat [options] [selection]\n");
 		log("\n");
-		log("This command solves an \"exists-forall\" 2QBF-SAT problem defined over the currently\n");
-		log("selected module. Existentially-quantified variables are declared by assigning a wire\n");
-		log("\"$anyconst\". Universally-quantified variables may be explicitly declared by assigning\n");
-		log("a wire \"$allconst\", but module inputs will be treated as universally-quantified\n");
-		log("variables by default.\n");
+		log("This command solves an \"exists-forall\" 2QBF-SAT problem defined over the\n");
+		log("currently selected module. Existentially-quantified variables are declared by\n");
+		log("assigning a wire \"$anyconst\". Universally-quantified variables may be\n");
+		log("explicitly declared by assigning a wire \"$allconst\", but module inputs will be\n");
+		log("treated as universally-quantified variables by default.\n");
 		log("\n");
 		log("    -nocleanup\n");
 		log("        Do not delete temporary files and directories. Useful for debugging.\n");
@@ -521,23 +521,25 @@ struct QbfSatPass : public Pass {
 		log("        Pass the --dump-smt2 option to yosys-smtbmc.\n");
 		log("\n");
 		log("    -assume-outputs\n");
-		log("        Add an \"$assume\" cell for the conjunction of all one-bit module output wires.\n");
+		log("        Add an \"$assume\" cell for the conjunction of all one-bit module output\n");
+		log("        wires.\n");
 		log("\n");
 		log("    -assume-negative-polarity\n");
-		log("        When adding $assume cells for one-bit module output wires, assume they are\n");
-		log("        negative polarity signals and should always be low, for example like the\n");
-		log("        miters created with the `miter` command.\n");
+		log("        When adding $assume cells for one-bit module output wires, assume they\n");
+		log("        are negative polarity signals and should always be low, for example like\n");
+		log("        the miters created with the `miter` command.\n");
 		log("\n");
 		log("    -nooptimize\n");
-		log("        Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n");
-		log("        \"(minimize)\" in the SMT-LIBv2, and generally make no attempt to optimize anything.\n");
+		log("        Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit\n");
+		log("        \"(maximize)\" or \"(minimize)\" in the SMT-LIBv2, and generally make no\n");
+		log("        attempt to optimize anything.\n");
 		log("\n");
 		log("    -nobisection\n");
-		log("        If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n");
-		log("        attempt to optimize that value with the default iterated solving and threshold\n");
-		log("        bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n");
-		log("        command in the SMT-LIBv2 output and hope that the solver supports optimizing\n");
-		log("        quantified bitvector problems.\n");
+		log("        If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute,\n");
+		log("        do not attempt to optimize that value with the default iterated solving\n");
+		log("        and threshold bisection approach. Instead, have yosys-smtbmc emit a\n");
+		log("        \"(minimize)\" or \"(maximize)\" command in the SMT-LIBv2 output and\n");
+		log("        hope that the solver supports optimizing quantified bitvector problems.\n");
 		log("\n");
 		log("    -solver <solver>\n");
 		log("        Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n");
@@ -567,13 +569,14 @@ struct QbfSatPass : public Pass {
 		log("        corresponding constant value from the model produced by the solver.\n");
 		log("\n");
 		log("    -specialize-from-file <solution file>\n");
-		log("        Do not run the solver, but instead only attempt to replace each \"$anyconst\"\n");
-		log("        cell in the current module with a constant value provided by the specified file.\n");
+		log("        Do not run the solver, but instead only attempt to replace each\n");
+		log("        \"$anyconst\" cell in the current module with a constant value provided\n");
+		log("        by the specified file.\n");
 		log("\n");
 		log("    -write-solution <solution file>\n");
-		log("        If the problem is satisfiable, write the corresponding constant value for each\n");
-		log("        \"$anyconst\" cell from the model produced by the solver to the specified file.");
-		log("\n");
+		log("        If the problem is satisfiable, write the corresponding constant value\n");
+		log("        for each \"$anyconst\" cell from the model produced by the solver to the\n");
+		log("        specified file.\n");
 		log("\n");
 	}
 
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 18a25a097..b68783f20 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -2013,7 +2013,8 @@ struct SimPass : public Pass {
 		log("        writeback mode: use final simulation state as new init state\n");
 		log("\n");
 		log("    -r\n");
-		log("        read simulation results file (file formats supported: FST, VCD, AIW and WIT)\n");
+		log("        read simulation results file\n");
+		log("            File formats supported: FST, VCD, AIW and WIT\n");
 		log("		 VCD support requires vcd2fst external tool to be present\n");
 		log("\n");
 		log("    -map <filename>\n");
@@ -2248,8 +2249,8 @@ struct Fst2TbPass : public Pass {
 		log("\n");
 		log("    fst2tb [options] [top-level]\n");
 		log("\n");
-		log("This command generates testbench for the circuit using the given top-level module\n");
-		log("and simulus signal from FST file\n");
+		log("This command generates testbench for the circuit using the given top-level\n");
+		log("module and simulus signal from FST file\n");
 		log("\n");
 		log("    -tb <name>\n");
 		log("        generated testbench name.\n");
-- 
cgit v1.2.3