Skip to content

Commit 02def16

Browse files
tsionyxtsionyx
committed
WIP: ANF
1 parent 7b83a36 commit 02def16

File tree

5 files changed

+543
-36
lines changed

5 files changed

+543
-36
lines changed

‎src/formula/general/equivalences/distrib.rs‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,38 @@ impl<T: Clone> RewritingRule<T> for DistributeDisjunctionOverConjunction {
7070
}
7171
}
7272

73+
#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Default)]
74+
/// Simplify a [`Formula`] by applying the rule of distributivity
75+
/// to conjunction where one of the operand is a XOR:
76+
///
77+
/// `r ⊕ (p ∧ q) ≡ (r ∧ p) ⊕ (r ∧ q)`
78+
///
79+
/// This transformation is useful to convert a [`Formula`] into _algebraic normal form_.
80+
pub struct DistributeConjunctionOverXor;
81+
82+
impl<T: Clone> RewritingRule<T> for DistributeConjunctionOverXor {
83+
fn reduce(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
84+
Err(formula)
85+
}
86+
87+
fn transform(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
88+
if let Formula::And(p, r) = formula {
89+
// (p ⊕ q) ∧ r ≡ (p ∧ r) ⊕ (q ∧ r)
90+
if let Formula::Xor(p, q) = *p {
91+
Ok((p & r.clone()) ^ (q & r))
92+
}
93+
// p ∧ (q ⊕ r) ≡ (p ∧ q) ⊕ (p ∧ r)
94+
else if let Formula::Xor(q, r) = *r {
95+
Ok((p.clone() & q) ^ (p & r))
96+
} else {
97+
Err(p & r)
98+
}
99+
} else {
100+
Err(formula)
101+
}
102+
}
103+
}
104+
73105
#[cfg(test)]
74106
mod tests {
75107
use super::{

‎src/formula/general/equivalences/mod.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ pub(crate) mod neg;
1414
mod prop_test;
1515
pub(crate) mod sort;
1616
mod traits;
17+
pub(crate) mod xor;
1718

1819
use std::fmt::Debug;
1920

‎src/formula/general/equivalences/xor.rs‎

Lines changed: 277 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,277 @@
1+
use super::{super::formula::Formula, RewritingRule};
2+
3+
#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Default)]
4+
/// Eliminate disjunctions from a [`Formula`] by converting them
5+
/// to a combination of XOR-ed conjunctions.
6+
///
7+
/// `p ∨ q ≡ p ⊕ q ⊕ (p ∧ q)`
8+
///
9+
/// This transformation is useful to convert a [`Formula`] into _algebraic normal form_.
10+
pub struct DisjunctionToXoredProducts;
11+
12+
impl<T: Clone> RewritingRule<T> for DisjunctionToXoredProducts {
13+
fn reduce(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
14+
Err(formula)
15+
}
16+
17+
fn transform(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
18+
if let Formula::Or(p, q) = formula {
19+
Ok(p.clone() ^ q.clone() ^ (p & q))
20+
} else {
21+
Err(formula)
22+
}
23+
}
24+
}
25+
26+
#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Default)]
27+
/// Replace an implication in a [`Formula`] with a disjunction:
28+
///
29+
/// p → q ≡ ¬p ∨ q ≡ (p ⊕ ⊤) ∨ q ≡ (p ⊕ ⊤) ⊕ q ⊕ ((p ∧ q) ⊕ (⊤ ∧ q)) ≡ p ⊕ ⊤ ⊕ q ⊕ (p ∧ q) ⊕ q ≡ p ⊕ ⊤ ⊕ (p ∧ q)
30+
///
31+
/// This transformation is useful to convert a [`Formula`] into _algebraic normal form_.
32+
pub struct Implication;
33+
34+
impl<T: Clone> RewritingRule<T> for Implication {
35+
fn reduce(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
36+
Err(formula)
37+
}
38+
39+
fn transform(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
40+
if let Formula::Implies(p, q) = formula {
41+
Ok(!p.clone() ^ (p & q))
42+
} else {
43+
Err(formula)
44+
}
45+
}
46+
}
47+
48+
#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Default)]
49+
/// Replace an equivalence in a [`Formula`]
50+
/// with a negation of exclusive disjunctions:
51+
/// `p ↔ q ≡ ¬(p ⊕ q)`
52+
pub struct Equiv;
53+
54+
impl<T> RewritingRule<T> for Equiv {
55+
fn reduce(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
56+
if let Formula::Equivalent(p, q) = formula {
57+
Ok(!(p ^ q))
58+
} else {
59+
Err(formula)
60+
}
61+
}
62+
}
63+
64+
#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Default)]
65+
/// Replace negative literal with a `⊕ ⊤`:
66+
///
67+
/// `¬p ≡ p ⊕ ⊤`
68+
///
69+
/// This transformation is useful to convert a [`Formula`] into _algebraic normal form_.
70+
pub struct NegLiteralAsXor1;
71+
72+
impl<T> RewritingRule<T> for NegLiteralAsXor1 {
73+
fn reduce(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
74+
Err(formula)
75+
}
76+
77+
fn transform(&self, formula: Formula<T>) -> Result<Formula<T>, Formula<T>> {
78+
if let Formula::Not(n) = formula {
79+
Ok(Formula::truth(true) ^ *n)
80+
} else {
81+
Err(formula)
82+
}
83+
}
84+
}
85+
86+
#[cfg(test)]
87+
mod tests {
88+
use crate::TruthTabled as _;
89+
90+
use super::{
91+
super::{examples::reduce_all, RewritingRuleDebug},
92+
*,
93+
};
94+
95+
fn rules<T>() -> Vec<Box<dyn RewritingRuleDebug<T>>>
96+
where
97+
T: PartialEq + Clone,
98+
{
99+
use super::super::*;
100+
101+
vec![
102+
// no `Formula::Dynamic`
103+
Box::new(canonical::NoDynamicConnective),
104+
// no `Formula::Truth` aside from top-level
105+
Box::new(constant::EliminateConstants),
106+
// no `Formula::Not(Formula::Not(...))`
107+
Box::new(neg::DoubleNegation),
108+
// reintroduce `⊤` for `Formula::Not`
109+
Box::new(NegLiteralAsXor1),
110+
// no `Formula::Implies`
111+
Box::new(Implication),
112+
// no `Formula::Equivalent`
113+
Box::new(Equiv),
114+
// no `Formula::And(Formula::Xor(...))`
115+
Box::new(distrib::DistributeConjunctionOverXor),
116+
// no `Formula::Or`
117+
Box::new(DisjunctionToXoredProducts),
118+
// additional rule to prevent repetitions early
119+
// Box::new(eq::Idempotence),
120+
]
121+
}
122+
123+
#[allow(clippy::needless_pass_by_value)]
124+
fn check_equivalent(f: Formula<char>) {
125+
let f2 = reduce_all(f.clone(), true, rules());
126+
assert!(f2.is_equivalent(&f));
127+
}
128+
129+
#[test]
130+
fn example1() {
131+
use crate::formula::Equivalent as _;
132+
133+
let f = Formula::atom('a').equivalent(Formula::atom('b') & (Formula::atom('c') | 'd'));
134+
check_equivalent(f);
135+
}
136+
137+
#[test]
138+
fn example2() {
139+
use crate::formula::{Equivalent as _, Implies as _};
140+
141+
// ¬a↔(d→c)∧a
142+
let f = (!Formula::atom('a')).equivalent(Formula::atom('d').implies('c') & 'a');
143+
check_equivalent(f);
144+
}
145+
146+
#[test]
147+
fn example3() {
148+
use crate::{
149+
connective::{NonConjunction, NonDisjunction},
150+
formula::{AnyConnective, Equivalent as _, Implies as _},
151+
Literal,
152+
};
153+
154+
// ((¬b∧d)⊕((b↑b)↓d))∨(((c→d)→a)↔¬(¬c∨(d∨¬d)))
155+
let f = ((!Formula::atom('b') & 'd')
156+
^ AnyConnective::binary(
157+
NonDisjunction,
158+
(
159+
AnyConnective::binary(NonConjunction, (Formula::atom('b'), Formula::atom('b')))
160+
.into(),
161+
Formula::atom('d'),
162+
),
163+
))
164+
| (Formula::atom('c')
165+
.implies('d')
166+
.implies('a')
167+
.equivalent(!(!Formula::atom('c') | (Formula::atom('d') | Literal::Neg('d')))));
168+
check_equivalent(f);
169+
}
170+
171+
#[test]
172+
fn example4() {
173+
use crate::{
174+
connective::{ConverseImplication, MaterialNonImplication, NonDisjunction},
175+
formula::{AnyConnective, Equivalent as _, Implies as _},
176+
Literal,
177+
};
178+
179+
// (((c↓⊥)↛c)↛¬(⊥←a))∨(((b→a)↔¬b)∨(d∧¬⊥))
180+
let f = Formula::from(AnyConnective::binary(
181+
MaterialNonImplication,
182+
(
183+
AnyConnective::binary(
184+
MaterialNonImplication,
185+
(
186+
AnyConnective::binary(
187+
NonDisjunction,
188+
(Formula::atom('c'), Formula::truth(false)),
189+
)
190+
.into(),
191+
Formula::atom('c'),
192+
),
193+
)
194+
.into(),
195+
!Formula::from(AnyConnective::binary(
196+
ConverseImplication,
197+
(Formula::truth(false), Formula::atom('a')),
198+
)),
199+
),
200+
)) | (Formula::atom('b')
201+
.implies('a')
202+
.equivalent(Literal::Neg('b'))
203+
| (Formula::atom('d') & !Formula::truth(false)));
204+
205+
check_equivalent(f);
206+
}
207+
208+
#[test]
209+
fn example5() {
210+
use crate::{
211+
connective::{
212+
ConverseImplication, MaterialNonImplication, NonConjunction, NonDisjunction,
213+
},
214+
formula::{AnyConnective, Equivalent as _},
215+
Literal,
216+
};
217+
218+
// TODO: investigate why so slow? (~50s)
219+
220+
// (a∨c↛a)∨¬d←(¬b↔(d↓a))↑¬((b∨a)∨¬a)
221+
let f = AnyConnective::binary(
222+
NonConjunction,
223+
(
224+
AnyConnective::binary(
225+
ConverseImplication,
226+
(
227+
Formula::from(AnyConnective::binary(
228+
MaterialNonImplication,
229+
(Formula::atom('a') | 'c', Formula::atom('a')),
230+
)) | !Formula::atom('d'),
231+
(!Formula::atom('b')).equivalent(AnyConnective::binary(
232+
NonDisjunction,
233+
(Formula::atom('d'), Formula::atom('a')),
234+
)),
235+
),
236+
)
237+
.into(),
238+
!(Formula::atom('b') | 'a' | Literal::Neg('a')),
239+
),
240+
);
241+
242+
check_equivalent(f.into());
243+
}
244+
245+
#[test]
246+
fn example6() {
247+
use crate::{
248+
connective::{MaterialNonImplication, NonDisjunction},
249+
formula::{AnyConnective, Equivalent as _, Implies as _},
250+
};
251+
252+
// (a↔(c↛a))↛((c↔(d→b))↛(d↓c))
253+
let f = AnyConnective::binary(
254+
MaterialNonImplication,
255+
(
256+
Formula::atom('a').equivalent(AnyConnective::binary(
257+
MaterialNonImplication,
258+
(Formula::atom('c'), Formula::atom('a')),
259+
)),
260+
AnyConnective::binary(
261+
MaterialNonImplication,
262+
(
263+
Formula::atom('c').equivalent(Formula::atom('d').implies('b')),
264+
AnyConnective::binary(
265+
NonDisjunction,
266+
(Formula::atom('d'), Formula::atom('c')),
267+
)
268+
.into(),
269+
),
270+
)
271+
.into(),
272+
),
273+
);
274+
275+
check_equivalent(f.into());
276+
}
277+
}

0 commit comments

Comments
 (0)