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

Small fixes

parent ab6c3a87
......@@ -16,12 +16,12 @@ const std::string prg_desc = "Program for comparing two CNFs as sets of "
struct config_t
{
std::string file_left;
std::string file_right;
unsigned verbosity; // 0 means no output
bool suppress_first;
bool suppress_second;
bool suppress_third;
std::string file_left{};
std::string file_right{};
unsigned verbosity{3}; // 0 means no output
bool suppress_first{false};
bool suppress_second{false};
bool suppress_third{false};
};
void
......
......@@ -41,15 +41,15 @@ const std::map<std::string, GRAPH_KIND> graph_kind_names = {
struct config_t
{
std::string input_file;
std::string output_file;
unsigned verbosity; // 0 means no output
GRAPH_KIND graph_kind;
OUTPUT output_type;
std::string var_prefix;
std::string var_color;
std::string clause_prefix;
std::string clause_color;
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};
std::string var_prefix{"x"};
std::string var_color{};
std::string clause_prefix{"c"};
std::string clause_color{};
};
void
......
......@@ -21,10 +21,10 @@
struct config_t
{
std::string input_file;
std::string output_file;
bool unitprop;
unsigned verbosity;
std::string input_file{};
std::string output_file{};
bool unitprop{false};
unsigned verbosity{3};
};
config_t
......
......@@ -20,10 +20,10 @@ const std::string prg_desc = "Make a given DNNF smooth.";
struct config_t
{
std::string input_file;
std::string output_file;
unsigned verbosity; // 0 means no output
bool check_only;
std::string input_file{};
std::string output_file{};
unsigned verbosity{3}; // 0 means no output
bool check_only{false};
};
void
......
......@@ -23,9 +23,9 @@ const std::string prg_desc =
struct config_t
{
std::string input_file;
std::string output_file;
unsigned verbosity; // 0 means no output
std::string input_file{};
std::string output_file{};
unsigned verbosity{3}; // 0 means no output
};
void
......
......@@ -19,64 +19,62 @@ SUBool::PDCNFGraph::Graph() const
std::pair<boost::dynamic_properties, std::string>
SUBool::PDCNFGraph::DynamicProperties(const std::string &vertex_prefix,
const std::string &vertex_color)
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));
if(!vertex_color.empty())
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));
boost::make_static_property_map<std::string>(vertex_color));
}
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);
auto dp = DynamicProperties(vertex_prefix, vertex_color);
boost::write_graphml(out, Graph(), dp.first, true);
}
void
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);
auto dp = DynamicProperties(vertex_prefix, vertex_color);
boost::write_graphviz_dp(out, Graph(), dp.first, dp.second);
}
SUBool::PDCNFGraph::PDCNFGraph()
{ }
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());
auto it = std::unique(edges.begin(), edges.end());
edges.resize(std::distance(edges.begin(), it));
mGraph=GraphType(edges.begin(), edges.end(), vertex_count);
mGraph = GraphType(edges.begin(), edges.end(), vertex_count);
}
SUBool::PrimalGraph::PrimalGraph(const CNF &cnf)
{
std::vector<std::pair<unsigned, unsigned> > edges;
for(const auto &clause : cnf)
std::vector<std::pair<unsigned, unsigned>> edges;
for (const auto &clause : cnf)
{
for(unsigned i=0; i<clause.Size(); ++i)
for (unsigned i = 0; i < clause.Size(); ++i)
{
for(unsigned j=i+1; j<clause.Size(); ++j)
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);
}
}
}
......@@ -86,25 +84,25 @@ SUBool::PrimalGraph::PrimalGraph(const CNF &cnf)
std::string
SUBool::PrimalGraph::NameOfIndex(unsigned i, const std::string &prefix)
{
return prefix+std::to_string(i+1);
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)
std::vector<std::vector<unsigned>> clauses2var(cnf.MaxVariable());
for (unsigned i = 0; i < cnf.Size(); ++i)
{
for(const auto &lit : cnf[i])
for (const auto &lit : cnf[i])
{
clauses2var[lit.Variable()-1].push_back(i);
clauses2var[lit.Variable() - 1].push_back(i);
}
}
std::vector<std::pair<unsigned, unsigned> > edges;
for(const auto &clauses : clauses2var)
std::vector<std::pair<unsigned, unsigned>> edges;
for (const auto &clauses : clauses2var)
{
for(unsigned i=0; i<clauses.size(); ++i)
for (unsigned i = 0; i < clauses.size(); ++i)
{
for(unsigned j=i+1; j<clauses.size(); ++j)
for (unsigned j = i + 1; j < clauses.size(); ++j)
{
edges.emplace_back(clauses[i], clauses[j]);
}
......@@ -116,5 +114,5 @@ SUBool::DualGraph::DualGraph(const CNF &cnf)
std::string
SUBool::DualGraph::NameOfIndex(unsigned i, const std::string &prefix)
{
return prefix+std::to_string(i);
return prefix + std::to_string(i);
}
......@@ -43,7 +43,7 @@ SUBool::IncidenceGraphT<Directionality>::WriteGraphViz(
template <class Directionality>
SUBool::IncidenceGraphT<Directionality>::IncidenceGraphT(const CNF &cnf)
: mMaxVariable(cnf.MaxVariable())
: mGraph(), mMaxVariable(cnf.MaxVariable())
{
std::vector<std::pair<unsigned, unsigned>> edges;
for (unsigned i = 0; i < cnf.Size(); ++i)
......
......@@ -18,7 +18,7 @@ SUBool::CompHypothesis::CompHypothesis(MINIMIZE_METHOD minimize_method)
mMinSubimplicant(&mRepresentation),
mSemPropagator(mSolver.GetSolverPtr(), &(mOneProveRepr.UP()),
&mMinSubimplicant),
mMinimizeMethod(minimize_method)
mMutex(), mMinimizeMethod(minimize_method)
{
}
......@@ -31,7 +31,7 @@ SUBool::CompHypothesis::CompHypothesis(MINIMIZE_METHOD minimize_method, CNF cnf,
mSemPropagator(mSolver.GetSolverPtr(),
safe ? &(mOneProveHyp.UP()) : &(mOneProveRepr.UP()),
&mMinSubimplicant),
mMinimizeMethod(minimize_method)
mMutex(), mMinimizeMethod(minimize_method)
{
}
......
Supports Markdown
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