From 8e444d8175736450b19f7349a19f57cd48f643ac Mon Sep 17 00:00:00 2001 From: mehrad31415 Date: Fri, 25 Jul 2025 01:07:25 -0400 Subject: [PATCH 1/5] all changes --- all_changes.patch | 390 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 390 insertions(+) create mode 100644 all_changes.patch diff --git a/all_changes.patch b/all_changes.patch new file mode 100644 index 00000000..7129ee6d --- /dev/null +++ b/all_changes.patch @@ -0,0 +1,390 @@ +diff --git a/z3-sys/src/lib.rs b/z3-sys/src/lib.rs +index 608ba12..206a75e 100644 +--- a/z3-sys/src/lib.rs ++++ b/z3-sys/src/lib.rs +@@ -6473,18 +6473,6 @@ unsafe extern "C" { + /// - [`Z3_fixedpoint_from_string`] + /// - [`Z3_fixedpoint_to_string`] + pub fn Z3_fixedpoint_from_file(c: Z3_context, f: Z3_fixedpoint, s: Z3_string) -> Z3_ast_vector; +- +- /// String less-than lexicographic comparison operation. +- /// Return a new AST node `Bool`. +- pub fn Z3_mk_str_lt(c: Z3_context, lhs: Z3_ast, rhs: Z3_ast) -> Z3_ast; +- +- /// String less-than-or-equal lexicographic comparison operation. +- /// Return a new AST node `Bool`. +- pub fn Z3_mk_str_le(c: Z3_context, lhs: Z3_ast, rhs: Z3_ast) -> Z3_ast; +- +- /// Cardinality of a set. +- /// Return a new AST node `Int` representing the cardinality of the given set. +- pub fn Z3_mk_set_card(c: Z3_context, set_ast: Z3_ast) -> Z3_ast; + } + /// The following utilities allows adding user-defined domains. + pub type Z3_fixedpoint_reduce_assign_callback_fptr = ::std::option::Option< +diff --git a/z3/src/ast.rs b/z3/src/ast.rs +index 88f05d7..196cad3 100644 +--- a/z3/src/ast.rs ++++ b/z3/src/ast.rs +@@ -1,14 +1,12 @@ + //! Abstract syntax tree (AST). + + use log::debug; +-use num::pow::Pow; + use std::borrow::Borrow; + use std::cmp::{Eq, PartialEq}; + use std::convert::{TryFrom, TryInto}; + use std::ffi::{CStr, CString}; + use std::fmt; + use std::hash::{Hash, Hasher}; +-use std::ops::{Add, Div, Mul, Sub}; + + pub use z3_sys::AstKind; + use z3_sys::*; +@@ -858,62 +856,6 @@ impl<'ctx> Int<'ctx> { + } + } + +- pub fn from_i128(ctx: &'ctx Context, v: i128) -> Int<'ctx> { +- 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, c_str.as_ptr(), int_sort.z3_sort), +- ) +- } +- } +- +- pub fn from_u128(ctx: &'ctx Context, v: u128) -> Int<'ctx> { +- 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, c_str.as_ptr(), int_sort.z3_sort), +- ) +- } +- } +- +- pub fn as_i128(&self) -> Option { +- if !unsafe { Z3_is_numeral_ast(self.get_ctx().z3_ctx, self.get_z3_ast()) } { +- return None; +- } +- +- let c_str = unsafe { +- std::ffi::CStr::from_ptr(Z3_get_numeral_string( +- self.get_ctx().z3_ctx, +- self.get_z3_ast(), +- )) +- }; +- +- let s = c_str.to_string_lossy(); +- s.parse::().ok() +- } +- +- pub fn as_u128(&self) -> Option { +- if !unsafe { Z3_is_numeral_ast(self.get_ctx().z3_ctx, self.get_z3_ast()) } { +- return None; +- } +- +- let c_str = unsafe { +- std::ffi::CStr::from_ptr(Z3_get_numeral_string( +- self.get_ctx().z3_ctx, +- self.get_z3_ast(), +- )) +- }; +- +- let s = c_str.to_string_lossy(); +- s.parse::().ok() +- } +- + pub fn from_real(ast: &Real<'ctx>) -> Int<'ctx> { + unsafe { Self::wrap(ast.ctx, Z3_mk_real2int(ast.ctx.z3_ctx, ast.z3_ast)) } + } +@@ -979,112 +921,21 @@ impl<'ctx> Int<'ctx> { + gt(Z3_mk_gt, Bool<'ctx>); + ge(Z3_mk_ge, Bool<'ctx>); + } ++ // Z3 does support mixing ints and reals in add(), sub(), mul(), div(), and power() ++ // (but not rem(), modulo(), lt(), le(), gt(), or ge()). ++ // TODO: we could consider expressing this by having a Numeric trait with these methods. ++ // Int and Real would have the Numeric trait, but not the other Asts. ++ // For example: ++ // fn add(&self, other: &impl Numeric<'ctx>) -> Dynamic<'ctx> { ... } ++ // Note the return type would have to be Dynamic I think (?), as the exact result type ++ // depends on the particular types of the inputs. ++ // Alternately, we could just have ++ // Int::add_real(&self, other: &Real<'ctx>) -> Real<'ctx> ++ // and ++ // Real::add_int(&self, other: &Int<'ctx>) -> Real<'ctx> ++ // This might be cleaner because we know exactly what the output type will be for these methods. + } + +-// Z3 does support mixing ints and reals in add(), sub(), mul(), div(), and power() +-fn add_int_real<'ctx>(i: &Int<'ctx>, r: &Real<'ctx>) -> Real<'ctx> { +- unsafe { +- let args = [i.z3_ast, r.z3_ast]; +- Real::wrap(i.ctx, Z3_mk_add(i.ctx.z3_ctx, 2, args.as_ptr())) +- } +-} +-fn add_real_int<'ctx>(r: &Real<'ctx>, i: &Int<'ctx>) -> Real<'ctx> { +- unsafe { +- let args = [r.z3_ast, i.z3_ast]; +- Real::wrap(r.ctx, Z3_mk_add(r.ctx.z3_ctx, 2, args.as_ptr())) +- } +-} +- +-fn sub_int_real<'ctx>(i: &Int<'ctx>, r: &Real<'ctx>) -> Real<'ctx> { +- unsafe { +- let args = [i.z3_ast, r.z3_ast]; +- Real::wrap(i.ctx, Z3_mk_sub(i.ctx.z3_ctx, 2, args.as_ptr())) +- } +-} +-fn sub_real_int<'ctx>(r: &Real<'ctx>, i: &Int<'ctx>) -> Real<'ctx> { +- unsafe { +- let args = [r.z3_ast, i.z3_ast]; +- Real::wrap(r.ctx, Z3_mk_sub(r.ctx.z3_ctx, 2, args.as_ptr())) +- } +-} +- +-fn mul_int_real<'ctx>(i: &Int<'ctx>, r: &Real<'ctx>) -> Real<'ctx> { +- unsafe { +- let args = [i.z3_ast, r.z3_ast]; +- Real::wrap(i.ctx, Z3_mk_mul(i.ctx.z3_ctx, 2, args.as_ptr())) +- } +-} +-fn mul_real_int<'ctx>(r: &Real<'ctx>, i: &Int<'ctx>) -> Real<'ctx> { +- unsafe { +- let args = [r.z3_ast, i.z3_ast]; +- Real::wrap(r.ctx, Z3_mk_mul(r.ctx.z3_ctx, 2, args.as_ptr())) +- } +-} +- +-fn div_int_real<'ctx>(i: &Int<'ctx>, r: &Real<'ctx>) -> Real<'ctx> { +- unsafe { Real::wrap(i.ctx, Z3_mk_div(i.ctx.z3_ctx, i.z3_ast, r.z3_ast)) } +-} +-fn div_real_int<'ctx>(r: &Real<'ctx>, i: &Int<'ctx>) -> Real<'ctx> { +- unsafe { Real::wrap(r.ctx, Z3_mk_div(r.ctx.z3_ctx, r.z3_ast, i.z3_ast)) } +-} +- +-fn pow_int_real<'ctx>(i: &Int<'ctx>, r: &Real<'ctx>) -> Real<'ctx> { +- unsafe { Real::wrap(i.ctx, Z3_mk_power(i.ctx.z3_ctx, i.z3_ast, r.z3_ast)) } +-} +-fn pow_real_int<'ctx>(r: &Real<'ctx>, i: &Int<'ctx>) -> Real<'ctx> { +- unsafe { Real::wrap(r.ctx, Z3_mk_power(r.ctx.z3_ctx, r.z3_ast, i.z3_ast)) } +-} +- +-// Generic macro to implement the four ownership combinations +-macro_rules! impl_mixed_binop { +- ($Trait:ident, $method:ident, $L:ident, $R:ident, $builder:ident) => { +- impl<'ctx> $Trait<&$R<'ctx>> for &$L<'ctx> { +- type Output = Real<'ctx>; +- fn $method(self, rhs: &$R<'ctx>) -> Real<'ctx> { +- $builder(self, rhs) +- } +- } +- impl<'ctx> $Trait<$R<'ctx>> for &$L<'ctx> { +- type Output = Real<'ctx>; +- fn $method(self, rhs: $R<'ctx>) -> Real<'ctx> { +- $builder(self, &rhs) +- } +- } +- impl<'ctx> $Trait<&$R<'ctx>> for $L<'ctx> { +- type Output = Real<'ctx>; +- fn $method(self, rhs: &$R<'ctx>) -> Real<'ctx> { +- $builder(&self, rhs) +- } +- } +- impl<'ctx> $Trait<$R<'ctx>> for $L<'ctx> { +- type Output = Real<'ctx>; +- fn $method(self, rhs: $R<'ctx>) -> Real<'ctx> { +- $builder(&self, &rhs) +- } +- } +- }; +-} +- +-// Add +-impl_mixed_binop!(Add, add, Int, Real, add_int_real); +-impl_mixed_binop!(Add, add, Real, Int, add_real_int); +- +-// Sub +-impl_mixed_binop!(Sub, sub, Int, Real, sub_int_real); +-impl_mixed_binop!(Sub, sub, Real, Int, sub_real_int); +- +-// Mul +-impl_mixed_binop!(Mul, mul, Int, Real, mul_int_real); +-impl_mixed_binop!(Mul, mul, Real, Int, mul_real_int); +- +-// Div +-impl_mixed_binop!(Div, div, Int, Real, div_int_real); +-impl_mixed_binop!(Div, div, Real, Int, div_real_int); +- +-// Pow +-impl_mixed_binop!(Pow, pow, Int, Real, pow_int_real); +-impl_mixed_binop!(Pow, pow, Real, Int, pow_real_int); +- + impl<'ctx> Real<'ctx> { + pub fn new_const>(ctx: &'ctx Context, name: S) -> Real<'ctx> { + let sort = Sort::real(ctx); +@@ -1262,16 +1113,6 @@ impl<'ctx> Float<'ctx> { + unsafe { Self::wrap(ctx, Z3_mk_fpa_round_toward_positive(ctx.z3_ctx)) } + } + +- // returns RoundingMode towards away from zero +- pub fn round_towards_nearest_away(ctx: &'ctx Context) -> Float<'ctx> { +- unsafe { Self::wrap(ctx, Z3_mk_fpa_round_nearest_ties_to_away(ctx.z3_ctx)) } +- } +- +- // returns RoundingMode towards nearest even +- pub fn round_towards_nearest_even(ctx: &'ctx Context) -> Float<'ctx> { +- unsafe { Self::wrap(ctx, Z3_mk_fpa_round_nearest_ties_to_even(ctx.z3_ctx)) } +- } +- + // Add two floats of the same size, rounding towards zero + pub fn add_towards_zero(&self, other: &Self) -> Float<'ctx> { + Self::round_towards_zero(self.ctx).add(self, other) +@@ -1297,22 +1138,6 @@ impl<'ctx> Float<'ctx> { + unsafe { BV::wrap(self.ctx, Z3_mk_fpa_to_ieee_bv(self.ctx.z3_ctx, self.z3_ast)) } + } + +- /// NaN for an arbitrary FP sort. +- pub fn nan(ctx: &'ctx Context, sort: &Sort<'ctx>) -> Float<'ctx> { +- debug_assert!(matches!(sort.kind(), SortKind::FloatingPoint)); +- unsafe { Self::wrap(ctx, Z3_mk_fpa_nan(ctx.z3_ctx, sort.z3_sort)) } +- } +- +- /// Convenience IEEE-754 single & double. +- pub fn nan32(ctx: &'ctx Context) -> Float<'ctx> { +- let s = Sort::float(ctx, 8, 24); +- Self::nan(ctx, &s) +- } +- pub fn nan64(ctx: &'ctx Context) -> Float<'ctx> { +- let s = Sort::float(ctx, 11, 53); +- Self::nan(ctx, &s) +- } +- + unop! { + unary_abs(Z3_mk_fpa_abs, Self); + unary_neg(Z3_mk_fpa_neg, Self); +@@ -1473,16 +1298,6 @@ impl<'ctx> String<'ctx> { + } + } + +- /// Greater than in lexicographic order (str.> s1 s2) +- pub fn str_gt(&self, other: &Self) -> Bool<'ctx> { +- other.str_lt(self) +- } +- +- /// Greater than or equal to in lexicographic order (str.>= s1 s2) +- pub fn str_ge(&self, other: &Self) -> Bool<'ctx> { +- other.str_le(self) +- } +- + varop! { + /// Appends the argument strings to `Self` + concat(Z3_mk_seq_concat, String<'ctx>); +@@ -1500,10 +1315,6 @@ impl<'ctx> String<'ctx> { + prefix(Z3_mk_seq_prefix, Bool<'ctx>); + /// Checks whether `Self` is a suffix of the argument + suffix(Z3_mk_seq_suffix, Bool<'ctx>); +- /// Checks whether `Self` is less than the argument in lexicographic order (str.< s1 s2) +- str_lt(Z3_mk_str_lt, Bool<'ctx>); +- /// Checks whether `Self` is less than or equal to the argument in lexicographic order (str.<= s1 s2) +- str_le(Z3_mk_str_le, Bool<'ctx>); + } + } + +@@ -2024,12 +1835,6 @@ impl<'ctx> Seq<'ctx> { + } + } + +- /// Create an empty sequence of the given sort. +- pub fn empty(ctx: &'ctx Context, eltype: &Sort<'ctx>) -> Self { +- let sort = Sort::seq(ctx, eltype); +- unsafe { Self::wrap(ctx, Z3_mk_seq_empty(ctx.z3_ctx, sort.z3_sort)) } +- } +- + /// Create a unit sequence of `a`. + pub fn unit>(ctx: &'ctx Context, a: &A) -> Self { + unsafe { Self::wrap(ctx, Z3_mk_seq_unit(ctx.z3_ctx, a.get_z3_ast())) } +@@ -2078,15 +1883,6 @@ impl<'ctx> Seq<'ctx> { + unsafe { Int::wrap(self.ctx, Z3_mk_seq_length(self.ctx.z3_ctx, self.z3_ast)) } + } + +- pub fn contains(&self, containee: &Self) -> Bool<'ctx> { +- unsafe { +- Bool::wrap( +- self.ctx, +- Z3_mk_seq_contains(self.ctx.z3_ctx, self.z3_ast, containee.z3_ast), +- ) +- } +- } +- + varop! { + /// Concatenate sequences. + concat(Z3_mk_seq_concat, Self); +diff --git a/z3/src/config.rs b/z3/src/config.rs +index 176b5dd..2c66e99 100644 +--- a/z3/src/config.rs ++++ b/z3/src/config.rs +@@ -39,12 +39,6 @@ impl Config { + /// + /// - [`Config::set_bool_param_value()`] + pub fn set_param_value(&mut self, k: &str, v: &str) { +- if k == "ctrl_c" { +- eprintln!( +- "WARNING: Parameter 'ctrl_c' is global-only; use `z3::set_global_param` instead." +- ); +- return; +- } + let ks = CString::new(k).unwrap(); + let vs = CString::new(v).unwrap(); + self.kvs.push((ks, vs)); +diff --git a/z3/src/probe.rs b/z3/src/probe.rs +index 9a25d60..b711f1a 100644 +--- a/z3/src/probe.rs ++++ b/z3/src/probe.rs +@@ -84,7 +84,7 @@ impl<'ctx> Probe<'ctx> { + /// by `self` is less than the value returned by `p`. + /// + /// NOTE: For probes, "true" is any value different from 0.0. +- pub fn lt(&self, p: &Probe) -> Probe<'ctx> { ++ pub fn lt(&self, p: Probe) -> Probe<'ctx> { + unsafe { + Self::wrap( + self.ctx, +diff --git a/z3/src/solver.rs b/z3/src/solver.rs +index 282cfa2..e24c83a 100644 +--- a/z3/src/solver.rs ++++ b/z3/src/solver.rs +@@ -39,6 +39,13 @@ impl<'ctx> Solver<'ctx> { + /// `solver2_unknown`, and `ignore_solver1` parameters of the combined + /// solver to change its behaviour. + /// ++ /// The function [`Solver::get_model()`] retrieves a model if the ++ /// assertions is satisfiable (i.e., the result is ++ /// `SatResult::Sat`) and [model construction is enabled]. ++ /// The function [`Solver::get_model()`] can also be used even ++ /// if the result is `SatResult::Unknown`, but the returned model ++ /// is not guaranteed to satisfy quantified assertions. ++ /// + /// [model construction is enabled]: crate::Config::set_model_generation + pub fn new(ctx: &'ctx Context) -> Solver<'ctx> { + unsafe { Self::wrap(ctx, Z3_mk_solver(ctx.z3_ctx)) } +@@ -296,13 +303,6 @@ impl<'ctx> Solver<'ctx> { + + /// Retrieve the model for the last [`Solver::check()`] + /// or [`Solver::check_assumptions()`]. +- /// +- /// The function [`Solver::get_model()`] retrieves a model if the +- /// assertions is satisfiable (i.e., the result is +- /// `SatResult::Sat`) and [model construction is enabled]. +- /// The function [`Solver::get_model()`] can also be used even +- /// if the result is `SatResult::Unknown`, but the returned model +- /// is not guaranteed to satisfy quantified assertions. + /// + /// The error handler is invoked if a model is not available because + /// the commands above were not invoked for the given solver, or if From afe7ba20a2c27f67fac8cf8b72b67d2e9d760912 Mon Sep 17 00:00:00 2001 From: mehrad31415 Date: Fri, 25 Jul 2025 01:07:55 -0400 Subject: [PATCH 2/5] d --- all_changes.patch | 390 ---------------------------------------------- 1 file changed, 390 deletions(-) delete mode 100644 all_changes.patch diff --git a/all_changes.patch b/all_changes.patch deleted file mode 100644 index 7129ee6d..00000000 --- a/all_changes.patch +++ /dev/null @@ -1,390 +0,0 @@ -diff --git a/z3-sys/src/lib.rs b/z3-sys/src/lib.rs -index 608ba12..206a75e 100644 ---- a/z3-sys/src/lib.rs -+++ b/z3-sys/src/lib.rs -@@ -6473,18 +6473,6 @@ unsafe extern "C" { - /// - [`Z3_fixedpoint_from_string`] - /// - [`Z3_fixedpoint_to_string`] - pub fn Z3_fixedpoint_from_file(c: Z3_context, f: Z3_fixedpoint, s: Z3_string) -> Z3_ast_vector; -- -- /// String less-than lexicographic comparison operation. -- /// Return a new AST node `Bool`. -- pub fn Z3_mk_str_lt(c: Z3_context, lhs: Z3_ast, rhs: Z3_ast) -> Z3_ast; -- -- /// String less-than-or-equal lexicographic comparison operation. -- /// Return a new AST node `Bool`. -- pub fn Z3_mk_str_le(c: Z3_context, lhs: Z3_ast, rhs: Z3_ast) -> Z3_ast; -- -- /// Cardinality of a set. -- /// Return a new AST node `Int` representing the cardinality of the given set. -- pub fn Z3_mk_set_card(c: Z3_context, set_ast: Z3_ast) -> Z3_ast; - } - /// The following utilities allows adding user-defined domains. - pub type Z3_fixedpoint_reduce_assign_callback_fptr = ::std::option::Option< -diff --git a/z3/src/ast.rs b/z3/src/ast.rs -index 88f05d7..196cad3 100644 ---- a/z3/src/ast.rs -+++ b/z3/src/ast.rs -@@ -1,14 +1,12 @@ - //! Abstract syntax tree (AST). - - use log::debug; --use num::pow::Pow; - use std::borrow::Borrow; - use std::cmp::{Eq, PartialEq}; - use std::convert::{TryFrom, TryInto}; - use std::ffi::{CStr, CString}; - use std::fmt; - use std::hash::{Hash, Hasher}; --use std::ops::{Add, Div, Mul, Sub}; - - pub use z3_sys::AstKind; - use z3_sys::*; -@@ -858,62 +856,6 @@ impl<'ctx> Int<'ctx> { - } - } - -- pub fn from_i128(ctx: &'ctx Context, v: i128) -> Int<'ctx> { -- 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, c_str.as_ptr(), int_sort.z3_sort), -- ) -- } -- } -- -- pub fn from_u128(ctx: &'ctx Context, v: u128) -> Int<'ctx> { -- 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, c_str.as_ptr(), int_sort.z3_sort), -- ) -- } -- } -- -- pub fn as_i128(&self) -> Option { -- if !unsafe { Z3_is_numeral_ast(self.get_ctx().z3_ctx, self.get_z3_ast()) } { -- return None; -- } -- -- let c_str = unsafe { -- std::ffi::CStr::from_ptr(Z3_get_numeral_string( -- self.get_ctx().z3_ctx, -- self.get_z3_ast(), -- )) -- }; -- -- let s = c_str.to_string_lossy(); -- s.parse::().ok() -- } -- -- pub fn as_u128(&self) -> Option { -- if !unsafe { Z3_is_numeral_ast(self.get_ctx().z3_ctx, self.get_z3_ast()) } { -- return None; -- } -- -- let c_str = unsafe { -- std::ffi::CStr::from_ptr(Z3_get_numeral_string( -- self.get_ctx().z3_ctx, -- self.get_z3_ast(), -- )) -- }; -- -- let s = c_str.to_string_lossy(); -- s.parse::().ok() -- } -- - pub fn from_real(ast: &Real<'ctx>) -> Int<'ctx> { - unsafe { Self::wrap(ast.ctx, Z3_mk_real2int(ast.ctx.z3_ctx, ast.z3_ast)) } - } -@@ -979,112 +921,21 @@ impl<'ctx> Int<'ctx> { - gt(Z3_mk_gt, Bool<'ctx>); - ge(Z3_mk_ge, Bool<'ctx>); - } -+ // Z3 does support mixing ints and reals in add(), sub(), mul(), div(), and power() -+ // (but not rem(), modulo(), lt(), le(), gt(), or ge()). -+ // TODO: we could consider expressing this by having a Numeric trait with these methods. -+ // Int and Real would have the Numeric trait, but not the other Asts. -+ // For example: -+ // fn add(&self, other: &impl Numeric<'ctx>) -> Dynamic<'ctx> { ... } -+ // Note the return type would have to be Dynamic I think (?), as the exact result type -+ // depends on the particular types of the inputs. -+ // Alternately, we could just have -+ // Int::add_real(&self, other: &Real<'ctx>) -> Real<'ctx> -+ // and -+ // Real::add_int(&self, other: &Int<'ctx>) -> Real<'ctx> -+ // This might be cleaner because we know exactly what the output type will be for these methods. - } - --// Z3 does support mixing ints and reals in add(), sub(), mul(), div(), and power() --fn add_int_real<'ctx>(i: &Int<'ctx>, r: &Real<'ctx>) -> Real<'ctx> { -- unsafe { -- let args = [i.z3_ast, r.z3_ast]; -- Real::wrap(i.ctx, Z3_mk_add(i.ctx.z3_ctx, 2, args.as_ptr())) -- } --} --fn add_real_int<'ctx>(r: &Real<'ctx>, i: &Int<'ctx>) -> Real<'ctx> { -- unsafe { -- let args = [r.z3_ast, i.z3_ast]; -- Real::wrap(r.ctx, Z3_mk_add(r.ctx.z3_ctx, 2, args.as_ptr())) -- } --} -- --fn sub_int_real<'ctx>(i: &Int<'ctx>, r: &Real<'ctx>) -> Real<'ctx> { -- unsafe { -- let args = [i.z3_ast, r.z3_ast]; -- Real::wrap(i.ctx, Z3_mk_sub(i.ctx.z3_ctx, 2, args.as_ptr())) -- } --} --fn sub_real_int<'ctx>(r: &Real<'ctx>, i: &Int<'ctx>) -> Real<'ctx> { -- unsafe { -- let args = [r.z3_ast, i.z3_ast]; -- Real::wrap(r.ctx, Z3_mk_sub(r.ctx.z3_ctx, 2, args.as_ptr())) -- } --} -- --fn mul_int_real<'ctx>(i: &Int<'ctx>, r: &Real<'ctx>) -> Real<'ctx> { -- unsafe { -- let args = [i.z3_ast, r.z3_ast]; -- Real::wrap(i.ctx, Z3_mk_mul(i.ctx.z3_ctx, 2, args.as_ptr())) -- } --} --fn mul_real_int<'ctx>(r: &Real<'ctx>, i: &Int<'ctx>) -> Real<'ctx> { -- unsafe { -- let args = [r.z3_ast, i.z3_ast]; -- Real::wrap(r.ctx, Z3_mk_mul(r.ctx.z3_ctx, 2, args.as_ptr())) -- } --} -- --fn div_int_real<'ctx>(i: &Int<'ctx>, r: &Real<'ctx>) -> Real<'ctx> { -- unsafe { Real::wrap(i.ctx, Z3_mk_div(i.ctx.z3_ctx, i.z3_ast, r.z3_ast)) } --} --fn div_real_int<'ctx>(r: &Real<'ctx>, i: &Int<'ctx>) -> Real<'ctx> { -- unsafe { Real::wrap(r.ctx, Z3_mk_div(r.ctx.z3_ctx, r.z3_ast, i.z3_ast)) } --} -- --fn pow_int_real<'ctx>(i: &Int<'ctx>, r: &Real<'ctx>) -> Real<'ctx> { -- unsafe { Real::wrap(i.ctx, Z3_mk_power(i.ctx.z3_ctx, i.z3_ast, r.z3_ast)) } --} --fn pow_real_int<'ctx>(r: &Real<'ctx>, i: &Int<'ctx>) -> Real<'ctx> { -- unsafe { Real::wrap(r.ctx, Z3_mk_power(r.ctx.z3_ctx, r.z3_ast, i.z3_ast)) } --} -- --// Generic macro to implement the four ownership combinations --macro_rules! impl_mixed_binop { -- ($Trait:ident, $method:ident, $L:ident, $R:ident, $builder:ident) => { -- impl<'ctx> $Trait<&$R<'ctx>> for &$L<'ctx> { -- type Output = Real<'ctx>; -- fn $method(self, rhs: &$R<'ctx>) -> Real<'ctx> { -- $builder(self, rhs) -- } -- } -- impl<'ctx> $Trait<$R<'ctx>> for &$L<'ctx> { -- type Output = Real<'ctx>; -- fn $method(self, rhs: $R<'ctx>) -> Real<'ctx> { -- $builder(self, &rhs) -- } -- } -- impl<'ctx> $Trait<&$R<'ctx>> for $L<'ctx> { -- type Output = Real<'ctx>; -- fn $method(self, rhs: &$R<'ctx>) -> Real<'ctx> { -- $builder(&self, rhs) -- } -- } -- impl<'ctx> $Trait<$R<'ctx>> for $L<'ctx> { -- type Output = Real<'ctx>; -- fn $method(self, rhs: $R<'ctx>) -> Real<'ctx> { -- $builder(&self, &rhs) -- } -- } -- }; --} -- --// Add --impl_mixed_binop!(Add, add, Int, Real, add_int_real); --impl_mixed_binop!(Add, add, Real, Int, add_real_int); -- --// Sub --impl_mixed_binop!(Sub, sub, Int, Real, sub_int_real); --impl_mixed_binop!(Sub, sub, Real, Int, sub_real_int); -- --// Mul --impl_mixed_binop!(Mul, mul, Int, Real, mul_int_real); --impl_mixed_binop!(Mul, mul, Real, Int, mul_real_int); -- --// Div --impl_mixed_binop!(Div, div, Int, Real, div_int_real); --impl_mixed_binop!(Div, div, Real, Int, div_real_int); -- --// Pow --impl_mixed_binop!(Pow, pow, Int, Real, pow_int_real); --impl_mixed_binop!(Pow, pow, Real, Int, pow_real_int); -- - impl<'ctx> Real<'ctx> { - pub fn new_const>(ctx: &'ctx Context, name: S) -> Real<'ctx> { - let sort = Sort::real(ctx); -@@ -1262,16 +1113,6 @@ impl<'ctx> Float<'ctx> { - unsafe { Self::wrap(ctx, Z3_mk_fpa_round_toward_positive(ctx.z3_ctx)) } - } - -- // returns RoundingMode towards away from zero -- pub fn round_towards_nearest_away(ctx: &'ctx Context) -> Float<'ctx> { -- unsafe { Self::wrap(ctx, Z3_mk_fpa_round_nearest_ties_to_away(ctx.z3_ctx)) } -- } -- -- // returns RoundingMode towards nearest even -- pub fn round_towards_nearest_even(ctx: &'ctx Context) -> Float<'ctx> { -- unsafe { Self::wrap(ctx, Z3_mk_fpa_round_nearest_ties_to_even(ctx.z3_ctx)) } -- } -- - // Add two floats of the same size, rounding towards zero - pub fn add_towards_zero(&self, other: &Self) -> Float<'ctx> { - Self::round_towards_zero(self.ctx).add(self, other) -@@ -1297,22 +1138,6 @@ impl<'ctx> Float<'ctx> { - unsafe { BV::wrap(self.ctx, Z3_mk_fpa_to_ieee_bv(self.ctx.z3_ctx, self.z3_ast)) } - } - -- /// NaN for an arbitrary FP sort. -- pub fn nan(ctx: &'ctx Context, sort: &Sort<'ctx>) -> Float<'ctx> { -- debug_assert!(matches!(sort.kind(), SortKind::FloatingPoint)); -- unsafe { Self::wrap(ctx, Z3_mk_fpa_nan(ctx.z3_ctx, sort.z3_sort)) } -- } -- -- /// Convenience IEEE-754 single & double. -- pub fn nan32(ctx: &'ctx Context) -> Float<'ctx> { -- let s = Sort::float(ctx, 8, 24); -- Self::nan(ctx, &s) -- } -- pub fn nan64(ctx: &'ctx Context) -> Float<'ctx> { -- let s = Sort::float(ctx, 11, 53); -- Self::nan(ctx, &s) -- } -- - unop! { - unary_abs(Z3_mk_fpa_abs, Self); - unary_neg(Z3_mk_fpa_neg, Self); -@@ -1473,16 +1298,6 @@ impl<'ctx> String<'ctx> { - } - } - -- /// Greater than in lexicographic order (str.> s1 s2) -- pub fn str_gt(&self, other: &Self) -> Bool<'ctx> { -- other.str_lt(self) -- } -- -- /// Greater than or equal to in lexicographic order (str.>= s1 s2) -- pub fn str_ge(&self, other: &Self) -> Bool<'ctx> { -- other.str_le(self) -- } -- - varop! { - /// Appends the argument strings to `Self` - concat(Z3_mk_seq_concat, String<'ctx>); -@@ -1500,10 +1315,6 @@ impl<'ctx> String<'ctx> { - prefix(Z3_mk_seq_prefix, Bool<'ctx>); - /// Checks whether `Self` is a suffix of the argument - suffix(Z3_mk_seq_suffix, Bool<'ctx>); -- /// Checks whether `Self` is less than the argument in lexicographic order (str.< s1 s2) -- str_lt(Z3_mk_str_lt, Bool<'ctx>); -- /// Checks whether `Self` is less than or equal to the argument in lexicographic order (str.<= s1 s2) -- str_le(Z3_mk_str_le, Bool<'ctx>); - } - } - -@@ -2024,12 +1835,6 @@ impl<'ctx> Seq<'ctx> { - } - } - -- /// Create an empty sequence of the given sort. -- pub fn empty(ctx: &'ctx Context, eltype: &Sort<'ctx>) -> Self { -- let sort = Sort::seq(ctx, eltype); -- unsafe { Self::wrap(ctx, Z3_mk_seq_empty(ctx.z3_ctx, sort.z3_sort)) } -- } -- - /// Create a unit sequence of `a`. - pub fn unit>(ctx: &'ctx Context, a: &A) -> Self { - unsafe { Self::wrap(ctx, Z3_mk_seq_unit(ctx.z3_ctx, a.get_z3_ast())) } -@@ -2078,15 +1883,6 @@ impl<'ctx> Seq<'ctx> { - unsafe { Int::wrap(self.ctx, Z3_mk_seq_length(self.ctx.z3_ctx, self.z3_ast)) } - } - -- pub fn contains(&self, containee: &Self) -> Bool<'ctx> { -- unsafe { -- Bool::wrap( -- self.ctx, -- Z3_mk_seq_contains(self.ctx.z3_ctx, self.z3_ast, containee.z3_ast), -- ) -- } -- } -- - varop! { - /// Concatenate sequences. - concat(Z3_mk_seq_concat, Self); -diff --git a/z3/src/config.rs b/z3/src/config.rs -index 176b5dd..2c66e99 100644 ---- a/z3/src/config.rs -+++ b/z3/src/config.rs -@@ -39,12 +39,6 @@ impl Config { - /// - /// - [`Config::set_bool_param_value()`] - pub fn set_param_value(&mut self, k: &str, v: &str) { -- if k == "ctrl_c" { -- eprintln!( -- "WARNING: Parameter 'ctrl_c' is global-only; use `z3::set_global_param` instead." -- ); -- return; -- } - let ks = CString::new(k).unwrap(); - let vs = CString::new(v).unwrap(); - self.kvs.push((ks, vs)); -diff --git a/z3/src/probe.rs b/z3/src/probe.rs -index 9a25d60..b711f1a 100644 ---- a/z3/src/probe.rs -+++ b/z3/src/probe.rs -@@ -84,7 +84,7 @@ impl<'ctx> Probe<'ctx> { - /// by `self` is less than the value returned by `p`. - /// - /// NOTE: For probes, "true" is any value different from 0.0. -- pub fn lt(&self, p: &Probe) -> Probe<'ctx> { -+ pub fn lt(&self, p: Probe) -> Probe<'ctx> { - unsafe { - Self::wrap( - self.ctx, -diff --git a/z3/src/solver.rs b/z3/src/solver.rs -index 282cfa2..e24c83a 100644 ---- a/z3/src/solver.rs -+++ b/z3/src/solver.rs -@@ -39,6 +39,13 @@ impl<'ctx> Solver<'ctx> { - /// `solver2_unknown`, and `ignore_solver1` parameters of the combined - /// solver to change its behaviour. - /// -+ /// The function [`Solver::get_model()`] retrieves a model if the -+ /// assertions is satisfiable (i.e., the result is -+ /// `SatResult::Sat`) and [model construction is enabled]. -+ /// The function [`Solver::get_model()`] can also be used even -+ /// if the result is `SatResult::Unknown`, but the returned model -+ /// is not guaranteed to satisfy quantified assertions. -+ /// - /// [model construction is enabled]: crate::Config::set_model_generation - pub fn new(ctx: &'ctx Context) -> Solver<'ctx> { - unsafe { Self::wrap(ctx, Z3_mk_solver(ctx.z3_ctx)) } -@@ -296,13 +303,6 @@ impl<'ctx> Solver<'ctx> { - - /// Retrieve the model for the last [`Solver::check()`] - /// or [`Solver::check_assumptions()`]. -- /// -- /// The function [`Solver::get_model()`] retrieves a model if the -- /// assertions is satisfiable (i.e., the result is -- /// `SatResult::Sat`) and [model construction is enabled]. -- /// The function [`Solver::get_model()`] can also be used even -- /// if the result is `SatResult::Unknown`, but the returned model -- /// is not guaranteed to satisfy quantified assertions. - /// - /// The error handler is invoked if a model is not available because - /// the commands above were not invoked for the given solver, or if From 7292259074db18a99c42fd7c5f1b6d83ce82d4af Mon Sep 17 00:00:00 2001 From: mehrad31415 Date: Mon, 18 Aug 2025 22:15:24 -0400 Subject: [PATCH 3/5] wrote unit tests for u128/i128 in tests/lib.rs --- z3/tests/lib.rs | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs index 8f65c1f5..1cbb39f6 100644 --- a/z3/tests/lib.rs +++ b/z3/tests/lib.rs @@ -1987,3 +1987,32 @@ fn test_model_iter() { vec![ast::Dynamic::new_const(&ctx, "a", &Sort::int(&ctx))] ); } + +#[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()); +} From 6e7de30fc796a27c7f329e18e23c73983b6768dd Mon Sep 17 00:00:00 2001 From: mehrad31415 Date: Tue, 19 Aug 2025 08:55:03 -0400 Subject: [PATCH 4/5] merge rebase with the master branch --- z3/src/ast/int.rs | 56 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/z3/src/ast/int.rs b/z3/src/ast/int.rs index 1980f358..e4fda735 100644 --- a/z3/src/ast/int.rs +++ b/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 { + 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::().ok() + } + + pub fn as_u128(&self) -> Option { + 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::().ok() + } + pub fn from_real(ast: &Real) -> Int { unsafe { Self::wrap(&ast.ctx, Z3_mk_real2int(ast.ctx.z3_ctx.0, ast.z3_ast)) } } From 7127e2fa20cb653ebe11d6845863174a7a09c1a1 Mon Sep 17 00:00:00 2001 From: Mark DenHoed Date: Tue, 19 Aug 2025 22:43:30 +0100 Subject: [PATCH 5/5] Update lib.rs --- z3/tests/lib.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs index 79eae3ab..98904419 100644 --- a/z3/tests/lib.rs +++ b/z3/tests/lib.rs @@ -2017,7 +2017,8 @@ fn test_int_i128_u128() { assert_eq!(int_i.to_string(), int_u.to_string()); } - fn test_round_towards_nearest_away() { +#[test] +fn test_round_towards_nearest_away() { let cfg = Config::new(); let ctx = Context::new(&cfg); let solver = Solver::new(&ctx);