pc_opt.cpp 2.81 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
/*
 * Project SUBool
 * Petr Kucera, 2021
 */
/**@file pc_opt.h
 * Common options of programs related to propagation completeness.
 */

#include "pc_opt.h"

11
12
const SUBool::EnumAnnotation<SUBool::PCCompAlgorithmOptions::ALGORITHM>
    SUBool::PCCompAlgorithmOptions::kAlgorithmAnnotation("ALGORITHM",
13
        {//
14
            {ALGORITHM::INCREMENT_PC, "incremental_pc",
15
16
17
18
                "heuristic algorithm based on incremental adding empowering "
                "implicates. The goal is an equivalent PC formula and SAT "
                "solver is used to "
                "check if the formula is PC."}, //
19
            {ALGORITHM::INCREMENT_URC, "incremental_urc",
20
21
22
23
                "heuristic algorithm based on incremental adding empowering "
                "implicates. The goal is an equivalent URC formula and SAT "
                "solver is used to "
                "check if the formula is URC."}, //
24
            {ALGORITHM::INCREMENT_URC_PC, "incremental_urc_pc",
25
26
                "heuristic algorithm based on incremental adding empowering "
                "implicates. The goal is URC formula and SAT solver is used to "
27
                "check if the formula is URC or PC in an interleaving way."}, //
28
29
30
31
32
            {ALGORITHM::LEARNING, "learning",
                "based on the algorithm for learning a Horn formula through "
                "equivalence and closure queries (Arias et al. 2015). The goal "
                "is an equivalent PC formula."}});

33
34
35
36
37
38
auto
SUBool::minimize_method_opt() -> EnumOption<MINIMIZE_METHOD>
{
   return make_enum_option(kMinimizeMethodAnnotation, "minimize-method",
       "Minimization method", kDefaultMinimizeMethod);
}
39

40
SUBool::PCCompAlgorithmOptions::PCCAlgorithmOptions()
41
    : OptionsGroup("Algorithm Selection"),
42
43
44
45
46
47
48
      mAlgorithmOption(kAlgorithmAnnotation, "algorithm,a",
          "Algorithm used for compilation", kDefaultAlgorithm)
{
   Add(mAlgorithmOption);
}

bool
49
SUBool::PCCompAlgorithmOptions::GetValues()
50
51
52
{
   return mAlgorithmOption.GetValue(mAlgorithm);
}
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

SUBool::PCLearnCompOptions::PCLearnCompOptions()
    : OptionsGroup("Learning Algorithm Options"),
      mInitialNegativesOption(PCLearnComp::kInitialNegativesAnnotation,
          "initial-negatives",
          "How the initial negative examples in the learning algorithm "
          "should be produced. The option specifies how the negatives for each "
          "clause in the preprocessed CNF are created.",
          kDefaultInitialNegatives)
{
   AddOptions()("use-empty-initial-hypothesis",
       po::bool_switch(&mUseEmptyInitialHypothesis),
       "Use empty initial hypothesis in the learning algorithm. If not "
       "set, the preprocessed input CNF is used as an initial hypothesis.");
   Add(mInitialNegativesOption);
}

bool
SUBool::PCLearnCompOptions::GetValues()
{
   return mInitialNegativesOption.GetValue(mInitialNegatives);
}