/*

  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/>.

*/

// SPDX-License-Identifier: GPL-3.0

#pragma once

#include <libsmtutil/Exceptions.h>

#include <libsolutil/Common.h>

#include <memory>

#include <vector>

namespace solidity::smtutil

{

enum class Kind

{

  Int,

  Bool,

  BitVector,

  Function,

  Array,

  Sort,

  Tuple

};

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 IntSort: public Sort

{

  IntSort(bool _signed):

    Sort(Kind::Int),

    isSigned(_signed)

  {}

  bool operator==(Sort const& _other) const override

  {

    if (!Sort::operator==(_other))

      return false;

    auto otherIntSort = dynamic_cast<IntSort const*>(&_other);

    smtAssert(otherIntSort);

    return isSigned == otherIntSort->isSigned;

  }

  bool isSigned;

};

struct BitVectorSort: public Sort

{

  BitVectorSort(unsigned _size):

    Sort(Kind::BitVector),

    size(_size)

  {}

  bool operator==(Sort const& _other) const override

  {

    if (!Sort::operator==(_other))

      return false;

    auto otherBitVectorSort = dynamic_cast<BitVectorSort const*>(&_other);

    smtAssert(otherBitVectorSort);

    return size == otherBitVectorSort->size;

  }

  unsigned size;

};

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);

    smtAssert(_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;

    smtAssert(codomain, "");

    smtAssert(_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);

    smtAssert(_otherArray, "");

    smtAssert(_otherArray->domain, "");

    smtAssert(_otherArray->range, "");

    smtAssert(domain, "");

    smtAssert(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);

    smtAssert(_otherSort, "");

    smtAssert(_otherSort->inner, "");

    smtAssert(inner, "");

    return *inner == *_otherSort->inner;

  }

  SortPointer inner;

};

struct TupleSort: public Sort

{

  TupleSort(

    std::string _name,

    std::vector<std::string> _members,

    std::vector<SortPointer> _components

  ):

    Sort(Kind::Tuple),

    name(std::move(_name)),

    members(std::move(_members)),

    components(std::move(_components))

  {

    for (size_t i = 0; i < members.size(); ++i)

      memberToIndex[members.at(i)] = i;

  }

  SortPointer memberSort(std::string const& _member)

  {

    return components.at(memberToIndex.at(_member));

  }

  bool operator==(Sort const& _other) const override

  {

    if (!Sort::operator==(_other))

      return false;

    auto _otherTuple = dynamic_cast<TupleSort const*>(&_other);

    smtAssert(_otherTuple, "");

    if (name != _otherTuple->name)

      return false;

    if (members != _otherTuple->members)

      return false;

    if (components.size() != _otherTuple->components.size())

      return false;

    if (!std::equal(

      components.begin(),

      components.end(),

      _otherTuple->components.begin(),

      [&](SortPointer _a, SortPointer _b) { return *_a == *_b; }

    ))

      return false;

    return true;

  }

  std::string const name;

  std::vector<std::string> const members;

  std::vector<SortPointer> const components;

  std::map<std::string, size_t> memberToIndex;

};

/** Frequently used sorts.*/

struct SortProvider

{

  static std::shared_ptr<Sort> const boolSort;

  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;

};

}