diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-04-30 21:27:18 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-05-25 20:38:29 +0000 |
| commit | 903456c267c84d6d924a96ddf4f2b4e2b5caec4a (patch) | |
| tree | 8c01bc44823e25afb480ab331f7f92dc98da89cd /backends/blif | |
| parent | 59b355fb85cb7cda4a25696850bb3caffce3115f (diff) | |
| download | yosys-903456c267c84d6d924a96ddf4f2b4e2b5caec4a.tar.gz yosys-903456c267c84d6d924a96ddf4f2b4e2b5caec4a.tar.bz2 yosys-903456c267c84d6d924a96ddf4f2b4e2b5caec4a.zip | |
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.
Diffstat (limited to 'backends/blif')
0 files changed, 0 insertions, 0 deletions