projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b839049) | patch
Add support for minimal unsat cores (#4605)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 22 Jul 2021 07:50:02 +0000 (00:50 -0700)
committerGitHub <noreply@github.com>
Thu, 22 Jul 2021 07:50:02 +0000 (07:50 +0000)
commitd3af203110d575a89a119c4f2c3956a4f6ce69f5
tree865ff8ba65e9ea03008680a493091d0ba4a441b6tree
parentb839049634d97025ac57ba9a342fd8ab70737a33commit | diff
Add support for minimal unsat cores (#4605)

This commit adds support for computing minimal unsat cores. The
algorithm implemented in this commit is just a trivial deletion-based
algorithm that tries to remove each assertion in the unsat core
individually.
NEWS diff | blob | history
src/options/smt_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/minimal_unsat_core.smt2 [new file with mode: 0644] blob