diff options
| author | N. Engelhardt <nak@yosyshq.com> | 2023-03-01 09:59:01 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-03-01 09:59:01 +0100 |
| commit | 981c934b5bb8805bba98ae1989a4c8eb3b6e9098 (patch) | |
| tree | 95e5e7c46bb27339f360dfe98113d59c16f03d69 | |
| parent | 25ebefc2a61ac5d8e46487396346bd4b24ababc8 (diff) | |
| parent | 4bb173e25609b836fc83473b544f404f8f76d2ff (diff) | |
| download | yosys-981c934b5bb8805bba98ae1989a4c8eb3b6e9098.tar.gz yosys-981c934b5bb8805bba98ae1989a4c8eb3b6e9098.tar.bz2 yosys-981c934b5bb8805bba98ae1989a4c8eb3b6e9098.zip | |
Merge pull request #3690 from whitequark/smtbmc-help-opt
| -rw-r--r-- | backends/smt2/smtbmc.py | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index cb21eb3aa..6b81740a2 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -59,9 +59,12 @@ detect_loops = False so = SmtOpts() -def usage(): +def help(): print(os.path.basename(sys.argv[0]) + """ [options] <yosys_smt2_output> + -h, --help + show this message + -t <num_steps> -t <skip_steps>:<num_steps> -t <skip_steps>:<step_size>:<num_steps> @@ -181,19 +184,25 @@ def usage(): (this feature is experimental and incomplete) """ + so.helpmsg()) + +def usage(): + help() sys.exit(1) try: - opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + - ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", + opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:higcm:", so.longopts + + ["help", "final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"]) except: usage() for o, a in opts: - if o == "-t": + if o in ("-h", "--help"): + help() + sys.exit(0) + elif o == "-t": got_topt = True a = a.split(":") if len(a) == 1: |