From: Andrew Reynolds Date: Mon, 9 Mar 2020 19:33:01 +0000 (-0500) Subject: Clean up more uses of ExprManager in parsers (#3932) X-Git-Tag: cvc5-1.0.0~3546 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e337310b9f5df6b7ecd0f2e351b9c0e4265e8e69;p=cvc5.git Clean up more uses of ExprManager in parsers (#3932) Towards parser migration. Beyond Datatypes, there are still a handful of calls to the ExprManager in the parsers. This eliminates a few missing cases from TPTP and also inlines the access of ExprManager in the places its used. --- 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& 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(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 Parser::mkMutualDatatypeTypes( try { std::set tset = api::sortSetToTypes(d_unresolved); std::vector dtypes = - getExprManager()->mkMutualDatatypeTypes(datatypes, tset, flags); + d_solver->getExprManager()->mkMutualDatatypeTypes( + datatypes, tset, flags); std::vector 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 ExprManager. */ - 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& 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>& 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()); cnames.push_back(std::vector()); cargs.push_back(std::vector>()); @@ -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& 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& 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::iterator i = args.begin(); i != args.end(); @@ -1884,7 +1883,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& 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& 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::iterator i = args.begin(); i != args.end(); @@ -352,7 +350,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector& 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."); }