Add i128 and u128 Support for Integer ASTs

z3/src/ast/int.rs

@@ -85,6 +85,62 @@ impl Int {
         }
     }
 
+    pub fn from_i128(ctx: &Context, v: i128) -> Int {
+        let int_sort = Sort::int(ctx);
+        let s = v.to_string();
+        let c_str = CString::new(s).unwrap();
+        unsafe {
+            Self::wrap(
+                ctx,
+                Z3_mk_numeral(ctx.z3_ctx.0, c_str.as_ptr(), int_sort.z3_sort),
+            )
+        }
+    }
+
+    pub fn from_u128(ctx: &Context, v: u128) -> Int {
+        let int_sort = Sort::int(ctx);
+        let s = v.to_string();
+        let c_str = CString::new(s).unwrap();
+        unsafe {
+            Self::wrap(
+                ctx,
+                Z3_mk_numeral(ctx.z3_ctx.0, c_str.as_ptr(), int_sort.z3_sort),
+            )
+        }
+    }
+
+    pub fn as_i128(&self) -> Option<i128> {
+        if !unsafe { Z3_is_numeral_ast(self.get_ctx().z3_ctx.0, self.get_z3_ast()) } {
+            return None;
+        }
+
+        let c_str = unsafe {
+            std::ffi::CStr::from_ptr(Z3_get_numeral_string(
+                self.get_ctx().z3_ctx.0,
+                self.get_z3_ast(),
+            ))
+        };
+
+        let s = c_str.to_string_lossy();
+        s.parse::<i128>().ok()
+    }
+
+    pub fn as_u128(&self) -> Option<u128> {
+        if !unsafe { Z3_is_numeral_ast(self.get_ctx().z3_ctx.0, self.get_z3_ast()) } {
+            return None;
+        }
+
+        let c_str = unsafe {
+            std::ffi::CStr::from_ptr(Z3_get_numeral_string(
+                self.get_ctx().z3_ctx.0,
+                self.get_z3_ast(),
+            ))
+        };
+
+        let s = c_str.to_string_lossy();
+        s.parse::<u128>().ok()
+    }
+
     pub fn from_real(ast: &Real) -> Int {
         unsafe { Self::wrap(&ast.ctx, Z3_mk_real2int(ast.ctx.z3_ctx.0, ast.z3_ast)) }
     }

z3/tests/lib.rs

@@ -1988,6 +1988,35 @@ fn test_model_iter() {
     );
 }
 
+#[test]
+fn test_int_i128_u128() {
+    let cfg = Config::new();
+    let ctx = Context::new(&cfg);
+
+    let cases_i128: [i128; 4] = [0, 42, -1234567890123456789, i128::MAX];
+    let cases_u128: [u128; 3] = [0, 42, u128::MAX];
+
+    // Check i128
+    for &val in &cases_i128 {
+        let int_ast = Int::from_i128(&ctx, val);
+        let back = int_ast.as_i128().unwrap();
+        assert_eq!(back, val, "i128 failed for {}", val);
+    }
+
+    // Check u128
+    for &val in &cases_u128 {
+        let int_ast = Int::from_u128(&ctx, val);
+        let back = int_ast.as_u128().unwrap();
+        assert_eq!(back, val, "u128 failed for {}", val);
+    }
+
+    let val: i128 = 12345;
+    let int_i = Int::from_i128(&ctx, val);
+    let int_u = Int::from_u128(&ctx, val as u128);
+    // Both should print the same SMT-LIB numeral string
+    assert_eq!(int_i.to_string(), int_u.to_string());
+}
+
 #[test]
 fn test_round_towards_nearest_away() {
     let cfg = Config::new();