From 5e08c3de2ebd981aca3b6126e839d6438c926290 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= Date: Fri, 6 Oct 2023 15:28:19 -0700 Subject: [PATCH] Add new constant kinds to is_value --- cvc5/src/cvc5_term.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/cvc5/src/cvc5_term.cpp b/cvc5/src/cvc5_term.cpp index 33c9a6a1d..dc3a5cd66 100644 --- a/cvc5/src/cvc5_term.cpp +++ b/cvc5/src/cvc5_term.cpp @@ -268,9 +268,15 @@ bool Cvc5Term::is_value() const // checking all possible const types for future-proofing // not all these sorts are even supported at this time ::cvc5::Kind k = term.getKind(); - return ((k == ::cvc5::Kind::CONST_BOOLEAN) || (k == ::cvc5::Kind::CONST_BITVECTOR) - || (k == ::cvc5::Kind::CONST_RATIONAL) || (k == ::cvc5::Kind::CONST_FLOATINGPOINT) - || (k == ::cvc5::Kind::CONST_ROUNDINGMODE) || (k == ::cvc5::Kind::CONST_STRING) + return ((k == ::cvc5::Kind::CONST_BOOLEAN) + || (k == ::cvc5::Kind::CONST_BITVECTOR) + || (k == ::cvc5::Kind::CONST_RATIONAL) + || (k == ::cvc5::Kind::CONST_INTEGER) + || (k == ::cvc5::Kind::CONST_FINITE_FIELD) + || (k == ::cvc5::Kind::CONST_FLOATINGPOINT) + || (k == ::cvc5::Kind::CONST_ROUNDINGMODE) + || (k == ::cvc5::Kind::CONST_STRING) + || (k == ::cvc5::Kind::CONST_SEQUENCE) || (k == ::cvc5::Kind::CONST_ARRAY)); }