z3rs 0.0.3

A pure-Rust port of the Z3 theorem prover, free of third-party and native dependencies
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

//! Boolean variables and literals — ported from `z3/src/sat/sat_types.h`
//! (Z3 4.17.0, MIT). Literals use Z3's `2*var + sign` packing so that negation
//! is a single bit flip and the literal is its own dense table index.

use core::fmt;
use core::ops::Not;

/// A propositional variable (a dense index).
pub type Var = u32;

/// A literal: a variable together with a sign. Encoded as `2*var + sign`, where
/// `sign == 1` denotes the *negative* literal (Z3's convention).
#[derive(Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub struct Lit(u32);

impl Lit {
    /// The literal `var` with the given sign (`true` = negated).
    #[inline]
    pub const fn new(var: Var, sign: bool) -> Lit {
        Lit((var << 1) | sign as u32)
    }

    /// The positive literal for `var`.
    #[inline]
    pub const fn pos(var: Var) -> Lit {
        Lit::new(var, false)
    }

    /// The negative literal for `var`.
    #[inline]
    pub const fn neg(var: Var) -> Lit {
        Lit::new(var, true)
    }

    /// The underlying variable.
    #[inline]
    pub const fn var(self) -> Var {
        self.0 >> 1
    }

    /// Is this the negative literal?
    #[inline]
    pub const fn sign(self) -> bool {
        (self.0 & 1) == 1
    }

    /// The dense index (`2*var + sign`), suitable for a lookup table.
    #[inline]
    pub const fn index(self) -> u32 {
        self.0
    }

    /// Reconstruct a literal from its [`index`](Self::index).
    #[inline]
    pub const fn from_index(i: u32) -> Lit {
        Lit(i)
    }
}

impl Not for Lit {
    type Output = Lit;
    /// Negate the literal (flip the sign bit).
    #[inline]
    fn not(self) -> Lit {
        Lit(self.0 ^ 1)
    }
}

impl fmt::Display for Lit {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        if self.sign() {
            write!(f, "-{}", self.var())
        } else {
            write!(f, "{}", self.var())
        }
    }
}

impl fmt::Debug for Lit {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "Lit({self})")
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn packing_and_negation() {
        let p = Lit::pos(3);
        let n = Lit::neg(3);
        assert_eq!(p.var(), 3);
        assert!(!p.sign());
        assert!(n.sign());
        assert_eq!(!p, n);
        assert_eq!(!n, p);
        assert_eq!(!!p, p);
        // index round-trips.
        assert_eq!(Lit::from_index(p.index()), p);
        assert_eq!(p.index(), 6);
        assert_eq!(n.index(), 7);
    }

    #[test]
    fn display() {
        use alloc::format;
        assert_eq!(format!("{}", Lit::pos(2)), "2");
        assert_eq!(format!("{}", Lit::neg(2)), "-2");
    }
}