pccheck.cpp 23 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
32
33
 */

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

#include <cxxopts.hpp>

#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"

34
35
const std::string SUBool::kPrgName = "pccheck";
const std::string SUBool::kPrgDesc = "Checking if a CNF is PC or URC";
36
37
38
39
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.";

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

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

   config_t()
   {
65
66
67
68
69
70
71
72
73
74
75
76
77
      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;
78
79
80
   };
};

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

87
88
89
90
91
92
93
94
95
96
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;
   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
97
   SUBool::logs.DumpValue("\t", level, "no_up_backbones", conf.no_up_backbones);
98
   SUBool::logs.TLog(level)
99
       << "\tup_empower: " << static_cast<unsigned>(conf.up_empower)
100
       << std::endl;
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;
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
110
111
   SUBool::dump_enum_value(
       "\t", level, "impl_system", conf.impl_system, SUBool::kImplSystemNames);
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);
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
117
118
   SUBool::dump_enum_value(
       "\t", level, "solver_type", conf.solver_type, SUBool::kSolverTypeNames);
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
153
154
155
156
157
         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;
}

int
parse_arguments(int argc, char *argv[], config_t &conf)
{
   try
   {
158
      cxxopts::Options options(SUBool::kPrgName, SUBool::kPrgDesc);
159
      options.positional_help("[input [output]]");
160
      options.show_positional_help();
161
      bool uc = false;
162
      std::string up_one_prove;
163
164
165
166
167
168
      unsigned up_empower = 0;
      std::string algorithm;
      std::string log_enc_opts;
      std::string amo_encoding;
      std::string exone_encoding;
      std::string impl_system;
169
      std::string solver_type;
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
170
171
172
173
174
175
      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",
176
          "Back mapping of variables (names) are used wherever possible",
177
          cxxopts::value<bool>(conf.enc_conf.use_backmap)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
178
              ->default_value("false"))("e,encode",
179
          "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
180
181
          cxxopts::value<bool>(conf.encode_only)
              ->default_value("false"))("1,one-prove",
182
183
184
185
186
187
188
189
190
191
192
193
          "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 "
194
195
          "rail encoding, the implication system type is determined by option "
          "--impl-system. "
196
197
198
199
200
201
202
203
          "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
204
205
206
              ->default_value(
                  SUBool::AbsEncoder::kUPOneProveNames.at(static_cast<unsigned>(
                      conf.enc_conf.up_one_prove))))("n,no-up-backbones",
207
208
209
          "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
210
211
          cxxopts::value<bool>(conf.no_up_backbones)
              ->default_value("false"))("log-enc-opts",
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
          "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
228
              ->default_value(std::string("amf,cex,flm,cml")))("w,empower",
229
230
231
232
233
          "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
234
235
              ->default_value(std::to_string(
                  static_cast<unsigned>(conf.up_empower))))("impl-system",
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
          "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 "
266
267
          "of bits used to encode a number of level. In case of choice -1 "
          "4 "
268
269
270
271
272
273
          "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.",
274
          cxxopts::value<unsigned>(conf.enc_conf.up_level_bound)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
275
276
              ->default_value(
                  std::to_string(conf.enc_conf.up_level_bound)))("u,uc",
277
278
          "Aim for unit refutation completeness instead of "
          "propagation completeness.",
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
279
          cxxopts::value<bool>(uc)->default_value("false"))("emp-timeout",
280
281
          "Timeout for a single SAT call which looks for an empowering "
          "implicate. The timeout is in seconds as a fractional number.",
282
          cxxopts::value<double>(conf.timeouts.timeout)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
283
284
              ->default_value(std::to_string(
                  conf.timeouts.timeout)))("emp-timeout-level-base",
285
286
287
288
289
          "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 "
290
          "as B and the value of emp-timeout-level-factor as F. For a "
291
292
293
294
295
          "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.",
296
          cxxopts::value<double>(conf.timeouts.level_base)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
297
298
              ->default_value(std::to_string(
                  conf.timeouts.level_base)))("emp-timeout-level-factor",
299
300
301
302
          "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 "
303
304
305
306
          "emp-timeout-level-base for more details). If the value is "
          "higher "
          "than emp-timeout, then the value of emp-timeout is used "
          "instead. "
307
          "The timeout is passed as a fractional number specifying the "
308
          "number of seconds.",
309
          cxxopts::value<double>(conf.timeouts.level_factor)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
310
311
              ->default_value(
                  std::to_string(conf.timeouts.level_factor)))("pccheck-solver",
312
313
314
315
316
317
318
319
320
          "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
321
                  conf.solver_type)]))("b,verbosity",
322
323
          "Verbosity level of the log which is written to standard output."
          " 0 means no log is written, however messages of glucose can "
324
          "still appear.",
325
          cxxopts::value<unsigned>(conf.verbosity)
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
326
              ->default_value(std::to_string(conf.verbosity)))("amo",
327
328
329
330
          "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)
331
332
              ->default_value(SUBool::AmoEncoder::kKindAnnotation.Name(
                  conf.amo_encoding)))("exactly-one",
333
334
335
336
          "Which encoding to use for the exactly-one constraint. "
          "repr = use the representation, "
          "split = use the splitting encoding.",
          cxxopts::value<std::string>(exone_encoding)
337
338
              ->default_value(SUBool::ExOneEncoder::kKindAnnotation.Name(
                  conf.exone_encoding)))("positional",
339
340
341
          "Positional arguments: these are the arguments that are entered "
          "without an option",
          cxxopts::value<std::vector<std::string>>());
342
343
344
345
346
347
348
349
350
      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"))
      {
351
         SUBool::print_version(std::cout);
352
353
354
355
356
357
358
359
360
361
         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);
362
      if (!parse_log_enc_opts(log_enc_opts, conf.enc_conf.log_conf))
363
364
365
366
367
368
      {
         std::cerr << "Error parsing logarithmic encoding options" << std::endl;
         return 1;
      }
      try
      {
369
         conf.enc_conf.up_one_prove =
370
             SUBool::AbsEncoder::ParseUPOneProve(up_one_prove);
371
         conf.up_empower =
372
             SUBool::enum_of_int<SUBool::PCEncoder::UP_EMPOWER>(up_empower);
373
374
375
376
         conf.amo_encoding =
             SUBool::AmoEncoder::kKindAnnotation.Parse(amo_encoding);
         conf.exone_encoding =
             SUBool::ExOneEncoder::kKindAnnotation.Parse(exone_encoding);
377
378
         conf.impl_system = SUBool::enum_of_name<SUBool::LIT_IMPL_SYSTEM>(
             impl_system, SUBool::kImplSystemNames);
379
         if (SUBool::AbsEncoder::AbsConfig::OneProveRequiresImplSystem(
380
381
                 conf.enc_conf.up_one_prove)
             && conf.impl_system == SUBool::LIT_IMPL_SYSTEM::NONE)
382
         {
383
            conf.impl_system = SUBool::kDefaultImplSystem;
384
         }
385
386
387
388
389
390
391
392
393
         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
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
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
      }
      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;
}

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();
}

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

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
518
519
      throw SUBool::BadParameterException(
          "empowering_variable_name", "Bad goal");
520
521
522
523
   }
}

int
524
empower(const config_t &conf, SUBool::CompHypothesis &hyp,
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
525
    SUBool::AbsCheckerSAT &checker)
526
{
527
528
   auto emp_result = hyp.FindEmpowering(checker, false);
   if (emp_result)
529
   {
530
531
532
533
534
535
536
537
      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;
538
   }
539
540
   SUBool::logs.TLog(1) << "No empowering implicate found, formula is "
                        << goal_name(conf) << " complete" << std::endl;
541
   return 0;
542
543
544
545
546
547
548
549
550
551
}

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

552
553
554
555
556
557
558
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
559
   checker->SetSolverType(conf.solver_type);
560
561
562
563
564
565
566
567
   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
568
   checker->SetSolverType(conf.solver_type);
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
   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");
   }
}

586
int
587
execute(const config_t &conf, SUBool::CNF cnf)
588
{
589
   auto repr = cnf;
590
   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
591
       std::move(cnf), std::move(repr), true);
592
593
594
595
   if (!conf.no_up_backbones)
   {
      hyp.PropagateUPBackbones();
   }
596
   auto checker = checker_sat(conf);
597
   if (conf.encode_only)
598
   {
599
      return encode(conf, hyp, *checker);
600
   }
601
   return empower(conf, hyp, *checker);
602
603
604
605
606
}

int
main(int argc, char *argv[])
{
607
608
   config_t conf;
   int r = parse_arguments(argc, argv, conf);
609
610
611
612
   if (r != 0)
   {
      return r;
   }
613
   SUBool::logs.mVerbLevel = conf.verbosity;
614
   SUBool::CNF cnf;
615
   r = input(conf, &cnf);
616
617
618
619
620
621
622
623
624
625
   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)
626
       << "PCCompile " << SUBool::kVersionInfo << std::endl;
627

Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
628
629
   dump_config(
       conf, static_cast<unsigned>(SUBool::LogStream::LOG_LEVEL::MINLINES));
630
631
632
   SUBool::AmoEncoder::sGlobalKind = conf.amo_encoding;
   SUBool::ExOneEncoder::sGlobalKind = conf.exone_encoding;
   auto ret = execute(conf, std::move(cnf));
633
634
   return ret;
}