projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e20a8b4) | patch
Consider polarity in relevance manager (#7768)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 9 Dec 2021 22:04:36 +0000 (16:04 -0600)
committerGitHub <noreply@github.com>
Thu, 9 Dec 2021 22:04:36 +0000 (22:04 +0000)
commit93e71ff09714d504da93fbdb0448c656f60c0b98
treebe72e8f8b33bd0f2dc47948e16de023fb6b09ef8tree
parente20a8b4ea58f77a2d8a21b15d639d5a2a6a7b48dcommit | diff
Consider polarity in relevance manager (#7768)

This ensures we only consider things relevant if their polarity is compatible with current asserted value.

As a consequence, this makes our computation of get-difficulty more accurate, as well as making Valuation::isRelevant more precise (e.g. for non-linear).

Notice that this fixes a bug in PolarityTermContext as well.
src/expr/term_context.cpp diff | blob | history
src/theory/relevance_manager.cpp diff | blob | history
src/theory/relevance_manager.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/difficulty-polarity.smt2 [new file with mode: 0644] blob