diff options
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 8 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 11 |
2 files changed, 9 insertions, 10 deletions
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."); } |