From a2cac93cbf0a39674a36ca77020c47231357e54b Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 11 May 2020 19:56:29 +0200 Subject: [PATCH] Introduce bitvector sort. --- libsmtutil/CVC4Interface.cpp | 2 ++ libsmtutil/SMTLib2Interface.cpp | 8 +++++--- libsmtutil/SMTLib2Interface.h | 6 +++--- libsmtutil/SMTPortfolio.cpp | 6 +++--- libsmtutil/SMTPortfolio.h | 6 +++--- libsmtutil/Sorts.cpp | 2 ++ libsmtutil/Sorts.h | 1 + libsmtutil/Z3Interface.cpp | 2 ++ 8 files changed, 21 insertions(+), 12 deletions(-) diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp index 40526306f..bd0300136 100644 --- a/libsmtutil/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -289,6 +289,8 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort) return m_context.booleanType(); case Kind::Int: return m_context.integerType(); + case Kind::BitVector: + return m_context.mkBitVectorType(dynamic_cast(_sort).size); case Kind::Function: { FunctionSort const& fSort = dynamic_cast(_sort); diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index f1d21c2cc..e1bc7d0b4 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -38,11 +38,11 @@ using namespace solidity::frontend; using namespace solidity::smtutil; SMTLib2Interface::SMTLib2Interface( - map const& _queryResponses, + map _queryResponses, ReadCallback::Callback _smtCallback ): - m_queryResponses(_queryResponses), - m_smtCallback(std::move(_smtCallback)) + m_queryResponses(move(_queryResponses)), + m_smtCallback(move(_smtCallback)) { reset(); } @@ -215,6 +215,8 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort) return "Int"; case Kind::Bool: return "Bool"; + case Kind::BitVector: + return "(_ BitVec " + to_string(dynamic_cast(_sort).size) + ")"; case Kind::Array: { auto const& arraySort = dynamic_cast(_sort); diff --git a/libsmtutil/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h index 2a43c0441..4c21b1f1c 100644 --- a/libsmtutil/SMTLib2Interface.h +++ b/libsmtutil/SMTLib2Interface.h @@ -39,8 +39,8 @@ class SMTLib2Interface: public SolverInterface, public boost::noncopyable { public: explicit SMTLib2Interface( - std::map const& _queryResponses, - frontend::ReadCallback::Callback _smtCallback + std::map _queryResponses = {}, + frontend::ReadCallback::Callback _smtCallback = {} ); void reset() override; @@ -77,7 +77,7 @@ private: std::map m_variables; std::set m_userSorts; - std::map const& m_queryResponses; + std::map m_queryResponses; std::vector m_unhandledQueries; frontend::ReadCallback::Callback m_smtCallback; diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index 334d91dd7..9858247a1 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -33,12 +33,12 @@ using namespace solidity::frontend; using namespace solidity::smtutil; SMTPortfolio::SMTPortfolio( - map const& _smtlib2Responses, - frontend::ReadCallback::Callback const& _smtCallback, + map _smtlib2Responses, + frontend::ReadCallback::Callback _smtCallback, [[maybe_unused]] SMTSolverChoice _enabledSolvers ) { - m_solvers.emplace_back(make_unique(_smtlib2Responses, _smtCallback)); + m_solvers.emplace_back(make_unique(move(_smtlib2Responses), move(_smtCallback))); #ifdef HAVE_Z3 if (_enabledSolvers.z3) m_solvers.emplace_back(make_unique()); diff --git a/libsmtutil/SMTPortfolio.h b/libsmtutil/SMTPortfolio.h index 3e933df5d..e4a662203 100644 --- a/libsmtutil/SMTPortfolio.h +++ b/libsmtutil/SMTPortfolio.h @@ -40,9 +40,9 @@ class SMTPortfolio: public SolverInterface, public boost::noncopyable { public: SMTPortfolio( - std::map const& _smtlib2Responses, - frontend::ReadCallback::Callback const& _smtCallback, - SMTSolverChoice _enabledSolvers + std::map _smtlib2Responses = {}, + frontend::ReadCallback::Callback _smtCallback = {}, + SMTSolverChoice _enabledSolvers = SMTSolverChoice::All() ); void reset() override; diff --git a/libsmtutil/Sorts.cpp b/libsmtutil/Sorts.cpp index 303e8bb84..543c7ba0f 100644 --- a/libsmtutil/Sorts.cpp +++ b/libsmtutil/Sorts.cpp @@ -35,4 +35,6 @@ shared_ptr SortProvider::intSort(bool _signed) return uintSort; } +shared_ptr const SortProvider::bitVectorSort{make_shared(256)}; + } diff --git a/libsmtutil/Sorts.h b/libsmtutil/Sorts.h index de94e8fff..45668f269 100644 --- a/libsmtutil/Sorts.h +++ b/libsmtutil/Sorts.h @@ -195,6 +195,7 @@ struct SortProvider static std::shared_ptr const uintSort; static std::shared_ptr const sintSort; static std::shared_ptr intSort(bool _signed = false); + static std::shared_ptr const bitVectorSort; }; } diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index 909a5cde2..c1d0be7c8 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -245,6 +245,8 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort) return m_context.bool_sort(); case Kind::Int: return m_context.int_sort(); + case Kind::BitVector: + return m_context.bv_sort(dynamic_cast(_sort).size); case Kind::Array: { auto const& arraySort = dynamic_cast(_sort);