pccheck.cpp 23.2 KB
Newer Older
1
2
3
4
/*
 * Project SUBool
 * Petr Kucera, 2018
 */
5
6
7
/**@file pccheck.cpp
 * Program for checking if a formula is PC or URC. Can also be used to get the
 * CNF encoding PC/URC property.
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
 */

#include <array>
#include <chrono>
#include <csignal>
#include <ctime>
#include <fstream>
#include <future>
#include <iostream>

#include "cardinal.h"
#include "cnfcompress.h"
#include "logstream.h"
#include "normalform.h"
#include "pccomp.h"
#include "pcenc.h"
#include "pclearncomp.h"
#include "prgutil.h"
#include "random_utils.h"
#include "resolve.h"
#include "uccomp.h"
#include "ucenc.h"
#include "unitprop.h"

32
33
const std::string SUBool::kPrgName = "pccheck";
const std::string SUBool::kPrgDesc = "Checking if a CNF is PC or URC";
34
35
36
37
const std::string prg_help =
    "Checks if a given CNF is propagation complete (PC) or unit refutation "
    "complete (URC). Can also output the SAT encoding of the required query.";

38
39
40
41
42
43
44
45
46
47
48
enum class GOAL
{
   PC,
   UC
};

struct config_t
{
   std::string input_file{};
   std::string output_file{};
   bool encode_only{false};
49
   unsigned verbosity{3}; // 0 means no output
50
   bool no_up_backbones{false};
51
52
53
54
   SUBool::PCEncoder::UP_EMPOWER up_empower{
       SUBool::PCEncoder::UP_EMPOWER::ONE_LEVEL};
   SUBool::AbsEncoder::AbsConfig enc_conf{};
   SUBool::AbsCheckerSAT::Timeouts timeouts{};
55
   SUBool::LIT_IMPL_SYSTEM impl_system{SUBool::LIT_IMPL_SYSTEM::Default};
56
57
58
   GOAL goal{GOAL::PC};
   SUBool::AmoEncoder::KIND amo_encoding{SUBool::AmoEncoder::KIND::REPR};
   SUBool::ExOneEncoder::KIND exone_encoding{SUBool::ExOneEncoder::KIND::REPR};
59
   SUBool::SOLVER_TYPE solver_type{SUBool::SOLVER_TYPE::GLUCOSE};
60
61
62

   config_t()
   {
63
64
65
66
67
68
69
70
71
72
73
74
75
      enc_conf.up_one_prove = SUBool::AbsEncoder::UP_ONE_PROVE::MIN_LQ;
      enc_conf.log_conf.literal_levels = false;
      enc_conf.log_conf.split_size = 4;
      enc_conf.log_conf.use_bit_level = false;
      enc_conf.log_conf.add_amo_on_fire_vars = true;
      enc_conf.log_conf.add_compare_exclusivity = true;
      enc_conf.log_conf.add_force_linear_order_on_max_level = true;
      enc_conf.log_conf.contradiction_has_max_level = true;
      enc_conf.min_lq_log_weights = {2.0, 2.0, 0.0};
      enc_conf.min_lq_quad_weights = {1.0, 1.0, 0.0};
      timeouts.timeout = -1.0;
      timeouts.level_base = -1.0;
      timeouts.level_factor = 0.0;
76
77
78
   };
};

79
80
81
82
83
84
constexpr const char *
goal_name(const config_t &conf)
{
   return (conf.goal == GOAL::PC ? "PC" : "URC");
}

85
86
87
88
89
90
91
void
dump_config(const config_t &conf, unsigned level)
{
   SUBool::logs.TLog(level) << "Configuration:" << std::endl;
   SUBool::logs.TLog(level) << "\tinput_file: " << conf.input_file << std::endl;
   SUBool::logs.TLog(level)
       << "\toutput_file: " << conf.output_file << std::endl;
92
   SUBool::logs.DumpVerbosity("\t", level);
93
94
95
   SUBool::logs.TLog(level)
       << "\tencode_only: " << SUBool::bool_to_string(conf.encode_only)
       << std::endl;
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
96
   SUBool::logs.DumpValue("\t", level, "no_up_backbones", conf.no_up_backbones);
97
98
   SUBool::kLitImplSystemAnnotation.DumpValue(
       "\t", level, "impl_system", conf.impl_system);
99
100
   SUBool::PCEncoder::kUPEmpowerAnnotation.DumpValue(
       "\t", level, "up_empower", conf.up_empower);
101
102
   SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl;
   conf.enc_conf.Dump("\t\t", level);
103
   SUBool::logs.TLog(level)
104
       << "\ttimeouts.timeout: " << conf.timeouts.timeout << std::endl;
105
   SUBool::logs.TLog(level)
106
       << "\ttimeouts.level_base: " << conf.timeouts.level_base << std::endl;
107
   SUBool::logs.TLog(level)
108
       << "\ttimeouts.level_factor: " << conf.timeouts.level_factor
109
       << std::endl;
110
111
   SUBool::kLitImplSystemAnnotation.DumpValue(
       "\t", level, "impl_system", conf.impl_system);
112
   SUBool::logs.TLog(level) << "\tgoal: " << goal_name(conf) << std::endl;
113
114
115
116
   SUBool::AmoEncoder::kKindAnnotation.DumpValue(
       "\t", level, "amo_encoding", conf.amo_encoding);
   SUBool::ExOneEncoder::kKindAnnotation.DumpValue(
       "\t", level, "exone_encoding", conf.exone_encoding);
117
118
   SUBool::kSolverTypeAnnotation.DumpValue(
       "\t", level, "solver_type", conf.solver_type);
119
120
121
122
123
124
   SUBool::logs.TLog(level) << "END" << std::endl;
}

std::vector<std::string> log_enc_opt_strings = {"amf", "cex", "flm", "cml"};

bool
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
125
126
parse_log_enc_opts(
    const std::string &opt_string, SUBool::UPEncLogarithmic::Config &conf)
127
128
129
130
131
132
133
134
135
{
   std::vector<bool> opt_values(log_enc_opt_strings.size(), false);
   size_t start = 0;
   size_t end = 0;
   if (!opt_string.empty())
   {
      while (start != std::string::npos)
      {
         end = opt_string.find_first_of(',', start);
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
136
137
         auto i = std::find(log_enc_opt_strings.begin(),
             log_enc_opt_strings.end(), opt_string.substr(start, end - start));
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
         if (i == log_enc_opt_strings.end())
         {
            return false;
         }
         opt_values[i - log_enc_opt_strings.begin()] = true;
         start = end + static_cast<size_t>(end < std::string::npos);
      }
   }
   conf.add_amo_on_fire_vars = opt_values[0];
   conf.add_compare_exclusivity = opt_values[1];
   conf.add_force_linear_order_on_max_level = opt_values[2];
   conf.contradiction_has_max_level = opt_values[3];
   return true;
}

153
154
std::optional<config_t>
parse_arguments(int argc, char *argv[])
155
{
156
157
158
159
160
161
162
163
164
165
   config_t conf;
   SUBool::PrgOptions opts(true);
   opts.SetHelpDesc(prg_help);
   opts.InputOutput(&conf.input_file, &conf.output_file);
   if (!opts.Parse(argc, argv))
   {
      return {};
   }
   return conf;
#if 0
166
167
   try
   {
168
      cxxopts::Options options(SUBool::kPrgName, SUBool::kPrgDesc);
169
      options.positional_help("[input [output]]");
170
      options.show_positional_help();
171
      bool uc = false;
172
      std::string up_one_prove;
173
174
175
176
177
178
      unsigned up_empower = 0;
      std::string algorithm;
      std::string log_enc_opts;
      std::string amo_encoding;
      std::string exone_encoding;
      std::string impl_system;
179
      std::string solver_type;
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
180
181
182
183
184
185
      options.add_options()("h,help", "Print help")(
          "v,version", "Print version info")("i,input",
          "Input file with a CNF in DIMACS format",
          cxxopts::value<std::string>(conf.input_file))("o,output",
          "Output file with the encoding CNF in DIMACS format",
          cxxopts::value<std::string>(conf.output_file))("d,dump",
186
          "Back mapping of variables (names) are used wherever possible",
187
          cxxopts::value<bool>(conf.enc_conf.use_backmap)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
188
              ->default_value("false"))("e,encode",
189
          "Do not check, just write the encoding to the output file",
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
190
191
          cxxopts::value<bool>(conf.encode_only)
              ->default_value("false"))("1,one-prove",
192
193
194
195
196
197
198
199
200
201
202
203
          "What kind of encoding should be used for 1-provability. It is "
          "possible to specify the value with a number or a string. The list "
          "below contains a string value with a number within the brackets."
          "quadratic_equiv (0) = quadratic encoding with equivalences. "
          "quadratic_one_sided (1) = quadratic encoding with implications. "
          "logarithmic (2) = logarithmic encoding. "
          "max_level (3) = max based encoding. "
          "min_lq (4) = the smaller one from quadratic encoding with "
          "implications and the logarithmic encoding, the choice is made "
          "before each SAT call."
          "quad_impl_system (5) = quadratic which uses an implication system "
          "to represent dual "
204
205
          "rail encoding, the implication system type is determined by option "
          "--impl-system. "
206
207
208
209
210
211
212
213
          "impl_level (6) = based on implication system where levels are "
          "encoded in binary, "
          "the implication system type is determined by option --impl-system. "
          "scc_unary (7) = based on the SCCs of implication system, unary "
          "encoding of levels. "
          "scc_binary (8) = based on the SCCs of implication system, binary "
          "encoding of levels. ",
          cxxopts::value<std::string>(up_one_prove)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
214
215
216
              ->default_value(
                  SUBool::AbsEncoder::kUPOneProveNames.at(static_cast<unsigned>(
                      conf.enc_conf.up_one_prove))))("n,no-up-backbones",
217
218
219
          "Do NOT perform propagation of literals which can be derived by unit "
          "propagation from the input formula. This is useful for checking the "
          "construction of an encoding.",
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
220
221
          cxxopts::value<bool>(conf.no_up_backbones)
              ->default_value("false"))("log-enc-opts",
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
          "Options to logarithmic encoding modifying some of its features. "
          "It "
          "is a string composed of comma separated option strings which "
          "specifies which additional parts should be added to the "
          "encoding. "
          "Possible values specifying the features are: "
          "amf -- AMO on fire variables for each derived literal will be "
          "part "
          "of the encoding. "
          "cex -- Comparison exclusivity clauses will be added to the "
          "encoding. "
          "flm -- Clauses forcing linear order when the number of levels is "
          "maximum will be added to the encoding. "
          "cml -- A variable is contradictory if and only its level has all "
          "ones.",
          cxxopts::value<std::string>(log_enc_opts)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
238
              ->default_value(std::string("amf,cex,flm,cml")))("w,empower",
239
240
241
242
243
          "What kind of encoding should be used for empowerment. "
          "0 = quadratic encoding with equivalences. "
          "1 = quadratic encoding with implications. "
          "2 = one level encoding. ",
          cxxopts::value<unsigned>(up_empower)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
244
245
              ->default_value(std::to_string(
                  static_cast<unsigned>(conf.up_empower))))("impl-system",
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
          "Determines the type of an implication system to be used when "
          "required by encoding of empowerement or 1-provability. "
          "'none' -- no implication system (must not be used with any choice "
          "of "
          "one-prove and empower options which requires an implication system. "
          "Should be used with other option combinations. "
          "'drenc' -- use plain dual rail encoding. "
          "'irredundant' -- make the dual rail encoding irredundant (both body "
          "and right). "
          "'gdbasis' -- use GD basis of the dual rail encoding. "
          "'gdbasis_right_irred' -- construct GD basis and make it right "
          "irredundant. "
          "'body_minimal' -- make the dual rail encoding body minimal (like GD "
          "basis but without left saturation). "
          "'body_minimal_irred' -- make the dual rail encoding body minimal "
          "and right irredundant. "
          "The default value depends on other options, it is none for the "
          "combination of options one-prove and empower which do not require "
          "any implication system, and "
              + SUBool::DefaultImplSystemName()
              + " for the option combination which needs an implication "
                "system. ",
          cxxopts::value<std::string>(impl_system)->default_value("none"))(
          "l,level",
          "Maximum level of unit propagation for "
          "1-provability. In case of compilation, the compilation "
          "stops when no empowering implicate with level at most l is "
          "found. Value 0 means, the level is not bounded. Note that "
          "in case of quadratic encoding this is really the maximum "
          "level, in case of logarithmic encoding this is the number "
276
277
          "of bits used to encode a number of level. In case of choice -1 "
          "4 "
278
279
280
281
282
283
          "when the minimum of quadratic and logarithmic encoding is "
          "considered, the level bounds the number of level of the "
          "quadratic "
          "encoding while the number of levels of the logarithmic encoding "
          "is "
          "bounded to the logarithm of the parameter rounded up.",
284
          cxxopts::value<unsigned>(conf.enc_conf.up_level_bound)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
285
286
              ->default_value(
                  std::to_string(conf.enc_conf.up_level_bound)))("u,uc",
287
288
          "Aim for unit refutation completeness instead of "
          "propagation completeness.",
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
289
          cxxopts::value<bool>(uc)->default_value("false"))("emp-timeout",
290
291
          "Timeout for a single SAT call which looks for an empowering "
          "implicate. The timeout is in seconds as a fractional number.",
292
          cxxopts::value<double>(conf.timeouts.timeout)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
293
294
              ->default_value(std::to_string(
                  conf.timeouts.timeout)))("emp-timeout-level-base",
295
296
297
298
299
          "This parameter together with emp-timeout-level-factor allows to "
          "set the timeout for a single SAT which looks for an empowering "
          "implicate depending on the number of levels of unit propagation "
          "allowed in the encoding. Denote the value of "
          "emp-timeout-level-base "
300
          "as B and the value of emp-timeout-level-factor as F. For a "
301
302
303
304
305
          "level L which is neither 0 nor maximum (i.e. the number of "
          "variables), the timeout is set as B+F*L. If the value is higher "
          "than emp-timeout, then the value of emp-timeout is used instead. "
          "The timeout is passed as a fractional number specifying the number "
          "of seconds.",
306
          cxxopts::value<double>(conf.timeouts.level_base)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
307
308
              ->default_value(std::to_string(
                  conf.timeouts.level_base)))("emp-timeout-level-factor",
309
310
311
312
          "This parameter together with emp-timeout-level-base allows to "
          "set the timeout for a single SAT which looks for an empowering "
          "implicate depending on the number of levels of unit propagation "
          "allowed in the encoding (see the description of "
313
314
315
316
          "emp-timeout-level-base for more details). If the value is "
          "higher "
          "than emp-timeout, then the value of emp-timeout is used "
          "instead. "
317
          "The timeout is passed as a fractional number specifying the "
318
          "number of seconds.",
319
          cxxopts::value<double>(conf.timeouts.level_factor)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
320
321
              ->default_value(
                  std::to_string(conf.timeouts.level_factor)))("pccheck-solver",
322
323
324
325
326
327
328
329
330
          "Solver to be used for the PC check. "
          "glucose = use glucose, "
#if HAS_KISSAT
          "kissat = use kissat.",
#else
          "(kissat NOT AVAILABLE).",
#endif
          cxxopts::value<std::string>(solver_type)
              ->default_value(SUBool::kSolverTypeNames[static_cast<unsigned>(
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
331
                  conf.solver_type)]))("b,verbosity",
332
333
          "Verbosity level of the log which is written to standard output."
          " 0 means no log is written, however messages of glucose can "
334
          "still appear.",
335
          cxxopts::value<unsigned>(conf.verbosity)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
336
              ->default_value(std::to_string(conf.verbosity)))("amo",
337
338
339
340
          "Which encoding to use for the at-most-one constraint. "
          "repr = use the representation, "
          "seq = use the sequential encoding.",
          cxxopts::value<std::string>(amo_encoding)
341
342
              ->default_value(SUBool::AmoEncoder::kKindAnnotation.Name(
                  conf.amo_encoding)))("exactly-one",
343
344
345
346
          "Which encoding to use for the exactly-one constraint. "
          "repr = use the representation, "
          "split = use the splitting encoding.",
          cxxopts::value<std::string>(exone_encoding)
347
348
              ->default_value(SUBool::ExOneEncoder::kKindAnnotation.Name(
                  conf.exone_encoding)))("positional",
349
350
351
          "Positional arguments: these are the arguments that are entered "
          "without an option",
          cxxopts::value<std::vector<std::string>>());
352
353
354
355
356
357
358
359
360
      options.parse_positional({"input", "output", "positional"});
      auto result = options.parse(argc, argv);
      if (result.count("help"))
      {
         std::cout << options.help() << std::endl;
         return 1;
      }
      if (result.count("version"))
      {
361
         SUBool::print_version(std::cout);
362
363
364
365
366
367
368
369
370
371
         return 1;
      }
      if (result.count("positional"))
      {
         std::cerr << "Multiple files passed as parameters, ";
         std::cerr << "only input and output are allowed" << std::endl;
         std::cerr << options.help() << std::endl;
         return 1;
      }
      conf.goal = (uc ? GOAL::UC : GOAL::PC);
372
      if (!parse_log_enc_opts(log_enc_opts, conf.enc_conf.log_conf))
373
374
375
376
377
378
      {
         std::cerr << "Error parsing logarithmic encoding options" << std::endl;
         return 1;
      }
      try
      {
379
         conf.enc_conf.up_one_prove =
380
             SUBool::AbsEncoder::ParseUPOneProve(up_one_prove);
381
         conf.up_empower =
382
             SUBool::enum_of_int<SUBool::PCEncoder::UP_EMPOWER>(up_empower);
383
384
385
386
         conf.amo_encoding =
             SUBool::AmoEncoder::kKindAnnotation.Parse(amo_encoding);
         conf.exone_encoding =
             SUBool::ExOneEncoder::kKindAnnotation.Parse(exone_encoding);
387
388
         conf.impl_system = SUBool::enum_of_name<SUBool::LIT_IMPL_SYSTEM>(
             impl_system, SUBool::kImplSystemNames);
389
         if (SUBool::AbsEncoder::AbsConfig::OneProveRequiresImplSystem(
390
391
                 conf.enc_conf.up_one_prove)
             && conf.impl_system == SUBool::LIT_IMPL_SYSTEM::NONE)
392
         {
393
            conf.impl_system = SUBool::kDefaultImplSystem;
394
         }
395
396
397
398
399
400
401
402
403
         conf.solver_type = SUBool::enum_of_name<SUBool::SOLVER_TYPE>(
             solver_type, SUBool::kSolverTypeNames);
#if !HAS_KISSAT
         if (conf.solver_type == SUBool::SOLVER_TYPE::KISSAT)
         {
            std::cerr << "Kissat not available" << std::endl;
            return 1;
         }
#endif
404
405
406
407
408
409
410
411
412
413
414
415
416
417
      }
      catch (SUBool::BadParameterException &e)
      {
         std::cerr << "Error parsing parameter values: " << e.what()
                   << std::endl;
         return 1;
      }
   }
   catch (const cxxopts::OptionException &e)
   {
      std::cerr << "Error parsing options: " << e.what() << std::endl;
      return 1;
   }
   return 0;
418
#endif
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
}

int
input(const config_t &conf, SUBool::CNF *cnf)
{
   if (cnf == nullptr)
   {
      throw SUBool::NullPointerException("input", "cnf == nullptr");
   }

   if (conf.input_file.empty() || conf.input_file == "-")
   {
      std::cin >> *cnf;
   }
   else
   {
      std::ifstream in(conf.input_file);
      if (!in)
      {
         std::cerr << "Failed to open file '" << conf.input_file
                   << "' for reading" << std::endl;
         return 2;
      }
      in >> *cnf;
   }
   return 0;
}

template <class T, class R>
R
wait_with_timeout(double timeout, std::future<R> &fut, T &comp)
{
   if (timeout > 0.0)
   {
      if (fut.wait_for(std::chrono::duration<double>(timeout))
          == std::future_status::timeout)
      {
         comp.Abort("timed out");
         comp.PrintStatistics(1);
         fut.wait();
         return SUBool::AbsComp::RESULT::TIMED_OUT; //_Exit(3);
      }
   }
   else
   {
      fut.wait();
   }
   return fut.get();
}

469
int
470
encode(const config_t &conf, const SUBool::CompHypothesis &hyp,
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
471
    SUBool::AbsCheckerSAT &checker)
472
{
473
474
475
476
   auto cnf = hyp.GetHypothesis(false);
   auto enc = checker.Encoder(conf.enc_conf.up_level_bound);
   SUBool::ClausesToLiterals cl2lit(cnf);
   SUBool::LitImplSystem impl_system;
477
   SUBool::LitISGraph scc_graph;
478
479
480
   if (enc->RequiresImplSystem())
   {
      impl_system = SUBool::init_lit_impl_system(cnf, conf.impl_system);
481
482
483
484
      if (enc->RequiresSCCGraph())
      {
         scc_graph = SUBool::LitISGraph(impl_system);
      }
485
   }
486
   enc->BuildEncoding(cnf, cl2lit, impl_system, scc_graph);
487
   SUBool::OutputStream os(conf.output_file);
488
489
490
   if (!os)
   {
      SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::NONE)
491
          << "[encode] Failed to open file '" << conf.output_file
492
493
494
          << "' for writing" << std::endl;
      return 2;
   }
495
   enc->WriteEncoding(os);
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
   return 0;
}

const std::string kPCEmpoweringImplicateName = "empowering implicate";
const std::string kUCEmpoweringImplicateName = "URC empowering implicate";
const std::string kPCEmpoweringVarName = "empowering variable";
const std::string kUCEmpoweringVarName = "extending variable";

const std::string &
empowering_implicate_name(const config_t &conf)
{
   switch (conf.goal)
   {
   case GOAL::PC:
      return kPCEmpoweringImplicateName;
   case GOAL::UC:
      return kUCEmpoweringImplicateName;
   default:
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
514
515
      throw SUBool::BadParameterException(
          "empowering_implicate_name", "Bad goal");
516
517
518
519
520
521
522
523
524
525
526
527
528
   }
}

const std::string &
empowering_variable_name(const config_t &conf)
{
   switch (conf.goal)
   {
   case GOAL::PC:
      return kPCEmpoweringVarName;
   case GOAL::UC:
      return kUCEmpoweringVarName;
   default:
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
529
530
      throw SUBool::BadParameterException(
          "empowering_variable_name", "Bad goal");
531
532
533
534
   }
}

int
535
empower(const config_t &conf, SUBool::CompHypothesis &hyp,
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
536
    SUBool::AbsCheckerSAT &checker)
537
{
538
539
   auto emp_result = hyp.FindEmpowering(checker, false);
   if (emp_result)
540
   {
541
542
543
544
545
546
547
548
      auto emp_var = checker.LastWitnessVariable();
      // TODO: change the last parameter to true if consistency is checked
      // before calling empower
      auto clause = hyp.PrimeSubimplicate(*emp_result, emp_var, false);
      SUBool::logs.TLog(1) << "Found empowering implicate " << clause
                           << " with empowered variable " << emp_var
                           << std::endl;
      return 1;
549
   }
550
551
   SUBool::logs.TLog(1) << "No empowering implicate found, formula is "
                        << goal_name(conf) << " complete" << std::endl;
552
   return 0;
553
554
555
556
557
558
559
560
561
562
}

void
terminate(int signal)
{
   std::stringstream ss;
   ss << "terminated by signal " << signal;
   _Exit(2);
}

563
564
565
566
567
568
569
std::unique_ptr<SUBool::PCCheckerSAT>
pc_checker_sat(const config_t &conf)
{
   auto checker = std::make_unique<SUBool::PCCheckerSAT>();
   SUBool::PCEncoder::Config check_conf(conf.enc_conf);
   check_conf.up_empower = conf.up_empower;
   checker->Init(check_conf, false, conf.timeouts);
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
570
   checker->SetSolverType(conf.solver_type);
571
572
573
574
575
576
577
578
   return checker;
}

std::unique_ptr<SUBool::UCCheckerSAT>
urc_checker_sat(const config_t &conf)
{
   auto checker = std::make_unique<SUBool::UCCheckerSAT>();
   checker->Init(conf.enc_conf, false, conf.timeouts);
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
579
   checker->SetSolverType(conf.solver_type);
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
   return checker;
}

std::unique_ptr<SUBool::AbsCheckerSAT>
checker_sat(const config_t &conf)
{
   switch (conf.goal)
   {
   case GOAL::PC:
      return pc_checker_sat(conf);
   case GOAL::UC:
      return urc_checker_sat(conf);
   default:
      throw SUBool::BadParameterException("checker_sat", "Unknown goal");
   }
}

597
int
598
execute(const config_t &conf, SUBool::CNF cnf)
599
{
600
   auto repr = cnf;
601
   SUBool::CompHypothesis hyp(SUBool::MINIMIZE_METHOD::FULL, conf.impl_system,
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
602
       std::move(cnf), std::move(repr), true);
603
604
605
606
   if (!conf.no_up_backbones)
   {
      hyp.PropagateUPBackbones();
   }
607
   auto checker = checker_sat(conf);
608
   if (conf.encode_only)
609
   {
610
      return encode(conf, hyp, *checker);
611
   }
612
   return empower(conf, hyp, *checker);
613
614
615
616
617
}

int
main(int argc, char *argv[])
{
618
619
   auto conf = parse_arguments(argc, argv);
   if (!conf)
620
   {
621
      return 1;
622
623
   }
   SUBool::CNF cnf;
624
   auto r = input(*conf, &cnf);
625
626
627
628
629
630
631
632
633
634
   if (r != 0)
   {
      return r;
   }

   std::signal(SIGTERM, terminate);
   std::signal(SIGQUIT, terminate);
   std::signal(SIGINT, terminate);

   SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::MINLINES)
635
       << "PCCheck" << SUBool::kVersionInfo << std::endl;
636

637
638
639
640
   dump_config(*conf, 3);
   SUBool::AmoEncoder::sGlobalKind = conf->amo_encoding;
   SUBool::ExOneEncoder::sGlobalKind = conf->exone_encoding;
   auto ret = execute(*conf, std::move(cnf));
641
642
   return ret;
}