aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat/qbfsat.cc
Commit message (Expand)AuthorAgeFilesLines
* qbfsat: Add support for CVC4.Alberto Gonzalez2020-05-251-2/+6
* qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices th...Alberto Gonzalez2020-05-251-20/+47
* qbfsat: Remove cruft inadvertently left untouched in commit 86fc49a9d60f9ad4c...Alberto Gonzalez2020-05-231-11/+0
* qbfsat: Add bisection mode and make it the default.Alberto Gonzalez2020-05-231-87/+207
* Merge pull request #1989 from boqwxp/qbfsat_anyconst_sourcelocsClaire Wolf2020-04-231-5/+2
|\
| * qbfsat: Make hole name recovery more robust. Allow multiple cell types to sha...Alberto Gonzalez2020-04-231-5/+2
* | qbfsat: Add `-assume-negative-polarity` option.Alberto Gonzalez2020-04-231-6/+22
|/
* qbfsat: Fix illegal use of 'stdout' identifierDavid Shah2020-04-171-3/+3
* Use `pool` instead of `std::set`.Alberto Gonzalez2020-04-111-6/+6
* Use `dict` instead of `std::map`.Alberto Gonzalez2020-04-111-8/+8
* Clean up `passes/sat/qbfsat.cc`.Alberto Gonzalez2020-04-091-13/+10
* Remove `$anyconst` cells before specialization to eliminate warnings and the ...Alberto Gonzalez2020-04-071-2/+25
* Use newly-renamed `-push-copy` option.Alberto Gonzalez2020-04-041-1/+1
* Improve style in `passes/sat/qbfsat.cc`.Alberto Gonzalez2020-04-041-4/+2
* Gracefully report error when module has nothing to prove.Alberto Gonzalez2020-04-041-5/+8
* Suppress `yosys-smtbmc` output unless the new `-show-smtbmc` option is provided.Alberto Gonzalez2020-04-041-5/+14
* Fix handling of `-sat` and `-unsat` options when the solver returns `unknown`.Alberto Gonzalez2020-04-041-0/+2
* Use `log_push()` and `log_pop()` and show the satisfiable model when `-specia...Alberto Gonzalez2020-04-041-0/+28
* Clean up `qbfsat` command and fix AND-reduction of miter outputs.Alberto Gonzalez2020-04-041-8/+10
* Use the `-duplicate` option rather than `-save` and `-load` with an explicit ...Alberto Gonzalez2020-04-041-2/+2
* Use internal `run_command()` API instead of `popen()`.Alberto Gonzalez2020-04-041-49/+15
* Clean up manual casting.Alberto Gonzalez2020-04-041-2/+2
* Remove unimplemented `-timeout` option.Alberto Gonzalez2020-04-041-16/+4
* Implement the `-assume-outputs`, `-sat`, and -unsat` options for the `qbfsat`...Alberto Gonzalez2020-04-041-3/+66
* Add NDEBUG guards to `qbfsat` assertions.Alberto Gonzalez2020-04-041-0/+18
* Implement `-specialize-from-file` option for the `qbfsat` command.Alberto Gonzalez2020-04-041-23/+56
* Implement `-write-solution` option for the `qbfsat` command.Alberto Gonzalez2020-04-041-7/+28
* Clean up `passes/sat/qbfsat.cc`.Alberto Gonzalez2020-04-041-86/+101
* Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole val...Alberto Gonzalez2020-04-041-29/+39
* Hole value recovery and specialization implementation for `qbfsat` command.Alberto Gonzalez2020-04-041-20/+63
* Barebones implementation of `qbfsat` command.Alberto Gonzalez2020-04-041-32/+157
* Initial skeleton for `qbfsat` command.Alberto Gonzalez2020-04-041-0/+206