GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/theory_options.cpp Lines: 29 96 30.2 %
Date: 2021-03-23 Branches: 3 61 4.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
2
template <> void Options::set(
24
    options::assignFunctionValues__option_t,
25
    const options::assignFunctionValues__option_t::type& x)
26
{
27
2
  d_holder->assignFunctionValues = x;
28
2
}
29
27861
template <> const options::assignFunctionValues__option_t::type& Options::operator[](
30
    options::assignFunctionValues__option_t) const
31
{
32
27861
  return d_holder->assignFunctionValues;
33
}
34
template <> bool Options::wasSetByUser(options::assignFunctionValues__option_t) const
35
{
36
  return d_holder->assignFunctionValues__setByUser__;
37
}
38
290649
template <> const options::condenseFunctionValues__option_t::type& Options::operator[](
39
    options::condenseFunctionValues__option_t) const
40
{
41
290649
  return d_holder->condenseFunctionValues;
42
}
43
template <> bool Options::wasSetByUser(options::condenseFunctionValues__option_t) const
44
{
45
  return d_holder->condenseFunctionValues__setByUser__;
46
}
47
template <> void Options::set(
48
    options::eeMode__option_t,
49
    const options::eeMode__option_t::type& x)
50
{
51
  d_holder->eeMode = x;
52
}
53
8999
template <> const options::eeMode__option_t::type& Options::operator[](
54
    options::eeMode__option_t) const
55
{
56
8999
  return d_holder->eeMode;
57
}
58
template <> bool Options::wasSetByUser(options::eeMode__option_t) const
59
{
60
  return d_holder->eeMode__setByUser__;
61
}
62
7
template <> void Options::set(
63
    options::relevanceFilter__option_t,
64
    const options::relevanceFilter__option_t::type& x)
65
{
66
7
  d_holder->relevanceFilter = x;
67
7
}
68
9009
template <> const options::relevanceFilter__option_t::type& Options::operator[](
69
    options::relevanceFilter__option_t) const
70
{
71
9009
  return d_holder->relevanceFilter;
72
}
73
7
template <> bool Options::wasSetByUser(options::relevanceFilter__option_t) const
74
{
75
7
  return d_holder->relevanceFilter__setByUser__;
76
}
77
template <> void Options::set(
78
    options::tcMode__option_t,
79
    const options::tcMode__option_t::type& x)
80
{
81
  d_holder->tcMode = x;
82
}
83
8999
template <> const options::tcMode__option_t::type& Options::operator[](
84
    options::tcMode__option_t) const
85
{
86
8999
  return d_holder->tcMode;
87
}
88
template <> bool Options::wasSetByUser(options::tcMode__option_t) const
89
{
90
  return d_holder->tcMode__setByUser__;
91
}
92
2104
template <> void Options::set(
93
    options::theoryOfMode__option_t,
94
    const options::theoryOfMode__option_t::type& x)
95
{
96
2104
  d_holder->theoryOfMode = x;
97
2104
}
98
158798268
template <> const options::theoryOfMode__option_t::type& Options::operator[](
99
    options::theoryOfMode__option_t) const
100
{
101
158798268
  return d_holder->theoryOfMode;
102
}
103
8999
template <> bool Options::wasSetByUser(options::theoryOfMode__option_t) const
104
{
105
8999
  return d_holder->theoryOfMode__setByUser__;
106
}
107
108
109
namespace options {
110
111
thread_local struct assignFunctionValues__option_t assignFunctionValues;
112
thread_local struct condenseFunctionValues__option_t condenseFunctionValues;
113
thread_local struct eeMode__option_t eeMode;
114
thread_local struct relevanceFilter__option_t relevanceFilter;
115
thread_local struct tcMode__option_t tcMode;
116
thread_local struct theoryOfMode__option_t theoryOfMode;
117
118
119
std::ostream&
120
operator<<(std::ostream& os, EqEngineMode mode)
121
{
122
  os << "EqEngineMode::";
123
  switch(mode) {
124
    case EqEngineMode::DISTRIBUTED:
125
      os << "DISTRIBUTED";
126
      break;
127
    default:
128
        Unreachable();
129
  }
130
  return os;
131
}
132
133
EqEngineMode
134
stringToEqEngineMode(const std::string& option, const std::string& optarg)
135
{
136
  if (optarg == "distributed")
137
  {
138
    return EqEngineMode::DISTRIBUTED;
139
  }
140
  else if (optarg == "help")
141
  {
142
    puts("Defines mode for managing equalities across theory solvers.\n"
143
         "Available modes for --ee-mode are:\n"
144
         "+ distributed (default)\n"
145
         "  Each theory maintains its own equality engine.\n");
146
    exit(1);
147
  }
148
  else
149
  {
150
    throw OptionException(std::string("unknown option for --ee-mode: `") +
151
                          optarg + "'.  Try --ee-mode=help.");
152
  }
153
}
154
155
std::ostream&
156
operator<<(std::ostream& os, TcMode mode)
157
{
158
  os << "TcMode::";
159
  switch(mode) {
160
    case TcMode::CARE_GRAPH:
161
      os << "CARE_GRAPH";
162
      break;
163
    default:
164
        Unreachable();
165
  }
166
  return os;
167
}
168
169
TcMode
170
stringToTcMode(const std::string& option, const std::string& optarg)
171
{
172
  if (optarg == "care-graph")
173
  {
174
    return TcMode::CARE_GRAPH;
175
  }
176
  else if (optarg == "help")
177
  {
178
    puts("Defines mode for theory combination.\n"
179
         "Available modes for --tc-mode are:\n"
180
         "+ care-graph (default)\n"
181
         "  Use care graphs for theory combination.\n");
182
    exit(1);
183
  }
184
  else
185
  {
186
    throw OptionException(std::string("unknown option for --tc-mode: `") +
187
                          optarg + "'.  Try --tc-mode=help.");
188
  }
189
}
190
191
std::ostream&
192
operator<<(std::ostream& os, TheoryOfMode mode)
193
{
194
  os << "TheoryOfMode::";
195
  switch(mode) {
196
    case TheoryOfMode::THEORY_OF_TYPE_BASED:
197
      os << "THEORY_OF_TYPE_BASED";
198
      break;
199
    case TheoryOfMode::THEORY_OF_TERM_BASED:
200
      os << "THEORY_OF_TERM_BASED";
201
      break;
202
    default:
203
        Unreachable();
204
  }
205
  return os;
206
}
207
208
TheoryOfMode
209
3
stringToTheoryOfMode(const std::string& option, const std::string& optarg)
210
{
211
3
  if (optarg == "type")
212
  {
213
3
    return TheoryOfMode::THEORY_OF_TYPE_BASED;
214
  }
215
  else if (optarg == "term")
216
  {
217
    return TheoryOfMode::THEORY_OF_TERM_BASED;
218
  }
219
  else if (optarg == "help")
220
  {
221
    puts("Defines how we associate theories with terms.\n"
222
         "Available modes for --theoryof-mode are:\n"
223
         "+ type (default)\n"
224
         "  Type variables, constants and equalities by type.\n"
225
         "+ term\n"
226
         "  Type variables as uninterpreted, type constants by theory, equalities by the\n"
227
         "  parametric theory.\n");
228
    exit(1);
229
  }
230
  else
231
  {
232
    throw OptionException(std::string("unknown option for --theoryof-mode: `") +
233
                          optarg + "'.  Try --theoryof-mode=help.");
234
  }
235
}
236
237
238
}  // namespace options
239
26691
}  // namespace CVC4