rust_formal_verification/solvers/sat/
assignment.rs

1// ************************************************************************************************
2// use
3// ************************************************************************************************
4
5use crate::formulas::literal::VariableType;
6use std::collections::HashSet;
7
8// ************************************************************************************************
9// struct
10// ************************************************************************************************
11
12#[derive(Debug, PartialEq, Eq)]
13pub struct Assignment {
14    true_variables: HashSet<VariableType>,
15    false_variables: HashSet<VariableType>,
16}
17
18// ************************************************************************************************
19// impl
20// ************************************************************************************************
21
22impl Assignment {
23    // ********************************************************************************************
24    // helper functions
25    // ********************************************************************************************
26
27    fn new(true_variables: HashSet<VariableType>, false_variables: HashSet<VariableType>) -> Self {
28        Self {
29            true_variables,
30            false_variables,
31        }
32    }
33
34    // ********************************************************************************************
35    // API
36    // ********************************************************************************************
37
38    pub fn from_dimacs_assignment(vector: &[i32]) -> Self {
39        let mut true_variables = HashSet::<VariableType>::new();
40        let mut false_variables = HashSet::<VariableType>::new();
41
42        for var in vector.iter() {
43            let var_num: VariableType = var.abs().try_into().unwrap();
44            debug_assert!(var_num != 0);
45            if var < &0 {
46                false_variables.insert(var_num);
47            } else {
48                true_variables.insert(var_num);
49            }
50        }
51
52        Self::new(true_variables, false_variables)
53    }
54
55    pub fn get_value(&self, variable: &VariableType) -> Option<bool> {
56        if self.true_variables.contains(variable) {
57            Some(true)
58        } else if self.false_variables.contains(variable) {
59            Some(false)
60        } else {
61            None
62        }
63    }
64}
rust_formal_verification/solvers/sat/assignment.rs

rust_formal_verification/solvers/sat/
assignment.rs
