pccompile.cpp 33.6 KB
Newer Older
1
2
/*
 * Project SUBool
3
 * Petr Kucera, 2018
4
5
 */
/**@file pccompile.cpp
6
 * Program for PC compilation via adding new empowering implicates.
7
8
 */

9
#include <array>
10
#include <chrono>
11
#include <csignal>
12
13
14
15
#include <ctime>
#include <fstream>
#include <future>
#include <iostream>
16

17
#include "cardinal.h"
18
19
#include "cnfcompress.h"
#include "logstream.h"
20
#include "normalform.h"
21
#include "pc_opt.h"
22
#include "pccomp.h"
23
#include "pcenc.h"
24
#include "pclearncomp.h"
25
#include "prgutil.h"
26
#include "random_utils.h"
27
#include "resolve.h"
28
#include "uccomp.h"
29
30
#include "ucenc.h"
#include "unitprop.h"
31

32
33
34
const std::string SUBool::kPrgName = "pccompile";
const std::string SUBool::kPrgDesc =
    "compiling a CNF into a propagation complete or unit refutation complete "
35
36
37
    "CNF.";
const std::string prg_help =
    "Implements an incremental algorithm based on adding empowering "
38
39
    "implicates and a learning algorithm";

40
41
struct config_t
{
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
42
43
   std::string input_file{};
   std::string output_file{};
44
   bool minimize{false};
45
   SUBool::MINIMIZE_METHOD minimize_method{SUBool::MINIMIZE_METHOD::FULL};
46
47
   SUBool::PCCompAlgorithmOptions::ALGORITHM algorithm{
       SUBool::PCCompAlgorithmOptions::kDefaultAlgorithm};
48
49
   bool level_simplify{true};                // simplification at level increase
   unsigned verbosity{3};                    // 0 means no output
50
   bool use_empty_initial_hypothesis{false}; // For PCLearnComp
51
52
53
   unsigned pccheck_random_rounds{100};
   unsigned pccheck_random_budget{10};
   unsigned pccheck_random_budget_inc{1};
54
55
   SUBool::PCLearnComp::INITIAL_NEGATIVES initial_negatives{
       SUBool::PCLearnComp::INITIAL_NEGATIVES::ALL_EMPOWERING};
56
   unsigned long long random_seed{0};
57
   double timeout{-1.0};
58
   SUBool::AbsComp::BaseConfig comp_base_config{
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
59
60
61
62
63
       SUBool::PCEncoder::UP_EMPOWER::ONE_LEVEL,
       50,
       true,
       SUBool::AbsComp::PREPROCESS_METHOD::PRIME_MINIMIZE,
       true,
64
       SUBool::MINIMIZE_METHOD::FULL,
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
65
       SUBool::AbsEncoder::AbsConfig(),
66
       SUBool::AbsCheckerSAT::Timeouts(),
67
68
69
70
       true,
       SUBool::LIT_IMPL_SYSTEM::NONE,
       SUBool::SOLVER_TYPE::GLUCOSE,
   };
71
   bool unfinished_write{true};
72
73
   SUBool::AmoEncoder::KIND amo_encoding{SUBool::AmoEncoder::KIND::REPR};
   SUBool::ExOneEncoder::KIND exone_encoding{SUBool::ExOneEncoder::KIND::REPR};
74
75
76

   config_t()
   {
77
78
79
80
81
82
83
84
85
86
87
88
      comp_base_config.enc_conf.up_one_prove =
          SUBool::AbsEncoder::UP_ONE_PROVE::MIN_LQ;
      comp_base_config.enc_conf.log_conf.literal_levels = false;
      comp_base_config.enc_conf.log_conf.split_size = 4;
      comp_base_config.enc_conf.log_conf.use_bit_level = false;
      comp_base_config.enc_conf.log_conf.add_amo_on_fire_vars = true;
      comp_base_config.enc_conf.log_conf.add_compare_exclusivity = true;
      comp_base_config.enc_conf.log_conf.add_force_linear_order_on_max_level =
          true;
      comp_base_config.enc_conf.log_conf.contradiction_has_max_level = true;
      comp_base_config.enc_conf.min_lq_log_weights = {2.0, 2.0, 0.0};
      comp_base_config.enc_conf.min_lq_quad_weights = {1.0, 1.0, 0.0};
89
90
91
      comp_base_config.timeouts.timeout = -1.0;
      comp_base_config.timeouts.level_base = -1.0;
      comp_base_config.timeouts.level_factor = 0.0;
92
   };
93
94
};

95
std::shared_ptr<SUBool::AbsComp> the_compiler;
96
config_t the_conf;
97

98
99
100
101
102
103
104
105
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)
106
       << "\tminimize: " << SUBool::bool_to_string(conf.minimize) << std::endl;
107
108
   SUBool::kMinimizeMethodAnnotation.DumpValue(
       "\t", level, "minimize_method", conf.comp_base_config.minimize_method);
109
   SUBool::PCCompAlgorithmOptions::kAlgorithmAnnotation.DumpValue(
110
       "\t", level, "algorithm", conf.algorithm);
111
   SUBool::logs.TLog(level)
112
113
       << "\tcomp_base_config.up_empower: "
       << static_cast<unsigned>(conf.comp_base_config.up_empower) << std::endl;
114
   SUBool::logs.TLog(level)
115
116
       << "\tcomp_base_config.simp_steps: " << conf.comp_base_config.simp_steps
       << (conf.comp_base_config.simp_steps > 0
117
118
                  ? ""
                  : "(no simplification in intervals)")
119
120
121
122
       << std::endl;
   SUBool::logs.TLog(level)
       << "\tlevel_simplify: " << (conf.level_simplify ? "yes" : "no")
       << std::endl;
123
   SUBool::dump_enum_value("\t", level, "comp_base_config.impl_system",
124
       conf.comp_base_config.impl_system, SUBool::kImplSystemNames);
125
126
   SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
   SUBool::logs.TLog(level)
127
128
       << "\tcomp_base_config.preprocess: "
       << static_cast<unsigned>(conf.comp_base_config.preprocess) << std::endl;
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
129
   SUBool::logs.DumpValue("\t", level, "comp_base_config.propagate_backbones",
130
       conf.comp_base_config.propagate_backbones);
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
131
   SUBool::logs.DumpValue("\t", level, "use_empty_initial_hypothesis",
132
       conf.use_empty_initial_hypothesis);
133
134
135
136
137
138
   SUBool::logs.TLog(level)
       << "\tpccheck_random_rounds: " << conf.pccheck_random_rounds
       << std::endl;
   SUBool::logs.TLog(level)
       << "\tpccheck_random_budget: " << conf.pccheck_random_budget
       << std::endl;
139
140
141
   SUBool::logs.TLog(level)
       << "\tpccheck_random_budget_inc: " << conf.pccheck_random_budget_inc
       << std::endl;
142
143
   SUBool::PCLearnComp::kInitialNegativesAnnotation.DumpValue(
       "\t", level, "initial_negatives", conf.initial_negatives);
144
145
   SUBool::logs.TLog(level)
       << "\trandom seed: " << conf.random_seed << std::endl;
146
   SUBool::logs.TLog(level) << "\ttimeout: " << conf.timeout << std::endl;
147
   SUBool::logs.TLog(level)
148
149
       << "\tcomp_base_config.timeouts.timeout: "
       << conf.comp_base_config.timeouts.timeout << std::endl;
150
   SUBool::logs.TLog(level)
151
152
       << "\tcomp_base_config.timeouts.level_base: "
       << conf.comp_base_config.timeouts.level_base << std::endl;
153
   SUBool::logs.TLog(level)
154
155
       << "\tcomp_base_config.timeouts.level_factor: "
       << conf.comp_base_config.timeouts.level_factor << std::endl;
156
   SUBool::dump_enum_value("\t", level, "cop_base_config.solver_type",
157
       conf.comp_base_config.solver_type, SUBool::kSolverTypeNames);
158
   SUBool::logs.TLog(level) << "\tenc_conf:" << std::endl;
159
   conf.comp_base_config.enc_conf.Dump("\t\t", level);
160
161
162
163
   SUBool::AmoEncoder::kKindAnnotation.DumpValue(
       "\t", level, "amo_encoding", conf.amo_encoding);
   SUBool::ExOneEncoder::kKindAnnotation.DumpValue(
       "\t", level, "exone_encoding", conf.exone_encoding);
164
   SUBool::logs.TLog(level) << "END" << std::endl;
165
166
}

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

bool
170
171
parse_log_enc_opts(
    const std::string &opt_string, SUBool::UPEncLogarithmic::Config &conf)
172
{
173
   std::vector<bool> opt_values(log_enc_opt_strings.size(), false);
174
   size_t start = 0;
175
   size_t end = 0;
176
   if (!opt_string.empty())
177
   {
178
      while (start != std::string::npos)
179
      {
180
         end = opt_string.find_first_of(',', start);
181
182
         auto i = std::find(log_enc_opt_strings.begin(),
             log_enc_opt_strings.end(), opt_string.substr(start, end - start));
183
184
185
186
187
188
         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);
189
      }
190
   }
191
192
193
   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];
194
   conf.contradiction_has_max_level = opt_values[3];
195
196
197
   return true;
}

198
199
200
int
parse_arguments(int argc, char *argv[], config_t &conf)
{
201
202
203
   SUBool::PrgOptions opts(true);
   opts.SetHelpDesc(prg_help);
   opts.InputOutput(&conf.input_file, &conf.output_file);
204
   auto algorithm_opts = std::make_shared<SUBool::PCCompAlgorithmOptions>();
205
   opts.AddOptionsGroup(algorithm_opts);
206
207
   auto pclearncomp_opts = std::make_shared<SUBool::PCLearnCompOptions>();
   opts.AddOptionsGroup(pclearncomp_opts);
208
209
210
211
   if (!opts.Parse(argc, argv))
   {
      return 1;
   }
212
   conf.algorithm = algorithm_opts->Algorithm();
213
214
215
216

   conf.use_empty_initial_hypothesis =
       pclearncomp_opts->UseEmptyInitialHypothesis();
   conf.initial_negatives = pclearncomp_opts->InitialNegatives();
217
218
   return 0;
#if 0
219
220
   try
   {
221
      cxxopts::Options options("pccompile",
222
          "pccompile - compiling a CNF into a propagation complete CNF "
223
224
          "based on adding empowering implicates.");
      options.positional_help("[input [output]]");
225
      options.show_positional_help();
226
      bool uc = false;
227
      std::string up_one_prove;
228
229
230
      unsigned up_empower = 0;
      unsigned preprocess = 0;
      std::string algorithm;
231
      bool no_level_simplify = false;
232
      bool no_backbone_propagation = false;
233
      unsigned long long seed;
234
      std::string log_enc_opts;
235
      std::string initial_negatives;
236
237
      std::string amo_encoding;
      std::string exone_encoding;
238
      std::string minimize_method;
239
      std::string impl_system;
240
      std::string solver_type;
241
242
243
244
245
246
      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))("1,one-prove",
247
248
249
250
251
252
253
254
255
256
257
258
          "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 "
259
          "rail encoding, the implication system type is determined by option "
260
          "--impl-system. "
261
          "impl_level (6) = based on implication system where levels are "
262
          "encoded in binary, "
263
264
265
266
267
          "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. ",
268
          cxxopts::value<std::string>(up_one_prove)
269
270
271
              ->default_value(SUBool::AbsEncoder::kUPOneProveNames.at(
                  static_cast<unsigned>(conf.comp_base_config.enc_conf
                                            .up_one_prove))))("log-enc-opts",
272
273
          "Options to logarithmic encoding modifying some of its features. "
          "It "
274
          "is a string composed of comma separated option strings which "
275
276
          "specifies which additional parts should be added to the "
          "encoding. "
277
          "Possible values specifying the features are: "
278
          "amf -- AMO on fire variables for each derived literal will be "
279
          "part of the encoding. "
280
281
282
          "cex -- Comparison exclusivity clauses will be added to the "
          "encoding. "
          "flm -- Clauses forcing linear order when the number of levels is "
283
284
285
          "maximum will be added to the encoding. "
          "cml -- A variable is contradictory if and only its level has all "
          "ones.",
286
          cxxopts::value<std::string>(log_enc_opts)
287
              ->default_value(std::string("amf,cex,flm,cml")))("w,empower",
288
289
290
291
          "What kind of encoding should be used for empowerment. "
          "0 = quadratic encoding with equivalences. "
          "1 = quadratic encoding with implications. "
          "2 = one level encoding. ",
292
          cxxopts::value<unsigned>(up_empower)
293
294
              ->default_value(std::to_string(static_cast<unsigned>(
                  conf.comp_base_config.up_empower))))("impl-system",
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
          "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 "
314
              + SUBool::DefaultImplSystemName()
315
316
317
              + " for the option combination which needs an implication "
                "system. ",
          cxxopts::value<std::string>(impl_system)->default_value("none"))(
318
          "m,minimize", "Minimize the compiled cnf.",
319
320
          cxxopts::value<bool>(conf.minimize)
              ->default_value("false"))("minimize-method",
321
322
323
324
325
326
327
328
329
330
331
332
          "Minimization method. Possible values: "
          "full -- full minimization (with the full CNF) "
          "simple_incremental -- sort in increasing order by sizes and then "
          "add nonabsorbed clauses in this sequence, starting with the empty "
          "CNF, the result is not necessarily fully minimized. "
          "full_incremental -- same as simple_incremental, in addition, now "
          "after a specific length of clauses is processed, they are "
          "reprocessed again as in full minimization. Only after then longer "
          "clauses are considered. The result is not necessarily fully "
          "minimized, but it can be significantly smaller than in case of "
          "simple_incremental.",
          cxxopts::value<std::string>(minimize_method)
333
334
              ->default_value(SUBool::kMinimizeMethodAnnotation.Name(
                  conf.comp_base_config.minimize_method)))("a,algorithm",
335
          "The compilation algorithm. "
336
337
338
339
          "'incremental' -- a heuristic algorithm based on incremental "
          "adding "
          "empowering implicates, allows preprocessing and inprocessing. "
          "This "
340
341
          "works in both kinds of goals (PC/UC). "
          "'learning' -- an algorithm based on the algorithm for learning a "
342
343
344
345
          "Horn formula through equivalence and closure queries (Arias et "
          "al. "
          "2015). This works only for goal PC. If goal is UC, the program "
          "ends "
346
          "with error. Other parameters are used appropriately.",
347
          cxxopts::value<std::string>(algorithm)->default_value(
348
349
              algorithm_names[static_cast<unsigned>(
                  conf.algorithm)]))("l,level",
350
351
352
353
354
355
          "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 "
356
357
          "of bits used to encode a number of level. In case of choice -1 4 "
          "when the minimum of quadratic and logarithmic encoding is "
358
359
360
361
          "considered, the level bounds the number of level of the "
          "quadratic "
          "encoding while the number of levels of the logarithmic encoding "
          "is "
362
          "bounded to the logarithm of the parameter rounded up.",
363
364
365
          cxxopts::value<unsigned>(
              conf.comp_base_config.enc_conf.up_level_bound)
              ->default_value(std::to_string(
366
                  conf.comp_base_config.enc_conf.up_level_bound)))("u,uc",
367
368
          "Aim for unit refutation completeness instead of "
          "propagation completeness.",
369
          cxxopts::value<bool>(uc)->default_value("false"))("interleave-pc",
370
371
          "In case of compilation to UC, "
          "interleave encodings for UC and PC.",
372
373
          cxxopts::value<bool>(conf.uc_interleave_pc)
              ->default_value("false"))("use-empty-initial-hypothesis",
374
375
          "Use empty initial hypothesis in the learning algorithm. If not "
          "set, "
376
377
          "the preprocessed input CNF is used as an initial hypothesis.",
          cxxopts::value<bool>(conf.use_empty_initial_hypothesis)
378
              ->default_value("false"))("pccheck-random-rounds",
379
380
          "Number of rounds during one random check of PC.",
          cxxopts::value<unsigned>(conf.pccheck_random_rounds)
381
382
              ->default_value(std::to_string(
                  conf.pccheck_random_rounds)))("pccheck-random-budget",
383
384
385
          "How many times unsucessful random PC check should be repeated. 0 "
          "means no random check is ever performed.",
          cxxopts::value<unsigned>(conf.pccheck_random_budget)
386
387
              ->default_value(std::to_string(
                  conf.pccheck_random_budget)))("pccheck-random-budget-inc",
388
389
390
391
          "Increase of the current budget in case a random negative example "
          "was successfully found. 0 "
          "means no increase.",
          cxxopts::value<unsigned>(conf.pccheck_random_budget_inc)
392
393
              ->default_value(std::to_string(
                  conf.pccheck_random_budget_inc)))("initial-negatives",
394
          "How the initial negative examples in the learning algorithm "
395
396
397
          "should be produced. The option specifies how the negatives for each "
          "clause in the preprocessed CNF are created. For a clause C, the "
          "possible options are as follows: "
398
399
          "'single_empowering' - Only one negative is produced (C without a "
          "literal with respect to which C is empowering), "
400
          "'all' - All negatives are produced (C without l fo every literal "
401
          "l in C), "
402
          "'all_empowering' - For every literal l in C if C is empowering "
403
404
405
          "with respect to l, then C without l is produced."
          "'gd_basis' - GD basis of the dual rail encoding of the "
          "prepreocessed CNF is computed, the bodies in the GD basis are used "
406
407
408
409
          "as an initial list of negatives."
          "'body_minimal' - body minimal representation for the dual rail "
          "encoding of the preprocessed CNF is computed. The bodies in this "
          "representation are used as an initial list of negatives.",
410
411
          cxxopts::value<std::string>(initial_negatives)
              ->default_value(
412
413
                  SUBool::PCLearnComp::cInitialNegativesNames[static_cast<
                      unsigned>(conf.initial_negatives)]))("s,simp-steps",
414
          "Number of empowering clauses after which a heuristic "
415
416
          "simplification of the current formula proceeds. Zero (0) means that "
          "no simplification is made during the compilation. However final "
417
          "minimization shall proceed depending on presence of -m option.",
418
          cxxopts::value<unsigned>(conf.comp_base_config.simp_steps)
419
420
              ->default_value(std::to_string(
                  conf.comp_base_config.simp_steps)))("no-level-simplify",
421
          "Do not perform simplification when the number of levels of unit "
422
          "propagation increases.",
423
424
          cxxopts::value<bool>(no_level_simplify)
              ->default_value("false"))("r,preprocess",
425
426
          "Method of preprocessing. "
          "0 = No preprocessing. "
427
          "1 = Minimize the formula before compilation. "
428
429
430
          "2 = First make CNF prime with respect to 1-provability, then "
          "minimize. "
          "3 = First make CNF prime and then minimize. "
431
          "4 = Only make CNF prime with respect to 1-provability, no "
Kučera Petr RNDr. Ph.D.'s avatar
Kučera Petr RNDr. Ph.D. committed
432
          "minimization. "
433
          "5 = Only make CNF prime, no minimization. ",
434
          cxxopts::value<unsigned>(preprocess)
435
436
437
              ->default_value(std::to_string(static_cast<unsigned>(
                  conf.comp_base_config
                      .preprocess))))("no-backbone-propagation",
438
439
          "Do not perform backbone propagation before preprocessing.",
          cxxopts::value<bool>(no_backbone_propagation)
440
              ->default_value("false"))("S,seed",
441
442
          "Initial random seed. Current time is used, if the seed is not "
          "provided explicitly.",
443
          cxxopts::value<unsigned long long>(seed))("t,timeout",
444
445
          "Timeout for compilation in seconds as a fractional number. "
          "After this amount of seconds, the process finishes. Value "
446
447
          "t<=0.0 means no timeout. The timer uses CLOCK_REALTIME.",
          cxxopts::value<double>(conf.timeout)
448
              ->default_value(std::to_string(conf.timeout)))("emp-timeout",
449
450
          "Timeout for a single SAT call which looks for an empowering "
          "implicate. The timeout is in seconds as a fractional number.",
451
          cxxopts::value<double>(conf.comp_base_config.timeouts.timeout)
452
              ->default_value(
453
454
                  std::to_string(conf.comp_base_config.timeouts
                                     .timeout)))("emp-timeout-level-base",
455
456
457
          "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 "
458
459
460
461
462
463
464
465
          "allowed in the encoding. Denote the value of "
          "emp-timeout-level-base "
          "as B and the value of emp-timeout-level-factor as F. For a 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, "
466
467
          "then the value of emp-timeout is used instead. The timeout is "
          "passed as a fractional number specifying the number of seconds.",
468
469
          cxxopts::value<double>(conf.comp_base_config.timeouts.level_base)
              ->default_value(
470
471
                  std::to_string(conf.comp_base_config.timeouts
                                     .level_base)))("emp-timeout-level-factor",
472
473
474
475
476
477
          "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 "
          "emp-timeout-level-base for more details). If the value is higher "
          "than emp-timeout, then the value of emp-timeout is used instead. "
478
479
          "The timeout is passed as a fractional number specifying the "
          "number "
480
          "of seconds.",
481
482
          cxxopts::value<double>(conf.comp_base_config.timeouts.level_factor)
              ->default_value(
483
484
                  std::to_string(conf.comp_base_config.timeouts
                                     .level_factor)))("pccheck-solver",
485
486
487
488
489
490
491
492
493
          "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>(
494
                  conf.comp_base_config.solver_type)]))("b,verbosity",
495
496
497
498
499
          "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)
500
              ->default_value(std::to_string(conf.verbosity)))("positional",
501
502
          "Positional arguments: these are the arguments that are entered "
          "without an option",
503
          cxxopts::value<std::vector<std::string>>())("amo",
504
505
506
507
          "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)
508
509
              ->default_value(SUBool::AmoEncoder::kKindAnnotation.Name(
                  conf.amo_encoding)))("exactly-one",
510
511
512
513
          "Which encoding to use for the exactly-one constraint. "
          "repr = use the representation, "
          "split = use the splitting encoding.",
          cxxopts::value<std::string>(exone_encoding)
514
515
              ->default_value(SUBool::ExOneEncoder::kKindAnnotation.Name(
                  conf.exone_encoding)));
516
517
518
519
520
521
522
523
524
      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"))
      {
525
         SUBool::print_version(std::cout);
526
         std::cout << std::endl;
527
528
529
530
531
532
533
534
535
         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;
      }
536
      conf.random_seed =
537
538
539
540
          (result.count("seed") > 0 ? seed
                                    : std::chrono::system_clock::now()
                                          .time_since_epoch()
                                          .count());
541
      conf.goal = (uc ? GOAL::UC : GOAL::PC);
542
      conf.level_simplify = !no_level_simplify;
543
      conf.comp_base_config.propagate_backbones = !no_backbone_propagation;
544
545
      if (!parse_log_enc_opts(
              log_enc_opts, conf.comp_base_config.enc_conf.log_conf))
546
      {
547
         std::cerr << "Error parsing logarithmic encoding options" << std::endl;
548
549
         return 1;
      }
550
551
      try
      {
552
         conf.comp_base_config.enc_conf.up_one_prove =
553
             SUBool::AbsEncoder::ParseUPOneProve(up_one_prove);
554
         conf.comp_base_config.up_empower =
555
             SUBool::enum_of_int<SUBool::PCEncoder::UP_EMPOWER>(up_empower);
556
         conf.comp_base_config.preprocess =
557
558
559
560
             SUBool::enum_of_int<SUBool::AbsIncrementalComp::PREPROCESS_METHOD>(
                 preprocess);
         conf.algorithm =
             SUBool::enum_of_name<ALGORITHM>(algorithm, algorithm_names);
561
562
563
564
         conf.initial_negatives =
             SUBool::enum_of_name<SUBool::PCLearnComp::INITIAL_NEGATIVES>(
                 initial_negatives,
                 SUBool::PCLearnComp::cInitialNegativesNames);
565
566
567
568
         conf.amo_encoding =
             SUBool::AmoEncoder::kKindAnnotation.Parse(amo_encoding);
         conf.exone_encoding =
             SUBool::ExOneEncoder::kKindAnnotation.Parse(exone_encoding);
569
         conf.comp_base_config.minimize_method =
570
             SUBool::kMinimizeMethodAnnotation.Parse(minimize_method);
571
572
573
         conf.comp_base_config.impl_system =
             SUBool::enum_of_name<SUBool::LIT_IMPL_SYSTEM>(
                 impl_system, SUBool::kImplSystemNames);
574
575
         if (SUBool::AbsEncoder::AbsConfig::OneProveRequiresImplSystem(
                 conf.comp_base_config.enc_conf.up_one_prove)
576
577
             && conf.comp_base_config.impl_system
                    == SUBool::LIT_IMPL_SYSTEM::NONE)
578
         {
579
            conf.comp_base_config.impl_system = SUBool::kDefaultImplSystem;
580
         }
581
582
583
584
585
586
587
588
589
590
         conf.comp_base_config.solver_type =
             SUBool::enum_of_name<SUBool::SOLVER_TYPE>(
                 solver_type, SUBool::kSolverTypeNames);
#if !HAS_KISSAT
         if (conf.comp_base_config.solver_type == SUBool::SOLVER_TYPE::KISSAT)
         {
            std::cerr << "Kissat not available" << std::endl;
            return 1;
         }
#endif
591
592
593
594
595
596
597
598
599
600
601
      }
      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;
602
      return 1;
603
604
   }
   return 0;
605
#endif
606
607
}

608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
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;
632
633
}

634
template <class T, class R>
635
R
636
wait_with_timeout(double timeout, std::future<R> &fut, T &comp)
637
{
638
   if (timeout > 0.0)
639
   {
640
      if (fut.wait_for(std::chrono::duration<double>(timeout))
641
642
643
          == std::future_status::timeout)
      {
         comp.Abort("timed out");
644
         comp.PrintStatistics(1);
645
         fut.wait();
646
         return SUBool::AbsComp::RESULT::TIMED_OUT; //_Exit(3);
647
648
649
650
651
652
653
      }
   }
   else
   {
      fut.wait();
   }
   return fut.get();
654
655
}

656
void
657
fill_base_conf(SUBool::AbsComp::BaseConfig &out_conf, const config_t &conf)
658
{
659
   out_conf = conf.comp_base_config;
660
   out_conf.final_simplify = conf.minimize;
661
662
663
   out_conf.level_simplify = conf.level_simplify;
}

664
// std::unique_ptr<SUBool::AbsIncrementalComp>
665
std::shared_ptr<SUBool::AbsIncrementalComp>
666
667
incremental_compiler(const config_t &conf, SUBool::CNF cnf)
{
668
669
   SUBool::AbsComp::BaseConfig a_conf;
   fill_base_conf(a_conf, conf);
670
   bool interleave_pc = false;
671

672
   switch (conf.algorithm)
673
   {
674
   case SUBool::PCCompAlgorithmOptions::ALGORITHM::INCREMENT_PC:
675
676
      return std::make_shared<SUBool::PCComp>(
          std::move(cnf), std::move(a_conf));
677
   case SUBool::PCCompAlgorithmOptions::ALGORITHM::INCREMENT_URC_PC:
678
679
      interleave_pc = true;
      [[fallthrough]];
680
   case SUBool::PCCompAlgorithmOptions::ALGORITHM::INCREMENT_URC:
681
682
   {
      SUBool::UCComp::Config uc_conf(a_conf);
683
      uc_conf.interleave_pc = interleave_pc;
684
685
      return std::make_shared<SUBool::UCComp>(
          std::move(cnf), std::move(uc_conf));
686
   }
687
688
689
   default:
      throw SUBool::BadParameterException(
          "compiler", "Bad algorithm specification");
690
   }
691
692
}

693
694
695
696
std::shared_ptr<SUBool::PCLearnComp>
learning_compiler(const config_t &conf, SUBool::CNF cnf)
{
   SUBool::PCLearnComp::Config l_conf;
697
   fill_base_conf(l_conf, conf);
698
   l_conf.use_empty_initial_hypothesis = conf.use_empty_initial_hypothesis;
699
700
   l_conf.pccheck_random_rounds = conf.pccheck_random_rounds;
   l_conf.pccheck_random_budget = conf.pccheck_random_budget;
701
   l_conf.pccheck_random_budget_inc = conf.pccheck_random_budget_inc;
702
   l_conf.initial_negatives = conf.initial_negatives;
703
704
   return std::make_shared<SUBool::PCLearnComp>(
       std::move(cnf), std::move(l_conf));
705
706
}

707
708
709
std::shared_ptr<SUBool::AbsComp>
compiler(const config_t &conf, SUBool::CNF cnf)
{
710
   if (conf.algorithm == SUBool::PCCompAlgorithmOptions::ALGORITHM::LEARNING)
711
712
713
   {
      return learning_compiler(conf, std::move(cnf));
   }
714
   return incremental_compiler(conf, std::move(cnf));
715
716
}

717
718
719
int
write_output()
{
720
   if (!the_compiler)
721
722
   {
      SUBool::logs.TLog(1)
723
          << "[write_output] the_compiler is nullptr, no output written"
724
725
726
727
          << std::endl;
   }
   try
   {
728
      std::stringstream ss;
729
      SUBool::print_version(ss, true);
730
      output(the_conf.output_file, the_compiler->CurrentCNF(), ss.str());
731
732
733
734
735
736
737
738
739
740
   }
   catch (SUBool::IOException &e)
   {
      SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::NONE)
          << "[write_output]" << e.what() << std::endl;
      return 2;
   }
   return 0;
}

741
int
742
compile(SUBool::CNF cnf)
743
{
744
   auto comp = compiler(the_conf, std::move(cnf));
745
   the_compiler = comp;
746
747
748
749
   auto fut = std::async(
       std::launch::async,
       [](std::shared_ptr<SUBool::AbsComp> comp) { return comp->Compile(); },
       comp);
750
751
   auto res = wait_with_timeout(the_conf.timeout, fut, *comp);
   if (res == SUBool::AbsComp::RESULT::COMPILED || the_conf.unfinished_write)
752
   {
753
      return write_output();
754
755
756
757
   }
   SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::MINLINES)
       << "No output written" << std::endl;
   return 1;
758
759
}

760
761
762
763
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";
764

765
766
767
768
769
void
terminate(int signal)
{
   std::stringstream ss;
   ss << "terminated by signal " << signal;
770
   if (the_compiler)
771
   {
772
773
      the_compiler->Abort(ss.str());
      the_compiler->PrintStatistics(1);
774
775
776
777
778
779
780
781
      if (the_conf.unfinished_write)
      {
         write_output();
      }
      else
      {
         SUBool::logs.TLog(3) << "c No output written" << std::endl;
      }
782
783
   }
   _Exit(2);
784
785
}

786
787
788
int
main(int argc, char *argv[])
{
789
   int r = parse_arguments(argc, argv, the_conf);
790
791
792
793
794
   if (r != 0)
   {
      return r;
   }
   SUBool::CNF cnf;
795
   r = input(the_conf, &cnf);
796
797
798
799
   if (r != 0)
   {
      return r;
   }
800
   SUBool::sub_rand.seed(the_conf.random_seed);
801
802
803
804
805
806

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

   SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::MINLINES)
807
       << "PCCompile " << SUBool::kVersionInfo << std::endl;
808

809
   dump_config(the_conf, 3);
810
811
   return 0;
#if 0
812
813
   SUBool::AmoEncoder::sGlobalKind = the_conf.amo_encoding;
   SUBool::ExOneEncoder::sGlobalKind = the_conf.exone_encoding;
814
   auto ret = compile(std::move(cnf));
Kučera Petr RNDr. Ph.D.'s avatar
Bug fix    
Kučera Petr RNDr. Ph.D. committed
815
816
   the_compiler = nullptr;
   return ret;
817
#endif
818
}