projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4975ae6) | patch
Adds a kind to hold RealAlgebraicNumber constants (#7908)
authorGereon Kremer <gkremer@stanford.edu>
Tue, 11 Jan 2022 22:44:43 +0000 (14:44 -0800)
committerGitHub <noreply@github.com>
Tue, 11 Jan 2022 22:44:43 +0000 (22:44 +0000)
commitebf4ff6cc2d93c59ef347f6db515bf3e44c036f3
tree1b834ec1b15340c9410999a6e6ffe0233aa0f753tree
parent4975ae6cd117f6103ada4ccca329b1e348583ce0commit | diff
Adds a kind to hold RealAlgebraicNumber constants (#7908)

This PR adds a new kind that holds RealAlgebraicNumber constants. As it can not be a constant in the sense of isConst(), it is wrapped within an operator, similar to IAND or CARDINALITY_CONSTRAINT.
src/theory/arith/kinds diff | blob | history
src/theory/arith/theory_arith_type_rules.cpp diff | blob | history
src/theory/arith/theory_arith_type_rules.h diff | blob | history