From 0e8773b06f119edd4107c53c80d4565c408a0df7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= Date: Thu, 19 Oct 2023 14:50:20 +0200 Subject: [PATCH] Update cvc5 to 1.0.8 (#332) Fixes #328 . --- .github/workflows/ci.yml | 2 +- contrib/setup-cvc5.sh | 2 +- cvc5/CMakeLists.txt | 4 +- cvc5/include/cvc5_datatype.h | 2 +- cvc5/include/cvc5_solver.h | 2 +- cvc5/include/cvc5_sort.h | 4 +- cvc5/include/cvc5_term.h | 2 +- cvc5/src/cvc5_solver.cpp | 144 +++++++++++----------- cvc5/src/cvc5_term.cpp | 174 ++++++++++++++------------- include/ops.h | 1 + tests/cvc5/cvc5-interpolants-api.cpp | 10 +- tests/cvc5/cvc5-printing.cpp | 2 +- tests/cvc5/cvc5-term-iter.cpp | 6 +- 13 files changed, 181 insertions(+), 174 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index aeec2e8d9..dea0f5d86 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -46,7 +46,7 @@ jobs: - name: Python Dependencies run: | python3 -m pip install --user Cython==0.29.* - python3 -m pip install --user pytest scikit-build toml + python3 -m pip install --user pytest scikit-build toml pyparsing echo "$(python3 -m site --user-base)/bin" >> $GITHUB_PATH - name: Install Bison diff --git a/contrib/setup-cvc5.sh b/contrib/setup-cvc5.sh index 777ac4eb6..419b2cf82 100755 --- a/contrib/setup-cvc5.sh +++ b/contrib/setup-cvc5.sh @@ -5,7 +5,7 @@ DEPS=$DIR/../deps mkdir -p $DEPS -CVC5_VERSION=77d0bec48a745e3c4acd65085f9c59bdfceed6c0 +CVC5_VERSION=cvc5-1.0.8 if [ "$(uname)" == "Darwin" ]; then NUM_CORES=$(sysctl -n hw.logicalcpu) diff --git a/cvc5/CMakeLists.txt b/cvc5/CMakeLists.txt index 859c1b49e..2ab2a3b1a 100644 --- a/cvc5/CMakeLists.txt +++ b/cvc5/CMakeLists.txt @@ -13,9 +13,9 @@ target_include_directories (smt-switch-cvc5 PUBLIC "${PROJECT_SOURCE_DIR}/includ target_include_directories (smt-switch-cvc5 PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/include") target_include_directories (smt-switch-cvc5 PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/cvc5/include") target_include_directories (smt-switch-cvc5 PUBLIC "${CVC5_HOME}/src") -target_include_directories (smt-switch-cvc5 PUBLIC "${CVC5_HOME}/src/include") +target_include_directories (smt-switch-cvc5 PUBLIC "${CVC5_HOME}/include") # TEMP only until the internal kinds are no longer part of public API -target_include_directories (smt-switch-cvc5 PUBLIC "${CVC5_HOME}/build/src") +target_include_directories (smt-switch-cvc5 PUBLIC "${CVC5_HOME}/build/include") target_include_directories (smt-switch-cvc5 PUBLIC ${GMP_INCLUDE_DIR}) if (LIBRT) diff --git a/cvc5/include/cvc5_datatype.h b/cvc5/include/cvc5_datatype.h index d706b7582..6e92a9c67 100644 --- a/cvc5/include/cvc5_datatype.h +++ b/cvc5/include/cvc5_datatype.h @@ -15,7 +15,7 @@ #pragma once -#include "api/cpp/cvc5.h" +#include "cvc5/cvc5.h" #include "datatype.h" #include "exceptions.h" diff --git a/cvc5/include/cvc5_solver.h b/cvc5/include/cvc5_solver.h index 015af2abe..281121b4a 100644 --- a/cvc5/include/cvc5_solver.h +++ b/cvc5/include/cvc5_solver.h @@ -24,7 +24,7 @@ #include #include -#include "api/cpp/cvc5.h" +#include "cvc5/cvc5.h" #include "cvc5_datatype.h" #include "cvc5_sort.h" #include "cvc5_term.h" diff --git a/cvc5/include/cvc5_sort.h b/cvc5/include/cvc5_sort.h index 8c938583d..56a5dd358 100644 --- a/cvc5/include/cvc5_sort.h +++ b/cvc5/include/cvc5_sort.h @@ -18,8 +18,8 @@ #include -#include "api/cpp/cvc5.h" -#include "api/cpp/cvc5_kind.h" +#include "cvc5/cvc5.h" +#include "cvc5/cvc5_kind.h" #include "sort.h" namespace smt { diff --git a/cvc5/include/cvc5_term.h b/cvc5/include/cvc5_term.h index 0b562c58f..3086e4574 100644 --- a/cvc5/include/cvc5_term.h +++ b/cvc5/include/cvc5_term.h @@ -16,7 +16,7 @@ #pragma once -#include "api/cpp/cvc5.h" +#include "cvc5/cvc5.h" #include "term.h" #include "utils.h" diff --git a/cvc5/src/cvc5_solver.cpp b/cvc5/src/cvc5_solver.cpp index 537d9b520..be7fedf3b 100644 --- a/cvc5/src/cvc5_solver.cpp +++ b/cvc5/src/cvc5_solver.cpp @@ -21,86 +21,86 @@ namespace smt { /* cvc5 Op mappings */ const std::unordered_map primop2kind( - { { And, ::cvc5::AND }, - { Or, ::cvc5::OR }, - { Xor, ::cvc5::XOR }, - { Not, ::cvc5::NOT }, - { Implies, ::cvc5::IMPLIES }, - { Ite, ::cvc5::ITE }, - { Equal, ::cvc5::EQUAL }, - { Distinct, ::cvc5::DISTINCT }, + { { And, ::cvc5::Kind::AND }, + { Or, ::cvc5::Kind::OR }, + { Xor, ::cvc5::Kind::XOR }, + { Not, ::cvc5::Kind::NOT }, + { Implies, ::cvc5::Kind::IMPLIES }, + { Ite, ::cvc5::Kind::ITE }, + { Equal, ::cvc5::Kind::EQUAL }, + { Distinct, ::cvc5::Kind::DISTINCT }, /* Uninterpreted Functions */ - { Apply, ::cvc5::APPLY_UF }, + { Apply, ::cvc5::Kind::APPLY_UF }, /* Arithmetic Theories */ - { Plus, ::cvc5::ADD }, - { Minus, ::cvc5::SUB }, - { Negate, ::cvc5::NEG }, - { Mult, ::cvc5::MULT }, - { Div, ::cvc5::DIVISION }, - { IntDiv, ::cvc5::INTS_DIVISION }, - { Lt, ::cvc5::LT }, - { Le, ::cvc5::LEQ }, - { Gt, ::cvc5::GT }, - { Ge, ::cvc5::GEQ }, - { Mod, ::cvc5::INTS_MODULUS }, - { Abs, ::cvc5::ABS }, - { Pow, ::cvc5::POW }, - { To_Real, ::cvc5::TO_REAL }, - { To_Int, ::cvc5::TO_INTEGER }, - { Is_Int, ::cvc5::IS_INTEGER }, + { Plus, ::cvc5::Kind::ADD }, + { Minus, ::cvc5::Kind::SUB }, + { Negate, ::cvc5::Kind::NEG }, + { Mult, ::cvc5::Kind::MULT }, + { Div, ::cvc5::Kind::DIVISION }, + { IntDiv, ::cvc5::Kind::INTS_DIVISION }, + { Lt, ::cvc5::Kind::LT }, + { Le, ::cvc5::Kind::LEQ }, + { Gt, ::cvc5::Kind::GT }, + { Ge, ::cvc5::Kind::GEQ }, + { Mod, ::cvc5::Kind::INTS_MODULUS }, + { Abs, ::cvc5::Kind::ABS }, + { Pow, ::cvc5::Kind::POW }, + { To_Real, ::cvc5::Kind::TO_REAL }, + { To_Int, ::cvc5::Kind::TO_INTEGER }, + { Is_Int, ::cvc5::Kind::IS_INTEGER }, /* Fixed Size BitVector Theory */ - { Concat, ::cvc5::BITVECTOR_CONCAT }, + { Concat, ::cvc5::Kind::BITVECTOR_CONCAT }, // Indexed Op - { Extract, ::cvc5::BITVECTOR_EXTRACT }, - { BVNot, ::cvc5::BITVECTOR_NOT }, - { BVNeg, ::cvc5::BITVECTOR_NEG }, - { BVAnd, ::cvc5::BITVECTOR_AND }, - { BVOr, ::cvc5::BITVECTOR_OR }, - { BVXor, ::cvc5::BITVECTOR_XOR }, - { BVNand, ::cvc5::BITVECTOR_NAND }, - { BVNor, ::cvc5::BITVECTOR_NOR }, - { BVXnor, ::cvc5::BITVECTOR_XNOR }, - { BVComp, ::cvc5::BITVECTOR_COMP }, - { BVAdd, ::cvc5::BITVECTOR_ADD }, - { BVSub, ::cvc5::BITVECTOR_SUB }, - { BVMul, ::cvc5::BITVECTOR_MULT }, - { BVUdiv, ::cvc5::BITVECTOR_UDIV }, - { BVSdiv, ::cvc5::BITVECTOR_SDIV }, - { BVUrem, ::cvc5::BITVECTOR_UREM }, - { BVSrem, ::cvc5::BITVECTOR_SREM }, - { BVSmod, ::cvc5::BITVECTOR_SMOD }, - { BVShl, ::cvc5::BITVECTOR_SHL }, - { BVAshr, ::cvc5::BITVECTOR_ASHR }, - { BVLshr, ::cvc5::BITVECTOR_LSHR }, - { BVUlt, ::cvc5::BITVECTOR_ULT }, - { BVUle, ::cvc5::BITVECTOR_ULE }, - { BVUgt, ::cvc5::BITVECTOR_UGT }, - { BVUge, ::cvc5::BITVECTOR_UGE }, - { BVSlt, ::cvc5::BITVECTOR_SLT }, - { BVSle, ::cvc5::BITVECTOR_SLE }, - { BVSgt, ::cvc5::BITVECTOR_SGT }, - { BVSge, ::cvc5::BITVECTOR_SGE }, + { Extract, ::cvc5::Kind::BITVECTOR_EXTRACT }, + { BVNot, ::cvc5::Kind::BITVECTOR_NOT }, + { BVNeg, ::cvc5::Kind::BITVECTOR_NEG }, + { BVAnd, ::cvc5::Kind::BITVECTOR_AND }, + { BVOr, ::cvc5::Kind::BITVECTOR_OR }, + { BVXor, ::cvc5::Kind::BITVECTOR_XOR }, + { BVNand, ::cvc5::Kind::BITVECTOR_NAND }, + { BVNor, ::cvc5::Kind::BITVECTOR_NOR }, + { BVXnor, ::cvc5::Kind::BITVECTOR_XNOR }, + { BVComp, ::cvc5::Kind::BITVECTOR_COMP }, + { BVAdd, ::cvc5::Kind::BITVECTOR_ADD }, + { BVSub, ::cvc5::Kind::BITVECTOR_SUB }, + { BVMul, ::cvc5::Kind::BITVECTOR_MULT }, + { BVUdiv, ::cvc5::Kind::BITVECTOR_UDIV }, + { BVSdiv, ::cvc5::Kind::BITVECTOR_SDIV }, + { BVUrem, ::cvc5::Kind::BITVECTOR_UREM }, + { BVSrem, ::cvc5::Kind::BITVECTOR_SREM }, + { BVSmod, ::cvc5::Kind::BITVECTOR_SMOD }, + { BVShl, ::cvc5::Kind::BITVECTOR_SHL }, + { BVAshr, ::cvc5::Kind::BITVECTOR_ASHR }, + { BVLshr, ::cvc5::Kind::BITVECTOR_LSHR }, + { BVUlt, ::cvc5::Kind::BITVECTOR_ULT }, + { BVUle, ::cvc5::Kind::BITVECTOR_ULE }, + { BVUgt, ::cvc5::Kind::BITVECTOR_UGT }, + { BVUge, ::cvc5::Kind::BITVECTOR_UGE }, + { BVSlt, ::cvc5::Kind::BITVECTOR_SLT }, + { BVSle, ::cvc5::Kind::BITVECTOR_SLE }, + { BVSgt, ::cvc5::Kind::BITVECTOR_SGT }, + { BVSge, ::cvc5::Kind::BITVECTOR_SGE }, // Indexed Op - { Zero_Extend, ::cvc5::BITVECTOR_ZERO_EXTEND }, + { Zero_Extend, ::cvc5::Kind::BITVECTOR_ZERO_EXTEND }, // Indexed Op - { Sign_Extend, ::cvc5::BITVECTOR_SIGN_EXTEND }, + { Sign_Extend, ::cvc5::Kind::BITVECTOR_SIGN_EXTEND }, // Indexed Op - { Repeat, ::cvc5::BITVECTOR_REPEAT }, + { Repeat, ::cvc5::Kind::BITVECTOR_REPEAT }, // Indexed Op - { Rotate_Left, ::cvc5::BITVECTOR_ROTATE_LEFT }, + { Rotate_Left, ::cvc5::Kind::BITVECTOR_ROTATE_LEFT }, // Indexed Op - { Rotate_Right, ::cvc5::BITVECTOR_ROTATE_RIGHT }, + { Rotate_Right, ::cvc5::Kind::BITVECTOR_ROTATE_RIGHT }, // Conversion - { BV_To_Nat, ::cvc5::BITVECTOR_TO_NAT }, + { BV_To_Nat, ::cvc5::Kind::BITVECTOR_TO_NAT }, // Indexed Op - { Int_To_BV, ::cvc5::INT_TO_BITVECTOR }, - { Select, ::cvc5::SELECT }, - { Store, ::cvc5::STORE }, - { Forall, ::cvc5::FORALL }, - { Exists, ::cvc5::EXISTS }, - { Apply_Selector, ::cvc5::APPLY_SELECTOR }, - { Apply_Tester, ::cvc5::APPLY_TESTER }, - { Apply_Constructor, ::cvc5::APPLY_CONSTRUCTOR } }); + { Int_To_BV, ::cvc5::Kind::INT_TO_BITVECTOR }, + { Select, ::cvc5::Kind::SELECT }, + { Store, ::cvc5::Kind::STORE }, + { Forall, ::cvc5::Kind::FORALL }, + { Exists, ::cvc5::Kind::EXISTS }, + { Apply_Selector, ::cvc5::Kind::APPLY_SELECTOR }, + { Apply_Tester, ::cvc5::Kind::APPLY_TESTER }, + { Apply_Constructor, ::cvc5::Kind::APPLY_CONSTRUCTOR } }); /* Cvc5Solver implementation */ @@ -405,7 +405,7 @@ UnorderedTermMap Cvc5Solver::get_array_values(const Term & arr, TermVec values; Term idx; Term val; - while (carr.hasOp() && carr.getKind() == cvc5::STORE) + while (carr.hasOp() && carr.getKind() == cvc5::Kind::STORE) { idx = make_shared_term(carr[1]); val = make_shared_term(carr[2]); @@ -414,7 +414,7 @@ UnorderedTermMap Cvc5Solver::get_array_values(const Term & arr, carr = carr[0]; } - if (carr.getKind() == cvc5::CONST_ARRAY) + if (carr.getKind() == cvc5::Kind::CONST_ARRAY) { out_const_base = make_shared_term(carr.getConstArrayBase()); } @@ -927,7 +927,7 @@ Term Cvc5Solver::make_term(Op op, const TermVec & terms) const while (cterms.size()) { ::cvc5::Term bound_var = - solver.mkTerm(cvc5::VARIABLE_LIST, { cterms.back() }); + solver.mkTerm(cvc5::Kind::VARIABLE_LIST, { cterms.back() }); cterms.pop_back(); quant_res = solver.mkTerm(quant_kind, { bound_var, quant_res }); } diff --git a/cvc5/src/cvc5_term.cpp b/cvc5/src/cvc5_term.cpp index 95eb544a3..d9b690fd5 100644 --- a/cvc5/src/cvc5_term.cpp +++ b/cvc5/src/cvc5_term.cpp @@ -16,7 +16,7 @@ #include "cvc5_term.h" -#include "api/cpp/cvc5.h" +#include "cvc5/cvc5.h" #include "assert.h" #include "cvc5_sort.h" #include "exceptions.h" @@ -25,95 +25,95 @@ namespace smt { // the kinds cvc5 needs to build an OpTerm for an indexed op const std::unordered_map<::cvc5::Kind, size_t> kind2numindices( - { { ::cvc5::BITVECTOR_EXTRACT, 2 }, - { ::cvc5::BITVECTOR_ZERO_EXTEND, 1 }, - { ::cvc5::BITVECTOR_SIGN_EXTEND, 1 }, - { ::cvc5::BITVECTOR_REPEAT, 1 }, - { ::cvc5::BITVECTOR_ROTATE_LEFT, 1 }, - { ::cvc5::BITVECTOR_ROTATE_RIGHT, 1 }, - { ::cvc5::INT_TO_BITVECTOR, 1 } }); + { { ::cvc5::Kind::BITVECTOR_EXTRACT, 2 }, + { ::cvc5::Kind::BITVECTOR_ZERO_EXTEND, 1 }, + { ::cvc5::Kind::BITVECTOR_SIGN_EXTEND, 1 }, + { ::cvc5::Kind::BITVECTOR_REPEAT, 1 }, + { ::cvc5::Kind::BITVECTOR_ROTATE_LEFT, 1 }, + { ::cvc5::Kind::BITVECTOR_ROTATE_RIGHT, 1 }, + { ::cvc5::Kind::INT_TO_BITVECTOR, 1 } }); const std::unordered_map<::cvc5::Kind, PrimOp> kind2primop( - { { ::cvc5::AND, And }, - { ::cvc5::OR, Or }, - { ::cvc5::XOR, Xor }, - { ::cvc5::NOT, Not }, - { ::cvc5::IMPLIES, Implies }, - { ::cvc5::ITE, Ite }, - { ::cvc5::EQUAL, Equal }, - { ::cvc5::DISTINCT, Distinct }, + { { ::cvc5::Kind::AND, And }, + { ::cvc5::Kind::OR, Or }, + { ::cvc5::Kind::XOR, Xor }, + { ::cvc5::Kind::NOT, Not }, + { ::cvc5::Kind::IMPLIES, Implies }, + { ::cvc5::Kind::ITE, Ite }, + { ::cvc5::Kind::EQUAL, Equal }, + { ::cvc5::Kind::DISTINCT, Distinct }, /* Uninterpreted Functions */ - { ::cvc5::APPLY_UF, Apply }, + { ::cvc5::Kind::APPLY_UF, Apply }, /* Arithmetic Theories */ - { ::cvc5::ADD, Plus }, - { ::cvc5::SUB, Minus }, - { ::cvc5::NEG, Negate }, - { ::cvc5::MULT, Mult }, - { ::cvc5::DIVISION, Div }, - { ::cvc5::LT, Lt }, - { ::cvc5::LEQ, Le }, - { ::cvc5::GT, Gt }, - { ::cvc5::GEQ, Ge }, - { ::cvc5::INTS_MODULUS, Mod }, - { ::cvc5::ABS, Abs }, - { ::cvc5::POW, Pow }, - { ::cvc5::TO_REAL, To_Real }, - { ::cvc5::TO_INTEGER, To_Int }, - { ::cvc5::IS_INTEGER, Is_Int }, + { ::cvc5::Kind::ADD, Plus }, + { ::cvc5::Kind::SUB, Minus }, + { ::cvc5::Kind::NEG, Negate }, + { ::cvc5::Kind::MULT, Mult }, + { ::cvc5::Kind::DIVISION, Div }, + { ::cvc5::Kind::LT, Lt }, + { ::cvc5::Kind::LEQ, Le }, + { ::cvc5::Kind::GT, Gt }, + { ::cvc5::Kind::GEQ, Ge }, + { ::cvc5::Kind::INTS_MODULUS, Mod }, + { ::cvc5::Kind::ABS, Abs }, + { ::cvc5::Kind::POW, Pow }, + { ::cvc5::Kind::TO_REAL, To_Real }, + { ::cvc5::Kind::TO_INTEGER, To_Int }, + { ::cvc5::Kind::IS_INTEGER, Is_Int }, /* Fixed Size BitVector Theory */ - { ::cvc5::BITVECTOR_CONCAT, Concat }, + { ::cvc5::Kind::BITVECTOR_CONCAT, Concat }, // Indexed Op - { ::cvc5::BITVECTOR_EXTRACT, Extract }, - { ::cvc5::BITVECTOR_NOT, BVNot }, - { ::cvc5::BITVECTOR_NEG, BVNeg }, - { ::cvc5::BITVECTOR_AND, BVAnd }, - { ::cvc5::BITVECTOR_OR, BVOr }, - { ::cvc5::BITVECTOR_XOR, BVXor }, - { ::cvc5::BITVECTOR_NAND, BVNand }, - { ::cvc5::BITVECTOR_NOR, BVNor }, - { ::cvc5::BITVECTOR_XNOR, BVXnor }, - { ::cvc5::BITVECTOR_COMP, BVComp }, - { ::cvc5::BITVECTOR_ADD, BVAdd }, - { ::cvc5::BITVECTOR_SUB, BVSub }, - { ::cvc5::BITVECTOR_MULT, BVMul }, - { ::cvc5::BITVECTOR_UDIV, BVUdiv }, - { ::cvc5::BITVECTOR_SDIV, BVSdiv }, - { ::cvc5::BITVECTOR_UREM, BVUrem }, - { ::cvc5::BITVECTOR_SREM, BVSrem }, - { ::cvc5::BITVECTOR_SMOD, BVSmod }, - { ::cvc5::BITVECTOR_SHL, BVShl }, - { ::cvc5::BITVECTOR_ASHR, BVAshr }, - { ::cvc5::BITVECTOR_LSHR, BVLshr }, - { ::cvc5::BITVECTOR_ULT, BVUlt }, - { ::cvc5::BITVECTOR_ULE, BVUle }, - { ::cvc5::BITVECTOR_UGT, BVUgt }, - { ::cvc5::BITVECTOR_UGE, BVUge }, - { ::cvc5::BITVECTOR_SLT, BVSlt }, - { ::cvc5::BITVECTOR_SLE, BVSle }, - { ::cvc5::BITVECTOR_SGT, BVSgt }, - { ::cvc5::BITVECTOR_SGE, BVSge }, + { ::cvc5::Kind::BITVECTOR_EXTRACT, Extract }, + { ::cvc5::Kind::BITVECTOR_NOT, BVNot }, + { ::cvc5::Kind::BITVECTOR_NEG, BVNeg }, + { ::cvc5::Kind::BITVECTOR_AND, BVAnd }, + { ::cvc5::Kind::BITVECTOR_OR, BVOr }, + { ::cvc5::Kind::BITVECTOR_XOR, BVXor }, + { ::cvc5::Kind::BITVECTOR_NAND, BVNand }, + { ::cvc5::Kind::BITVECTOR_NOR, BVNor }, + { ::cvc5::Kind::BITVECTOR_XNOR, BVXnor }, + { ::cvc5::Kind::BITVECTOR_COMP, BVComp }, + { ::cvc5::Kind::BITVECTOR_ADD, BVAdd }, + { ::cvc5::Kind::BITVECTOR_SUB, BVSub }, + { ::cvc5::Kind::BITVECTOR_MULT, BVMul }, + { ::cvc5::Kind::BITVECTOR_UDIV, BVUdiv }, + { ::cvc5::Kind::BITVECTOR_SDIV, BVSdiv }, + { ::cvc5::Kind::BITVECTOR_UREM, BVUrem }, + { ::cvc5::Kind::BITVECTOR_SREM, BVSrem }, + { ::cvc5::Kind::BITVECTOR_SMOD, BVSmod }, + { ::cvc5::Kind::BITVECTOR_SHL, BVShl }, + { ::cvc5::Kind::BITVECTOR_ASHR, BVAshr }, + { ::cvc5::Kind::BITVECTOR_LSHR, BVLshr }, + { ::cvc5::Kind::BITVECTOR_ULT, BVUlt }, + { ::cvc5::Kind::BITVECTOR_ULE, BVUle }, + { ::cvc5::Kind::BITVECTOR_UGT, BVUgt }, + { ::cvc5::Kind::BITVECTOR_UGE, BVUge }, + { ::cvc5::Kind::BITVECTOR_SLT, BVSlt }, + { ::cvc5::Kind::BITVECTOR_SLE, BVSle }, + { ::cvc5::Kind::BITVECTOR_SGT, BVSgt }, + { ::cvc5::Kind::BITVECTOR_SGE, BVSge }, // Indexed Op - { ::cvc5::BITVECTOR_ZERO_EXTEND, Zero_Extend }, + { ::cvc5::Kind::BITVECTOR_ZERO_EXTEND, Zero_Extend }, // Indexed Op - { ::cvc5::BITVECTOR_SIGN_EXTEND, Sign_Extend }, + { ::cvc5::Kind::BITVECTOR_SIGN_EXTEND, Sign_Extend }, // Indexed Op - { ::cvc5::BITVECTOR_REPEAT, Repeat }, + { ::cvc5::Kind::BITVECTOR_REPEAT, Repeat }, // Indexed Op - { ::cvc5::BITVECTOR_ROTATE_LEFT, Rotate_Left }, + { ::cvc5::Kind::BITVECTOR_ROTATE_LEFT, Rotate_Left }, // Indexed Op - { ::cvc5::BITVECTOR_ROTATE_RIGHT, Rotate_Right }, + { ::cvc5::Kind::BITVECTOR_ROTATE_RIGHT, Rotate_Right }, // Conversion - { ::cvc5::BITVECTOR_TO_NAT, BV_To_Nat }, + { ::cvc5::Kind::BITVECTOR_TO_NAT, BV_To_Nat }, // Indexed Op - { ::cvc5::INT_TO_BITVECTOR, Int_To_BV }, - { ::cvc5::SELECT, Select }, - { ::cvc5::STORE, Store }, - { ::cvc5::FORALL, Forall }, - { ::cvc5::EXISTS, Exists }, + { ::cvc5::Kind::INT_TO_BITVECTOR, Int_To_BV }, + { ::cvc5::Kind::SELECT, Select }, + { ::cvc5::Kind::STORE, Store }, + { ::cvc5::Kind::FORALL, Forall }, + { ::cvc5::Kind::EXISTS, Exists }, // Datatype - { ::cvc5::APPLY_CONSTRUCTOR, Apply_Constructor }, - { ::cvc5::APPLY_TESTER, Apply_Tester }, - { ::cvc5::APPLY_SELECTOR, Apply_Selector } }); + { ::cvc5::Kind::APPLY_CONSTRUCTOR, Apply_Constructor }, + { ::cvc5::Kind::APPLY_TESTER, Apply_Tester }, + { ::cvc5::Kind::APPLY_SELECTOR, Apply_Selector } }); // struct for hashing std::hash termhash; @@ -148,7 +148,7 @@ const Term Cvc5TermIter::operator*() // smt-switch cvc5 backend guarantees that the length is only one by // construction ::cvc5::Term t = term[pos]; - if (t.getKind() == ::cvc5::VARIABLE_LIST) + if (t.getKind() == ::cvc5::Kind::VARIABLE_LIST) { if (t.getNumChildren() != 1) { @@ -262,14 +262,14 @@ bool Cvc5Term::is_symbol() const { // functions, parameters, and symbolic constants are all symbols ::cvc5::Kind k = term.getKind(); - return (k == ::cvc5::CONSTANT || k == ::cvc5::VARIABLE); + return (k == ::cvc5::Kind::CONSTANT || k == ::cvc5::Kind::VARIABLE); } -bool Cvc5Term::is_param() const { return (term.getKind() == ::cvc5::VARIABLE); } +bool Cvc5Term::is_param() const { return (term.getKind() == ::cvc5::Kind::VARIABLE); } bool Cvc5Term::is_symbolic_const() const { - return (term.getKind() == ::cvc5::CONSTANT && !term.getSort().isFunction()); + return (term.getKind() == ::cvc5::Kind::CONSTANT && !term.getSort().isFunction()); } bool Cvc5Term::is_value() const @@ -277,10 +277,16 @@ 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::CONST_BOOLEAN) || (k == ::cvc5::CONST_BITVECTOR) - || (k == ::cvc5::CONST_RATIONAL) || (k == ::cvc5::CONST_FLOATINGPOINT) - || (k == ::cvc5::CONST_ROUNDINGMODE) || (k == ::cvc5::CONST_STRING) - || (k == ::cvc5::CONST_ARRAY)); + 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)); } std::string Cvc5Term::to_string() { return term.toString(); } diff --git a/include/ops.h b/include/ops.h index 39e3f23a0..d759f58b8 100644 --- a/include/ops.h +++ b/include/ops.h @@ -16,6 +16,7 @@ #pragma once +#include #include #include #include diff --git a/tests/cvc5/cvc5-interpolants-api.cpp b/tests/cvc5/cvc5-interpolants-api.cpp index da671c222..795660548 100644 --- a/tests/cvc5/cvc5-interpolants-api.cpp +++ b/tests/cvc5/cvc5-interpolants-api.cpp @@ -2,7 +2,7 @@ #include #include -#include "api/cpp/cvc5.h" +#include "cvc5/cvc5.h" #include "assert.h" #include "cvc5_factory.h" #include "smt.h" @@ -19,14 +19,14 @@ int main() Term b1 = s.mkConst(boolsort, "b1"); Term b2 = s.mkConst(boolsort, "b2"); - cout << (b2.getKind() == CONSTANT) << std::endl; + cout << (b2.getKind() == Kind::CONSTANT) << std::endl; - if (b2.getKind() != CONSTANT) + if (b2.getKind() != Kind::CONSTANT) { throw std::exception(); } - s.assertFormula(s.mkTerm(AND, { b1, b2 })); + s.assertFormula(s.mkTerm(Kind::AND, { b1, b2 })); Term I = s.getInterpolant(b2); if (!I.isNull()) @@ -36,7 +36,7 @@ int main() cout << (I == b2) << endl; - if (I.getKind() != CONSTANT) + if (I.getKind() != Kind::CONSTANT) { cout << "ERROR The interpolant should have kind CONSTANT but has kind: " << kindToString(I.getKind()) << endl; diff --git a/tests/cvc5/cvc5-printing.cpp b/tests/cvc5/cvc5-printing.cpp index 6757f0b46..f601e10e6 100644 --- a/tests/cvc5/cvc5-printing.cpp +++ b/tests/cvc5/cvc5-printing.cpp @@ -145,7 +145,7 @@ void test1(SmtSolver s, ostream & os, stringbuf & strbuf) s->pop(1); s->check_sat(); s->get_value(x); - dump_and_run(strbuf, "unsat\n()\nsat\n((x (_ bv0 32)))\n"); + dump_and_run(strbuf, "unsat\n(ind1)\nsat\n((x (_ bv0 32)))\n"); } int main() diff --git a/tests/cvc5/cvc5-term-iter.cpp b/tests/cvc5/cvc5-term-iter.cpp index 092efc96b..26620f154 100644 --- a/tests/cvc5/cvc5-term-iter.cpp +++ b/tests/cvc5/cvc5-term-iter.cpp @@ -18,7 +18,7 @@ #include #include -#include "api/cpp/cvc5.h" +#include "cvc5/cvc5.h" #include "assert.h" #include "cvc5_term.h" #include "gtest/gtest.h" @@ -37,8 +37,8 @@ TEST(Cvc5TermIterTest, Copy) ::cvc5::Term v = solver.mkConst(bvsort4, "v"); ::cvc5::Term f = solver.mkConst(funsort, "f"); - ::cvc5::Term fx = solver.mkTerm(cvc5::APPLY_UF, { f, x }); - ::cvc5::Term fv = solver.mkTerm(cvc5::APPLY_UF, { f, v }); + ::cvc5::Term fx = solver.mkTerm(cvc5::Kind::APPLY_UF, { f, x }); + ::cvc5::Term fv = solver.mkTerm(cvc5::Kind::APPLY_UF, { f, v }); Cvc5TermIter it1(fx, 0); Cvc5TermIter it2(fx, 0);