diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
commit | ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (patch) | |
tree | 4ff6643e38469ceb84cd6791c5cbc295f625a735 /src/parser/parser.h | |
parent | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (diff) |
declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 64 |
1 files changed, 40 insertions, 24 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 0faf9bebf..1c492c843 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -186,26 +186,21 @@ public: bool strictModeEnabled() { return d_strictMode; } - /** Get the name of the input file. */ -/* - inline const std::string getFilename() { - return d_filename; - } -*/ - /** - * Sets the logic for the current benchmark. Declares any logic symbols. + * Returns a variable, given a name. * - * @param name the name of the logic (e.g., QF_UF, AUFLIA) + * @param name the name of the variable + * @return the variable expression */ -// void setLogic(const std::string& name); + Expr getVariable(const std::string& name); /** - * Returns a variable, given a name and a type. + * Returns a function, given a name. + * * @param var_name the name of the variable * @return the variable expression */ - Expr getVariable(const std::string& var_name); + Expr getFunction(const std::string& name); /** * Returns a sort, given a name. @@ -213,7 +208,7 @@ public: Type getSort(const std::string& sort_name); /** - * Returns a sort, given a name and args. + * Returns a (parameterized) sort, given a name and args. */ Type getSort(const std::string& sort_name, const std::vector<Type>& params); @@ -240,7 +235,8 @@ public: /** * Checks whether the given name is bound to a function. * @param name the name to check - * @throws ParserException if checks are enabled and name is not bound to a function + * @throws ParserException if checks are enabled and name is not + * bound to a function */ void checkFunction(const std::string& name) throw (ParserException); @@ -248,23 +244,26 @@ public: * Check that <code>kind</code> can accept <code>numArgs</code> arguments. * @param kind the built-in operator to check * @param numArgs the number of actual arguments - * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be - * applied to <code>numArgs</code> arguments. + * @throws ParserException if checks are enabled and the operator + * <code>kind</code> cannot be applied to <code>numArgs</code> + * arguments. */ void checkArity(Kind kind, unsigned int numArgs) throw (ParserException); - /** Check that <code>kind</code> is a legal operator in the current logic and - * that it can accept <code>numArgs</code> arguments. + /** + * Check that <code>kind</code> is a legal operator in the current + * logic and that it can accept <code>numArgs</code> arguments. * * @param kind the built-in operator to check * @param numArgs the number of actual arguments - * @throws ParserException if the parser mode is strict and the operator <code>kind</kind> - * has not been enabled + * @throws ParserException if the parser mode is strict and the + * operator <code>kind</kind> has not been enabled */ void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException); /** * Returns the type for the variable with the given name. + * * @param var_name the symbol to lookup * @param type the (namespace) type of the symbol */ @@ -274,27 +273,41 @@ public: Expr mkVar(const std::string& name, const Type& type); /** - * Create a set of new CVC4 variable expressions of the given - * type. + * Create a set of new CVC4 variable expressions of the given type. */ const std::vector<Expr> mkVars(const std::vector<std::string> names, const Type& type); + /** Create a new CVC4 function expression of the given type. */ + Expr mkFunction(const std::string& name, const Type& type); + /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); + /** Create a new function definition (e.g., from a define-fun). */ + void defineFunction(const std::string& name, const Expr& val); + /** Create a new type definition. */ void defineType(const std::string& name, const Type& type); + /** Create a new (parameterized) type definition. */ + void defineType(const std::string& name, + const std::vector<Type>& params, const Type& type); + /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */ void defineParameterizedType(const std::string& name, const std::vector<Type>& params, const Type& type); /** - * Creates a new sort with the given name and arity. + * Creates a new sort with the given name. + */ + Type mkSort(const std::string& name); + + /** + * Creates a new sort constructor with the given name and arity. */ - Type mkSort(const std::string& name, size_t arity = 0); + Type mkSortConstructor(const std::string& name, size_t arity); /** * Creates new sorts with the given names (all of arity 0). @@ -314,6 +327,9 @@ public: /** Is the symbol bound to a function? */ bool isFunction(const std::string& name); + /** Is the symbol bound to a defined function? */ + bool isDefinedFunction(const std::string& name); + /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); |