cnfdiff.cpp 4.87 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
/*
 * 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>

11
#include "normalform.h"
12
13
#include "prgutil.h"

14
15
16
17
const std::string SUBool::kPrgName = "cnfdiff";
const std::string SUBool::kPrgDesc =
    "Program for comparing two CNFs as sets of "
    "clauses (not as representations of * functions).";
18
19
20

struct config_t
{
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
21
22
23
24
25
26
   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};
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
};

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
   {
46
      cxxopts::Options options(SUBool::kPrgName, SUBool::kPrgDesc);
47
48
      options.positional_help("[input-left [input-right]]");
      std::string check_kind;
49
50
      options.add_options()("h,help", "Print help")(
          "v,version", "Print version info")("b,verbosity",
51
52
53
54
          "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)
55
56
57
58
59
60
61
62
63
64
65
66
              ->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 both CNF formulas.",
67
68
69
70
71
72
73
74
75
76
          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"))
      {
77
         SUBool::print_version(std::cout);
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
         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),
161
       SUBool::input_or_die<SUBool::CNF>(conf.file_right, SUBool::logs), conf);
162
163
   return 0;
}