Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | qbfsat: Add `-solver-option` option. | Alberto Gonzalez | 2020-07-20 | 1 | -1/+14 |
| | |||||
* | qbfsat: Remove useless comment and #ifndef guards. | Alberto Gonzalez | 2020-07-01 | 1 | -5/+0 |
| | |||||
* | qbfsat: Specify default values for some options in the help message. | Alberto Gonzalez | 2020-07-01 | 1 | -0/+2 |
| | |||||
* | qbfsat: Clean up external executable command lines and update temporary ↵ | Alberto Gonzalez | 2020-07-01 | 1 | -3/+7 |
| | | | | directory name. | ||||
* | qbfsat: Clean up and refactor data structures into `qbfsat.h`. | Alberto Gonzalez | 2020-07-01 | 1 | -248/+13 |
| | |||||
* | Merge pull request #2138 from boqwxp/qbfsat-oflag | clairexen | 2020-07-01 | 1 | -16/+47 |
|\ | | | | | qbfsat: Add `-O[012]` options to control pre-solving simplification with ABC | ||||
| * | qbfsat: Add `-O[012]` options to control pre-solving simplification with ABC. | Alberto Gonzalez | 2020-06-30 | 1 | -16/+47 |
| | | | | | | | | | | | | Thanks to @mwk for the gate mapping part of the ABC scripts. Co-Authored-By: Marcelina Kościelnicka <mwk@0x04.net> | ||||
* | | qbfsat: Fix name-based hole specialization. | Alberto Gonzalez | 2020-06-30 | 1 | -2/+24 |
|/ | | | | Look for unique connections in the containing module with the $anyconst port Y SigBit on the RHS and use those. If no such connection is found, fall back to using the name of the $anyconst port Y SigBit. | ||||
* | log, qbfsat: Include child process time in `PerformanceTimer::query()` and ↵ | Alberto Gonzalez | 2020-06-21 | 1 | -1/+6 |
| | | | | report the time for each call to the QBF-SAT solver. | ||||
* | qbfsat: Simplify solution recovery parsing and tweak the solution regexes. | Alberto Gonzalez | 2020-06-21 | 1 | -22/+12 |
| | |||||
* | qbfsat: Avoid instantiating `AttrObject`s directly. | Alberto Gonzalez | 2020-06-21 | 1 | -9/+6 |
| | | | | Co-Authored-By: Claire Wolf <claire@symbioticeda.com> | ||||
* | qbfsat: Simplify solution format and replace `SigBit::str()` with ↵ | Alberto Gonzalez | 2020-06-21 | 1 | -19/+37 |
| | | | | | | `log_signal()`. Co-Authored-By: Claire Wolf <claire@symbioticeda.com> | ||||
* | qbfsat: Fixes three bugs. | Alberto Gonzalez | 2020-06-21 | 1 | -5/+17 |
| | | | | | | 1. Infinite loop in the optimization procedure when the first solution found while maximizing is at zero. 2. A signed-ness issue when maximizing. 3. Erroneously entering bisection mode with no wire to optimize. | ||||
* | qbfsat: Use bit precise mapping for hole value wires and a more robust hole ↵ | Alberto Gonzalez | 2020-06-21 | 1 | -80/+113 |
| | | | | spec for writing to and specializing from a solution file. | ||||
* | Use C++11 final/override keywords. | whitequark | 2020-06-18 | 1 | -2/+2 |
| | |||||
* | smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, ↵ | Alberto Gonzalez | 2020-05-25 | 1 | -13/+53 |
| | | | | and CVC4. | ||||
* | qbfsat: Add support for CVC4. | Alberto Gonzalez | 2020-05-25 | 1 | -2/+6 |
| | |||||
* | qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices ↵ | Alberto Gonzalez | 2020-05-25 | 1 | -20/+47 |
| | | | | | | 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. | ||||
* | qbfsat: Remove cruft inadvertently left untouched in commit ↵ | Alberto Gonzalez | 2020-05-23 | 1 | -11/+0 |
| | | | | 86fc49a9d60f9ad4cdeec93663e7245a9fdf60c6. | ||||
* | qbfsat: Add bisection mode and make it the default. | Alberto Gonzalez | 2020-05-23 | 1 | -87/+207 |
| | | | | Also adds `-nooptimize` and reorganizes `qbfsat.cc` a bit. | ||||
* | Merge pull request #1989 from boqwxp/qbfsat_anyconst_sourcelocs | Claire Wolf | 2020-04-23 | 1 | -5/+2 |
|\ | | | | | qbfsat: Make hole name recovery from source locations more robust. | ||||
| * | qbfsat: Make hole name recovery more robust. Allow multiple cell types to ↵ | Alberto Gonzalez | 2020-04-23 | 1 | -5/+2 |
| | | | | | | | | share the same source location as long as only one `$anyconst` or `$anyseq` has that location. | ||||
* | | qbfsat: Add `-assume-negative-polarity` option. | Alberto Gonzalez | 2020-04-23 | 1 | -6/+22 |
|/ | |||||
* | qbfsat: Fix illegal use of 'stdout' identifier | David Shah | 2020-04-17 | 1 | -3/+3 |
| | | | | Signed-off-by: David Shah <dave@ds0.me> | ||||
* | Use `pool` instead of `std::set`. | Alberto Gonzalez | 2020-04-11 | 1 | -6/+6 |
| | |||||
* | Use `dict` instead of `std::map`. | Alberto Gonzalez | 2020-04-11 | 1 | -8/+8 |
| | |||||
* | Clean up `passes/sat/qbfsat.cc`. | Alberto Gonzalez | 2020-04-09 | 1 | -13/+10 |
| | | | | Makes various cosmetic fixes, removes superfluous `hasPort()` check, and uses `emplace_back()` instead of `push_back()`. | ||||
* | Remove `$anyconst` cells before specialization to eliminate warnings and the ↵ | Alberto Gonzalez | 2020-04-07 | 1 | -2/+25 |
| | | | | need to run `opt_clean`. | ||||
* | Use newly-renamed `-push-copy` option. | Alberto Gonzalez | 2020-04-04 | 1 | -1/+1 |
| | |||||
* | Improve style in `passes/sat/qbfsat.cc`. | Alberto Gonzalez | 2020-04-04 | 1 | -4/+2 |
| | |||||
* | Gracefully report error when module has nothing to prove. | Alberto Gonzalez | 2020-04-04 | 1 | -5/+8 |
| | |||||
* | Suppress `yosys-smtbmc` output unless the new `-show-smtbmc` option is provided. | Alberto Gonzalez | 2020-04-04 | 1 | -5/+14 |
| | |||||
* | Fix handling of `-sat` and `-unsat` options when the solver returns `unknown`. | Alberto Gonzalez | 2020-04-04 | 1 | -0/+2 |
| | |||||
* | Use `log_push()` and `log_pop()` and show the satisfiable model when ↵ | Alberto Gonzalez | 2020-04-04 | 1 | -0/+28 |
| | | | | | | `-specialize` is not specified. Co-Authored-By: N. Engelhardt <nak@symbioticeda.com> | ||||
* | Clean up `qbfsat` command and fix AND-reduction of miter outputs. | Alberto Gonzalez | 2020-04-04 | 1 | -8/+10 |
| | |||||
* | Use the `-duplicate` option rather than `-save` and `-load` with an explicit ↵ | Alberto Gonzalez | 2020-04-04 | 1 | -2/+2 |
| | | | | | | name. Co-Authored-By: Claire Wolf <claire@symbioticeda.com> | ||||
* | Use internal `run_command()` API instead of `popen()`. | Alberto Gonzalez | 2020-04-04 | 1 | -49/+15 |
| | | | | Co-Authored-By: Claire Wolf <claire@symbioticeda.com> | ||||
* | Clean up manual casting. | Alberto Gonzalez | 2020-04-04 | 1 | -2/+2 |
| | | | | Co-Authored-By: David Shah <dave@ds0.me> | ||||
* | Remove unimplemented `-timeout` option. | Alberto Gonzalez | 2020-04-04 | 1 | -16/+4 |
| | |||||
* | Implement the `-assume-outputs`, `-sat`, and -unsat` options for the ↵ | Alberto Gonzalez | 2020-04-04 | 1 | -3/+66 |
| | | | | `qbfsat` command. | ||||
* | Add NDEBUG guards to `qbfsat` assertions. | Alberto Gonzalez | 2020-04-04 | 1 | -0/+18 |
| | |||||
* | Implement `-specialize-from-file` option for the `qbfsat` command. | Alberto Gonzalez | 2020-04-04 | 1 | -23/+56 |
| | |||||
* | Implement `-write-solution` option for the `qbfsat` command. | Alberto Gonzalez | 2020-04-04 | 1 | -7/+28 |
| | |||||
* | Clean up `passes/sat/qbfsat.cc`. | Alberto Gonzalez | 2020-04-04 | 1 | -86/+101 |
| | |||||
* | Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole ↵ | Alberto Gonzalez | 2020-04-04 | 1 | -29/+39 |
| | | | | value recovery using that mode. | ||||
* | Hole value recovery and specialization implementation for `qbfsat` command. | Alberto Gonzalez | 2020-04-04 | 1 | -20/+63 |
| | |||||
* | Barebones implementation of `qbfsat` command. | Alberto Gonzalez | 2020-04-04 | 1 | -32/+157 |
| | |||||
* | Initial skeleton for `qbfsat` command. | Alberto Gonzalez | 2020-04-04 | 1 | -0/+206 |