diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-04-16 06:10:28 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-16 08:10:28 -0500 |
| commit | e32d2f22c26bc94f238ee8d28315e4911f09f4ee (patch) | |
| tree | 30185b1c9536e616a963149113379d3a30f4a8f3 /test/unit/util/stats_black.cpp | |
| parent | cddee98272723b5816c449e8ed48fa2c5bb85a9e (diff) | |
Add assumption-based unsat cores. (#5887)
This PR adds an assumption-based unsat cores option. If enabled it will disable proof logging in the SAT solver and adds input assertions as assumptions to the SAT solver. When an unsat core is requested we extract the unsat core in terms of the unsat assumption in the SAT solver. Assumption-based unsat cores use the proof infrastructure to map the input assumptions back to the original assertions.
Diffstat (limited to 'test/unit/util/stats_black.cpp')
0 files changed, 0 insertions, 0 deletions