satgalaxy 0.2.0

satgalaxy-rs is a Rust library that provides Rust bindings for multiple popular SAT solvers
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

#[cfg(feature = "cadical")]
pub mod cadical;
#[cfg(feature = "cadical")]
pub use cadical::CaDiCaLSolver;
#[cfg(feature = "glucose")]
pub mod glucose;
#[cfg(feature = "glucose")]
pub use glucose::GlucoseSolver;
#[cfg(feature = "minisat")]
pub mod minisat;
#[cfg(feature = "minisat")]
pub use minisat::MinisatSolver;
#[cfg(feature = "picosat")]
pub mod picosat;
#[cfg(feature = "picosat")]
pub use picosat::PicoSATSolver;

use crate::errors::SolverError;

#[macro_export]
macro_rules! create_solver {
    (cadical) => {
        $crate::cadical::CaDiCaLSolver::new()
    };
    (minisat) => {
        $crate::minisat::MiniSatSolver::new()
    };
}


#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum RawStatus {
    Satisfiable,
    Unsatisfiable,
    Unknown,
}

impl Default for RawStatus {
    fn default() -> Self {
        Self::Unknown
    }
}

impl From<i32> for RawStatus {
    fn from(value: i32) -> Self {
        match value {
            10 => Self::Satisfiable,
            20 => Self::Unsatisfiable,
            _ => Self::Unknown,
        }
    }
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum SatStatus {
    Satisfiable(Vec<i32>),
    Unsatisfiable,
    Unknown,
}

impl Default for SatStatus {
    fn default() -> Self {
        Self::Unknown
    }
}

pub trait SatSolver {
    fn push_clause(&mut self, clause: &[i32]) -> Result<(), SolverError>;

    fn solve_model(&mut self) -> Result<SatStatus, SolverError> {
        let status = self.solve_sat()?;
        return match status {
            RawStatus::Satisfiable => self.model().map(SatStatus::Satisfiable),
            RawStatus::Unsatisfiable => Ok(SatStatus::Unsatisfiable),
            RawStatus::Unknown => Ok(SatStatus::Unknown),
        };
    }
    fn solve_sat(&mut self) -> Result<RawStatus, SolverError>;
    fn model(&mut self) -> Result<Vec<i32>, SolverError>;
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum MusStatus {
    Satisfiable,
    Unsatisfiable(Vec<usize>),
    Unknown,
}

impl Default for MusStatus {
    fn default() -> Self {
        Self::Unknown
    }
}

pub trait MusSolver {
    fn push_clause(&mut self, clause: &[i32]) -> Result<(), SolverError>;

    fn solve_mus(&mut self) -> Result<MusStatus, SolverError>;
}