inverse_conway/
lib.rs

1#![no_std]
2#![forbid(unsafe_code)]
3#![doc = include_str!("../README.md")]
4
5#[macro_use] extern crate alloc;
6
7use core::fmt;
8use alloc::vec::Vec;
9
10use z3::{Context, Solver, SatResult};
11use z3::ast::{Ast, Bool, Int};
12
13/// A finite tile map for Conway's game of life.
14#[derive(Clone, PartialEq, Eq)]
15pub struct Conway {
16    rows: usize,
17    cols: usize,
18    data: Vec<bool>,
19}
20impl Conway {
21    /// Creates a new, empty board devoid of all life and purpose.
22    pub fn new(mut rows: usize, mut cols: usize) -> Self {
23        if rows == 0 || cols == 0 {
24            (rows, cols) = (0, 0);
25        }
26
27        Self { rows, cols, data: vec![false; rows * cols] }
28    }
29    /// Gets the value of a tile.
30    pub fn get(&self, row: usize, col: usize) -> Result<bool, ()> {
31        if row < self.rows && col < self.cols {
32            Ok(self.data[row * self.cols + col])
33        } else {
34            Err(())
35        }
36    }
37    /// Sets the value of a tile.
38    pub fn set(&mut self, row: usize, col: usize, value: bool) -> Result<(), ()> {
39        if row < self.rows && col < self.cols {
40            self.data[row * self.cols + col] = value;
41            Ok(())
42        } else {
43            Err(())
44        }
45    }
46    /// Increases the board size by `padding` in all directions.
47    pub fn inflate(&self, padding: usize) -> Self {
48        let mut res = Self::new(self.rows + 2 * padding, self.cols + 2 * padding);
49        for row in 0..self.rows {
50            for col in 0..self.cols {
51                res.set(row + padding, col + padding, self.get(row, col).unwrap()).unwrap();
52            }
53        }
54        res
55    }
56    /// Performs a forward pass in time. Boring.
57    pub fn forward(&self, steps: usize) -> Self {
58        let mut res = self.clone();
59        for _ in 0..steps {
60            let mut counts = vec![0; res.rows * res.cols];
61            for row in 0..res.rows {
62                for col in 0..res.cols {
63                    if res.data[row * res.cols + col] {
64                        for c_row in row.saturating_sub(1)..(row + 2).min(res.rows) {
65                            for c_col in col.saturating_sub(1)..(col + 2).min(res.cols) {
66                                counts[c_row * res.cols + c_col] += 1;
67                            }
68                        }
69                    }
70                }
71            }
72            res = Conway { rows: res.rows, cols: res.cols, data: res.data.iter().zip(counts).map(|(live, count)| (*live && count == 4) || count == 3).collect() };
73        }
74        res
75    }
76    /// Performs a backward pass in time. Now we're talkin'!
77    ///
78    /// Not all board states are reachable, so this can fail with [`None`].
79    /// Additionally, the operation is not separable, so `backward(1)` followed by `backward(1)` may fail even if `backward(2)` would succeed.
80    pub fn backward(&self, steps: usize) -> Option<Self> {
81        let context = Context::new(&Default::default());
82
83        let zero = Int::from_u64(&context, 0);
84        let one = Int::from_u64(&context, 1);
85        let three = Int::from_u64(&context, 3);
86        let four = Int::from_u64(&context, 4);
87
88        let vars = {
89            let mut vars = Vec::with_capacity(self.rows * self.cols);
90            for row in 0..self.rows {
91                for col in 0..self.cols {
92                    vars.push(Bool::new_const(&context, format!("d{row},{col}")));
93                }
94            }
95            vars
96        };
97
98        let mut res = vars.clone();
99        for _ in 0..steps {
100            let mut counts = vec![zero.clone(); self.rows * self.cols];
101            for row in 0..self.rows {
102                for col in 0..self.cols {
103                    for c_row in row.saturating_sub(1)..(row + 2).min(self.rows) {
104                        for c_col in col.saturating_sub(1)..(col + 2).min(self.cols) {
105                            counts[c_row * self.cols + c_col] += res[row * self.cols + col].ite(&one, &zero);
106                        }
107                    }
108                }
109            }
110            res = res.iter().zip(counts).map(|(live, count)| (live & count._eq(&four) | count._eq(&three))).collect();
111        }
112
113        let s = Solver::new(&context);
114        for (res, actual) in res.iter().zip(&self.data) {
115            if *actual {
116                s.assert(res);
117            } else {
118                let res = res.not();
119                s.assert(&res);
120            }
121        }
122
123        match s.check() {
124            SatResult::Sat => {
125                let model = s.get_model().unwrap();
126                Some(Self { rows: self.rows, cols: self.cols, data: vars.iter().map(|v| model.eval(v, true).unwrap().as_bool().unwrap()).collect() })
127            }
128            SatResult::Unsat => None,
129            SatResult::Unknown => unreachable!(),
130        }
131    }
132}
133impl fmt::Debug for Conway {
134    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
135        if self.rows == 0 || self.cols == 0 {
136            return f.write_str("[]");
137        }
138
139        for row in 0..self.rows {
140            for col in 0..self.cols {
141                f.write_str(if self.data[row * self.cols + col] { "■" } else { "□" })?;
142            }
143            f.write_str("\n")?;
144        }
145        Ok(())
146    }
147}
inverse_conway/lib.rs

inverse_conway/
lib.rs
