summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r--src/parser/smt2/smt2.cpp17
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback