heh
| -rw-r--r-- | src/main.rs | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/src/main.rs b/src/main.rs index e9ba1ad..d3dcd85 100644 --- a/src/main.rs +++ b/src/main.rs @@ -28,6 +28,7 @@ pub mod util; use std::mem::MaybeUninit; pub use util::prelude::*; +use z3::ast::{Ast, Int}; pub unsafe fn intersect( p0x: f32, @@ -45,6 +46,66 @@ pub unsafe fn intersect( (t0 > 0. && t1 > 0.).then_some((x, p0y + t0 * v0y)) } +pub fn p2(i: &str) -> impl Display { + let mut v: [MaybeUninit::<_>; 300] = + // SAFETY: mu likes this + unsafe { MaybeUninit::uninit().assume_init() }; + let mut x = i.as_bytes(); + for i in 0..300 { + let α = 読む::迄::<i64>(&mut x, b','); + x.skip(1); + let β = 読む::迄::<i64>(&mut x, b','); + x.skip(1); + let γ = 読む::迄::<i64>(&mut x, b' '); + x.skip(2); + let δ = 読む::負迄(&mut x, b','); + x.skip(1); + let ε = 読む::負迄(&mut x, b','); + x.skip(1); + let ζ = { + let (sign, mut n) = match x.by().ψ() { + b'-' => (-1, 0), + b => (1, i64::from(b - b'0')), + }; + while let Ok(b) = x.by() + && b != b'\n' + { + n = n * 10 + i64::from(b - b'0'); + } + n * sign as i64 + }; + v[i].write(([α, β, γ], [δ, ε, ζ])); + } + let v = v.map(|elem| unsafe { elem.assume_init() }); + let c = z3::Context::new(&z3::Config::new()); + let s = z3::Solver::new(&c); + macro_rules! dec { + (from $($x:ident)+) => { + $(let $x = z3::ast::Int::from_i64(&c, $x);)+ + }; + ($($x:ident)+) => { + $(let $x = z3::ast::Int::new_const(&c, stringify!($x));)+ + }; + } + dec!(x y z vx vy vz); + for (([xi, yi, zi], [vxi, vyi, vzi]), i) in v.into_iter().ι::<u16>() { + dec!(from xi yi zi vxi vyi vzi); + let ti = Int::new_const(&c, format!("t{i}")); + s.assert(&(xi + vxi * &ti)._eq(&(&x + &vx * &ti))); + s.assert(&(yi + vyi * &ti)._eq(&(&y + &vy * &ti))); + s.assert(&(zi + vzi * &ti)._eq(&(&z + &vz * &ti))); + } + s.check(); + let r = s + .get_model() + .unwrap() + .eval(&(x + y + z), true) + .unwrap() + .as_i64() + .unwrap(); + r +} + pub fn run(i: &str) -> impl Display { let mut v: [MaybeUninit::<_>; 300] = // SAFETY: mu likes this |