Method implies_not

src/analysis/memory/symbolic_value.rs:898–909

Returns true if "self => !other" is known at compile time to be true. Returning false does not imply the implication is false, just that we do not know.

(&self, other: &Rc<SymbolicValue>)

    /// Returns true if "self => !other" is known at compile time to be true.
    /// Returning false does not imply the implication is false, just that we do not know.
    fn implies_not(&self, other: &Rc<SymbolicValue>) -> bool {
        // x => !false, is always true
        // false => !x, is always true
        if !other.as_bool_if_known().unwrap_or(true) || !self.as_bool_if_known().unwrap_or(true) {
            return true;
        };
        // !x => !x
        if let Expression::LogicalNot { ref operand } = self.expression {
            return (**operand).eq(other);
        }
        false
    }

    /// Returns true if "!self => other" is known at compile time to be true.
    /// Returning false does not imply the implication is false, just that we do not know.