diff options
Diffstat (limited to 'src/parser/parser.h')
| -rw-r--r-- | src/parser/parser.h | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 8add1c698..4b04c77b7 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -303,9 +303,10 @@ public: virtual api::Term getExpressionForName(const std::string& name); /** - * Returns the expression that name should be interpreted as, based on the current binding. + * Returns the expression that name should be interpreted as, based on the + * current binding. * - * This is the same as above but where the name has been type cast to t. + * This is the same as above but where the name has been type cast to t. */ virtual api::Term getExpressionForNameAndType(const std::string& name, api::Sort t); @@ -331,9 +332,9 @@ public: * This is a generalization of ExprManager::operatorToKind that also * handles variables whose types are "function-like", i.e. where * checkFunctionLike(fun) returns true. - * + * * For examples of the latter, this function returns - * APPLY_UF if fun has function type, + * APPLY_UF if fun has function type, * APPLY_CONSTRUCTOR if fun has constructor type. */ api::Kind getKindForFunction(api::Term fun); @@ -379,7 +380,7 @@ public: /** * Checks whether the given expression is function-like, i.e. - * it expects arguments. This is checked by looking at the type + * it expects arguments. This is checked by looking at the type * of fun. Examples of function types are function, constructor, * selector, tester. * @param fun the expression to check @@ -443,11 +444,12 @@ public: std::vector<api::Term> bindBoundVars(const std::vector<std::string> names, const api::Sort& type); - /** Create a new variable definition (e.g., from a let binding). + /** Create a new variable definition (e.g., from a let binding). * levelZero is set if the binding must be done at level 0. * If a symbol with name already exists, * then if doOverload is true, we create overloaded operators. - * else if doOverload is false, the existing expression is shadowed by the new expression. + * else if doOverload is false, the existing expression is shadowed by the + * new expression. */ void defineVar(const std::string& name, const api::Term& val, @@ -648,9 +650,10 @@ public: /** Is the symbol bound to a boolean variable? */ bool isBoolean(const std::string& name); - /** Is fun a function (or function-like thing)? - * Currently this means its type is either a function, constructor, tester, or selector. - */ + /** Is fun a function (or function-like thing)? + * Currently this means its type is either a function, constructor, tester, or + * selector. + */ bool isFunctionLike(api::Term fun); /** Is the symbol bound to a predicate? */ |