Jannis Harder a52088b6af smtbmc: Improvements for --incremental and .yw fixes ...

This extends the experimental incremental JSON API to allow arbitrary
smtlib subexpressions, defining smtlib constants and to allow access of
signals by their .yw path.

It also fixes a bug during .yw writing where values would be re-emitted
in later cycles if they have no newer defined value and a potential
crash when using --track-assumes.

2024-05-07 17:57:37 +02:00

..

.gitignore

Various fixes and improvements in "write_smt2 -bv"

2014-12-25 20:28:34 +01:00

example.v

Added smtbmc.py

2015-10-13 17:17:23 +02:00

example.ys

Added smtbmc.py

2015-10-13 17:17:23 +02:00

Makefile.inc

smtbmc: Add native json based witness format + smt2 backend support

2022-08-16 13:37:30 +02:00

smt2.cc

rename -witness: Bug fix and rename formal cells

2024-03-04 16:53:03 +01:00

smtbmc_incremental.py

smtbmc: Improvements for --incremental and .yw fixes

2024-05-07 17:57:37 +02:00

smtbmc.py

smtbmc: Improvements for --incremental and .yw fixes

2024-05-07 17:57:37 +02:00

smtio.py

smtbmc: Improvements for --incremental and .yw fixes

2024-05-07 17:57:37 +02:00

test_cells.sh

tests: use /usr/bin/env for bash.

2023-08-12 11:59:39 +10:00

witness.py

yosys-witness: Add aiw2yw --present-only to omit unused signals

2023-12-14 16:45:19 +01:00

ywio.py

smtbmc: Add --incremental mode

2023-11-16 13:22:17 +01:00