square_trick

actual_square.txt

@@ -0,0 +1,20 @@
+41
+93
+197
+387
+782
+1558
+3114
+6231
+12465
+24891
+49826
+99812
+199358
+398938
+797880
+1596582
+3194034
+6388255
+12776280
+25552902

examples/sample/standard_gaussian_observe_test.jl

@@ -1,28 +1,34 @@
 using Revise
 using Dice
 using Distributions
+using DelimitedFiles
 
 # The density of a normal distribution is as follows:
 # 
 #   1/√2πσ^2  e^{-(x - μ)^2/2σ^2}
 #
 
-# function standard_gaussian_observe(x::DistFix{W, F}) where {W, F}
+naive_observe = Vector(undef, 20)
 
-W = 6
-F = 2
-DFiP = DistFix{W, F}
-x = uniform(DFiP, 3)
+for i in 1:20
+    W = 4 + i
+    F = i
+    DFiP = DistFix{W, F}
+    x = uniform(DFiP, i+4)
 
-normal = bitblast(DFiP, Normal(0, 1), 8, -8.0, 8.0)
+    normal = bitblast(DFiP, Normal(0, 1), 8, -8.0, 8.0)
 
-code = @dice begin 
-                observe(prob_equals(x, normal))
-                x
+    code = @dice begin 
+                    observe(prob_equals(x, normal))
+                    x
+    end
+
+    naive_observe[i] = num_nodes(allobservations(code))
+    io = open("naive_observe.txt", "a")
+    writedlm(io, [naive_observe[i]])
+    close(io)
 end
 
-pr(code)
-num_nodes(allobservations(code))
 
 function squarex(x::DistFix{W, F}) where {W, F}
     square_coeff = Matrix(undef, W, W)
@@ -40,42 +46,67 @@ function squarex(x::DistFix{W, F}) where {W, F}
     square_coeff
 end
 
-code2 = @dice begin
-    x = uniform(DFiP, 3)
-    squared_x = x*x
-    for i in 1:length(squared_x.mantissa.number.bits)
-        flip_param = exp(-2.0^(W-F-i-1))
-        # flip_param = flip_param/(1+flip_param)
-        if squared_x.mantissa.number.bits[i] observe(flip(flip_param)) else true end
-        # observe(prob_equals(squared_x.mantissa.number.bits[i], flip(flip_param)))
+actual_square = Vector(undef, 20)
+
+for i in 1:20
+    W = 4 + i
+    F = i
+    DFiP = DistFix{W, F}
+    x = uniform(DFiP, i+4)
+    code2 = @dice begin
+        squared_x = x*x
+        for i in 1:length(squared_x.mantissa.number.bits)
+            flip_param = exp(-2.0^(W-F-i-1))
+            observe(!squared_x.mantissa.number.bits[i] | (squared_x.mantissa.number.bits[i] & flip(flip_param)))
+        end
+        x
     end
-    x
+
+    actual_square[i] = num_nodes(allobservations(code2))
+    io = open("actual_square.txt", "a")
+    writedlm(io, [actual_square[i]])
+    close(io)
 end
 
-pr(code2)
-
-num_nodes(allobservations(code2))
-
-code3 = @dice begin
-            x = uniform(DFiP, 3)
-            squared_x = squarex(x)
-            for i in 1:W
-                for j in 1:i
-                    i_hat = 2.0^(W-F-i)
-                    j_hat = 2.0^(W-F-j)
-                    if i==j
-                        flip_param = exp(-i_hat * j_hat/2)
-                    else
-                        flip_param = exp(-i_hat * j_hat)
+
+square_trick = Vector(undef, 20)
+
+for i in 10:10
+    W = 4 + i
+    F = i
+    DFiP = DistFix{W, F}
+    x = uniform(DFiP, i+4)
+    code3 = @dice begin
+                squared_x = squarex(x)
+                for i in 1:W
+                    for j in 1:i
+                        i_hat = 2.0^(W-F-i)
+                        j_hat = 2.0^(W-F-j)
+                        if i==j
+                            flip_param = exp(-i_hat * j_hat/2)
+                        else
+                            flip_param = exp(-i_hat * j_hat)
+                        end
+                        observe(!squared_x[i, j] | (squared_x[i, j] & flip(flip_param)))
                     end
-                    # if squared_x[i, j] observe(flip(flip_param)) else true end
-                    # squared_x[i, j] && observe(flip(flip_param))
-                    observe(!squared_x[i, j] | (squared_x[i, j] & flip(flip_param)))
                 end
-            end
-            x
-end
+                x
+    end
 
-pr(code3)
+    dump_dot(allobservations(code3), filename="square_trick.dot")
+
+    square_trick[i] = num_nodes(allobservations(code3))
+    io = open("square_trick.txt", "a")
+    writedlm(io, [square_trick[i]])
+    close(io)
+
+end
 
-num_nodes(allobservations(code3))
+using Plots
+naive_observe = readdlm("naive_observe.txt")
+actual_square = readdlm("actual_square.txt")
+square_trick = readdlm("square_trick.txt")
+plot(naive_observe, marker=:dot, labels = "prob_equals", xlabel="# bits", ylabel="# BDD Nodes", yaxis=:log, legend=:topleft)
+plot!(actual_square, marker=:dot, labels = "x*x")
+plot!(square_trick, marker=:dot, labels = "square_matrix")
+savefig("square_tricks.png")

naive_observe.txt

@@ -0,0 +1,17 @@
+174
+357
+724
+1459
+2930
+5873
+11760
+23535
+47086
+94189
+188396
+376811
+753642
+1507305
+3014632
+6029287
+12058598