fn general_ne()

in checker/src/z3_solver.rs [491:540]

• 50 lines of code
• 10 McCabe index (conditional complexity)

    fn general_ne(&self, left: &Rc<AbstractValue>, right: &Rc<AbstractValue>) -> z3_sys::Z3_ast {
        let num_bits = if left.expression.is_bit_vector() {
            u32::from(left.expression.infer_type().bit_length())
        } else if right.expression.is_bit_vector() {
            let mut result = u32::from(right.expression.infer_type().bit_length());
            if let Expression::BitAnd { left, .. } = &right.expression {
                if let Expression::CompileTimeConstant(ConstantDomain::U128(v)) = left.expression {
                    if v < u128::MAX && (v + 1).is_power_of_two() {
                        result = 0;
                    }
                }
            }
            result
        } else {
            0
        };
        if num_bits > 0 {
            let left_ast = self.get_as_bv_z3_ast(&(**left).expression, num_bits);
            let right_ast = self.get_as_bv_z3_ast(&(**right).expression, num_bits);
            unsafe {
                z3_sys::Z3_mk_not(
                    self.z3_context,
                    z3_sys::Z3_mk_eq(self.z3_context, left_ast, right_ast),
                )
            }
        } else {
            let (lf, left_ast) = self.get_as_numeric_z3_ast(&(**left).expression);
            let (rf, right_ast) = self.get_as_numeric_z3_ast(&(**right).expression);
            if lf != rf {
                warn!("can't encode {:?} != {:?}", left, right);
                return self
                    .general_variable(&Path::get_as_path(left.clone()), ExpressionType::Bool);
            }
            unsafe {
                if lf {
                    let l = z3_sys::Z3_mk_fpa_is_nan(self.z3_context, left_ast);
                    let r = z3_sys::Z3_mk_fpa_is_nan(self.z3_context, right_ast);
                    let eq = z3_sys::Z3_mk_fpa_eq(self.z3_context, left_ast, right_ast);
                    let ne = z3_sys::Z3_mk_not(self.z3_context, eq);
                    let tmp = vec![l, r, ne];
                    z3_sys::Z3_mk_or(self.z3_context, 3, tmp.as_ptr())
                } else {
                    z3_sys::Z3_mk_not(
                        self.z3_context,
                        z3_sys::Z3_mk_eq(self.z3_context, left_ast, right_ast),
                    )
                }
            }
        }
    }