pldag 4.2.2

#[cfg(feature = "glpk")]
mod glpk_tests {
    use pldag::{Bound, Pldag};
    use std::collections::HashMap;

    #[test]
    fn or_three_vars_is_feasible() {
        //   x ∨ y ∨ z  with all vars boolean
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        let _root = dag.set_or(vec!["x", "y", "z"]).unwrap();

        let objective = HashMap::<&str, f64>::new(); // dummy objective
        let mut assume = HashMap::<&str, Bound>::new(); // no fixed vars
        assume.insert(_root.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "model should be feasible");
        assert!(
            *solns[0].as_ref().unwrap().get(&_root).unwrap() == (1, 1),
            "solution should be (1,1) for root node"
        );
    }

    #[test]
    fn and_constraint_all_true() {
        // x ∧ y ∧ z with all vars true
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        let and_node = dag.set_and(vec!["x", "y", "z"]).unwrap();

        let objective = HashMap::<&str, f64>::from_iter(vec![("x", 1.0), ("y", 1.0), ("z", 1.0)]);
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(and_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "AND with all true should be feasible");
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get("x").unwrap(), (1, 1));
        assert_eq!(*soln.get("y").unwrap(), (1, 1));
        assert_eq!(*soln.get("z").unwrap(), (1, 1));
    }

    #[test]
    fn and_constraint_mixed_infeasible() {
        // x ∧ y ∧ z with x=1, y=1, z=0 should make AND=0, but we require AND=1
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        let and_node = dag.set_and(vec!["x", "y", "z"]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (1, 1));
        assume.insert("z", (0, 0));
        assume.insert(and_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "AND with mixed values should be infeasible when requiring AND=1"
        );
    }

    #[test]
    fn not_constraint() {
        // ¬x with x boolean
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        let not_node = dag.set_not(vec!["x"]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(not_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "NOT constraint should be feasible");
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get("x").unwrap(), (0, 0));
        assert_eq!(*soln.get(not_node.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn xor_constraint_exactly_one() {
        // x ⊕ y ⊕ z with exactly one true
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        let xor_node = dag.set_xor(vec!["x", "y", "z"]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(xor_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "XOR constraint should be feasible");
        let soln = solns[0].as_ref().unwrap();

        // Count how many variables are true
        let x_val = soln.get("x").unwrap().0;
        let y_val = soln.get("y").unwrap().0;
        let z_val = soln.get("z").unwrap().0;
        assert_eq!(
            x_val + y_val + z_val,
            1,
            "XOR should have exactly one true variable"
        );
    }

    #[test]
    fn nand_constraint() {
        // ¬(x ∧ y) - not all can be true
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let nand_node = dag.set_nand(vec!["x", "y"]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(nand_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "NAND constraint should be feasible");
        let soln = solns[0].as_ref().unwrap();

        let x_val = soln.get("x").unwrap().0;
        let y_val = soln.get("y").unwrap().0;
        assert!(
            !(x_val == 1 && y_val == 1),
            "NAND should not allow both variables to be true"
        );
    }

    #[test]
    fn nor_constraint() {
        // ¬(x ∨ y) - none can be true
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let nor_node = dag.set_nor(vec!["x", "y"]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(nor_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "NOR constraint should be feasible");
        let soln = solns[0].as_ref().unwrap();

        assert_eq!(*soln.get("x").unwrap(), (0, 0));
        assert_eq!(*soln.get("y").unwrap(), (0, 0));
    }

    #[test]
    fn xnor_constraint() {
        // x ⊙ y - either both true or both false
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let xnor_node = dag.set_xnor(vec!["x", "y"]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(xnor_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "XNOR constraint should be feasible");
        let soln = solns[0].as_ref().unwrap();

        let x_val = soln.get("x").unwrap().0;
        let y_val = soln.get("y").unwrap().0;
        assert_eq!(x_val, y_val, "XNOR should have both variables equal");
    }

    #[test]
    fn implication_true_true() {
        // x → y with x=1, y=1 should be true
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let imply_node = dag.set_imply("x", "y").unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (1, 1));
        assume.insert(imply_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Implication x=1, y=1 should be feasible"
        );
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(imply_node.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn implication_true_false_infeasible() {
        // x → y with x=1, y=0 should be false, but we require implication=1
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let imply_node = dag.set_imply("x", "y").unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (0, 0));
        assume.insert(imply_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "Implication x=1, y=0 should be infeasible when requiring implication=1"
        );
    }

    #[test]
    fn implication_false_any() {
        // x → y with x=0, y=any should be true
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let imply_node = dag.set_imply("x", "y").unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (0, 0));
        assume.insert(imply_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Implication x=0, y=any should be feasible"
        );
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(imply_node.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn equivalence_both_true() {
        // x ↔ y with both true
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let equiv_node = dag.set_equiv("x", "y").unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (1, 1));
        assume.insert(equiv_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Equivalence x=1, y=1 should be feasible"
        );
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(equiv_node.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn equivalence_both_false() {
        // x ↔ y with both false
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let equiv_node = dag.set_equiv("x", "y").unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (0, 0));
        assume.insert("y", (0, 0));
        assume.insert(equiv_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Equivalence x=0, y=0 should be feasible"
        );
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(equiv_node.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn equivalence_different_infeasible() {
        // x ↔ y with x=1, y=0 should be false, but we require equivalence=1
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let equiv_node = dag.set_equiv("x", "y").unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (0, 0));
        assume.insert(equiv_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "Equivalence x=1, y=0 should be infeasible when requiring equivalence=1"
        );
    }

    #[test]
    fn atleast_constraint_satisfied() {
        // x + y + z >= 2 with x=1, y=1, z=0
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        let atleast_node = dag.set_atleast(vec!["x", "y", "z"], 2).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (1, 1));
        assume.insert("z", (0, 0));
        assume.insert(atleast_node.as_str(), (0, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "At least 2 constraint should be satisfied"
        );
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(atleast_node.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn atleast_constraint_not_satisfied() {
        // x + y + z >= 2 with x=1, y=0, z=0, but we require atleast=1
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        let atleast_node = dag.set_atleast(vec!["x", "y", "z"], 2).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (0, 0));
        assume.insert("z", (0, 0));
        assume.insert(atleast_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "At least 2 constraint should not be satisfied with only 1 variable"
        );
    }

    #[test]
    fn atmost_constraint_satisfied() {
        // x + y + z <= 2 with x=1, y=1, z=0
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        let atmost_node = dag.set_atmost(vec!["x", "y", "z"], 2).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (1, 1));
        assume.insert("z", (0, 0));
        assume.insert(atmost_node.as_str(), (0, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "At most 2 constraint should be satisfied"
        );
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(atmost_node.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn atmost_constraint_not_satisfied() {
        // x + y + z <= 1 with x=1, y=1, z=0, but we require atmost=1
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        let atmost_node = dag.set_atmost(vec!["x", "y", "z"], 1).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (1, 1));
        assume.insert("z", (0, 0));
        assume.insert(atmost_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "At most 1 constraint should not be satisfied with 2 variables"
        );
    }

    #[test]
    fn equal_constraint_satisfied() {
        // x + y + z = 2 with x=1, y=1, z=0
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        let equal_node = dag.set_equal(vec!["x", "y", "z"], 2).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (1, 1));
        assume.insert("z", (0, 0));
        assume.insert(equal_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Equal 2 constraint should be satisfied");
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(equal_node.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn equal_constraint_not_satisfied() {
        // x + y + z = 2 with x=1, y=0, z=0, but we require equal=1
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        let equal_node = dag.set_equal(vec!["x", "y", "z"], 2).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (0, 0));
        assume.insert("z", (0, 0));
        assume.insert(equal_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "Equal 2 constraint should not be satisfied with sum=1"
        );
    }

    #[test]
    fn general_linear_inequality() {
        // 2x + 3y - z >= 4 (represented as 2x + 3y - z - 4 >= 0)
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 5));
        dag.set_primitive("y", (0, 5));
        dag.set_primitive("z", (0, 5));
        let gelineq_node = dag.set_gelineq(vec![("x", 2), ("y", 3), ("z", -1)], -4).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (2, 2));
        assume.insert("y", (1, 1));
        assume.insert("z", (0, 0));
        assume.insert(gelineq_node.as_str(), (1, 1));
        // 2*2 + 3*1 - 0 = 7 >= 4, so constraint should be satisfied

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "General linear inequality should be satisfied"
        );
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(gelineq_node.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn general_linear_inequality_not_satisfied() {
        // 2x + 3y - z >= 4 with x=1, y=0, z=0, but we require gelineq=1
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 5));
        dag.set_primitive("y", (0, 5));
        dag.set_primitive("z", (0, 5));
        let gelineq_node = dag.set_gelineq(vec![("x", 2), ("y", 3), ("z", -1)], -4).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (0, 0));
        assume.insert("z", (0, 0));
        assume.insert(gelineq_node.as_str(), (1, 1));
        // 2*1 + 3*0 - 0 = 2 < 4, so constraint should not be satisfied

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "General linear inequality should not be satisfied when sum < threshold"
        );
    }

    #[test]
    fn nested_logical_structure() {
        // (x ∧ y) ∨ (z ∧ w) - complex nested structure
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        dag.set_primitive("w", (0, 1));

        let and1 = dag.set_and(vec!["x", "y"]).unwrap();
        let and2 = dag.set_and(vec!["z", "w"]).unwrap();
        let or_root = dag.set_or(vec![and1, and2]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (0, 0));
        assume.insert("y", (1, 1));
        assume.insert("z", (1, 1));
        assume.insert("w", (1, 1));
        assume.insert(or_root.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Nested structure should be feasible when second branch is true"
        );
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(or_root.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn mixed_constraint_types() {
        // Combine logical and linear constraints: (x ∧ y) → (a + b + c >= 2)
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("a", (0, 1));
        dag.set_primitive("b", (0, 1));
        dag.set_primitive("c", (0, 1));

        let and_node = dag.set_and(vec!["x", "y"]).unwrap();
        let atleast_node = dag.set_atleast(vec!["a", "b", "c"], 2).unwrap();
        let imply_node = dag.set_imply(and_node, atleast_node).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (1, 1));
        assume.insert("a", (1, 1));
        assume.insert("b", (1, 1));
        assume.insert("c", (0, 0));
        assume.insert(imply_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Mixed constraint should be feasible");
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(imply_node.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn deep_nesting_levels() {
        // Deep nesting: x ∧ (y ∨ (z ∧ (w ∨ v)))
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        dag.set_primitive("w", (0, 1));
        dag.set_primitive("v", (0, 1));

        let or_inner = dag.set_or(vec!["w", "v"]).unwrap();
        let and_inner = dag.set_and(vec!["z".to_string(), or_inner]).unwrap();
        let or_middle = dag.set_or(vec!["y".to_string(), and_inner]).unwrap();
        let and_root = dag.set_and(vec!["x".to_string(), or_middle]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (0, 0));
        assume.insert("z", (1, 1));
        assume.insert("w", (0, 0));
        assume.insert("v", (1, 1));
        assume.insert(and_root.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Deep nesting should be feasible");
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(and_root.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn circular_dependency_prevention() {
        // Test that the DAG prevents circular dependencies through proper construction
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));

        let and_node = dag.set_and(vec!["x", "y"]).unwrap();
        let or_node = dag.set_or(vec![and_node.clone(), "x".to_string()]).unwrap();

        // This should work fine - no circular dependency
        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (0, 0));
        assume.insert(or_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Valid DAG structure should be feasible");
    }

    #[test]
    fn multiple_references_to_same_node() {
        // Test referencing the same intermediate node multiple times
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));

        let and_node = dag.set_and(vec!["x", "y"]).unwrap();
        let or_node1 = dag.set_or(vec![and_node.clone(), "z".to_string()]).unwrap();
        let or_node2 = dag.set_or(vec![and_node.clone(), "x".to_string()]).unwrap();
        let final_and = dag.set_and(vec![or_node1, or_node2]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert("y", (1, 1));
        assume.insert("z", (0, 0));
        assume.insert(final_and.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Multiple references to same node should work"
        );
        let soln = solns[0].as_ref().unwrap();
        assert_eq!(*soln.get(final_and.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn optimization_maximize_single_variable() {
        // Maximize x subject to x + y <= 3
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 5));
        dag.set_primitive("y", (0, 5));
        let atmost_node = dag.set_atmost(vec!["x", "y"], 3).unwrap();

        let mut objective = HashMap::<&str, f64>::new();
        objective.insert("x", 1.0);

        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(atmost_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Optimization should be feasible");
        let soln = solns[0].as_ref().unwrap();

        // Should maximize x while keeping x + y <= 3
        let x_val = soln.get("x").unwrap().0;
        let y_val = soln.get("y").unwrap().0;
        assert!(x_val + y_val <= 3, "Constraint should be satisfied");
        assert!(x_val >= 0, "x should be maximized subject to constraints");
    }

    #[test]
    fn optimization_minimize_objective() {
        // Minimize 2x + 3y subject to x + y >= 2
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 5));
        dag.set_primitive("y", (0, 5));
        let atleast_node = dag.set_atleast(vec!["x", "y"], 2).unwrap();

        let mut objective = HashMap::<&str, f64>::new();
        objective.insert("x", 2.0);
        objective.insert("y", 3.0);

        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(atleast_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, false).unwrap(); // minimiz.unwrap()e
        assert!(solns[0].is_some(), "Minimization should be feasible");
        let soln = solns[0].as_ref().unwrap();

        let x_val = soln.get("x").unwrap().0;
        let y_val = soln.get("y").unwrap().0;
        assert!(x_val + y_val >= 2, "Constraint should be satisfied");

        // Should minimize 2x + 3y, so prefer x over y
        let objective_value = 2 * x_val + 3 * y_val;
        assert!(
            objective_value >= 4,
            "Minimum objective should be at least 4"
        );
    }

    #[test]
    fn optimization_multiple_objectives() {
        // Test with multiple different objectives
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 2));
        dag.set_primitive("y", (0, 2));
        dag.set_primitive("z", (0, 2));
        let equal_node = dag.set_equal(vec!["x", "y", "z"], 2).unwrap();

        let mut obj1 = HashMap::<&str, f64>::new();
        obj1.insert("x", 1.0);

        let mut obj2 = HashMap::<&str, f64>::new();
        obj2.insert("y", 2.0);

        let mut obj3 = HashMap::<&str, f64>::new();
        obj3.insert("z", 3.0);

        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(equal_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![obj1, obj2, obj3], assume, true).unwrap();
        assert!(solns[0].is_some(), "First objective should be feasible");
        assert!(solns[1].is_some(), "Second objective should be feasible");
        assert!(solns[2].is_some(), "Third objective should be feasible");

        // All should satisfy x + y + z = 2
        for soln in solns.iter().flatten() {
            let x_val = soln.get("x").unwrap().0;
            let y_val = soln.get("y").unwrap().0;
            let z_val = soln.get("z").unwrap().0;
            assert_eq!(
                x_val + y_val + z_val,
                2,
                "All solutions should satisfy constraint"
            );
        }
    }

    #[test]
    fn optimization_with_logical_constraints() {
        // Maximize x + y subject to x ∧ y → (z ∨ w)
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        dag.set_primitive("w", (0, 1));

        let and_node = dag.set_and(vec!["x", "y"]).unwrap();
        let or_node = dag.set_or(vec!["z", "w"]).unwrap();
        let imply_node = dag.set_imply(and_node, or_node).unwrap();

        let mut objective = HashMap::<&str, f64>::new();
        objective.insert("x", 1.0);
        objective.insert("y", 1.0);

        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(imply_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Optimization with logical constraints should be feasible"
        );
        let soln = solns[0].as_ref().unwrap();

        let x_val = soln.get("x").unwrap().0;
        let y_val = soln.get("y").unwrap().0;
        let z_val = soln.get("z").unwrap().0;
        let w_val = soln.get("w").unwrap().0;

        // If x=1 and y=1, then z ∨ w must be true
        if x_val == 1 && y_val == 1 {
            assert!(
                z_val == 1 || w_val == 1,
                "Implication constraint should be satisfied"
            );
        }
    }

    #[test]
    fn optimization_with_coefficients() {
        // Test optimization using coefficients in objective
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 5));
        dag.set_primitive("y", (0, 5));

        let atmost_node = dag.set_atmost(vec!["x", "y"], 4).unwrap();

        let mut objective = HashMap::<&str, f64>::new();
        objective.insert("x", 2.5);
        objective.insert("y", 1.5);

        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(atmost_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Optimization with coefficients should be feasible"
        );
        let soln = solns[0].as_ref().unwrap();

        let x_val = soln.get("x").unwrap().0;
        let y_val = soln.get("y").unwrap().0;
        assert!(x_val + y_val <= 4, "Constraint should be satisfied");

        // Should prefer x since it has higher coefficient
        let objective_value = 2.5 * (x_val as f64) + 1.5 * (y_val as f64);
        assert!(objective_value >= 0.0, "Objective should be non-negative");
    }

    #[test]
    fn infeasible_contradictory_constraints() {
        // Create a real contradiction: x = 1 AND x = 0 using constraint nodes
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));

        // Create two equal constraints: x = 1 and x = 0
        let eq1 = dag.set_equal(vec!["x"], 1).unwrap(); // x = 1
        let eq2 = dag.set_equal(vec!["x"], 0).unwrap(); // x = 0
        let both = dag.set_and(vec![eq1, eq2]).unwrap(); // Both must be true (contradiction)

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(both.as_str(), (1, 1)); // Require both constraints to be satisfied

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "Contradictory constraints should be infeasible"
        );
    }

    #[test]
    fn infeasible_impossible_linear_constraint() {
        // x + y = 5 with x, y ∈ [0, 1]
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let equal_node = dag.set_equal(vec!["x", "y"], 5).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(equal_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "Impossible linear constraint should be infeasible"
        );
    }

    #[test]
    fn infeasible_logical_contradiction() {
        // x ∧ ¬x should be false
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        let not_node = dag.set_not(vec!["x"]).unwrap();
        let and_node = dag.set_and(vec!["x".to_string(), not_node]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(and_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "Logical contradiction should be infeasible"
        );
    }

    #[test]
    fn infeasible_conflicting_implications() {
        // x → y and x → ¬y with x = 1
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        let not_y = dag.set_not(vec!["y"]).unwrap();
        let imply1 = dag.set_imply("x", "y").unwrap();
        let imply2 = dag.set_imply("x", not_y).unwrap();
        let and_node = dag.set_and(vec![imply1, imply2]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert(and_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "Conflicting implications should be infeasible"
        );
    }

    #[test]
    fn infeasible_over_constrained_system() {
        // x + y = 2, x + y = 3, x ≥ 0, y ≥ 0
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 5));
        dag.set_primitive("y", (0, 5));
        let equal1 = dag.set_equal(vec!["x", "y"], 2).unwrap();
        let equal2 = dag.set_equal(vec!["x", "y"], 3).unwrap();
        let and_node = dag.set_and(vec![equal1, equal2]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(and_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "Over-constrained system should be infeasible"
        );
    }

    #[test]
    fn infeasible_boundary_violation() {
        // x ∈ [0, 1] but require x = 2
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (2, 2));

        let result = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true);
        assert!(
            result.is_err(),
            "Boundary violation should result in an error"
        );
    }

    #[test]
    fn infeasible_complex_nested_contradiction() {
        // (x ∧ y) ∨ (z ∧ w) = 1, but x=0, y=0, z=0, w=0
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        dag.set_primitive("y", (0, 1));
        dag.set_primitive("z", (0, 1));
        dag.set_primitive("w", (0, 1));

        let and1 = dag.set_and(vec!["x", "y"]).unwrap();
        let and2 = dag.set_and(vec!["z", "w"]).unwrap();
        let or_node = dag.set_or(vec![and1, and2]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (0, 0));
        assume.insert("y", (0, 0));
        assume.insert("z", (0, 0));
        assume.insert("w", (0, 0));
        assume.insert(or_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "Complex nested contradiction should be infeasible"
        );
    }

    #[test]
    fn infeasible_optimization_no_solution() {
        // Maximize x subject to x + y <= -1 with x, y ≥ 0
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 5));
        dag.set_primitive("y", (0, 5));
        let atmost_node = dag.set_atmost(vec!["x", "y"], -1).unwrap();

        let mut objective = HashMap::<&str, f64>::new();
        objective.insert("x", 1.0);

        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(atmost_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_none(),
            "Optimization with impossible constraints should be infeasible"
        );
    }

    #[test]
    fn edge_case_empty_integer_constraints() {
        // No constraints, just maximize x
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 10));

        let mut objective = HashMap::<&str, f64>::new();
        objective.insert("x", 1.0);

        let assume = HashMap::<&str, Bound>::new();

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Empty constraints should be feasible");
        let soln = solns[0].as_ref().unwrap();

        // Should maximize x to its upper bound
        let x_val = soln.get("x").unwrap().0;
        assert_eq!(x_val, 10, "Should maximize x to upper bound");
    }

    #[test]
    fn edge_case_single_variable_bounds() {
        // Test various single variable bound scenarios
        let mut dag = Pldag::new();
        dag.set_primitive("x", (5, 5)); // Fixed value

        let objective = HashMap::<&str, f64>::new();
        let assume = HashMap::<&str, Bound>::new();

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Fixed value should be feasible");
        let soln = solns[0].as_ref().unwrap();

        assert_eq!(
            *soln.get("x").unwrap(),
            (5, 5),
            "Fixed value should be exact"
        );
    }

    #[test]
    fn edge_case_zero_coefficients() {
        // Test optimization with zero coefficients
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 5));
        dag.set_primitive("y", (0, 5));

        let mut objective = HashMap::<&str, f64>::new();
        objective.insert("x", 0.0);
        objective.insert("y", 0.0);

        let assume = HashMap::<&str, Bound>::new();

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Zero coefficients should be feasible");
        // Any solution should be valid when coefficients are zero
    }

    #[test]
    fn edge_case_large_bounds() {
        // Test with large bound values
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1000000));
        dag.set_primitive("y", (0, 1000000));
        let atmost_node = dag.set_atmost(vec!["x", "y"], 999999).unwrap();

        let mut objective = HashMap::<&str, f64>::new();
        objective.insert("x", 1.0);

        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(atmost_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Large bounds should be feasible");
        let soln = solns[0].as_ref().unwrap();

        let x_val = soln.get("x").unwrap().0;
        let y_val = soln.get("y").unwrap().0;
        assert!(
            x_val + y_val <= 999999,
            "Large bound constraint should be satisfied"
        );
    }

    #[test]
    fn edge_case_negative_bounds() {
        // Test with negative bounds
        let mut dag = Pldag::new();
        dag.set_primitive("x", (-10, 10));
        dag.set_primitive("y", (-5, 5));
        let atleast_node = dag.set_atleast(vec!["x", "y"], -3).unwrap();

        let mut objective = HashMap::<&str, f64>::new();
        objective.insert("x", 1.0);

        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(atleast_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Negative bounds should be feasible");
        let soln = solns[0].as_ref().unwrap();

        let x_val = soln.get("x").unwrap().0;
        let y_val = soln.get("y").unwrap().0;
        assert!(
            x_val + y_val >= -3,
            "Negative bound constraint should be satisfied"
        );
    }

    #[test]
    fn edge_case_single_element_operations() {
        // Test logical operations with single elements
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));

        let and_single = dag.set_and(vec!["x"]).unwrap();
        let or_single = dag.set_or(vec!["x"]).unwrap();
        let xor_single = dag.set_xor(vec!["x"]).unwrap();
        let root = dag.set_and(vec![
            and_single.clone(),
            or_single.clone(),
            xor_single.clone(),
        ]).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert("x", (1, 1));
        assume.insert(root.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Single element operations should be feasible"
        );
        let soln = solns[0].as_ref().unwrap();

        assert_eq!(*soln.get(and_single.as_str()).unwrap(), (1, 1));
        assert_eq!(*soln.get(or_single.as_str()).unwrap(), (1, 1));
        assert_eq!(*soln.get(xor_single.as_str()).unwrap(), (1, 1));
    }

    #[test]
    fn edge_case_identical_variables_in_constraint() {
        // Test constraint with repeated variables: x + x + x >= 3
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 2));
        let atleast_node = dag.set_atleast(vec!["x", "x", "x"], 3).unwrap();

        let objective = HashMap::<&str, f64>::new();
        let mut assume = HashMap::<&str, Bound>::new();
        assume.insert(atleast_node.as_str(), (1, 1));

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Repeated variables in constraint should be feasible"
        );
        let soln = solns[0].as_ref().unwrap();

        let x_val = soln.get("x").unwrap().0;
        assert!(
            3 * x_val >= 3,
            "Repeated variable constraint should be satisfied"
        );
    }

    #[test]
    fn edge_case_very_small_coefficients() {
        // Test with very small floating point coefficients
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1000));
        dag.set_primitive("y", (0, 1000));

        let mut objective = HashMap::<&str, f64>::new();
        objective.insert("x", 0.000001);
        objective.insert("y", 0.000002);

        let assume = HashMap::<&str, Bound>::new();

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(
            solns[0].is_some(),
            "Very small coefficients should be feasible"
        );
        let soln = solns[0].as_ref().unwrap();

        // Should still maximize according to relative coefficients
        let x_val = soln.get("x").unwrap().0;
        let y_val = soln.get("y").unwrap().0;
        assert!(x_val >= 0 && y_val >= 0, "Solution should be within bounds");
    }

    #[test]
    fn edge_case_empty_variable_lists() {
        // Test operations with empty variable lists - should fail gracefully
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));

        // Most operations should handle empty lists gracefully
        // This is mainly testing that the library doesn't crash
        let objective = HashMap::<&str, f64>::new();
        let assume = HashMap::<&str, Bound>::new();

        let solns = Pldag::solve(&dag.sub_dag(vec![]).unwrap(), vec![objective], assume, true).unwrap();
        assert!(solns[0].is_some(), "Empty operations should not crash");
    }

    #[test]
    fn test_common_dag_with_xor_conjunction() {
        let mut dag = Pldag::new();
        dag.set_primitives(vec!["s1", "s2", "f1", "f2"], (0, 1));
        let s = dag.set_xor(vec!["s1", "s2"]).unwrap();
        let f = dag.set_xor(vec!["f1", "f2"]).unwrap();
        let root = dag.set_and(vec![s, f]).unwrap();
        let solution = Pldag::solve(
            &dag.sub_dag(vec![]).unwrap(),
            vec![HashMap::from([
                ("s1", 1.0),
                ("s2", -1.0),
                ("f2", 1.0),
                ("f1", -1.0),
            ])],
            HashMap::from([(root.as_str(), (1, 1))]),
            true,
        ).unwrap();
        let solution = &solution[0];
        assert!(solution.is_some(), "Expected a feasible solution");
        let solution_unwrapped = solution.as_ref().unwrap();
        assert_eq!(
            *solution_unwrapped.get("s1").unwrap(),
            (1, 1),
            "s1 should be selected"
        );
        assert_eq!(
            *solution_unwrapped.get("s2").unwrap(),
            (0, 0),
            "s2 should not be selected"
        );
        assert_eq!(
            *solution_unwrapped.get("f1").unwrap(),
            (0, 0),
            "f1 should not be selected"
        );
        assert_eq!(
            *solution_unwrapped.get("f2").unwrap(),
            (1, 1),
            "f2 should be selected"
        );
    }

    #[test]
    fn test_atleast_with_no_variables_will_result_to_false() {
        let mut dag = Pldag::new();
        dag.set_primitive("x", (0, 1));
        let atleast = dag.set_atleast(Vec::<&str>::new(), 1).unwrap();
        let equiv = dag.set_equiv("x", atleast.as_str()).unwrap();
        let solutions = Pldag::solve(
            &dag.sub_dag(vec![]).unwrap(),
            vec![HashMap::new()],
            HashMap::from([(equiv.as_str(), (1, 1)), ("x", (1, 1))]),
            true,
        ).unwrap();
        assert!(solutions[0].is_none());
    }

    #[test]
    fn test_exactly_one_boolean_selection() {
        let mut model = Pldag::new();
        model.set_primitive("a", (0, 1));
        model.set_primitive("b", (0, 1));
        model.set_primitive("c", (0, 1));
        let xor = model.set_atmost(vec!["a", "b", "c"], 1).unwrap();

        let solutions = Pldag::solve(
            &model.sub_dag(vec![]).unwrap(),
            vec![HashMap::from([("a", 1.0), ("b", 1.0), ("c", 1.0)])],
            HashMap::from([(xor.as_str(), (1, 1))]),
            true,
        ).unwrap();
        let assignments = solutions[0].as_ref().unwrap();
        let selected_vars: Vec<&&str> = ["a", "b", "c"]
            .iter()
            .filter(|&var| assignments.get(*var).unwrap().0 == 1)
            .collect();
        assert_eq!(
            selected_vars.len(),
            1,
            "Exactly one variable should be selected"
        );
    }

    #[test]
    fn test_solve_with_equalities_and_integers() {
        let mut model = Pldag::new();
        model.set_primitive("a", (0, 2));
        model.set_primitive("b", (0, 2));
        let lr = model.set_equal(vec!["a", "b"], 1).unwrap();
        let rr = model.set_equal(vec!["a", "b"], 2).unwrap();
        let root = model.set_and(vec![lr, rr]).unwrap();
        let solutions = Pldag::solve(
            &model.sub_dag(vec![]).unwrap(),
            vec![HashMap::from([("a", 1.0), ("b", 1.0)])],
            HashMap::from([(root.as_str(), (1, 1))]),
            true,
        ).unwrap();
        assert!(
            solutions[0].is_none(),
            "Conflicting equalities should be infeasible"
        );
    }

    #[test]
    fn test_solve_with_integer_decision_variables_1() {
        // This test is from an issue in the pldag-python repo. It turns out that the solver
        // returns a solution which is not valid according to the constraints.
        let mut model = Pldag::new();
        model.set_primitive("a", (0, 2));
        model.set_primitive("b", (0, 2));
        model.set_primitive("c", (0, 2));
        model.set_primitive("x", (0, 2));
        model.set_primitive("y", (0, 2));
        model.set_primitive("z", (0, 2));

        let root = model.set_equal(vec!["x", "y", "z"], 1).unwrap();
        let solutions = Pldag::solve(
            &model.sub_dag(vec![]).unwrap(),
            vec![HashMap::from([
                ("a", -1.0),
                ("b", -1.0),
                ("c", -1.0),
                ("x", -1.0),
                ("y", -1.0),
                ("z", -1.0),
            ])],
            HashMap::from([(root.as_str(), (1, 1)), ("a", (1, 1))]),
            true,
        ).unwrap();
        if let Some(assignments) = &solutions[0] {
            // Convert String keys to &str keys for propagate
            let str_assignments = assignments.iter().map(|(k, v)| (k.as_str(), *v));
            let propagated = model.propagate(str_assignments).unwrap();

            // Check that root is Some and is equal to 1
            assert!(
                assignments.get(root.as_str()).is_some(),
                "Root constraint should be assigned"
            );
            assert!(
                assignments.get(root.as_str()).unwrap().0 == 1,
                "Root constraint should be equal to 1"
            );
            assert!(
                assignments.get("a").is_some(),
                "Variable 'a' should be assigned"
            );
            assert!(
                assignments.get("a").unwrap().0 == 1,
                "Variable 'a' should be equal to 1"
            );

            assert!(
                propagated.get(root.as_str()).is_some(),
                "Root constraint should be satisfied after propagation"
            );
            assert!(
                propagated.get(root.as_str()).unwrap().0 == 1,
                "Root constraint should be equal to 1 after propagation"
            );
            assert!(
                propagated.get("a").is_some(),
                "Variable 'a' should be satisfied after propagation"
            );
            assert!(
                propagated.get("a").unwrap().0 == 1,
                "Variable 'a' should be equal to 1 after propagation"
            );
        } else {
            panic!("Expected a feasible solution");
        }
    }

    #[test]
    fn test_solve_when_composites_are_tautologies_or_contradictions() {
        let mut model = Pldag::new();
        let sand = model.set_and(Vec::<String>::new()).unwrap();
        let sor = model.set_gelineq(Vec::<(&str, i32)>::new(), -5).unwrap();
        let assume = HashMap::new();
        let solutions = Pldag::solve(
            &model.sub_dag(vec![]).unwrap(),
            vec![HashMap::from([(sand.as_str(), -1.0), (sor.as_str(), 1.0)])],
            assume.clone(),
            true,
        ).unwrap();
        let solution = solutions[0].as_ref().unwrap();
        assert_eq!(*solution.get(sand.as_str()).unwrap(), (1, 1));
        assert_eq!(*solution.get(sor.as_str()).unwrap(), (0, 0));

        let mut model = Pldag::new();
        model.set_primitive("x", (0, 1));
        model.set_primitive("y", (0, 1));
        model.set_primitive("z", (0, 1));
        let atmost_taut = model.set_atmost(vec!["x", "y", "z"], 3).unwrap();
        let solutions = Pldag::solve(
            &model.sub_dag(vec![]).unwrap(),
            vec![HashMap::from([(atmost_taut.as_str(), -1.0)])],
            HashMap::new(),
            true,
        ).unwrap();
        let solution = solutions[0].as_ref().unwrap();
        assert_eq!(*solution.get(atmost_taut.as_str()).unwrap(), (1, 1));
    }
}