Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/parser/parser_builder.cpp	Lines:	74	76	97.4 %
Date:	2021-05-24	Branches:	26	43	60.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Christopher L. Conway, Morgan Deters, 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.
 */

// This must be included first.
#include "parser/parser_builder.h"

#include <string>

#include "api/cpp/cvc5.h"
#include "base/check.h"
#include "cvc/cvc.h"
#include "options/options.h"
#include "parser/antlr_input.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "smt2/smt2.h"
#include "tptp/tptp.h"

namespace cvc5 {
namespace parser {

ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm)
    : d_solver(solver), d_symman(sm)
{
  init(solver, sm);
}

ParserBuilder::ParserBuilder(api::Solver* solver,
                             SymbolManager* sm,
                             const Options& options)
    : d_solver(solver), d_symman(sm)
{
  init(solver, sm);
  withOptions(options);
}

void ParserBuilder::init(api::Solver* solver, SymbolManager* sm)
{
  d_lang = language::input::LANG_AUTO;
  d_solver = solver;
  d_symman = sm;
  d_checksEnabled = true;
  d_strictMode = false;
  d_canIncludeFile = true;
  d_parseOnly = false;
  d_logicIsForced = false;
  d_forcedLogic = "";
}

Parser* ParserBuilder::build()
{
  Parser* parser = NULL;
  switch (d_lang)
  {
    case language::input::LANG_SYGUS_V2:
      parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
      break;
    case language::input::LANG_TPTP:
      parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
      break;
    default:
      if (language::isInputLang_smt2(d_lang))
      {
        parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
      }
      else
      {
        parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
      }
      break;
  }

  if( d_checksEnabled ) {
    parser->enableChecks();
  } else {
    parser->disableChecks();
  }

  if( d_canIncludeFile ) {
    parser->allowIncludeFile();
  } else {
    parser->disallowIncludeFile();
  }

  if( d_logicIsForced ) {
    parser->forceLogic(d_forcedLogic);
  }

  return parser;
}

ParserBuilder& ParserBuilder::withChecks(bool flag) {
  d_checksEnabled = flag;
  return *this;
}

ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) {
  d_lang = lang;
  return *this;
}

ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
  d_parseOnly = flag;
  return *this;
}

ParserBuilder& ParserBuilder::withOptions(const Options& options) {
  ParserBuilder& retval = *this;
  retval =
      retval.withInputLanguage(options.getInputLanguage())
      .withChecks(options.getSemanticChecks())
      .withStrictMode(options.getStrictParsing())
      .withParseOnly(options.getParseOnly())
      .withIncludeFile(options.getFilesystemAccess());
  if(options.wasSetByUserForceLogicString()) {
    LogicInfo tmp(options.getForceLogicString());
    retval = retval.withForcedLogic(tmp.getLogicString());
  }
  return retval;
}

ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
  d_strictMode = flag;
  return *this;
}

ParserBuilder& ParserBuilder::withIncludeFile(bool flag) {
  d_canIncludeFile = flag;
  return *this;
}

ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) {
  d_logicIsForced = true;
  d_forcedLogic = logic;
  return *this;
}

}  // namespace parser
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Christopher L. Conway, Morgan Deters, Andrew Reynolds
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* A builder for parsers.
14		*/
15
16		// This must be included first.
17		#include "parser/parser_builder.h"
18
19		#include <string>
20
21		#include "api/cpp/cvc5.h"
22		#include "base/check.h"
23		#include "cvc/cvc.h"
24		#include "options/options.h"
25		#include "parser/antlr_input.h"
26		#include "parser/input.h"
27		#include "parser/parser.h"
28		#include "smt2/smt2.h"
29		#include "tptp/tptp.h"
30
31		namespace cvc5 {
32		namespace parser {
33
34	244	ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm)
35	244	: d_solver(solver), d_symman(sm)
36		{
37	244	init(solver, sm);
38	244	}
39
40	5902	ParserBuilder::ParserBuilder(api::Solver* solver,
41		SymbolManager* sm,
42	5902	const Options& options)
43	5902	: d_solver(solver), d_symman(sm)
44		{
45	5902	init(solver, sm);
46	5902	withOptions(options);
47	5902	}
48
49	6146	void ParserBuilder::init(api::Solver* solver, SymbolManager* sm)
50		{
51	6146	d_lang = language::input::LANG_AUTO;
52	6146	d_solver = solver;
53	6146	d_symman = sm;
54	6146	d_checksEnabled = true;
55	6146	d_strictMode = false;
56	6146	d_canIncludeFile = true;
57	6146	d_parseOnly = false;
58	6146	d_logicIsForced = false;
59	6146	d_forcedLogic = "";
60	6146	}
61
62	6146	Parser* ParserBuilder::build()
63		{
64	6146	Parser* parser = NULL;
65	6146	switch (d_lang)
66		{
67	191	case language::input::LANG_SYGUS_V2:
68	191	parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
69	191	break;
70	43	case language::input::LANG_TPTP:
71	43	parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
72	43	break;
73	5912	default:
74	5912	if (language::isInputLang_smt2(d_lang))
75		{
76	4973	parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
77		}
78		else
79		{
80	939	parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
81		}
82	5912	break;
83		}
84
85	6146	if( d_checksEnabled ) {
86	6146	parser->enableChecks();
87		} else {
88		parser->disableChecks();
89		}
90
91	6146	if( d_canIncludeFile ) {
92	6146	parser->allowIncludeFile();
93		} else {
94		parser->disallowIncludeFile();
95		}
96
97	6146	if( d_logicIsForced ) {
98	9	parser->forceLogic(d_forcedLogic);
99		}
100
101	6146	return parser;
102		}
103
104	6110	ParserBuilder& ParserBuilder::withChecks(bool flag) {
105	6110	d_checksEnabled = flag;
106	6110	return *this;
107		}
108
109	6354	ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) {
110	6354	d_lang = lang;
111	6354	return *this;
112		}
113
114	6110	ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
115	6110	d_parseOnly = flag;
116	6110	return *this;
117		}
118
119	6110	ParserBuilder& ParserBuilder::withOptions(const Options& options) {
120	6110	ParserBuilder& retval = *this;
121	6110	retval =
122	6110	retval.withInputLanguage(options.getInputLanguage())
123	6110	.withChecks(options.getSemanticChecks())
124	6110	.withStrictMode(options.getStrictParsing())
125	6110	.withParseOnly(options.getParseOnly())
126	6110	.withIncludeFile(options.getFilesystemAccess());
127	6110	if(options.wasSetByUserForceLogicString()) {
128	18	LogicInfo tmp(options.getForceLogicString());
129	9	retval = retval.withForcedLogic(tmp.getLogicString());
130		}
131	6110	return retval;
132		}
133
134	6212	ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
135	6212	d_strictMode = flag;
136	6212	return *this;
137		}
138
139	6110	ParserBuilder& ParserBuilder::withIncludeFile(bool flag) {
140	6110	d_canIncludeFile = flag;
141	6110	return *this;
142		}
143
144	9	ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) {
145	9	d_logicIsForced = true;
146	9	d_forcedLogic = logic;
147	9	return *this;
148		}
149
150		} // namespace parser
151	28179	} // namespace cvc5