/*

  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

#include <libsolidity/formal/EncodingContext.h>

#include <libsolidity/formal/Predicate.h>

#include <libsolidity/formal/SymbolicVariables.h>

#include <libsmtutil/Sorts.h>

#include <vector>

namespace solidity::frontend

{

/**

 * Contains the set of rules to compute an array slice.

 * Rules:

 * 1. end > start => ArraySliceHeader(a, b, start, end, 0)

 * 2. ArraySliceHeader(a, b, start, end, i) && i >= (end - start) => ArraySlice(a, b, start, end)

 * 3. ArraySliceHeader(a, b, start, end, i) && i >= 0 && i < (end - start) => ArraySliceLoop(a, b, start, end, i)

 * 4. ArraySliceLoop(a, b, start, end, i) && b[i] = a[start + i] => ArraySliceHeader(a, b, start, end, i + 1)

 *

 * The rule to be used by CHC is ArraySlice(a, b, start, end).

 */

struct ArraySlicePredicate

{

  /// Contains the predicates and rules created to compute

  /// array slices for a given sort.

  struct SliceData

  {

    std::vector<Predicate const*> predicates;

    std::vector<smtutil::Expression> rules;

  };

  /// @returns a flag representing whether the array slice predicates had already been created before for this sort,

  /// and the corresponding slice data.

  static std::pair<bool, SliceData const&> create(smtutil::SortPointer _sort, smt::EncodingContext& _context);

  static void reset() { m_slicePredicates.clear(); }

private:

  /// Maps a unique sort name to its slice data.

  static std::map<std::string, SliceData> m_slicePredicates;

};

}