aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat/qbfsat.cc
Commit message (Collapse)AuthorAgeFilesLines
* support file locations containing spacesMiodrag Milanovic2022-08-081-1/+1
|
* Observe $TMPDIR variable when creating tmp filesMohamed A. Bamakhrama2022-05-271-1/+1
| | | | | | | | | POSIX defines $TMPDIR as containing the pathname of the directory where programs can create temporary files. On most systems, this variable points to "/tmp". However, on some systems it can point to a different location. Without respecting this variable, yosys fails to run on such systems. Signed-off-by: Mohamed A. Bamakhrama <mohamed@alumni.tum.de>
* qbfsat: Add `-solver-option` option.Alberto Gonzalez2020-07-201-1/+14
|
* qbfsat: Remove useless comment and #ifndef guards.Alberto Gonzalez2020-07-011-5/+0
|
* qbfsat: Specify default values for some options in the help message.Alberto Gonzalez2020-07-011-0/+2
|
* qbfsat: Clean up external executable command lines and update temporary ↵Alberto Gonzalez2020-07-011-3/+7
| | | | directory name.
* qbfsat: Clean up and refactor data structures into `qbfsat.h`.Alberto Gonzalez2020-07-011-248/+13
|
* Merge pull request #2138 from boqwxp/qbfsat-oflagclairexen2020-07-011-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 Gonzalez2020-06-301-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 Gonzalez2020-06-301-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 Gonzalez2020-06-211-1/+6
| | | | report the time for each call to the QBF-SAT solver.
* qbfsat: Simplify solution recovery parsing and tweak the solution regexes.Alberto Gonzalez2020-06-211-22/+12
|
* qbfsat: Avoid instantiating `AttrObject`s directly.Alberto Gonzalez2020-06-211-9/+6
| | | | Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
* qbfsat: Simplify solution format and replace `SigBit::str()` with ↵Alberto Gonzalez2020-06-211-19/+37
| | | | | | `log_signal()`. Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
* qbfsat: Fixes three bugs.Alberto Gonzalez2020-06-211-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 Gonzalez2020-06-211-80/+113
| | | | spec for writing to and specializing from a solution file.
* Use C++11 final/override keywords.whitequark2020-06-181-2/+2
|
* smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, ↵Alberto Gonzalez2020-05-251-13/+53
| | | | and CVC4.
* qbfsat: Add support for CVC4.Alberto Gonzalez2020-05-251-2/+6
|
* qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices ↵Alberto Gonzalez2020-05-251-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 Gonzalez2020-05-231-11/+0
| | | | 86fc49a9d60f9ad4cdeec93663e7245a9fdf60c6.
* qbfsat: Add bisection mode and make it the default.Alberto Gonzalez2020-05-231-87/+207
| | | | Also adds `-nooptimize` and reorganizes `qbfsat.cc` a bit.
* Merge pull request #1989 from boqwxp/qbfsat_anyconst_sourcelocsClaire Wolf2020-04-231-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 Gonzalez2020-04-231-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 Gonzalez2020-04-231-6/+22
|/
* qbfsat: Fix illegal use of 'stdout' identifierDavid Shah2020-04-171-3/+3
| | | | Signed-off-by: David Shah <dave@ds0.me>
* 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
| | | | 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 Gonzalez2020-04-071-2/+25
| | | | need to run `opt_clean`.
* 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 ↵Alberto Gonzalez2020-04-041-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 Gonzalez2020-04-041-8/+10
|
* Use the `-duplicate` option rather than `-save` and `-load` with an explicit ↵Alberto Gonzalez2020-04-041-2/+2
| | | | | | name. Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
* Use internal `run_command()` API instead of `popen()`.Alberto Gonzalez2020-04-041-49/+15
| | | | Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
* Clean up manual casting.Alberto Gonzalez2020-04-041-2/+2
| | | | Co-Authored-By: David Shah <dave@ds0.me>
* Remove unimplemented `-timeout` option.Alberto Gonzalez2020-04-041-16/+4
|
* Implement the `-assume-outputs`, `-sat`, and -unsat` options for the ↵Alberto Gonzalez2020-04-041-3/+66
| | | | `qbfsat` command.
* 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 ↵Alberto Gonzalez2020-04-041-29/+39
| | | | value recovery using that mode.
* 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-22 13:59:11 +0000