sddrs/manager/
model.rs

1//! Models of the compiled knowledge base.
2use crate::literal::{Literal, Polarity, Variable};
3use bitvec::prelude::*;
4use std::fmt::Display;
5use tabled::{builder::Builder, grid::config::HorizontalLine, settings::Theme};
6
7/// All models of the knowledge base.
8#[derive(Debug, PartialEq)]
9pub struct Models {
10    models: Vec<BitVec>,
11    variables: Vec<Variable>,
12}
13
14impl Models {
15    pub(crate) fn new(models: &[BitVec], variables: Vec<Variable>) -> Self {
16        let mut models = models.to_owned();
17        models.sort();
18        Models { models, variables }
19    }
20
21    /// Get all models of the knowledge base.
22    #[must_use]
23    pub fn all_models(&self) -> Vec<Model> {
24        self.models
25            .iter()
26            .map(|enumeration_bitvec| {
27                Model::new_from_bitvector(enumeration_bitvec, &self.variables)
28            })
29            .collect()
30    }
31}
32
33impl Display for Models {
34    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
35        let mut builder = Builder::default();
36        builder.push_record(self.variables.iter().map(Variable::label));
37
38        for model in &self.models {
39            builder.push_record(
40                model
41                    .iter()
42                    .map(|assignment| if *assignment { "1" } else { "0" }),
43            );
44        }
45
46        let mut style = Theme::default();
47        style.insert_horizontal_line(1, HorizontalLine::full('-', '-', ' ', ' '));
48        let output = builder.build().with(style).to_string();
49        write!(f, "{output}")
50    }
51}
52
53/// Single model of the knowledge base. The model
54/// is displayable.
55#[derive(Debug, PartialEq, Eq)]
56pub struct Model {
57    literals: Vec<Literal>,
58}
59
60impl Model {
61    #[allow(unused)]
62    pub(crate) fn new_from_literals(literals: &[Literal]) -> Self {
63        let mut literals = literals.to_owned();
64        literals.sort();
65        Model { literals }
66    }
67
68    fn new_from_bitvector(model: &BitVec, labels: &[Variable]) -> Self {
69        Model {
70            literals: model
71                .iter()
72                .zip(labels.iter())
73                .map(|(polarity, var_label)| {
74                    Literal::new_with_label(Polarity::from(*polarity), var_label.clone())
75                })
76                .collect(),
77        }
78    }
79}
80
81impl Display for Model {
82    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
83        fn lit_repr(literal: &Literal) -> String {
84            format!(
85                "{}{literal}",
86                if literal.polarity() == Polarity::Negative {
87                    ""
88                } else {
89                    " "
90                }
91            )
92        }
93
94        write!(
95            f,
96            "{{{}}}",
97            self.literals
98                .iter()
99                .map(lit_repr)
100                .collect::<Vec<String>>()
101                .join(", ")
102        )
103    }
104}
sddrs/manager/model.rs

sddrs/manager/
model.rs
