mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
126 lines
3.1 KiB
C++
126 lines
3.1 KiB
C++
/*
|
|
This file is part of solidity.
|
|
|
|
solidity is free software: you can redistribute it and/or modify
|
|
it under the terms of the GNU General Public License as published by
|
|
the Free Software Foundation, either version 3 of the License, or
|
|
(at your option) any later version.
|
|
|
|
solidity is distributed in the hope that it will be useful,
|
|
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
GNU General Public License for more details.
|
|
|
|
You should have received a copy of the GNU General Public License
|
|
along with solidity. If not, see <http://www.gnu.org/licenses/>.
|
|
*/
|
|
|
|
#pragma once
|
|
|
|
#include <liblangutil/Exceptions.h>
|
|
#include <libsolutil/Common.h>
|
|
#include <libsolutil/Exceptions.h>
|
|
|
|
#include <memory>
|
|
#include <vector>
|
|
|
|
namespace solidity::frontend::smt
|
|
{
|
|
|
|
enum class Kind
|
|
{
|
|
Int,
|
|
Bool,
|
|
Function,
|
|
Array,
|
|
Sort
|
|
};
|
|
|
|
struct Sort
|
|
{
|
|
Sort(Kind _kind):
|
|
kind(_kind) {}
|
|
virtual ~Sort() = default;
|
|
virtual bool operator==(Sort const& _other) const { return kind == _other.kind; }
|
|
|
|
Kind const kind;
|
|
};
|
|
using SortPointer = std::shared_ptr<Sort>;
|
|
|
|
struct FunctionSort: public Sort
|
|
{
|
|
FunctionSort(std::vector<SortPointer> _domain, SortPointer _codomain):
|
|
Sort(Kind::Function), domain(std::move(_domain)), codomain(std::move(_codomain)) {}
|
|
bool operator==(Sort const& _other) const override
|
|
{
|
|
if (!Sort::operator==(_other))
|
|
return false;
|
|
auto _otherFunction = dynamic_cast<FunctionSort const*>(&_other);
|
|
solAssert(_otherFunction, "");
|
|
if (domain.size() != _otherFunction->domain.size())
|
|
return false;
|
|
if (!std::equal(
|
|
domain.begin(),
|
|
domain.end(),
|
|
_otherFunction->domain.begin(),
|
|
[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
|
|
))
|
|
return false;
|
|
solAssert(codomain, "");
|
|
solAssert(_otherFunction->codomain, "");
|
|
return *codomain == *_otherFunction->codomain;
|
|
}
|
|
|
|
std::vector<SortPointer> domain;
|
|
SortPointer codomain;
|
|
};
|
|
|
|
struct ArraySort: public Sort
|
|
{
|
|
/// _domain is the sort of the indices
|
|
/// _range is the sort of the values
|
|
ArraySort(SortPointer _domain, SortPointer _range):
|
|
Sort(Kind::Array), domain(std::move(_domain)), range(std::move(_range)) {}
|
|
bool operator==(Sort const& _other) const override
|
|
{
|
|
if (!Sort::operator==(_other))
|
|
return false;
|
|
auto _otherArray = dynamic_cast<ArraySort const*>(&_other);
|
|
solAssert(_otherArray, "");
|
|
solAssert(_otherArray->domain, "");
|
|
solAssert(_otherArray->range, "");
|
|
solAssert(domain, "");
|
|
solAssert(range, "");
|
|
return *domain == *_otherArray->domain && *range == *_otherArray->range;
|
|
}
|
|
|
|
SortPointer domain;
|
|
SortPointer range;
|
|
};
|
|
|
|
struct SortSort: public Sort
|
|
{
|
|
SortSort(SortPointer _inner): Sort(Kind::Sort), inner(std::move(_inner)) {}
|
|
bool operator==(Sort const& _other) const override
|
|
{
|
|
if (!Sort::operator==(_other))
|
|
return false;
|
|
auto _otherSort = dynamic_cast<SortSort const*>(&_other);
|
|
solAssert(_otherSort, "");
|
|
solAssert(_otherSort->inner, "");
|
|
solAssert(inner, "");
|
|
return *inner == *_otherSort->inner;
|
|
}
|
|
|
|
SortPointer inner;
|
|
};
|
|
|
|
/** Frequently used sorts.*/
|
|
struct SortProvider
|
|
{
|
|
static std::shared_ptr<Sort> const boolSort;
|
|
static std::shared_ptr<Sort> const intSort;
|
|
};
|
|
|
|
}
|