diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
commit | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (patch) | |
tree | 8db12e260b24978bbbed3363846f6daf7c0da04f /src/expr/expr_manager_template.h | |
parent | 5e2f381b26d683691d9a040589536dc39c5831e0 (diff) |
parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 8e02c8ca4..316a9b7b1 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -224,11 +224,11 @@ public: /** Make the type of arrays with the given parameterization */ ArrayType mkArrayType(Type indexType, Type constituentType) const; - /** Make a new sort with the given name. */ - SortType mkSort(const std::string& name) const; + /** Make a new sort with the given name and arity. */ + SortType mkSort(const std::string& name, size_t arity = 0) const; /** Get the type of an expression */ - Type getType(const Expr& e, bool check = false) + Type getType(const Expr& e, bool check = false) throw (TypeCheckingException); // variables are special, because duplicates are permitted |