projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f976478) | patch
Consider PI to be a model value (#8176)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 25 Feb 2022 22:48:12 +0000 (16:48 -0600)
committerGitHub <noreply@github.com>
Fri, 25 Feb 2022 22:48:12 +0000 (16:48 -0600)
commitf051883afa31d9dbe14a5d1ae1c9700cffded3b1
tree89d1f0cd19bf4a3b3f9aeeeb26b1311dcb194321tree
parentf9764781383b86608cae4bff2fe3cd0edc6e1107commit | diff
Consider PI to be a model value (#8176)

Fixes cvc5/cvc5-projects#460.

The special case is necessary due to the node representation of nullary operators, which uses variables internally to represent operators. The other nullary operators are not model values.
src/theory/theory_model.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/nta/proj-issue460-pi-value.smt2 [new file with mode: 0644] blob