diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f66bd1f76..395e42d60 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -420,6 +420,12 @@ namespace z3 { sort uninterpreted_sort(char const* name); sort uninterpreted_sort(symbol const& name); + /** + \brief create a type variable sort with the name given by the string or symbol. + */ + sort type_variable(char const* name); + sort type_variable(symbol const& name); + func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range); func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range); func_decl function(symbol const& name, sort_vector const& domain, sort const& range); @@ -792,6 +798,10 @@ namespace z3 { \brief Return true if this sort is a Floating point sort. */ bool is_fpa() const { return sort_kind() == Z3_FLOATING_POINT_SORT; } + /** + \brief Return true if this sort is a type variable sort. + */ + bool is_type_var() const { return sort_kind() == Z3_TYPE_VAR; } /** \brief Return the size of this Bit-vector sort. @@ -3869,6 +3879,13 @@ namespace z3 { inline sort context::uninterpreted_sort(symbol const& name) { return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name)); } + inline sort context::type_variable(char const* name) { + Z3_symbol _name = Z3_mk_string_symbol(*this, name); + return to_sort(*this, Z3_mk_type_variable(*this, _name)); + } + inline sort context::type_variable(symbol const& name) { + return to_sort(*this, Z3_mk_type_variable(*this, name)); + } inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) { array args(arity); diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index c309f4027..0d72590d5 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -113,6 +113,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE Symbol.cs Tactic.cs TupleSort.cs + TypeVarSort.cs UninterpretedSort.cs UserPropagator.cs Version.cs diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 52c9af8f6..adb5da91d 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -227,6 +227,26 @@ namespace Microsoft.Z3 return MkUninterpretedSort(sym); } + /// + /// Create a new type variable sort. + /// + public TypeVarSort MkTypeVariable(Symbol s) + { + Debug.Assert(s != null); + + CheckContextMatch(s); + return new TypeVarSort(this, s); + } + + /// + /// Create a new type variable sort. + /// + public TypeVarSort MkTypeVariable(string str) + { + using var sym = MkSymbol(str); + return MkTypeVariable(sym); + } + /// /// Create a new integer sort. /// diff --git a/src/api/dotnet/TypeVarSort.cs b/src/api/dotnet/TypeVarSort.cs new file mode 100644 index 000000000..21fa4d4c1 --- /dev/null +++ b/src/api/dotnet/TypeVarSort.cs @@ -0,0 +1,44 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + TypeVarSort.cs + +Abstract: + + Z3 Managed API: Type Variable Sorts + +Author: + + Christoph Wintersteiger (cwinter) 2012-11-23 + +Notes: + +--*/ + +using System; +using System.Diagnostics; + +namespace Microsoft.Z3 +{ + /// + /// Type variable sorts for use in polymorphic functions and datatypes. + /// + public class TypeVarSort : Sort + { + #region Internal + internal TypeVarSort(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Debug.Assert(ctx != null); + } + internal TypeVarSort(Context ctx, Symbol s) + : base(ctx, Native.Z3_mk_type_variable(ctx.nCtx, s.NativeObject)) + { + Debug.Assert(ctx != null); + Debug.Assert(s != null); + } + #endregion + } +} diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 71f156557..4287c9975 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -743,6 +743,7 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel { ///////////// const Sort = { declare: (name: string) => new SortImpl(Z3.mk_uninterpreted_sort(contextPtr, _toSymbol(name))), + typeVariable: (name: string) => new SortImpl(Z3.mk_type_variable(contextPtr, _toSymbol(name))), }; const Function = { declare: [], RangeSort extends Sort>( diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index db28c8d16..7c61f54a6 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -1988,6 +1988,7 @@ export interface Statistics extends Iterable { declare(name: string): Sort; + typeVariable(name: string): Sort; } export interface Sort extends Ast {