projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9cd5bbf) | patch
Fixes for extended rewriter (#4278)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 12 Apr 2020 20:10:31 +0000 (15:10 -0500)
committerGitHub <noreply@github.com>
Sun, 12 Apr 2020 20:10:31 +0000 (15:10 -0500)
commitb9a903cc9a13c7bcdd334eb38730e62858321f07
tree040863b41d21f4c14726eeb27fd0b19bc3d6cfcctree
parent9cd5bbf8c659d2e260bad71a841f5153f358a58bcommit | diff
Fixes for extended rewriter (#4278)

Fixes #4273 and fixes #4274 .

This also removes a spurious assertion from the Node::substitute method that the result node is not equal to the domain. This is violated for f(f(x)) { f(x) -> x }.
src/expr/node.h diff | blob | history
src/theory/quantifiers/extended_rewrite.cpp diff | blob | history
src/theory/quantifiers/extended_rewrite.h diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/issue4273-ext-rew-cache.smt2 [new file with mode: 0644] blob