haloumi-picus 0.5.6

Haloumi backend to the Picus Constraint Language.
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

use haloumi_ir::Prime;

use crate::pcl::{
    display::{TextRepresentable, TextRepresentation},
    expr::{Expr, impls::BinaryExpr},
    stmt::traits::ConstraintLike,
};

use super::{OpFolder, OpLike};

#[derive(Copy, Clone, Debug, PartialEq, Hash)]
pub enum Boolean {
    And,
    Or,
    Implies,
    Iff,
}

impl Boolean {
    fn fold_side(&self, lhs: &Expr, rhs: &Expr) -> Option<Expr> {
        log::debug!("Trying to fold ({self:?}  {lhs:?}  {rhs:?})");
        lhs.constraint_expr()
            .and_then(move |clhs| match self {
                // T && x == x
                Boolean::And if clhs.is_constant_true() => Some(rhs.clone()),
                // F && x == F
                Boolean::And if clhs.is_constant_false() => Some(lhs.clone()),
                // T || x == T
                Boolean::Or if clhs.is_constant_true() => Some(lhs.clone()),
                // F || x == x
                Boolean::Or if clhs.is_constant_false() => Some(rhs.clone()),
                _ => None,
            })
            .inspect(|e| log::debug!("Folded to {e:?}"))
    }
}

impl OpFolder for Boolean {
    fn fold(&self, lhs: Expr, rhs: Expr, _: Prime) -> Option<Expr> {
        self.fold_side(&lhs, &rhs).or_else(|| {
            self.flip(&lhs, &rhs)
                .and_then(|flipped| flipped.op().fold_side(&flipped.lhs(), &flipped.rhs()))
        })
    }

    fn commutative(&self) -> bool {
        !matches!(self, Boolean::Implies)
    }

    fn flip(&self, lhs: &Expr, rhs: &Expr) -> Option<BinaryExpr<Self>> {
        match self {
            Boolean::And => Some(BinaryExpr::new(Self::And, rhs.clone(), lhs.clone())),
            Boolean::Or => Some(BinaryExpr::new(Self::Or, rhs.clone(), lhs.clone())),
            Boolean::Iff => Some(BinaryExpr::new(Self::Iff, rhs.clone(), lhs.clone())),
            _ => None,
        }
    }
}

impl TextRepresentable for Boolean {
    fn to_repr(&self) -> TextRepresentation<'_> {
        TextRepresentation::atom(match self {
            Boolean::And => "&&",
            Boolean::Or => "||",
            Boolean::Implies => "=>",
            Boolean::Iff => "<=>",
        })
    }

    fn width_hint(&self) -> usize {
        match self {
            Boolean::And => 2,
            Boolean::Or => 2,
            Boolean::Implies => 2,
            Boolean::Iff => 3,
        }
    }
}

impl OpLike for Boolean {
    fn extraible(&self) -> bool {
        true
    }
}