projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 554d96c) | patch
Add support for RANs in rewriter for `MULT` (#7940)
authorGereon Kremer <gkremer@stanford.edu>
Fri, 14 Jan 2022 15:57:24 +0000 (07:57 -0800)
committerGitHub <noreply@github.com>
Fri, 14 Jan 2022 15:57:24 +0000 (15:57 +0000)
commit549329cd3803b1ebe6e59036e1d69fb21474ca2d
treecca9f4a5845f7647d87a4fc0a1a9bfe8567f6501tree
parent554d96c4c74118ad4078eb12eccd537434baca41commit | diff
Add support for RANs in rewriter for `MULT` (#7940)

This PR refactors the post rewriter for multiplication. It now supports real algebraic numbers and tries a bit harder to avoid the overhead of the normal form abstraction.
src/theory/arith/arith_rewriter.cpp diff | blob | history
test/unit/theory/theory_arith_rewriter_black.cpp diff | blob | history