GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/parser/parser_builder.cpp Lines: 104 123 84.6 %
Date: 2021-03-22 Branches: 33 96 34.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file parser_builder.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Christopher L. Conway, Morgan Deters, 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
// This must be included first.
18
#include "parser/parser_builder.h"
19
20
#include <string>
21
22
#include "api/cvc4cpp.h"
23
#include "base/check.h"
24
#include "cvc/cvc.h"
25
#include "options/options.h"
26
#include "parser/antlr_input.h"
27
#include "parser/input.h"
28
#include "parser/parser.h"
29
#include "smt2/smt2.h"
30
#include "tptp/tptp.h"
31
32
namespace CVC4 {
33
namespace parser {
34
35
244
ParserBuilder::ParserBuilder(api::Solver* solver,
36
                             SymbolManager* sm,
37
244
                             const std::string& filename)
38
244
    : d_filename(filename), d_solver(solver), d_symman(sm)
39
{
40
244
  init(solver, sm, filename);
41
244
}
42
43
5480
ParserBuilder::ParserBuilder(api::Solver* solver,
44
                             SymbolManager* sm,
45
                             const std::string& filename,
46
5480
                             const Options& options)
47
5480
    : d_filename(filename), d_solver(solver), d_symman(sm)
48
{
49
5480
  init(solver, sm, filename);
50
5480
  withOptions(options);
51
5480
}
52
53
5724
void ParserBuilder::init(api::Solver* solver,
54
                         SymbolManager* sm,
55
                         const std::string& filename)
56
{
57
5724
  d_inputType = FILE_INPUT;
58
5724
  d_lang = language::input::LANG_AUTO;
59
5724
  d_filename = filename;
60
5724
  d_streamInput = NULL;
61
5724
  d_solver = solver;
62
5724
  d_symman = sm;
63
5724
  d_checksEnabled = true;
64
5724
  d_strictMode = false;
65
5724
  d_canIncludeFile = true;
66
5724
  d_mmap = false;
67
5724
  d_parseOnly = false;
68
5724
  d_logicIsForced = false;
69
5724
  d_forcedLogic = "";
70
5724
}
71
72
5724
Parser* ParserBuilder::build()
73
{
74
5724
  Input* input = NULL;
75
5724
  switch( d_inputType ) {
76
5461
  case FILE_INPUT:
77
5461
    input = Input::newFileInput(d_lang, d_filename, d_mmap);
78
5461
    break;
79
  case LINE_BUFFERED_STREAM_INPUT:
80
    Assert(d_streamInput != NULL);
81
    input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true);
82
    break;
83
4
  case STREAM_INPUT:
84
4
    Assert(d_streamInput != NULL);
85
4
    input = Input::newStreamInput(d_lang, *d_streamInput, d_filename);
86
4
    break;
87
259
  case STRING_INPUT:
88
259
    input = Input::newStringInput(d_lang, d_stringInput, d_filename);
89
259
    break;
90
  }
91
92
5724
  Assert(input != NULL);
93
94
5724
  Parser* parser = NULL;
95
5724
  switch (d_lang)
96
  {
97
362
    case language::input::LANG_SYGUS_V2:
98
362
      parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly);
99
362
      break;
100
42
    case language::input::LANG_TPTP:
101
42
      parser = new Tptp(d_solver, d_symman, input, d_strictMode, d_parseOnly);
102
42
      break;
103
5320
    default:
104
5320
      if (language::isInputLang_smt2(d_lang))
105
      {
106
4633
        parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly);
107
      }
108
      else
109
      {
110
687
        parser = new Cvc(d_solver, d_symman, input, d_strictMode, d_parseOnly);
111
      }
112
5320
      break;
113
  }
114
115
5724
  if( d_checksEnabled ) {
116
5724
    parser->enableChecks();
117
  } else {
118
    parser->disableChecks();
119
  }
120
121
5724
  if( d_canIncludeFile ) {
122
5724
    parser->allowIncludeFile();
123
  } else {
124
    parser->disallowIncludeFile();
125
  }
126
127
5724
  if( d_logicIsForced ) {
128
9
    parser->forceLogic(d_forcedLogic);
129
  }
130
131
5724
  return parser;
132
}
133
134
5688
ParserBuilder& ParserBuilder::withChecks(bool flag) {
135
5688
  d_checksEnabled = flag;
136
5688
  return *this;
137
}
138
139
ParserBuilder& ParserBuilder::withSolver(api::Solver* solver)
140
{
141
  d_solver = solver;
142
  return *this;
143
}
144
145
ParserBuilder& ParserBuilder::withFileInput() {
146
  d_inputType = FILE_INPUT;
147
  return *this;
148
}
149
150
ParserBuilder& ParserBuilder::withFilename(const std::string& filename) {
151
  d_filename = filename;
152
  return *this;
153
}
154
155
5932
ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) {
156
5932
  d_lang = lang;
157
5932
  return *this;
158
}
159
160
5688
ParserBuilder& ParserBuilder::withMmap(bool flag) {
161
5688
  d_mmap = flag;
162
5688
  return *this;
163
}
164
165
5688
ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
166
5688
  d_parseOnly = flag;
167
5688
  return *this;
168
}
169
170
5688
ParserBuilder& ParserBuilder::withOptions(const Options& options) {
171
5688
  ParserBuilder& retval = *this;
172
5688
  retval =
173
5688
      retval.withInputLanguage(options.getInputLanguage())
174
5688
      .withMmap(options.getMemoryMap())
175
5688
      .withChecks(options.getSemanticChecks())
176
5688
      .withStrictMode(options.getStrictParsing())
177
5688
      .withParseOnly(options.getParseOnly())
178
5688
      .withIncludeFile(options.getFilesystemAccess());
179
5688
  if(options.wasSetByUserForceLogicString()) {
180
18
    LogicInfo tmp(options.getForceLogicString());
181
9
    retval = retval.withForcedLogic(tmp.getLogicString());
182
  }
183
5688
  return retval;
184
}
185
186
5790
ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
187
5790
  d_strictMode = flag;
188
5790
  return *this;
189
}
190
191
5688
ParserBuilder& ParserBuilder::withIncludeFile(bool flag) {
192
5688
  d_canIncludeFile = flag;
193
5688
  return *this;
194
}
195
196
9
ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) {
197
9
  d_logicIsForced = true;
198
9
  d_forcedLogic = logic;
199
9
  return *this;
200
}
201
202
4
ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) {
203
4
  d_inputType = STREAM_INPUT;
204
4
  d_streamInput = &input;
205
4
  return *this;
206
}
207
208
ParserBuilder& ParserBuilder::withLineBufferedStreamInput(std::istream& input) {
209
  d_inputType = LINE_BUFFERED_STREAM_INPUT;
210
  d_streamInput = &input;
211
  return *this;
212
}
213
214
259
ParserBuilder& ParserBuilder::withStringInput(const std::string& input) {
215
259
  d_inputType = STRING_INPUT;
216
259
  d_stringInput = input;
217
259
  return *this;
218
}
219
220
}/* CVC4::parser namespace */
221
26664
}/* CVC4 namespace */