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

use std::ops::Not;

/// A variable.
pub type Var = usize;

/// A literal.
#[derive(Clone, Copy, PartialEq, Debug)]
pub struct Lit(pub usize);

impl Lit {
    /// Returns true if literal is signed (i.e. a negated literal).
    pub fn sign(self) -> bool {
        self.0 & 1 == 1
    }

    /// Returns the var cooressponding to the literal.
    pub fn var(self) -> Var {
        self.0 >> 1
    }

    /// Returns the actual value stored inside
    /// that can be used to index arrays.
    pub fn index(self) -> usize {
        self.0
    }

    /// Create lit from var and sign
    pub fn new(var: Var, sign: bool) -> Lit {
        Lit(var + var + (sign as usize))
    }
}

impl Not for Lit {
    type Output = Self;

    /// Returns x for -x and -x for x.
    fn not(self) -> Self {
        Lit(self.0 ^ 1)
    }
}

/// A Lifted boolean.
#[derive(Clone, Copy, PartialEq, Debug)]
pub enum LBool {
    /// Represents True.
    True,
    /// Represents False.
    False,
    /// Represents neither True nor False, usually used when variable is unassigned.
    Undef,
}

impl Not for LBool {
    type Output = Self;

    /// Returns True for False and False for True.
    /// If the input is Undef, then Undef is returned.
    fn not(self) -> Self {
        match self {
            LBool::True => LBool::False,
            LBool::False => LBool::True,
            LBool::Undef => LBool::Undef,
        }
    }
}

impl From<bool> for LBool {
    /// Convert bool to LBool.
    fn from(b: bool) -> Self {
        if b {
            LBool::True
        } else {
            LBool::False
        }
    }
}

/// A Clause.
#[derive(Clone)]
pub struct Clause {
    /// A vector of literals forming the clause.
    pub lits: Vec<Lit>,
}

/// Solution to the SAT Formula.
#[derive(Debug)]
pub enum Solution {
    /// The formula is unsatisfiable
    Unsat,
    /// Neither SAT or UNSAT was proven. Best model known so far.
    Best(Vec<bool>),
    /// The formula is satisfiable. A satifying model for the formula.
    Sat(Vec<bool>),
}