Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update cvc5 to 1.0.8 #332

Merged
merged 8 commits into from
Oct 19, 2023
Merged

Update cvc5 to 1.0.8 #332

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
47ed909
Add cstdint header for uint64_t type
CyanoKobalamyne Oct 4, 2023
1dbe9da
Fix cvc5 API header locations
CyanoKobalamyne Oct 4, 2023
c904e75
Fix namespace of enum values moved to cvc5::Kind
CyanoKobalamyne Oct 4, 2023
d29b26e
Update downloaded cvc5 version to 1.0.8
CyanoKobalamyne Oct 4, 2023
8fe0d4a
Add pyparsing to CI deps
CyanoKobalamyne Oct 5, 2023
2038490
Fix cvc5 header locations
CyanoKobalamyne Oct 6, 2023
2958f3d
Add new constant kinds to is_value
CyanoKobalamyne Oct 6, 2023
342b59e
Update expected output in printing test
CyanoKobalamyne Oct 19, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion contrib/setup-cvc5.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions cvc5/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion cvc5/include/cvc5_datatype.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@

#pragma once

#include "api/cpp/cvc5.h"
#include "cvc5/cvc5.h"
#include "datatype.h"
#include "exceptions.h"

Expand Down
2 changes: 1 addition & 1 deletion cvc5/include/cvc5_solver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
#include <unordered_set>
#include <vector>

#include "api/cpp/cvc5.h"
#include "cvc5/cvc5.h"
#include "cvc5_datatype.h"
#include "cvc5_sort.h"
#include "cvc5_term.h"
Expand Down
4 changes: 2 additions & 2 deletions cvc5/include/cvc5_sort.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,8 @@

#include <unordered_map>

#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 {
Expand Down
2 changes: 1 addition & 1 deletion cvc5/include/cvc5_term.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@

#pragma once

#include "api/cpp/cvc5.h"
#include "cvc5/cvc5.h"
#include "term.h"
#include "utils.h"

Expand Down
144 changes: 72 additions & 72 deletions cvc5/src/cvc5_solver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,86 +21,86 @@ namespace smt {

/* cvc5 Op mappings */
const std::unordered_map<PrimOp, ::cvc5::Kind> 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 */

Expand Down Expand Up @@ -401,7 +401,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 = Term(new Cvc5Term(carr[1]));
val = Term(new Cvc5Term(carr[2]));
Expand All @@ -410,7 +410,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 = Term(new Cvc5Term(carr.getConstArrayBase()));
}
Expand Down Expand Up @@ -905,7 +905,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 });
}
Expand Down
Loading