diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-22 00:50:02 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-22 07:50:02 +0000 |
| commit | d3af203110d575a89a119c4f2c3956a4f6ce69f5 (patch) | |
| tree | 865ff8ba65e9ea03008680a493091d0ba4a441b6 /src/smt/smt_engine.h | |
| parent | b839049634d97025ac57ba9a342fd8ab70737a33 (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.
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3128257e6..02e5c6b06 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds, Morgan Deters, Aina Niemetz + * * This file is part of the cvc5 project. * @@ -368,6 +368,11 @@ class CVC5_EXPORT SmtEngine Result assertFormula(const Node& formula, bool inUnsatCore = true); /** + * Reduce an unsatisfiable core to make it minimal. + */ + std::vector<Node> reduceUnsatCore(const std::vector<Node>& core); + + /** * Check if a given (set of) expression(s) is entailed with respect to the * current set of assertions. We check this by asserting the negation of * the (big AND over the) given (set of) expression(s). |