fn get_as_bool_z3_ast()

in checker/src/z3_solver.rs [1679:1767]

• 88 lines of code
• 4 McCabe index (conditional complexity)

    fn get_as_bool_z3_ast(&self, expression: &Expression) -> z3_sys::Z3_ast {
        match expression {
            Expression::BitAnd { .. } | Expression::BitOr { .. } | Expression::BitXor { .. } => {
                //todo: get operands as booleans and treat these operands as logical
                let bv = self.get_as_bv_z3_ast(expression, 128);
                unsafe {
                    let i = z3_sys::Z3_mk_bv2int(self.z3_context, bv, false);
                    let f = z3_sys::Z3_mk_eq(self.z3_context, i, self.zero);
                    z3_sys::Z3_mk_not(self.z3_context, f)
                }
            }
            Expression::CompileTimeConstant(const_domain) => match const_domain {
                ConstantDomain::False => unsafe { z3_sys::Z3_mk_false(self.z3_context) },
                ConstantDomain::True => unsafe { z3_sys::Z3_mk_true(self.z3_context) },
                ConstantDomain::U128(val) => unsafe {
                    if *val == 0 {
                        z3_sys::Z3_mk_false(self.z3_context)
                    } else {
                        z3_sys::Z3_mk_true(self.z3_context)
                    }
                },
                _ => self.get_as_z3_ast(expression),
            },
            Expression::ConditionalExpression {
                condition,
                consequent,
                alternate,
            } => {
                let condition_ast = self.get_as_bool_z3_ast(&(**condition).expression);
                let consequent_ast = self.get_as_bool_z3_ast(&(**consequent).expression);
                let alternate_ast = self.get_as_bool_z3_ast(&(**alternate).expression);
                unsafe {
                    z3_sys::Z3_mk_ite(
                        self.z3_context,
                        condition_ast,
                        consequent_ast,
                        alternate_ast,
                    )
                }
            }
            Expression::Join { left, right } => self.boolean_join(left, right),
            Expression::Reference(path) => unsafe {
                let path_symbol = self.get_symbol_for(path);
                z3_sys::Z3_mk_const(self.z3_context, path_symbol, self.bool_sort)
            },
            Expression::Switch {
                discriminator,
                cases,
                default,
            } => self.general_switch(discriminator, cases, default, |e| {
                self.get_as_bool_z3_ast(e)
            }),
            Expression::Top | Expression::Bottom => unsafe {
                z3_sys::Z3_mk_fresh_const(self.z3_context, self.empty_str, self.bool_sort)
            },
            Expression::UninterpretedCall {
                result_type: var_type,
                path,
                ..
            }
            | Expression::InitialParameterValue { path, var_type }
            | Expression::Variable { path, var_type } => {
                if *var_type != ExpressionType::Bool {
                    debug!("path {:?}, type {:?}", path, var_type);
                }
                unsafe {
                    let path_symbol = self.get_symbol_for(path);
                    z3_sys::Z3_mk_const(self.z3_context, path_symbol, self.bool_sort)
                }
            }
            Expression::WidenedJoin { path, operand } => {
                self.get_ast_for_widened(path, operand, ExpressionType::Bool)
            }
            _ => {
                let expression_type = expression.infer_type();
                if expression_type.is_integer() {
                    let (_, ast) = self.get_as_numeric_z3_ast(expression);
                    unsafe {
                        z3_sys::Z3_mk_not(
                            self.z3_context,
                            z3_sys::Z3_mk_eq(self.z3_context, ast, self.zero),
                        )
                    }
                } else {
                    self.get_as_z3_ast(expression)
                }
            }
        }
    }