summaryrefslogtreecommitdiff
path: root/src/parser/parser.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r--src/parser/parser.h27
1 files changed, 23 insertions, 4 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 28a033eb9..42badf4c5 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -526,12 +526,31 @@ public:
void defineVar(const std::string& name, const Expr& val,
bool levelZero = false, bool doOverload = false);
- /** Create a new type definition. */
- void defineType(const std::string& name, const Type& type);
+ /**
+ * Create a new type definition.
+ *
+ * @param name The name of the type
+ * @param type The type that should be associated with the name
+ * @param levelZero If true, the type definition is considered global and
+ * cannot be removed by poppoing the user context
+ */
+ void defineType(const std::string& name,
+ const Type& type,
+ bool levelZero = false);
- /** Create a new (parameterized) type definition. */
+ /**
+ * Create a new (parameterized) type definition.
+ *
+ * @param name The name of the type
+ * @param params The type parameters
+ * @param type The type that should be associated with the name
+ * @param levelZero If true, the type definition is considered global and
+ * cannot be removed by poppoing the user context
+ */
void defineType(const std::string& name,
- const std::vector<Type>& params, const Type& type);
+ const std::vector<Type>& params,
+ const Type& type,
+ bool levelZero = false);
/** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
void defineParameterizedType(const std::string& name,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback