/*

  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 <libsmtutil/CHCSmtLib2Interface.h>

#include <libsolutil/Keccak256.h>

#include <boost/algorithm/string/join.hpp>

#include <boost/algorithm/string/predicate.hpp>

#include <range/v3/view.hpp>

#include <array>

#include <fstream>

#include <iostream>

#include <memory>

#include <stdexcept>

using namespace std;

using namespace solidity;

using namespace solidity::util;

using namespace solidity::frontend;

using namespace solidity::smtutil;

CHCSmtLib2Interface::CHCSmtLib2Interface(

  map<h256, string> const& _queryResponses,

  ReadCallback::Callback _smtCallback,

  optional<unsigned> _queryTimeout

):

  CHCSolverInterface(_queryTimeout),

  m_smtlib2(make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),

  m_queryResponses(move(_queryResponses)),

  m_smtCallback(_smtCallback)

{

  reset();

}

void CHCSmtLib2Interface::reset()

{

  m_accumulatedOutput.clear();

  m_variables.clear();

  m_unhandledQueries.clear();

  m_sortNames.clear();

}

void CHCSmtLib2Interface::registerRelation(Expression const& _expr)

{

  smtAssert(_expr.sort);

  smtAssert(_expr.sort->kind == Kind::Function);

  if (!m_variables.count(_expr.name))

  {

    auto fSort = dynamic_pointer_cast<FunctionSort>(_expr.sort);

    string domain = toSmtLibSort(fSort->domain);

    // Relations are predicates which have implicit codomain Bool.

    m_variables.insert(_expr.name);

    write(

      "(declare-fun |" +

      _expr.name +

      "| " +

      domain +

      " Bool)"

    );

  }

}

void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /*_name*/)

{

  write(

    "(assert\n(forall " + forall() + "\n" +

    m_smtlib2->toSExpr(_expr) +

    "))\n\n"

  );

}

tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)

{

  string accumulated{};

  swap(m_accumulatedOutput, accumulated);

  solAssert(m_smtlib2, "");

  writeHeader();

  for (auto const& decl: m_smtlib2->userSorts() | ranges::views::values)

    write(decl);

  m_accumulatedOutput += accumulated;

  string queryRule = "(assert\n(forall " + forall() + "\n" +

    "(=> " + _block.name + " false)"

    "))";

  string response = querySolver(

    m_accumulatedOutput +

    queryRule +

    "\n(check-sat)"

  );

  swap(m_accumulatedOutput, accumulated);

  CheckResult result;

  // TODO proper parsing

  if (boost::starts_with(response, "sat"))

    result = CheckResult::UNSATISFIABLE;

  else if (boost::starts_with(response, "unsat"))

    result = CheckResult::SATISFIABLE;

  else if (boost::starts_with(response, "unknown"))

    result = CheckResult::UNKNOWN;

  else

    result = CheckResult::ERROR;

  return {result, Expression(true), {}};

}

void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)

{

  smtAssert(_sort);

  if (_sort->kind == Kind::Function)

    declareFunction(_name, _sort);

  else if (!m_variables.count(_name))

  {

    m_variables.insert(_name);

    write("(declare-var |" + _name + "| " + toSmtLibSort(*_sort) + ')');

  }

}

string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort)

{

  if (!m_sortNames.count(&_sort))

    m_sortNames[&_sort] = m_smtlib2->toSmtLibSort(_sort);

  return m_sortNames.at(&_sort);

}

string CHCSmtLib2Interface::toSmtLibSort(vector<SortPointer> const& _sorts)

{

  string ssort("(");

  for (auto const& sort: _sorts)

    ssort += toSmtLibSort(*sort) + " ";

  ssort += ")";

  return ssort;

}

void CHCSmtLib2Interface::writeHeader()

{

  if (m_queryTimeout)

    write("(set-option :timeout " + to_string(*m_queryTimeout) + ")");

  write("(set-logic HORN)\n");

}

string CHCSmtLib2Interface::forall()

{

  string vars("(");

  for (auto const& [name, sort]: m_smtlib2->variables())

  {

    solAssert(sort, "");

    if (sort->kind != Kind::Function)

      vars += " (" + name + " " + toSmtLibSort(*sort) + ")";

  }

  vars += ")";

  return vars;

}

void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)

{

  smtAssert(_sort);

  smtAssert(_sort->kind == Kind::Function);

  // TODO Use domain and codomain as key as well

  if (!m_variables.count(_name))

  {

    auto fSort = dynamic_pointer_cast<FunctionSort>(_sort);

    smtAssert(fSort->codomain);

    string domain = toSmtLibSort(fSort->domain);

    string codomain = toSmtLibSort(*fSort->codomain);

    m_variables.insert(_name);

    write(

      "(declare-fun |" +

      _name +

      "| " +

      domain +

      " " +

      codomain +

      ")"

    );

  }

}

void CHCSmtLib2Interface::write(string _data)

{

  m_accumulatedOutput += move(_data) + "\n";

}

string CHCSmtLib2Interface::querySolver(string const& _input)

{

  util::h256 inputHash = util::keccak256(_input);

  if (m_queryResponses.count(inputHash))

    return m_queryResponses.at(inputHash);

  if (m_smtCallback)

  {

    auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);

    if (result.success)

      return result.responseOrErrorMessage;

  }

  m_unhandledQueries.push_back(_input);

  return "unknown\n";

}