-
Notifications
You must be signed in to change notification settings - Fork 4
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
clean folder structure and additional readme changes
- Loading branch information
1 parent
cf2d801
commit e3c7874
Showing
226 changed files
with
1,826 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,66 @@ | ||
using Revise | ||
using Dice | ||
using BenchmarkTools | ||
|
||
# localARGS = ARGS | ||
# num_bits = parse(Int64, localARGS[1]) | ||
|
||
|
||
|
||
function less(num_bits) | ||
nbpow = 2^num_bits | ||
# code = @dice begin | ||
a = discrete(DistUInt{num_bits+1}, [1/nbpow for _ in 1:nbpow]) | ||
b = discrete(DistUInt{num_bits+1}, [1/nbpow for _ in 1:nbpow]) | ||
# c = (a < b) | ||
# return c | ||
# end | ||
#~begin less | ||
return pr(a < b) | ||
end | ||
|
||
function equal(num_bits) | ||
nbpow = 2^num_bits | ||
|
||
a = discrete(DistUInt{num_bits+1}, [1/nbpow for _ in 1:nbpow]) | ||
b = discrete(DistUInt{num_bits+1}, [1/nbpow for _ in 1:nbpow]) | ||
|
||
#~begin less | ||
return pr(prob_equals(a, b)) | ||
end | ||
|
||
function add(num_bits) | ||
nbpow = 2^num_bits | ||
|
||
a = discrete(DistUInt{num_bits+1}, [1/nbpow for _ in 1:nbpow]) | ||
b = discrete(DistUInt{num_bits+1}, [1/nbpow for _ in 1:nbpow]) | ||
|
||
#~begin less | ||
return expectation(a + b) | ||
end | ||
#~end | ||
|
||
#~begin equals | ||
println(pr(prob_equals(a, b))) | ||
#~end | ||
|
||
#~begin sum | ||
println(expectation(a + b)) | ||
|
||
for i = 14:15 | ||
t = @benchmark c = less($i) | ||
med = ((median(t).time)/10^9) | ||
@show (i, med) | ||
end | ||
|
||
for i = 1:15 | ||
t = @benchmark c = equal($i) | ||
med = ((median(t).time)/10^9) | ||
@show (i, med) | ||
end | ||
|
||
for i = 1:15 | ||
t = @benchmark c = add($i) | ||
med = ((median(t).time)/10^9) | ||
@show (i, med) | ||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,65 @@ | ||
using Dice | ||
using BenchmarkTools | ||
|
||
# localARGS = ARGS | ||
# num_bits = parse(Int64, localARGS[1]) | ||
|
||
|
||
|
||
function less(num_bits) | ||
nbpow = 2^num_bits | ||
# code = @dice begin | ||
a = discrete(DistUIntOH{nbpow}, [1/nbpow for _ in 1:nbpow]) | ||
b = discrete(DistUIntOH{nbpow}, [1/nbpow for _ in 1:nbpow]) | ||
# c = (a < b) | ||
# return c | ||
# end | ||
#~begin less | ||
return pr(a < b) | ||
end | ||
|
||
function equal(num_bits) | ||
nbpow = 2^num_bits | ||
|
||
a = discrete(DistUIntOH{nbpow}, [1/nbpow for _ in 1:nbpow]) | ||
b = discrete(DistUIntOH{nbpow}, [1/nbpow for _ in 1:nbpow]) | ||
|
||
#~begin less | ||
return pr(prob_equals(a, b)) | ||
end | ||
|
||
function add(num_bits) | ||
nbpow = 2^num_bits | ||
|
||
a = discrete(DistUIntOH{2 * nbpow}, [1/nbpow for _ in 1:nbpow]) | ||
b = discrete(DistUIntOH{2 * nbpow}, [1/nbpow for _ in 1:nbpow]) | ||
|
||
#~begin less | ||
return expectation(a + b) | ||
end | ||
#~end | ||
|
||
#~begin equals | ||
# println(pr(prob_equals(a, b))) | ||
#~end | ||
|
||
#~begin sum | ||
# println(expectation(a + b)) | ||
|
||
# for i = 1:15 | ||
# t = @benchmark c = less($i) | ||
# med = ((median(t).time)/10^9) | ||
# @show (i, med) | ||
# end | ||
|
||
# for i = 1:15 | ||
# t = @benchmark c = equal($i) | ||
# med = ((median(t).time)/10^9) | ||
# @show (i, med) | ||
# end | ||
|
||
for i = 7:7 | ||
t = @benchmark c = add($i) | ||
med = ((median(t).time)/10^9) | ||
@show (i, med) | ||
end |
147 changes: 147 additions & 0 deletions
147
experiments/microbenchmarks/Problog_binary/binary.problog
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,147 @@ | ||
%%%%%% SHARED SETUP %%%%%% | ||
|
||
num_bits(N) :- cmd_args([NAtom]), atom_number(NAtom, N). | ||
|
||
is_var(a). | ||
is_var(b). | ||
|
||
not(f, t). | ||
not(t, f). | ||
xor(f, f, f). | ||
xor(f, t, t). | ||
xor(t, f, t). | ||
xor(t, t, f). | ||
and(f, f, f). | ||
and(f, t, f). | ||
and(t, f, f). | ||
and(t, t, t). | ||
or(f, f, f). | ||
or(f, t, t). | ||
or(t, f, t). | ||
or(t, t, t). | ||
eq(f, f, t). | ||
eq(f, t, f). | ||
eq(t, f, f). | ||
eq(t, t, t). | ||
lt(f, f, f). | ||
lt(f, t, t). | ||
lt(t, f, f). | ||
lt(t, t, f). | ||
at_least_two_of_three(f, f, f, f). | ||
at_least_two_of_three(f, f, t, f). | ||
at_least_two_of_three(f, t, f, f). | ||
at_least_two_of_three(f, t, t, t). | ||
at_least_two_of_three(t, f, f, f). | ||
at_least_two_of_three(t, f, t, t). | ||
at_least_two_of_three(t, t, f, t). | ||
at_least_two_of_three(t, t, t, t). | ||
ite(t, X, Y, X). | ||
ite(f, X, Y, Y). | ||
|
||
% Flips are id'd by var and a list/bitstring. | ||
% See the BDD proofs to see how to choose probability of a particular list's | ||
% flip to create any discrete distribution. | ||
% Because we are generating uniforms, it's always 0.5. | ||
0.5::flip(X, f); 0.5::flip(X, t). | ||
|
||
ite(t, X, Y, X). | ||
ite(f, X, Y, Y). | ||
|
||
var_i_to_flip_bitstring(Var, 1, []) :- | ||
is_var(Var). | ||
|
||
var_i_to_flip_bitstring(Var, I, [Val | L]) :- | ||
is_var(Var), | ||
I > 1, | ||
Im1 is I - 1, | ||
var_i_to_flip_bitstring(Var, Im1, L), | ||
bit(Var, Im1, Val). | ||
|
||
bit(Var, I, Val) :- | ||
is_var(Var), | ||
num_bits(N), | ||
between(1, N, I), | ||
var_i_to_flip_bitstring(Var, I, L), | ||
flip([Var, L], Val). | ||
|
||
%~begin less | ||
%%%%%% LESS THAN %%%%%% | ||
|
||
less_than(X, Y, 1, Res) :- bit(X, 1, X1), bit(Y, 1, Y1), lt(X1, Y1, Res). | ||
less_than(X, Y, I, Res) :- | ||
bit(X, I, Xi), bit(Y, I, Yi), | ||
Im1 is I - 1, less_than(X, Y, Im1, SuffixLess), | ||
lt(Xi, Yi, HighestLess), | ||
eq(Xi, Yi, HighestEq), | ||
and(SuffixLess, HighestEq, SuffixLessAndHighestEq), | ||
or(HighestLess, SuffixLessAndHighestEq, Res). | ||
|
||
less_than(X, Y, Res) :- num_bits(N), less_than(X, Y, N, Res). | ||
|
||
query(less_than(a, b, t)). | ||
%~end | ||
|
||
%~begin equals | ||
%%%%%% EQUALS %%%%%% | ||
|
||
equals(X, Y, 1, Res) :- bit(X, 1, X1), bit(Y, 1, Y1), eq(X1, Y1, Res). | ||
equals(X, Y, I, Res) :- | ||
bit(X, I, Xi), bit(Y, I, Yi), | ||
Im1 is I - 1, equals(X, Y, Im1, SuffixEq), | ||
eq(Xi, Yi, HighestEq), | ||
and(SuffixEq, HighestEq, Res). | ||
|
||
equals(X, Y, Res) :- num_bits(N), equals(X, Y, N, Res). | ||
|
||
query(equals(a, b, t)). | ||
%~end | ||
|
||
%~begin sum | ||
%%%%%% ADDITION %%%%%% | ||
|
||
add_carry_in(X, Y, 1, f). | ||
add_carry_in(X, Y, I, Res) :- | ||
Im1 is I - 1, | ||
bit(X, Im1, Xi1), | ||
bit(Y, Im1, Yi1), | ||
add_carry_in(X, Y, Im1, Carry1), | ||
at_least_two_of_three(Xi1, Yi1, Carry1, Res). | ||
|
||
bit(add(X, Y), I, Res) :- | ||
bit(X, I, Xi), bit(Y, I, Yi), | ||
add_carry_in(X, Y, I, Carry), | ||
xor(Xi, Yi, Xor1), | ||
xor(Xor1, Carry, Res). | ||
|
||
final_carry(X, Y, Res) :- | ||
num_bits(N), | ||
Np1 is N + 1, | ||
add_carry_in(a, b, Np1, Res). | ||
|
||
query(bit(add(a, b), _, t)). | ||
query(final_carry(a, b, t)). | ||
%~end | ||
|
||
%~begin _ | ||
%%%%%% ADDITION - MATERIALIZE VALUE FOR TESTING %%%%%% | ||
|
||
bit_val(X, I, Res) :- bit(X, I, Xi), IPow is 2 ** (I - 1), ite(Xi, IPow, 0, Res). | ||
|
||
val_of(X, 0, 0). | ||
val_of(X, I, Res) :- | ||
I > 0, | ||
Im1 is I - 1, | ||
val_of(X, Im1, PrevRes), | ||
bit_val(X, I, Val), | ||
Res is PrevRes + Val. | ||
|
||
add_val(X, Y, Res) :- | ||
num_bits(N), | ||
val_of(add(X, Y), N, SumWithoutCarry), | ||
final_carry(X, Y, FinalCarry), | ||
NPow is 2 ** N, | ||
ite(FinalCarry, NPow, 0, FinalCarryVal), | ||
Res is SumWithoutCarry + FinalCarryVal. | ||
|
||
query(add_val(a, b, _)). | ||
%~end |
Oops, something went wrong.