GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/printer_options.cpp Lines: 11 80 13.8 %
Date: 2021-03-22 Branches: 4 46 8.7 %

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 <> void Options::set(
24
    options::flattenHOChains__option_t,
25
    const options::flattenHOChains__option_t::type& x)
26
{
27
  d_holder->flattenHOChains = x;
28
}
29
template <> const options::flattenHOChains__option_t::type& Options::operator[](
30
    options::flattenHOChains__option_t) const
31
{
32
  return d_holder->flattenHOChains;
33
}
34
template <> bool Options::wasSetByUser(options::flattenHOChains__option_t) const
35
{
36
  return d_holder->flattenHOChains__setByUser__;
37
}
38
template <> void Options::set(
39
    options::instFormatMode__option_t,
40
    const options::instFormatMode__option_t::type& x)
41
{
42
  d_holder->instFormatMode = x;
43
}
44
109
template <> const options::instFormatMode__option_t::type& Options::operator[](
45
    options::instFormatMode__option_t) const
46
{
47
109
  return d_holder->instFormatMode;
48
}
49
template <> bool Options::wasSetByUser(options::instFormatMode__option_t) const
50
{
51
  return d_holder->instFormatMode__setByUser__;
52
}
53
template <> void Options::set(
54
    options::modelFormatMode__option_t,
55
    const options::modelFormatMode__option_t::type& x)
56
{
57
  d_holder->modelFormatMode = x;
58
}
59
template <> const options::modelFormatMode__option_t::type& Options::operator[](
60
    options::modelFormatMode__option_t) const
61
{
62
  return d_holder->modelFormatMode;
63
}
64
template <> bool Options::wasSetByUser(options::modelFormatMode__option_t) const
65
{
66
  return d_holder->modelFormatMode__setByUser__;
67
}
68
template <> void Options::set(
69
    options::printInstFull__option_t,
70
    const options::printInstFull__option_t::type& x)
71
{
72
  d_holder->printInstFull = x;
73
}
74
12
template <> const options::printInstFull__option_t::type& Options::operator[](
75
    options::printInstFull__option_t) const
76
{
77
12
  return d_holder->printInstFull;
78
}
79
template <> bool Options::wasSetByUser(options::printInstFull__option_t) const
80
{
81
  return d_holder->printInstFull__setByUser__;
82
}
83
template <> void Options::set(
84
    options::printInstMode__option_t,
85
    const options::printInstMode__option_t::type& x)
86
{
87
  d_holder->printInstMode = x;
88
}
89
30
template <> const options::printInstMode__option_t::type& Options::operator[](
90
    options::printInstMode__option_t) const
91
{
92
30
  return d_holder->printInstMode;
93
}
94
template <> bool Options::wasSetByUser(options::printInstMode__option_t) const
95
{
96
  return d_holder->printInstMode__setByUser__;
97
}
98
99
100
namespace options {
101
102
thread_local struct flattenHOChains__option_t flattenHOChains;
103
thread_local struct instFormatMode__option_t instFormatMode;
104
thread_local struct modelFormatMode__option_t modelFormatMode;
105
thread_local struct printInstFull__option_t printInstFull;
106
thread_local struct printInstMode__option_t printInstMode;
107
108
109
std::ostream&
110
operator<<(std::ostream& os, ModelFormatMode mode)
111
{
112
  os << "ModelFormatMode::";
113
  switch(mode) {
114
    case ModelFormatMode::TABLE:
115
      os << "TABLE";
116
      break;
117
    case ModelFormatMode::DEFAULT:
118
      os << "DEFAULT";
119
      break;
120
    default:
121
        Unreachable();
122
  }
123
  return os;
124
}
125
126
ModelFormatMode
127
stringToModelFormatMode(const std::string& option, const std::string& optarg)
128
{
129
  if (optarg == "table")
130
  {
131
    return ModelFormatMode::TABLE;
132
  }
133
  else if (optarg == "default")
134
  {
135
    return ModelFormatMode::DEFAULT;
136
  }
137
  else if (optarg == "help")
138
  {
139
    puts("Model format modes.\n"
140
         "Available modes for --model-format are:\n"
141
         "+ table\n"
142
         "  Print functional expressions over finite domains in a table format.\n"
143
         "+ default\n"
144
         "  Print model as expressions in the output language format.\n");
145
    exit(1);
146
  }
147
  else
148
  {
149
    throw OptionException(std::string("unknown option for --model-format: `") +
150
                          optarg + "'.  Try --model-format=help.");
151
  }
152
}
153
154
std::ostream&
155
operator<<(std::ostream& os, PrintInstMode mode)
156
{
157
  os << "PrintInstMode::";
158
  switch(mode) {
159
    case PrintInstMode::LIST:
160
      os << "LIST";
161
      break;
162
    case PrintInstMode::NUM:
163
      os << "NUM";
164
      break;
165
    default:
166
        Unreachable();
167
  }
168
  return os;
169
}
170
171
PrintInstMode
172
3
stringToPrintInstMode(const std::string& option, const std::string& optarg)
173
{
174
3
  if (optarg == "list")
175
  {
176
    return PrintInstMode::LIST;
177
  }
178
3
  else if (optarg == "num")
179
  {
180
3
    return PrintInstMode::NUM;
181
  }
182
  else if (optarg == "help")
183
  {
184
    puts("Print format for printing instantiations.\n"
185
         "Available modes for --print-inst are:\n"
186
         "+ list (default)\n"
187
         "  Print the list of instantiations per quantified formula, when non-empty.\n"
188
         "+ num\n"
189
         "  Print the total number of instantiations per quantified formula, when\n"
190
         "  non-zero.\n");
191
    exit(1);
192
  }
193
  else
194
  {
195
    throw OptionException(std::string("unknown option for --print-inst: `") +
196
                          optarg + "'.  Try --print-inst=help.");
197
  }
198
}
199
200
201
}  // namespace options
202
26676
}  // namespace CVC4