projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b272d60) | patch
Generalize inequality elimination in quantifiers rewriter (#7030)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 23 Aug 2021 21:42:14 +0000 (16:42 -0500)
committerGitHub <noreply@github.com>
Mon, 23 Aug 2021 21:42:14 +0000 (21:42 +0000)
commit982b585a1b766a933055d7328579cdb482504fe4
tree085328ba996448cd3926468770ba858b4b0c2f14tree
parentb272d60452028025d56dbf6ffe10276d6f9281cbcommit | diff
Generalize inequality elimination in quantifiers rewriter (#7030)

This generalizes our inequality elimination technique to handle disequalities as well as inequalities.

#6999 is an example where a variable can be eliminated: if a variable x occurs only in an equality with negative required polarity, then the variable and that literal can be eliminated.

Fixes #6999.
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/quantifiers/issue6999-deq-elim.smt2 [new file with mode: 0644] blob