1 
#[cfg(test)]
2 
#[test]
3 
fn test1() {
4 
    use kissat_rs::Assignment;
5 
    use kissat_rs::Solver;
6 

            

        

            

                7
            

            

                
            

            

                
    // Define three literals used in both formulae.

            

        

            

                8
            

            

                
            

            

                
    let x = 1;

            

        

            

                9
            

            

                
            

            

                
    let y = 2;

            

        

            

                10
            

            

                
            

            

                
    let z = 3;

            

        

            

                11
            

            

                
            

            

                

            

        

            

                12
            

            

                
            

            

                
    // Construct a formula from clauses (i.e. an iterator over literals).

            

        

            

                13
            

            

                
            

            

                
    // (~x || y) && (~y || z) && (x || ~z) && (x || y || z)

            

        

            

                14
            

            

                
            

            

                
    let formula1 = vec![vec![-x, y], vec![-y, z], vec![x, -z], vec![x, y, z]];

            

        

            

                15
            

            

                
            

            

                
    let satisfying_assignment = Solver::solve_formula(formula1).unwrap();

            

        

            

                16
            

            

                
            

            

                

            

        

            

                17
            

            

                
            

            

                
    // The formula from above is satisfied by the assignment: x -> True, y -> True, z -> True

            

        

            

                18
            

            

                
            

            

                
    if let Some(assignments) = satisfying_assignment {

            

        

            

                19
            

            

                
            

            

                
        assert_eq!(assignments.get(&x).unwrap(), &Some(Assignment::True));

            

        

            

                20
            

            

                
            

            

                
        assert_eq!(assignments.get(&y).unwrap(), &Some(Assignment::True));

            

        

            

                21
            

            

                
            

            

                
        assert_eq!(assignments.get(&z).unwrap(), &Some(Assignment::True));

            

        

            

                22
            

            

                
            

            

                
    }

            

        

            

                23
            

            

                
            

            

                

            

        

            

                24
            

            

                
            

            

                
    // (x || y || ~z) && ~x && (x || y || z) && (x || ~y)

            

        

            

                25
            

            

                
            

            

                
    let formula2 = vec![vec![x, y, -z], vec![-x], vec![x, y, z], vec![x, -y]];

            

        

            

                26
            

            

                
            

            

                
    let unsat_result = Solver::solve_formula(formula2).unwrap();

            

        

            

                27
            

            

                
            

            

                

            

        

            

                28
            

            

                
            

            

                
    // The second formula is unsatisfiable.

            

        

            

                29
            

            

                
            

            

                
    // This can for example be proved by resolution.

            

        

            

                30
            

            

                
            

            

                
    assert_eq!(unsat_result, None);

            

        

            

                31
            

            

                
            

            

                
}