GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/proof_options.cpp Lines: 12 84 14.3 %
Date: 2021-03-23 Branches: 2 52 3.8 %

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
19
template <> void Options::set(
24
    options::proofEagerChecking__option_t,
25
    const options::proofEagerChecking__option_t::type& x)
26
{
27
19
  d_holder->proofEagerChecking = x;
28
19
}
29
9295472
template <> const options::proofEagerChecking__option_t::type& Options::operator[](
30
    options::proofEagerChecking__option_t) const
31
{
32
9295472
  return d_holder->proofEagerChecking;
33
}
34
template <> bool Options::wasSetByUser(options::proofEagerChecking__option_t) const
35
{
36
  return d_holder->proofEagerChecking__setByUser__;
37
}
38
template <> void Options::set(
39
    options::proofFormatMode__option_t,
40
    const options::proofFormatMode__option_t::type& x)
41
{
42
  d_holder->proofFormatMode = x;
43
}
44
template <> const options::proofFormatMode__option_t::type& Options::operator[](
45
    options::proofFormatMode__option_t) const
46
{
47
  return d_holder->proofFormatMode;
48
}
49
template <> bool Options::wasSetByUser(options::proofFormatMode__option_t) const
50
{
51
  return d_holder->proofFormatMode__setByUser__;
52
}
53
template <> void Options::set(
54
    options::proofGranularityMode__option_t,
55
    const options::proofGranularityMode__option_t::type& x)
56
{
57
  d_holder->proofGranularityMode = x;
58
}
59
2886
template <> const options::proofGranularityMode__option_t::type& Options::operator[](
60
    options::proofGranularityMode__option_t) const
61
{
62
2886
  return d_holder->proofGranularityMode;
63
}
64
template <> bool Options::wasSetByUser(options::proofGranularityMode__option_t) const
65
{
66
  return d_holder->proofGranularityMode__setByUser__;
67
}
68
962
template <> const options::proofPedantic__option_t::type& Options::operator[](
69
    options::proofPedantic__option_t) const
70
{
71
962
  return d_holder->proofPedantic;
72
}
73
template <> bool Options::wasSetByUser(options::proofPedantic__option_t) const
74
{
75
  return d_holder->proofPedantic__setByUser__;
76
}
77
199691
template <> const options::proofPrintConclusion__option_t::type& Options::operator[](
78
    options::proofPrintConclusion__option_t) const
79
{
80
199691
  return d_holder->proofPrintConclusion;
81
}
82
template <> bool Options::wasSetByUser(options::proofPrintConclusion__option_t) const
83
{
84
  return d_holder->proofPrintConclusion__setByUser__;
85
}
86
87
88
namespace options {
89
90
thread_local struct proofEagerChecking__option_t proofEagerChecking;
91
thread_local struct proofFormatMode__option_t proofFormatMode;
92
thread_local struct proofGranularityMode__option_t proofGranularityMode;
93
thread_local struct proofPedantic__option_t proofPedantic;
94
thread_local struct proofPrintConclusion__option_t proofPrintConclusion;
95
96
97
std::ostream&
98
operator<<(std::ostream& os, ProofFormatMode mode)
99
{
100
  os << "ProofFormatMode::";
101
  switch(mode) {
102
    case ProofFormatMode::DOT:
103
      os << "DOT";
104
      break;
105
    case ProofFormatMode::NONE:
106
      os << "NONE";
107
      break;
108
    default:
109
        Unreachable();
110
  }
111
  return os;
112
}
113
114
ProofFormatMode
115
stringToProofFormatMode(const std::string& option, const std::string& optarg)
116
{
117
  if (optarg == "dot")
118
  {
119
    return ProofFormatMode::DOT;
120
  }
121
  else if (optarg == "none")
122
  {
123
    return ProofFormatMode::NONE;
124
  }
125
  else if (optarg == "help")
126
  {
127
    puts("Proof format modes.\n"
128
         "Available modes for --proof-format-mode are:\n"
129
         "+ dot\n"
130
         "  Output DOT proof\n"
131
         "+ none (default)\n"
132
         "  Do not translate proof output\n");
133
    exit(1);
134
  }
135
  else
136
  {
137
    throw OptionException(std::string("unknown option for --proof-format-mode: `") +
138
                          optarg + "'.  Try --proof-format-mode=help.");
139
  }
140
}
141
142
std::ostream&
143
operator<<(std::ostream& os, ProofGranularityMode mode)
144
{
145
  os << "ProofGranularityMode::";
146
  switch(mode) {
147
    case ProofGranularityMode::DSL_REWRITE:
148
      os << "DSL_REWRITE";
149
      break;
150
    case ProofGranularityMode::REWRITE:
151
      os << "REWRITE";
152
      break;
153
    case ProofGranularityMode::THEORY_REWRITE:
154
      os << "THEORY_REWRITE";
155
      break;
156
    case ProofGranularityMode::OFF:
157
      os << "OFF";
158
      break;
159
    default:
160
        Unreachable();
161
  }
162
  return os;
163
}
164
165
ProofGranularityMode
166
stringToProofGranularityMode(const std::string& option, const std::string& optarg)
167
{
168
  if (optarg == "dsl-rewrite")
169
  {
170
    return ProofGranularityMode::DSL_REWRITE;
171
  }
172
  else if (optarg == "rewrite")
173
  {
174
    return ProofGranularityMode::REWRITE;
175
  }
176
  else if (optarg == "theory-rewrite")
177
  {
178
    return ProofGranularityMode::THEORY_REWRITE;
179
  }
180
  else if (optarg == "off")
181
  {
182
    return ProofGranularityMode::OFF;
183
  }
184
  else if (optarg == "help")
185
  {
186
    puts("Modes for proof granularity.\n"
187
         "Available modes for --proof-granularity are:\n"
188
         "+ dsl-rewrite\n"
189
         "  Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution,\n"
190
         "  and theory rewrite steps.\n"
191
         "+ rewrite\n"
192
         "  Allow rewrite or substitution steps, expand macros.\n"
193
         "+ theory-rewrite (default)\n"
194
         "  Allow theory rewrite steps, expand macros, rewrite and substitution steps.\n"
195
         "+ off\n"
196
         "  Do not improve the granularity of proofs.\n");
197
    exit(1);
198
  }
199
  else
200
  {
201
    throw OptionException(std::string("unknown option for --proof-granularity: `") +
202
                          optarg + "'.  Try --proof-granularity=help.");
203
  }
204
}
205
206
207
}  // namespace options
208
26685
}  // namespace CVC4