linear_solver 0.2.2

A linear solver designed to be easy to use with Rust enum expressions
Documentation 
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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117

/*

In this example, we prove the following:

    X <= Y
    Y <= Z
    Z <= X
    ------
    Y = Z
    Y = X

*/

extern crate linear_solver;

use linear_solver::{solve_minimum, Inference};
use linear_solver::Inference::*;

use std::collections::HashSet;

use self::Expr::*;

#[derive(Clone, PartialEq, Eq, Debug, Hash)]
pub enum Expr {
    Var(&'static str),
    Le(Box<Expr>, Box<Expr>),
    Eq(Box<Expr>, Box<Expr>),
}

pub fn infer(cache: &HashSet<Expr>, facts: &[Expr]) -> Option<Inference<Expr>> {
    // Put simplification rules first to find simplest set of facts.
    for ea in facts {
        if let Le(ref a, ref b) = *ea {
            if a == b {
                // (X <= X) <=> true
                return Some(OneTrue {from: ea.clone()});
            }

            for eb in facts {
                if let Le(ref c, ref d) = *eb {
                    if a == d && b == c {
                        // (X <= Y) ∧ (Y <= X) <=> (X = Y)
                        return Some(Inference::replace(
                            vec![ea.clone(), eb.clone()],
                            Eq(a.clone(), b.clone()),
                            cache
                        ))
                    }
                }
            }
        }

        if let Eq(ref a, ref b) = *ea {
            for eb in facts {
                if let Le(ref c, ref d) = *eb {
                    if c == b {
                        // (X = Y) ∧ (Y <= Z) <=> (X = Y) ∧ (X <= Z)
                        return Some(Inference::replace_one(
                            eb.clone(),
                            Le(a.clone(), d.clone()),
                            cache
                        ));
                    } else if d == b {
                        // (X = Y) ∧ (Z <= Y) <=> (X = Y) ∧ (Z <= X)
                        return Some(Inference::replace_one(
                            eb.clone(),
                            Le(c.clone(), a.clone()),
                            cache
                        ));
                    }
                }

                if let Eq(ref c, ref d) = *eb {
                    if b == c {
                        // (X = Y) ∧ (Y = Z) <=> (X = Y) ∧ (X = Z)
                        return Some(Inference::replace_one(
                            eb.clone(),
                            Eq(a.clone(), d.clone()),
                            cache
                        ));
                    }
                }
            }
        }
    }

    // Put propagation rules last to find simplest set of facts.
    for ea in facts {
        if let Le(ref a, ref b) = *ea {
            for eb in facts {
                if let Le(ref c, ref d) = *eb {
                    if b == c {
                        // (X <= Y) ∧ (Y <= Z) => (X <= Z)
                        let new_expr = Le(a.clone(), d.clone());
                        if !cache.contains(&new_expr) {return Some(Propagate(new_expr))};
                    }
                }
            }
        }
    }
    None
}

pub fn var(name: &'static str) -> Box<Expr> {Box::new(Var(name))}

fn main() {
    let start = vec![
        Le(var("X"), var("Y")), // X <= Y
        Le(var("Y"), var("Z")), // Y <= Z
        Le(var("Z"), var("X")), // Z <= X
    ];

    let res = solve_minimum(start, infer);
    for i in 0..res.len() {
        println!("{:?}", res[i]);
    }
}