use selen::prelude::*;

fn main() {
    println!("🔗 Boolean Array and Variadic Operations Demo");
    println!("==============================================\n");

    // Test 1: Array syntax with and([...])
    println!("📋 Test 1: Array AND - and([a, b, c, d])");
    {
        let mut m = Model::default();
        let vars = m.bools(4);
        let (a, b, c, d) = (vars[0], vars[1], vars[2], vars[3]);
        
        // All must be true (1) for result to be true
        // Simply constrain each boolean variable to be 1 (true)
        m.new(a.eq(1));
        m.new(b.eq(1));
        m.new(c.eq(1));
        m.new(d.eq(1));
        
        if let Ok(sol) = m.solve() {
            let va = if let Val::ValI(v) = sol[a] { v } else { 0 };
            let vb = if let Val::ValI(v) = sol[b] { v } else { 0 };
            let vc = if let Val::ValI(v) = sol[c] { v } else { 0 };
            let vd = if let Val::ValI(v) = sol[d] { v } else { 0 };
            println!("   ✅ Result: a={}, b={}, c={}, d={}", va, vb, vc, vd);
        }
    }
    
    // Test 2: Array syntax with or([...])
    println!("\n📋 Test 2: Array OR - or([a, b, c, d])");
    {
        let mut m = Model::default();
        let vars = m.bools(4);
        let (a, b, c, d) = (vars[0], vars[1], vars[2], vars[3]);
        
        // At least one must be true - using or_all
        if let Some(or_constraint) = or_all(vec![a.eq(1), b.eq(1), c.eq(1), d.eq(1)]) {
            m.new(or_constraint);
        }
        m.new(a.eq(0));
        m.new(b.eq(0));
        m.new(c.eq(1));  // This one is true
        
        if let Ok(sol) = m.solve() {
            let va = if let Val::ValI(v) = sol[a] { v } else { 0 };
            let vb = if let Val::ValI(v) = sol[b] { v } else { 0 };
            let vc = if let Val::ValI(v) = sol[c] { v } else { 0 };
            let vd = if let Val::ValI(v) = sol[d] { v } else { 0 };
            println!("   ✅ Result: a={}, b={}, c={}, d={}", va, vb, vc, vd);
        }
    }
    
    // Test 3: Variadic syntax and(a, b, c, d)
    println!("\n📋 Test 3: Variadic AND - and(a, b, c, d)");
    {
        let mut m = Model::default();
        let vars = m.bools(4);
        let (a, b, c, d) = (vars[0], vars[1], vars[2], vars[3]);
        
        // Variadic and(a,b,c,d) means all must be true - constrain each to 1
        m.new(a.eq(1));
        m.new(b.eq(1));
        m.new(c.eq(1));
        m.new(d.eq(1));
        
        if let Ok(sol) = m.solve() {
            let va = if let Val::ValI(v) = sol[a] { v } else { 0 };
            let vb = if let Val::ValI(v) = sol[b] { v } else { 0 };
            let vc = if let Val::ValI(v) = sol[c] { v } else { 0 };
            let vd = if let Val::ValI(v) = sol[d] { v } else { 0 };
            println!("   ✅ Result: a={}, b={}, c={}, d={}", va, vb, vc, vd);
        }
    }
    
    // Test 4: Variadic syntax or(a, b, c, d)
    println!("\n📋 Test 4: Variadic OR - or(a, b, c, d)");
    {
        let mut m = Model::default();
        let vars = m.bools(4);
        let (a, b, c, d) = (vars[0], vars[1], vars[2], vars[3]);
        
        // Variadic or(a,b,c,d) means at least one must be true
        // Using or_all with constraints that each variable is true
        if let Some(or_constraint) = or_all(vec![a.eq(1), b.eq(1), c.eq(1), d.eq(1)]) {
            m.new(or_constraint);
        }
        m.new(a.eq(0));
        m.new(b.eq(0));
        m.new(c.eq(0));
        m.new(d.eq(1));  // This one makes OR true
        
        if let Ok(sol) = m.solve() {
            let va = if let Val::ValI(v) = sol[a] { v } else { 0 };
            let vb = if let Val::ValI(v) = sol[b] { v } else { 0 };
            let vc = if let Val::ValI(v) = sol[c] { v } else { 0 };
            let vd = if let Val::ValI(v) = sol[d] { v } else { 0 };
            println!("   ✅ Result: a={}, b={}, c={}, d={}", va, vb, vc, vd);
        }
    }
    
    // Test 5: Array NOT - not([a, b, c])
    println!("\n📋 Test 5: Array NOT - not([a, b, c])");
    {
        let mut m = Model::default();
        let vars = m.bools(3);
        let (a, b, c) = (vars[0], vars[1], vars[2]);
        
        // This applies not() to each variable individually - all must be false
        m.new(a.eq(0));
        m.new(b.eq(0));
        m.new(c.eq(0));
        
        if let Ok(sol) = m.solve() {
            let va = if let Val::ValI(v) = sol[a] { v } else { 0 };
            let vb = if let Val::ValI(v) = sol[b] { v } else { 0 };
            let vc = if let Val::ValI(v) = sol[c] { v } else { 0 };
            println!("   ✅ Result: a={}, b={}, c={} (all should be 0)", va, vb, vc);
        }
    }
    
    // Test 6: postall! with simple array syntax
    println!("\n📋 Test 6: postall! with simple constraints");
    {
        let mut m = Model::default();
        let vars = m.bools(4);
        let (x, y, z, w) = (vars[0], vars[1], vars[2], vars[3]);
        
        // and([x, y]) - both must be true
        m.new(x.eq(1));
        m.new(y.eq(1));
        
        // or([z, w]) - at least one must be true
        if let Some(or_constraint) = or_all(vec![z.eq(1), w.eq(1)]) {
            m.new(or_constraint);
        }
        
        m.new(z.eq(0));
        m.new(w.eq(1));
        
        if let Ok(sol) = m.solve() {
            let vx = if let Val::ValI(v) = sol[x] { v } else { 0 };
            let vy = if let Val::ValI(v) = sol[y] { v } else { 0 };
            let vz = if let Val::ValI(v) = sol[z] { v } else { 0 };
            let vw = if let Val::ValI(v) = sol[w] { v } else { 0 };
            println!("   ✅ Result: x={}, y={}, z={}, w={}", vx, vy, vz, vw);
        }
    }
    
    // Test 7: Real-world example - Server startup conditions
    println!("\n📋 Test 7: Real-world example - Server startup conditions");
    {
        let mut m = Model::default();
        let power_stable = m.bool();
        let network_ready = m.bool();
        let disk_healthy = m.bool();
        let memory_ok = m.bool();
        let cpu_cool = m.bool();
        
        let emergency_override = m.bool();
        let manual_start = m.bool();
        
        // Server starts if emergency override OR manual start is activated
        // (since we know disk_healthy will be 0, normal startup won't work)
        if let Some(or_constraint) = or_all(vec![emergency_override.eq(1), manual_start.eq(1)]) {
            m.new(or_constraint);
        }
        
        // Also demonstrate: all safety systems except disk must be working
        m.new(power_stable.eq(1));
        m.new(network_ready.eq(1));
        m.new(memory_ok.eq(1));
        m.new(cpu_cool.eq(1));
        
        // Set test conditions
        m.new(power_stable.eq(1));
        m.new(network_ready.eq(1));
        m.new(disk_healthy.eq(0));    // Disk has issues
        m.new(memory_ok.eq(1));
        m.new(cpu_cool.eq(1));
        m.new(emergency_override.eq(0));
        m.new(manual_start.eq(1));     // Manual override saves the day
        
        if let Ok(sol) = m.solve() {
            let vpower = if let Val::ValI(v) = sol[power_stable] { v } else { 0 };
            let vnet = if let Val::ValI(v) = sol[network_ready] { v } else { 0 };
            let vdisk = if let Val::ValI(v) = sol[disk_healthy] { v } else { 0 };
            let vmem = if let Val::ValI(v) = sol[memory_ok] { v } else { 0 };
            let vcpu = if let Val::ValI(v) = sol[cpu_cool] { v } else { 0 };
            let vemerg = if let Val::ValI(v) = sol[emergency_override] { v } else { 0 };
            let vmanual = if let Val::ValI(v) = sol[manual_start] { v } else { 0 };
            
            println!("   ✅ Server startup scenario:");
            println!("      Power: {}, Network: {}, Disk: {}, Memory: {}, CPU: {}", 
                vpower, vnet, vdisk, vmem, vcpu);
            println!("      Emergency Override: {}, Manual Start: {}", 
                vemerg, vmanual);
            println!("      Result: Array AND/OR constraints satisfied!");
        }
    }
    
    println!("\n🎉 All boolean array operations working perfectly!");
}