summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g2
-rw-r--r--src/parser/parser.cpp20
-rw-r--r--src/parser/parser.h3
-rw-r--r--src/parser/smt2/Smt2.g8
-rw-r--r--src/parser/smt2/smt2.cpp11
-rw-r--r--src/parser/tptp/tptp.cpp16
6 files changed, 26 insertions, 34 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 64eb56c74..abfd363f8 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2331,7 +2331,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
)* RBRACKET
)?
{
- datatypes.push_back(Datatype(PARSER_STATE->getExprManager(),
+ datatypes.push_back(Datatype(SOLVER->getExprManager(),
id,
api::sortVectorToTypes(params),
false));
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 87fa93dcc..e9a037d6e 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -76,11 +76,6 @@ Parser::~Parser() {
delete d_input;
}
-ExprManager* Parser::getExprManager() const
-{
- return d_solver->getExprManager();
-}
-
api::Solver* Parser::getSolver() const { return d_solver; }
api::Term Parser::getSymbol(const std::string& name, SymbolType type)
@@ -339,7 +334,7 @@ void Parser::defineParameterizedType(const std::string& name,
api::Sort Parser::mkSort(const std::string& name, uint32_t flags)
{
Debug("parser") << "newSort(" << name << ")" << std::endl;
- api::Sort type = getExprManager()->mkSort(name, flags);
+ api::Sort type = d_solver->getExprManager()->mkSort(name, flags);
defineType(
name,
type,
@@ -353,7 +348,8 @@ api::Sort Parser::mkSortConstructor(const std::string& name,
{
Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
<< std::endl;
- api::Sort type = getExprManager()->mkSortConstructor(name, arity, flags);
+ api::Sort type =
+ d_solver->getExprManager()->mkSortConstructor(name, arity, flags);
defineType(
name,
vector<api::Sort>(arity),
@@ -383,7 +379,7 @@ api::Sort Parser::mkUnresolvedTypeConstructor(
{
Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
<< ")" << std::endl;
- api::Sort unresolved = getExprManager()->mkSortConstructor(
+ api::Sort unresolved = d_solver->getExprManager()->mkSortConstructor(
name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER);
defineType(name, params, unresolved);
api::Sort t = getSort(name, params);
@@ -404,7 +400,8 @@ std::vector<api::Sort> Parser::mkMutualDatatypeTypes(
try {
std::set<Type> tset = api::sortSetToTypes(d_unresolved);
std::vector<DatatypeType> dtypes =
- getExprManager()->mkMutualDatatypeTypes(datatypes, tset, flags);
+ d_solver->getExprManager()->mkMutualDatatypeTypes(
+ datatypes, tset, flags);
std::vector<api::Sort> types;
for (unsigned i = 0, dtsize = dtypes.size(); i < dtsize; i++)
{
@@ -593,7 +590,7 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
// parametric datatype.
if (s.isParametricDatatype())
{
- ExprManager* em = getExprManager();
+ ExprManager* em = d_solver->getExprManager();
// apply type ascription to the operator
Expr e = t.getExpr();
const DatatypeConstructor& dtc =
@@ -633,7 +630,8 @@ api::Term Parser::mkVar(const std::string& name,
const api::Sort& type,
uint32_t flags)
{
- return api::Term(getExprManager()->mkVar(name, type.getType(), flags));
+ return api::Term(
+ d_solver->getExprManager()->mkVar(name, type.getType(), flags));
}
//!!!!!!!!!!! temporary
diff --git a/src/parser/parser.h b/src/parser/parser.h
index c7efcbacb..1197c1ff6 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -265,9 +265,6 @@ public:
virtual ~Parser();
- /** Get the associated <code>ExprManager</code>. */
- ExprManager* getExprManager() const;
-
/** Get the associated solver. */
api::Solver* getSolver() const;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index aa62eab5d..d87c44a68 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -959,7 +959,7 @@ sygusGrammar[CVC4::api::Sort & ret,
Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
// make the datatype, which encodes terms generated by this non-terminal
std::string dname = i.first;
- datatypes.push_back(Datatype(PARSER_STATE->getExprManager(), dname));
+ datatypes.push_back(Datatype(SOLVER->getExprManager(), dname));
// make its unresolved type, used for referencing the final version of
// the datatype
PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
@@ -1537,7 +1537,7 @@ datatypesDef[bool isCo,
PARSER_STATE->parseError("Wrong number of parameters for datatype.");
}
Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
- dts.push_back(Datatype(PARSER_STATE->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo));
+ dts.push_back(Datatype(SOLVER->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo));
}
LPAREN_TOK
( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
@@ -1547,7 +1547,7 @@ datatypesDef[bool isCo,
PARSER_STATE->parseError("No parameters given for datatype.");
}
Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
- dts.push_back(Datatype(PARSER_STATE->getExprManager(),
+ dts.push_back(Datatype(SOLVER->getExprManager(),
dnames[dts.size()],
api::sortVectorToTypes(params),
isCo));
@@ -2532,7 +2532,7 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
* below. */
: symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
{
- datatypes.push_back(Datatype(PARSER_STATE->getExprManager(),
+ datatypes.push_back(Datatype(SOLVER->getExprManager(),
id,
api::sortVectorToTypes(params),
isCo));
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2df73d9e4..c0484e52b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1112,7 +1112,7 @@ bool Smt2::pushSygusDatatypeDef(
std::vector<std::vector<std::string>>& unresolved_gterm_sym)
{
sorts.push_back(t);
- datatypes.push_back(Datatype(getExprManager(), dname));
+ datatypes.push_back(Datatype(d_solver->getExprManager(), dname));
ops.push_back(std::vector<ParseOp>());
cnames.push_back(std::vector<std::string>());
cargs.push_back(std::vector<std::vector<api::Sort>>());
@@ -1573,7 +1573,7 @@ void Smt2::addSygusConstructorVariables(Datatype& dt,
InputLanguage Smt2::getLanguage() const
{
- return getExprManager()->getOptions().getInputLanguage();
+ return d_solver->getExprManager()->getOptions().getInputLanguage();
}
void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
@@ -1746,7 +1746,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
}
}
// Second phase: apply the arguments to the parse op
- ExprManager* em = getExprManager();
+ const Options& opts = d_solver->getExprManager()->getOptions();
// handle special cases
if (p.d_kind == api::STORE_ALL && !p.d_type.isNull())
{
@@ -1842,8 +1842,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
else if (isBuiltinOperator)
{
Trace("ajr-temp") << "mkTerm builtin operator" << std::endl;
- if (!em->getOptions().getUfHo()
- && (kind == api::EQUAL || kind == api::DISTINCT))
+ if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
{
// need --uf-ho if these operators are applied over function args
for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
@@ -1884,7 +1883,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
unsigned arity = argt.getFunctionArity();
if (args.size() - 1 < arity)
{
- if (!em->getOptions().getUfHo())
+ if (!opts.getUfHo())
{
parseError("Cannot partially apply functions unless --uf-ho is set.");
}
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index a21cc6785..51b852eac 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -69,20 +69,19 @@ Tptp::~Tptp() {
}
void Tptp::addTheory(Theory theory) {
- ExprManager * em = getExprManager();
switch(theory) {
case THEORY_CORE:
//TPTP (CNF and FOF) is unsorted so we define this common type
{
std::string d_unsorted_name = "$$unsorted";
- d_unsorted = api::Sort(em->mkSort(d_unsorted_name));
+ d_unsorted = d_solver->mkUninterpretedSort(d_unsorted_name);
preemptCommand(
new DeclareTypeCommand(d_unsorted_name, 0, d_unsorted.getType()));
}
// propositionnal
- defineType("Bool", em->booleanType());
- defineVar("$true", em->mkConst(true));
- defineVar("$false", em->mkConst(false));
+ defineType("Bool", d_solver->getBooleanSort());
+ defineVar("$true", d_solver->mkTrue());
+ defineVar("$false", d_solver->mkFalse());
addOperator(api::AND);
addOperator(api::EQUAL);
addOperator(api::IMPLIES);
@@ -312,12 +311,11 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
isBuiltinKind = true;
}
assert(kind != api::NULL_EXPR);
- ExprManager* em = getExprManager();
+ const Options& opts = d_solver->getExprManager()->getOptions();
// Second phase: apply parse op to the arguments
if (isBuiltinKind)
{
- if (!em->getOptions().getUfHo()
- && (kind == api::EQUAL || kind == api::DISTINCT))
+ if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
{
// need --uf-ho if these operators are applied over function args
for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
@@ -352,7 +350,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
unsigned arity = argt.getFunctionArity();
if (args.size() - 1 < arity)
{
- if (!em->getOptions().getUfHo())
+ if (!opts.getUfHo())
{
parseError("Cannot partially apply functions unless --uf-ho is set.");
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback