Commit e9fac54b authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

Comments removed, readme update

parent 953b8729
......@@ -146,260 +146,6 @@ parse_arguments(int argc, char *argv[])
conf.amo_encoding = cardinal_opt_group->AmoEncoding();
conf.exone_encoding = cardinal_opt_group->ExOneEncoding();
return conf;
#if 0
cxxopts::Options options(SUBool::kPrgName, SUBool::kPrgDesc);
options.positional_help("[input [output]]");
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",
"Output file with the encoding CNF in DIMACS format",
"Back mapping of variables (names) are used wherever possible",
"Do not check, just write the encoding to the output file",
"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. ",
"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.",
"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 "
"What kind of encoding should be used for empowerment. "
"0 = quadratic encoding with equivalences. "
"1 = quadratic encoding with implications. "
"2 = one level encoding. ",
"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. ",
"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.",
"Aim for unit refutation completeness instead of "
"propagation completeness.",
"Timeout for a single SAT call which looks for an empowering "
"implicate. The timeout is in seconds as a fractional number.",
"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.",
"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.",
"Solver to be used for the PC check. "
"glucose = use glucose, "
"kissat = use kissat.",
"(kissat NOT AVAILABLE).",
"Verbosity level of the log which is written to standard output."
" 0 means no log is written, however messages of glucose can "
"still appear.",
"Which encoding to use for the at-most-one constraint. "
"repr = use the representation, "
"seq = use the sequential encoding.",
"Which encoding to use for the exactly-one constraint. "
"repr = use the representation, "
"split = use the splitting encoding.",
"Positional arguments: these are the arguments that are entered "
"without an option",
options.parse_positional({"input", "output", "positional"});
auto result = options.parse(argc, argv);
if (result.count("help"))
std::cout << << std::endl;
return 1;
if (result.count("version"))
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 << << 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;
conf.enc_conf.up_one_prove =
conf.up_empower =
conf.amo_encoding =
conf.exone_encoding =
conf.impl_system = SUBool::enum_of_name<SUBool::LIT_IMPL_SYSTEM>(
impl_system, SUBool::kImplSystemNames);
if (SUBool::AbsEncoder::AbsConfig::OneProveRequiresImplSystem(
&& 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 (conf.solver_type == SUBool::SOLVER_TYPE::KISSAT)
std::cerr << "Kissat not available" << std::endl;
return 1;
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;
This diff is collapsed.
......@@ -12,17 +12,26 @@ For the compilation the following prerequisities are needed.
- C++17 compiler and a POSIX shell.
- [cmake]( of version at least 3.0.2
- [cxxopts]( -- processing command line
parameters. It is a one header file, needs to be in the include path.
- [glucose]( compiled as a library
(`lib_release.a`) with incremental capabilities. For more details see [glucose](#glucose) subsection below.
- [Boost libraries]( of version at least 1.64.0. Only the
header files are needed for all of the following boost libraries. Some of the
- [Boost libraries]( of version at least 1.64.0. Some of the
boost libraries have their own dependencies within the boost library.
- [Boost Graph Library](
- [Boost Graph Library](,
in this library, only the header files are needed.
- [Boost.Program_options](
is needed as a compiled library.
- (OPTIONAL) [kissat]( -- Kissat solver
for PC checking as an option
for checking propagation completeness as an option
### Options parsing
Until version 2.4, the programs needed library
[cxxopts]( to parse command line
parameters. From version 2.5, this dependence was removed and instead,
is used to parse command line parameters. The disadvantage is that it is needed
as a compiled library, on the other hand, it allows an easy processing of
config files and makes thus easy to use different sets of parameters.
## Compilation
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment