From 0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Sun, 8 Mar 2020 06:34:47 +0000 Subject: Add support for optimizing exists-forall problems. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- backends/smt2/smtbmc.py | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'backends/smt2/smtbmc.py') diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 3d6d3e1b3..630464419 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1158,6 +1158,8 @@ def smt_forall_assert(): global asserts_cache_dirty asserts_cache_dirty = False + assert (len(smt.modinfo[topmod].maximize) + len(smt.modinfo[topmod].minimize) <= 1) + def make_assert_expr(asserts_cache): expr = list() for lst in asserts_cache: @@ -1236,6 +1238,18 @@ def smt_forall_assert(): smt.write("".join(assert_expr)) + if len(smt.modinfo[topmod].maximize) > 0: + for s in states: + if s in used_states_db: + smt.write("(maximize (|%s| %s))\n" % (smt.modinfo[topmod].maximize.copy().pop(), s)) + break + + if len(smt.modinfo[topmod].minimize) > 0: + for s in states: + if s in used_states_db: + smt.write("(minimize (|%s| %s))\n" % (smt.modinfo[topmod].minimize.copy().pop(), s)) + break + def smt_push(): global asserts_cache_dirty asserts_cache_dirty = True -- cgit v1.2.3