initial commit

.gitignore

@@ -0,0 +1,2 @@
+/target
+/.cargo

Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "heterogeneous-polyhedral-units"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
+kiss3d = "0.37.2"
+z3 = "0.19.6"

MATH.md

@@ -0,0 +1,12 @@
+# Procedural Generation with Heterogeneous Polyhedral Units using pseudo-Boolean Satisfiability
+
+> DO NOT TOUCH, FOR MATHEMATICAL DEFINITION ONLY
+
+`Primitive Atom`: An indivisible volumetric unit whose geometry is a single convex polyhedron.
+Atom Type: An equivalence class of primitive atoms under rigid motions of ℝ³.
+
+`Adjacency Relation`: A symmetric binary relation over primitive atoms indicating admissible face-to-face contact.
+
+`Aggregate`: A finite set of primitive atoms whose induced adjacency graph is connected and whose internal adjacencies are fixed.
+
+`Placement instance:` A rigid motion mapping an aggregate’s atoms into the global adjacency graph such that all internal and external adjacency constraints are satisfied.

lines.sh

@@ -0,0 +1,4 @@
+find src -type f -iname '*.rs' \
+| xargs wc -l \
+| sort -nr \
+| xargs printf "\033[96m%d %s\033[0m\n"

src/adjacency/mod.rs

@@ -0,0 +1,2 @@
+pub mod adjacency_relation;
+pub mod interface;

src/geometry/aggregate.rs

@@ -0,0 +1,19 @@
+use crate::geometry::{
+    atom::{AtomRef, PrimitiveAtom},
+    face::FaceId,
+};
+
+#[derive(Debug, Clone)]
+pub struct Aggregate {
+    atoms: Vec<AtomRef>,
+    internal_adjacency: Vec<(AtomRef, FaceId, AtomRef, FaceId)>,
+}
+
+pub fn load_aggregates(atoms: Vec<PrimitiveAtom>) -> Vec<Aggregate> {
+    let mut aggregates = Vec::new();
+    for atom in atoms {
+        let aggregate = Aggregate {
+            
+        }
+    }
+}

src/geometry/atom.rs

@@ -0,0 +1,27 @@
+use std::{cell::RefCell, collections::HashMap, rc::Rc};
+
+use kiss3d::nalgebra::Point3;
+
+use crate::geometry::{
+    face::{Face, FaceId, FaceType},
+    polyhedra::cube::create_cube_atom,
+};
+
+#[derive(Debug, Clone)]
+pub struct Polyhedron {
+    pub vertices: Vec<Point3<f32>>,
+    pub faces: Vec<Face>,
+}
+
+#[derive(Debug, Clone)]
+pub struct PrimitiveAtom {
+    pub geometry: Polyhedron,
+    pub faces: Vec<FaceId>,
+    pub face_types: HashMap<FaceId, FaceType>,
+}
+
+pub fn load_atoms() -> Vec<PrimitiveAtom> {
+    vec![create_cube_atom()]
+}
+
+pub type AtomRef = Rc<RefCell<PrimitiveAtom>>;

src/geometry/face.rs

@@ -0,0 +1,48 @@
+use std::hash::{DefaultHasher, Hash, Hasher};
+
+use kiss3d::nalgebra::Vector3;
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
+pub enum FaceType {
+    Solid,
+    Empty,
+    Connector(String),
+}
+
+pub type FaceId = String;
+
+#[derive(Debug, Clone)]
+pub struct Face {
+    vertex_indices: Vec<usize>,
+    normal: Vector3<f32>,
+    id: FaceId,
+}
+
+impl Face {
+    pub fn from_type(face_type: FaceType, indices: Vec<usize>, normal: Vector3<f32>) -> Face {
+        let mut hasher = DefaultHasher::new();
+        face_type.hash(&mut hasher);
+        Face {
+            vertex_indices: indices,
+            normal: normal,
+            id: hasher.finish().to_string(),
+        }
+    }
+
+    pub fn id(self) -> FaceId {
+        self.id.clone()
+    }
+}
+
+impl Hash for Face {
+    fn hash<H: Hasher>(&self, state: &mut H) {
+        // Hash only fields that implement Hash; exclude `normal` because it contains f32 which is not Hash.
+        self.vertex_indices.hash(state);
+        self.id.hash(state);
+    }
+}
+
+pub fn is_topology_compatible(_a: FaceType, _b: FaceType) -> bool {
+    // todo: implement the thing lol
+    return true;
+}

src/geometry/mod.rs

@@ -0,0 +1,4 @@
+pub mod aggregate;
+pub mod atom;
+pub mod face;
+pub mod polyhedra;

src/geometry/polyhedra/cube.rs

@@ -0,0 +1,83 @@
+use std::collections::HashMap;
+
+use kiss3d::nalgebra::{Point3, Vector3};
+
+use crate::geometry::{
+    atom::{Polyhedron, PrimitiveAtom},
+    face::{Face, FaceType},
+};
+
+pub fn create_cube_atom() -> PrimitiveAtom {
+    let cube = create_cube_polyhedron();
+
+    // Create 6 solid faces for the cube
+    let mut face_types = HashMap::new();
+    let mut face_ids = vec![];
+
+    for face in &cube.faces {
+        face_types.insert(face.clone().id(), FaceType::Solid);
+        face_ids.push(face.clone().id());
+    }
+
+    PrimitiveAtom {
+        geometry: cube,
+        faces: face_ids,
+        face_types,
+    }
+}
+
+pub fn create_cube_polyhedron() -> Polyhedron {
+    // Unit cube vertices: 8 corners
+    let vertices = vec![
+        Point3::new(0.0f32, 0.0, 0.0), // 0: origin
+        Point3::new(1.0f32, 0.0, 0.0), // 1
+        Point3::new(1.0f32, 1.0, 0.0), // 2
+        Point3::new(0.0f32, 1.0, 0.0), // 3
+        Point3::new(0.0f32, 0.0, 1.0), // 4
+        Point3::new(1.0f32, 0.0, 1.0), // 5
+        Point3::new(1.0f32, 1.0, 1.0), // 6
+        Point3::new(0.0f32, 1.0, 1.0), // 7
+    ];
+
+    // 6 faces of the cube, each defined by 4 vertex indices
+    let faces = vec![
+        // Bottom face (z=0), normal pointing down
+        Face::from_type(
+            FaceType::Solid,
+            vec![0, 1, 2, 3],
+            Vector3::new(0.0f32, 0.0, -1.0),
+        ),
+        // Top face (z=1), normal pointing up
+        Face::from_type(
+            FaceType::Solid,
+            vec![4, 7, 6, 5],
+            Vector3::new(0.0f32, 0.0, 1.0),
+        ),
+        // Front face (y=0), normal pointing forward
+        Face::from_type(
+            FaceType::Solid,
+            vec![0, 4, 5, 1],
+            Vector3::new(0.0f32, -1.0, 0.0),
+        ),
+        // Back face (y=1), normal pointing back
+        Face::from_type(
+            FaceType::Solid,
+            vec![3, 2, 6, 7],
+            Vector3::new(0.0f32, 1.0, 0.0),
+        ),
+        // Left face (x=0), normal pointing left
+        Face::from_type(
+            FaceType::Solid,
+            vec![0, 3, 7, 4],
+            Vector3::new(-1.0f32, 0.0, 0.0),
+        ),
+        // Right face (x=1), normal pointing right
+        Face::from_type(
+            FaceType::Solid,
+            vec![1, 5, 6, 2],
+            Vector3::new(1.0f32, 0.0, 0.0),
+        ),
+    ];
+
+    Polyhedron { vertices, faces }
+}

src/geometry/polyhedra/mod.rs

@@ -0,0 +1 @@
+pub mod cube;

src/logic/formula.rs

@@ -0,0 +1,353 @@
+use std::collections::HashMap;
+use std::fmt;
+
+/// Represents a Boolean variable in a SAT formula
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub struct BoolVar {
+    name: String,
+}
+
+impl BoolVar {
+    pub fn new(name: impl Into<String>) -> Self {
+        Self { name: name.into() }
+    }
+
+    pub fn get_name(&self) -> &str {
+        &self.name
+    }
+}
+
+/// Represents an integer variable for PB constraints
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub struct IntVar {
+    name: String,
+    min: Option<i64>,
+    max: Option<i64>,
+}
+
+impl IntVar {
+    pub fn new(name: impl Into<String>) -> Self {
+        Self {
+            name: name.into(),
+            min: None,
+            max: None,
+        }
+    }
+
+    pub fn with_bounds(name: impl Into<String>, min: i64, max: i64) -> Self {
+        Self {
+            name: name.into(),
+            min: Some(min),
+            max: Some(max),
+        }
+    }
+
+    pub fn get_name(&self) -> &str {
+        &self.name
+    }
+
+    pub fn get_bounds(&self) -> (Option<i64>, Option<i64>) {
+        (self.min, self.max)
+    }
+}
+
+/// Represents an arithmetic expression over IntVar
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub enum IntExpr {
+    Var(IntVar),
+    Const(i64),
+    Add(Box<IntExpr>, Box<IntExpr>), // a + b
+    Sub(Box<IntExpr>, Box<IntExpr>), // a - b
+    Mul(Box<IntExpr>, Box<IntExpr>), // a * b (only with constants)
+    Neg(Box<IntExpr>),               // -a
+}
+
+impl IntExpr {
+    pub fn var(v: IntVar) -> Self {
+        IntExpr::Var(v)
+    }
+
+    pub fn const_val(c: i64) -> Self {
+        IntExpr::Const(c)
+    }
+
+    pub fn add(a: IntExpr, b: IntExpr) -> Self {
+        IntExpr::Add(Box::new(a), Box::new(b))
+    }
+
+    pub fn sub(a: IntExpr, b: IntExpr) -> Self {
+        IntExpr::Sub(Box::new(a), Box::new(b))
+    }
+
+    pub fn mul(a: IntExpr, b: IntExpr) -> Self {
+        IntExpr::Mul(Box::new(a), Box::new(b))
+    }
+
+    pub fn neg(a: IntExpr) -> Self {
+        IntExpr::Neg(Box::new(a))
+    }
+}
+
+/// Helper function to convert IntExpr to string representation
+fn expr_to_string(expr: &IntExpr) -> String {
+    match expr {
+        IntExpr::Var(v) => v.get_name().to_string(),
+        IntExpr::Const(c) => c.to_string(),
+        IntExpr::Add(a, b) => format!("({} + {})", expr_to_string(a), expr_to_string(b)),
+        IntExpr::Sub(a, b) => format!("({} - {})", expr_to_string(a), expr_to_string(b)),
+        IntExpr::Mul(a, b) => format!("({} * {})", expr_to_string(a), expr_to_string(b)),
+        IntExpr::Neg(a) => format!("(-{})", expr_to_string(a)),
+    }
+}
+
+/// A Boolean formula that can be converted to Z3 constraints
+#[derive(Debug, Clone)]
+
+pub enum Formula {
+    // Boolean operations
+    And(Vec<Formula>),
+    Or(Vec<Formula>),
+    Not(Box<Formula>),
+    Implies(Box<Formula>, Box<Formula>),
+
+    // Comparisons
+    BoolVar(BoolVar),
+    IntEq(IntVar, i64),
+    IntNe(IntVar, i64),
+    IntLe(IntVar, i64),
+    IntLt(IntVar, i64),
+    IntGe(IntVar, i64),
+    IntGt(IntVar, i64),
+
+    // Expression comparisons (IntExpr to IntExpr)
+    ExprEq(IntExpr, IntExpr), // expr1 == expr2
+    ExprNe(IntExpr, IntExpr), // expr1 != expr2
+    ExprLe(IntExpr, IntExpr), // expr1 <= expr2
+    ExprLt(IntExpr, IntExpr), // expr1 < expr2
+    ExprGe(IntExpr, IntExpr), // expr1 >= expr2
+    ExprGt(IntExpr, IntExpr), // expr1 > expr2
+
+    // Pseudo-Boolean constraints
+    AtLeast(Vec<(i64, BoolVar)>, i64), // sum(weights * vars) >= threshold
+    AtMost(Vec<(i64, BoolVar)>, i64),  // sum(weights * vars) <= threshold
+    Exactly(Vec<(i64, BoolVar)>, i64), // sum(weights * vars) == threshold
+}
+
+impl Formula {
+    /// Create an AND formula
+    pub fn and(formulas: Vec<Formula>) -> Self {
+        Formula::And(formulas)
+    }
+
+    /// Create an OR formula
+    pub fn or(formulas: Vec<Formula>) -> Self {
+        Formula::Or(formulas)
+    }
+
+    /// Create a NOT formula
+    pub fn not(formula: Formula) -> Self {
+        Formula::Not(Box::new(formula))
+    }
+
+    /// Create an IMPLIES formula (a => b)
+    pub fn implies(premise: Formula, conclusion: Formula) -> Self {
+        Formula::Implies(Box::new(premise), Box::new(conclusion))
+    }
+
+    /// Create an "at least" pseudo-Boolean constraint
+    pub fn at_least(weighted_vars: Vec<(i64, BoolVar)>, threshold: i64) -> Self {
+        Formula::AtLeast(weighted_vars, threshold)
+    }
+
+    /// Create an "at most" pseudo-Boolean constraint
+    pub fn at_most(weighted_vars: Vec<(i64, BoolVar)>, threshold: i64) -> Self {
+        Formula::AtMost(weighted_vars, threshold)
+    }
+
+    /// Create an "exactly" pseudo-Boolean constraint
+    pub fn exactly(weighted_vars: Vec<(i64, BoolVar)>, threshold: i64) -> Self {
+        Formula::Exactly(weighted_vars, threshold)
+    }
+
+    /// Get a human-readable representation of the formula in DIMACS CNF-like format
+    pub fn to_string_representation(&self) -> String {
+        match self {
+            Formula::And(formulas) => {
+                let parts: Vec<String> = formulas
+                    .iter()
+                    .map(|f| f.to_string_representation())
+                    .collect();
+                format!("({})", parts.join(" AND "))
+            }
+            Formula::Or(formulas) => {
+                let parts: Vec<String> = formulas
+                    .iter()
+                    .map(|f| f.to_string_representation())
+                    .collect();
+                format!("({})", parts.join(" OR "))
+            }
+            Formula::Not(formula) => format!("NOT({})", formula.to_string_representation()),
+            Formula::Implies(premise, conclusion) => {
+                format!(
+                    "({} => {})",
+                    premise.to_string_representation(),
+                    conclusion.to_string_representation()
+                )
+            }
+            Formula::BoolVar(var) => var.get_name().to_string(),
+            Formula::IntEq(var, val) => format!("{} == {}", var.get_name(), val),
+            Formula::IntNe(var, val) => format!("{} != {}", var.get_name(), val),
+            Formula::IntLe(var, val) => format!("{} <= {}", var.get_name(), val),
+            Formula::IntLt(var, val) => format!("{} < {}", var.get_name(), val),
+            Formula::IntGe(var, val) => format!("{} >= {}", var.get_name(), val),
+            Formula::IntGt(var, val) => format!("{} > {}", var.get_name(), val),
+            Formula::ExprEq(expr1, expr2) => {
+                format!("{} == {}", expr_to_string(expr1), expr_to_string(expr2))
+            }
+            Formula::ExprNe(expr1, expr2) => {
+                format!("{} != {}", expr_to_string(expr1), expr_to_string(expr2))
+            }
+            Formula::ExprLe(expr1, expr2) => {
+                format!("{} <= {}", expr_to_string(expr1), expr_to_string(expr2))
+            }
+            Formula::ExprLt(expr1, expr2) => {
+                format!("{} < {}", expr_to_string(expr1), expr_to_string(expr2))
+            }
+            Formula::ExprGe(expr1, expr2) => {
+                format!("{} >= {}", expr_to_string(expr1), expr_to_string(expr2))
+            }
+            Formula::ExprGt(expr1, expr2) => {
+                format!("{} > {}", expr_to_string(expr1), expr_to_string(expr2))
+            }
+            Formula::AtLeast(weighted_vars, threshold) => {
+                let terms: Vec<String> = weighted_vars
+                    .iter()
+                    .map(|(w, v)| {
+                        if *w == 1 {
+                            v.get_name().to_string()
+                        } else {
+                            format!("{}*{}", w, v.get_name())
+                        }
+                    })
+                    .collect();
+                format!("({} >= {})", terms.join(" + "), threshold)
+            }
+            Formula::AtMost(weighted_vars, threshold) => {
+                let terms: Vec<String> = weighted_vars
+                    .iter()
+                    .map(|(w, v)| {
+                        if *w == 1 {
+                            v.get_name().to_string()
+                        } else {
+                            format!("{}*{}", w, v.get_name())
+                        }
+                    })
+                    .collect();
+                format!("({} <= {})", terms.join(" + "), threshold)
+            }
+            Formula::Exactly(weighted_vars, threshold) => {
+                let terms: Vec<String> = weighted_vars
+                    .iter()
+                    .map(|(w, v)| {
+                        if *w == 1 {
+                            v.get_name().to_string()
+                        } else {
+                            format!("{}*{}", w, v.get_name())
+                        }
+                    })
+                    .collect();
+                format!("({} == {})", terms.join(" + "), threshold)
+            }
+        }
+    }
+
+    /// Assert this formula to a Z3 solver (stub for now)
+    pub fn assert_to_solver(
+        &self,
+        _context: &z3::Context,
+        _solver: &z3::Solver,
+        _var_map: &HashMap<String, z3::ast::Bool>,
+    ) {
+        // This is a placeholder. The actual Z3 integration would go here.
+        // For now, users can use to_string_representation() to get a formula
+        // that can be converted to SMT-LIB format or similar.
+    }
+}
+
+impl fmt::Display for Formula {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{}", self.to_string_representation())
+    }
+}
+
+/// Builder for constructing SAT formulas
+pub struct FormulaBuilder {
+    constraints: Vec<Formula>,
+    bool_vars: HashMap<String, BoolVar>,
+    int_vars: HashMap<String, IntVar>,
+}
+
+impl FormulaBuilder {
+    pub fn new() -> Self {
+        Self {
+            constraints: Vec::new(),
+            bool_vars: HashMap::new(),
+            int_vars: HashMap::new(),
+        }
+    }
+
+    pub fn add_bool_var(&mut self, name: impl Into<String>) -> BoolVar {
+        let var = BoolVar::new(name);
+        self.bool_vars
+            .insert(var.get_name().to_string(), var.clone());
+        var
+    }
+
+    pub fn add_int_var(&mut self, name: impl Into<String>) -> IntVar {
+        let var = IntVar::new(name);
+        self.int_vars
+            .insert(var.get_name().to_string(), var.clone());
+        var
+    }
+
+    pub fn add_int_var_with_bounds(
+        &mut self,
+        name: impl Into<String>,
+        min: i64,
+        max: i64,
+    ) -> IntVar {
+        let var = IntVar::with_bounds(name, min, max);
+        self.int_vars
+            .insert(var.get_name().to_string(), var.clone());
+        var
+    }
+
+    pub fn add_constraint(&mut self, constraint: Formula) -> &mut Self {
+        self.constraints.push(constraint);
+        self
+    }
+
+    pub fn build(self) -> Formula {
+        if self.constraints.is_empty() {
+            Formula::And(vec![]) // Trivially true
+        } else if self.constraints.len() == 1 {
+            self.constraints.into_iter().next().unwrap()
+        } else {
+            Formula::And(self.constraints)
+        }
+    }
+
+    pub fn get_bool_vars(&self) -> &HashMap<String, BoolVar> {
+        &self.bool_vars
+    }
+
+    pub fn get_int_vars(&self) -> &HashMap<String, IntVar> {
+        &self.int_vars
+    }
+}
+
+impl Default for FormulaBuilder {
+    fn default() -> Self {
+        Self::new()
+    }
+}

src/logic/mod.rs

@@ -0,0 +1,2 @@
+pub mod formula;
+pub mod solver;

src/logic/solver.rs

@@ -0,0 +1,372 @@
+use crate::logic::formula::{Formula, FormulaBuilder, IntExpr, IntVar};
+use std::collections::HashMap;
+use z3::Solver;
+use z3::ast::Bool;
+
+/// A PB-SAT solver for aggregate placement and constraint satisfaction.
+/// Uses Z3 to solve pseudo-Boolean satisfiability problems for atom placement.
+pub struct PBSATSolver;
+
+/// Complete assignment from a Z3 solution including both booleans and integers
+#[derive(Debug, Clone)]
+pub struct Assignment {
+    pub booleans: HashMap<String, bool>,
+    pub integers: HashMap<String, i64>,
+}
+
+impl Assignment {
+    pub fn new() -> Self {
+        Self {
+            booleans: HashMap::new(),
+            integers: HashMap::new(),
+        }
+    }
+
+    pub fn get_bool(&self, name: &str) -> Option<bool> {
+        self.booleans.get(name).copied()
+    }
+
+    pub fn get_int(&self, name: &str) -> Option<i64> {
+        self.integers.get(name).copied()
+    }
+}
+
+impl PBSATSolver {
+    /// Create a new formula builder for constructing SAT formulas
+    pub fn create_formula_builder() -> FormulaBuilder {
+        FormulaBuilder::new()
+    }
+
+    /// Solve a formula using Z3 and return the complete satisfying assignment (booleans + integers)
+    pub fn solve_formula(formula: &Formula) -> Option<Assignment> {
+        // Extract all variables from the formula
+        let mut bool_vars = Vec::new();
+        let mut int_vars = Vec::new();
+        extract_bool_vars(formula, &mut bool_vars);
+        extract_int_vars(formula, &mut int_vars);
+        bool_vars.sort();
+        bool_vars.dedup();
+        int_vars.sort_by(|a, b| a.get_name().cmp(b.get_name()));
+        int_vars.dedup_by(|a, b| a.get_name() == b.get_name());
+
+        // Create solver with default context
+        let solver = Solver::new();
+
+        // Create Z3 Boolean variables
+        let mut bool_var_map: HashMap<String, Bool> = HashMap::new();
+        for var_name in &bool_vars {
+            let z3_var = Bool::fresh_const(var_name.as_str());
+            bool_var_map.insert(var_name.clone(), z3_var);
+        }
+
+        // Create Z3 Integer variables
+        let mut int_var_map: HashMap<String, z3::ast::Int> = HashMap::new();
+        for int_var in &int_vars {
+            let z3_var = z3::ast::Int::fresh_const(int_var.get_name());
+
+            // Add bounds constraints if specified
+            if let (Some(min), Some(max)) = int_var.get_bounds() {
+                let min_const = z3::ast::Int::from_i64(min);
+                let max_const = z3::ast::Int::from_i64(max);
+                solver.assert(&z3_var.ge(&min_const));
+                solver.assert(&z3_var.le(&max_const));
+            }
+
+            int_var_map.insert(int_var.get_name().to_string(), z3_var);
+        }
+
+        // Convert formula to Z3 and assert
+        if let Some(z3_formula) = formula_to_z3(formula, &bool_var_map, &int_var_map) {
+            solver.assert(&z3_formula);
+        }
+
+        // Check satisfiability
+        match solver.check() {
+            z3::SatResult::Sat => {
+                if let Some(model) = solver.get_model() {
+                    let mut assignment = Assignment::new();
+
+                    // Extract boolean assignments
+                    for var_name in &bool_vars {
+                        if let Some(z3_var) = bool_var_map.get(var_name) {
+                            if let Some(evaluated) = model.eval(z3_var, false) {
+                                if let Some(val_bool) = evaluated.as_bool() {
+                                    assignment.booleans.insert(var_name.clone(), val_bool);
+                                }
+                            }
+                        }
+                    }
+
+                    // Extract integer assignments
+                    for int_var in &int_vars {
+                        if let Some(z3_var) = int_var_map.get(int_var.get_name()) {
+                            if let Some(evaluated) = model.eval(z3_var, false) {
+                                if let Some(val_int) = evaluated.as_i64() {
+                                    assignment
+                                        .integers
+                                        .insert(int_var.get_name().to_string(), val_int);
+                                }
+                            }
+                        }
+                    }
+
+                    Some(assignment)
+                } else {
+                    None
+                }
+            }
+            _ => None,
+        }
+    }
+
+    /// Solve a formula using Z3 and return the satisfying assignment (legacy - returns only booleans)
+    pub fn solve_formula_with_z3(formula: &Formula) -> Option<HashMap<String, bool>> {
+        // Extract all variables from the formula
+        let mut bool_vars = Vec::new();
+        let mut int_vars = Vec::new();
+        extract_bool_vars(formula, &mut bool_vars);
+        extract_int_vars(formula, &mut int_vars);
+        bool_vars.sort();
+        bool_vars.dedup();
+        int_vars.sort_by(|a, b| a.get_name().cmp(b.get_name()));
+        int_vars.dedup_by(|a, b| a.get_name() == b.get_name());
+
+        // Create solver with default context
+        let solver = Solver::new();
+
+        // Create Z3 Boolean variables
+        let mut bool_var_map: HashMap<String, Bool> = HashMap::new();
+        for var_name in &bool_vars {
+            let z3_var = Bool::fresh_const(var_name.as_str());
+            bool_var_map.insert(var_name.clone(), z3_var);
+        }
+
+        // Create Z3 Integer variables
+        let mut int_var_map: HashMap<String, z3::ast::Int> = HashMap::new();
+        for int_var in &int_vars {
+            let z3_var = z3::ast::Int::fresh_const(int_var.get_name());
+
+            // Add bounds constraints if specified
+            if let (Some(min), Some(max)) = int_var.get_bounds() {
+                let min_const = z3::ast::Int::from_i64(min);
+                let max_const = z3::ast::Int::from_i64(max);
+                solver.assert(&z3_var.ge(&min_const));
+                solver.assert(&z3_var.le(&max_const));
+            }
+
+            int_var_map.insert(int_var.get_name().to_string(), z3_var);
+        }
+
+        // Convert formula to Z3 and assert
+        if let Some(z3_formula) = formula_to_z3(formula, &bool_var_map, &int_var_map) {
+            solver.assert(&z3_formula);
+        }
+
+        // Check satisfiability
+        match solver.check() {
+            z3::SatResult::Sat => {
+                if let Some(model) = solver.get_model() {
+                    let mut assignment = HashMap::new();
+
+                    // Extract the assignment from the model
+                    for var_name in &bool_vars {
+                        if let Some(z3_var) = bool_var_map.get(var_name) {
+                            if let Some(evaluated) = model.eval(z3_var, false) {
+                                if let Some(val_bool) = evaluated.as_bool() {
+                                    assignment.insert(var_name.clone(), val_bool);
+                                }
+                            }
+                        }
+                    }
+
+                    Some(assignment)
+                } else {
+                    None
+                }
+            }
+            _ => None,
+        }
+    }
+}
+
+/// Extract all boolean variables from a formula
+fn extract_bool_vars(formula: &Formula, vars: &mut Vec<String>) {
+    match formula {
+        Formula::And(formulas) | Formula::Or(formulas) => {
+            for f in formulas {
+                extract_bool_vars(f, vars);
+            }
+        }
+        Formula::Not(f) | Formula::Implies(f, _) => {
+            extract_bool_vars(f, vars);
+        }
+        Formula::BoolVar(var) => {
+            let name = var.get_name().to_string();
+            if !vars.contains(&name) {
+                vars.push(name);
+            }
+        }
+        _ => {}
+    }
+}
+
+/// Extract all integer variables from a formula
+fn extract_int_vars(formula: &Formula, vars: &mut Vec<IntVar>) {
+    match formula {
+        Formula::And(formulas) | Formula::Or(formulas) => {
+            for f in formulas {
+                extract_int_vars(f, vars);
+            }
+        }
+        Formula::Not(f) | Formula::Implies(f, _) => {
+            extract_int_vars(f, vars);
+        }
+        Formula::IntEq(var, _)
+        | Formula::IntNe(var, _)
+        | Formula::IntLe(var, _)
+        | Formula::IntLt(var, _)
+        | Formula::IntGe(var, _)
+        | Formula::IntGt(var, _) => {
+            if !vars.iter().any(|v| v.get_name() == var.get_name()) {
+                vars.push(var.clone());
+            }
+        }
+        _ => {}
+    }
+}
+
+/// Convert an IntExpr to a Z3 integer expression
+fn expr_to_z3(expr: &IntExpr, int_var_map: &HashMap<String, z3::ast::Int>) -> Option<z3::ast::Int> {
+    match expr {
+        IntExpr::Var(v) => int_var_map.get(v.get_name()).cloned(),
+        IntExpr::Const(c) => Some(z3::ast::Int::from_i64(*c)),
+        IntExpr::Add(a, b) => {
+            let z3_a = expr_to_z3(a, int_var_map)?;
+            let z3_b = expr_to_z3(b, int_var_map)?;
+            Some(z3::ast::Int::add(&[&z3_a, &z3_b]))
+        }
+        IntExpr::Sub(a, b) => {
+            let z3_a = expr_to_z3(a, int_var_map)?;
+            let z3_b = expr_to_z3(b, int_var_map)?;
+            Some(z3::ast::Int::sub(&[&z3_a, &z3_b]))
+        }
+        IntExpr::Mul(a, b) => {
+            let z3_a = expr_to_z3(a, int_var_map)?;
+            let z3_b = expr_to_z3(b, int_var_map)?;
+            Some(z3::ast::Int::mul(&[&z3_a, &z3_b]))
+        }
+        IntExpr::Neg(a) => {
+            let z3_a = expr_to_z3(a, int_var_map)?;
+            Some(z3::ast::Int::mul(&[&z3_a, &z3::ast::Int::from_i64(-1)]))
+        }
+    }
+}
+
+/// Convert a formula to Z3 AST
+fn formula_to_z3(
+    formula: &Formula,
+    bool_var_map: &HashMap<String, Bool>,
+    int_var_map: &HashMap<String, z3::ast::Int>,
+) -> Option<Bool> {
+    match formula {
+        Formula::And(formulas) => {
+            let z3_formulas: Vec<Bool> = formulas
+                .iter()
+                .filter_map(|f| formula_to_z3(f, bool_var_map, int_var_map))
+                .collect();
+            if z3_formulas.is_empty() {
+                Some(Bool::from_bool(true))
+            } else if z3_formulas.len() == 1 {
+                Some(z3_formulas[0].clone())
+            } else {
+                Some(Bool::and(&z3_formulas.iter().collect::<Vec<_>>()))
+            }
+        }
+        Formula::Or(formulas) => {
+            let z3_formulas: Vec<Bool> = formulas
+                .iter()
+                .filter_map(|f| formula_to_z3(f, bool_var_map, int_var_map))
+                .collect();
+            if z3_formulas.is_empty() {
+                Some(Bool::from_bool(false))
+            } else if z3_formulas.len() == 1 {
+                Some(z3_formulas[0].clone())
+            } else {
+                Some(Bool::or(&z3_formulas.iter().collect::<Vec<_>>()))
+            }
+        }
+        Formula::Not(f) => formula_to_z3(f, bool_var_map, int_var_map).map(|b| b.not()),
+        Formula::Implies(premise, conclusion) => {
+            let p = formula_to_z3(premise, bool_var_map, int_var_map)?;
+            let c = formula_to_z3(conclusion, bool_var_map, int_var_map)?;
+            Some(Bool::implies(&p, &c))
+        }
+        Formula::BoolVar(var) => bool_var_map.get(var.get_name()).cloned(),
+
+        // Integer comparisons
+        Formula::IntLt(var, value) => {
+            let z3_var = int_var_map.get(var.get_name())?;
+            let z3_val = z3::ast::Int::from_i64(*value);
+            Some(z3_var.lt(&z3_val))
+        }
+        Formula::IntLe(var, value) => {
+            let z3_var = int_var_map.get(var.get_name())?;
+            let z3_val = z3::ast::Int::from_i64(*value);
+            Some(z3_var.le(&z3_val))
+        }
+        Formula::IntGt(var, value) => {
+            let z3_var = int_var_map.get(var.get_name())?;
+            let z3_val = z3::ast::Int::from_i64(*value);
+            Some(z3_var.gt(&z3_val))
+        }
+        Formula::IntGe(var, value) => {
+            let z3_var = int_var_map.get(var.get_name())?;
+            let z3_val = z3::ast::Int::from_i64(*value);
+            Some(z3_var.ge(&z3_val))
+        }
+        Formula::IntEq(var, value) => {
+            let z3_var = int_var_map.get(var.get_name())?;
+            let z3_val = z3::ast::Int::from_i64(*value);
+            Some(z3_var.eq(&z3_val))
+        }
+        Formula::IntNe(var, value) => {
+            let z3_var = int_var_map.get(var.get_name())?;
+            let z3_val = z3::ast::Int::from_i64(*value);
+            Some(z3_var.eq(&z3_val).not())
+        }
+
+        // Expression comparisons
+        Formula::ExprEq(expr1, expr2) => {
+            let z3_expr1 = expr_to_z3(expr1, int_var_map)?;
+            let z3_expr2 = expr_to_z3(expr2, int_var_map)?;
+            Some(z3_expr1.eq(&z3_expr2))
+        }
+        Formula::ExprNe(expr1, expr2) => {
+            let z3_expr1 = expr_to_z3(expr1, int_var_map)?;
+            let z3_expr2 = expr_to_z3(expr2, int_var_map)?;
+            Some(z3_expr1.eq(&z3_expr2).not())
+        }
+        Formula::ExprLe(expr1, expr2) => {
+            let z3_expr1 = expr_to_z3(expr1, int_var_map)?;
+            let z3_expr2 = expr_to_z3(expr2, int_var_map)?;
+            Some(z3_expr1.le(&z3_expr2))
+        }
+        Formula::ExprLt(expr1, expr2) => {
+            let z3_expr1 = expr_to_z3(expr1, int_var_map)?;
+            let z3_expr2 = expr_to_z3(expr2, int_var_map)?;
+            Some(z3_expr1.lt(&z3_expr2))
+        }
+        Formula::ExprGe(expr1, expr2) => {
+            let z3_expr1 = expr_to_z3(expr1, int_var_map)?;
+            let z3_expr2 = expr_to_z3(expr2, int_var_map)?;
+            Some(z3_expr1.ge(&z3_expr2))
+        }
+        Formula::ExprGt(expr1, expr2) => {
+            let z3_expr1 = expr_to_z3(expr1, int_var_map)?;
+            let z3_expr2 = expr_to_z3(expr2, int_var_map)?;
+            Some(z3_expr1.gt(&z3_expr2))
+        }
+
+        _ => None, // Unsupported for now (AtLeast, AtMost, Exactly)
+    }
+}

src/main.rs

@@ -0,0 +1,10 @@
+extern crate kiss3d;
+
+pub mod adjacency;
+pub mod geometry;
+pub mod logic;
+pub mod placements;
+pub mod render;
+
+#[kiss3d::main]
+async fn main() {}

src/placements/mod.rs

@@ -0,0 +1,2 @@
+pub mod placement_enum;
+pub mod placement_instance;

src/placements/placement_instance.rs

@@ -0,0 +1,5 @@
+use kiss3d::nalgebra::Rotation3;
+
+struct Orientation {
+    rotation: Rotation3<f32>,
+}

src/render/mod.rs

@@ -0,0 +1,114 @@
+use kiss3d::{
+    camera::{Camera, FirstPerson},
+    event::{Action, Key, WindowEvent},
+    light::Light,
+    nalgebra::Point3,
+    window::Window,
+};
+
+pub mod mesh_gen;
+
+pub struct Renderer {
+    window: Window,
+    at: Point3<f32>,
+    eye: Point3<f32>,
+    first_person: FirstPerson,
+}
+
+impl Renderer {
+    pub fn new() -> Self {
+        let mut window = Window::new("PB-SAT PGC - Heterogeneous Polyhedral Units");
+        window.set_light(Light::StickToCamera);
+
+        let at = Point3::new(0.0f32, 0.0, 0.0);
+        let eye = Point3::new(20.0f32, 15.0, 20.0);
+        let mut first_person = FirstPerson::new(eye, at);
+        first_person.rebind_up_key(Some(Key::W));
+        first_person.rebind_left_key(Some(Key::A));
+        first_person.rebind_down_key(Some(Key::S));
+        first_person.rebind_right_key(Some(Key::D));
+        first_person.set_move_step(0.1);
+
+        println!("\n--- RENDERING CONTROLS ---");
+        println!("WASD: Move camera");
+        println!("Mouse: Look around");
+        println!("C: Rotate camera down");
+        println!("Shift: Rotate camera up");
+
+        Self {
+            window,
+            at,
+            eye,
+            first_person,
+        }
+    }
+
+    pub fn get_window(&mut self) -> &Window {
+        return &self.window;
+    }
+
+    pub fn get_window_mut(&mut self) -> &mut Window {
+        return &mut self.window;
+    }
+
+    pub async fn render(&mut self) {
+        while !self.window.should_close() {
+            for event in self.window.events().iter() {
+                match event.value {
+                    WindowEvent::Key(key, Action::Press, _) => match key {
+                        Key::C => {
+                            let eye = self.eye;
+                            // Convert to spherical coordinates
+                            let dx = eye.x - self.at.x;
+                            let dy = eye.y - self.at.y;
+                            let dz = eye.z - self.at.z;
+
+                            let r = (dx * dx + dy * dy + dz * dz).sqrt();
+                            let mut theta = dy.atan2((dx * dx + dz * dz).sqrt());
+                            let phi = dz.atan2(dx);
+
+                            // Rotate down (decrease theta)
+                            theta -= 0.1;
+
+                            // Convert back to Cartesian
+                            let new_eye = Point3::new(
+                                self.at.x + r * theta.cos() * phi.cos(),
+                                self.at.y + r * theta.sin(),
+                                self.at.z + r * theta.cos() * phi.sin(),
+                            );
+                            self.first_person.look_at(new_eye, self.at);
+                        }
+                        Key::LShift => {
+                            let eye = self.first_person.eye();
+                            // Convert to spherical coordinates
+                            let dx = eye.x - self.at.x;
+                            let dy = eye.y - self.at.y;
+                            let dz = eye.z - self.at.z;
+
+                            let r = (dx * dx + dy * dy + dz * dz).sqrt();
+                            let mut theta = dy.atan2((dx * dx + dz * dz).sqrt());
+                            let phi = dz.atan2(dx);
+
+                            // Rotate up (increase theta)
+                            theta += 0.1;
+
+                            // Convert back to Cartesian
+                            let new_eye = Point3::new(
+                                self.at.x + r * theta.cos() * phi.cos(),
+                                self.at.y + r * theta.sin(),
+                                self.at.z + r * theta.cos() * phi.sin(),
+                            );
+                            self.first_person.look_at(new_eye, self.at);
+                        }
+                        _ => {}
+                    },
+                    _ => {}
+                }
+            }
+
+            self.first_person.look_at(self.first_person.eye(), self.at);
+
+            self.window.render_with_camera(&mut self.first_person).await;
+        }
+    }
+}