GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/parser/parser_builder.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file parser_builder.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Christopher L. Conway, Andrew Reynolds
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 A builder for parsers.
13
 **
14
 ** A builder for parsers.
15
 **/
16
17
#include "cvc4parser_public.h"
18
19
#ifndef CVC4__PARSER__PARSER_BUILDER_H
20
#define CVC4__PARSER__PARSER_BUILDER_H
21
22
#include <string>
23
24
#include "cvc4_export.h"
25
#include "options/language.h"
26
#include "parser/input.h"
27
28
namespace CVC4 {
29
30
namespace api {
31
class Solver;
32
}
33
34
class Options;
35
class SymbolManager;
36
37
namespace parser {
38
39
class Parser;
40
41
/**
42
 * A builder for input language parsers. <code>build()</code> can be
43
 * called any number of times on an instance and will generate a fresh
44
 * parser each time.
45
 */
46
11425
class CVC4_EXPORT ParserBuilder
47
{
48
  enum InputType {
49
    FILE_INPUT,
50
    LINE_BUFFERED_STREAM_INPUT,
51
    STREAM_INPUT,
52
    STRING_INPUT
53
  };
54
55
  /** The input type. */
56
  InputType d_inputType;
57
58
  /** The input language */
59
  InputLanguage d_lang;
60
61
  /** The file name (may not exist) */
62
  std::string d_filename;
63
64
  /** The string input, if any. */
65
  std::string d_stringInput;
66
67
  /** The stream input, if any. */
68
  std::istream* d_streamInput;
69
70
  /** The API Solver object. */
71
  api::Solver* d_solver;
72
73
  /** The symbol manager */
74
  SymbolManager* d_symman;
75
76
  /** Should semantic checks be enabled during parsing? */
77
  bool d_checksEnabled;
78
79
  /** Should we parse in strict mode? */
80
  bool d_strictMode;
81
82
  /** Should we allow include-file commands? */
83
  bool d_canIncludeFile;
84
85
  /** Should we memory-map a file input? */
86
  bool d_mmap;
87
88
  /** Are we parsing only? */
89
  bool d_parseOnly;
90
91
  /** Is the logic forced by the user? */
92
  bool d_logicIsForced;
93
94
  /** The forced logic name */
95
  std::string d_forcedLogic;
96
97
  /** Initialize this parser builder */
98
  void init(api::Solver* solver,
99
            SymbolManager* sm,
100
            const std::string& filename);
101
102
 public:
103
  /** Create a parser builder using the given Solver and filename. */
104
  ParserBuilder(api::Solver* solver,
105
                SymbolManager* sm,
106
                const std::string& filename);
107
108
  ParserBuilder(api::Solver* solver,
109
                SymbolManager* sm,
110
                const std::string& filename,
111
                const Options& options);
112
113
  /** Build the parser, using the current settings. */
114
  Parser* build();
115
116
  /** Should semantic checks be enabled in the parser? (Default: yes) */
117
  ParserBuilder& withChecks(bool flag = true);
118
119
  /** Set the Solver to use with the parser. */
120
  ParserBuilder& withSolver(api::Solver* solver);
121
122
  /** Set the parser to read a file for its input. (Default) */
123
  ParserBuilder& withFileInput();
124
125
  /**
126
   * Set the filename for use by the parser. If file input is used,
127
   * this file will be opened and read by the parser. Otherwise, the
128
   * filename string (possibly a non-existent path) will only be used
129
   * in error messages.
130
   */
131
  ParserBuilder& withFilename(const std::string& filename);
132
133
  /**
134
   * Set the input language to be used by the parser.
135
   *
136
   * (Default: LANG_AUTO)
137
   */
138
  ParserBuilder& withInputLanguage(InputLanguage lang);
139
140
  /**
141
   * Should the parser memory-map its input? This is only relevant if
142
   * the parser will have a file input.
143
   *
144
   * (Default: no)
145
   */
146
  ParserBuilder& withMmap(bool flag = true);
147
148
  /**
149
   * Are we only parsing, or doing something with the resulting
150
   * commands and expressions?  This setting affects whether the
151
   * parser will raise certain errors about unimplemented features,
152
   * even if there isn't a parsing error, because the result of the
153
   * parse would otherwise be an incorrect parse tree and the error
154
   * would go undetected.  This is specifically for circumstances
155
   * where the parser is ahead of the functionality present elsewhere
156
   * in CVC4 (such as quantifiers, subtypes, records, etc. in the CVC
157
   * language parser).
158
   */
159
  ParserBuilder& withParseOnly(bool flag = true);
160
161
  /** Derive settings from the given options. */
162
  ParserBuilder& withOptions(const Options& options);
163
164
  /**
165
   * Should the parser use strict mode?
166
   *
167
   * (Default: no)
168
   */
169
  ParserBuilder& withStrictMode(bool flag = true);
170
171
  /**
172
   * Should the include-file commands be enabled?
173
   *
174
   * (Default: yes)
175
   */
176
  ParserBuilder& withIncludeFile(bool flag = true);
177
178
  /** Set the parser to use the given stream for its input. */
179
  ParserBuilder& withStreamInput(std::istream& input);
180
181
  /** Set the parser to use the given stream for its input. */
182
  ParserBuilder& withLineBufferedStreamInput(std::istream& input);
183
184
  /** Set the parser to use the given string for its input. */
185
  ParserBuilder& withStringInput(const std::string& input);
186
187
  /** Set the parser to use the given logic string. */
188
  ParserBuilder& withForcedLogic(const std::string& logic);
189
}; /* class ParserBuilder */
190
191
}/* CVC4::parser namespace */
192
}/* CVC4 namespace */
193
194
#endif /* CVC4__PARSER__PARSER_BUILDER_H */