diff options
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 20 |
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 ); |