Inline format args.

z3-sys/build.rs

@@ -31,7 +31,7 @@ fn find_library_header_by_vcpkg() -> String {
         include.push("z3.h");
         if include.exists() {
             let header = include.to_str().unwrap().to_owned();
-            println!("cargo:rerun-if-changed={}", header);
+            println!("cargo:rerun-if-changed={header}");
             return header;
         }
     }
@@ -70,8 +70,8 @@ fn generate_binding(header: &str) {
             .header(header)
             .parse_callbacks(Box::new(bindgen::CargoCallbacks))
             .generate_comments(false)
-            .rustified_enum(format!("Z3_{}", x))
-            .allowlist_type(format!("Z3_{}", x));
+            .rustified_enum(format!("Z3_{x}"))
+            .allowlist_type(format!("Z3_{x}"));
         if env::var("TARGET").unwrap() == "wasm32-unknown-emscripten" {
             enum_bindings = enum_bindings.clang_arg(format!(
                 "--sysroot={}/upstream/emscripten/cache/sysroot",
@@ -81,7 +81,7 @@ fn generate_binding(header: &str) {
         enum_bindings
             .generate()
             .expect("Unable to generate bindings")
-            .write_to_file(out_path.join(format!("{}.rs", x)))
+            .write_to_file(out_path.join(format!("{x}.rs")))
             .expect("Couldn't write bindings!");
     }
 }

z3/src/ast.rs

@@ -594,7 +594,7 @@ impl<'ctx> Real<'ctx> {
     pub fn from_real_str(ctx: &'ctx Context, num: &str, den: &str) -> Option<Real<'ctx>> {
         let sort = Sort::real(ctx);
         let ast = unsafe {
-            let fraction_cstring = CString::new(format!("{:} / {:}", num, den)).unwrap();
+            let fraction_cstring = CString::new(format!("{num:} / {den:}")).unwrap();
             let numeral_ptr = Z3_mk_numeral(ctx.z3_ctx, fraction_cstring.as_ptr(), sort.z3_sort);
             if numeral_ptr.is_null() {
                 return None;

z3/src/config.rs

@@ -84,7 +84,7 @@ impl Config {
     }
 
     pub fn set_timeout_msec(&mut self, ms: u64) {
-        self.set_param_value("timeout", &format!("{}", ms));
+        self.set_param_value("timeout", &format!("{ms}"));
     }
 }
 

z3/src/func_decl.rs

@@ -106,7 +106,7 @@ impl<'ctx> fmt::Display for FuncDecl<'ctx> {
             return Result::Err(fmt::Error);
         }
         match unsafe { CStr::from_ptr(p) }.to_str() {
-            Ok(s) => write!(f, "{}", s),
+            Ok(s) => write!(f, "{s}"),
             Err(_) => Result::Err(fmt::Error),
         }
     }

z3/src/goal.rs

@@ -119,7 +119,7 @@ impl<'ctx> fmt::Display for Goal<'ctx> {
             return Result::Err(fmt::Error);
         }
         match unsafe { CStr::from_ptr(p) }.to_str() {
-            Ok(s) => write!(f, "{}", s),
+            Ok(s) => write!(f, "{s}"),
             Err(_) => Result::Err(fmt::Error),
         }
     }

z3/src/model.rs

@@ -146,7 +146,7 @@ impl<'ctx> fmt::Display for Model<'ctx> {
             return Result::Err(fmt::Error);
         }
         match unsafe { CStr::from_ptr(p) }.to_str() {
-            Ok(s) => write!(f, "{}", s),
+            Ok(s) => write!(f, "{s}"),
             Err(_) => Result::Err(fmt::Error),
         }
     }

z3/src/optimize.rs

@@ -218,7 +218,7 @@ impl<'ctx> fmt::Display for Optimize<'ctx> {
             return Result::Err(fmt::Error);
         }
         match unsafe { CStr::from_ptr(p) }.to_str() {
-            Ok(s) => write!(f, "{}", s),
+            Ok(s) => write!(f, "{s}"),
             Err(_) => Result::Err(fmt::Error),
         }
     }

z3/src/params.rs

@@ -106,7 +106,7 @@ impl<'ctx> fmt::Display for Params<'ctx> {
             return Result::Err(fmt::Error);
         }
         match unsafe { CStr::from_ptr(p) }.to_str() {
-            Ok(s) => write!(f, "{}", s),
+            Ok(s) => write!(f, "{s}"),
             Err(_) => Result::Err(fmt::Error),
         }
     }

z3/src/pattern.rs

@@ -53,7 +53,7 @@ impl<'ctx> fmt::Debug for Pattern<'ctx> {
             return Result::Err(fmt::Error);
         }
         match unsafe { CStr::from_ptr(p) }.to_str() {
-            Ok(s) => write!(f, "{}", s),
+            Ok(s) => write!(f, "{s}"),
             Err(_) => Result::Err(fmt::Error),
         }
     }

z3/src/rec_func_decl.rs

@@ -101,7 +101,7 @@ impl<'ctx> fmt::Display for RecFuncDecl<'ctx> {
             return Result::Err(fmt::Error);
         }
         match unsafe { CStr::from_ptr(p) }.to_str() {
-            Ok(s) => write!(f, "{}", s),
+            Ok(s) => write!(f, "{s}"),
             Err(_) => Result::Err(fmt::Error),
         }
     }

z3/src/solver.rs

@@ -318,7 +318,7 @@ impl<'ctx> fmt::Display for Solver<'ctx> {
             return Result::Err(fmt::Error);
         }
         match unsafe { CStr::from_ptr(p) }.to_str() {
-            Ok(s) => write!(f, "{}", s),
+            Ok(s) => write!(f, "{s}"),
             Err(_) => Result::Err(fmt::Error),
         }
     }

z3/src/sort.rs

@@ -281,7 +281,7 @@ impl<'ctx> fmt::Display for Sort<'ctx> {
             return Result::Err(fmt::Error);
         }
         match unsafe { CStr::from_ptr(p) }.to_str() {
-            Ok(s) => write!(f, "{}", s),
+            Ok(s) => write!(f, "{s}"),
             Err(_) => Result::Err(fmt::Error),
         }
     }

z3/src/tactic.rs

@@ -251,7 +251,7 @@ impl<'ctx> fmt::Display for Tactic<'ctx> {
             return Result::Err(fmt::Error);
         }
         match unsafe { CStr::from_ptr(p) }.to_str() {
-            Ok(s) => write!(f, "{}", s),
+            Ok(s) => write!(f, "{s}"),
             Err(_) => Result::Err(fmt::Error),
         }
     }

z3/tests/lib.rs

@@ -139,10 +139,10 @@ fn test_format() {
     let cfg = Config::new();
     let ctx = Context::new(&cfg);
     let ast = ast::Int::new_const(&ctx, "x");
-    assert_eq!("x", format!("{}", ast));
+    assert_eq!("x", format!("{ast}"));
 
     let int = Sort::int(&ctx);
-    assert_eq!("Int", format!("{}", int));
+    assert_eq!("Int", format!("{int}"));
 }
 
 #[test]
@@ -974,7 +974,7 @@ fn check_application_of_tactic_to_goal() {
     goal.assert(&y_greater_than_or_equal_to_one);
 
     assert_eq!(
-        format!("{}", goal),
+        format!("{goal}"),
         "(goal\n  x\n  (>= (+ y 1) 2)\n  (>= y 1))"
     );
     let apply_results = repeat_tactic.apply(&goal, Some(&params));
@@ -984,7 +984,7 @@ fn check_application_of_tactic_to_goal() {
         .collect::<Vec<Goal>>();
     let goal_result = goal_results.first().unwrap();
 
-    assert_eq!(format!("{}", goal_result), "(goal\n  x\n  (>= y 1))");
+    assert_eq!(format!("{goal_result}"), "(goal\n  x\n  (>= y 1))");
 }
 
 #[test]
@@ -1084,9 +1084,9 @@ fn test_goal_reset() {
     let a = ast::Bool::new_const(&ctx, "a");
     let goal = Goal::new(&ctx, false, false, false);
     goal.assert(&a);
-    assert_eq!(format!("{}", goal), "(goal\n  a)");
+    assert_eq!(format!("{goal}"), "(goal\n  a)");
     goal.reset();
-    assert_eq!(format!("{}", goal), "(goal)");
+    assert_eq!(format!("{goal}"), "(goal)");
 }
 
 #[test]
@@ -1247,7 +1247,7 @@ fn test_tactic_try_for() {
         .list_subgoals()
         .collect::<Vec<Goal>>();
     let goal_result = goal_results.first().unwrap();
-    assert_eq!(format!("{}", goal_result), "(goal\n  (>= x 3))");
+    assert_eq!(format!("{goal_result}"), "(goal\n  (>= x 3))");
 }
 
 #[test]
@@ -1324,8 +1324,7 @@ fn test_goal_apply_tactic() {
         assert_eq!(
             goal_result.get_formulas::<Bool>(),
             after_formulas,
-            "Before: {:?}",
-            before_formulas
+            "Before: {before_formulas:?}"
         );
     }
 
@@ -1644,10 +1643,10 @@ fn test_array_example1() {
     for a in g.get_formulas() {
         s.assert(&a);
     }
-    println!("Solver: {}", s);
+    println!("Solver: {s}");
 
     let q = s.check();
-    println!("Status: {:?}", q);
+    println!("Status: {q:?}");
 
     if q != SatResult::Sat {
         panic!("Solver did not return sat");