diff options
| author | Andrew Zonenberg <azonenberg@drawersteak.com> | 2017-01-05 06:05:58 -0800 |
|---|---|---|
| committer | Andrew Zonenberg <azonenberg@drawersteak.com> | 2017-01-05 06:05:58 -0800 |
| commit | ac90de73becaeac034b226def9c387645698c363 (patch) | |
| tree | c1ceac5fd4994ab583eb0221ec4518b1000e5f91 /backends | |
| parent | babd8dc5b1790533f4f6674724524223c7ae48f4 (diff) | |
| parent | 2d32c6c4f61052254df32bc7942e4339dd59acaa (diff) | |
| download | yosys-ac90de73becaeac034b226def9c387645698c363.tar.gz yosys-ac90de73becaeac034b226def9c387645698c363.tar.bz2 yosys-ac90de73becaeac034b226def9c387645698c363.zip | |
Merge https://github.com/cliffordwolf/yosys
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smtbmc.py | 12 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 9 |
2 files changed, 10 insertions, 11 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index dc89b795d..8dbb047aa 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -201,10 +201,9 @@ for fn in inconstr: current_states = set(["final-%d" % i for i in range(0, num_steps+1)]) constr_final_start = 0 elif len(tokens) == 2: - i = int(tokens[1]) - assert i < 0 - current_states = set(["final-%d" % i for i in range(-i, num_steps+1)]) - constr_final_start = -i if constr_final_start is None else min(constr_final_start, -i) + arg = abs(int(tokens[1])) + current_states = set(["final-%d" % i for i in range(arg, num_steps+1)]) + constr_final_start = arg if constr_final_start is None else min(constr_final_start, arg) else: assert False continue @@ -232,9 +231,8 @@ for fn in inconstr: if len(tokens) == 1: current_states = set(range(0, num_steps+1)) elif len(tokens) == 2: - i = int(tokens[1]) - assert i < 0 - current_states = set(range(-i, num_steps+1)) + arg = abs(int(tokens[1])) + current_states = set(range(arg, num_steps+1)) else: assert False continue diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 10a134711..497b72db8 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -16,7 +16,7 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import sys, subprocess, re +import sys, subprocess, re, os from copy import deepcopy from select import select from time import time @@ -73,7 +73,7 @@ class SmtIo: self.debug_print = False self.debug_file = None self.dummy_file = None - self.timeinfo = True + self.timeinfo = os.name != "nt" self.unroll = False self.noincr = False self.info_stmts = list() @@ -618,7 +618,7 @@ class SmtOpts: self.dummy_file = None self.unroll = False self.noincr = False - self.timeinfo = True + self.timeinfo = os.name != "nt" self.logic = None self.info_stmts = list() self.nocomments = False @@ -633,7 +633,7 @@ class SmtOpts: elif o == "--noincr": self.noincr = True elif o == "--noprogress": - self.timeinfo = True + self.timeinfo = False elif o == "--dump-smt2": self.debug_file = open(a, "w") elif o == "--logic": @@ -673,6 +673,7 @@ class SmtOpts: --noprogress disable timer display during solving + (this option is set implicitly on Windows) --dump-smt2 <filename> write smt2 statements to file |