minisat 0.4.1

MiniSat Rust interface. Solves a boolean satisfiability problem given in conjunctive normal form.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99

use super::{Bool, Solver, Model, ModelValue, ModelEq};
use std::iter::once;

pub struct Symbolic<T>(Vec<(Bool, T)>);

impl<T> Symbolic<T> {
    pub fn domain(&self) -> impl Iterator<Item = &T> {
        self.0.iter().map(|(_, t)| t)
    }

    pub fn new(solver: &mut Solver, mut xs: Vec<T>) -> Symbolic<T> {
        if xs.len() == 0 {
            panic!("Symbolic value cannot be initialized from empty list.");
        } else if xs.len() == 1 {
            Symbolic(vec![(true.into(), xs.remove(0))])
        } else if xs.len() == 1 {
            let l = solver.new_lit();
            let a = xs.remove(0);
            let b = xs.remove(0);
            Symbolic(vec![(l, a), (!l, b)])
        } else {
            let lits = xs.iter().map(|_| solver.new_lit()).collect::<Vec<_>>();
            solver.assert_exactly_one(lits.iter().cloned());
            Symbolic(lits.into_iter().zip(xs.into_iter()).collect())
        }
    }
}

impl<T: Eq> Symbolic<T> {
    pub fn has_value(&self, a: &T) -> Bool {
        for (v, x) in &self.0 {
            if x == a {
                return *v;
            }
        }
        false.into()
    }
}

impl<V: Ord> ModelEq for Symbolic<V> {
    fn assert_equal_or(solver: &mut Solver, prefix: Vec<Bool>, a: &Symbolic<V>, b: &Symbolic<V>) {
        for (p, q, x) in stitch(a, b) {
            match (p, q, x) {
                (Some(p), None, _) => solver.add_clause(once(!p).chain(prefix.iter().cloned())),
                (None, Some(q), _) => solver.add_clause(once(!q).chain(prefix.iter().cloned())),
                (Some(p), Some(q), _) => {
                    solver.add_clause(once(!p).chain(once(q)).chain(prefix.iter().cloned()))
                }
                _ => unreachable!(),
            }
        }
    }

    fn assert_not_equal_or(solver: &mut Solver,
                           prefix: Vec<Bool>,
                           a: &Symbolic<V>,
                           b: &Symbolic<V>) {
        for (p, q, x) in stitch(a, b) {
            match (p, q, x) {
                (Some(p), Some(q), _) => {
                    solver.add_clause(once(!p).chain(once(!q)).chain(prefix.iter().cloned()))
                }
                _ => {}
            }
        }
    }
}

fn stitch<'a, V: Ord>(a: &'a Symbolic<V>,
                      b: &'a Symbolic<V>)
                      -> impl Iterator<Item = (Option<Bool>, Option<Bool>, &'a V)> {
    use itertools::Itertools;
    let mut v: Vec<(Option<Bool>, Option<Bool>, &'a V)> = a.0
        .iter()
        .map(|(v, x)| (Some(*v), None, x))
        .chain(b.0.iter().map(|(v, x)| (None, Some(*v), x)))
        .collect();
    v.sort_by(|(_, _, x), (_, _, y)| x.cmp(y));
    v.into_iter().coalesce(|(a, b, x), (c, d, y)| if x == y {
        Ok((a.or(c), b.or(d), x))
    } else {
        Err(((a, b, x), (c, d, y)))
    })
}



impl<'a, V: 'a> ModelValue<'a> for Symbolic<V> {
    type T = &'a V;

    fn value(&'a self, m: &'a Model) -> Self::T {
        for (v, x) in &self.0 {
            if m.value(v) {
                return x;
            }
        }
        unreachable!()
    }
}