Upgrade z3

Author: BakerNet

Cargo.lock

@@ -25,6 +25,6 @@ petgraph = "0.6.4"
 pico-args = "0.5.0"
 regex = "1.11.1"
 rustworkx-core = "0.13.2"
-z3 = { version = "0.13" }
+z3 = "0.19"
 
 # Solution dependencies

aoc2023/Cargo.toml

@@ -99,24 +99,22 @@ pub fn part_one(input: &str) -> Option<u64> {
 pub fn part_two(input: &str) -> Option<u64> {
     let stones = input.lines().map(Hailstone::from).collect::<Vec<_>>();
 
-    let z3_conf = z3::Config::new();
-    let ctx = z3::Context::new(&z3_conf);
-    let solver = z3::Solver::new(&ctx);
+    let solver = z3::Solver::new();
 
-    let x = Int::new_const(&ctx, "x");
-    let y = Int::new_const(&ctx, "y");
-    let z = Int::new_const(&ctx, "z");
+    let x = Int::new_const("x");
+    let y = Int::new_const("y");
+    let z = Int::new_const("z");
 
-    let vx = Int::new_const(&ctx, "vx");
-    let vy = Int::new_const(&ctx, "vy");
-    let vz = Int::new_const(&ctx, "vz");
+    let vx = Int::new_const("vx");
+    let vy = Int::new_const("vy");
+    let vz = Int::new_const("vz");
 
     stones.iter().enumerate().for_each(|(i, hs)| {
-        let t_intercept = Int::new_const(&ctx, format!("t_{}", i));
+        let t_intercept = Int::new_const(format!("t_{}", i));
 
-        solver.assert(&(&x + &vx * &t_intercept)._eq(&(hs.point.0 + hs.velocity.0 * &t_intercept)));
-        solver.assert(&(&y + &vy * &t_intercept)._eq(&(hs.point.1 + hs.velocity.1 * &t_intercept)));
-        solver.assert(&(&z + &vz * &t_intercept)._eq(&(hs.point.2 + hs.velocity.2 * &t_intercept)));
+        solver.assert(&(&x + &vx * &t_intercept).eq(&(hs.point.0 + hs.velocity.0 * &t_intercept)));
+        solver.assert(&(&y + &vy * &t_intercept).eq(&(hs.point.1 + hs.velocity.1 * &t_intercept)));
+        solver.assert(&(&z + &vz * &t_intercept).eq(&(hs.point.2 + hs.velocity.2 * &t_intercept)));
     });
 
     let res = solver.check();

aoc2023/src/bin/24.rs

@@ -27,6 +27,6 @@ pico-args = "0.5"
 regex = "1.11"
 tinyjson = "2.5"
 tinyvec = "1.8"
-z3 = "0.13"
+z3 = "0.19"
 
 # Solution dependencies

aoc2025/Cargo.toml

@@ -1,9 +1,6 @@
 use aoc_utils::*;
 use itertools::Itertools;
-use z3::{
-    ast::{Ast, Int},
-    Config, Context, Optimize, SatResult,
-};
+use z3::{ast::Int, Optimize, SatResult};
 
 advent_of_code::solution!(10);
 
@@ -66,13 +63,11 @@ pub fn part_one(input: &str) -> Option<u64> {
 }
 
 fn solve_part2(buttons: &[Vec<usize>], joltages: &[u64]) -> u64 {
-    let cfg = Config::new();
-    let ctx = Context::new(&cfg);
-    let opt = Optimize::new(&ctx);
+    let opt = Optimize::new();
 
     // target_counts = number of times to press each button (what we're solving for)
     let target_counts: Vec<Int> = (0..buttons.len())
-        .map(|i| Int::new_const(&ctx, format!("p{i}")))
+        .map(|i| Int::new_const(format!("p{i}")))
         .collect();
 
     // Constraint: (sum of target_counts[i] for all i where pos in buttons[i]) == joltages[pos]
@@ -84,19 +79,19 @@ fn solve_part2(buttons: &[Vec<usize>], joltages: &[u64]) -> u64 {
             .map(|(i, _)| &target_counts[i])
             .collect();
 
-        let sum = Int::add(&ctx, &terms);
-        opt.assert(&sum._eq(&Int::from_u64(&ctx, jolt)));
+        let sum = Int::add(&terms);
+        opt.assert(&sum.eq(&Int::from_u64(jolt)));
     }
 
     // Constraint: t >= 0 (can't press a button negative times)
-    let zero = Int::from_u64(&ctx, 0);
+    let zero = Int::from_u64(0);
     for t in &target_counts {
         opt.assert(&t.ge(&zero));
     }
 
     // Minimize sum of target_counts
     let target_count_refs: Vec<_> = target_counts.iter().collect();
-    let total = Int::add(&ctx, &target_count_refs);
+    let total = Int::add(&target_count_refs);
     opt.minimize(&total);
 
     // Solve and extract result