diff options
Diffstat (limited to 'passes/sat/qbfsat.cc')
| -rw-r--r-- | passes/sat/qbfsat.cc | 45 |
1 files changed, 24 insertions, 21 deletions
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"); } |