Minor cleaning of smt2 parser (#3823)

[cvc5.git] / src / parser / smt2 / smt2.cpp

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 88d8b527b8e9c8a779a4969c133b00ad0565169b..8c2b50b042723e9f71a73787b43e4f948b0ff989 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -934,6 +934,19 @@ void Smt2::includeFile(const std::string& filename) {
   }
 }
 
+bool Smt2::isAbstractValue(const std::string& name)
+{
+  return name.length() >= 2 && name[0] == '@' && name[1] != '0'
+         && name.find_first_not_of("0123456789", 1) == std::string::npos;
+}
+
+Expr Smt2::mkAbstractValue(const std::string& name)
+{
+  assert(isAbstractValue(name));
+  // remove the '@'
+  return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1))));
+}
+
 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
   if( type.isInteger() ){
     ops.push_back(getExprManager()->mkConst(Rational(0)));