feat: Add Sort::type_variable

z3-sys/src/lib.rs

@@ -3801,6 +3801,13 @@ unsafe extern "C" {
         value: Z3_ast,
     ) -> Option<Z3_ast>;
 
+    /// Create a type variable.
+    ///
+    /// Functions using type variables can be applied to instantiations that match the signature
+    /// of the function. Assertions using type variables correspond to assertions over all possible
+    /// instantiations.
+    pub fn Z3_mk_type_variable(c: Z3_context, s: Z3_symbol) -> Option<Z3_sort>;
+
     /// Return arity of relation.
     ///
     /// # Preconditions:

z3/Cargo.toml

@@ -28,6 +28,7 @@ static-link-z3 = ["z3-sys/bundled", "z3-sys/deprecated-static-link-z3"]
 # By default we use features present in 4.8.13 and up, but these features
 # allow for turning off these bindings.
 # Once ubuntu stops distributing 4.8.12, we can remove this for convenience.
+z3_4_12_13 = ["z3_4_8_15"]
 z3_4_8_15 = ["z3_4_8_14"]
 z3_4_8_14 = ["z3_4_8_13"]
 z3_4_8_13 = []

z3/src/sort.rs

@@ -32,6 +32,38 @@ impl Sort {
         }
     }
 
+    /// Creates a type-variable `Sort` from anything that can convert into a `Symbol`.
+    ///
+    /// # Examples
+    ///
+    /// ```
+    /// # use z3::{Sort, Symbol};
+    ///
+    /// // Accepts &str via Into<Symbol>
+    /// let t1 = Sort::type_variable("T");
+    /// // Accepts Symbol explicitly
+    /// let t2 = Sort::type_variable(Symbol::from("T"));
+    ///
+    /// // Same name → same type variable
+    /// assert_eq!(t1, t2);
+    ///
+    /// // Different names → different type variables
+    /// let u = Sort::type_variable("U");
+    /// assert_ne!(t1, u);
+    /// ```
+    #[cfg(feature = "z3_4_12_13")]
+    pub fn type_variable<T: Into<Symbol>>(name: T) -> Sort {
+        let ctx = &Context::thread_local();
+        let name = name.into();
+
+        unsafe {
+            Self::wrap(
+                ctx,
+                Z3_mk_type_variable(ctx.z3_ctx.0, name.as_z3_symbol()).unwrap(),
+            )
+        }
+    }
+
     pub fn bool() -> Sort {
         unsafe {
             let ctx = &Context::thread_local();