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

New program cnfdiff for checking differences between CNF formulas

parent 6a027895
......@@ -18,6 +18,9 @@ target_link_libraries (cnfprime subool ${GLUCOSE_LIB})
add_executable (cnfcomp cnfcomp.cpp)
target_link_libraries (cnfcomp subool ${GLUCOSE_LIB})
add_executable (cnfdiff cnfdiff.cpp)
target_link_libraries (cnfdiff subool)
add_executable (cnfgraph cnfgraphx.cpp)
target_link_libraries (cnfgraph subool)
......
......@@ -3,7 +3,7 @@
* Petr Kucera, 2018
*/
/**@file cnfcomp.cpp
* Program for comparing two CNFs.
* Program for comparing two functions represented by CNFs.
*/
#include <cxxopts.hpp>
......@@ -29,7 +29,8 @@ const std::map<std::string, CheckKind> check_kind_names = {
{"leq", CheckKind::LEQ}, {"geq", CheckKind::GEQ}};
const std::string prg_name = "cnfcomp";
const std::string prg_desc = "compare two CNF formulas";
const std::string prg_desc =
"compare two functions represented by CNF formulas";
struct config_t
{
......@@ -67,14 +68,6 @@ parse_check_kind(const std::string &check_kind)
}
}
void
print_version()
{
std::cout << prg_name << " - " << prg_desc << std::endl;
std::cout << SUBool::author_year_info() << '\n';
std::cout << SUBool::version_info() << std::endl;
}
int
parse_arguments(int argc, char *argv[], config_t &conf)
{
......@@ -112,7 +105,7 @@ parse_arguments(int argc, char *argv[], config_t &conf)
}
if (result.count("version"))
{
print_version();
SUBool::print_version(prg_name, prg_desc);
return 1;
}
if (result.count("positional"))
......
/*
* Project SUBool
* Petr Kucera, 2020
*/
/*@file cnfdiff.cpp
* Program for comparing two CNFs as sets of clauses (not as representations of
* functions).
*/
#include <cxxopts.hpp>
#include "prgutil.h"
const std::string prg_name = "cnfdiff";
const std::string prg_desc = "Program for comparing two CNFs as sets of "
"clauses (not as representations of * functions).";
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;
};
void
dump_config(const config_t &conf, unsigned level)
{
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::dump_value("\t", level, "file_left", conf.file_left);
SUBool::dump_value("\t", level, "file_right", conf.file_right);
SUBool::dump_value("\t", level, "verbosity", conf.verbosity);
SUBool::dump_value("\t", level, "suppress_first", conf.suppress_first);
SUBool::dump_value("\t", level, "suppress_second", conf.suppress_second);
SUBool::dump_value("\t", level, "suppress_third", conf.suppress_third);
}
int
parse_arguments(int argc, char *argv[], config_t &conf)
{
try
{
cxxopts::Options options(prg_name, prg_desc);
options.positional_help("[input-left [input-right]]");
std::string check_kind;
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))(
"l,input-left", "The left hand input file",
cxxopts::value<std::string>(conf.file_left))(
"r,input-right", "The right hand input file",
cxxopts::value<std::string>(conf.file_right))(
"1", "Suppress printing the clauses unique to the first CNF.",
cxxopts::value<bool>(conf.suppress_first)->default_value("false"))(
"2", "Suppress printing the clauses unique to the second CNF.",
cxxopts::value<bool>(conf.suppress_second)->default_value("false"))(
"3", "Suppress printing the clauses which are in bothCNF formulas.",
cxxopts::value<bool>(conf.suppress_third)->default_value("false"));
options.parse_positional({"input-left", "input-right", "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(prg_name, prg_desc);
return 1;
}
if (result.count("positional"))
{
SUBool::logs.TLog(0) << "Multiple files passed as parameters, ";
SUBool::logs.TLog(0) << "only two input files allowed" << std::endl;
SUBool::logs.TLog(0) << options.help() << std::endl;
return 1;
}
}
catch (const cxxopts::OptionException &e)
{
std::cerr << "Error parsing options: " << e.what() << std::endl;
return 1;
}
return 0;
}
void
compare(SUBool::CNF left, SUBool::CNF right, config_t &conf)
{
left.Sort();
right.Sort();
auto i_left = left.cbegin();
auto i_right = right.cbegin();
SUBool::AnnotatedCNF only_first;
SUBool::AnnotatedCNF only_second;
SUBool::AnnotatedCNF both;
while (i_left != left.cend() && i_right != right.cend())
{
if (*i_left < *i_right)
{
only_first.nf.PushBack(*i_left);
++i_left;
continue;
}
if (*i_right < *i_left)
{
only_second.nf.PushBack(*i_right);
++i_right;
continue;
}
both.nf.PushBack(*i_right);
++i_left;
++i_right;
}
while (i_left != left.end())
{
only_first.nf.PushBack(*i_left);
++i_left;
}
while (i_right != right.end())
{
only_second.nf.PushBack(*i_right);
++i_right;
}
if (!conf.suppress_first)
{
only_first.dimacs_annotation = "c Clauses unique to " + conf.file_left;
std::cout << only_first << std::endl;
}
if (!conf.suppress_second)
{
only_second.dimacs_annotation = "c Clauses unique to " + conf.file_right;
std::cout << only_second << std::endl;
}
if (!conf.suppress_third)
{
both.dimacs_annotation = "c Clauses in both files";
std::cout << both << std::endl;
}
}
int
main(int argc, char *argv[])
{
config_t conf;
int r = parse_arguments(argc, argv, conf);
if (r != 0)
{
return r;
}
compare(SUBool::input_or_die<SUBool::CNF>(conf.file_left, SUBool::logs),
SUBool::input_or_die<SUBool::CNF>(conf.file_right, SUBool::logs),
conf);
return 0;
}
......@@ -87,6 +87,7 @@ namespace SUBool
const tElements &Elements() const &;
tElements Elements() &&;
void Sort();
template <class Compare> void Sort(Compare comp);
void Set(size_t index, ElementType element);
......
......@@ -512,6 +512,13 @@ SUBool::NormalForm<ElementType, DETERMINING_VALUE>::Sort(Compare comp)
std::sort(mElements.begin(), mElements.end(), comp);
}
template <class ElementType, bool DETERMINING_VALUE>
void
SUBool::NormalForm<ElementType, DETERMINING_VALUE>::Sort()
{
std::sort(mElements.begin(), mElements.end());
}
template <class T>
std::ostream &
SUBool::operator<<(std::ostream &output, const AnnotatedNF<T> &nf)
......
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