1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
/******************************************************************************
* Top contributors (to current version):
* Morgan Deters, Christopher L. Conway, Andrew Reynolds
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* A builder for parsers.
*/
#include "cvc5parser_public.h"
#ifndef CVC5__PARSER__PARSER_BUILDER_H
#define CVC5__PARSER__PARSER_BUILDER_H
#include <string>
#include "cvc5_export.h"
#include "options/language.h"
#include "parser/input.h"
namespace cvc5 {
namespace api {
class Solver;
}
class Options;
class SymbolManager;
namespace parser {
class Parser;
/**
* A builder for input language parsers. <code>build()</code> can be
* called any number of times on an instance and will generate a fresh
* parser each time.
*/
class CVC5_EXPORT ParserBuilder
{
/** The input language */
InputLanguage d_lang;
/** The API Solver object. */
api::Solver* d_solver;
/** The symbol manager */
SymbolManager* d_symman;
/** Should semantic checks be enabled during parsing? */
bool d_checksEnabled;
/** Should we parse in strict mode? */
bool d_strictMode;
/** Should we allow include-file commands? */
bool d_canIncludeFile;
/** Are we parsing only? */
bool d_parseOnly;
/** Is the logic forced by the user? */
bool d_logicIsForced;
/** The forced logic name */
std::string d_forcedLogic;
/** Initialize this parser builder */
void init(api::Solver* solver, SymbolManager* sm);
public:
/** Create a parser builder using the given Solver and filename. */
ParserBuilder(api::Solver* solver, SymbolManager* sm);
ParserBuilder(api::Solver* solver,
SymbolManager* sm,
const Options& options);
/** Build the parser, using the current settings. */
Parser* build();
/** Should semantic checks be enabled in the parser? (Default: yes) */
ParserBuilder& withChecks(bool flag = true);
/**
* Set the input language to be used by the parser.
*
* (Default: LANG_AUTO)
*/
ParserBuilder& withInputLanguage(InputLanguage lang);
/**
* Are we only parsing, or doing something with the resulting
* commands and expressions? This setting affects whether the
* parser will raise certain errors about unimplemented features,
* even if there isn't a parsing error, because the result of the
* parse would otherwise be an incorrect parse tree and the error
* would go undetected. This is specifically for circumstances
* where the parser is ahead of the functionality present elsewhere
* in cvc5 (such as quantifiers, subtypes, records, etc. in the CVC
* language parser).
*/
ParserBuilder& withParseOnly(bool flag = true);
/** Derive settings from the given options. */
ParserBuilder& withOptions(const Options& options);
/**
* Should the parser use strict mode?
*
* (Default: no)
*/
ParserBuilder& withStrictMode(bool flag = true);
/**
* Should the include-file commands be enabled?
*
* (Default: yes)
*/
ParserBuilder& withIncludeFile(bool flag = true);
/** Set the parser to use the given logic string. */
ParserBuilder& withForcedLogic(const std::string& logic);
}; /* class ParserBuilder */
} // namespace parser
} // namespace cvc5
#endif /* CVC5__PARSER__PARSER_BUILDER_H */
|
