1 files changed, 8 insertions, 12 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 6427b32d5..954bca314 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -333,19 +333,15 @@ class Smt2 : public Parser
     return d_lastNamedTerm;
   }
 
-  bool 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 mkAbstractValue(const std::string& name) {
-    assert(isAbstractValue(name));
-    return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1))));
-  }
+  /** Does name denote an abstract value? (of the form '@n' for numeral n). */
+  bool isAbstractValue(const std::string& name);
 
-  void mkSygusVar(const std::string& name,
-                  const Type& type,
-                  bool isPrimed = false);
+  /** Make abstract value
+   *
+   * Abstract values are used for processing get-value calls. The argument
+   * name should be such that isAbstractValue(name) is true.
+   */
+  Expr mkAbstractValue(const std::string& name);
 
   void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );