Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Kučera Petr RNDr. Ph.D.
PCCompile
Commits
042376c3
Commit
042376c3
authored
Aug 03, 2021
by
Kučera Petr RNDr. Ph.D.
Browse files
gdbasis program options
parent
9e7632fb
Changes
2
Hide whitespace changes
Inline
Side-by-side
bin/dpelim.cpp
View file @
042376c3
...
...
@@ -115,134 +115,6 @@ parse_arguments(int argc, char *argv[])
conf
.
minimize_size_step
=
minimize_opts
.
SizeStep
();
conf
.
minimize_size_factor
=
minimize_opts
.
SizeFactor
();
#if 0
cxxopts::Options options(SUBool::kPrgName, prg_help);
options.positional_help("[input [output]]");
std::string encoding_type;
bool eliminate_all = false;
long double factor = 0.0;
unsigned max_increase = 0;
std::string ignore_policy;
std::string inprocessing;
std::string increase_policy;
std::string block_prime;
options.add_options()("h,help", "Print help")(
"v,version", "Print version info")("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(SUBool::LogStream::kMaxLogLevels))("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))("x,max-input-var",
"Maximum input variable. Up to this variable no variable is "
"eliminated",
cxxopts::value<unsigned>(conf.max_input_var)
->default_value("0"))("f,eliminate-factor",
"Perform elimination of auxiliary variables and allow increase of "
"the number of clauses by a given factor",
cxxopts::value<long double>(factor))("s,eliminate-size-increase",
"Perform elimination of auxiliary variables and allow increase of "
"the number of clauses by at most a given number (additively).",
cxxopts::value<unsigned >(max_increase))("c,increase-policy",
"How the size bound should be checked. "
"estimate = stop when the estimate of increase gets over the bound, "
"bound = stop when the size got over the bound, "
"new = stop when the current number of new clauses gets over the "
"bound, "
"new_total = stop when the total number of new clauses gets over the "
"bound.",
cxxopts::value<std::string>(increase_policy)
->default_value(elim_increase_policy_names.at(
static_cast<unsigned>(conf.elim.increase_policy))))("m,minimize",
"Perform minimization at the end (not needed with -M option).",
cxxopts::value<bool>(conf.final_minimize)
->default_value("false"))("M,elim-minimize",
"Use minimization during elimination.",
cxxopts::value<bool>(conf.elim.use_minimize)
->default_value("false"))("elim-minimize-step",
"Size increase step between two minimizations.",
cxxopts::value<unsigned >(conf.elim.minimize_size_step)
->default_value(std::to_string(
conf.elim.minimize_size_step)))("elim-minimize-factor",
"Factor of the cnf size to be added to the minimize step.",
cxxopts::value<double>(conf.elim.minimize_size_factor)
->default_value(
std::to_string(conf.elim.minimize_size_factor)))("P,block-prime",
"Make new clauses prime after each block of DP elimination. Possible "
"values: "
"none = cnf is not made prime, "
"up_prime = use unit propagation for primality, "
"prime = use SAT for primality.",
cxxopts::value<std::string>(block_prime)
->default_value("none"))("g,ignore-policy",
"Which resolvents should be discarded during auxiliary variable "
"elimination. "
"none = do not discard any resolvents, "
"implicate = discard the clauses which are implicates of others, "
"absorbed = discard the abosrbed clauses (not empowering)",
cxxopts::value<std::string>(ignore_policy)
->default_value(elim_ignore_policy_names.at(
static_cast<unsigned>(conf.elim.ignore_policy))))("p,process",
"how to inprocess the resolvent during auxiliary variable "
"elimination. "
"none = no inprocessing, "
"prime = find prime subimplicate",
cxxopts::value<std::string>(inprocessing)
->default_value(elim_inprocessing_names.at(
static_cast<unsigned>(conf.elim.inprocessing))));
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"))
{
SUBool::logs.TLog(0) << "Multiple files passed as parameters, ";
SUBool::logs.TLog(0) << "only input and output are allowed" << std::endl;
SUBool::logs.TLog(0) << options.help() << std::endl;
return 1;
}
if (eliminate_all)
{
conf.elim.eliminate = ELIMINATE::ALL;
}
else if (result.count("f") > 0)
{
conf.elim.eliminate = ELIMINATE::FACTOR;
conf.elim.factor = factor;
}
else if (result.count("s") > 0)
{
conf.elim.eliminate = ELIMINATE::MAX_INCREASE;
conf.elim.max_increase = max_increase;
}
try
{
conf.elim.ignore_policy =
SUBool::enum_of_name<SUBool::DPEliminator::IGNORE_POLICY>(
ignore_policy, elim_ignore_policy_names);
conf.elim.inprocessing =
SUBool::enum_of_name<SUBool::DPEliminator::INPROCESSING>(
inprocessing, elim_inprocessing_names);
conf.elim.increase_policy =
SUBool::enum_of_name<SUBool::DPEliminator::INCREASE_POLICY>(
increase_policy, elim_increase_policy_names);
conf.elim.block_prime =
SUBool::enum_of_name<SUBool::CNFEncoding::BLOCK_PRIME>(
block_prime, block_prime_names);
}
#endif
return
conf
;
}
...
...
bin/gdbasis.cpp
View file @
042376c3
...
...
@@ -5,45 +5,60 @@
/*@file gdhorn.cpp
* Program computing the GD basis of a given definite Horn CNF
*/
#include <cxxopts.hpp>
#include "cpuutil.h"
#include "drenc.h"
#include "enum_opt.h"
#include "horn.h"
#include "prgutil.h"
const
std
::
string
SUBool
::
kPrgName
=
"gd
horn
"
;
const
std
::
string
SUBool
::
kPrgName
=
"gd
basis
"
;
const
std
::
string
SUBool
::
kPrgDesc
=
"Program computing the GD basis of a given definite Horn CNF"
;
enum
class
I
mplType
enum
class
I
MPL_TYPE
{
HORN
,
DUAL_RAIL
,
Last
=
DUAL_RAIL
};
const
std
::
array
<
std
::
string
,
static_cast
<
size_t
>
(
ImplType
::
Last
)
+
1
>
impl_type_names
{
"horn"
,
"dual_rail"
};
const
SUBool
::
EnumAnnotation
<
IMPL_TYPE
>
kImplTypeAnnotation
(
"IMPL_TYPE"
,
{
//
{
IMPL_TYPE
::
HORN
,
"horn"
,
"the input is a definite Horn CNF describing an implicational "
"system whose basis should be computed"
},
//
{
IMPL_TYPE
::
DUAL_RAIL
,
"dual_rail"
,
"the input is a general CNF. The basis should be constructed for "
"the dual rail encoding of the input CNF."
}});
const
IMPL_TYPE
kDefaultImplType
=
IMPL_TYPE
::
DUAL_RAIL
;
enum
class
O
utputType
enum
class
O
UTPUT_TYPE
{
IMPLICATIONS
,
CNF
,
Last
=
CNF
};
const
std
::
array
<
std
::
string
,
static_cast
<
size_t
>
(
OutputType
::
Last
)
+
1
>
output_type_names
{
"implications"
,
"cnf"
};
const
SUBool
::
EnumAnnotation
<
OUTPUT_TYPE
>
kOutputTypeAnnotation
(
"OUTPUT_TYPE"
,
{
//
{
OUTPUT_TYPE
::
IMPLICATIONS
,
"implications"
,
"output consists of a list of implications"
},
{
OUTPUT_TYPE
::
CNF
,
"cnf"
,
"output is a CNF after projecting the implications back to "
"clauses"
}});
const
OUTPUT_TYPE
kDefaultOutputType
=
OUTPUT_TYPE
::
IMPLICATIONS
;
const
std
::
string
kDefaultSeparator
=
":"
;
struct
config_t
{
std
::
string
input_file
{};
std
::
string
output_file
{};
unsigned
verbosity
{
3
};
// 0 means no output
ImplType
impl_type
{
ImplType
::
DUAL_RAIL
};
OutputType
output_type
{
OutputType
::
IMPLICATIONS
};
std
::
string
impl_sep
{
":"
};
IMPL_TYPE
impl_type
{
kDefaultImplType
};
OUTPUT_TYPE
output_type
{
kDefaultOutputType
};
std
::
string
impl_sep
{
kDefaultSeparator
};
bool
keep_body_in_closure
{
false
};
// Closure of the empty body should be part of
// both the body and cons at the and
...
...
@@ -60,11 +75,10 @@ dump_config(const config_t &conf, unsigned level)
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"input_file"
,
conf
.
input_file
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"output_file"
,
conf
.
output_file
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"verbosity"
,
conf
.
verbosity
);
SUBool
::
dump_enum_value
(
"
\t
"
,
level
,
"impl_type"
,
conf
.
impl_type
,
impl_type_names
);
SUBool
::
dump_enum_value
(
"
\t
"
,
level
,
"output_type"
,
conf
.
output_type
,
output_type_names
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"verbosity"
,
SUBool
::
logs
.
mVerbLevel
);
kImplTypeAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"impl_type"
,
conf
.
impl_type
);
kOutputTypeAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"output_type"
,
conf
.
output_type
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"impl_sep"
,
conf
.
impl_sep
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"keep_body_in_closure"
,
conf
.
keep_body_in_closure
);
...
...
@@ -75,108 +89,58 @@ dump_config(const config_t &conf, unsigned level)
"
\t
"
,
level
,
"right_irredundant"
,
conf
.
right_irredundant
);
}
int
parse_arguments
(
int
argc
,
char
*
argv
[]
,
config_t
&
conf
)
std
::
optional
<
config_t
>
parse_arguments
(
int
argc
,
char
*
argv
[])
{
try
{
cxxopts
::
Options
options
(
SUBool
::
kPrgName
,
SUBool
::
kPrgDesc
);
options
.
positional_help
(
"[input-left [input-right]]"
);
std
::
string
check_kind
;
std
::
string
impl_type
;
std
::
string
output_type
;
options
.
add_options
()(
"h,help"
,
"Print help"
)(
"v,version"
,
"Print version info"
)(
"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
(
SUBool
::
LogStream
::
kMaxLogLevels
))(
"i,input"
,
"Input file with a definite Horn CNF in DIMACS format"
,
cxxopts
::
value
<
std
::
string
>
(
conf
.
input_file
))(
"o,output"
,
"Output file with the GD basis"
,
cxxopts
::
value
<
std
::
string
>
(
conf
.
output_file
))(
"I,impl-type"
,
"The type of the implications in the system: "
"'horn' -- the input is a definite Horn CNF describing an "
"implicational system whose basis should be computed. "
"'dual_rail' -- the input is a general CNF. The basis should be "
"constructed for the dual rail encoding of the input CNF."
,
cxxopts
::
value
<
std
::
string
>
(
impl_type
)
->
default_value
(
impl_type_names
[
static_cast
<
unsigned
>
(
conf
.
impl_type
)]))(
"O,output-type"
,
"The type of the output: "
"'implications' -- the implications should be written. "
"'cnf' -- CNF after projecting the implications back to clauses. "
,
cxxopts
::
value
<
std
::
string
>
(
output_type
)
->
default_value
(
output_type_names
[
static_cast
<
unsigned
>
(
conf
.
output_type
)]))(
"s,impl-sep"
,
"String which separates the consequence part from the body in the "
"implications output type"
,
cxxopts
::
value
<
std
::
string
>
(
conf
.
impl_sep
)
->
default_value
(
conf
.
impl_sep
))(
"k,keep-body-in-closure"
,
"whether the body should be part of the closure in the output basis"
,
cxxopts
::
value
<
bool
>
(
conf
.
keep_body_in_closure
)
->
default_value
(
"false"
))(
"e,omit-empty-closure"
,
"whether the closure of the empty body should be omitted from the "
"bodies and consequences in the implications"
,
cxxopts
::
value
<
bool
>
(
conf
.
omit_empty_closure
)
->
default_value
(
"false"
))(
"m,body-minimal"
,
"compute only body minimal representation, i.e. do not use "
"left-saturation, options keep-body-in-closure and "
"omit-empty-closure are ignored in this case"
,
cxxopts
::
value
<
bool
>
(
conf
.
body_minimal
)
->
default_value
(
"false"
))(
"r,right-irredundant"
,
"make the implication system right irredundant at the end, options "
"keep-body-in-closure and omit-empty-closure are ignored in this "
"case, however left saturation can proceed if not suppressed by "
"option body-minimal."
,
cxxopts
::
value
<
bool
>
(
conf
.
right_irredundant
)
->
default_value
(
"false"
));
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
;
}
try
{
conf
.
impl_type
=
SUBool
::
enum_of_name
<
ImplType
>
(
impl_type
,
impl_type_names
);
conf
.
output_type
=
SUBool
::
enum_of_name
<
OutputType
>
(
output_type
,
output_type_names
);
}
catch
(
SUBool
::
BadParameterException
&
e
)
{
std
::
cerr
<<
"Error parsing parameter values: "
<<
e
.
what
()
<<
std
::
endl
;
return
1
;
}
if
(
result
.
count
(
"positional"
))
{
SUBool
::
logs
.
TLog
(
0
)
<<
"Multiple files passed as parameters, "
<<
"only input and output files are allowed"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
0
)
<<
options
.
help
()
<<
std
::
endl
;
return
1
;
}
SUBool
::
logs
.
mVerbLevel
=
conf
.
verbosity
;
}
catch
(
const
cxxopts
::
OptionException
&
e
)
config_t
conf
;
auto
opt_impl_type
=
SUBool
::
make_enum_option
(
kImplTypeAnnotation
,
"impl-type,I"
,
"Specifies how the input implications are derived from the input CNF."
,
kDefaultImplType
);
auto
opt_output_type
=
SUBool
::
make_enum_option
(
kOutputTypeAnnotation
,
"output-type,O"
,
"Type of the output."
,
kDefaultOutputType
);
SUBool
::
PrgOptions
opts
(
true
);
opts
.
InputOutput
(
&
conf
.
input_file
,
&
conf
.
output_file
);
po
::
options_description
input_opts
(
"Input system"
);
input_opts
.
add
(
opt_impl_type
);
opts
.
Add
(
input_opts
);
po
::
options_description
output_opts
(
"Output system"
);
output_opts
.
add
(
opt_output_type
);
output_opts
.
add_options
()
//
(
"impl-sep,s"
,
po
::
value
<
std
::
string
>
(
&
conf
.
impl_sep
)
->
default_value
(
kDefaultSeparator
),
"String which separates the consequence part from the body in the "
"implications output type"
)
//
(
"keep-body-in-closure,k"
,
po
::
bool_switch
(
&
conf
.
keep_body_in_closure
),
"if present, the body will be part of the closure in the output "
"basis, otherwise, body is subtracted from the closure"
)
//
(
"omit-empty-closure,e"
,
po
::
bool_switch
(
&
conf
.
omit_empty_closure
),
"if present, the closure of the empty body will be omitted from the "
"bodies and consequences in the implications. Otherwise, the "
"closure of the empty body is part of every set of consequences and "
"every body (in case of left saturation)."
)
//
(
"body-minimal,m"
,
po
::
bool_switch
(
&
conf
.
body_minimal
),
"compute only body minimal representation, i.e. do not use "
"left-saturation, options keep-body-in-closure and "
"omit-empty-closure are ignored in this case"
)
//
(
"right-irredundant,r"
,
po
::
bool_switch
(
&
conf
.
right_irredundant
),
"make the implication system right irredundant at the end, options "
"keep-body-in-closure and omit-empty-closure are ignored in this "
"case, however left saturation is performed if not suppressed by "
"option body-minimal."
);
opts
.
Add
(
output_opts
);
if
(
!
opts
.
Parse
(
argc
,
argv
)
||
!
opt_impl_type
.
GetValue
(
conf
.
impl_type
)
||
!
opt_output_type
.
GetValue
(
conf
.
output_type
))
{
std
::
cerr
<<
"Error parsing options: "
<<
e
.
what
()
<<
std
::
endl
;
return
1
;
return
{};
}
if
(
conf
.
right_irredundant
||
conf
.
body_minimal
)
{
conf
.
omit_empty_closure
=
true
;
conf
.
keep_body_in_closure
=
false
;
}
return
0
;
return
conf
;
}
template
<
class
Var
>
...
...
@@ -208,7 +172,7 @@ compute_gd(SUBool::ImplSystem<Var> &is, const config_t &conf)
is
.
AddEmptyClosureToImpl
(
true
,
false
);
}
if
(
conf
.
keep_body_in_closure
&&
conf
.
output_type
==
O
utputType
::
IMPLICATIONS
)
&&
conf
.
output_type
==
O
UTPUT_TYPE
::
IMPLICATIONS
)
{
SUBool
::
logs
.
TLog
(
2
)
<<
"Adding bodies to the consequences"
<<
std
::
endl
;
is
.
AddBodyToCons
();
...
...
@@ -223,13 +187,13 @@ print_is(const SUBool::ImplSystem<Var> &is, unsigned max_variable,
auto
var_printer
=
[](
const
auto
&
v
)
{
return
v
;
};
switch
(
conf
.
output_type
)
{
case
O
utputType
::
IMPLICATIONS
:
case
O
UTPUT_TYPE
::
IMPLICATIONS
:
SUBool
::
output
(
conf
.
output_file
,
SUBool
::
make_annotated_is
(
// SUBool::AnnotatedImplSystem<Var, decltype(var_printer)>(
is
,
var_printer
,
max_variable
,
""
,
":"
));
break
;
case
O
utputType
::
CNF
:
case
O
UTPUT_TYPE
::
CNF
:
SUBool
::
output
(
conf
.
output_file
,
to_cnf
(
is
));
break
;
default:
...
...
@@ -284,21 +248,20 @@ process_dual_rail(const SUBool::CNF &cnf, const config_t &conf)
int
main
(
int
argc
,
char
*
argv
[])
{
config_t
conf
;
int
r
=
parse_arguments
(
argc
,
argv
,
conf
);
if
(
r
!=
0
)
auto
conf
=
parse_arguments
(
argc
,
argv
);
if
(
!
conf
)
{
return
r
;
return
1
;
}
dump_config
(
conf
,
2
);
dump_config
(
*
conf
,
3
);
SUBool
::
logs
.
TLog
(
2
)
<<
"Reading input"
<<
std
::
endl
;
auto
in_cnf
=
SUBool
::
input
<
SUBool
::
CNF
>
(
conf
.
input_file
);
switch
(
conf
.
impl_type
)
auto
in_cnf
=
SUBool
::
input
<
SUBool
::
CNF
>
(
conf
->
input_file
);
switch
(
conf
->
impl_type
)
{
case
I
mplType
::
HORN
:
return
process_horn
(
in_cnf
,
conf
);
case
I
mplType
::
DUAL_RAIL
:
return
process_dual_rail
(
in_cnf
,
conf
);
case
I
MPL_TYPE
::
HORN
:
return
process_horn
(
in_cnf
,
*
conf
);
case
I
MPL_TYPE
::
DUAL_RAIL
:
return
process_dual_rail
(
in_cnf
,
*
conf
);
default:
SUBool
::
logs
.
TLog
(
1
)
<<
"Unknown impl_type"
;
return
1
;
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment