conjure_core/solver/adaptors/
kissat.rs

1use crate::solver::{SolveSuccess, SolverCallback, SolverFamily, SolverMutCallback};
2use crate::Model as ConjureModel;
3
4use super::super::model_modifier::NotModifiable;
5use super::super::private;
6use super::super::SearchComplete::*;
7use super::super::SearchIncomplete::*;
8use super::super::SearchStatus::*;
9use super::super::SolverAdaptor;
10use super::super::SolverError;
11use super::super::SolverError::*;
12use super::super::SolverError::*;
13use super::sat_common::CNFModel;
14
15/// A [SolverAdaptor] for interacting with the Kissat SAT solver.
16pub struct Kissat {
17    __non_constructable: private::Internal,
18    model: Option<CNFModel>,
19}
20
21impl private::Sealed for Kissat {}
22
23impl Kissat {
24    pub fn new() -> Self {
25        Kissat {
26            __non_constructable: private::Internal,
27            model: None,
28        }
29    }
30}
31
32impl Default for Kissat {
33    fn default() -> Self {
34        Kissat::new()
35    }
36}
37
38impl SolverAdaptor for Kissat {
39    fn solve(
40        &mut self,
41        callback: SolverCallback,
42        _: private::Internal,
43    ) -> Result<SolveSuccess, SolverError> {
44        Err(OpNotImplemented("solve(): todo!".to_owned()))
45    }
46
47    fn solve_mut(
48        &mut self,
49        callback: SolverMutCallback,
50        _: private::Internal,
51    ) -> Result<SolveSuccess, SolverError> {
52        Err(OpNotSupported("solve_mut".to_owned()))
53    }
54
55    fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> {
56        self.model = Some(CNFModel::from_conjure(model)?);
57        Ok(())
58    }
59
60    fn get_family(&self) -> SolverFamily {
61        SolverFamily::SAT
62    }
63}
conjure_core/solver/adaptors/kissat.rs

conjure_core/solver/adaptors/
kissat.rs
