projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 74aad1b) | patch
Rewrite witness terms at prerewrite (#5419)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 11 Nov 2020 18:39:38 +0000 (12:39 -0600)
committerGitHub <noreply@github.com>
Wed, 11 Nov 2020 18:39:38 +0000 (12:39 -0600)
commit7d3198d18304eb6ea5f087a82defb4952fce31b9
tree8eb045184b7fcb1902c76c8cdb3fa75919872244tree
parent74aad1b10d0ed716624abfadf9cccc4ae7e4ba96commit | diff
Rewrite witness terms at prerewrite (#5419)

Ensures (witness ((x Int)) (= x (+ 1 a)) is rewritten to (+ 1 a), instead of e.g. (witness ((x Int)) (= a (- x 1)).

This is required for supporting purification skolems for arithmetic terms in the new proof architecture.
src/theory/builtin/theory_builtin_rewriter.cpp diff | blob | history
src/theory/builtin/theory_builtin_rewriter.h diff | blob | history