local_searcher.cpp

#include "engines/local_searcher.h"

#include "engines/options_handler.h"
#include "utils/logger.h"

#include "smt-switch/smtlib_reader.h"
#include "smt/available_solvers.h"

#include <chrono>
#include <filesystem>
#include <cmath>

using namespace smt;

namespace pono {
LocalSearcher::LocalSearcher(const PonoOptions &opt)
  : opt_(opt)
{
  initializeConfig();
}

LocalSearcher::~LocalSearcher(){
  for (auto &option : options_)
    delete option;
  options_.clear();
}

void LocalSearcher::initializeConfig() {
  OptionsHandler::loadOptions(opt_.config_input_, options_);

  sumOfWeights_ = 0;
  for (auto &option : options_) {
    currentConfig_[option] = option->default_value_;
    if (option->weight_)
      sumOfWeights_ += std::pow(WEIGHT_BASE_, option->weight_);
  }

  logger.log(2, "Config initialized");
  dumpCurrentConfig();
}

void LocalSearcher::localSearch(std::string filename, unsigned iterations) {
  logger.log(1, "Optimizing local search for {} iterations (repeat: {})", iterations, opt_.solver_runs_);
  double currentCost = evaluateCurrentConfig(filename, 3);
  double lastAcceptedCost = currentCost;
  acceptCurrentConfig();
  bestConfig_ = currentConfig_; bestIter_ = 0; bestCost_ = currentCost;
  initialCost_ = currentCost;

  printStatus(0, currentCost);

  unsigned printEvery = 5;
  // MCMC Sampling
  for (unsigned iter = 1; iter <= iterations; ++iter) {
    proposeConfigUpdate();
    currentCost = evaluateCurrentConfig(filename, opt_.solver_runs_);
    if (decideToAcceptCurrentProposal(currentCost, lastAcceptedCost)) {
      lastAcceptedCost = currentCost;
      acceptCurrentConfig();
      if (currentCost < bestCost_) {
        bestConfig_ = currentConfig_; bestIter_ = iter; bestCost_ = currentCost;
      }
    }
    if (iter % printEvery == 0)
      printStatus(iter, currentCost);
  }
}

void LocalSearcher::writeBestConfig(std::string filename) {
  logger.log(1, "Writing best configuration to {}", filename);
  logger.log(1, "\tIteration: {}, initial cost: {}, best cost: {}",
             bestIter_, initialCost_, bestCost_);
  std::vector<SolverOption *> options;
  for (const auto &option : options_) {
    options.push_back(new SolverOption
                      (option->option_name_,
                       lastAcceptedConfig_[option],
                       option->values_,
                       option->weight_));
  }
  OptionsHandler::writeOptions(filename, options);
  for (auto &option : options)
    delete option;
}


void LocalSearcher::proposeConfigUpdate() {
  logger.log(2, "Proposing configuration update");
  currentConfig_ = lastAcceptedConfig_;

  // Select an option
  int rnd = (int) rand() % sumOfWeights_;
  SolverOption *option = nullptr;
  for (auto &o : options_) {
    if (o->weight_) {
      int v = std::pow(WEIGHT_BASE_, o->weight_);
      if (rnd < v) {
        option = o;
        break;
      }
      rnd -= v;
    }
  }

  if (option->weight_ == 0) {
    logger.log(0, "Cannot select option with zero weights");
    exit(0);
  }

  // Select a value
  std::string val1 = currentConfig_[option];
  std::string val2 = option->alternative(val1);
  currentConfig_[option] = val2;
  logger.log(2, "Proposed update for {}: {} -> {} ",
             option->option_name_, val1, val2);
}

double LocalSearcher::evaluateCurrentConfig(std::string filename, unsigned solverRuns) {
  logger.log(2, "Evaluating configuration...");

  std::string configStr = currentConfigtoString();
  if (configToCost_.count(configStr)) {
    double score = configToCost_[configStr];
    logger.log(2, "Configuration cached, cost: {}", score);
    return score;
  } else {
    unsigned long long sum = 0;
    unsigned long long runtime;
    for (unsigned i = 0; i < solverRuns; ++i) {
        SmtSolver s = create_solver_for(opt_.smt_solver_,
                                        opt_.engine_,
                                        false,
                                        opt_.ceg_prophecy_arrays_);

        loadConfig(s, currentConfig_);
        SmtLibReader reader(s);
        auto begin = std::chrono::high_resolution_clock::now();
        reader.parse(opt_.filename_);

        auto end = std::chrono::high_resolution_clock::now();

        runtime = std::chrono::duration_cast<std::chrono::milliseconds>(end-begin).count();
        logger.log(2, "\tAttempt {}: cost {}", i, runtime);
        sum += runtime;
    }
    sum /= solverRuns;

    configToCost_[configStr] = sum;
    logger.log(2, "Evaluating configuration - done, cost: {}", sum);
    return sum;
  }
}
void LocalSearcher::loadConfig(smt::SmtSolver &solver,
                               const std::unordered_map<SolverOption *, std::string> &config) const {
  for (const auto &pair : config) {
    solver->set_opt(pair.first->option_name_, pair.second);
  }
}

bool LocalSearcher::decideToAcceptCurrentProposal(double currentCost,
                                                  double lastAcceptedCost) const {
  double mcmcBeta = 1;

  logger.log(2, "Current cost: {}, last accepted cost: {}",
             currentCost, lastAcceptedCost);
  if (currentCost < lastAcceptedCost) {
    logger.log(2, "\tPobability to accept: {}", 1);
    return true;
  } else {
    // The smaller the difference between the proposed phase pattern and the
    // current phase pattern, the more likely to accept the proposal.
    double prob = std::exp(- currentCost / lastAcceptedCost * mcmcBeta);
    logger.log(2, "\tPobability to accept: {}", prob);

    return ((double)rand() / RAND_MAX) < prob;
  }
}

void LocalSearcher::acceptCurrentConfig() {
  lastAcceptedConfig_ = currentConfig_;
  logger.log(2, "\tCurrent configuration accepted");
}

void LocalSearcher::dumpCurrentConfig() const {
  logger.log(0, "Dumping current configuration:");
  for (auto &pair : currentConfig_) {
    std::string s;
    pair.first->dump(s);
    logger.log(0, s);
    logger.log(0, "    current value: {}", pair.second);
  }
}

std::string LocalSearcher::currentConfigtoString() const {
  std::string s = "";
  for (auto &pair : currentConfig_) {
    s += pair.second + ",";
  }
  return s;
}

void LocalSearcher::printStatus(unsigned iter,
                                double currentCost) const {
  logger.log(1, "---- Iteration: {}, current cost: {}, best cost: {} ----\n",
             iter, currentCost, bestCost_);
}


}  // namespace pono