/*
 * Project SUBool
 * Petr Kucera, 2018
 */
/**@file pccompile.cpp
 * Program for PC compilation via adding new empowering implicates.
 */

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

#include "cardinal.h"
#include "cnfcompress.h"
#include "logstream.h"
#include "normalform.h"
#include "pc_opt.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 = "pccompile";
const std::string SUBool::kPrgDesc =
    "compiling a CNF into a propagation complete or unit refutation complete "
    "CNF.";
const std::string prg_help =
    "Implements an incremental algorithm based on adding empowering "
    "implicates and a learning algorithm";

struct config_t
{
   std::string input_file{};
   std::string output_file{};
   bool minimize{false};
   SUBool::MINIMIZE_METHOD minimize_method{SUBool::MINIMIZE_METHOD::FULL};
   SUBool::PCCompAlgorithmOptions::ALGORITHM algorithm{
       SUBool::PCCompAlgorithmOptions::kDefaultAlgorithm};
   bool level_simplify{true};                // simplification at level increase
   unsigned verbosity{3};                    // 0 means no output
   bool use_empty_initial_hypothesis{false}; // For PCLearnComp
   unsigned pccheck_random_rounds{100};
   unsigned pccheck_random_budget{10};
   unsigned pccheck_random_budget_inc{1};
   SUBool::PCLearnComp::INITIAL_NEGATIVES initial_negatives{
       SUBool::PCLearnComp::INITIAL_NEGATIVES::ALL_EMPOWERING};
   unsigned long long random_seed{0};
   double timeout{-1.0};
   SUBool::AbsComp::BaseConfig comp_base_config{
       SUBool::PCEncoder::UP_EMPOWER::ONE_LEVEL,
       50,
       true,
       SUBool::AbsComp::PREPROCESS_METHOD::PRIME_MINIMIZE,
       true,
       SUBool::MINIMIZE_METHOD::FULL,
       SUBool::AbsEncoder::AbsConfig(),
       SUBool::AbsCheckerSAT::Timeouts(),
       true,
       SUBool::LIT_IMPL_SYSTEM::NONE,
       SUBool::SOLVER_TYPE::GLUCOSE,
   };
   bool unfinished_write{true};
   SUBool::AmoEncoder::KIND amo_encoding{SUBool::AmoEncoder::KIND::REPR};
   SUBool::ExOneEncoder::KIND exone_encoding{SUBool::ExOneEncoder::KIND::REPR};

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

std::shared_ptr<SUBool::AbsComp> the_compiler;
config_t the_conf;

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)
       << "\tminimize: " << SUBool::bool_to_string(conf.minimize) << std::endl;
   SUBool::kMinimizeMethodAnnotation.DumpValue(
       "\t", level, "minimize_method", conf.comp_base_config.minimize_method);
   SUBool::PCCompAlgorithmOptions::kAlgorithmAnnotation.DumpValue(
       "\t", level, "algorithm", conf.algorithm);
   SUBool::logs.TLog(level)
       << "\tcomp_base_config.up_empower: "
       << static_cast<unsigned>(conf.comp_base_config.up_empower) << std::endl;
   SUBool::logs.TLog(level)
       << "\tcomp_base_config.simp_steps: " << conf.comp_base_config.simp_steps
       << (conf.comp_base_config.simp_steps > 0
                  ? ""
                  : "(no simplification in intervals)")
       << std::endl;
   SUBool::logs.TLog(level)
       << "\tlevel_simplify: " << (conf.level_simplify ? "yes" : "no")
       << std::endl;
   SUBool::dump_enum_value("\t", level, "comp_base_config.impl_system",
       conf.comp_base_config.impl_system, SUBool::kImplSystemNames);
   SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
   SUBool::logs.TLog(level)
       << "\tcomp_base_config.preprocess: "
       << static_cast<unsigned>(conf.comp_base_config.preprocess) << std::endl;
   SUBool::logs.DumpValue("\t", level, "comp_base_config.propagate_backbones",
       conf.comp_base_config.propagate_backbones);
   SUBool::logs.DumpValue("\t", level, "use_empty_initial_hypothesis",
       conf.use_empty_initial_hypothesis);
   SUBool::logs.TLog(level)
       << "\tpccheck_random_rounds: " << conf.pccheck_random_rounds
       << std::endl;
   SUBool::logs.TLog(level)
       << "\tpccheck_random_budget: " << conf.pccheck_random_budget
       << std::endl;
   SUBool::logs.TLog(level)
       << "\tpccheck_random_budget_inc: " << conf.pccheck_random_budget_inc
       << std::endl;
   SUBool::PCLearnComp::kInitialNegativesAnnotation.DumpValue(
       "\t", level, "initial_negatives", conf.initial_negatives);
   SUBool::logs.TLog(level)
       << "\trandom seed: " << conf.random_seed << std::endl;
   SUBool::logs.TLog(level) << "\ttimeout: " << conf.timeout << std::endl;
   SUBool::logs.TLog(level)
       << "\tcomp_base_config.timeouts.timeout: "
       << conf.comp_base_config.timeouts.timeout << std::endl;
   SUBool::logs.TLog(level)
       << "\tcomp_base_config.timeouts.level_base: "
       << conf.comp_base_config.timeouts.level_base << std::endl;
   SUBool::logs.TLog(level)
       << "\tcomp_base_config.timeouts.level_factor: "
       << conf.comp_base_config.timeouts.level_factor << std::endl;
   SUBool::dump_enum_value("\t", level, "cop_base_config.solver_type",
       conf.comp_base_config.solver_type, SUBool::kSolverTypeNames);
   SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl;
   conf.comp_base_config.enc_conf.Dump("\t\t", level);
   SUBool::AmoEncoder::kKindAnnotation.DumpValue(
       "\t", level, "amo_encoding", conf.amo_encoding);
   SUBool::ExOneEncoder::kKindAnnotation.DumpValue(
       "\t", level, "exone_encoding", conf.exone_encoding);
   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)
{
   SUBool::PrgOptions opts(true);
   opts.SetHelpDesc(prg_help);
   opts.InputOutput(&conf.input_file, &conf.output_file);
   auto algorithm_opts = std::make_shared<SUBool::PCCompAlgorithmOptions>();
   opts.AddOptionsGroup(algorithm_opts);
   auto pclearncomp_opts = std::make_shared<SUBool::PCLearnCompOptions>();
   opts.AddOptionsGroup(pclearncomp_opts);
   if (!opts.Parse(argc, argv))
   {
      return 1;
   }
   conf.algorithm = algorithm_opts->Algorithm();

   conf.use_empty_initial_hypothesis =
       pclearncomp_opts->UseEmptyInitialHypothesis();
   conf.initial_negatives = pclearncomp_opts->InitialNegatives();
   return 0;
#if 0
   try
   {
      cxxopts::Options options("pccompile",
          "pccompile - compiling a CNF into a propagation complete CNF "
          "based on adding empowering implicates.");
      options.positional_help("[input [output]]");
      options.show_positional_help();
      bool uc = false;
      std::string up_one_prove;
      unsigned up_empower = 0;
      unsigned preprocess = 0;
      std::string algorithm;
      bool no_level_simplify = false;
      bool no_backbone_propagation = false;
      unsigned long long seed;
      std::string log_enc_opts;
      std::string initial_negatives;
      std::string amo_encoding;
      std::string exone_encoding;
      std::string minimize_method;
      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))("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.comp_base_config.enc_conf
                                            .up_one_prove))))("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.comp_base_config.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"))(
          "m,minimize", "Minimize the compiled cnf.",
          cxxopts::value<bool>(conf.minimize)
              ->default_value("false"))("minimize-method",
          "Minimization method. Possible values: "
          "full -- full minimization (with the full CNF) "
          "simple_incremental -- sort in increasing order by sizes and then "
          "add nonabsorbed clauses in this sequence, starting with the empty "
          "CNF, the result is not necessarily fully minimized. "
          "full_incremental -- same as simple_incremental, in addition, now "
          "after a specific length of clauses is processed, they are "
          "reprocessed again as in full minimization. Only after then longer "
          "clauses are considered. The result is not necessarily fully "
          "minimized, but it can be significantly smaller than in case of "
          "simple_incremental.",
          cxxopts::value<std::string>(minimize_method)
              ->default_value(SUBool::kMinimizeMethodAnnotation.Name(
                  conf.comp_base_config.minimize_method)))("a,algorithm",
          "The compilation algorithm. "
          "'incremental' -- a heuristic algorithm based on incremental "
          "adding "
          "empowering implicates, allows preprocessing and inprocessing. "
          "This "
          "works in both kinds of goals (PC/UC). "
          "'learning' -- an algorithm based on the algorithm for learning a "
          "Horn formula through equivalence and closure queries (Arias et "
          "al. "
          "2015). This works only for goal PC. If goal is UC, the program "
          "ends "
          "with error. Other parameters are used appropriately.",
          cxxopts::value<std::string>(algorithm)->default_value(
              algorithm_names[static_cast<unsigned>(
                  conf.algorithm)]))("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.comp_base_config.enc_conf.up_level_bound)
              ->default_value(std::to_string(
                  conf.comp_base_config.enc_conf.up_level_bound)))("u,uc",
          "Aim for unit refutation completeness instead of "
          "propagation completeness.",
          cxxopts::value<bool>(uc)->default_value("false"))("interleave-pc",
          "In case of compilation to UC, "
          "interleave encodings for UC and PC.",
          cxxopts::value<bool>(conf.uc_interleave_pc)
              ->default_value("false"))("use-empty-initial-hypothesis",
          "Use empty initial hypothesis in the learning algorithm. If not "
          "set, "
          "the preprocessed input CNF is used as an initial hypothesis.",
          cxxopts::value<bool>(conf.use_empty_initial_hypothesis)
              ->default_value("false"))("pccheck-random-rounds",
          "Number of rounds during one random check of PC.",
          cxxopts::value<unsigned>(conf.pccheck_random_rounds)
              ->default_value(std::to_string(
                  conf.pccheck_random_rounds)))("pccheck-random-budget",
          "How many times unsucessful random PC check should be repeated. 0 "
          "means no random check is ever performed.",
          cxxopts::value<unsigned>(conf.pccheck_random_budget)
              ->default_value(std::to_string(
                  conf.pccheck_random_budget)))("pccheck-random-budget-inc",
          "Increase of the current budget in case a random negative example "
          "was successfully found. 0 "
          "means no increase.",
          cxxopts::value<unsigned>(conf.pccheck_random_budget_inc)
              ->default_value(std::to_string(
                  conf.pccheck_random_budget_inc)))("initial-negatives",
          "How the initial negative examples in the learning algorithm "
          "should be produced. The option specifies how the negatives for each "
          "clause in the preprocessed CNF are created. For a clause C, the "
          "possible options are as follows: "
          "'single_empowering' - Only one negative is produced (C without a "
          "literal with respect to which C is empowering), "
          "'all' - All negatives are produced (C without l fo every literal "
          "l in C), "
          "'all_empowering' - For every literal l in C if C is empowering "
          "with respect to l, then C without l is produced."
          "'gd_basis' - GD basis of the dual rail encoding of the "
          "prepreocessed CNF is computed, the bodies in the GD basis are used "
          "as an initial list of negatives."
          "'body_minimal' - body minimal representation for the dual rail "
          "encoding of the preprocessed CNF is computed. The bodies in this "
          "representation are used as an initial list of negatives.",
          cxxopts::value<std::string>(initial_negatives)
              ->default_value(
                  SUBool::PCLearnComp::cInitialNegativesNames[static_cast<
                      unsigned>(conf.initial_negatives)]))("s,simp-steps",
          "Number of empowering clauses after which a heuristic "
          "simplification of the current formula proceeds. Zero (0) means that "
          "no simplification is made during the compilation. However final "
          "minimization shall proceed depending on presence of -m option.",
          cxxopts::value<unsigned>(conf.comp_base_config.simp_steps)
              ->default_value(std::to_string(
                  conf.comp_base_config.simp_steps)))("no-level-simplify",
          "Do not perform simplification when the number of levels of unit "
          "propagation increases.",
          cxxopts::value<bool>(no_level_simplify)
              ->default_value("false"))("r,preprocess",
          "Method of preprocessing. "
          "0 = No preprocessing. "
          "1 = Minimize the formula before compilation. "
          "2 = First make CNF prime with respect to 1-provability, then "
          "minimize. "
          "3 = First make CNF prime and then minimize. "
          "4 = Only make CNF prime with respect to 1-provability, no "
          "minimization. "
          "5 = Only make CNF prime, no minimization. ",
          cxxopts::value<unsigned>(preprocess)
              ->default_value(std::to_string(static_cast<unsigned>(
                  conf.comp_base_config
                      .preprocess))))("no-backbone-propagation",
          "Do not perform backbone propagation before preprocessing.",
          cxxopts::value<bool>(no_backbone_propagation)
              ->default_value("false"))("S,seed",
          "Initial random seed. Current time is used, if the seed is not "
          "provided explicitly.",
          cxxopts::value<unsigned long long>(seed))("t,timeout",
          "Timeout for compilation in seconds as a fractional number. "
          "After this amount of seconds, the process finishes. Value "
          "t<=0.0 means no timeout. The timer uses CLOCK_REALTIME.",
          cxxopts::value<double>(conf.timeout)
              ->default_value(std::to_string(conf.timeout)))("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.comp_base_config.timeouts.timeout)
              ->default_value(
                  std::to_string(conf.comp_base_config.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.comp_base_config.timeouts.level_base)
              ->default_value(
                  std::to_string(conf.comp_base_config.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.comp_base_config.timeouts.level_factor)
              ->default_value(
                  std::to_string(conf.comp_base_config.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.comp_base_config.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)))("positional",
          "Positional arguments: these are the arguments that are entered "
          "without an option",
          cxxopts::value<std::vector<std::string>>())("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)));
      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);
         std::cout << std::endl;
         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.random_seed =
          (result.count("seed") > 0 ? seed
                                    : std::chrono::system_clock::now()
                                          .time_since_epoch()
                                          .count());
      conf.goal = (uc ? GOAL::UC : GOAL::PC);
      conf.level_simplify = !no_level_simplify;
      conf.comp_base_config.propagate_backbones = !no_backbone_propagation;
      if (!parse_log_enc_opts(
              log_enc_opts, conf.comp_base_config.enc_conf.log_conf))
      {
         std::cerr << "Error parsing logarithmic encoding options" << std::endl;
         return 1;
      }
      try
      {
         conf.comp_base_config.enc_conf.up_one_prove =
             SUBool::AbsEncoder::ParseUPOneProve(up_one_prove);
         conf.comp_base_config.up_empower =
             SUBool::enum_of_int<SUBool::PCEncoder::UP_EMPOWER>(up_empower);
         conf.comp_base_config.preprocess =
             SUBool::enum_of_int<SUBool::AbsIncrementalComp::PREPROCESS_METHOD>(
                 preprocess);
         conf.algorithm =
             SUBool::enum_of_name<ALGORITHM>(algorithm, algorithm_names);
         conf.initial_negatives =
             SUBool::enum_of_name<SUBool::PCLearnComp::INITIAL_NEGATIVES>(
                 initial_negatives,
                 SUBool::PCLearnComp::cInitialNegativesNames);
         conf.amo_encoding =
             SUBool::AmoEncoder::kKindAnnotation.Parse(amo_encoding);
         conf.exone_encoding =
             SUBool::ExOneEncoder::kKindAnnotation.Parse(exone_encoding);
         conf.comp_base_config.minimize_method =
             SUBool::kMinimizeMethodAnnotation.Parse(minimize_method);
         conf.comp_base_config.impl_system =
             SUBool::enum_of_name<SUBool::LIT_IMPL_SYSTEM>(
                 impl_system, SUBool::kImplSystemNames);
         if (SUBool::AbsEncoder::AbsConfig::OneProveRequiresImplSystem(
                 conf.comp_base_config.enc_conf.up_one_prove)
             && conf.comp_base_config.impl_system
                    == SUBool::LIT_IMPL_SYSTEM::NONE)
         {
            conf.comp_base_config.impl_system = SUBool::kDefaultImplSystem;
         }
         conf.comp_base_config.solver_type =
             SUBool::enum_of_name<SUBool::SOLVER_TYPE>(
                 solver_type, SUBool::kSolverTypeNames);
#if !HAS_KISSAT
         if (conf.comp_base_config.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;
#endif
}

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

void
fill_base_conf(SUBool::AbsComp::BaseConfig &out_conf, const config_t &conf)
{
   out_conf = conf.comp_base_config;
   out_conf.final_simplify = conf.minimize;
   out_conf.level_simplify = conf.level_simplify;
}

// std::unique_ptr<SUBool::AbsIncrementalComp>
std::shared_ptr<SUBool::AbsIncrementalComp>
incremental_compiler(const config_t &conf, SUBool::CNF cnf)
{
   SUBool::AbsComp::BaseConfig a_conf;
   fill_base_conf(a_conf, conf);
   bool interleave_pc = false;

   switch (conf.algorithm)
   {
   case SUBool::PCCompAlgorithmOptions::ALGORITHM::INCREMENT_PC:
      return std::make_shared<SUBool::PCComp>(
          std::move(cnf), std::move(a_conf));
   case SUBool::PCCompAlgorithmOptions::ALGORITHM::INCREMENT_URC_PC:
      interleave_pc = true;
      [[fallthrough]];
   case SUBool::PCCompAlgorithmOptions::ALGORITHM::INCREMENT_URC:
   {
      SUBool::UCComp::Config uc_conf(a_conf);
      uc_conf.interleave_pc = interleave_pc;
      return std::make_shared<SUBool::UCComp>(
          std::move(cnf), std::move(uc_conf));
   }
   default:
      throw SUBool::BadParameterException(
          "compiler", "Bad algorithm specification");
   }
}

std::shared_ptr<SUBool::PCLearnComp>
learning_compiler(const config_t &conf, SUBool::CNF cnf)
{
   SUBool::PCLearnComp::Config l_conf;
   fill_base_conf(l_conf, conf);
   l_conf.use_empty_initial_hypothesis = conf.use_empty_initial_hypothesis;
   l_conf.pccheck_random_rounds = conf.pccheck_random_rounds;
   l_conf.pccheck_random_budget = conf.pccheck_random_budget;
   l_conf.pccheck_random_budget_inc = conf.pccheck_random_budget_inc;
   l_conf.initial_negatives = conf.initial_negatives;
   return std::make_shared<SUBool::PCLearnComp>(
       std::move(cnf), std::move(l_conf));
}

std::shared_ptr<SUBool::AbsComp>
compiler(const config_t &conf, SUBool::CNF cnf)
{
   if (conf.algorithm == SUBool::PCCompAlgorithmOptions::ALGORITHM::LEARNING)
   {
      return learning_compiler(conf, std::move(cnf));
   }
   return incremental_compiler(conf, std::move(cnf));
}

int
write_output()
{
   if (!the_compiler)
   {
      SUBool::logs.TLog(1)
          << "[write_output] the_compiler is nullptr, no output written"
          << std::endl;
   }
   try
   {
      std::stringstream ss;
      SUBool::print_version(ss, true);
      output(the_conf.output_file, the_compiler->CurrentCNF(), ss.str());
   }
   catch (SUBool::IOException &e)
   {
      SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::NONE)
          << "[write_output]" << e.what() << std::endl;
      return 2;
   }
   return 0;
}

int
compile(SUBool::CNF cnf)
{
   auto comp = compiler(the_conf, std::move(cnf));
   the_compiler = comp;
   auto fut = std::async(
       std::launch::async,
       [](std::shared_ptr<SUBool::AbsComp> comp) { return comp->Compile(); },
       comp);
   auto res = wait_with_timeout(the_conf.timeout, fut, *comp);
   if (res == SUBool::AbsComp::RESULT::COMPILED || the_conf.unfinished_write)
   {
      return write_output();
   }
   SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::MINLINES)
       << "No output written" << std::endl;
   return 1;
}

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

void
terminate(int signal)
{
   std::stringstream ss;
   ss << "terminated by signal " << signal;
   if (the_compiler)
   {
      the_compiler->Abort(ss.str());
      the_compiler->PrintStatistics(1);
      if (the_conf.unfinished_write)
      {
         write_output();
      }
      else
      {
         SUBool::logs.TLog(3) << "c No output written" << std::endl;
      }
   }
   _Exit(2);
}

int
main(int argc, char *argv[])
{
   int r = parse_arguments(argc, argv, the_conf);
   if (r != 0)
   {
      return r;
   }
   SUBool::CNF cnf;
   r = input(the_conf, &cnf);
   if (r != 0)
   {
      return r;
   }
   SUBool::sub_rand.seed(the_conf.random_seed);

   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(the_conf, 3);
   return 0;
#if 0
   SUBool::AmoEncoder::sGlobalKind = the_conf.amo_encoding;
   SUBool::ExOneEncoder::sGlobalKind = the_conf.exone_encoding;
   auto ret = compile(std::move(cnf));
   the_compiler = nullptr;
   return ret;
#endif
}