diff options
| author | N. Engelhardt <nak@symbioticeda.com> | 2020-03-16 12:23:14 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-16 12:23:14 +0100 |
| commit | a2e340de435a6cfeeeb18dc23236cc550be8ca1a (patch) | |
| tree | 97b54427f3c40ce54cc8a7582880d07688ae77af /backends/smt2/smtbmc.py | |
| parent | 685392fed88db3df3dbc077f3d52fb0b4ae36c45 (diff) | |
| parent | 0fda8308bccf6f97b31b104ea1e2b000e4b8c7c7 (diff) | |
| download | yosys-a2e340de435a6cfeeeb18dc23236cc550be8ca1a.tar.gz yosys-a2e340de435a6cfeeeb18dc23236cc550be8ca1a.tar.bz2 yosys-a2e340de435a6cfeeeb18dc23236cc550be8ca1a.zip | |
Merge pull request #1746 from boqwxp/optimization
Add support for optimizing exists-forall problems.
Diffstat (limited to 'backends/smt2/smtbmc.py')
| -rw-r--r-- | backends/smt2/smtbmc.py | 14 |
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 |