Skip to content

Commit

Permalink
Merge branch 'master' into add-strings
Browse files Browse the repository at this point in the history
  • Loading branch information
@ntsis
ntsis authored Oct 27, 2023
2 parents 88a943f + 25ead08 commit c0f950f
Show file tree
Hide file tree
Showing 13 changed files with 189 additions and 182 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
View file
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
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
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
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
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
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
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
152 changes: 76 additions & 76 deletions cvc5/src/cvc5_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,90 +21,90 @@ 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 },
{ StrLt, ::cvc5::STRING_LT },
{ StrLeq, ::cvc5::STRING_LEQ },
{ StrLen, ::cvc5::STRING_LENGTH },
{ StrConcat, ::cvc5::STRING_CONCAT },
{ 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 },
{ StrLt, ::cvc5::Kind::STRING_LT },
{ StrLeq, ::cvc5::Kind::STRING_LEQ },
{ StrLen, ::cvc5::Kind::STRING_LENGTH },
{ StrConcat, ::cvc5::Kind::STRING_CONCAT },
{ 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 @@ -459,7 +459,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 @@ -468,7 +468,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 @@ -967,7 +967,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

0 comments on commit c0f950f

Please sign in to comment.