projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 709d61c) | patch
Add new ordering utility (#8008)
authorGereon Kremer <gkremer@stanford.edu>
Tue, 1 Feb 2022 19:16:24 +0000 (11:16 -0800)
committerGitHub <noreply@github.com>
Tue, 1 Feb 2022 19:16:24 +0000 (19:16 +0000)
commita7705df3f4df10c0e26bdda3f119c74801ec275d
treefa8f7ec7034cd708ea92c67eea7b52d6631f59a9tree
parent709d61c8ffaf89e544ca2c8eead966348da2160ccommit | diff
Add new ordering utility (#8008)

This PR provides a clean implementation of the comparators from the normal form utility, also supporting real algebraic numbers. They will be used within the refactored arithmetic rewriter.
src/CMakeLists.txt diff | blob | history
src/theory/arith/rewriter/ordering.h [new file with mode: 0644] blob