projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ffed5a4) | patch
(proof-new) Improve rewriter for WITNESS (#4661)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Jul 2020 04:48:08 +0000 (23:48 -0500)
committerGitHub <noreply@github.com>
Wed, 1 Jul 2020 04:48:08 +0000 (23:48 -0500)
commitb58e0b24b1f5e319ceb468e9009b727df481af7c
tree5b98baebdef6758817c6c8a81a1a2c66e790ee1etree
parentffed5a43764641d4808aa77bb0e393623fd4442dcommit | diff
(proof-new) Improve rewriter for WITNESS (#4661)

Proof checking failures revealed that we are not rewriting witness for Boolean variables (witness ((x Bool)) x) ---> true and (witness ((x Bool)) (not x)) ---> false.

Also adds 2 assertions that are required for elimination (witness ((x T)) (= x t)) ---> t. These assertions should always hold due to the witness terms we construct.
src/theory/builtin/theory_builtin_rewriter.cpp diff | blob | history