Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/parser/parser_builder.cpp	Lines:	73	75	97.3 %
Date:	2021-08-17	Branches:	25	41	61.0 %


/******************************************************************************
 * 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/base_options.h"
#include "options/options.h"
#include "options/parser_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& opts)
{
  ParserBuilder& retval = *this;
  retval = retval.withInputLanguage(opts.base.inputLanguage)
               .withChecks(opts.parser.semanticChecks)
               .withStrictMode(opts.parser.strictParsing)
               .withParseOnly(opts.base.parseOnly)
               .withIncludeFile(opts.parser.filesystemAccess);
  if (opts.parser.forceLogicStringWasSetByUser)
  {
    LogicInfo tmp(opts.parser.forceLogicString);
    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/base_options.h"
25		#include "options/options.h"
26		#include "options/parser_options.h"
27		#include "parser/antlr_input.h"
28		#include "parser/input.h"
29		#include "parser/parser.h"
30		#include "smt2/smt2.h"
31		#include "tptp/tptp.h"
32
33		namespace cvc5 {
34		namespace parser {
35
36	244	ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm)
37	244	: d_solver(solver), d_symman(sm)
38		{
39	244	init(solver, sm);
40	244	}
41
42	6153	ParserBuilder::ParserBuilder(api::Solver* solver,
43		SymbolManager* sm,
44	6153	const Options& options)
45	6153	: d_solver(solver), d_symman(sm)
46		{
47	6153	init(solver, sm);
48	6153	withOptions(options);
49	6153	}
50
51	6397	void ParserBuilder::init(api::Solver* solver, SymbolManager* sm)
52		{
53	6397	d_lang = language::input::LANG_AUTO;
54	6397	d_solver = solver;
55	6397	d_symman = sm;
56	6397	d_checksEnabled = true;
57	6397	d_strictMode = false;
58	6397	d_canIncludeFile = true;
59	6397	d_parseOnly = false;
60	6397	d_logicIsForced = false;
61	6397	d_forcedLogic = "";
62	6397	}
63
64	6397	Parser* ParserBuilder::build()
65		{
66	6397	Parser* parser = NULL;
67	6397	switch (d_lang)
68		{
69	194	case language::input::LANG_SYGUS_V2:
70	194	parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
71	194	break;
72	41	case language::input::LANG_TPTP:
73	41	parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
74	41	break;
75	6162	default:
76	6162	if (language::isInputLang_smt2(d_lang))
77		{
78	5225	parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
79		}
80		else
81		{
82	937	parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
83		}
84	6162	break;
85		}
86
87	6397	if( d_checksEnabled ) {
88	6397	parser->enableChecks();
89		} else {
90		parser->disableChecks();
91		}
92
93	6397	if( d_canIncludeFile ) {
94	6397	parser->allowIncludeFile();
95		} else {
96		parser->disallowIncludeFile();
97		}
98
99	6397	if( d_logicIsForced ) {
100	9	parser->forceLogic(d_forcedLogic);
101		}
102
103	6397	return parser;
104		}
105
106	6361	ParserBuilder& ParserBuilder::withChecks(bool flag) {
107	6361	d_checksEnabled = flag;
108	6361	return *this;
109		}
110
111	6605	ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) {
112	6605	d_lang = lang;
113	6605	return *this;
114		}
115
116	6361	ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
117	6361	d_parseOnly = flag;
118	6361	return *this;
119		}
120
121	6361	ParserBuilder& ParserBuilder::withOptions(const Options& opts)
122		{
123	6361	ParserBuilder& retval = *this;
124	12722	retval = retval.withInputLanguage(opts.base.inputLanguage)
125	6361	.withChecks(opts.parser.semanticChecks)
126	6361	.withStrictMode(opts.parser.strictParsing)
127	6361	.withParseOnly(opts.base.parseOnly)
128	6361	.withIncludeFile(opts.parser.filesystemAccess);
129	6361	if (opts.parser.forceLogicStringWasSetByUser)
130		{
131	18	LogicInfo tmp(opts.parser.forceLogicString);
132	9	retval = retval.withForcedLogic(tmp.getLogicString());
133		}
134	6361	return retval;
135		}
136
137	6463	ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
138	6463	d_strictMode = flag;
139	6463	return *this;
140		}
141
142	6361	ParserBuilder& ParserBuilder::withIncludeFile(bool flag) {
143	6361	d_canIncludeFile = flag;
144	6361	return *this;
145		}
146
147	9	ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic)
148		{
149	9	d_logicIsForced = true;
150	9	d_forcedLogic = logic;
151	9	return *this;
152		}
153
154		} // namespace parser
155	29322	} // namespace cvc5