diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-03-08 06:34:47 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-03-13 17:10:29 +0000 |
| commit | 0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7 (patch) | |
| tree | 7ebed8b82028a5ddc35771917e16aba5774cf354 /backends/smt2/smtio.py | |
| parent | bfeba9ad11847e6a0cbe47f880f3642d5e3a8061 (diff) | |
| download | yosys-0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7.tar.gz yosys-0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7.tar.bz2 yosys-0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7.zip | |
Add support for optimizing exists-forall problems.
Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate.
Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al.
Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
Diffstat (limited to 'backends/smt2/smtio.py')
| -rw-r--r-- | backends/smt2/smtio.py | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 34bf7ef38..4c691716e 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -101,6 +101,8 @@ class SmtModInfo: self.cells = dict() self.asserts = dict() self.covers = dict() + self.maximize = set() + self.minimize = set() self.anyconsts = dict() self.anyseqs = dict() self.allconsts = dict() @@ -502,6 +504,12 @@ class SmtIo: if fields[1] == "yosys-smt2-cover": self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] + if fields[1] == "yosys-smt2-maximize": + self.modinfo[self.curmod].maximize.add(fields[2]) + + if fields[1] == "yosys-smt2-minimize": + self.modinfo[self.curmod].minimize.add(fields[2]) + if fields[1] == "yosys-smt2-anyconst": self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5]) self.modinfo[self.curmod].asize[fields[2]] = int(fields[3]) @@ -696,7 +704,9 @@ class SmtIo: if msg is not None: print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True) - result = self.read() + result = "" + while result not in ["sat", "unsat"]: + result = self.read() if self.debug_file: print("(set-info :status %s)" % result, file=self.debug_file) |