Solver option in some other programs

bin/cnfcanon.cpp

@@ -21,6 +21,7 @@
 #include "normalform.h"
 #include "prgutil.h"
 #include "sbexception.h"
+#include "solver_opt.h"
 
 const std::string SUBool::kPrgName = "cnfcanon";
 const std::string SUBool::kPrgDesc =
@@ -59,6 +60,7 @@ parse_arguments(int argc, char *argv[])
    std::string process;
    SUBool::PrgOptions opts;
    opts.InputOutput(&conf.input_file, &conf.output_file);
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
    po::options_description desc("Configuration options");
    desc.add(opt_process);
    opts.Add(desc);
@@ -72,6 +74,7 @@ parse_arguments(int argc, char *argv[])
 void
 config_t::InnerDump(unsigned level) const
 {
+   SUBool::SolverPool::DumpSolverTypes("\t", level);
    SUBool::logs.DumpValue("\t", level, "input_file", input_file);
    SUBool::logs.DumpValue("\t", level, "output_file", output_file);
    kProcessAnnotation.DumpValue("\t", level, "process", process);

bin/cnfprime.cpp

@@ -20,6 +20,7 @@
 #include "normalform.h"
 #include "prgutil.h"
 #include "sbexception.h"
+#include "solver_opt.h"
 
 const std::string SUBool::kPrgName = "cnfprime";
 const std::string SUBool::kPrgDesc = "Making a CNF prime";
@@ -43,6 +44,7 @@ parse_arguments(int argc, char *argv[])
    SUBool::PrgOptions opts;
    opts.SetHelpDesc(prg_help);
    opts.InputOutput(&conf.input_file, &conf.output_file);
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
    po::options_description desc("Configuration options");
    desc.add_options()("unitprop,u", po::bool_switch(&conf.unitprop),
        "Use only unit propagation instead of SAT. It means "
@@ -63,6 +65,7 @@ parse_arguments(int argc, char *argv[])
 void
 config_t::InnerDump(unsigned level) const
 {
+   SUBool::SolverPool::DumpSolverTypes("\t", level);
    SUBool::logs.DumpValue("\t", level, "input_file", input_file);
    SUBool::logs.DumpValue("\t", level, "output_file", output_file);
    SUBool::logs.DumpValue("\t", level, "unitprop", unitprop);

bin/dpelim.cpp

@@ -15,6 +15,7 @@
 #include "enum_opt.h"
 #include "logstream.h"
 #include "prgutil.h"
+#include "solver_opt.h"
 
 const std::string SUBool::kPrgName = "dpelim";
 const std::string SUBool::kPrgDesc = "DP elimination of variables";
@@ -55,6 +56,7 @@ struct config_t : public SUBool::PrgConfigBase
 void
 config_t::InnerDump(unsigned level) const
 {
+   SUBool::SolverPool::DumpSolverTypes("\t", level);
    SUBool::logs.DumpValue("\t", level, "input_file", input_file);
    SUBool::logs.DumpValue("\t", level, "output_file", output_file);
    SUBool::logs.DumpValue("\t", level, "max_input_var", max_input_var);
@@ -87,6 +89,7 @@ parse_arguments(int argc, char *argv[])
    opts.InputOutput(&conf.input_file, &conf.output_file);
    opts.SetHelpDesc(prg_help);
 
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
    auto elim_opts = opts.MakeOptionsGroup<SUBool::DPElimEliminationOptions>();
    auto clause_manip_opts =
        opts.MakeOptionsGroup<SUBool::DPElimClauseManipOptions>();

bin/nnfencode.cpp

@@ -17,6 +17,7 @@
 #include "enum_opt.h"
 #include "logstream.h"
 #include "prgutil.h"
+#include "solver_opt.h"
 
 const std::string SUBool::kPrgName = "nnfencode";
 const std::string SUBool::kPrgDesc =
@@ -70,6 +71,7 @@ struct config_t : public SUBool::PrgConfigBase
 void
 config_t::InnerDump(unsigned level) const
 {
+   SUBool::SolverPool::DumpSolverTypes("\t", level);
    SUBool::logs.DumpValue("\t", level, "input_file", input_file);
    SUBool::logs.DumpValue("\t", level, "output_file", output_file);
    kEncodingTypeAnnotation.DumpValue(
@@ -105,6 +107,7 @@ parse_arguments(int argc, char *argv[])
    SUBool::PrgOptions opts(true);
    opts.SetHelpDesc(kPrgHelp);
    opts.InputOutput(&conf.input_file, &conf.output_file);
+   auto solver_opts = opts.MakeOptionsGroup<SUBool::SolverOptions>();
    po::options_description desc("Encoding construction");
    desc.add(opt_encoding_type);
    desc.add(opt_level_func);