projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ee00caa) | patch
Add the relevance manager module (#4894)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 18 Aug 2020 16:17:26 +0000 (11:17 -0500)
committerGitHub <noreply@github.com>
Tue, 18 Aug 2020 16:17:26 +0000 (11:17 -0500)
commitc460fd4ba1cdacf04305475e605071889ed0e92f
treed9348644ef9030ae606803107345fe5f67a59911tree
parentee00caa684da76ce494d57d30b22ad20c082b652commit | diff
Add the relevance manager module (#4894)

This PR adds the relevance manager module, which will be used in forthcoming PRs to query assignments for whether a literal is "relevant" (e.g. critical for satisfying the input formula). Leveraging this technique has led to noticeable improvements for non-linear arithmetic (https://github.com/ajreynol/CVC4/tree/relManager).

This PR does not enable it, but adds the module only.
src/CMakeLists.txt diff | blob | history
src/theory/relevance_manager.cpp [new file with mode: 0644] blob
src/theory/relevance_manager.h [new file with mode: 0644] blob