Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/parser/parser_builder.cpp	Lines:	64	66	97.0 %
Date:	2021-09-21	Branches:	50	86	58.1 %


/******************************************************************************
 * 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 "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,
                             bool useOptions)
    : d_solver(solver), d_symman(sm)
{
  init(solver, sm);
  if (useOptions)
  {
    withOptions();
  }
}

void ParserBuilder::init(api::Solver* solver, SymbolManager* sm)
{
  d_lang = "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;
  if (d_lang == "LANG_SYGUS_V2" || d_lang == "LANG_SMTLIB_V2_6")
  {
    parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
  }
  else if (d_lang == "LANG_TPTP")
  {
    parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
  }
  else
  {
    parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
  }

  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(const std::string& lang)
{
  d_lang = lang;
  return *this;
}

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

ParserBuilder& ParserBuilder::withOptions()
{
  ParserBuilder& retval = *this;
  retval = retval.withInputLanguage(d_solver->getOption("input-language"))
               .withChecks(d_solver->getOptionInfo("semantic-checks").boolValue())
               .withStrictMode(d_solver->getOptionInfo("strict-parsing").boolValue())
               .withParseOnly(d_solver->getOptionInfo("parse-only").boolValue())
               .withIncludeFile(d_solver->getOptionInfo("filesystem-access").boolValue());
  auto info = d_solver->getOptionInfo("force-logic");
  if (info.setByUser)
  {
    LogicInfo tmp(info.stringValue());
    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 "parser/antlr_input.h"
25		#include "parser/input.h"
26		#include "parser/parser.h"
27		#include "smt2/smt2.h"
28		#include "tptp/tptp.h"
29
30		namespace cvc5 {
31		namespace parser {
32
33	6442	ParserBuilder::ParserBuilder(api::Solver* solver,
34		SymbolManager* sm,
35	6442	bool useOptions)
36	6442	: d_solver(solver), d_symman(sm)
37		{
38	6442	init(solver, sm);
39	6442	if (useOptions)
40		{
41	6406	withOptions();
42		}
43	6442	}
44
45	6442	void ParserBuilder::init(api::Solver* solver, SymbolManager* sm)
46		{
47	6442	d_lang = "LANG_AUTO";
48	6442	d_solver = solver;
49	6442	d_symman = sm;
50	6442	d_checksEnabled = true;
51	6442	d_strictMode = false;
52	6442	d_canIncludeFile = true;
53	6442	d_parseOnly = false;
54	6442	d_logicIsForced = false;
55	6442	d_forcedLogic = "";
56	6442	}
57
58	6442	Parser* ParserBuilder::build()
59		{
60	6442	Parser* parser = NULL;
61	6442	if (d_lang == "LANG_SYGUS_V2" \|\| d_lang == "LANG_SMTLIB_V2_6")
62		{
63	5475	parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
64		}
65	967	else if (d_lang == "LANG_TPTP")
66		{
67	41	parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
68		}
69		else
70		{
71	926	parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
72		}
73
74	6442	if( d_checksEnabled ) {
75	6442	parser->enableChecks();
76		} else {
77		parser->disableChecks();
78		}
79
80	6442	if( d_canIncludeFile ) {
81	6442	parser->allowIncludeFile();
82		} else {
83		parser->disallowIncludeFile();
84		}
85
86	6442	if( d_logicIsForced ) {
87	9	parser->forceLogic(d_forcedLogic);
88		}
89
90	6442	return parser;
91		}
92
93	6406	ParserBuilder& ParserBuilder::withChecks(bool flag) {
94	6406	d_checksEnabled = flag;
95	6406	return *this;
96		}
97
98	6650	ParserBuilder& ParserBuilder::withInputLanguage(const std::string& lang)
99		{
100	6650	d_lang = lang;
101	6650	return *this;
102		}
103
104	6406	ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
105	6406	d_parseOnly = flag;
106	6406	return *this;
107		}
108
109	6406	ParserBuilder& ParserBuilder::withOptions()
110		{
111	6406	ParserBuilder& retval = *this;
112	19218	retval = retval.withInputLanguage(d_solver->getOption("input-language"))
113	12812	.withChecks(d_solver->getOptionInfo("semantic-checks").boolValue())
114	12812	.withStrictMode(d_solver->getOptionInfo("strict-parsing").boolValue())
115	12812	.withParseOnly(d_solver->getOptionInfo("parse-only").boolValue())
116	12812	.withIncludeFile(d_solver->getOptionInfo("filesystem-access").boolValue());
117	12812	auto info = d_solver->getOptionInfo("force-logic");
118	6406	if (info.setByUser)
119		{
120	18	LogicInfo tmp(info.stringValue());
121	9	retval = retval.withForcedLogic(tmp.getLogicString());
122		}
123	12812	return retval;
124		}
125
126	6508	ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
127	6508	d_strictMode = flag;
128	6508	return *this;
129		}
130
131	6406	ParserBuilder& ParserBuilder::withIncludeFile(bool flag) {
132	6406	d_canIncludeFile = flag;
133	6406	return *this;
134		}
135
136	9	ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic)
137		{
138	9	d_logicIsForced = true;
139	9	d_forcedLogic = logic;
140	9	return *this;
141		}
142
143		} // namespace parser
144	29574	} // namespace cvc5