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.

1 files changed, 14 insertions, 0 deletions

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