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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
use std::fmt;
use std::fmt::{Debug, Display};
use std::hash::{Hash, Hasher};
use std::collections::hash_map::DefaultHasher;
#[derive(Eq, Ord, PartialOrd, Clone)]
pub struct Proposition<PropositionId> where PropositionId: Hash {
pub id: PropositionId,
pub negation: bool,
}
impl<PropositionId: Display + Hash> Debug for Proposition<PropositionId> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "{}P:{}", if self.negation {"¬"} else {""}, self.id)
}
}
impl<PropositionId: Hash> Hash for Proposition<PropositionId> {
fn hash<H>(&self, state: &mut H) where H: Hasher {
self.negation.hash(state);
self.id.hash(state);
}
}
impl<PropositionId: Hash> PartialEq for Proposition<PropositionId> {
fn eq(&self, other: &Self) -> bool {
let mut hasher_left = DefaultHasher::new();
let mut hasher_right = DefaultHasher::new();
self.hash(&mut hasher_left);
other.hash(&mut hasher_right);
hasher_left.finish() == hasher_right.finish()
}
}
impl<PropositionId: Clone + PartialEq + Hash> Proposition<PropositionId> {
pub fn new(id: PropositionId, negation: bool) -> Self {
Proposition {id, negation}
}
pub fn negate(&self) -> Self {
Proposition { id: self.id.clone(), negation: !self.negation }
}
pub fn is_negation(&self, prop: &Self) -> bool {
prop.id == self.id && prop.negation == !self.negation
}
}
impl From<&'static str> for Proposition<&'static str> {
fn from(s: &'static str) -> Self {
Proposition {id: s, negation: false}
}
}
#[cfg(test)]
mod proposition_test {
use super::*;
#[derive(PartialEq, Clone, Hash, Eq)]
enum Props {
A,
B,
}
impl From<Props> for Proposition<Props> {
fn from(prop: Props) -> Self {
Self::new(prop, false)
}
}
#[test]
fn propositions_can_be_negated() {
assert_eq!(Proposition::from("test"), Proposition::from("test"));
let p1 = Proposition::from("test");
assert!(false == p1.negation);
assert!(true == Proposition::from("test").negate().negation);
let p2 = Proposition::from("test").negate();
assert!(
p2.is_negation(&p1),
format!("{:?} is not a negation of {:?}", p1, p2)
);
assert!(p1.is_negation(&p2));
}
#[test]
fn proposition_hashing_works() {
let set = hashset!{Proposition::from("caffeinated")};
assert!(set.contains(&Proposition::from("caffeinated")));
let set = hashset!{Proposition::from("caffeinated").negate()};
assert!(set.contains(&Proposition::from("caffeinated").negate()));
let set = hashset!{Proposition::from("caffeinated").negate()};
assert!(!set.contains(&Proposition::from("caffeinated")));
}
#[test]
fn proposition_ids_are_extensible() {
let p1 = Proposition::from(Props::A);
let p2 = Proposition::from(Props::B);
let set = hashset!{p1.clone()};
assert!(set.contains(&p1));
assert!(!set.contains(&p2));
}
}