X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fparser%2Fsmt2%2Fsmt2.cpp;h=8c2b50b042723e9f71a73787b43e4f948b0ff989;hb=b28ff31b6713791f27b4860f439aaa3f63aab9d7;hp=88d8b527b8e9c8a779a4969c133b00ad0565169b;hpb=808bb1bd855799535a1b690865dc873793a37f7f;p=cvc5.git

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 88d8b527b..8c2b50b04 100644
--- 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)));