razor-chase 0.1.0

razor-chase implements a variation of The Chase algorithm to find models for theories in geometric form.
Documentation 
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

//! Implements various bounders for bounding the size of models, generated by the Chase.
//!
//! The bounders are instances of [`BounderTrait`].
//!
//! [`BounderTrait`]: ../trait.BounderTrait.html
use crate::chase::{BounderTrait, ModelTrait, WitnessTermTrait, Observation};

/// Bounds the size of a [model] by the number of elements in its [domain].
///
/// [model]: ../trait.ModelTrait.html
/// [domain]: ../trait.ModelTrait.html#tymethod.domain
pub struct DomainSize {
    /// Is the maximum size of the [domain] of elements for models accepted by this bounder.
    ///
    /// [domain]: ../trait.ModelTrait.html#tymethod.domain
    max_domain_size: usize,
}

impl From<usize> for DomainSize {
    fn from(size : usize) -> Self {
        Self { max_domain_size: size }
    }
}

impl BounderTrait for DomainSize {
    fn bound<M: ModelTrait>(&self, model: &M, observation: &Observation<M::TermType>) -> bool {
        match observation {
            Observation::Fact { relation: _, terms } => {
                let model_size = model.domain().len();
                let terms: Vec<Option<&<<M as ModelTrait>::TermType as WitnessTermTrait>::ElementType>> = terms.iter()
                    .map(|t| model.element(t))
                    .filter(|t| t.is_none()).collect();
                let size = terms.len();
                model_size + size > self.max_domain_size
            }
            Observation::Identity { left, right } => {
                let mut size = model.domain().len();
                if model.element(left).is_none() {
                    size += 1;
                }
                if model.element(right).is_none() {
                    size += 1;
                }
                size > self.max_domain_size
            }
        }
    }
}