diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e1ce29b65..203be81b9 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -325,16 +325,6 @@ bool Smt2::logicIsSet() { return d_logicSet; } -api::Term Smt2::getExpressionForNameAndType(const std::string& name, - api::Sort t) -{ - if (isAbstractValue(name)) - { - return mkAbstractValue(name); - } - return Parser::getExpressionForNameAndType(name, t); -} - bool Smt2::getTesterName(api::Term cons, std::string& name) { if ((v2_6() || sygus()) && strictModeEnabled()) @@ -832,13 +822,6 @@ bool Smt2::isAbstractValue(const std::string& name) && name.find_first_not_of("0123456789", 1) == std::string::npos; } -api::Term Smt2::mkAbstractValue(const std::string& name) -{ - Assert(isAbstractValue(name)); - // remove the '@' - return d_solver->mkAbstractValue(name.substr(1)); -} - void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) { Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type |