projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ac2a185) | patch
Consider RANs in variable ordering (#7964)
authorGereon Kremer <gkremer@stanford.edu>
Tue, 1 Feb 2022 02:19:58 +0000 (18:19 -0800)
committerGitHub <noreply@github.com>
Tue, 1 Feb 2022 02:19:58 +0000 (02:19 +0000)
commitfc620343734a9a2415792182a91f7fd273d9c9c1
treeca303cfbcf6bad1c7b9da7cca6da42066f911c44tree
parentac2a185f2895095f2c8e1ddb52aa33c40ab07e2ecommit | diff
Consider RANs in variable ordering (#7964)

The variable ordering in the arithmetic normal form should also consider real algebraic numbers. This PR also adds new comparators (essentially doing the same) in the rewriter that will replace the normal form utility classes.
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/normal_form.h diff | blob | history