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
use crate::solver::SolverError;
#[derive(Copy, Clone, Eq, PartialEq, Debug)]
pub enum SatState {
Unknown,
Sat,
Unsat,
UnsatUnderAssumptions,
}
impl Default for SatState {
fn default() -> SatState {
SatState::Unknown
}
}
pub struct SolverState {
pub sat_state: SatState,
pub formula_is_empty: bool,
pub solver_invoked: bool,
pub state_is_invalid: bool,
pub solver_error: Option<SolverError>,
}
impl Default for SolverState {
fn default() -> SolverState {
SolverState {
sat_state: SatState::Unknown,
formula_is_empty: true,
solver_invoked: false,
state_is_invalid: false,
solver_error: None,
}
}
}