euf.rs

/// Check if two items are in the same equivalence class.
fn in_class(rel: BTreeMap<EUFTerm, BTreeSet<EUFTerm>>, left: &EUFTerm, right: &EUFTerm) -> bool {
    let mut seen = BTreeSet::new();
    let mut todo = vec![left];
    let empty_set = BTreeSet::new();

    while let Some(next) = todo.pop() {
        for candidate in rel.get(next).unwrap_or(&empty_set).difference(&seen) {
            if *candidate == *right {
                return true;
            }
            todo.push(candidate);
        }
        seen.insert(next.clone());
    }

    false
}

/*
error[E0502]: cannot borrow `seen` as mutable because it is also borrowed as immutable
  --> src/smt/euf.rs:93:9
   |
86 |     while let Some(next) = todo.pop() {
   |                            ---- immutable borrow later used here
87 |         for candidate in rel.get(next).unwrap_or(&empty_set).difference(&seen) {
   |                                                                         ----- immutable borrow occurs here
...
93 |         seen.insert(next.clone());
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^ mutable borrow occurs here

error: aborting due to previous error

For more information about this error, try `rustc --explain E0502`.
error: Could not compile `sat`.

To learn more, run the command again with --verbose.
8?

/// An EUF term is either an atom (represented as numbers) or a
/// function applied to an EUF term.
#[derive(Clone, Debug, PartialEq, PartialOrd, Eq, Ord)]
pub enum EUFTerm {
    Atom(usize),
    Application {
        function_atom: usize,
        parameters: Vec<EUFTerm>,
    },
}

/// Check if two items are in the same equivalence class.
fn in_class(rel: BTreeMap<EUFTerm, BTreeSet<EUFTerm>>, left: &EUFTerm, right: &EUFTerm) -> bool {
    let mut seen = BTreeSet::new();
    let mut todo = vec![left];
    let empty_set = BTreeSet::new();

    while let Some(next) = todo.pop() {
        {
            for candidate in rel.get(next).unwrap_or(&empty_set) {
                if seen.contains(candidate) {
                    continue;
                }
                if *candidate == *right {
                    return true;
                }
                todo.push(candidate);
            }
        }
        seen.insert(next.clone());
    }

    false
}