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

use crate::solver::{SolveSuccess, SolverCallback, SolverFamily, SolverMutCallback};
use crate::Model as ConjureModel;

use super::super::model_modifier::NotModifiable;
use super::super::private;
use super::super::SearchComplete::*;
use super::super::SearchIncomplete::*;
use super::super::SearchStatus::*;
use super::super::SolverAdaptor;
use super::super::SolverError;
use super::super::SolverError::*;
use super::super::SolverError::*;
use super::sat_common::CNFModel;

/// A [SolverAdaptor] for interacting with the Kissat SAT solver.
pub struct Kissat {
    __non_constructable: private::Internal,
    model: Option<CNFModel>,
}

impl private::Sealed for Kissat {}

impl Kissat {
    pub fn new() -> Self {
        Kissat {
            __non_constructable: private::Internal,
            model: None,
        }
    }
}

impl Default for Kissat {
    fn default() -> Self {
        Kissat::new()
    }
}

impl SolverAdaptor for Kissat {
    fn solve(
        &mut self,
        callback: SolverCallback,
        _: private::Internal,
    ) -> Result<SolveSuccess, SolverError> {
        Err(OpNotImplemented("solve(): todo!".to_owned()))
    }

    fn solve_mut(
        &mut self,
        callback: SolverMutCallback,
        _: private::Internal,
    ) -> Result<SolveSuccess, SolverError> {
        Err(OpNotSupported("solve_mut".to_owned()))
    }

    fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> {
        self.model = Some(CNFModel::from_conjure(model)?);
        Ok(())
    }

    fn get_family(&self) -> SolverFamily {
        SolverFamily::SAT
    }
}