Skip to content

Pldi revisions #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mlb2251 wants to merge 11 commits into
base: pldi_camera_ready
Choose a base branch
from
Open

Pldi revisions #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
4fe5132
refactor monads and add table 1 check
mlb2251 Apr 14, 2025
77e9ea1
tweaks
mlb2251 Apr 14, 2025
e6cf569
cleanup
mlb2251 Apr 14, 2025
0f7529f
cleanup
mlb2251 Apr 14, 2025
2ab5b4b
tweaks
mlb2251 Apr 14, 2025
dcfed57
cleaner thunk unions
mlb2251 Apr 14, 2025
ed17c1f
faster caching approach restored + condition worlds faster
mlb2251 Apr 14, 2025
2b2ab0f
fixed BDD_TRUE typing
mlb2251 Apr 14, 2025
a7b1961
tweaks
mlb2251 Apr 15, 2025
8f4516e
bix mutabiliity bug
mlb2251 Apr 15, 2025
0b660cf
tweak
mlb2251 Apr 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
128 changes: 58 additions & 70 deletions src/RSDD/RSDD.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ export RSDD
module RSDD
using Libdl

export WmcParams, new_weights, wmc_param_f64_set_weight, bdd_wmc
export WmcParams, new_weights, wmc_param_f64_set_weight, bdd_wmc, bdd_true, bdd_false

export BDD,
bdd_and,
Expand Down Expand Up @@ -134,34 +134,39 @@ end
const ManagerPtr = Ptr{Cvoid}
const Label = Csize_t


struct BDD
manager_ptr::ManagerPtr
ptr::Csize_t
function BDD(manager_ptr::ManagerPtr, ptr::Csize_t)
bdd = new(manager_ptr, ptr)
push!(bdds_of_manager_ptr[manager_ptr], bdd)
return bdd
end
end
mutable struct Manager
ptr::ManagerPtr
bdds::Vector{Any}
bdds::Vector{BDD}
freed::Bool
BDD_TRUE::Any
BDD_FALSE::Any
BDD_TRUE::BDD
BDD_FALSE::BDD
weights::AbstractWmcParams

function Manager(; num_vars::Int=0)
manager_ptr = ccall(mk_bdd_manager_default_order_ptr, ManagerPtr, (Cint,), num_vars)
manager_ptr = @rsdd_timed ccall(mk_bdd_manager_default_order_ptr, ManagerPtr, (Cint,), num_vars)
bdds_of_manager_ptr[manager_ptr] = BDD[]
BDD_TRUE = BDD(manager_ptr, @rsdd_timed ccall(bdd_true_ptr, Csize_t, (ManagerPtr,), manager_ptr))
BDD_FALSE = BDD(manager_ptr, @rsdd_timed ccall(bdd_false_ptr, Csize_t, (ManagerPtr,), manager_ptr))
weights = new_weights()
manager = new(manager_ptr, [], false, nothing, nothing, weights)
manager.BDD_TRUE = bdd_true(manager)
manager.BDD_FALSE = bdd_false(manager)
manager = new(manager_ptr, [], false, BDD_TRUE, BDD_FALSE, weights)
@assert !haskey(manager_of_ptr, manager_ptr)
manager_of_ptr[manager_ptr] = manager
return manager
end
end


struct BDD
manager::Manager
ptr::Csize_t
function BDD(manager::Manager, ptr::Csize_t)
bdd = new(manager, ptr)
push!(manager.bdds, bdd)
return bdd
end
end
const bdds_of_manager_ptr = Dict{ManagerPtr, Vector{BDD}}()
const manager_of_ptr = Dict{ManagerPtr, Manager}()



Expand Down Expand Up @@ -229,11 +234,11 @@ Returns: BDD
"""
function bdd_and(a::BDD, b::BDD)
# tstart = time()
@assert a.manager == b.manager "BDDs must belong to the same manager"
ptr = @rsdd_timed ccall(bdd_and_ptr, Csize_t, (ManagerPtr, Csize_t, Csize_t), a.manager.ptr, a.ptr, b.ptr)
@assert a.manager_ptr == b.manager_ptr "BDDs must belong to the same manager"
ptr = @rsdd_timed ccall(bdd_and_ptr, Csize_t, (ManagerPtr, Csize_t, Csize_t), a.manager_ptr, a.ptr, b.ptr)
# tstop = time()
# bdd_time.bdd_and += (tstop - tstart)
return BDD(a.manager, ptr)
return BDD(a.manager_ptr, ptr)
end

"""
Expand All @@ -242,29 +247,29 @@ Returns: BDD
"""
function bdd_or(a::BDD, b::BDD)
# tstart = time()
@assert a.manager == b.manager "BDDs must belong to the same manager"
ptr = @rsdd_timed ccall(bdd_or_ptr, Csize_t, (ManagerPtr, Csize_t, Csize_t), a.manager.ptr, a.ptr, b.ptr)
@assert a.manager_ptr == b.manager_ptr "BDDs must belong to the same manager"
ptr = @rsdd_timed ccall(bdd_or_ptr, Csize_t, (ManagerPtr, Csize_t, Csize_t), a.manager_ptr, a.ptr, b.ptr)
# tstop = time()
# bdd_time.bdd_or += (tstop - tstart)
return BDD(a.manager, ptr)
return BDD(a.manager_ptr, ptr)
end

"""
Performs logical IFF (if and only if) operation on two BDDs.
Returns: BDD
"""
function bdd_iff(a::BDD, b::BDD)
@assert a.manager == b.manager "BDDs must belong to the same manager"
ptr = @rsdd_timed ccall(bdd_iff_ptr, Csize_t, (ManagerPtr, Csize_t, Csize_t), a.manager.ptr, a.ptr, b.ptr)
BDD(a.manager, ptr)
@assert a.manager_ptr == b.manager_ptr "BDDs must belong to the same manager"
ptr = @rsdd_timed ccall(bdd_iff_ptr, Csize_t, (ManagerPtr, Csize_t, Csize_t), a.manager_ptr, a.ptr, b.ptr)
BDD(a.manager_ptr, ptr)
end

"""
Performs logical XOR operation on two BDDs.
Returns: BDD
"""
function bdd_xor(a::BDD, b::BDD)
@assert a.manager == b.manager "BDDs must belong to the same manager"
@assert a.manager_ptr == b.manager_ptr "BDDs must belong to the same manager"
bdd_ite(a, bdd_negate(b), b)
end

Expand All @@ -273,8 +278,8 @@ Negates a BDD.
Returns: BDD
"""
function bdd_negate(bdd::BDD)
ptr = @rsdd_timed ccall(bdd_negate_ptr, Csize_t, (ManagerPtr, Csize_t), bdd.manager.ptr, bdd.ptr)
BDD(bdd.manager, ptr)
ptr = @rsdd_timed ccall(bdd_negate_ptr, Csize_t, (ManagerPtr, Csize_t), bdd.manager_ptr, bdd.ptr)
BDD(bdd.manager_ptr, ptr)
end

"""
Expand All @@ -289,31 +294,13 @@ Returns: Bool
"""
bdd_is_false(bdd::BDD) = @rsdd_timed ccall(bdd_is_false_ptr, Bool, (Csize_t,), bdd.ptr)

"""
Creates a BDD representing the constant true.
Returns: BDD
"""
function bdd_true(manager::Manager)
ptr = @rsdd_timed ccall(bdd_true_ptr, Csize_t, (Manager,), manager)
BDD(manager, ptr)
end

"""
Creates a BDD representing the constant false.
Returns: BDD
"""
function bdd_false(manager::Manager)
ptr = @rsdd_timed ccall(bdd_false_ptr, Csize_t, (Manager,), manager)
BDD(manager, ptr)
end

"""
Performs if-then-else operation on three BDDs.
Returns: BDD
"""
function bdd_ite(f::BDD, g::BDD, h::BDD)
@assert f.manager == g.manager == h.manager "BDDs must belong to the same manager"
ptr = @rsdd_timed ccall(bdd_ite_ptr, Csize_t, (ManagerPtr, Csize_t, Csize_t, Csize_t), f.manager.ptr, f.ptr, g.ptr, h.ptr)
ptr = @rsdd_timed ccall(bdd_ite_ptr, Csize_t, (ManagerPtr, Csize_t, Csize_t, Csize_t), f.manager_ptr, f.ptr, g.ptr, h.ptr)
BDD(f.manager, ptr)
end

Expand All @@ -322,26 +309,26 @@ Checks if two BDDs are equal.
Returns: Bool
"""
function bdd_eq(a::BDD, b::BDD)
@assert a.manager == b.manager "BDDs must belong to the same manager"
@rsdd_timed ccall(bdd_eq_ptr, Bool, (ManagerPtr, Csize_t, Csize_t), a.manager.ptr, a.ptr, b.ptr)
@assert a.manager_ptr == b.manager_ptr "BDDs must belong to the same manager"
@rsdd_timed ccall(bdd_eq_ptr, Bool, (ManagerPtr, Csize_t, Csize_t), a.manager_ptr, a.ptr, b.ptr)
end

"""
Gets the high child of a BDD node.
Returns: BDD
"""
function bdd_high(bdd::BDD)
ptr = @rsdd_timed ccall(bdd_high_ptr, Csize_t, (ManagerPtr, Csize_t), bdd.manager.ptr, bdd.ptr)
BDD(bdd.manager, ptr)
ptr = @rsdd_timed ccall(bdd_high_ptr, Csize_t, (ManagerPtr, Csize_t), bdd.manager_ptr, bdd.ptr)
BDD(bdd.manager_ptr, ptr)
end

"""
Gets the low child of a BDD node.
Returns: BDD
"""
function bdd_low(bdd::BDD)
ptr = @rsdd_timed ccall(bdd_low_ptr, Csize_t, (ManagerPtr, Csize_t), bdd.manager.ptr, bdd.ptr)
BDD(bdd.manager, ptr)
ptr = @rsdd_timed ccall(bdd_low_ptr, Csize_t, (ManagerPtr, Csize_t), bdd.manager_ptr, bdd.ptr)
BDD(bdd.manager_ptr, ptr)
end

"""
Expand Down Expand Up @@ -379,17 +366,17 @@ Existentially quantifies a variable in a BDD.
Returns: BDD
"""
function bdd_exists(bdd::BDD, var::Label)
ptr = @rsdd_timed ccall(bdd_exists_ptr, Csize_t, (ManagerPtr, Csize_t, Label), bdd.manager.ptr, bdd.ptr, var)
BDD(bdd.manager, ptr)
ptr = @rsdd_timed ccall(bdd_exists_ptr, Csize_t, (ManagerPtr, Csize_t, Label), bdd.manager_ptr, bdd.ptr, var)
BDD(bdd.manager_ptr, ptr)
end

"""
Conditions a BDD on a variable.
Returns: BDD
"""
function bdd_condition(bdd::BDD, var::Label, value::Bool)
ptr = @rsdd_timed ccall(bdd_condition_ptr, Csize_t, (ManagerPtr, Csize_t, Label, Bool), bdd.manager.ptr, bdd.ptr, var, value)
BDD(bdd.manager, ptr)
ptr = @rsdd_timed ccall(bdd_condition_ptr, Csize_t, (ManagerPtr, Csize_t, Label, Bool), bdd.manager_ptr, bdd.ptr, var, value)
BDD(bdd.manager_ptr, ptr)
end

"""
Expand All @@ -398,7 +385,7 @@ Returns: BDD
"""
function bdd_compose(f::BDD, var::Label, g::BDD)
@assert f.manager == g.manager "BDDs must belong to the same manager"
ptr = @rsdd_timed ccall(bdd_compose_ptr, Csize_t, (ManagerPtr, Csize_t, Label, Csize_t), f.manager.ptr, f.ptr, var, g.ptr)
ptr = @rsdd_timed ccall(bdd_compose_ptr, Csize_t, (ManagerPtr, Csize_t, Label, Csize_t), f.manager_ptr, f.ptr, var, g.ptr)
BDD(f.manager, ptr)
end

Expand All @@ -418,7 +405,7 @@ bdd_size(bdd::BDD) = @rsdd_timed ccall(bdd_size_ptr, UInt64, (Csize_t,), bdd.ptr
Checks if a BDD represents a variable.
Returns: Bool
"""
bdd_is_var(bdd::BDD) = @rsdd_timed ccall(bdd_is_var_ptr, Bool, (ManagerPtr, Csize_t), bdd.manager.ptr, bdd.ptr)
bdd_is_var(bdd::BDD) = @rsdd_timed ccall(bdd_is_var_ptr, Bool, (ManagerPtr, Csize_t), bdd.manager_ptr, bdd.ptr)

"""
Prints statistics about the BDD manager.
Expand Down Expand Up @@ -453,7 +440,7 @@ end
Checks if a BDD has a variable.
Returns: Bool
"""
bdd_has_variable(bdd::BDD, var::Label) = @rsdd_timed ccall(bdd_has_variable_ptr, Bool, (ManagerPtr, Csize_t, Label), bdd.manager.ptr, bdd.ptr, var)
bdd_has_variable(bdd::BDD, var::Label) = @rsdd_timed ccall(bdd_has_variable_ptr, Bool, (ManagerPtr, Csize_t, Label), bdd.manager_ptr, bdd.ptr, var)

# Convenience operators
Base.:&(a::BDD, b::BDD) = bdd_and(a, b)
Expand Down Expand Up @@ -495,7 +482,7 @@ Performs weighted model counting on a BDD.
Returns: Float64
"""
function bdd_wmc(bdd::BDD)
bdd_wmc_manual(bdd, bdd.manager.weights)
bdd_wmc_manual(bdd, manager_of_ptr[bdd.manager_ptr].weights)
end

function bdd_wmc_manual(bdd::BDD, params::WmcParams)
Expand All @@ -516,10 +503,11 @@ Frees the memory associated with a BDD manager.
function free_bdd_manager(manager::Manager)
free_wmc_params(manager.weights)
manager.freed && return
for bdd in manager.bdds
for bdd in bdds_of_manager_ptr[manager.ptr]
free_bdd(bdd)
end
manager.bdds = []
delete!(bdds_of_manager_ptr, manager.ptr)
delete!(manager_of_ptr, manager.ptr)
manager.freed = true
@rsdd_timed ccall(free_bdd_manager_ptr, Cvoid, (ManagerPtr,), manager.ptr)
end
Expand Down Expand Up @@ -547,7 +535,7 @@ A new BDD representing the variable.
"""
function bdd_new_var_at_position(manager::Manager, position::Integer, polarity::Bool)
ptr = @rsdd_timed ccall(bdd_new_var_at_position_ptr, Csize_t, (ManagerPtr, Csize_t, Bool), manager.ptr, position, polarity)
BDD(manager, ptr)
BDD(manager.ptr, ptr)
end

struct WeightedSampleResult
Expand All @@ -561,17 +549,17 @@ Returns: Tuple of (BDD, Float64) representing the sampled BDD and its probabilit
function weighted_sample(bdd::BDD, wmc_params::WmcParams)
result = @rsdd_timed ccall(robdd_weighted_sample_ptr, WeightedSampleResult,
(ManagerPtr, Csize_t, Ptr{Cvoid}),
bdd.manager.ptr, bdd.ptr, wmc_params.ptr)
bdd.manager_ptr, bdd.ptr, wmc_params.ptr)

sample_bdd = BDD(bdd.manager, result.sample)
sample_bdd = BDD(bdd.manager_ptr, result.sample)
probability = result.probability

return (sample_bdd, probability)
end

function bdd_top_k_paths(bdd::BDD, k::Integer, wmc_params::WmcParams)
ptr = @rsdd_timed ccall(robdd_top_k_paths_ptr, Csize_t, (ManagerPtr, Csize_t, Csize_t, Ptr{Cvoid}), bdd.manager.ptr, bdd.ptr, k, wmc_params.ptr)
BDD(bdd.manager, ptr)
ptr = @rsdd_timed ccall(robdd_top_k_paths_ptr, Csize_t, (ManagerPtr, Csize_t, Csize_t, Ptr{Cvoid}), bdd.manager_ptr, bdd.ptr, k, wmc_params.ptr)
BDD(bdd.manager_ptr, ptr)
end

# Add these to the exports at the end of the file
Expand Down
Loading