#![deny(missing_docs)]
pub const F: u64 = 0b00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000;
pub const P0: u64 = 0b10101010_10101010_10101010_10101010_10101010_10101010_10101010_10101010;
pub const P1: u64 = 0b11001100_11001100_11001100_11001100_11001100_11001100_11001100_11001100;
pub const P2: u64 = 0b11110000_11110000_11110000_11110000_11110000_11110000_11110000_11110000;
pub const P3: u64 = 0b11111111_00000000_11111111_00000000_11111111_00000000_11111111_00000000;
pub const P4: u64 = 0b11111111_11111111_00000000_00000000_11111111_11111111_00000000_00000000;
pub const P5: u64 = 0b11111111_11111111_11111111_11111111_00000000_00000000_00000000_00000000;
pub const T: u64 = 0b11111111_11111111_11111111_11111111_11111111_11111111_11111111_11111111;
pub fn count1<F: FnMut(u64) -> u64>(f: &mut F) -> u32 {((f)(P0) & 0x3).count_ones()}
pub fn count2<F: FnMut(u64, u64) -> u64>(f: &mut F) -> u32 {((f)(P0, P1) & 0xf).count_ones()}
pub fn count3<F: FnMut(u64, u64, u64) -> u64>(f: &mut F) -> u32 {((f)(P0, P1, P2) & 0xff).count_ones()}
pub fn count4<F: FnMut(u64, u64, u64, u64) -> u64>(f: &mut F) -> u32 {((f)(P0, P1, P2, P3) & 0xffff).count_ones()}
pub fn count5<F: FnMut(u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> u32 {
((f)(P0, P1, P2, P3, P4) & 0xffff_ffff).count_ones()
}
pub fn count6<F: FnMut(u64, u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> u32 {
(f)(P0, P1, P2, P3, P4, P5).count_ones()
}
pub fn count7<F: FnMut(u64, u64, u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> u32 {
(f)(P0, P1, P2, P3, P4, P5, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T).count_ones()
}
pub fn count8<F: FnMut(u64, u64, u64, u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> u32 {
(f)(P0, P1, P2, P3, P4, P5, F, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, T).count_ones()
}
pub fn count9<F: FnMut(u64, u64, u64, u64, u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> u32 {
(f)(P0, P1, P2, P3, P4, P5, F, F, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, F, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, T, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, T, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, F, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, F, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, T, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, T, T).count_ones()
}
pub fn count10<F: FnMut(u64, u64, u64, u64, u64, u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> u32 {
(f)(P0, P1, P2, P3, P4, P5, F, F, F, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, F, F, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, F, T, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, F, T, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, T, F, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, T, F, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, T, T, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, F, T, T, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, F, F, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, F, F, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, F, T, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, F, T, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, T, F, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, T, F, T).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, T, T, F).count_ones() +
(f)(P0, P1, P2, P3, P4, P5, T, T, T, T).count_ones()
}
pub fn countn(n: usize, fun: &mut FnMut(&[u64]) -> u64) -> u64 {
match n {
0 => fun(&[]).count_ones() as u64,
1 => count1(&mut |a| fun(&[a])) as u64,
2 => count2(&mut |a, b| fun(&[a, b])) as u64,
3 => count3(&mut |a, b, c| fun(&[a, b, c])) as u64,
4 => count4(&mut |a, b, c, d| fun(&[a, b, c, d])) as u64,
5 => count5(&mut |a, b, c, d, e| fun(&[a, b, c, d, e])) as u64,
6 => count6(&mut |a, b, c, d, e, f| fun(&[a, b, c, d, e, f])) as u64,
7 => count7(&mut |a, b, c, d, e, f, g| fun(&[a, b, c, d, e, f, g])) as u64,
8 => count8(&mut |a, b, c, d, e, f, g, h| fun(&[a, b, c, d, e, f, g, h])) as u64,
9 => count9(&mut |a, b, c, d, e, f, g, h, i| fun(&[a, b, c, d, e, f, g, h, i])) as u64,
10 => count10(&mut |a, b, c, d, e, f, g, h, i, j| fun(&[a, b, c, d, e, f, g, h, i, j])) as u64,
_ => {
if n >= 19 {
let ref mut args = vec![0; n];
let mut sum = 0;
for i in 0..512 {
args[0] = if (i & 0b1) == 0b1 {T} else {F};
args[1] = if (i & 0b10) == 0b10 {T} else {F};
args[2] = if (i & 0b100) == 0b100 {T} else {F};
args[3] = if (i & 0b1000) == 0b1000 {T} else {F};
args[4] = if (i & 0b10000) == 0b10000 {T} else {F};
args[5] = if (i & 0b100000) == 0b100000 {T} else {F};
args[6] = if (i & 0b1000000) == 0b1000000 {T} else {F};
args[7] = if (i & 0b10000000) == 0b10000000 {T} else {F};
args[8] = if (i & 0b100000000) == 0b100000000 {T} else {F};
sum += countn(n-9, &mut |vs: &[u64]| {
for i in 0..n-9 {args[i+9] = vs[i]}
fun(&args)
});
}
sum
} else {
let ref mut args = vec![0; n];
let mut sum = 0;
for i in 0..32 {
args[0] = if (i & 0b1) == 0b1 {T} else {F};
args[1] = if (i & 0b10) == 0b10 {T} else {F};
args[2] = if (i & 0b100) == 0b100 {T} else {F};
args[3] = if (i & 0b1000) == 0b1000 {T} else {F};
args[4] = if (i & 0b10000) == 0b10000 {T} else {F};
sum += countn(n-5, &mut |vs: &[u64]| {
for i in 0..n-5 {args[i+5] = vs[i]}
fun(&args)
});
}
sum
}
}
}
}
pub fn prove1<F: FnMut(u64) -> u64>(f: &mut F) -> bool {count1(f) == 2}
pub fn prove2<F: FnMut(u64, u64) -> u64>(f: &mut F) -> bool {count2(f) == 4}
pub fn prove3<F: FnMut(u64, u64, u64) -> u64>(f: &mut F) -> bool {count3(f) == 8}
pub fn prove4<F: FnMut(u64, u64, u64, u64) -> u64>(f: &mut F) -> bool {count4(f) == 16}
pub fn prove5<F: FnMut(u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> bool {count5(f) == 32}
pub fn prove6<F: FnMut(u64, u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> bool {count6(f) == 64}
pub fn prove7<F: FnMut(u64, u64, u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> bool {count7(f) == 128}
pub fn prove8<F: FnMut(u64, u64, u64, u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> bool {
count8(f) == 256
}
pub fn prove9<F: FnMut(u64, u64, u64, u64, u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> bool {
count9(f) == 512
}
pub fn prove10<F: FnMut(u64, u64, u64, u64, u64, u64, u64, u64, u64, u64) -> u64>(f: &mut F) -> bool {
count10(f) == 1024
}
pub fn proven<F: FnMut(&[u64]) -> u64>(n: usize, f: &mut F) -> bool {
countn(n, f) == 1 << n
}
pub fn prop(a: bool) -> u64 {if a {T} else {F}}
pub fn false_1(_: u64) -> u64 {0}
pub fn not(a: u64) -> u64 {!a}
pub fn id(a: u64) -> u64 {a}
pub fn true_1(_: u64) -> u64 {T}
pub fn false_2(_: u64, _: u64) -> u64 {0}
pub fn and(a: u64, b: u64) -> u64 {a & b}
pub fn or(a: u64, b: u64) -> u64 {a | b}
pub fn xor(a: u64, b: u64) -> u64 {a ^ b}
pub fn eq(a: u64, b: u64) -> u64 {!(a ^ b)}
pub fn imply(a: u64, b: u64) -> u64 {!a | b}
pub fn true_2(_: u64, _: u64) -> u64 {T}
pub fn false_3(_: u64, _: u64, _: u64) -> u64 {0}
pub fn false_4(_: u64, _: u64, _: u64, _: u64) -> u64 {0}
pub fn false_5(_: u64, _: u64, _: u64, _: u64, _: u64) -> u64 {0}
pub fn false_6(_: u64, _: u64, _: u64, _: u64, _: u64, _: u64) -> u64 {0}
pub fn false_7(_: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64) -> u64 {0}
pub fn false_8(_: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64) -> u64 {0}
pub fn false_9(_: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64) -> u64 {0}
pub fn false_10(
_: u64, _: u64, _: u64, _: u64, _: u64,
_: u64, _: u64, _: u64, _: u64, _: u64
) -> u64 {0}
pub fn true_3(_: u64, _: u64, _: u64) -> u64 {T}
pub fn true_4(_: u64, _: u64, _: u64, _: u64) -> u64 {T}
pub fn true_5(_: u64, _: u64, _: u64, _: u64, _: u64) -> u64 {T}
pub fn true_6(_: u64, _: u64, _: u64, _: u64, _: u64, _: u64) -> u64 {T}
pub fn true_7(_: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64) -> u64 {T}
pub fn true_8(_: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64) -> u64 {T}
pub fn true_9(_: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64, _: u64) -> u64 {T}
pub fn true_10(
_: u64, _: u64, _: u64, _: u64, _: u64,
_: u64, _: u64, _: u64, _: u64, _: u64
) -> u64 {T}
pub fn and3(a: u64, b: u64, c: u64) -> u64 {and(and(a, b), c)}
pub fn and4(a: u64, b: u64, c: u64, d: u64) -> u64 {and(and(a, b), and(c, d))}
pub fn and5(a: u64, b: u64, c: u64, d: u64, e: u64) -> u64 {and(and(a, b), and3(c, d, e))}
pub fn and6(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64) -> u64 {
and(and3(a, b, c), and3(d, e, f))
}
pub fn and7(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64) -> u64 {
and(and4(a, b, c, d), and3(e, f, g))
}
pub fn and8(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64, h: u64) -> u64 {
and(and4(a, b, c, d), and4(e, f, g, h))
}
pub fn and9(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64, h: u64, i: u64) -> u64 {
and(and5(a, b, c, d, e), and4(f, g, h, i))
}
pub fn and10(
a: u64, b: u64, c: u64, d: u64, e: u64,
f: u64, g: u64, h: u64, i: u64, j: u64
) -> u64 {
and(and5(a, b, c, d, e), and5(f, g, h, i, j))
}
pub fn andn(vs: &[u64]) -> u64 {
match vs.len() {
0 => T,
1 => vs[0],
2 => and(vs[0], vs[1]),
3 => and3(vs[0], vs[1], vs[2]),
4 => and4(vs[0], vs[1], vs[2], vs[3]),
5 => and5(vs[0], vs[1], vs[2], vs[3], vs[4]),
6 => and6(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5]),
7 => and7(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6]),
8 => and8(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7]),
9 => and9(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7], vs[8]),
10 => and10(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7], vs[8], vs[9]),
_ => and(andn(&vs[..10]), andn(&vs[10..]))
}
}
pub fn or3(a: u64, b: u64, c: u64) -> u64 {or(or(a, b), c)}
pub fn or4(a: u64, b: u64, c: u64, d: u64) -> u64 {or(or(a, b), or(c, d))}
pub fn or5(a: u64, b: u64, c: u64, d: u64, e: u64) -> u64 {or(or3(a, b, c), or(d, e))}
pub fn or6(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64) -> u64 {or(or3(a, b, c), or3(d, e, f))}
pub fn or7(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64) -> u64 {
or(or4(a, b, c, d), or3(e, f, g))
}
pub fn or8(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64, h: u64) -> u64 {
or(or4(a, b, c, d), or4(e, f, g, h))
}
pub fn or9(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64, h: u64, i: u64) -> u64 {
or(or5(a, b, c, d, e), or4(f, g, h, i))
}
pub fn or10(
a: u64, b: u64, c: u64, d: u64, e: u64,
f: u64, g: u64, h: u64, i: u64, j: u64
) -> u64 {
or(or5(a, b, c, d, e), or5(f, g, h, i, j))
}
pub fn orn(vs: &[u64]) -> u64 {
match vs.len() {
0 => F,
1 => vs[0],
2 => or(vs[0], vs[1]),
3 => or3(vs[0], vs[1], vs[2]),
4 => or4(vs[0], vs[1], vs[2], vs[3]),
5 => or5(vs[0], vs[1], vs[2], vs[3], vs[4]),
6 => or6(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5]),
7 => or7(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6]),
8 => or8(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7]),
9 => or9(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7], vs[8]),
10 => or10(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7], vs[8], vs[9]),
_ => or(orn(&vs[..10]), orn(&vs[10..]))
}
}
pub fn xor3(a: u64, b: u64, c: u64) -> u64 {
or(
and(xor(a, b), not(c)),
not(or3(a, b, not(c)))
)
}
pub fn xor4(a: u64, b: u64, c: u64, d: u64) -> u64 {
or(
and(xor3(a, b, c), not(d)),
not(or4(a, b, c, not(d)))
)
}
pub fn xor5(a: u64, b: u64, c: u64, d: u64, e: u64) -> u64 {
or(
and(xor4(a, b, c, d), not(e)),
not(or5(a, b, c, d, not(e)))
)
}
pub fn xor6(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64) -> u64 {
or(
and(xor5(a, b, c, d, e), not(f)),
not(or6(a, b, c, d, e, not(f)))
)
}
pub fn xor7(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64) -> u64 {
or(
and(xor6(a, b, c, d, e, f), not(g)),
not(or7(a, b, c, d, e, f, not(g)))
)
}
pub fn xor8(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64, h: u64) -> u64 {
or(
and(xor7(a, b, c, d, e, f, g), not(h)),
not(or8(a, b, c, d, e, f, g, not(h)))
)
}
pub fn xor9(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64, h: u64, i: u64) -> u64 {
or(
and(xor8(a, b, c, d, e, f, g, h), not(i)),
not(or9(a, b, c, d, e, f, g, h, not(i)))
)
}
pub fn xor10(
a: u64, b: u64, c: u64, d: u64, e: u64,
f: u64, g: u64, h: u64, i: u64, j: u64
) -> u64 {
or(
and(xor9(a, b, c, d, e, f, g, h, i), not(j)),
not(or10(a, b, c, d, e, f, g, h, i, not(j)))
)
}
pub fn xorn(vs: &[u64]) -> u64 {
match vs.len() {
0 => F,
1 => vs[0],
2 => xor(vs[0], vs[1]),
3 => xor3(vs[0], vs[1], vs[2]),
4 => xor4(vs[0], vs[1], vs[2], vs[3]),
5 => xor5(vs[0], vs[1], vs[2], vs[3], vs[4]),
6 => xor6(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5]),
7 => xor7(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6]),
8 => xor8(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7]),
9 => xor9(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7], vs[8]),
10 => xor10(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7], vs[8], vs[9]),
x => {
or(
and(xorn(&vs[..x]), not(vs[x-1])),
not(or(orn(&vs[..x]), not(vs[x-1])))
)
}
}
}
pub fn imply3(a: u64, b: u64, c: u64) -> u64 {and(imply(a, b), imply(b, c))}
pub fn imply4(a: u64, b: u64, c: u64, d: u64) -> u64 {
and3(imply(a, b), imply(b, c), imply(c, d))
}
pub fn imply5(a: u64, b: u64, c: u64, d: u64, e: u64) -> u64 {
and4(imply(a, b), imply(b, c), imply(c, d), imply(d, e))
}
pub fn imply6(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64) -> u64 {
and5(imply(a, b), imply(b, c), imply(c, d), imply(d, e), imply(e, f))
}
pub fn imply7(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64) -> u64 {
and6(imply(a, b), imply(b, c), imply(c, d), imply(d, e), imply(e, f), imply(f, g))
}
pub fn imply8(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64, h: u64) -> u64 {
and7(imply(a, b), imply(b, c), imply(c, d), imply(d, e), imply(e, f), imply(f, g), imply(g, h))
}
pub fn imply9(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64, h: u64, i: u64) -> u64 {
and8(imply(a, b), imply(b, c), imply(c, d), imply(d, e),
imply(e, f), imply(f, g), imply(g, h), imply(h, i))
}
pub fn imply10(
a: u64, b: u64, c: u64, d: u64, e: u64,
f: u64, g: u64, h: u64, i: u64, j: u64,
) -> u64 {
and9(imply(a, b), imply(b, c), imply(c, d), imply(d, e),
imply(e, f), imply(f, g), imply(g, h), imply(h, i), imply(i, j))
}
pub fn implyn(vs: &[u64]) -> u64 {
match vs.len() {
0 => T,
1 => vs[0],
2 => imply(vs[0], vs[1]),
3 => imply3(vs[0], vs[1], vs[2]),
4 => imply4(vs[0], vs[1], vs[2], vs[3]),
5 => imply5(vs[0], vs[1], vs[2], vs[3], vs[4]),
6 => imply6(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5]),
7 => imply7(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6]),
8 => imply8(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7]),
9 => imply9(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7], vs[8]),
10 => imply10(vs[0], vs[1], vs[2], vs[3], vs[4], vs[5], vs[6], vs[7], vs[8], vs[9]),
x => {
and(implyn(&vs[..x]), imply(vs[x-2], vs[x-1]))
}
}
}
pub type Pred1 = fn(u64) -> u64;
pub type Pred2 = fn(u64, u64) -> u64;
pub trait Enumerable: Sized {
fn start() -> Self;
fn inc(&self) -> Option<Self>;
}
impl Enumerable for Pred1 {
fn start() -> Self {false_1}
fn inc(&self) -> Option<Self> {
match *self {
x if x == false_1 => Some(not),
x if x == not => Some(id),
x if x == id => Some(true_1),
x if x == true_1 => None,
_ => panic!("Unknown function"),
}
}
}
impl Enumerable for u8 {
fn start() -> u8 {0}
fn inc(&self) -> Option<Self> {self.checked_add(1)}
}
pub fn any<E: Enumerable + Copy, F: Fn(E) -> u64>(f: &F) -> u64 {
let mut val = E::start();
while let Some(new_val) = E::inc(&val) {
if f(new_val) != F {return T};
val = new_val;
}
F
}
pub fn all<E: Enumerable + Copy, F: Fn(E) -> u64>(f: &F) -> u64 {
let mut val = E::start();
while let Some(new_val) = E::inc(&val) {
if f(new_val) != T {return F};
val = new_val;
}
T
}
pub trait Prove: Sized + Copy {
fn count<F: Fn(Self) -> u64>(f: F) -> u64;
fn prove<F: Fn(Self) -> u64>(f: F) -> bool {
Self::count(f) == Self::count(|_| T)
}
fn does_not_mean<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(
assumption: F, conclusion: G
) -> bool {
!Self::prove(|x| imply(assumption(x), conclusion(x))) &&
!Self::prove(|x| imply(assumption(x), not(conclusion(x))))
}
fn means<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(assumption: F, conclusion: G) -> bool {
Self::prove(|x| imply(assumption(x), conclusion(x))) &&
!Self::prove(|x| imply(assumption(x), not(conclusion(x))))
}
fn eq<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(a: F, b: G) -> bool {
Self::prove(|x| eq(a(x), b(x)))
}
fn exc<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(a: F, b: G) -> bool {
Self::prove(|x| and(
imply(a(x), not(b(x))),
imply(b(x), not(a(x)))
))
}
fn imply<F: Fn(Self) -> u64, G: Fn(Self) -> u64>(a: F, b: G) -> bool {
Self::prove(|x| imply(a(x), b(x)))
}
fn prob<F: Fn(Self) -> u64>(f: F) -> Option<f64> {
let fa = Self::count(|_| F);
let tr = Self::count(|_| T);
let full_rules = tr - fa;
if full_rules == 0 {return None}
else {
Some((Self::count(f) - fa) as f64 / full_rules as f64)
}
}
fn prob_imply<A: Fn(Self) -> u64 + Copy, B: Fn(Self) -> u64>(a: A, b: B) -> Option<f64> {
let fa = Self::count(|_| F);
let count_a = Self::count(a) - fa;
if count_a == 0 {return None}
else {
Some((Self::count(|x| and(a(x), b(x))) - fa) as f64 / count_a as f64)
}
}
}
impl<T> Prove for T where T: Copy + Construct + ExtendRules {
fn count<F: Fn(Self) -> u64>(f: F) -> u64 {
countn(<Self as Construct>::n(), &mut |vs| {
let v: Self = Construct::construct(vs);
imply(v.full_rules(), f(v))
})
}
fn prove<F: Fn(Self) -> u64>(f: F) -> bool {
Self::count(f) == 1 << <Self as Construct>::n()
}
}
pub trait CoreRules {
fn core_rules(&self) -> u64;
}
pub trait ExtendRules: CoreRules {
type Inner: ExtendRules;
fn inner(&self) -> &Self::Inner;
fn extend_rules(&self, inner: &Self::Inner) -> u64;
fn full_rules(&self) -> u64 {
and3(self.core_rules(), self.extend_rules(self.inner()), self.inner().full_rules())
}
}
pub trait BaseSystem: Construct + CoreRules {}
impl<T> ExtendRules for T where T: BaseSystem {
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &Self::Inner) -> u64 {T}
}
impl CoreRules for () {
fn core_rules(&self) -> u64 {T}
}
impl<T0: CoreRules, T1: CoreRules> CoreRules for (T0, T1) {
fn core_rules(&self) -> u64 {
and(self.0.core_rules(), self.1.core_rules())
}
}
impl<T0, T1, T2> CoreRules for (T0, T1, T2)
where T0: CoreRules, T1: CoreRules, T2: CoreRules
{
fn core_rules(&self) -> u64 {
and3(
self.0.core_rules(),
self.1.core_rules(),
self.2.core_rules(),
)
}
}
impl<T0, T1, T2, T3> CoreRules for (T0, T1, T2, T3)
where T0: CoreRules, T1: CoreRules,
T2: CoreRules, T3: CoreRules,
{
fn core_rules(&self) -> u64 {
and4(
self.0.core_rules(),
self.1.core_rules(),
self.2.core_rules(),
self.3.core_rules(),
)
}
}
impl<T0, T1, T2, T3, T4> CoreRules for (T0, T1, T2, T3, T4)
where T0: CoreRules, T1: CoreRules,
T2: CoreRules, T3: CoreRules,
T4: CoreRules,
{
fn core_rules(&self) -> u64 {
and5(
self.0.core_rules(),
self.1.core_rules(),
self.2.core_rules(),
self.3.core_rules(),
self.4.core_rules(),
)
}
}
impl<T0, T1, T2, T3, T4, T5> CoreRules for (T0, T1, T2, T3, T4, T5)
where T0: CoreRules, T1: CoreRules,
T2: CoreRules, T3: CoreRules,
T4: CoreRules, T5: CoreRules,
{
fn core_rules(&self) -> u64 {
and6(
self.0.core_rules(),
self.1.core_rules(),
self.2.core_rules(),
self.3.core_rules(),
self.4.core_rules(),
self.5.core_rules(),
)
}
}
impl<T0, T1, T2, T3, T4, T5, T6> CoreRules for (T0, T1, T2, T3, T4, T5, T6)
where T0: CoreRules, T1: CoreRules,
T2: CoreRules, T3: CoreRules,
T4: CoreRules, T5: CoreRules,
T6: CoreRules,
{
fn core_rules(&self) -> u64 {
and7(
self.0.core_rules(),
self.1.core_rules(),
self.2.core_rules(),
self.3.core_rules(),
self.4.core_rules(),
self.5.core_rules(),
self.6.core_rules(),
)
}
}
impl<T0, T1, T2, T3, T4, T5, T6, T7> CoreRules for (T0, T1, T2, T3, T4, T5, T6, T7)
where T0: CoreRules, T1: CoreRules,
T2: CoreRules, T3: CoreRules,
T4: CoreRules, T5: CoreRules,
T6: CoreRules, T7: CoreRules,
{
fn core_rules(&self) -> u64 {
and8(
self.0.core_rules(),
self.1.core_rules(),
self.2.core_rules(),
self.3.core_rules(),
self.4.core_rules(),
self.5.core_rules(),
self.6.core_rules(),
self.7.core_rules(),
)
}
}
impl<T0, T1, T2, T3, T4, T5, T6, T7, T8> CoreRules for (T0, T1, T2, T3, T4, T5, T6, T7, T8)
where T0: CoreRules, T1: CoreRules,
T2: CoreRules, T3: CoreRules,
T4: CoreRules, T5: CoreRules,
T6: CoreRules, T7: CoreRules,
T8: CoreRules,
{
fn core_rules(&self) -> u64 {
and9(
self.0.core_rules(),
self.1.core_rules(),
self.2.core_rules(),
self.3.core_rules(),
self.4.core_rules(),
self.5.core_rules(),
self.6.core_rules(),
self.7.core_rules(),
self.8.core_rules(),
)
}
}
impl<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> CoreRules for (T0, T1, T2, T3, T4, T5, T6, T7, T8, T9)
where T0: CoreRules, T1: CoreRules,
T2: CoreRules, T3: CoreRules,
T4: CoreRules, T5: CoreRules,
T6: CoreRules, T7: CoreRules,
T8: CoreRules, T9: CoreRules,
{
fn core_rules(&self) -> u64 {
and10(
self.0.core_rules(),
self.1.core_rules(),
self.2.core_rules(),
self.3.core_rules(),
self.4.core_rules(),
self.5.core_rules(),
self.6.core_rules(),
self.7.core_rules(),
self.8.core_rules(),
self.9.core_rules(),
)
}
}
impl ExtendRules for () {
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &()) -> u64 {T}
fn full_rules(&self) -> u64 {T}
}
impl<T0: ExtendRules, T1: ExtendRules> ExtendRules for (T0, T1) {
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &()) -> u64 {T}
}
impl<T0, T1, T2> ExtendRules for (T0, T1, T2)
where T0: ExtendRules, T1: ExtendRules, T2: ExtendRules
{
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &()) -> u64 {T}
}
impl<T0, T1, T2, T3> ExtendRules for (T0, T1, T2, T3)
where T0: ExtendRules, T1: ExtendRules,
T2: ExtendRules, T3: ExtendRules
{
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &()) -> u64 {T}
}
impl<T0, T1, T2, T3, T4> ExtendRules for (T0, T1, T2, T3, T4)
where T0: ExtendRules, T1: ExtendRules,
T2: ExtendRules, T3: ExtendRules,
T4: ExtendRules,
{
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &()) -> u64 {T}
}
impl<T0, T1, T2, T3, T4, T5> ExtendRules for (T0, T1, T2, T3, T4, T5)
where T0: ExtendRules, T1: ExtendRules,
T2: ExtendRules, T3: ExtendRules,
T4: ExtendRules, T5: ExtendRules,
{
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &()) -> u64 {T}
}
impl<T0, T1, T2, T3, T4, T5, T6> ExtendRules for (T0, T1, T2, T3, T4, T5, T6)
where T0: ExtendRules, T1: ExtendRules,
T2: ExtendRules, T3: ExtendRules,
T4: ExtendRules, T5: ExtendRules,
T6: ExtendRules,
{
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &()) -> u64 {T}
}
impl<T0, T1, T2, T3, T4, T5, T6, T7> ExtendRules for (T0, T1, T2, T3, T4, T5, T6, T7)
where T0: ExtendRules, T1: ExtendRules,
T2: ExtendRules, T3: ExtendRules,
T4: ExtendRules, T5: ExtendRules,
T6: ExtendRules, T7: ExtendRules,
{
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &()) -> u64 {T}
}
impl<T0, T1, T2, T3, T4, T5, T6, T7, T8> ExtendRules for (T0, T1, T2, T3, T4, T5, T6, T7, T8)
where T0: ExtendRules, T1: ExtendRules,
T2: ExtendRules, T3: ExtendRules,
T4: ExtendRules, T5: ExtendRules,
T6: ExtendRules, T7: ExtendRules,
T8: ExtendRules,
{
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &()) -> u64 {T}
}
impl<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> ExtendRules
for (T0, T1, T2, T3, T4, T5, T6, T7, T8, T9)
where T0: ExtendRules, T1: ExtendRules,
T2: ExtendRules, T3: ExtendRules,
T4: ExtendRules, T5: ExtendRules,
T6: ExtendRules, T7: ExtendRules,
T8: ExtendRules, T9: ExtendRules,
{
type Inner = ();
fn inner(&self) -> &() {&()}
fn extend_rules(&self, _: &()) -> u64 {T}
}
pub trait Construct: Sized {
fn construct(vs: &[u64]) -> Self;
fn n() -> usize {
use std::mem::size_of;
size_of::<Self>() / size_of::<u64>()
}
}
impl Construct for () {
fn construct(_vs: &[u64]) -> Self {()}
}
impl<T0: Construct, T1: Construct> Construct for (T0, T1) {
fn construct(vs: &[u64]) -> Self {
let n = <T0 as Construct>::n();
(Construct::construct(vs), Construct::construct(&vs[n..]))
}
}
impl<T0, T1, T2> Construct for (T0, T1, T2)
where T0: Construct, T1: Construct, T2: Construct
{
fn construct(vs: &[u64]) -> Self {
let n0 = <T0 as Construct>::n();
let n1 = <T1 as Construct>::n() + n0;
(
Construct::construct(vs),
Construct::construct(&vs[n0..]),
Construct::construct(&vs[n1..])
)
}
}
impl<T0, T1, T2, T3> Construct for (T0, T1, T2, T3)
where T0: Construct, T1: Construct, T2: Construct, T3: Construct
{
fn construct(vs: &[u64]) -> Self {
let n0 = <T0 as Construct>::n();
let n1 = <T1 as Construct>::n() + n0;
let n2 = <T2 as Construct>::n() + n1;
(
Construct::construct(vs),
Construct::construct(&vs[n0..]),
Construct::construct(&vs[n1..]),
Construct::construct(&vs[n2..])
)
}
}
impl<T0, T1, T2, T3, T4> Construct for (T0, T1, T2, T3, T4)
where T0: Construct, T1: Construct,
T2: Construct, T3: Construct,
T4: Construct
{
fn construct(vs: &[u64]) -> Self {
let n0 = <T0 as Construct>::n();
let n1 = <T1 as Construct>::n() + n0;
let n2 = <T2 as Construct>::n() + n1;
let n3 = <T3 as Construct>::n() + n2;
(
Construct::construct(vs),
Construct::construct(&vs[n0..]),
Construct::construct(&vs[n1..]),
Construct::construct(&vs[n2..]),
Construct::construct(&vs[n3..])
)
}
}
impl<T0, T1, T2, T3, T4, T5> Construct for (T0, T1, T2, T3, T4, T5)
where T0: Construct, T1: Construct,
T2: Construct, T3: Construct,
T4: Construct, T5: Construct,
{
fn construct(vs: &[u64]) -> Self {
let n0 = <T0 as Construct>::n();
let n1 = <T1 as Construct>::n() + n0;
let n2 = <T2 as Construct>::n() + n1;
let n3 = <T3 as Construct>::n() + n2;
let n4 = <T4 as Construct>::n() + n3;
(
Construct::construct(vs),
Construct::construct(&vs[n0..]),
Construct::construct(&vs[n1..]),
Construct::construct(&vs[n2..]),
Construct::construct(&vs[n3..]),
Construct::construct(&vs[n4..])
)
}
}
impl<T0, T1, T2, T3, T4, T5, T6> Construct for (T0, T1, T2, T3, T4, T5, T6)
where T0: Construct, T1: Construct,
T2: Construct, T3: Construct,
T4: Construct, T5: Construct,
T6: Construct
{
fn construct(vs: &[u64]) -> Self {
let n0 = <T0 as Construct>::n();
let n1 = <T1 as Construct>::n() + n0;
let n2 = <T2 as Construct>::n() + n1;
let n3 = <T3 as Construct>::n() + n2;
let n4 = <T4 as Construct>::n() + n3;
let n5 = <T5 as Construct>::n() + n4;
(
Construct::construct(vs),
Construct::construct(&vs[n0..]),
Construct::construct(&vs[n1..]),
Construct::construct(&vs[n2..]),
Construct::construct(&vs[n3..]),
Construct::construct(&vs[n4..]),
Construct::construct(&vs[n5..])
)
}
}
impl<T0, T1, T2, T3, T4, T5, T6, T7> Construct for (T0, T1, T2, T3, T4, T5, T6, T7)
where T0: Construct, T1: Construct,
T2: Construct, T3: Construct,
T4: Construct, T5: Construct,
T6: Construct, T7: Construct
{
fn construct(vs: &[u64]) -> Self {
let n0 = <T0 as Construct>::n();
let n1 = <T1 as Construct>::n() + n0;
let n2 = <T2 as Construct>::n() + n1;
let n3 = <T3 as Construct>::n() + n2;
let n4 = <T4 as Construct>::n() + n3;
let n5 = <T5 as Construct>::n() + n4;
let n6 = <T6 as Construct>::n() + n5;
(
Construct::construct(vs),
Construct::construct(&vs[n0..]),
Construct::construct(&vs[n1..]),
Construct::construct(&vs[n2..]),
Construct::construct(&vs[n3..]),
Construct::construct(&vs[n4..]),
Construct::construct(&vs[n5..]),
Construct::construct(&vs[n6..])
)
}
}
impl<T0, T1, T2, T3, T4, T5, T6, T7, T8> Construct for (T0, T1, T2, T3, T4, T5, T6, T7, T8)
where T0: Construct, T1: Construct,
T2: Construct, T3: Construct,
T4: Construct, T5: Construct,
T6: Construct, T7: Construct,
T8: Construct
{
fn construct(vs: &[u64]) -> Self {
let n0 = <T0 as Construct>::n();
let n1 = <T1 as Construct>::n() + n0;
let n2 = <T2 as Construct>::n() + n1;
let n3 = <T3 as Construct>::n() + n2;
let n4 = <T4 as Construct>::n() + n3;
let n5 = <T5 as Construct>::n() + n4;
let n6 = <T6 as Construct>::n() + n5;
let n7 = <T7 as Construct>::n() + n6;
(
Construct::construct(vs),
Construct::construct(&vs[n0..]),
Construct::construct(&vs[n1..]),
Construct::construct(&vs[n2..]),
Construct::construct(&vs[n3..]),
Construct::construct(&vs[n4..]),
Construct::construct(&vs[n5..]),
Construct::construct(&vs[n6..]),
Construct::construct(&vs[n7..])
)
}
}
impl<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> Construct for (T0, T1, T2, T3, T4, T5, T6, T7, T8, T9)
where T0: Construct, T1: Construct,
T2: Construct, T3: Construct,
T4: Construct, T5: Construct,
T6: Construct, T7: Construct,
T8: Construct, T9: Construct
{
fn construct(vs: &[u64]) -> Self {
let n0 = <T0 as Construct>::n();
let n1 = <T1 as Construct>::n() + n0;
let n2 = <T2 as Construct>::n() + n1;
let n3 = <T3 as Construct>::n() + n2;
let n4 = <T4 as Construct>::n() + n3;
let n5 = <T5 as Construct>::n() + n4;
let n6 = <T6 as Construct>::n() + n5;
let n7 = <T7 as Construct>::n() + n6;
let n8 = <T8 as Construct>::n() + n7;
(
Construct::construct(vs),
Construct::construct(&vs[n0..]),
Construct::construct(&vs[n1..]),
Construct::construct(&vs[n2..]),
Construct::construct(&vs[n3..]),
Construct::construct(&vs[n4..]),
Construct::construct(&vs[n5..]),
Construct::construct(&vs[n6..]),
Construct::construct(&vs[n7..]),
Construct::construct(&vs[n8..])
)
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_2() {
assert_eq!(count1(&mut false_1), 0);
assert_eq!(count1(&mut not), 1);
assert_eq!(count1(&mut id), 1);
assert_eq!(count1(&mut true_1), 2);
assert_eq!(count2(&mut false_2), 0);
assert_eq!(count2(&mut and), 1);
assert_eq!(count2(&mut xor), 2);
assert_eq!(count2(&mut eq), 2);
assert_eq!(count2(&mut or), 3);
assert_eq!(count2(&mut true_2), 4);
assert_eq!(count2(&mut imply), 3);
assert_eq!(count2(&mut |a, b| imply(and(a, b), or(a, b))), 4);
assert_eq!(count3(&mut |a, b, c| and(or(a, b), and(a, c))), 2);
assert_eq!(count4(&mut |a, b, c, d| and(or(a, b), or(c, d))), 9);
assert_eq!(count5(&mut |_, _, _, _, _| T), 32);
assert_eq!(count6(&mut |_, _, _, _, _, _| T), 64);
assert_eq!(count7(&mut |_, _, _, _, _, _, _| T), 128);
assert_eq!(count8(&mut |_, _, _, _, _, _, _, _| T), 256);
assert_eq!(count9(&mut |_, _, _, _, _, _, _, _, _| T), 512);
assert_eq!(count10(&mut |_, _, _, _, _, _, _, _, _, _| T), 1024);
}
}