Jannis Harder
0c5f62f6ff
smtbmc: noincr: keep solver running for post check-sat unrolling
2022-06-08 13:20:25 +02:00
Jannis Harder
6db2948938
Merge pull request #3357 from jix/smtbmc-cvc5
...
smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
2022-06-08 12:52:51 +02:00
Jannis Harder
ab9e887dee
smtbmc: Force nonincremental mode when yices is used with forall
2022-06-03 16:45:23 +02:00
Jannis Harder
0207d7b0cf
smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
2022-06-03 16:24:09 +02:00
Jannis Harder
d25daa6203
smtbmc: Avoid unnecessary deep copies during unrolling
2022-03-28 13:03:48 +02:00
N. Engelhardt
dc739362c7
print cell name for properties in yosys-smtbmc
2022-02-22 17:00:10 +01:00
GCHQDeveloper560
4379375d89
Add support for the Bitwuzla solver
2021-07-12 22:07:58 +02:00
Claire Xenia Wolf
72787f52fc
Fixing old e-mail addresses and deadnames
...
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g ;
2021-06-08 00:39:36 +02:00
Alberto Gonzalez
42fb75c570
smtio: Emit `mode: start` options before `set-logic` command and any other options after it.
...
Refer to the SMT-LIB specification, section 4.1.7. According to the spec, some options can only be specified in `start` mode. Once the solver sees `set-logic`, it moves to `assert` mode.
2020-07-20 22:09:44 +00:00
Alberto Gonzalez
654864658f
smtio: Add support for parsing `yosys-smt2-solver-option` info statements.
2020-07-20 21:54:56 +00:00
Claire Wolf
a207cb362c
Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-20 19:35:32 +02:00
Yehowshua Immanuel
da0778350b
more reasonable numbers for memory
2020-06-04 17:00:04 -04:00
Yehowshua Immanuel
5d29a9f633
MacOS has even stricter stack limits in catalina.
...
Invoking sby in macOS Catalina fails because of bizarre stack limits in Catalina.
2020-06-04 14:01:56 -04:00
Alberto Gonzalez
ea30465107
smtbmc: Remove superfluous `yosys-smt2-timeout` file macro.
...
Co-Authored-By: clairexen <claire@symbioticeda.com>
2020-05-29 21:33:00 +00:00
Alberto Gonzalez
9847a4eea8
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.
2020-05-25 20:39:30 +00:00
Alberto Gonzalez
54570a3978
qbfsat: Move SMT2 info statements back to the top of the file.
2020-05-25 20:38:29 +00:00
Alberto Gonzalez
903456c267
qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.
...
Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode.
2020-05-25 20:38:29 +00:00
Alberto Gonzalez
d72cb8ea2a
Do not change solver output parsing for non-exists-forall problems.
2020-03-26 23:00:00 +00:00
Alberto Gonzalez
5accf08ef9
Skip reading stdout from the solver that if it isn't a line reading only "sat", "unsat", or "unknown".
2020-03-26 01:21:01 +00:00
Claire Wolf
c9555c9ade
Revert part of 0fda8308
from #1746 that broke other smtbmc flows
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-24 17:33:46 +01:00
Alberto Gonzalez
0fda8308bc
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.
2020-03-13 17:10:29 +00:00
Claire Wolf
485f31f681
Improve yosys-smtbmc "solver not found" handling
...
Signed-off-by: Claire Wolf <clifford@clifford.at>
2020-01-27 17:48:56 +01:00
Clifford Wolf
f02623abb5
Bugfix in smtio vcd handling of $-identifiers
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-10-23 00:04:34 +02:00
N. Engelhardt
ab4b9e8db4
smt: handle failure of setrlimit syscall
2019-07-15 23:33:18 +08:00
Clifford Wolf
b3c36b4448
Escape scope names starting with dollar sign in smtio.py
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-26 10:58:39 +02:00
Clifford Wolf
c23bbc4291
Add timescale and generated-by header to yosys-smtbmc MkVcd
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-16 23:12:03 +02:00
Clifford Wolf
e112d2fbf5
Add missing blackslash-to-slash convertion to smtio.py (matching Smt2Worker::get_id() behavior)
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-06 16:35:59 +01:00
Clifford Wolf
825b4c1aa9
Merge pull request #693 from YosysHQ/rlimit
...
improve rlimit handling in smtio.py
2018-11-07 20:16:40 +01:00
Clifford Wolf
b54bf7c0f9
Limit stack size to 16 MB on Darwin
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-07 15:32:34 +01:00
Clifford Wolf
f6c4485a3a
Run solver in non-incremental mode whem smtio.py is configured for non-incremental solving
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-06 11:11:05 +01:00
Clifford Wolf
4c50e3abb9
Fix for improved smtio.py rlimit code
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-06 10:09:03 +01:00
Clifford Wolf
79075d123f
Improve stack rlimit code in smtio.py
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-06 10:05:23 +01:00
Arjen Roodselaar
2b93542171
Use conservative stack size for SMT2 on MacOS
2018-11-04 21:58:09 -08:00
William D. Jones
0caa62802c
Gate POSIX-only signals and resource module to only run on POSIX Python implementations.
2018-07-06 01:44:34 -04:00
Clifford Wolf
4d6af2969c
Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-04 18:12:27 +02:00
Clifford Wolf
dd5fab69c1
Add smtio status msgs when --progress is inactive
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 21:59:30 +02:00
Clifford Wolf
a48c7e5abf
Bugfix in smtio.py VCD file generator
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 12:45:31 +02:00
Clifford Wolf
3f00702475
Improve yosys-smtbmc log output and error handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-17 18:06:17 +01:00
Clifford Wolf
4d4e3a8ca6
Improve handling of invalid check-sat result in smtio.py
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-17 12:17:53 +01:00
Clifford Wolf
3545c0fffb
Remove debug prints from yosys-smtbmc VCD writer
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-08 16:24:35 +01:00
Clifford Wolf
8b604004da
Check results of (check-sat) in yosys-smtbmc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-07 22:54:19 +01:00
Clifford Wolf
cedbc35f4b
Imporove yosys-smtbmc error handling, Improve VCD output
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-05 12:17:22 +01:00
Clifford Wolf
45a6fce92c
Fix a hangup in yosys-smtbmc error handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-04 21:13:30 +01:00
Clifford Wolf
ae4e204c76
Improved error handling in yosys-smtbmc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-03 20:00:07 +01:00
Clifford Wolf
a44e1edaa3
Terminate running SMT solver when smtbmc is terminated
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-03 14:50:40 +01:00
Clifford Wolf
90ae426078
Mangle names with square brackets in VCD files to work around issues in gtkwave
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-01 14:15:27 +01:00
Clifford Wolf
b13e6bd375
Add smtbmc support for exist-forall problems
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-23 19:33:30 +01:00
Clifford Wolf
17583b6a21
Add support for mockup clock signals in yosys-smtbmc vcd output
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-20 17:45:22 +01:00
Clifford Wolf
e97f10b142
Fix smtio.py for large SMT2 S-expressions
2018-01-29 12:34:28 +01:00
Clifford Wolf
54aeca0983
Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output
2018-01-18 14:25:22 +01:00