Function revise 

pub fn revise(set: &[Belief], belief: Belief, out: &mut [Belief]) -> usize

AGM revision K * φ via the Levi identity: drop any belief about belief.atom (so the contrary ¬φ is contracted), then add φ. The result satisfies success (φ ∈ K*φ) and consistency (never both φ and ¬φ). Writes into out, returns its length.