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
a2027d23
Commit
a2027d23
authored
Jan 08, 2022
by
Kučera Petr RNDr. Ph.D.
Browse files
PrgConfigBase and random seed as a common parameter
parent
452ff186
Changes
18
Hide whitespace changes
Inline
Side-by-side
bin/balanced_cnf.cpp
View file @
a2027d23
...
...
@@ -22,27 +22,19 @@ const std::string SUBool::kPrgDesc =
"Generates special CNF with 3n variables and all prime implicates having n "
"positive, n negative and n missing literals."
;
struct
config_t
struct
config_t
:
public
SUBool
::
PrgConfigBase
{
std
::
string
output_file
{};
unsigned
n
{
2
};
unsigned
long
long
random_seed
{
0
};
virtual
void
InnerDump
(
unsigned
level
)
const
override
;
};
void
dump_
config
(
const
config_t
&
con
f
)
config
_t
::
InnerDump
(
unsigned
level
)
con
st
{
const
auto
level
=
SUBool
::
LogStream
::
kDumpConfigLevel
;
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"output_file"
,
conf
.
output_file
);
SUBool
::
logs
.
DumpVerbosity
(
"
\t
"
,
level
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"n"
,
conf
.
n
);
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
random seed: "
<<
conf
.
random_seed
<<
std
::
endl
;
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"output_file"
,
output_file
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"n"
,
n
);
}
std
::
optional
<
config_t
>
...
...
@@ -55,11 +47,10 @@ parse_arguments(int argc, char *argv[])
desc
.
add_options
()(
"block-size,n"
,
po
::
value
<
unsigned
>
(
&
conf
.
n
)
->
default_value
(
conf
.
n
),
"The number of variables is 3n"
);
if
(
!
opts
.
Parse
(
argc
,
argv
))
if
(
!
opts
.
Parse
(
argc
,
argv
,
conf
))
{
return
{};
}
conf
.
random_seed
=
opts
.
Seed
();
return
conf
;
}
...
...
@@ -114,7 +105,7 @@ main(int argc, char *argv[])
std
::
signal
(
SIGTERM
,
term_func
);
std
::
signal
(
SIGQUIT
,
term_func
);
std
::
signal
(
SIGINT
,
term_func
);
dump_config
(
*
conf
);
conf
->
Dump
(
);
auto
cnf
=
generate
(
conf
->
n
);
try
{
...
...
bin/cnfcanon.cpp
View file @
a2027d23
...
...
@@ -37,18 +37,17 @@ const SUBool::EnumAnnotation<PROCESS> kProcessAnnotation("PROCESS",
{{
PROCESS
::
NONE
,
"none"
,
"no inprocessing."
},
{
PROCESS
::
PRIME
,
"prime"
,
"use SAT to find a prime subimplicate."
}});
const
std
::
array
<
std
::
string
,
static_cast
<
size_t
>
(
PROCESS
::
Last
)
+
1
>
process_names
{
"none"
,
"prime"
};
const
char
*
kProcessOptDesc
=
"Clause inprocessing and preprocessing level.
\n
"
"none = No inprocessing,
\n
"
"prime = use SAT to find a prime subimplicate."
;
struct
config_t
struct
config_t
:
public
SUBool
::
PrgConfigBase
{
std
::
string
input_file
{};
std
::
string
output_file
{};
PROCESS
process
{
PROCESS
::
PRIME
};
unsigned
long
long
random_seed
{
0
};
virtual
void
InnerDump
(
unsigned
level
)
const
override
;
};
std
::
optional
<
config_t
>
...
...
@@ -63,32 +62,19 @@ parse_arguments(int argc, char *argv[])
po
::
options_description
desc
(
"Configuration options"
);
desc
.
add
(
opt_process
);
opts
.
Add
(
desc
);
if
(
!
opts
.
Parse
(
argc
,
argv
)
||
!
opt_process
.
GetValue
(
conf
.
process
))
if
(
!
opts
.
Parse
(
argc
,
argv
,
conf
)
||
!
opt_process
.
GetValue
(
conf
.
process
))
{
return
{};
}
conf
.
random_seed
=
opts
.
Seed
();
return
conf
;
}
void
dump_
config
(
const
config_t
&
con
f
)
config
_t
::
InnerDump
(
unsigned
level
)
con
st
{
const
auto
level
=
SUBool
::
LogStream
::
kDumpConfigLevel
;
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
input_file: "
<<
conf
.
input_file
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
output_file: "
<<
conf
.
output_file
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
process: "
<<
process_names
.
at
(
static_cast
<
unsigned
>
(
conf
.
process
))
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
random seed: "
<<
conf
.
random_seed
<<
std
::
endl
;
SUBool
::
logs
.
DumpVerbosity
(
"
\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
);
}
std
::
unique_ptr
<
SUBool
::
AbsCanon
>
...
...
@@ -113,7 +99,7 @@ main(int argc, char *argv[])
{
return
1
;
}
dump_config
(
*
conf
);
conf
->
Dump
(
);
auto
cnf
=
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
input_file
,
0
,
2
,
"Failed to parse the input file"
);
auto
canon
=
canon_procedure
(
*
conf
,
cnf
);
...
...
bin/cnfcomp.cpp
View file @
a2027d23
...
...
@@ -51,32 +51,23 @@ const SUBool::EnumAnnotation<COMPARE_KIND> kCompareKindAnnotation(
"check if the clauses in one CNF are absorbed by the other (not "
"empowering)"
}});
struct
config_t
struct
config_t
:
public
SUBool
::
PrgConfigBase
{
std
::
string
file_left
{};
std
::
string
file_right
{};
RELATION
relation
{
RELATION
::
EQUAL
};
COMPARE_KIND
compare_kind
{
COMPARE_KIND
::
IMPLICATE
};
unsigned
long
long
random_seed
{
0
};
virtual
void
InnerDump
(
unsigned
level
)
const
override
;
};
void
dump_
config
(
const
config_t
&
con
f
)
config
_t
::
InnerDump
(
unsigned
level
)
con
st
{
const
auto
level
=
SUBool
::
LogStream
::
kDumpConfigLevel
;
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
file_left: "
<<
conf
.
file_left
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
file_right: "
<<
conf
.
file_right
<<
std
::
endl
;
SUBool
::
logs
.
DumpVerbosity
(
"
\t
"
,
level
);
kRelationAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"relation"
,
conf
.
relation
);
kCompareKindAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"compare_kind"
,
conf
.
compare_kind
);
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
random seed: "
<<
conf
.
random_seed
<<
std
::
endl
;
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"file_left"
,
file_left
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"file_right"
,
file_right
);
kRelationAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"relation"
,
relation
);
kCompareKindAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"compare_kind"
,
compare_kind
);
}
std
::
optional
<
config_t
>
...
...
@@ -96,12 +87,11 @@ parse_arguments(int argc, char *argv[])
desc
.
add
(
opt_relation
);
desc
.
add
(
opt_compare_kind
);
opts
.
Add
(
desc
);
if
(
!
opts
.
Parse
(
argc
,
argv
)
||
!
opt_relation
.
GetValue
(
conf
.
relation
)
if
(
!
opts
.
Parse
(
argc
,
argv
,
conf
)
||
!
opt_relation
.
GetValue
(
conf
.
relation
)
||
!
opt_compare_kind
.
GetValue
(
conf
.
compare_kind
))
{
return
{};
}
conf
.
random_seed
=
opts
.
Seed
();
return
conf
;
}
...
...
@@ -309,7 +299,7 @@ main(int argc, char *argv[])
{
return
1
;
}
dump_config
(
*
conf
);
conf
->
Dump
(
);
auto
left_cnf
=
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
file_left
);
auto
right_cnf
=
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
file_right
);
SUBool
::
CPUTime
cpu_time
;
...
...
bin/cnfdiff.cpp
View file @
a2027d23
...
...
@@ -15,33 +15,25 @@ const std::string SUBool::kPrgDesc =
"Program for comparing two CNFs as sets of "
"clauses (not as representations of * functions)."
;
struct
config_t
struct
config_t
:
public
SUBool
::
PrgConfigBase
{
std
::
string
file_left
{};
std
::
string
file_right
{};
bool
suppress_first
{
false
};
bool
suppress_second
{
false
};
bool
suppress_third
{
false
};
unsigned
long
long
random_seed
{
0
};
virtual
void
InnerDump
(
unsigned
level
)
const
override
;
};
void
dump_
config
(
const
config_t
&
con
f
)
config
_t
::
InnerDump
(
unsigned
level
)
con
st
{
const
auto
level
=
SUBool
::
LogStream
::
kDumpConfigLevel
;
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"file_left"
,
conf
.
file_left
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"file_right"
,
conf
.
file_right
);
SUBool
::
logs
.
DumpVerbosity
(
"
\t
"
,
level
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_first"
,
conf
.
suppress_first
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_second"
,
conf
.
suppress_second
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_third"
,
conf
.
suppress_third
);
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
random seed: "
<<
conf
.
random_seed
<<
std
::
endl
;
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"file_left"
,
file_left
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"file_right"
,
file_right
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_first"
,
suppress_first
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_second"
,
suppress_second
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_third"
,
suppress_third
);
}
std
::
optional
<
config_t
>
...
...
@@ -59,11 +51,10 @@ parse_arguments(int argc, char *argv[])
po
::
bool_switch
(
&
conf
.
suppress_third
),
"Suppress printing the clauses unique to the third CNF."
);
opts
.
Add
(
desc
);
if
(
!
opts
.
Parse
(
argc
,
argv
))
if
(
!
opts
.
Parse
(
argc
,
argv
,
conf
))
{
return
{};
}
conf
.
random_seed
=
opts
.
Seed
();
return
conf
;
}
...
...
@@ -130,7 +121,7 @@ main(int argc, char *argv[])
{
return
1
;
}
dump_config
(
*
conf
);
conf
->
Dump
(
);
compare
(
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
file_left
),
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
file_right
),
*
conf
);
return
0
;
...
...
bin/cnfgraphx.cpp
View file @
a2027d23
...
...
@@ -45,7 +45,7 @@ const SUBool::EnumAnnotation<GRAPH_KIND> kGraphKindAnnotation("GRAPH_KIND",
{
GRAPH_KIND
::
INCIDENCE
,
"incidence"
,
"incidence graph"
},
{
GRAPH_KIND
::
DINCIDENCE
,
"dincidence"
,
"directed incidence graph"
}});
struct
config_t
struct
config_t
:
public
SUBool
::
PrgConfigBase
{
std
::
string
input_file
{};
std
::
string
output_file
{};
...
...
@@ -55,30 +55,21 @@ struct config_t
std
::
string
var_color
{};
std
::
string
clause_prefix
{
"c"
};
std
::
string
clause_color
{};
virtual
void
InnerDump
(
unsigned
level
)
const
override
;
};
void
dump_
config
(
const
config_t
&
con
f
)
config
_t
::
InnerDump
(
unsigned
level
)
con
st
{
const
auto
level
=
SUBool
::
LogStream
::
kDumpConfigLevel
;
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
input_file: "
<<
conf
.
input_file
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
output_file: "
<<
conf
.
output_file
<<
std
::
endl
;
SUBool
::
logs
.
DumpVerbosity
(
"
\t
"
,
level
);
kGraphKindAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"graph_kind"
,
conf
.
graph_kind
);
kOutputTypeAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"output_type"
,
conf
.
output_type
);
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
var_prefix: "
<<
conf
.
var_prefix
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
var_color: "
<<
conf
.
var_color
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
clause_prefix: "
<<
conf
.
clause_prefix
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
clause_color: "
<<
conf
.
clause_color
<<
std
::
endl
;
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"input_file"
,
input_file
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"output_file"
,
output_file
);
kGraphKindAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"graph_kind"
,
graph_kind
);
kOutputTypeAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"output_type"
,
output_type
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"var_prefix"
,
var_prefix
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"var_color"
,
var_color
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"clause_prefix"
,
clause_prefix
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"clause_color"
,
clause_color
);
}
std
::
optional
<
config_t
>
...
...
@@ -117,7 +108,8 @@ parse_arguments(int argc, char *argv[])
+
". Empty string means no color."
)
.
c_str
());
opts
.
Add
(
desc
);
if
(
!
opts
.
Parse
(
argc
,
argv
)
||
!
opt_output_type
.
GetValue
(
conf
.
output_type
)
if
(
!
opts
.
Parse
(
argc
,
argv
,
conf
)
||
!
opt_output_type
.
GetValue
(
conf
.
output_type
)
||
!
opt_graph_kind
.
GetValue
(
conf
.
graph_kind
))
{
return
{};
...
...
@@ -214,7 +206,7 @@ main(int argc, char *argv[])
{
return
1
;
}
dump_config
(
*
conf
);
conf
->
Dump
(
);
auto
cnf
=
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
input_file
);
return
do_graph
(
*
conf
,
cnf
);
}
bin/cnfprime.cpp
View file @
a2027d23
...
...
@@ -26,11 +26,13 @@ const std::string SUBool::kPrgDesc = "Making a CNF prime";
const
std
::
string
prg_help
=
"Makes a given CNF prime, possibly only with respect to 1-provability."
;
struct
config_t
struct
config_t
:
public
SUBool
::
PrgConfigBase
{
std
::
string
input_file
{};
std
::
string
output_file
{};
bool
unitprop
{
false
};
virtual
void
InnerDump
(
unsigned
level
)
const
override
;
};
std
::
optional
<
config_t
>
...
...
@@ -47,7 +49,7 @@ parse_arguments(int argc, char *argv[])
"respect to 1-provability (although not fully as only one round of "
"prime subimplicate finding is performed"
);
opts
.
Add
(
desc
);
if
(
!
opts
.
Parse
(
argc
,
argv
))
if
(
!
opts
.
Parse
(
argc
,
argv
,
conf
))
{
return
{};
}
...
...
@@ -55,20 +57,11 @@ parse_arguments(int argc, char *argv[])
}
void
dump_
config
(
const
config_t
&
con
f
)
config
_t
::
InnerDump
(
unsigned
level
)
con
st
{
const
auto
level
=
SUBool
::
LogStream
::
kDumpConfigLevel
;
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
input_file: "
<<
conf
.
input_file
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
output_file: "
<<
conf
.
output_file
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
unitprop: "
<<
SUBool
::
bool_to_string
(
conf
.
unitprop
)
<<
std
::
endl
;
SUBool
::
logs
.
DumpVerbosity
(
"
\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
);
}
SUBool
::
CNF
...
...
@@ -92,7 +85,7 @@ main(int argc, char *argv[])
{
return
1
;
}
dump_config
(
*
conf
);
conf
->
Dump
(
);
SUBool
::
logs
.
TLog
(
2
)
<<
"Reading input"
<<
std
::
endl
;
auto
in_cnf
=
SUBool
::
input
<
SUBool
::
CNF
>
(
conf
->
input_file
);
SUBool
::
logs
.
TLog
(
1
)
<<
"Starting computation"
<<
std
::
endl
;
...
...
bin/dpelim.cpp
View file @
a2027d23
...
...
@@ -27,7 +27,7 @@ const std::string prg_help =
"may have different indices in the output (they are considered auxiliary "
"in that their names do not matter)."
;
struct
config_t
struct
config_t
:
public
SUBool
::
PrgConfigBase
{
std
::
string
input_file
{};
std
::
string
output_file
{};
...
...
@@ -48,40 +48,34 @@ struct config_t
double
minimize_size_factor
{
0.6
};
unsigned
max_increase
{
SUBool
::
DPElimEliminationOptions
::
kDefaultMaxIncrease
};
long
double
factor
{
SUBool
::
DPElimEliminationOptions
::
kDefaultFactor
};
virtual
void
InnerDump
(
unsigned
level
)
const
override
;
};
void
dump_
config
(
const
config_t
&
con
f
)
config
_t
::
InnerDump
(
unsigned
level
)
con
st
{
const
auto
level
=
SUBool
::
LogStream
::
kDumpConfigLevel
;
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
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
.
DumpVerbosity
(
"
\t
"
,
level
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"max_input_var"
,
conf
.
max_input_var
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"elim_minimize"
,
conf
.
elim_minimize
);
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
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"elim_minimize"
,
elim_minimize
);
SUBool
::
CNFEncoding
::
kBlockPrimeAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"block_prime"
,
conf
.
block_prime
);
"
\t
"
,
level
,
"block_prime"
,
block_prime
);
SUBool
::
DPElimEliminationOptions
::
kEliminatePolicyAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"eliminate"
,
conf
.
eliminate
);
"
\t
"
,
level
,
"eliminate"
,
eliminate
);
SUBool
::
DPEliminator
::
kIgnorePolicyAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"ignore_policy"
,
conf
.
ignore_policy
);
"
\t
"
,
level
,
"ignore_policy"
,
ignore_policy
);
SUBool
::
DPEliminator
::
kInprocessingAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"inprocessing"
,
conf
.
inprocessing
);
"
\t
"
,
level
,
"inprocessing"
,
inprocessing
);
SUBool
::
DPEliminator
::
kIncreasePolicyAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"increase_policy"
,
conf
.
increase_policy
);
"
\t
"
,
level
,
"increase_policy"
,
increase_policy
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"minimize_size_step"
,
conf
.
minimize_size_step
);
"
\t
"
,
level
,
"minimize_size_step"
,
minimize_size_step
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"minimize_size_factor"
,
conf
.
minimize_size_factor
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"max_increase"
,
conf
.
max_increase
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"factor"
,
conf
.
factor
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"final_minimize"
,
conf
.
final_minimize
);
SUBool
::
logs
.
TLog
(
level
)
<<
"END"
<<
std
::
endl
;
"
\t
"
,
level
,
"minimize_size_factor"
,
minimize_size_factor
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"max_increase"
,
max_increase
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"factor"
,
factor
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"final_minimize"
,
final_minimize
);
}
std
::
optional
<
config_t
>
...
...
@@ -98,7 +92,7 @@ parse_arguments(int argc, char *argv[])
opts
.
MakeOptionsGroup
<
SUBool
::
DPElimClauseManipOptions
>
();
auto
minimize_opts
=
opts
.
MakeOptionsGroup
<
SUBool
::
DPElimMinimizeOptions
>
();
if
(
!
opts
.
Parse
(
argc
,
argv
))
if
(
!
opts
.
Parse
(
argc
,
argv
,
conf
))
{
return
{};
}
...
...
@@ -184,7 +178,7 @@ main(int argc, char *argv[])
std
::
signal
(
SIGTERM
,
term_func
);
std
::
signal
(
SIGQUIT
,
term_func
);
std
::
signal
(
SIGINT
,
term_func
);
dump_config
(
*
conf
);
conf
->
Dump
(
);
auto
cnf
=
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
input_file
);
SUBool
::
PCEncoding
enc
(
cnf
,
conf
->
max_input_var
,
false
);
eliminate
(
enc
,
*
conf
);
...
...
bin/gdbasis.cpp
View file @
a2027d23
...
...
@@ -53,7 +53,7 @@ const OUTPUT_TYPE kDefaultOutputType = OUTPUT_TYPE::IMPLICATIONS;
const
std
::
string
kDefaultSeparator
=
":"
;
struct
config_t
struct
config_t
:
public
SUBool
::
PrgConfigBase
{
std
::
string
input_file
{};
std
::
string
output_file
{};
...
...
@@ -68,31 +68,24 @@ struct config_t
bool
body_minimal
{
false
};
// At the end, make it right irredundant
bool
right_irredundant
{
false
};
virtual
void
InnerDump
(
unsigned
level
)
const
override
;
};
void
dump_
config
(
const
config_t
&
con
f
)
config
_t
::
InnerDump
(
unsigned
level
)
con
st
{
const
auto
level
=
SUBool
::
LogStream
::
kDumpConfigLevel
;
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
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
.
DumpVerbosity
(
"
\t
"
,
level
);
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
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"input_file"
,
input_file
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"output_file"
,
output_file
);
kImplTypeAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"impl_type"
,
impl_type
);
kOutputTypeAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"output_type"
,
output_type
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"impl_sep"
,
impl_sep
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"omit_empty_closure"
,
conf
.
omit_empty_closure
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"body_minimal"
,
conf
.
body_minimal
);
"
\t
"
,
level
,
"keep_body_in_closure"
,
keep_body_in_closure
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"right_irredundant"
,
conf
.
right_irredundant
);
"
\t
"
,
level
,
"omit_empty_closure"
,
omit_empty_closure
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"body_minimal"
,
body_minimal
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"right_irredundant"
,
right_irredundant
);
}
std
::
optional
<
config_t
>
...
...
@@ -138,7 +131,7 @@ parse_arguments(int argc, char *argv[])
"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
)
if
(
!
opts
.
Parse
(
argc
,
argv
,
conf
)
||
!
opt_impl_type
.
GetValue
(
conf
.
impl_type
)
||
!
opt_output_type
.
GetValue
(
conf
.
output_type
))
{
return
{};
...
...
@@ -261,7 +254,7 @@ main(int argc, char *argv[])
{
return
1
;
}
dump_config
(
*
conf
);
conf
->
Dump
(
);
SUBool
::
logs
.
TLog
(
2
)
<<
"Reading input"
<<
std
::
endl
;
auto
in_cnf
=
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
input_file
,
0
,
2
,
"Failed to parse the input file"
);
...
...
bin/nnfencode.cpp
View file @
a2027d23
...
...
@@ -51,7 +51,7 @@ const SUBool::EnumAnnotation<ENCODING_TYPE> kEncodingTypeAnnotation(
const
ENCODING_TYPE
kDefaultEncodingType
=
ENCODING_TYPE
::
CC
;
const
SUBool
::
LEVEL_FUNC
kDefaultLevelFunc
=
SUBool
::
LEVEL_FUNC
::
FROM_LEAVES
;
struct
config_t
struct
config_t
:
public
SUBool
::
PrgConfigBase
{
std
::
string
input_file
{};
std
::
string
output_file
{};
...
...
@@ -63,33 +63,25 @@ struct config_t
SUBool
::
CardinalOptionsGroup
::
kDefaultAmoEncoding
};
SUBool
::
ExOneEncoder
::
KIND
exone_encoding
{
SUBool
::
CardinalOptionsGroup
::
kDefaultExOneEncoding
};
virtual
void
InnerDump
(
unsigned
level
)
const
override
;
};
void
dump_
config
(
const
config_t
&
con
f
)
config
_t
::
InnerDump
(
unsigned
level
)
con
st
{
const
auto
level
=
SUBool
::
LogStream
::
kDumpConfigLevel
;
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
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
.
DumpVerbosity
(
"
\t
"
,
level
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"input_file"
,
input_file
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"output_file"
,
output_file
);
kEncodingTypeAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"encoding_type"
,
conf
.
encoding_type
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"final_minimize"
,
conf
.
final_minimize
);
"
\t
"
,
level
,
"encoding_type"
,
encoding_type
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"final_minimize"
,
final_minimize
);
SUBool
::
kLevelFuncAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"level_func"
,
conf
.
level_func
);
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
check_smooth: "
<<
SUBool
::
bool_to_string
(
conf
.
check_smooth
)
<<
std
::
endl
;
"
\t
"
,
level
,
"level_func"
,
level_func
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"check_smooth"
,
check_smooth
);
SUBool
::
AmoEncoder
::
kKindAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"amo_encoding"
,
conf
.
amo_encoding
);
"
\t
"
,
level
,
"amo_encoding"
,
amo_encoding
);
SUBool
::
ExOneEncoder
::
kKindAnnotation
.
DumpValue
(
"
\t
"
,
level
,
"exone_encoding"
,
conf
.
exone_encoding
);
SUBool
::
logs
.
TLog
(
level
)
<<
"END"
<<
std
::
endl
;
"
\t
"
,
level
,
"exone_encoding"
,
exone_encoding
);
}
bool
...
...
@@ -125,7 +117,7 @@ parse_arguments(int argc, char *argv[])
opts
.
Add
(
desc
);
auto
cardinal_opt_group
=
opts
.
MakeOptionsGroup
<
SUBool
::
CardinalOptionsGroup
>
();
if
(
!
opts
.
Parse
(
argc
,
argv
)
if
(
!
opts
.
Parse
(
argc
,
argv
,
conf
)
||
!
opt_encoding_type
.
GetValue
(
conf
.
encoding_type
)
||
!
opt_level_fun