cnfdiff.cpp 3.52 KB
Newer Older
1
2
3
4
5
6
7
8
/*
 * Project SUBool
 * Petr Kucera, 2020
 */
/*@file cnfdiff.cpp
 * Program for comparing two CNFs as sets of clauses (not as representations of
 * functions).
 */
9
#include "normalform.h"
10
11
#include "prgutil.h"

12
13
14
15
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).";
16
17
18

struct config_t
{
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
19
20
21
22
23
   std::string file_left{};
   std::string file_right{};
   bool suppress_first{false};
   bool suppress_second{false};
   bool suppress_third{false};
24
25
26
27
28
};

void
dump_config(const config_t &conf, unsigned level)
{
29
30
31
32
   if (!SUBool::logs.CheckLevel(level))
   {
      return;
   }
33
   SUBool::logs.TLog(level) << "Configuration:" << std::endl;
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
34
35
   SUBool::logs.DumpValue("\t", level, "file_left", conf.file_left);
   SUBool::logs.DumpValue("\t", level, "file_right", conf.file_right);
36
   SUBool::logs.DumpValue("\t", level, "verbosity", SUBool::logs.mVerbLevel);
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
37
38
39
   SUBool::logs.DumpValue("\t", level, "suppress_first", conf.suppress_first);
   SUBool::logs.DumpValue("\t", level, "suppress_second", conf.suppress_second);
   SUBool::logs.DumpValue("\t", level, "suppress_third", conf.suppress_third);
40
41
}

42
43
std::optional<config_t>
parse_arguments(int argc, char *argv[])
44
{
45
46
47
48
49
50
51
52
53
54
55
56
57
   config_t conf;
   SUBool::PrgOptions opts;
   opts.InputPair(
       {&conf.file_left, "input-left"}, {&conf.file_right, "input-right"});
   po::options_description desc("Configuration options");
   desc.add_options()(",1", po::bool_switch(&conf.suppress_first),
       "Suppress printing the clauses unique to the first CNF.")(",2",
       po::bool_switch(&conf.suppress_second),
       "Suppress printing the clauses unique to the second CNF.")(",3",
       po::bool_switch(&conf.suppress_third),
       "Suppress printing the clauses unique to the third CNF.");
   opts.Add(desc);
   if (!opts.Parse(argc, argv))
58
   {
59
      return {};
60
   }
61
   return conf;
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
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
}

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[])
{
122
123
   auto conf = parse_arguments(argc, argv);
   if (!conf)
124
   {
125
      return 1;
126
   }
127
128
129
130
   dump_config(*conf, 4);
   compare(SUBool::input_or_die<SUBool::CNF>(conf->file_left, SUBool::logs),
       SUBool::input_or_die<SUBool::CNF>(conf->file_right, SUBool::logs),
       *conf);
131
132
   return 0;
}