Elide lifetimes

prove-rs · Dec 9, 2024 · 419643b · 419643b
1 parent 0eb903d
commit 419643b
Show file tree

Hide file tree

Showing 15 changed files with 53 additions and 53 deletions.
diff --git a/z3/src/context.rs b/z3/src/context.rs
@@ -59,7 +59,7 @@ impl Context {
     }
 }
 
-impl<'ctx> ContextHandle<'ctx> {
+impl ContextHandle<'_> {
     /// Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
     pub fn interrupt(&self) {
         unsafe {
@@ -68,8 +68,8 @@ impl<'ctx> ContextHandle<'ctx> {
     }
 }
 
-unsafe impl<'ctx> Sync for ContextHandle<'ctx> {}
-unsafe impl<'ctx> Send for ContextHandle<'ctx> {}
+unsafe impl Sync for ContextHandle<'_> {}
+unsafe impl Send for ContextHandle<'_> {}
 
 impl Drop for Context {
     fn drop(&mut self) {

diff --git a/z3/src/func_decl.rs b/z3/src/func_decl.rs
@@ -99,7 +99,7 @@ impl<'ctx> FuncDecl<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for FuncDecl<'ctx> {
+impl fmt::Display for FuncDecl<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_func_decl_to_string(self.ctx.z3_ctx, self.z3_func_decl) };
         if p.is_null() {
@@ -112,13 +112,13 @@ impl<'ctx> fmt::Display for FuncDecl<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for FuncDecl<'ctx> {
+impl fmt::Debug for FuncDecl<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for FuncDecl<'ctx> {
+impl Drop for FuncDecl<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_dec_ref(

diff --git a/z3/src/func_entry.rs b/z3/src/func_entry.rs
@@ -41,7 +41,7 @@ impl<'ctx> FuncEntry<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for FuncEntry<'ctx> {
+impl fmt::Display for FuncEntry<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         write!(f, "[")?;
         self.get_args()
@@ -52,13 +52,13 @@ impl<'ctx> fmt::Display for FuncEntry<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for FuncEntry<'ctx> {
+impl fmt::Debug for FuncEntry<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for FuncEntry<'ctx> {
+impl Drop for FuncEntry<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_func_entry_dec_ref(self.ctx.z3_ctx, self.z3_func_entry);

diff --git a/z3/src/func_interp.rs b/z3/src/func_interp.rs
@@ -68,7 +68,7 @@ impl<'ctx> FuncInterp<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for FuncInterp<'ctx> {
+impl fmt::Display for FuncInterp<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         write!(f, "[")?;
         self.get_entries().into_iter().try_for_each(|e| {
@@ -95,13 +95,13 @@ impl<'ctx> fmt::Display for FuncInterp<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for FuncInterp<'ctx> {
+impl fmt::Debug for FuncInterp<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for FuncInterp<'ctx> {
+impl Drop for FuncInterp<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_func_interp_dec_ref(self.ctx.z3_ctx, self.z3_func_interp);

diff --git a/z3/src/goal.rs b/z3/src/goal.rs
@@ -5,7 +5,7 @@ use z3_sys::*;
 
 use crate::{ast, ast::Ast, Context, Goal};
 
-impl<'ctx> Clone for Goal<'ctx> {
+impl Clone for Goal<'_> {
     fn clone(&self) -> Self {
         Self {
             ctx: self.ctx,
@@ -109,7 +109,7 @@ impl<'ctx> Goal<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Goal<'ctx> {
+impl fmt::Display for Goal<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_goal_to_string(self.ctx.z3_ctx, self.z3_goal) };
         if p.is_null() {
@@ -122,13 +122,13 @@ impl<'ctx> fmt::Display for Goal<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Goal<'ctx> {
+impl fmt::Debug for Goal<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Goal<'ctx> {
+impl Drop for Goal<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_goal_dec_ref(self.ctx.z3_ctx, self.z3_goal);

diff --git a/z3/src/model.rs b/z3/src/model.rs
@@ -135,7 +135,7 @@ impl<'ctx> Model<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Model<'ctx> {
+impl fmt::Display for Model<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_model_to_string(self.ctx.z3_ctx, self.z3_mdl) };
         if p.is_null() {
@@ -148,13 +148,13 @@ impl<'ctx> fmt::Display for Model<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Model<'ctx> {
+impl fmt::Debug for Model<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Model<'ctx> {
+impl Drop for Model<'_> {
     fn drop(&mut self) {
         unsafe { Z3_model_dec_ref(self.ctx.z3_ctx, self.z3_mdl) };
     }
@@ -181,7 +181,7 @@ impl<'a, 'ctx> IntoIterator for &'a Model<'ctx> {
     }
 }
 
-impl<'a, 'ctx> Iterator for ModelIter<'a, 'ctx> {
+impl<'ctx> Iterator for ModelIter<'_, 'ctx> {
     type Item = FuncDecl<'ctx>;
 
     fn next(&mut self) -> Option<Self::Item> {

diff --git a/z3/src/optimize.rs b/z3/src/optimize.rs
@@ -274,7 +274,7 @@ impl<'ctx> Optimize<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Optimize<'ctx> {
+impl fmt::Display for Optimize<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_optimize_to_string(self.ctx.z3_ctx, self.z3_opt) };
         if p.is_null() {
@@ -287,13 +287,13 @@ impl<'ctx> fmt::Display for Optimize<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Optimize<'ctx> {
+impl fmt::Debug for Optimize<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Optimize<'ctx> {
+impl Drop for Optimize<'_> {
     fn drop(&mut self) {
         unsafe { Z3_optimize_dec_ref(self.ctx.z3_ctx, self.z3_opt) };
     }

diff --git a/z3/src/params.rs b/z3/src/params.rs
@@ -99,7 +99,7 @@ pub fn reset_all_global_params() {
     unsafe { Z3_global_param_reset_all() };
 }
 
-impl<'ctx> fmt::Display for Params<'ctx> {
+impl fmt::Display for Params<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_params_to_string(self.ctx.z3_ctx, self.z3_params) };
         if p.is_null() {
@@ -112,13 +112,13 @@ impl<'ctx> fmt::Display for Params<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Params<'ctx> {
+impl fmt::Debug for Params<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Params<'ctx> {
+impl Drop for Params<'_> {
     fn drop(&mut self) {
         unsafe { Z3_params_dec_ref(self.ctx.z3_ctx, self.z3_params) };
     }

diff --git a/z3/src/pattern.rs b/z3/src/pattern.rs
@@ -46,7 +46,7 @@ impl<'ctx> Pattern<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Pattern<'ctx> {
+impl fmt::Debug for Pattern<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_pattern_to_string(self.ctx.z3_ctx, self.z3_pattern) };
         if p.is_null() {
@@ -59,13 +59,13 @@ impl<'ctx> fmt::Debug for Pattern<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Pattern<'ctx> {
+impl fmt::Display for Pattern<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Debug>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Pattern<'ctx> {
+impl Drop for Pattern<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_dec_ref(self.ctx.z3_ctx, self.z3_pattern as Z3_ast);

diff --git a/z3/src/probe.rs b/z3/src/probe.rs
@@ -167,25 +167,25 @@ impl<'ctx> Probe<'ctx> {
     }
 }
 
-impl<'ctx> Clone for Probe<'ctx> {
+impl Clone for Probe<'_> {
     fn clone(&self) -> Self {
         unsafe { Self::wrap(self.ctx, self.z3_probe) }
     }
 }
 
-impl<'ctx> fmt::Display for Probe<'ctx> {
+impl fmt::Display for Probe<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         write!(f, "<z3.probe>")
     }
 }
 
-impl<'ctx> fmt::Debug for Probe<'ctx> {
+impl fmt::Debug for Probe<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Probe<'ctx> {
+impl Drop for Probe<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_probe_dec_ref(self.ctx.z3_ctx, self.z3_probe);

diff --git a/z3/src/rec_func_decl.rs b/z3/src/rec_func_decl.rs
@@ -94,7 +94,7 @@ impl<'ctx> RecFuncDecl<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for RecFuncDecl<'ctx> {
+impl fmt::Display for RecFuncDecl<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_func_decl_to_string(self.ctx.z3_ctx, self.z3_func_decl) };
         if p.is_null() {
@@ -107,13 +107,13 @@ impl<'ctx> fmt::Display for RecFuncDecl<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for RecFuncDecl<'ctx> {
+impl fmt::Debug for RecFuncDecl<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for RecFuncDecl<'ctx> {
+impl Drop for RecFuncDecl<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_dec_ref(

diff --git a/z3/src/solver.rs b/z3/src/solver.rs
@@ -400,7 +400,7 @@ impl<'ctx> Solver<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Solver<'ctx> {
+impl fmt::Display for Solver<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_solver_to_string(self.ctx.z3_ctx, self.z3_slv) };
         if p.is_null() {
@@ -413,13 +413,13 @@ impl<'ctx> fmt::Display for Solver<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Solver<'ctx> {
+impl fmt::Debug for Solver<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Solver<'ctx> {
+impl Drop for Solver<'_> {
     fn drop(&mut self) {
         unsafe { Z3_solver_dec_ref(self.ctx.z3_ctx, self.z3_slv) };
     }

diff --git a/z3/src/sort.rs b/z3/src/sort.rs
@@ -274,13 +274,13 @@ impl<'ctx> Sort<'ctx> {
     }
 }
 
-impl<'ctx> Clone for Sort<'ctx> {
+impl Clone for Sort<'_> {
     fn clone(&self) -> Self {
         unsafe { Self::wrap(self.ctx, self.z3_sort) }
     }
 }
 
-impl<'ctx> fmt::Display for Sort<'ctx> {
+impl fmt::Display for Sort<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_sort_to_string(self.ctx.z3_ctx, self.z3_sort) };
         if p.is_null() {
@@ -293,7 +293,7 @@ impl<'ctx> fmt::Display for Sort<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Sort<'ctx> {
+impl fmt::Debug for Sort<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
@@ -305,9 +305,9 @@ impl<'ctx> PartialEq<Sort<'ctx>> for Sort<'ctx> {
     }
 }
 
-impl<'ctx> Eq for Sort<'ctx> {}
+impl Eq for Sort<'_> {}
 
-impl<'ctx> Drop for Sort<'ctx> {
+impl Drop for Sort<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_dec_ref(
@@ -332,7 +332,7 @@ impl<'ctx> SortDiffers<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for SortDiffers<'ctx> {
+impl fmt::Display for SortDiffers<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         write!(
             f,

diff --git a/z3/src/statistics.rs b/z3/src/statistics.rs
@@ -79,19 +79,19 @@ impl<'ctx> Statistics<'ctx> {
     }
 }
 
-impl<'ctx> Clone for Statistics<'ctx> {
+impl Clone for Statistics<'_> {
     fn clone(&self) -> Self {
         unsafe { Self::wrap(self.ctx, self.z3_stats) }
     }
 }
 
-impl<'ctx> fmt::Display for Statistics<'ctx> {
+impl fmt::Display for Statistics<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         write!(f, "<z3.stats>")
     }
 }
 
-impl<'ctx> fmt::Debug for Statistics<'ctx> {
+impl fmt::Debug for Statistics<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let mut s = f.debug_struct("Statistics");
         for e in self.entries() {
@@ -104,7 +104,7 @@ impl<'ctx> fmt::Debug for Statistics<'ctx> {
     }
 }
 
-impl<'ctx> Drop for Statistics<'ctx> {
+impl Drop for Statistics<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_stats_dec_ref(self.ctx.z3_ctx, self.z3_stats);