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/expr/expr_manager_template.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/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 316a9b7b1..92d039bd3 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -173,7 +173,8 @@ public: template <class T> Expr mkConst(const T&); - /** Create an Expr by applying an associative operator to the children. + /** + * Create an Expr by applying an associative operator to the children. * If <code>children.size()</code> is greater than the max arity for * <code>kind</code>, then the expression will be broken up into * suitably-sized chunks, taking advantage of the associativity of @@ -224,8 +225,16 @@ 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 and arity. */ - SortType mkSort(const std::string& name, size_t arity = 0) const; + /** Make a new sort with the given name. */ + SortType mkSort(const std::string& name) const; + + /** Make a new sort from a constructor */ + SortType mkSort(SortConstructorType constructor, + const std::vector<TypeNode>& children) const; + + /** Make a sort constructor from a name and arity */ + SortConstructorType mkSortConstructor(const std::string& name, + size_t arity) const; /** Get the type of an expression */ Type getType(const Expr& e, bool check = false) |