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

/// All term-like objects in our context have an inverse.
pub trait Term {
    fn inverse(&self) -> Self;
}

/// If terms can be cleaned up in a non-expensive way, they
/// implement this trait.
pub trait Reducable {
    fn reduced(self) -> Self;
}

/*
pub trait Meet<Rhs=Self> {
    type Output;
    fn meet(self, other: Rhs) -> Self::Output;
}

pub trait Join<Rhs=Self> {
    type Output;
    fn join(self, other: Rhs) -> Self::Output;
}
*/

/// The module containing everything about free group terms,
/// in particular the struct `FreeGroupTerm`.
pub mod free_group_term;

/// The module containing everything about literals,
/// in particular the struct `Literal`.
pub mod literal;

/// The module containing everything about l_group_formulas
/// (but not their cnfs), in particular the struct `LGroupTerm`.
pub mod l_group_term;
mod l_group_term_reducing;

/// The module containing everything about 'short' (shorter than three)
/// free group terms, in particular the struct `ShortFreeGroupTerm`.
pub mod short_free_group_term;


pub mod parsing_error;
pub mod formula;