projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d603925) | patch
Refactor atom rewriting to be RAN-aware (#7928)
authorGereon Kremer <gkremer@stanford.edu>
Wed, 12 Jan 2022 22:51:29 +0000 (14:51 -0800)
committerGitHub <noreply@github.com>
Wed, 12 Jan 2022 22:51:29 +0000 (22:51 +0000)
commitdefb0de81171b6633e5ef745f927217614a4fe54
tree68badc96890454bd904f75c6a78e706101373e73tree
parentd603925de77bc465fe6bfe5097e848224337acf9commit | diff
Refactor atom rewriting to be RAN-aware (#7928)

This PR starts refactoring the arithmetic rewriter by making rewriting of atoms aware of real algebraic numbers.
It also is slightly more aggressive now, directly rewriting relational operators where lhs = rhs in the preRewrite stage.
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history