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
84c0c5e5
Commit
84c0c5e5
authored
Jul 14, 2021
by
Kučera Petr RNDr. Ph.D.
Browse files
cnfgraph program using PrgOptions
parent
29b3d9af
Changes
5
Hide whitespace changes
Inline
Side-by-side
bin/cnfcanon.cpp
View file @
84c0c5e5
...
...
@@ -57,7 +57,7 @@ parse_arguments(int argc, char *argv[])
"Clause inprocessing and preprocessing level."
,
conf
.
process
);
std
::
string
process
;
SUBool
::
PrgOptions
opts
;
opts
.
InputOutput
(
conf
.
input_file
,
conf
.
output_file
);
opts
.
InputOutput
(
&
conf
.
input_file
,
&
conf
.
output_file
);
po
::
options_description
desc
(
"Configuration options"
);
desc
.
add
(
opt_process
);
opts
.
Add
(
desc
);
...
...
bin/cnfgraphx.cpp
View file @
84c0c5e5
...
...
@@ -6,24 +6,28 @@
* Program for exporting a CNF as a graph.
*/
#include <cxxopts.hpp>
#include <iostream>
#include "cnfgraph.h"
#include "enum_opt.h"
#include "logstream.h"
#include "prgutil.h"
enum
class
OUTPUT
enum
class
OUTPUT
_TYPE
{
GRAPHML
,
DOT
,
Last
=
DOT
};
const
SUBool
::
EnumAnnotation
<
OUTPUT_TYPE
>
kOutputTypeAnnotation
(
"OUTPUT_TYPE"
,
{{
OUTPUT_TYPE
::
GRAPHML
,
"graphml"
,
"GraphML"
},
{
OUTPUT_TYPE
::
DOT
,
"dot"
,
"dot format"
}});
const
std
::
string
SUBool
::
kPrgName
=
"cnfgraph"
;
const
std
::
string
SUBool
::
kPrgDesc
=
"export a CNF as a graph"
;
const
std
::
string
i
ncidence
_g
raph
_var_c
olor
=
"red"
;
const
std
::
string
i
ncidence
_g
raph
_c
lause
_c
olor
=
"blue"
;
const
std
::
string
kDefaultI
ncidence
G
raph
VarC
olor
=
"red"
;
const
std
::
string
kDefaultI
ncidence
G
raph
C
lause
C
olor
=
"blue"
;
enum
class
GRAPH_KIND
{
...
...
@@ -33,18 +37,19 @@ enum class GRAPH_KIND
DINCIDENCE
,
Last
=
DINCIDENCE
};
const
std
::
map
<
std
::
string
,
GRAPH_KIND
>
graph_kind_names
=
{
{
"primal"
,
GRAPH_KIND
::
PRIMAL
},
{
"dual"
,
GRAPH_KIND
::
DUAL
},
{
"incidence"
,
GRAPH_KIND
::
INCIDENCE
},
{
"dincidence"
,
GRAPH_KIND
::
DINCIDENCE
}};
const
SUBool
::
EnumAnnotation
<
GRAPH_KIND
>
kGraphKindAnnotation
(
"GRAPH_KIND"
,
{{
GRAPH_KIND
::
PRIMAL
,
"primal"
,
"primal graph"
},
{
GRAPH_KIND
::
DUAL
,
"dual"
,
"dual graph"
},
{
GRAPH_KIND
::
INCIDENCE
,
"incidence"
,
"incidence graph"
},
{
GRAPH_KIND
::
DINCIDENCE
,
"dincidence"
,
"directed incidence graph"
}});
struct
config_t
{
std
::
string
input_file
{};
std
::
string
output_file
{};
unsigned
verbosity
{
3
};
// 0 means no output
GRAPH_KIND
graph_kind
{
GRAPH_KIND
::
PRIMAL
};
OUTPUT
output_type
{
OUTPUT
::
GRAPHML
};
OUTPUT
_TYPE
output_type
{
OUTPUT
_TYPE
::
GRAPHML
};
std
::
string
var_prefix
{
"x"
};
std
::
string
var_color
{};
std
::
string
clause_prefix
{
"c"
};
...
...
@@ -58,13 +63,11 @@ dump_config(const config_t &conf, unsigned level)
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
verbosity: "
<<
conf
.
verbosity
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
graph_kind: "
<<
static_cast
<
unsigned
>
(
conf
.
graph_kind
)
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
output_type: "
<<
static_cast
<
unsigned
>
(
conf
.
output_type
)
<<
std
::
endl
;
<<
"
\t
verbosity: "
<<
SUBool
::
logs
.
mVerbLevel
<<
std
::
endl
;
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
)
...
...
@@ -73,154 +76,81 @@ dump_config(const config_t &conf, unsigned level)
<<
"
\t
clause_color: "
<<
conf
.
clause_color
<<
std
::
endl
;
}
GRAPH_KIND
parse_
graph_kind
(
const
std
::
string
&
kind
)
std
::
optional
<
config_t
>
parse_
arguments
(
int
argc
,
char
*
argv
[]
)
{
try
{
return
graph_kind_names
.
at
(
kind
);
}
catch
(
std
::
out_of_range
&
e
)
config_t
conf
;
auto
opt_output_type
=
SUBool
::
make_enum_option
(
kOutputTypeAnnotation
,
"output-type,t"
,
"Type of the output."
,
conf
.
output_type
);
auto
opt_graph_kind
=
SUBool
::
make_enum_option
(
kGraphKindAnnotation
,
"graph-kind,g"
,
"Kind of the graph to be exported."
,
conf
.
graph_kind
);
boost
::
optional
<
std
::
string
>
var_color
;
boost
::
optional
<
std
::
string
>
clause_color
;
SUBool
::
PrgOptions
opts
(
true
);
opts
.
InputOutput
(
&
conf
.
input_file
,
&
conf
.
output_file
);
po
::
options_description
desc
(
"Configuration options"
);
desc
.
add
(
opt_output_type
);
desc
.
add
(
opt_graph_kind
);
desc
.
add_options
()(
"var-prefix"
,
po
::
value
<
std
::
string
>
(
&
conf
.
var_prefix
)
->
default_value
(
conf
.
var_prefix
),
"Prefix of a name of a vertex corresponding to a variable."
)(
"clause-prefix"
,
po
::
value
<
std
::
string
>
(
&
conf
.
clause_prefix
)
->
default_value
(
conf
.
clause_prefix
),
"Prefix of a name of a vertex corresponding to a clause."
)(
"var-color"
,
po
::
value
(
&
var_color
),
(
"Color of a vertex corresponding to a variable. "
"The default depends on the graph kind. In case of primal and "
"dual graph, it is no color, in case of an incidence graph, it is "
+
kDefaultIncidenceGraphVarColor
+
". Empty string means no color."
)
.
c_str
())(
"clause-color"
,
po
::
value
(
&
clause_color
),
(
"Color of a vertex corresponding to a clause. "
"The default depends on the graph kind. In case of primal and "
"dual graph, it is no color, in case of an incidence graph, it is "
+
kDefaultIncidenceGraphClauseColor
+
". Empty string means no color."
)
.
c_str
());
opts
.
Add
(
desc
);
if
(
!
opts
.
Parse
(
argc
,
argv
)
||
!
opt_output_type
.
GetValue
(
conf
.
output_type
)
||
!
opt_graph_kind
.
GetValue
(
conf
.
graph_kind
))
{
throw
SUBool
::
BadParameterException
(
"parse_graph_kind"
,
"Unknown graph kind "
+
kind
);
return
{};
}
}
OUTPUT
parse_output_type
(
const
std
::
string
&
output_type
)
{
if
(
output_type
==
"graphml"
)
if
(
var_color
)
{
return
OUTPUT
::
GRAPHML
;
conf
.
var_color
=
*
var_color
;
}
if
(
output_type
==
"dot"
)
if
(
clause_color
)
{
return
OUTPUT
::
DOT
;
conf
.
clause_color
=
*
clause_color
;
}
throw
SUBool
::
BadParameterException
(
"parse_output_type"
,
"Unknown output type "
+
output_type
);
}
int
parse_arguments
(
int
argc
,
char
*
argv
[],
config_t
&
conf
)
{
try
if
(
conf
.
graph_kind
==
GRAPH_KIND
::
INCIDENCE
||
conf
.
graph_kind
==
GRAPH_KIND
::
DINCIDENCE
)
{
cxxopts
::
Options
options
(
SUBool
::
kPrgName
,
SUBool
::
kPrgDesc
);
options
.
positional_help
(
"[input [output]]"
);
std
::
string
graph_kind
;
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 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
))(
"t,output-type"
,
"Type of the output. "
"graphml = GraphML, "
"dot = GraphViz DOT. "
,
cxxopts
::
value
<
std
::
string
>
(
output_type
)
->
default_value
(
"graphml"
))(
"g,graph-kind"
,
"Kind of the graph to be exported. "
"primal = primal graph, "
"dual = dual graph, "
"incidence = incidence graph."
"dincidence = directed incidence graph."
,
cxxopts
::
value
<
std
::
string
>
(
graph_kind
)
->
default_value
(
"primal"
))(
"var-prefix"
,
"Prefix of a name of a vertex corresponding to a variable."
,
cxxopts
::
value
<
std
::
string
>
(
conf
.
var_prefix
)
->
default_value
(
"x"
))(
"clause-prefix"
,
"Prefix of a name of a vertex corresponding to a clause."
,
cxxopts
::
value
<
std
::
string
>
(
conf
.
clause_prefix
)
->
default_value
(
"c"
))(
"var-color"
,
"Color of a vertex corresponding to a variable. "
"The default depends on the graph kind. In case of primal and "
"dual graph, it is no color, in case of an incidence graph, it is "
+
incidence_graph_var_color
+
". Empty string means no color."
,
cxxopts
::
value
<
std
::
string
>
(
conf
.
var_color
))(
"clause-color"
,
"Color of a vertex corresponding to a clause. "
"The default depends on the graph kind. In case of primal and "
"dual graph, it is no color, in case of an incidence graph, it is "
+
incidence_graph_clause_color
+
". Empty string means no color."
,
cxxopts
::
value
<
std
::
string
>
(
conf
.
var_color
));
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"
))
if
(
!
var_color
)
{
SUBool
::
print_version
(
std
::
cout
);
return
1
;
conf
.
var_color
=
kDefaultIncidenceGraphVarColor
;
}
if
(
result
.
count
(
"positional"
)
)
if
(
!
clause_color
)
{
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
;
conf
.
clause_color
=
kDefaultIncidenceGraphClauseColor
;
}
try
{
conf
.
graph_kind
=
parse_graph_kind
(
graph_kind
);
}
catch
(
SUBool
::
BadParameterException
&
e
)
{
SUBool
::
logs
.
TLog
(
0
)
<<
"Error parsing the graph kind: "
<<
e
.
what
()
<<
std
::
endl
;
return
1
;
}
try
{
conf
.
output_type
=
parse_output_type
(
output_type
);
}
catch
(
SUBool
::
BadParameterException
&
e
)
{
SUBool
::
logs
.
TLog
(
0
)
<<
"Error parsing the output type: "
<<
e
.
what
()
<<
std
::
endl
;
return
1
;
}
if
(
conf
.
graph_kind
==
GRAPH_KIND
::
INCIDENCE
||
conf
.
graph_kind
==
GRAPH_KIND
::
DINCIDENCE
)
{
if
(
!
result
.
count
(
"var-color"
))
{
conf
.
var_color
=
incidence_graph_var_color
;
}
if
(
!
result
.
count
(
"clause-color"
))
{
conf
.
clause_color
=
incidence_graph_clause_color
;
}
}
}
catch
(
const
cxxopts
::
OptionException
&
e
)
{
std
::
cerr
<<
"Error parsing options: "
<<
e
.
what
()
<<
std
::
endl
;
return
1
;
}
return
0
;
return
conf
;
}
template
<
typename
T
,
typename
...
Args
>
int
write_graph
(
std
::
ostream
&
os
,
OUTPUT
output_type
,
T
&
g
,
const
Args
&
...
args
)
write_graph
(
std
::
ostream
&
os
,
OUTPUT_TYPE
output_type
,
T
&
g
,
const
Args
&
...
args
)
{
switch
(
output_type
)
{
case
OUTPUT
::
GRAPHML
:
case
OUTPUT
_TYPE
::
GRAPHML
:
g
.
WriteGraphML
(
os
,
args
...);
break
;
case
OUTPUT
::
DOT
:
case
OUTPUT
_TYPE
::
DOT
:
g
.
WriteGraphViz
(
os
,
args
...);
break
;
default:
...
...
@@ -274,14 +204,12 @@ do_graph(const config_t &conf, const SUBool::CNF &cnf)
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
;
}
SUBool
::
logs
.
mVerbLevel
=
conf
.
verbosity
;
dump_config
(
conf
,
0
);
auto
cnf
=
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
.
input_file
,
SUBool
::
logs
);
return
do_graph
(
conf
,
cnf
);
dump_config
(
*
conf
,
4
);
auto
cnf
=
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
input_file
,
SUBool
::
logs
);
return
do_graph
(
*
conf
,
cnf
);
}
lib/cnfgraph.cpp
View file @
84c0c5e5
...
...
@@ -18,26 +18,26 @@ SUBool::PDCNFGraph::Graph() const
}
std
::
pair
<
boost
::
dynamic_properties
,
std
::
string
>
SUBool
::
PDCNFGraph
::
DynamicProperties
(
const
std
::
string
&
vertex_prefix
,
const
std
::
string
&
vertex_color
)
SUBool
::
PDCNFGraph
::
DynamicProperties
(
const
std
::
string
&
vertex_prefix
,
const
std
::
string
&
vertex_color
)
{
boost
::
dynamic_properties
dp
;
auto
index
=
boost
::
get
(
boost
::
vertex_index
,
mGraph
);
auto
index2name
=
[
&
](
unsigned
i
)
{
return
NameOfIndex
(
i
,
vertex_prefix
);
};
dp
.
property
(
"name"
,
boost
::
make_transform_value_property_map
(
index2name
,
index
));
dp
.
property
(
"name"
,
boost
::
make_transform_value_property_map
(
index2name
,
index
));
if
(
!
vertex_color
.
empty
())
{
dp
.
property
(
"color"
,
boost
::
make_static_property_map
<
std
::
string
>
(
vertex_color
));
boost
::
make_transform_value_property_map
(
[
&
vertex_color
](
unsigned
)
{
return
vertex_color
;
},
index
));
}
return
std
::
make_pair
(
std
::
move
(
dp
),
"name"
);
}
void
SUBool
::
PDCNFGraph
::
WriteGraphML
(
std
::
ostream
&
out
,
const
std
::
string
&
vertex_prefix
,
const
std
::
string
&
vertex_color
)
const
std
::
string
&
vertex_prefix
,
const
std
::
string
&
vertex_color
)
{
auto
dp
=
DynamicProperties
(
vertex_prefix
,
vertex_color
);
boost
::
write_graphml
(
out
,
Graph
(),
dp
.
first
,
true
);
...
...
@@ -45,8 +45,7 @@ SUBool::PDCNFGraph::WriteGraphML(std::ostream &out,
void
SUBool
::
PDCNFGraph
::
WriteGraphViz
(
std
::
ostream
&
out
,
const
std
::
string
&
vertex_prefix
,
const
std
::
string
&
vertex_color
)
const
std
::
string
&
vertex_prefix
,
const
std
::
string
&
vertex_color
)
{
auto
dp
=
DynamicProperties
(
vertex_prefix
,
vertex_color
);
boost
::
write_graphviz_dp
(
out
,
Graph
(),
dp
.
first
,
dp
.
second
);
...
...
@@ -55,8 +54,8 @@ SUBool::PDCNFGraph::WriteGraphViz(std::ostream &out,
SUBool
::
PDCNFGraph
::
PDCNFGraph
()
:
mGraph
()
{}
void
SUBool
::
PDCNFGraph
::
InitGraph
(
std
::
vector
<
std
::
pair
<
unsigned
,
unsigned
>>
edges
,
unsigned
vertex_count
)
SUBool
::
PDCNFGraph
::
InitGraph
(
std
::
vector
<
std
::
pair
<
unsigned
,
unsigned
>>
edges
,
unsigned
vertex_count
)
{
std
::
sort
(
edges
.
begin
(),
edges
.
end
());
auto
it
=
std
::
unique
(
edges
.
begin
(),
edges
.
end
());
...
...
@@ -73,8 +72,8 @@ SUBool::PrimalGraph::PrimalGraph(const CNF &cnf)
{
for
(
unsigned
j
=
i
+
1
;
j
<
clause
.
Size
();
++
j
)
{
edges
.
emplace_back
(
clause
[
i
].
Variable
()
-
1
,
clause
[
j
].
Variable
()
-
1
);
edges
.
emplace_back
(
clause
[
i
].
Variable
()
-
1
,
clause
[
j
].
Variable
()
-
1
);
}
}
}
...
...
lib/prgutil.cpp
View file @
84c0c5e5
...
...
@@ -64,10 +64,10 @@ SUBool::PrgOptions::InitCommon()
void
SUBool
::
PrgOptions
::
InputOutput
(
std
::
string
&
input_file
,
std
::
string
&
output_file
)
std
::
string
*
input_file
,
std
::
string
*
output_file
)
{
mHidden
.
add_options
()(
"input"
,
po
::
value
<
std
::
string
>
(
&
input_file
))(
"output"
,
po
::
value
<
std
::
string
>
(
&
output_file
));
mHidden
.
add_options
()(
"input"
,
po
::
value
<
std
::
string
>
(
input_file
))(
"output"
,
po
::
value
<
std
::
string
>
(
output_file
));
mPositional
.
add
(
"input"
,
1
);
mPositional
.
add
(
"output"
,
1
);
mPositionalHelp
+=
"[input [output]]"
;
...
...
@@ -151,14 +151,14 @@ SUBool::PrgOptions::Parse(int argc, char *argv[])
{
return
true
;
}
std
::
cout
<<
"Reading
config file: "
<<
mConfigFile
<<
std
::
endl
;
logs
.
TLog
(
4
)
<<
"Trying to read
config file: "
<<
mConfigFile
<<
std
::
endl
;
std
::
ifstream
ifs
(
mConfigFile
);
if
(
!
ifs
)
{
if
(
mVM
[
"config"
].
defaulted
())
{
std
::
cout
<<
"Failed to open the default config file ("
<<
mConfigFile
<<
")"
<<
std
::
endl
;
logs
.
TLog
(
4
)
<<
"Failed to open the default config file ("
<<
mConfigFile
<<
")"
<<
std
::
endl
;
return
true
;
}
std
::
cerr
<<
"Failed to open config file: "
<<
mConfigFile
<<
std
::
endl
;
...
...
lib/prgutil.h
View file @
84c0c5e5
...
...
@@ -173,7 +173,7 @@ namespace SUBool
void
SetPrgName
(
std
::
string
prg_name
);
void
SetPrgDesc
(
std
::
string
prg_desc
);
void
SetHelpDesc
(
std
::
string
prg_help_desc
);
void
InputOutput
(
std
::
string
&
input_file
,
std
::
string
&
output_file
);
void
InputOutput
(
std
::
string
*
input_file
,
std
::
string
*
output_file
);
void
InputPair
(
const
PositFileDesc
&
first
,
const
PositFileDesc
&
second
);
bool
Parse
(
int
argc
,
char
*
argv
[]);
unsigned
Verbosity
()
const
;
...
...
@@ -181,6 +181,7 @@ namespace SUBool
const
po
::
variables_map
&
VarMap
()
const
;
po
::
options_description_easy_init
AddOptions
();
void
Add
(
const
po
::
options_description
&
desc
);
bool
HasValue
(
const
std
::
string
&
opt_name
)
const
;
};
}
// namespace SUBool
...
...
@@ -235,4 +236,10 @@ SUBool::PrgOptions::Info() const
std
::
cout
<<
mPrgName
<<
" - "
<<
mPrgDesc
<<
std
::
endl
;
}
inline
bool
SUBool
::
PrgOptions
::
HasValue
(
const
std
::
string
&
opt_name
)
const
{
return
mVM
.
count
(
opt_name
);
}
#endif
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