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

cnfgraph: Refactoring, plus now cnfgraph program accepts options for

setting colors of vertices and prefixes of vertex names.
parent f193d416
......@@ -17,12 +17,15 @@ enum class OUTPUT { GRAPHML, DOT, Last=DOT };
const std::string prg_name="cnfgraph";
const std::string prg_desc="export a CNF as a graph";
const std::string incidence_graph_var_color="red";
const std::string incidence_graph_clause_color="blue";
const std::map<std::string, SUBool::CNFGraph::KIND> graph_kind_names={
{"primal", SUBool::CNFGraph::KIND::PRIMAL},
{"dual", SUBool::CNFGraph::KIND::DUAL},
{"incidence", SUBool::CNFGraph::KIND::INCIDENCE},
{"dincidence", SUBool::CNFGraph::KIND::DINCIDENCE}
enum class GRAPH_KIND { PRIMAL, DUAL, INCIDENCE, 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}
};
struct config_t
......@@ -30,8 +33,12 @@ struct config_t
std::string input_file;
std::string output_file;
unsigned verbosity; // 0 means no output
SUBool::CNFGraph::KIND graph_kind;
GRAPH_KIND graph_kind;
OUTPUT output_type;
std::string var_prefix;
std::string var_color;
std::string clause_prefix;
std::string clause_color;
};
SUBool::LogStream logs(std::cout, static_cast<unsigned>(SUBool::LogStream::LOG_LEVEL::NONE));
......@@ -44,6 +51,10 @@ void dump_config(const config_t &conf, unsigned level)
logs.TLog(level)<<"\tverbosity: "<<conf.verbosity<<std::endl;
logs.TLog(level)<<"\tgraph_kind: "<<static_cast<unsigned>(conf.graph_kind)<<std::endl;
logs.TLog(level)<<"\toutput_type: "<<static_cast<unsigned>(conf.output_type)<<std::endl;
logs.TLog(level)<<"\tvar_prefix: "<<conf.var_prefix<<std::endl;
logs.TLog(level)<<"\tvar_color: "<<conf.var_color<<std::endl;
logs.TLog(level)<<"\tclause_prefix: "<<conf.clause_prefix<<std::endl;
logs.TLog(level)<<"\tclause_color: "<<conf.clause_color<<std::endl;
}
void print_version()
......@@ -53,7 +64,7 @@ void print_version()
std::cout<<SUBool::version_info()<<std::endl;
}
SUBool::CNFGraph::KIND
GRAPH_KIND
parse_graph_kind(const std::string &kind)
{
try
......@@ -111,7 +122,21 @@ parse_arguments(int argc, char *argv[],
"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"))
......@@ -149,6 +174,18 @@ parse_arguments(int argc, char *argv[],
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)
{
......@@ -158,6 +195,66 @@ parse_arguments(int argc, char *argv[],
return 0;
}
template<typename T, typename... Args>
int write_graph(std::ostream &os, OUTPUT output_type,
T &g, const Args&... args)
{
switch(output_type)
{
case OUTPUT::GRAPHML:
g.WriteGraphML(os, args...);
break;
case OUTPUT::DOT:
g.WriteGraphViz(os, args...);
break;
default:
throw SUBool::InvariantFailedException(
"write_graph", "Unknown output type");
}
return 0;
}
int
do_graph(const config_t &conf, const SUBool::CNF &cnf)
{
SUBool::OutputStream os(conf.output_file);
if(!os)
{
logs.TLog(0)<<"Failed to open file "
<<conf.output_file<<" for writing."<<std::endl;
return 2;
}
switch(conf.graph_kind)
{
case GRAPH_KIND::PRIMAL:
{
SUBool::PrimalGraph g(cnf);
return write_graph(os, conf.output_type, g, conf.var_prefix,
conf.var_color);
}
case GRAPH_KIND::DUAL:
{
SUBool::DualGraph g(cnf);
return write_graph(os, conf.output_type, g, conf.clause_prefix,
conf.clause_color);
}
case GRAPH_KIND::INCIDENCE:
{
SUBool::IncidenceGraph g(cnf);
return write_graph(os, conf.output_type, g, conf.var_prefix,
conf.var_color, conf.clause_prefix, conf.clause_color);
}
case GRAPH_KIND::DINCIDENCE:
{
SUBool::DIncidenceGraph g(cnf);
return write_graph(os, conf.output_type, g, conf.var_prefix,
conf.var_color, conf.clause_prefix, conf.clause_color);
}
default:
throw SUBool::InvariantFailedException("do_graph", "Unknown graph kind");
}
}
int main(int argc, char *argv[])
{
config_t conf;
......@@ -182,25 +279,5 @@ int main(int argc, char *argv[])
{
return r;
}
auto g=std::unique_ptr<SUBool::CNFGraph>(SUBool::CNFGraph::Construct(cnf, conf.graph_kind));
SUBool::OutputStream os(conf.output_file);
if(!os)
{
logs.TLog(0)<<"Failed to open file "
<<conf.output_file<<" for writing."<<std::endl;
return 2;
}
switch(conf.output_type)
{
case OUTPUT::GRAPHML:
g->WriteGraphML(os);
break;
case OUTPUT::DOT:
g->WriteGraphViz(os);
break;
default:
throw SUBool::InvariantFailedException("main", "Unknown output type");
}
return 0;
return do_graph(conf, cnf);
}
......@@ -11,66 +11,63 @@
#include "cnfgraph.h"
SUBool::CNFGraph *
SUBool::CNFGraph::Construct(const CNF &cnf, KIND kind)
const SUBool::PDCNFGraph::GraphType &
SUBool::PDCNFGraph::Graph() const
{
switch(kind)
{
case KIND::PRIMAL:
return PrimalGraph::Construct(cnf);
case KIND::DUAL:
return DualGraph::Construct(cnf);
case KIND::INCIDENCE:
return IncidenceGraph::Construct(cnf);
case KIND::DINCIDENCE:
return DIncidenceGraph::Construct(cnf);
default:
throw NotImplementedException("CNFGraph::Construct", "Not implemented for this kind");
}
return mGraph;
}
const SUBool::SimpleCNFGraph::GraphType &
SUBool::SimpleCNFGraph::Graph() const
std::pair<boost::dynamic_properties, std::string>
SUBool::PDCNFGraph::DynamicProperties(const std::string &vertex_prefix,
const std::string &vertex_color)
{
return mGraph;
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));
if(!vertex_color.empty())
{
dp.property("color",
boost::make_static_property_map<std::string>(vertex_color));
}
return std::make_pair(std::move(dp), "name");
}
void
SUBool::SimpleCNFGraph::WriteGraphML(std::ostream &out)
SUBool::PDCNFGraph::WriteGraphML(std::ostream &out,
const std::string &vertex_prefix,
const std::string &vertex_color)
{
boost::dynamic_properties dp;
dp.property("name", boost::get(boost::vertex_name_t(), mGraph));
boost::write_graphml(out, Graph(), dp, true);
auto dp=DynamicProperties(vertex_prefix, vertex_color);
boost::write_graphml(out, Graph(), dp.first, true);
}
void
SUBool::SimpleCNFGraph::WriteGraphViz(std::ostream &out)
SUBool::PDCNFGraph::WriteGraphViz(std::ostream &out,
const std::string &vertex_prefix,
const std::string &vertex_color)
{
boost::dynamic_properties dp;
dp.property("name", boost::get(boost::vertex_name_t(), mGraph));
boost::write_graphviz_dp(out, Graph(), dp, "name");
auto dp=DynamicProperties(vertex_prefix, vertex_color);
boost::write_graphviz_dp(out, Graph(), dp.first, dp.second);
}
SUBool::SimpleCNFGraph::SimpleCNFGraph(std::vector<std::pair<unsigned, unsigned> > edges,
unsigned vertex_count, const std::string &vertex_prefix, unsigned vertex_base)
SUBool::PDCNFGraph::PDCNFGraph()
{ }
void
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());
edges.resize(std::distance(edges.begin(), it));
mGraph=GraphType(edges.begin(), edges.end(), vertex_count);
boost::graph_traits<GraphType>::vertex_iterator v, v_end;
auto index=boost::get(boost::vertex_index, mGraph);
for(boost::tie(v, v_end)=boost::vertices(mGraph);
v!=v_end; ++v)
{
std::stringstream ss;
ss<<vertex_prefix<<index[*v]+vertex_base;
boost::put(boost::vertex_name_t(), mGraph, *v, ss.str());
}
}
SUBool::PrimalGraph *
SUBool::PrimalGraph::Construct(const CNF &cnf)
SUBool::PrimalGraph::PrimalGraph(const CNF &cnf)
{
std::vector<std::pair<unsigned, unsigned> > edges;
for(const auto &clause : cnf)
......@@ -83,11 +80,16 @@ SUBool::PrimalGraph::Construct(const CNF &cnf)
}
}
}
return new PrimalGraph(std::move(edges), cnf.MaxVariable(), "x", 1);
InitGraph(std::move(edges), cnf.MaxVariable());
}
SUBool::DualGraph *
SUBool::DualGraph::Construct(const CNF &cnf)
std::string
SUBool::PrimalGraph::NameOfIndex(unsigned i, const std::string &prefix)
{
return prefix+std::to_string(i+1);
}
SUBool::DualGraph::DualGraph(const CNF &cnf)
{
std::vector< std::vector<unsigned> > clauses2var(cnf.MaxVariable());
for(unsigned i=0; i<cnf.Size(); ++i)
......@@ -108,6 +110,11 @@ SUBool::DualGraph::Construct(const CNF &cnf)
}
}
}
return new DualGraph(std::move(edges), cnf.MaxVariable(), "c", 0);
InitGraph(std::move(edges), cnf.MaxVariable());
}
std::string
SUBool::DualGraph::NameOfIndex(unsigned i, const std::string &prefix)
{
return prefix+std::to_string(i);
}
......@@ -12,86 +12,92 @@
#include "normalform.h"
#include <boost/graph/adjacency_list.hpp>
#include <boost/property_map/dynamic_property_map.hpp>
namespace SUBool
{
class CNFGraph
class PDCNFGraph
{
public:
enum class KIND { PRIMAL, DUAL, INCIDENCE, DINCIDENCE, Last=DINCIDENCE };
virtual void WriteGraphML(std::ostream &out)=0;
virtual void WriteGraphViz(std::ostream &out)=0;
static CNFGraph *Construct(const CNF &cnf, KIND kind);
};
class SimpleCNFGraph : public CNFGraph
{
public:
typedef boost::property<boost::vertex_name_t, std::string> VertexNameProperty;
typedef boost::adjacency_list<boost::vecS, boost::vecS,
boost::undirectedS, VertexNameProperty> GraphType;
boost::undirectedS> GraphType;
private:
GraphType mGraph;
protected:
SimpleCNFGraph(std::vector<std::pair<unsigned, unsigned> > edges, unsigned vertex_count,
const std::string &vertex_prefix, unsigned vertex_base);
PDCNFGraph();
void InitGraph(std::vector<std::pair<unsigned, unsigned> > edges, unsigned vertex_count);
virtual std::string NameOfIndex(unsigned i, const std::string &prefix)=0;
virtual std::pair<boost::dynamic_properties, std::string> DynamicProperties(
const std::string &vertex_prefix,
const std::string &vertex_color);
public:
const GraphType &Graph() const;
virtual void WriteGraphML(std::ostream &out) override;
virtual void WriteGraphViz(std::ostream &out) override;
virtual void WriteGraphML(std::ostream &out,
const std::string &vertex_prefix,
const std::string &vertex_color="");
virtual void WriteGraphViz(std::ostream &out,
const std::string &vertex_prefix,
const std::string &vertex_color="");
};
class PrimalGraph : public SimpleCNFGraph
class PrimalGraph : public PDCNFGraph
{
PrimalGraph(std::vector<std::pair<unsigned, unsigned> > edges,
unsigned vertex_count, const std::string &vertex_prefix,
unsigned vertex_base)
: SimpleCNFGraph(std::move(edges), vertex_count, vertex_prefix,
vertex_base) {}
protected:
virtual std::string NameOfIndex(unsigned i, const std::string &prefix) override;
public:
static PrimalGraph *Construct(const CNF &cnf);
PrimalGraph(const CNF &cnf);
};
class DualGraph : public SimpleCNFGraph
class DualGraph : public PDCNFGraph
{
DualGraph(std::vector<std::pair<unsigned, unsigned> > edges,
unsigned vertex_count, const std::string &vertex_prefix,
unsigned vertex_base)
: SimpleCNFGraph(std::move(edges), vertex_count, vertex_prefix,
vertex_base) {}
protected:
virtual std::string NameOfIndex(unsigned i, const std::string &prefix) override;
public:
static DualGraph *Construct(const CNF &cnf);
DualGraph(const CNF &cnf);
};
template<class Directionality>
class IncidenceGraphT : public CNFGraph
class IncidenceGraphT
{
public:
enum class VERTEX_TYPE { VARIABLE, CLAUSE };
typedef boost::property<boost::vertex_name_t, std::string,
boost::property<boost::vertex_color_t, VERTEX_TYPE> > VertexProperty;
typedef boost::property<boost::vertex_color_t, VERTEX_TYPE> VertexProperty;
typedef boost::adjacency_list<boost::vecS, boost::vecS,
Directionality, VertexProperty> GraphType;
private:
GraphType mGraph;
IncidenceGraphT(GraphType g)
: mGraph(std::move(g)) {}
unsigned mMaxVariable;
protected:
virtual std::pair<boost::dynamic_properties, std::string> DynamicProperties(
const std::string &var_prefix,
const std::string &var_color,
const std::string &clause_prefix,
const std::string &clause_color);
public:
const GraphType &Graph() const;
virtual void WriteGraphML(std::ostream &out) override;
virtual void WriteGraphViz(std::ostream &out) override;
IncidenceGraphT(const CNF &cnf);
static IncidenceGraphT<Directionality> *Construct(const CNF &cnf);
const GraphType &Graph() const;
void WriteGraphML(std::ostream &out,
const std::string &var_prefix,
const std::string &var_color,
const std::string &clause_prefix,
const std::string &clause_color);
void WriteGraphViz(std::ostream &out,
const std::string &var_prefix,
const std::string &var_color,
const std::string &clause_prefix,
const std::string &clause_color);
};
typedef IncidenceGraphT<boost::undirectedS> IncidenceGraph;
......
......@@ -18,31 +18,33 @@ SUBool::IncidenceGraphT<Directionality>::Graph() const
template<class Directionality>
void
SUBool::IncidenceGraphT<Directionality>::WriteGraphML(std::ostream &out)
SUBool::IncidenceGraphT<Directionality>::WriteGraphML(std::ostream &out,
const std::string &var_prefix,
const std::string &var_color,
const std::string &clause_prefix,
const std::string &clause_color)
{
boost::dynamic_properties dp;
dp.property("name", boost::get(boost::vertex_name_t(), mGraph));
auto vertex_type=boost::get(boost::vertex_color, mGraph);
auto func=[](const VERTEX_TYPE &vt)->std::string{return (vt==VERTEX_TYPE::VARIABLE ? "red" : "blue");};
dp.property("color", boost::make_transform_value_property_map(func, vertex_type));
boost::write_graphml(out, Graph(), dp, true);
auto dp=DynamicProperties(var_prefix, var_color, clause_prefix,
clause_color);
boost::write_graphml(out, Graph(), dp.first, true);
}
template<class Directionality>
void
SUBool::IncidenceGraphT<Directionality>::WriteGraphViz(std::ostream &out)
SUBool::IncidenceGraphT<Directionality>::WriteGraphViz(std::ostream &out,
const std::string &var_prefix,
const std::string &var_color,
const std::string &clause_prefix,
const std::string &clause_color)
{
boost::dynamic_properties dp;
dp.property("name", boost::get(boost::vertex_name, mGraph));
auto vertex_type=boost::get(boost::vertex_color, mGraph);
auto func=[](const VERTEX_TYPE &vt)->std::string{return (vt==VERTEX_TYPE::VARIABLE ? "red" : "blue");};
dp.property("color", boost::make_transform_value_property_map(func, vertex_type));
boost::write_graphviz_dp(out, Graph(), dp, "name");
auto dp=DynamicProperties(var_prefix, var_color, clause_prefix,
clause_color);
boost::write_graphviz_dp(out, Graph(), dp.first, dp.second);
}
template<class Directionality>
SUBool::IncidenceGraphT<Directionality> *
SUBool::IncidenceGraphT<Directionality>::Construct(const CNF &cnf)
SUBool::IncidenceGraphT<Directionality>::IncidenceGraphT(const CNF &cnf)
: mMaxVariable(cnf.MaxVariable())
{
std::vector<std::pair<unsigned, unsigned> > edges;
for(unsigned i=0; i<cnf.Size(); ++i)
......@@ -59,24 +61,46 @@ SUBool::IncidenceGraphT<Directionality>::Construct(const CNF &cnf)
}
}
}
GraphType g(edges.begin(), edges.end(), cnf.MaxVariable()+cnf.Size());
mGraph=GraphType(edges.begin(), edges.end(), cnf.MaxVariable()+cnf.Size());
typename boost::graph_traits<GraphType>::vertex_iterator v, v_end;
auto index=boost::get(boost::vertex_index, g);
for(boost::tie(v, v_end)=boost::vertices(g);
auto index=boost::get(boost::vertex_index, mGraph);
for(boost::tie(v, v_end)=boost::vertices(mGraph);
v!=v_end; ++v)
{
std::stringstream ss;
if(index[*v]<cnf.MaxVariable())
{
ss<<"x"<<index[*v]+1;
boost::put(boost::vertex_color_t(), g, *v, VERTEX_TYPE::VARIABLE);
boost::put(boost::vertex_color_t(), mGraph, *v, VERTEX_TYPE::VARIABLE);
}
else
{
ss<<"c"<<index[*v]-cnf.MaxVariable();
boost::put(boost::vertex_color_t(), g, *v, VERTEX_TYPE::CLAUSE);
boost::put(boost::vertex_color_t(), mGraph, *v, VERTEX_TYPE::CLAUSE);
}
boost::put(boost::vertex_name_t(), g, *v, ss.str());
}
return new IncidenceGraphT<Directionality>(g);
}
template<class Directionality>
std::pair<boost::dynamic_properties, std::string>
SUBool::IncidenceGraphT<Directionality>::DynamicProperties(
const std::string &var_prefix,
const std::string &var_color,
const std::string &clause_prefix,
const std::string &clause_color)
{
boost::dynamic_properties dp;
auto index=boost::get(boost::vertex_index, mGraph);
auto index2name=[&](unsigned i)
{
return (i<mMaxVariable
? var_prefix+std::to_string(i+1)
: clause_prefix+std::to_string(i-mMaxVariable));
};
dp.property("name", boost::make_transform_value_property_map(index2name, index));
auto vertex_type=boost::get(boost::vertex_color, mGraph);
auto func=[&](const VERTEX_TYPE &vt)->std::string
{
return (vt==VERTEX_TYPE::VARIABLE ? var_color : clause_color);
};
dp.property("color", boost::make_transform_value_property_map(func, vertex_type));
return std::make_pair(dp, "name");
}
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