GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/decision_options.cpp Lines: 23 90 25.6 %
Date: 2021-03-23 Branches: 6 55 10.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file module_template.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Option template for option modules.
13
 **
14
 ** For each <module>_options.toml configuration file, mkoptions.py
15
 ** expands this template and generates a <module>_options.cpp file.
16
 **/
17
18
#include "options/options_holder.h"
19
#include "base/check.h"
20
21
namespace CVC4 {
22
23
template <> const options::decisionRandomWeight__option_t::type& Options::operator[](
24
    options::decisionRandomWeight__option_t) const
25
{
26
  return d_holder->decisionRandomWeight;
27
}
28
template <> bool Options::wasSetByUser(options::decisionRandomWeight__option_t) const
29
{
30
  return d_holder->decisionRandomWeight__setByUser__;
31
}
32
743545
template <> const options::decisionThreshold__option_t::type& Options::operator[](
33
    options::decisionThreshold__option_t) const
34
{
35
743545
  return d_holder->decisionThreshold;
36
}
37
template <> bool Options::wasSetByUser(options::decisionThreshold__option_t) const
38
{
39
  return d_holder->decisionThreshold__setByUser__;
40
}
41
13039484
template <> const options::decisionUseWeight__option_t::type& Options::operator[](
42
    options::decisionUseWeight__option_t) const
43
{
44
13039484
  return d_holder->decisionUseWeight;
45
}
46
template <> bool Options::wasSetByUser(options::decisionUseWeight__option_t) const
47
{
48
  return d_holder->decisionUseWeight__setByUser__;
49
}
50
template <> const options::decisionWeightInternal__option_t::type& Options::operator[](
51
    options::decisionWeightInternal__option_t) const
52
{
53
  return d_holder->decisionWeightInternal;
54
}
55
template <> bool Options::wasSetByUser(options::decisionWeightInternal__option_t) const
56
{
57
  return d_holder->decisionWeightInternal__setByUser__;
58
}
59
8868
template <> void Options::set(
60
    options::decisionMode__option_t,
61
    const options::decisionMode__option_t::type& x)
62
{
63
8868
  d_holder->decisionMode = x;
64
8868
}
65
34558
template <> const options::decisionMode__option_t::type& Options::operator[](
66
    options::decisionMode__option_t) const
67
{
68
34558
  return d_holder->decisionMode;
69
}
70
8997
template <> bool Options::wasSetByUser(options::decisionMode__option_t) const
71
{
72
8997
  return d_holder->decisionMode__setByUser__;
73
}
74
8945
template <> void Options::set(
75
    options::decisionStopOnly__option_t,
76
    const options::decisionStopOnly__option_t::type& x)
77
{
78
8945
  d_holder->decisionStopOnly = x;
79
8945
}
80
2519991
template <> const options::decisionStopOnly__option_t::type& Options::operator[](
81
    options::decisionStopOnly__option_t) const
82
{
83
2519991
  return d_holder->decisionStopOnly;
84
}
85
template <> bool Options::wasSetByUser(options::decisionStopOnly__option_t) const
86
{
87
  return d_holder->decisionStopOnly__setByUser__;
88
}
89
90
91
namespace options {
92
93
thread_local struct decisionRandomWeight__option_t decisionRandomWeight;
94
thread_local struct decisionThreshold__option_t decisionThreshold;
95
thread_local struct decisionUseWeight__option_t decisionUseWeight;
96
thread_local struct decisionWeightInternal__option_t decisionWeightInternal;
97
thread_local struct decisionMode__option_t decisionMode;
98
thread_local struct decisionStopOnly__option_t decisionStopOnly;
99
100
101
std::ostream&
102
operator<<(std::ostream& os, DecisionWeightInternal mode)
103
{
104
  os << "DecisionWeightInternal::";
105
  switch(mode) {
106
    case DecisionWeightInternal::USR1:
107
      os << "USR1";
108
      break;
109
    case DecisionWeightInternal::SUM:
110
      os << "SUM";
111
      break;
112
    case DecisionWeightInternal::MAX:
113
      os << "MAX";
114
      break;
115
    case DecisionWeightInternal::OFF:
116
      os << "OFF";
117
      break;
118
    default:
119
        Unreachable();
120
  }
121
  return os;
122
}
123
124
DecisionWeightInternal
125
stringToDecisionWeightInternal(const std::string& option, const std::string& optarg)
126
{
127
  if (optarg == "usr1")
128
  {
129
    return DecisionWeightInternal::USR1;
130
  }
131
  else if (optarg == "sum")
132
  {
133
    return DecisionWeightInternal::SUM;
134
  }
135
  else if (optarg == "max")
136
  {
137
    return DecisionWeightInternal::MAX;
138
  }
139
  else if (optarg == "off")
140
  {
141
    return DecisionWeightInternal::OFF;
142
  }
143
  else if (optarg == "help")
144
  {
145
    puts("Decision weight internal mode.\n"
146
         "Available modes for --decision-weight-internal are:\n"
147
         "+ usr1\n"
148
         "+ sum\n"
149
         "+ max\n"
150
         "+ off (default)\n");
151
    exit(1);
152
  }
153
  else
154
  {
155
    throw OptionException(std::string("unknown option for --decision-weight-internal: `") +
156
                          optarg + "'.  Try --decision-weight-internal=help.");
157
  }
158
}
159
160
std::ostream&
161
operator<<(std::ostream& os, DecisionMode mode)
162
{
163
  os << "DecisionMode::";
164
  switch(mode) {
165
    case DecisionMode::JUSTIFICATION:
166
      os << "JUSTIFICATION";
167
      break;
168
    case DecisionMode::RELEVANCY:
169
      os << "RELEVANCY";
170
      break;
171
    case DecisionMode::INTERNAL:
172
      os << "INTERNAL";
173
      break;
174
    default:
175
        Unreachable();
176
  }
177
  return os;
178
}
179
180
DecisionMode
181
77
stringToDecisionMode(const std::string& option, const std::string& optarg)
182
{
183
77
  if (optarg == "justification")
184
  {
185
63
    return DecisionMode::JUSTIFICATION;
186
  }
187
14
  else if (optarg == "justification-stoponly")
188
  {
189
    return DecisionMode::RELEVANCY;
190
  }
191
14
  else if (optarg == "internal")
192
  {
193
14
    return DecisionMode::INTERNAL;
194
  }
195
  else if (optarg == "help")
196
  {
197
    puts("Decision modes.\n"
198
         "Available modes for --decision are:\n"
199
         "+ justification\n"
200
         "  An ATGP-inspired justification heuristic.\n"
201
         "+ justification-stoponly\n"
202
         "  Use the justification heuristic only to stop early, not for decisions.\n"
203
         "+ internal (default)\n"
204
         "  Use the internal decision heuristics of the SAT solver.\n");
205
    exit(1);
206
  }
207
  else
208
  {
209
    throw OptionException(std::string("unknown option for --decision: `") +
210
                          optarg + "'.  Try --decision=help.");
211
  }
212
}
213
214
215
}  // namespace options
216
26685
}  // namespace CVC4