mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #9771 from ethereum/refactorInterface
Introduce bitvector sort.
This commit is contained in:
commit
9ced804236
@ -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<BitVectorSort const&>(_sort).size);
|
||||
case Kind::Function:
|
||||
{
|
||||
FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);
|
||||
|
@ -38,11 +38,11 @@ using namespace solidity::frontend;
|
||||
using namespace solidity::smtutil;
|
||||
|
||||
SMTLib2Interface::SMTLib2Interface(
|
||||
map<h256, string> const& _queryResponses,
|
||||
map<h256, string> _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<BitVectorSort const&>(_sort).size) + ")";
|
||||
case Kind::Array:
|
||||
{
|
||||
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
|
||||
|
@ -39,8 +39,8 @@ class SMTLib2Interface: public SolverInterface, public boost::noncopyable
|
||||
{
|
||||
public:
|
||||
explicit SMTLib2Interface(
|
||||
std::map<util::h256, std::string> const& _queryResponses,
|
||||
frontend::ReadCallback::Callback _smtCallback
|
||||
std::map<util::h256, std::string> _queryResponses = {},
|
||||
frontend::ReadCallback::Callback _smtCallback = {}
|
||||
);
|
||||
|
||||
void reset() override;
|
||||
@ -77,7 +77,7 @@ private:
|
||||
std::map<std::string, SortPointer> m_variables;
|
||||
std::set<std::string> m_userSorts;
|
||||
|
||||
std::map<util::h256, std::string> const& m_queryResponses;
|
||||
std::map<util::h256, std::string> m_queryResponses;
|
||||
std::vector<std::string> m_unhandledQueries;
|
||||
|
||||
frontend::ReadCallback::Callback m_smtCallback;
|
||||
|
@ -33,12 +33,12 @@ using namespace solidity::frontend;
|
||||
using namespace solidity::smtutil;
|
||||
|
||||
SMTPortfolio::SMTPortfolio(
|
||||
map<h256, string> const& _smtlib2Responses,
|
||||
frontend::ReadCallback::Callback const& _smtCallback,
|
||||
map<h256, string> _smtlib2Responses,
|
||||
frontend::ReadCallback::Callback _smtCallback,
|
||||
[[maybe_unused]] SMTSolverChoice _enabledSolvers
|
||||
)
|
||||
{
|
||||
m_solvers.emplace_back(make_unique<SMTLib2Interface>(_smtlib2Responses, _smtCallback));
|
||||
m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback)));
|
||||
#ifdef HAVE_Z3
|
||||
if (_enabledSolvers.z3)
|
||||
m_solvers.emplace_back(make_unique<Z3Interface>());
|
||||
|
@ -40,9 +40,9 @@ class SMTPortfolio: public SolverInterface, public boost::noncopyable
|
||||
{
|
||||
public:
|
||||
SMTPortfolio(
|
||||
std::map<util::h256, std::string> const& _smtlib2Responses,
|
||||
frontend::ReadCallback::Callback const& _smtCallback,
|
||||
SMTSolverChoice _enabledSolvers
|
||||
std::map<util::h256, std::string> _smtlib2Responses = {},
|
||||
frontend::ReadCallback::Callback _smtCallback = {},
|
||||
SMTSolverChoice _enabledSolvers = SMTSolverChoice::All()
|
||||
);
|
||||
|
||||
void reset() override;
|
||||
|
@ -35,4 +35,6 @@ shared_ptr<IntSort> SortProvider::intSort(bool _signed)
|
||||
return uintSort;
|
||||
}
|
||||
|
||||
shared_ptr<BitVectorSort> const SortProvider::bitVectorSort{make_shared<BitVectorSort>(256)};
|
||||
|
||||
}
|
||||
|
@ -195,6 +195,7 @@ struct SortProvider
|
||||
static std::shared_ptr<IntSort> const uintSort;
|
||||
static std::shared_ptr<IntSort> const sintSort;
|
||||
static std::shared_ptr<IntSort> intSort(bool _signed = false);
|
||||
static std::shared_ptr<BitVectorSort> const bitVectorSort;
|
||||
};
|
||||
|
||||
}
|
||||
|
@ -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<BitVectorSort const&>(_sort).size);
|
||||
case Kind::Array:
|
||||
{
|
||||
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
|
||||
|
Loading…
Reference in New Issue
Block a user