solhop_types/
lib.rs

1#![deny(missing_docs)]
2
3//! Common types used in SolHOP.
4
5use std::ops::Not;
6
7/// Dimacs module
8pub mod dimacs;
9
10/// A variable.
11#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
12pub struct Var(usize);
13
14impl Var {
15    /// Create new var TODO: Make it private
16    pub fn new(index: usize) -> Self {
17        Self(index)
18    }
19
20    /// Returns the actual value stored inside that can be used to index arrays.
21    pub fn index(self) -> usize {
22        self.0
23    }
24
25    /// Create positive literal from variable.
26    pub fn pos_lit(self) -> Lit {
27        Lit::new(self, false)
28    }
29
30    /// Create negative literal from variable.
31    pub fn neg_lit(self) -> Lit {
32        Lit::new(self, true)
33    }
34}
35
36/// A literal.
37#[derive(Clone, Copy, PartialEq, Debug)]
38pub struct Lit(usize);
39
40/// Placeholder Lit
41pub const UNDEF_LIT: Lit = Lit(usize::MAX);
42
43impl Lit {
44    /// Returns true if literal is signed (i.e. a negated literal).
45    pub fn sign(self) -> bool {
46        self.0 & 1 == 1
47    }
48
49    /// Returns the var corresponding to the literal.
50    pub fn var(self) -> Var {
51        Var(self.0 >> 1)
52    }
53
54    /// Returns the actual value stored inside that can be used to index arrays.
55    pub fn index(self) -> usize {
56        self.0
57    }
58
59    /// Create lit from var and sign
60    pub fn new(var: Var, sign: bool) -> Lit {
61        Lit(var.0 + var.0 + (sign as usize))
62    }
63}
64
65impl Not for Lit {
66    type Output = Self;
67
68    /// Returns x for -x and -x for x.
69    fn not(self) -> Self {
70        Lit(self.0 ^ 1)
71    }
72}
73
74/// A Lifted boolean.
75#[derive(Clone, Copy, PartialEq, Debug)]
76pub enum LBool {
77    /// Represents True.
78    True,
79    /// Represents False.
80    False,
81    /// Represents neither True nor False, usually used when variable is unassigned.
82    Undef,
83}
84
85impl Not for LBool {
86    type Output = Self;
87
88    /// Returns True for False and False for True.
89    /// If the input is Undef, then Undef is returned.
90    fn not(self) -> Self {
91        match self {
92            LBool::True => LBool::False,
93            LBool::False => LBool::True,
94            LBool::Undef => LBool::Undef,
95        }
96    }
97}
98
99impl From<bool> for LBool {
100    /// Convert bool to LBool.
101    fn from(b: bool) -> Self {
102        if b {
103            LBool::True
104        } else {
105            LBool::False
106        }
107    }
108}
109
110/// A Clause.
111#[derive(Clone, Debug)]
112pub struct Clause {
113    /// A vector of literals forming the clause.
114    pub lits: Vec<Lit>,
115}
116
117/// Solution to the SAT Formula.
118#[derive(Debug, PartialEq)]
119pub enum Solution {
120    /// The formula is unsatisfiable.
121    Unsat,
122    /// Neither SAT or UNSAT was proven. Best model known so far.
123    Best(Vec<bool>),
124    /// The formula is satisfiable. A satifying model for the formula.
125    Sat(Vec<bool>),
126    /// No solution could be found.
127    Unknown,
128}
solhop_types/lib.rs

solhop_types/
lib.rs
