GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/uf_options.cpp Lines: 27 76 35.5 %
Date: 2021-03-23 Branches: 4 28 14.3 %

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
8999
template <> void Options::set(
24
    options::ufSymmetryBreaker__option_t,
25
    const options::ufSymmetryBreaker__option_t::type& x)
26
{
27
8999
  d_holder->ufSymmetryBreaker = x;
28
8999
}
29
104434
template <> const options::ufSymmetryBreaker__option_t::type& Options::operator[](
30
    options::ufSymmetryBreaker__option_t) const
31
{
32
104434
  return d_holder->ufSymmetryBreaker;
33
}
34
8999
template <> bool Options::wasSetByUser(options::ufSymmetryBreaker__option_t) const
35
{
36
8999
  return d_holder->ufSymmetryBreaker__setByUser__;
37
}
38
template <> void Options::set(
39
    options::ufHo__option_t,
40
    const options::ufHo__option_t::type& x)
41
{
42
  d_holder->ufHo = x;
43
}
44
16770340
template <> const options::ufHo__option_t::type& Options::operator[](
45
    options::ufHo__option_t) const
46
{
47
16770340
  return d_holder->ufHo;
48
}
49
template <> bool Options::wasSetByUser(options::ufHo__option_t) const
50
{
51
  return d_holder->ufHo__setByUser__;
52
}
53
template <> void Options::set(
54
    options::ufHoExt__option_t,
55
    const options::ufHoExt__option_t::type& x)
56
{
57
  d_holder->ufHoExt = x;
58
}
59
70246
template <> const options::ufHoExt__option_t::type& Options::operator[](
60
    options::ufHoExt__option_t) const
61
{
62
70246
  return d_holder->ufHoExt;
63
}
64
template <> bool Options::wasSetByUser(options::ufHoExt__option_t) const
65
{
66
  return d_holder->ufHoExt__setByUser__;
67
}
68
7345
template <> const options::ufssAbortCardinality__option_t::type& Options::operator[](
69
    options::ufssAbortCardinality__option_t) const
70
{
71
7345
  return d_holder->ufssAbortCardinality;
72
}
73
template <> bool Options::wasSetByUser(options::ufssAbortCardinality__option_t) const
74
{
75
  return d_holder->ufssAbortCardinality__setByUser__;
76
}
77
11794
template <> const options::ufssFairness__option_t::type& Options::operator[](
78
    options::ufssFairness__option_t) const
79
{
80
11794
  return d_holder->ufssFairness;
81
}
82
template <> bool Options::wasSetByUser(options::ufssFairness__option_t) const
83
{
84
  return d_holder->ufssFairness__setByUser__;
85
}
86
1529
template <> void Options::set(
87
    options::ufssFairnessMonotone__option_t,
88
    const options::ufssFairnessMonotone__option_t::type& x)
89
{
90
1529
  d_holder->ufssFairnessMonotone = x;
91
1529
}
92
98858
template <> const options::ufssFairnessMonotone__option_t::type& Options::operator[](
93
    options::ufssFairnessMonotone__option_t) const
94
{
95
98858
  return d_holder->ufssFairnessMonotone;
96
}
97
template <> bool Options::wasSetByUser(options::ufssFairnessMonotone__option_t) const
98
{
99
  return d_holder->ufssFairnessMonotone__setByUser__;
100
}
101
template <> const options::ufssTotalityLimited__option_t::type& Options::operator[](
102
    options::ufssTotalityLimited__option_t) const
103
{
104
  return d_holder->ufssTotalityLimited;
105
}
106
template <> bool Options::wasSetByUser(options::ufssTotalityLimited__option_t) const
107
{
108
  return d_holder->ufssTotalityLimited__setByUser__;
109
}
110
template <> const options::ufssTotalitySymBreak__option_t::type& Options::operator[](
111
    options::ufssTotalitySymBreak__option_t) const
112
{
113
  return d_holder->ufssTotalitySymBreak;
114
}
115
template <> bool Options::wasSetByUser(options::ufssTotalitySymBreak__option_t) const
116
{
117
  return d_holder->ufssTotalitySymBreak__setByUser__;
118
}
119
1202012
template <> const options::ufssMode__option_t::type& Options::operator[](
120
    options::ufssMode__option_t) const
121
{
122
1202012
  return d_holder->ufssMode;
123
}
124
template <> bool Options::wasSetByUser(options::ufssMode__option_t) const
125
{
126
  return d_holder->ufssMode__setByUser__;
127
}
128
129
130
namespace options {
131
132
thread_local struct ufSymmetryBreaker__option_t ufSymmetryBreaker;
133
thread_local struct ufHo__option_t ufHo;
134
thread_local struct ufHoExt__option_t ufHoExt;
135
thread_local struct ufssAbortCardinality__option_t ufssAbortCardinality;
136
thread_local struct ufssFairness__option_t ufssFairness;
137
thread_local struct ufssFairnessMonotone__option_t ufssFairnessMonotone;
138
thread_local struct ufssTotalityLimited__option_t ufssTotalityLimited;
139
thread_local struct ufssTotalitySymBreak__option_t ufssTotalitySymBreak;
140
thread_local struct ufssMode__option_t ufssMode;
141
142
143
std::ostream&
144
operator<<(std::ostream& os, UfssMode mode)
145
{
146
  os << "UfssMode::";
147
  switch(mode) {
148
    case UfssMode::FULL:
149
      os << "FULL";
150
      break;
151
    case UfssMode::NO_MINIMAL:
152
      os << "NO_MINIMAL";
153
      break;
154
    case UfssMode::NONE:
155
      os << "NONE";
156
      break;
157
    default:
158
        Unreachable();
159
  }
160
  return os;
161
}
162
163
UfssMode
164
7
stringToUfssMode(const std::string& option, const std::string& optarg)
165
{
166
7
  if (optarg == "full")
167
  {
168
    return UfssMode::FULL;
169
  }
170
7
  else if (optarg == "no-minimal")
171
  {
172
7
    return UfssMode::NO_MINIMAL;
173
  }
174
  else if (optarg == "none")
175
  {
176
    return UfssMode::NONE;
177
  }
178
  else if (optarg == "help")
179
  {
180
    puts("UF with cardinality options currently supported by the --uf-ss option when\n"
181
         "combined with finite model finding.\n"
182
         "Available modes for --uf-ss are:\n"
183
         "+ full (default)\n"
184
         "  Default, use UF with cardinality to find minimal models for uninterpreted\n"
185
         "  sorts.\n"
186
         "+ no-minimal\n"
187
         "  Use UF with cardinality to shrink models, but do no enforce minimality.\n"
188
         "+ none\n"
189
         "  Do not use UF with cardinality to shrink model sizes.\n");
190
    exit(1);
191
  }
192
  else
193
  {
194
    throw OptionException(std::string("unknown option for --uf-ss: `") +
195
                          optarg + "'.  Try --uf-ss=help.");
196
  }
197
}
198
199
200
}  // namespace options
201
26691
}  // namespace CVC4