GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/proof_options.h Lines: 11 13 84.6 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file module_template.h
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 Contains code for handling command-line options.
13
 **
14
 ** For each <module>_options.toml configuration file, mkoptions.py
15
 ** expands this template and generates a <module>_options.h file.
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__OPTIONS__PROOF_H
21
#define CVC4__OPTIONS__PROOF_H
22
23
#include "options/options.h"
24
25
26
27
28
#define CVC4_OPTIONS__PROOF__FOR_OPTION_HOLDER \
29
  proofEagerChecking__option_t::type proofEagerChecking;\
30
  bool proofEagerChecking__setByUser__; \
31
  proofFormatMode__option_t::type proofFormatMode;\
32
  bool proofFormatMode__setByUser__; \
33
  proofGranularityMode__option_t::type proofGranularityMode;\
34
  bool proofGranularityMode__setByUser__; \
35
  proofPedantic__option_t::type proofPedantic;\
36
  bool proofPedantic__setByUser__; \
37
  proofPrintConclusion__option_t::type proofPrintConclusion;\
38
  bool proofPrintConclusion__setByUser__;
39
40
41
namespace CVC4 {
42
43
namespace options {
44
45
46
enum class ProofFormatMode
47
{
48
  NONE,
49
  DOT
50
};
51
std::ostream&
52
operator<<(std::ostream& os, ProofFormatMode mode);
53
ProofFormatMode
54
stringToProofFormatMode(const std::string& option, const std::string& optarg);
55
enum class ProofGranularityMode
56
{
57
  DSL_REWRITE,
58
  OFF,
59
  REWRITE,
60
  THEORY_REWRITE
61
};
62
std::ostream&
63
operator<<(std::ostream& os, ProofGranularityMode mode);
64
ProofGranularityMode
65
stringToProofGranularityMode(const std::string& option, const std::string& optarg);
66
67
extern struct proofEagerChecking__option_t
68
{
69
  typedef bool type;
70
  type operator()() const;
71
  bool wasSetByUser() const;
72
  void set(const type& v);
73
  const char* getName() const;
74
} thread_local proofEagerChecking;
75
extern struct proofFormatMode__option_t
76
{
77
  typedef ProofFormatMode type;
78
  type operator()() const;
79
  bool wasSetByUser() const;
80
  void set(const type& v);
81
  const char* getName() const;
82
} thread_local proofFormatMode;
83
extern struct proofGranularityMode__option_t
84
{
85
  typedef ProofGranularityMode type;
86
  type operator()() const;
87
  bool wasSetByUser() const;
88
  void set(const type& v);
89
  const char* getName() const;
90
} thread_local proofGranularityMode;
91
extern struct proofPedantic__option_t
92
{
93
  typedef uint32_t type;
94
  type operator()() const;
95
  bool wasSetByUser() const;
96
  const char* getName() const;
97
} thread_local proofPedantic;
98
extern struct proofPrintConclusion__option_t
99
{
100
  typedef bool type;
101
  type operator()() const;
102
  bool wasSetByUser() const;
103
  const char* getName() const;
104
} thread_local proofPrintConclusion;
105
106
}  // namespace options
107
108
template <> void Options::set(
109
    options::proofEagerChecking__option_t,
110
    const options::proofEagerChecking__option_t::type& x);
111
template <> const options::proofEagerChecking__option_t::type& Options::operator[](
112
    options::proofEagerChecking__option_t) const;
113
template <> bool Options::wasSetByUser(options::proofEagerChecking__option_t) const;
114
template <> void Options::assignBool(
115
    options::proofEagerChecking__option_t,
116
    std::string option,
117
    bool value);
118
template <> void Options::set(
119
    options::proofFormatMode__option_t,
120
    const options::proofFormatMode__option_t::type& x);
121
template <> const options::proofFormatMode__option_t::type& Options::operator[](
122
    options::proofFormatMode__option_t) const;
123
template <> bool Options::wasSetByUser(options::proofFormatMode__option_t) const;
124
template <> void Options::assign(
125
    options::proofFormatMode__option_t,
126
    std::string option,
127
    std::string value);
128
template <> void Options::set(
129
    options::proofGranularityMode__option_t,
130
    const options::proofGranularityMode__option_t::type& x);
131
template <> const options::proofGranularityMode__option_t::type& Options::operator[](
132
    options::proofGranularityMode__option_t) const;
133
template <> bool Options::wasSetByUser(options::proofGranularityMode__option_t) const;
134
template <> void Options::assign(
135
    options::proofGranularityMode__option_t,
136
    std::string option,
137
    std::string value);
138
template <> const options::proofPedantic__option_t::type& Options::operator[](
139
    options::proofPedantic__option_t) const;
140
template <> bool Options::wasSetByUser(options::proofPedantic__option_t) const;
141
template <> void Options::assign(
142
    options::proofPedantic__option_t,
143
    std::string option,
144
    std::string value);
145
template <> const options::proofPrintConclusion__option_t::type& Options::operator[](
146
    options::proofPrintConclusion__option_t) const;
147
template <> bool Options::wasSetByUser(options::proofPrintConclusion__option_t) const;
148
template <> void Options::assignBool(
149
    options::proofPrintConclusion__option_t,
150
    std::string option,
151
    bool value);
152
153
154
namespace options {
155
156
9295286
inline proofEagerChecking__option_t::type proofEagerChecking__option_t::operator()() const
157
{
158
9295286
  return (*Options::current())[*this];
159
}
160
inline bool proofEagerChecking__option_t::wasSetByUser() const
161
{
162
  return Options::current()->wasSetByUser(*this);
163
}
164
19
inline void proofEagerChecking__option_t::set(const proofEagerChecking__option_t::type& v)
165
{
166
19
  Options::current()->set(*this, v);
167
19
}
168
inline const char* proofEagerChecking__option_t::getName() const
169
{
170
  return "proof-eager-checking";
171
}
172
inline proofFormatMode__option_t::type proofFormatMode__option_t::operator()() const
173
{
174
  return (*Options::current())[*this];
175
}
176
inline bool proofFormatMode__option_t::wasSetByUser() const
177
{
178
  return Options::current()->wasSetByUser(*this);
179
}
180
inline void proofFormatMode__option_t::set(const proofFormatMode__option_t::type& v)
181
{
182
  Options::current()->set(*this, v);
183
}
184
inline const char* proofFormatMode__option_t::getName() const
185
{
186
  return "proof-format-mode";
187
}
188
2886
inline proofGranularityMode__option_t::type proofGranularityMode__option_t::operator()() const
189
{
190
2886
  return (*Options::current())[*this];
191
}
192
inline bool proofGranularityMode__option_t::wasSetByUser() const
193
{
194
  return Options::current()->wasSetByUser(*this);
195
}
196
inline void proofGranularityMode__option_t::set(const proofGranularityMode__option_t::type& v)
197
{
198
  Options::current()->set(*this, v);
199
}
200
inline const char* proofGranularityMode__option_t::getName() const
201
{
202
  return "proof-granularity";
203
}
204
962
inline proofPedantic__option_t::type proofPedantic__option_t::operator()() const
205
{
206
962
  return (*Options::current())[*this];
207
}
208
inline bool proofPedantic__option_t::wasSetByUser() const
209
{
210
  return Options::current()->wasSetByUser(*this);
211
}
212
inline const char* proofPedantic__option_t::getName() const
213
{
214
  return "proof-pedantic";
215
}
216
199691
inline proofPrintConclusion__option_t::type proofPrintConclusion__option_t::operator()() const
217
{
218
199691
  return (*Options::current())[*this];
219
}
220
inline bool proofPrintConclusion__option_t::wasSetByUser() const
221
{
222
  return Options::current()->wasSetByUser(*this);
223
}
224
inline const char* proofPrintConclusion__option_t::getName() const
225
{
226
  return "proof-print-conclusion";
227
}
228
229
}  // namespace options
230
}  // namespace CVC4
231
232
#endif /* CVC4__OPTIONS__PROOF_H */