/*
 * Project SUBool
 * Petr Kucera, 2018
 */
/**@file pccheck.cpp
 * Program for checking if a formula is PC or URC. Can also be used to get the
 * CNF encoding PC/URC property.
 */

#include <array>
#include <chrono>
#include <csignal>
#include <ctime>
#include <fstream>
#include <future>
#include <iostream>

#include <cxxopts.hpp>

#include "cardinal.h"
#include "cnfcompress.h"
#include "logstream.h"
#include "normalform.h"
#include "pccomp.h"
#include "pcenc.h"
#include "pclearncomp.h"
#include "prgutil.h"
#include "random_utils.h"
#include "resolve.h"
#include "uccomp.h"
#include "ucenc.h"
#include "unitprop.h"

const std::string SUBool::kPrgName = "pccheck";
const std::string SUBool::kPrgDesc = "Checking if a CNF is PC or URC";
const std::string prg_help =
    "Checks if a given CNF is propagation complete (PC) or unit refutation "
    "complete (URC). Can also output the SAT encoding of the required query.";

enum class GOAL
{
   PC,
   UC
};

struct config_t
{
   std::string input_file{};
   std::string output_file{};
   bool encode_only{false};
   unsigned verbosity{3}; // 0 means no output
   bool no_up_backbones{false};
   SUBool::PCEncoder::UP_EMPOWER up_empower{
       SUBool::PCEncoder::UP_EMPOWER::ONE_LEVEL};
   SUBool::AbsEncoder::AbsConfig enc_conf{};
   SUBool::AbsCheckerSAT::Timeouts timeouts{};
   SUBool::LIT_IMPL_SYSTEM impl_system{SUBool::LIT_IMPL_SYSTEM::NONE};
   GOAL goal{GOAL::PC};
   SUBool::AmoEncoder::KIND amo_encoding{SUBool::AmoEncoder::KIND::REPR};
   SUBool::ExOneEncoder::KIND exone_encoding{SUBool::ExOneEncoder::KIND::REPR};
   SUBool::SOLVER_TYPE solver_type{SUBool::SOLVER_TYPE::GLUCOSE};

   config_t()
   {
      enc_conf.up_one_prove = SUBool::AbsEncoder::UP_ONE_PROVE::MIN_LQ;
      enc_conf.log_conf.literal_levels = false;
      enc_conf.log_conf.split_size = 4;
      enc_conf.log_conf.use_bit_level = false;
      enc_conf.log_conf.add_amo_on_fire_vars = true;
      enc_conf.log_conf.add_compare_exclusivity = true;
      enc_conf.log_conf.add_force_linear_order_on_max_level = true;
      enc_conf.log_conf.contradiction_has_max_level = true;
      enc_conf.min_lq_log_weights = {2.0, 2.0, 0.0};
      enc_conf.min_lq_quad_weights = {1.0, 1.0, 0.0};
      timeouts.timeout = -1.0;
      timeouts.level_base = -1.0;
      timeouts.level_factor = 0.0;
   };
};

constexpr const char *
goal_name(const config_t &conf)
{
   return (conf.goal == GOAL::PC ? "PC" : "URC");
}

void
dump_config(const config_t &conf, unsigned level)
{
   SUBool::logs.TLog(level) << "Configuration:" << std::endl;
   SUBool::logs.TLog(level) << "\tinput_file: " << conf.input_file << std::endl;
   SUBool::logs.TLog(level)
       << "\toutput_file: " << conf.output_file << std::endl;
   SUBool::logs.TLog(level)
       << "\tencode_only: " << SUBool::bool_to_string(conf.encode_only)
       << std::endl;
   SUBool::logs.DumpValue("\t", level, "no_up_backbones", conf.no_up_backbones);
   SUBool::logs.TLog(level)
       << "\tup_empower: " << static_cast<unsigned>(conf.up_empower)
       << std::endl;
   SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl;
   conf.enc_conf.Dump("\t\t", level);
   SUBool::logs.TLog(level)
       << "\ttimeouts.timeout: " << conf.timeouts.timeout << std::endl;
   SUBool::logs.TLog(level)
       << "\ttimeouts.level_base: " << conf.timeouts.level_base << std::endl;
   SUBool::logs.TLog(level)
       << "\ttimeouts.level_factor: " << conf.timeouts.level_factor
       << std::endl;
   SUBool::dump_enum_value(
       "\t", level, "impl_system", conf.impl_system, SUBool::kImplSystemNames);
   SUBool::logs.TLog(level) << "\tgoal: " << goal_name(conf) << std::endl;
   SUBool::AmoEncoder::kKindAnnotation.DumpValue(
       "\t", level, "amo_encoding", conf.amo_encoding);
   SUBool::ExOneEncoder::kKindAnnotation.DumpValue(
       "\t", level, "exone_encoding", conf.exone_encoding);
   SUBool::dump_enum_value(
       "\t", level, "solver_type", conf.solver_type, SUBool::kSolverTypeNames);
   SUBool::logs.TLog(level) << "END" << std::endl;
}

std::vector<std::string> log_enc_opt_strings = {"amf", "cex", "flm", "cml"};

bool
parse_log_enc_opts(
    const std::string &opt_string, SUBool::UPEncLogarithmic::Config &conf)
{
   std::vector<bool> opt_values(log_enc_opt_strings.size(), false);
   size_t start = 0;
   size_t end = 0;
   if (!opt_string.empty())
   {
      while (start != std::string::npos)
      {
         end = opt_string.find_first_of(',', start);
         auto i = std::find(log_enc_opt_strings.begin(),
             log_enc_opt_strings.end(), opt_string.substr(start, end - start));
         if (i == log_enc_opt_strings.end())
         {
            return false;
         }
         opt_values[i - log_enc_opt_strings.begin()] = true;
         start = end + static_cast<size_t>(end < std::string::npos);
      }
   }
   conf.add_amo_on_fire_vars = opt_values[0];
   conf.add_compare_exclusivity = opt_values[1];
   conf.add_force_linear_order_on_max_level = opt_values[2];
   conf.contradiction_has_max_level = opt_values[3];
   return true;
}

int
parse_arguments(int argc, char *argv[], config_t &conf)
{
   try
   {
      cxxopts::Options options(SUBool::kPrgName, SUBool::kPrgDesc);
      options.positional_help("[input [output]]");
      options.show_positional_help();
      bool uc = false;
      std::string up_one_prove;
      unsigned up_empower = 0;
      std::string algorithm;
      std::string log_enc_opts;
      std::string amo_encoding;
      std::string exone_encoding;
      std::string impl_system;
      std::string solver_type;
      options.add_options()("h,help", "Print help")(
          "v,version", "Print version info")("i,input",
          "Input file with a CNF in DIMACS format",
          cxxopts::value<std::string>(conf.input_file))("o,output",
          "Output file with the encoding CNF in DIMACS format",
          cxxopts::value<std::string>(conf.output_file))("d,dump",
          "Back mapping of variables (names) are used wherever possible",
          cxxopts::value<bool>(conf.enc_conf.use_backmap)
              ->default_value("false"))("e,encode",
          "Do not check, just write the encoding to the output file",
          cxxopts::value<bool>(conf.encode_only)
              ->default_value("false"))("1,one-prove",
          "What kind of encoding should be used for 1-provability. It is "
          "possible to specify the value with a number or a string. The list "
          "below contains a string value with a number within the brackets."
          "quadratic_equiv (0) = quadratic encoding with equivalences. "
          "quadratic_one_sided (1) = quadratic encoding with implications. "
          "logarithmic (2) = logarithmic encoding. "
          "max_level (3) = max based encoding. "
          "min_lq (4) = the smaller one from quadratic encoding with "
          "implications and the logarithmic encoding, the choice is made "
          "before each SAT call."
          "quad_impl_system (5) = quadratic which uses an implication system "
          "to represent dual "
          "rail encoding, the implication system type is determined by option "
          "--impl-system. "
          "impl_level (6) = based on implication system where levels are "
          "encoded in binary, "
          "the implication system type is determined by option --impl-system. "
          "scc_unary (7) = based on the SCCs of implication system, unary "
          "encoding of levels. "
          "scc_binary (8) = based on the SCCs of implication system, binary "
          "encoding of levels. ",
          cxxopts::value<std::string>(up_one_prove)
              ->default_value(
                  SUBool::AbsEncoder::kUPOneProveNames.at(static_cast<unsigned>(
                      conf.enc_conf.up_one_prove))))("n,no-up-backbones",
          "Do NOT perform propagation of literals which can be derived by unit "
          "propagation from the input formula. This is useful for checking the "
          "construction of an encoding.",
          cxxopts::value<bool>(conf.no_up_backbones)
              ->default_value("false"))("log-enc-opts",
          "Options to logarithmic encoding modifying some of its features. "
          "It "
          "is a string composed of comma separated option strings which "
          "specifies which additional parts should be added to the "
          "encoding. "
          "Possible values specifying the features are: "
          "amf -- AMO on fire variables for each derived literal will be "
          "part "
          "of the encoding. "
          "cex -- Comparison exclusivity clauses will be added to the "
          "encoding. "
          "flm -- Clauses forcing linear order when the number of levels is "
          "maximum will be added to the encoding. "
          "cml -- A variable is contradictory if and only its level has all "
          "ones.",
          cxxopts::value<std::string>(log_enc_opts)
              ->default_value(std::string("amf,cex,flm,cml")))("w,empower",
          "What kind of encoding should be used for empowerment. "
          "0 = quadratic encoding with equivalences. "
          "1 = quadratic encoding with implications. "
          "2 = one level encoding. ",
          cxxopts::value<unsigned>(up_empower)
              ->default_value(std::to_string(
                  static_cast<unsigned>(conf.up_empower))))("impl-system",
          "Determines the type of an implication system to be used when "
          "required by encoding of empowerement or 1-provability. "
          "'none' -- no implication system (must not be used with any choice "
          "of "
          "one-prove and empower options which requires an implication system. "
          "Should be used with other option combinations. "
          "'drenc' -- use plain dual rail encoding. "
          "'irredundant' -- make the dual rail encoding irredundant (both body "
          "and right). "
          "'gdbasis' -- use GD basis of the dual rail encoding. "
          "'gdbasis_right_irred' -- construct GD basis and make it right "
          "irredundant. "
          "'body_minimal' -- make the dual rail encoding body minimal (like GD "
          "basis but without left saturation). "
          "'body_minimal_irred' -- make the dual rail encoding body minimal "
          "and right irredundant. "
          "The default value depends on other options, it is none for the "
          "combination of options one-prove and empower which do not require "
          "any implication system, and "
              + SUBool::DefaultImplSystemName()
              + " for the option combination which needs an implication "
                "system. ",
          cxxopts::value<std::string>(impl_system)->default_value("none"))(
          "l,level",
          "Maximum level of unit propagation for "
          "1-provability. In case of compilation, the compilation "
          "stops when no empowering implicate with level at most l is "
          "found. Value 0 means, the level is not bounded. Note that "
          "in case of quadratic encoding this is really the maximum "
          "level, in case of logarithmic encoding this is the number "
          "of bits used to encode a number of level. In case of choice -1 "
          "4 "
          "when the minimum of quadratic and logarithmic encoding is "
          "considered, the level bounds the number of level of the "
          "quadratic "
          "encoding while the number of levels of the logarithmic encoding "
          "is "
          "bounded to the logarithm of the parameter rounded up.",
          cxxopts::value<unsigned>(conf.enc_conf.up_level_bound)
              ->default_value(
                  std::to_string(conf.enc_conf.up_level_bound)))("u,uc",
          "Aim for unit refutation completeness instead of "
          "propagation completeness.",
          cxxopts::value<bool>(uc)->default_value("false"))("emp-timeout",
          "Timeout for a single SAT call which looks for an empowering "
          "implicate. The timeout is in seconds as a fractional number.",
          cxxopts::value<double>(conf.timeouts.timeout)
              ->default_value(std::to_string(
                  conf.timeouts.timeout)))("emp-timeout-level-base",
          "This parameter together with emp-timeout-level-factor allows to "
          "set the timeout for a single SAT which looks for an empowering "
          "implicate depending on the number of levels of unit propagation "
          "allowed in the encoding. Denote the value of "
          "emp-timeout-level-base "
          "as B and the value of emp-timeout-level-factor as F. For a "
          "level L which is neither 0 nor maximum (i.e. the number of "
          "variables), the timeout is set as B+F*L. If the value is higher "
          "than emp-timeout, then the value of emp-timeout is used instead. "
          "The timeout is passed as a fractional number specifying the number "
          "of seconds.",
          cxxopts::value<double>(conf.timeouts.level_base)
              ->default_value(std::to_string(
                  conf.timeouts.level_base)))("emp-timeout-level-factor",
          "This parameter together with emp-timeout-level-base allows to "
          "set the timeout for a single SAT which looks for an empowering "
          "implicate depending on the number of levels of unit propagation "
          "allowed in the encoding (see the description of "
          "emp-timeout-level-base for more details). If the value is "
          "higher "
          "than emp-timeout, then the value of emp-timeout is used "
          "instead. "
          "The timeout is passed as a fractional number specifying the "
          "number of seconds.",
          cxxopts::value<double>(conf.timeouts.level_factor)
              ->default_value(
                  std::to_string(conf.timeouts.level_factor)))("pccheck-solver",
          "Solver to be used for the PC check. "
          "glucose = use glucose, "
#if HAS_KISSAT
          "kissat = use kissat.",
#else
          "(kissat NOT AVAILABLE).",
#endif
          cxxopts::value<std::string>(solver_type)
              ->default_value(SUBool::kSolverTypeNames[static_cast<unsigned>(
                  conf.solver_type)]))("b,verbosity",
          "Verbosity level of the log which is written to standard output."
          " 0 means no log is written, however messages of glucose can "
          "still appear.",
          cxxopts::value<unsigned>(conf.verbosity)
              ->default_value(std::to_string(conf.verbosity)))("amo",
          "Which encoding to use for the at-most-one constraint. "
          "repr = use the representation, "
          "seq = use the sequential encoding.",
          cxxopts::value<std::string>(amo_encoding)
              ->default_value(SUBool::AmoEncoder::kKindAnnotation.Name(
                  conf.amo_encoding)))("exactly-one",
          "Which encoding to use for the exactly-one constraint. "
          "repr = use the representation, "
          "split = use the splitting encoding.",
          cxxopts::value<std::string>(exone_encoding)
              ->default_value(SUBool::ExOneEncoder::kKindAnnotation.Name(
                  conf.exone_encoding)))("positional",
          "Positional arguments: these are the arguments that are entered "
          "without an option",
          cxxopts::value<std::vector<std::string>>());
      options.parse_positional({"input", "output", "positional"});
      auto result = options.parse(argc, argv);
      if (result.count("help"))
      {
         std::cout << options.help() << std::endl;
         return 1;
      }
      if (result.count("version"))
      {
         SUBool::print_version(std::cout);
         return 1;
      }
      if (result.count("positional"))
      {
         std::cerr << "Multiple files passed as parameters, ";
         std::cerr << "only input and output are allowed" << std::endl;
         std::cerr << options.help() << std::endl;
         return 1;
      }
      conf.goal = (uc ? GOAL::UC : GOAL::PC);
      if (!parse_log_enc_opts(log_enc_opts, conf.enc_conf.log_conf))
      {
         std::cerr << "Error parsing logarithmic encoding options" << std::endl;
         return 1;
      }
      try
      {
         conf.enc_conf.up_one_prove =
             SUBool::AbsEncoder::ParseUPOneProve(up_one_prove);
         conf.up_empower =
             SUBool::enum_of_int<SUBool::PCEncoder::UP_EMPOWER>(up_empower);
         conf.amo_encoding =
             SUBool::AmoEncoder::kKindAnnotation.Parse(amo_encoding);
         conf.exone_encoding =
             SUBool::ExOneEncoder::kKindAnnotation.Parse(exone_encoding);
         conf.impl_system = SUBool::enum_of_name<SUBool::LIT_IMPL_SYSTEM>(
             impl_system, SUBool::kImplSystemNames);
         if (SUBool::AbsEncoder::AbsConfig::OneProveRequiresImplSystem(
                 conf.enc_conf.up_one_prove)
             && conf.impl_system == SUBool::LIT_IMPL_SYSTEM::NONE)
         {
            conf.impl_system = SUBool::kDefaultImplSystem;
         }
         conf.solver_type = SUBool::enum_of_name<SUBool::SOLVER_TYPE>(
             solver_type, SUBool::kSolverTypeNames);
#if !HAS_KISSAT
         if (conf.solver_type == SUBool::SOLVER_TYPE::KISSAT)
         {
            std::cerr << "Kissat not available" << std::endl;
            return 1;
         }
#endif
      }
      catch (SUBool::BadParameterException &e)
      {
         std::cerr << "Error parsing parameter values: " << e.what()
                   << std::endl;
         return 1;
      }
   }
   catch (const cxxopts::OptionException &e)
   {
      std::cerr << "Error parsing options: " << e.what() << std::endl;
      return 1;
   }
   return 0;
}

int
input(const config_t &conf, SUBool::CNF *cnf)
{
   if (cnf == nullptr)
   {
      throw SUBool::NullPointerException("input", "cnf == nullptr");
   }

   if (conf.input_file.empty() || conf.input_file == "-")
   {
      std::cin >> *cnf;
   }
   else
   {
      std::ifstream in(conf.input_file);
      if (!in)
      {
         std::cerr << "Failed to open file '" << conf.input_file
                   << "' for reading" << std::endl;
         return 2;
      }
      in >> *cnf;
   }
   return 0;
}

template <class T, class R>
R
wait_with_timeout(double timeout, std::future<R> &fut, T &comp)
{
   if (timeout > 0.0)
   {
      if (fut.wait_for(std::chrono::duration<double>(timeout))
          == std::future_status::timeout)
      {
         comp.Abort("timed out");
         comp.PrintStatistics(1);
         fut.wait();
         return SUBool::AbsComp::RESULT::TIMED_OUT; //_Exit(3);
      }
   }
   else
   {
      fut.wait();
   }
   return fut.get();
}

int
encode(const config_t &conf, const SUBool::CompHypothesis &hyp,
    SUBool::AbsCheckerSAT &checker)
{
   auto cnf = hyp.GetHypothesis(false);
   auto enc = checker.Encoder(conf.enc_conf.up_level_bound);
   SUBool::ClausesToLiterals cl2lit(cnf);
   SUBool::LitImplSystem impl_system;
   SUBool::LitISGraph scc_graph;
   if (enc->RequiresImplSystem())
   {
      impl_system = SUBool::init_lit_impl_system(cnf, conf.impl_system);
      if (enc->RequiresSCCGraph())
      {
         scc_graph = SUBool::LitISGraph(impl_system);
      }
   }
   enc->BuildEncoding(cnf, cl2lit, impl_system, scc_graph);
   SUBool::OutputStream os(conf.output_file);
   if (!os)
   {
      SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::NONE)
          << "[encode] Failed to open file '" << conf.output_file
          << "' for writing" << std::endl;
      return 2;
   }
   enc->WriteEncoding(os);
   return 0;
}

const std::string kPCEmpoweringImplicateName = "empowering implicate";
const std::string kUCEmpoweringImplicateName = "URC empowering implicate";
const std::string kPCEmpoweringVarName = "empowering variable";
const std::string kUCEmpoweringVarName = "extending variable";

const std::string &
empowering_implicate_name(const config_t &conf)
{
   switch (conf.goal)
   {
   case GOAL::PC:
      return kPCEmpoweringImplicateName;
   case GOAL::UC:
      return kUCEmpoweringImplicateName;
   default:
      throw SUBool::BadParameterException(
          "empowering_implicate_name", "Bad goal");
   }
}

const std::string &
empowering_variable_name(const config_t &conf)
{
   switch (conf.goal)
   {
   case GOAL::PC:
      return kPCEmpoweringVarName;
   case GOAL::UC:
      return kUCEmpoweringVarName;
   default:
      throw SUBool::BadParameterException(
          "empowering_variable_name", "Bad goal");
   }
}

int
empower(const config_t &conf, SUBool::CompHypothesis &hyp,
    SUBool::AbsCheckerSAT &checker)
{
   auto emp_result = hyp.FindEmpowering(checker, false);
   if (emp_result)
   {
      auto emp_var = checker.LastWitnessVariable();
      // TODO: change the last parameter to true if consistency is checked
      // before calling empower
      auto clause = hyp.PrimeSubimplicate(*emp_result, emp_var, false);
      SUBool::logs.TLog(1) << "Found empowering implicate " << clause
                           << " with empowered variable " << emp_var
                           << std::endl;
      return 1;
   }
   SUBool::logs.TLog(1) << "No empowering implicate found, formula is "
                        << goal_name(conf) << " complete" << std::endl;
   return 0;
}

void
terminate(int signal)
{
   std::stringstream ss;
   ss << "terminated by signal " << signal;
   _Exit(2);
}

std::unique_ptr<SUBool::PCCheckerSAT>
pc_checker_sat(const config_t &conf)
{
   auto checker = std::make_unique<SUBool::PCCheckerSAT>();
   SUBool::PCEncoder::Config check_conf(conf.enc_conf);
   check_conf.up_empower = conf.up_empower;
   checker->Init(check_conf, false, conf.timeouts);
   checker->SetSolverType(conf.solver_type);
   return checker;
}

std::unique_ptr<SUBool::UCCheckerSAT>
urc_checker_sat(const config_t &conf)
{
   auto checker = std::make_unique<SUBool::UCCheckerSAT>();
   checker->Init(conf.enc_conf, false, conf.timeouts);
   checker->SetSolverType(conf.solver_type);
   return checker;
}

std::unique_ptr<SUBool::AbsCheckerSAT>
checker_sat(const config_t &conf)
{
   switch (conf.goal)
   {
   case GOAL::PC:
      return pc_checker_sat(conf);
   case GOAL::UC:
      return urc_checker_sat(conf);
   default:
      throw SUBool::BadParameterException("checker_sat", "Unknown goal");
   }
}

int
execute(const config_t &conf, SUBool::CNF cnf)
{
   auto repr = cnf;
   SUBool::CompHypothesis hyp(SUBool::MINIMIZE_METHOD::FULL, conf.impl_system,
       std::move(cnf), std::move(repr), true);
   if (!conf.no_up_backbones)
   {
      hyp.PropagateUPBackbones();
   }
   auto checker = checker_sat(conf);
   if (conf.encode_only)
   {
      return encode(conf, hyp, *checker);
   }
   return empower(conf, hyp, *checker);
}

int
main(int argc, char *argv[])
{
   config_t conf;
   int r = parse_arguments(argc, argv, conf);
   if (r != 0)
   {
      return r;
   }
   SUBool::logs.mVerbLevel = conf.verbosity;
   SUBool::CNF cnf;
   r = input(conf, &cnf);
   if (r != 0)
   {
      return r;
   }

   std::signal(SIGTERM, terminate);
   std::signal(SIGQUIT, terminate);
   std::signal(SIGINT, terminate);

   SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::MINLINES)
       << "PCCompile " << SUBool::kVersionInfo << std::endl;

   dump_config(
       conf, static_cast<unsigned>(SUBool::LogStream::LOG_LEVEL::MINLINES));
   SUBool::AmoEncoder::sGlobalKind = conf.amo_encoding;
   SUBool::ExOneEncoder::sGlobalKind = conf.exone_encoding;
   auto ret = execute(conf, std::move(cnf));
   return ret;
}