From e78f1442b37ef49520e7e40399266f8a7a5d6875 Mon Sep 17 00:00:00 2001 From: adrienbanse Date: Mon, 23 Oct 2023 13:10:46 +0200 Subject: [PATCH 1/3] remove all BDDUtils --- Project.toml | 2 - src/utils/data_structures/BDD/BDD.jl | 33 ----- src/utils/data_structures/BDD/BitSet.jl | 80 ----------- src/utils/data_structures/BDD/inttupleset.jl | 136 ------------------ test/runtests.jl | 4 - test/utils/data_structures/BDD/test_BDD.jl | 37 ----- .../data_structures/BDD/test_inttupleset.jl | 72 ---------- 7 files changed, 364 deletions(-) delete mode 100644 src/utils/data_structures/BDD/BDD.jl delete mode 100644 src/utils/data_structures/BDD/BitSet.jl delete mode 100644 src/utils/data_structures/BDD/inttupleset.jl delete mode 100644 test/utils/data_structures/BDD/test_BDD.jl delete mode 100644 test/utils/data_structures/BDD/test_inttupleset.jl diff --git a/Project.toml b/Project.toml index 2adcf0692..70ffc07ad 100644 --- a/Project.toml +++ b/Project.toml @@ -5,7 +5,6 @@ version = "0.0.1" [deps] ArnoldiMethod = "ec485272-7323-5ecc-a04f-4719b315124d" -CUDD = "345a2cc7-28d8-58b2-abdf-cff77ea7d7f1" Colors = "5ae59095-9a9b-59fe-a467-6f913c188581" DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8" DiscreteMarkovChains = "8abcb7ef-b365-4f7b-ac38-56893fb62f9f" @@ -44,7 +43,6 @@ Symbolics = "0c5d862f-8b57-4792-8d23-62f2024744c7" [compat] ArnoldiMethod = "0.2" -CUDD = "0.3" Colors = "0.12" DataStructures = "0.18" DiscreteMarkovChains = "0.2" diff --git a/src/utils/data_structures/BDD/BDD.jl b/src/utils/data_structures/BDD/BDD.jl deleted file mode 100644 index d9ab5f9ae..000000000 --- a/src/utils/data_structures/BDD/BDD.jl +++ /dev/null @@ -1,33 +0,0 @@ -module BDD - -using CUDD - -# Helper functions - -# Inline and remove assert later -function cube( - manager::Ptr{CUDD.DdManager}, - vars::Vector{Ptr{CUDD.DdNode}}, - values::Vector{Cint}, -) - @assert length(vars) == length(values) - return CUDD.Cudd_bddComputeCube(manager, vars, values, length(vars)) -end - -@inline _bit(x::T) where {T <: Integer} = iszero(x & one(T)) ? zero(Cint) : one(Cint) - -function phase_rem(x::Int, n::Int) - phase = zeros(Cint, n) - for i in 1:n - if !iszero(x & 1) - phase[i] = one(Cint) - end - x >>= 1 - end - return phase, x -end - -include("BitSet.jl") -include("inttupleset.jl") - -end # module diff --git a/src/utils/data_structures/BDD/BitSet.jl b/src/utils/data_structures/BDD/BitSet.jl deleted file mode 100644 index 78340292a..000000000 --- a/src/utils/data_structures/BDD/BitSet.jl +++ /dev/null @@ -1,80 +0,0 @@ -""" - mutable struct BitSet <: AbstractSet{Int} - -Same as `Base.BitSet` but with `CUDD`. -""" -mutable struct BitSet <: AbstractSet{Int} - manager::Ptr{CUDD.DdManager} - variables::Vector{Ptr{CUDD.DdNode}} - root::Ptr{CUDD.DdNode} - function BitSet() - manager = CUDD.initialize_cudd() - return new(manager, Ptr{CUDD.DdNode}[], CUDD.Cudd_ReadLogicZero(manager)) - end -end - -Base.show(io::IO, set::BitSet) = Base.summary(io, set) -function Base.summary(io::IO, set::BitSet) - n = length(set.variables) - Base.showarg(io, set, true) - print(io, " with ", n, " bit") - if !isone(n) - print(io, "s") - end -end - -Base.eltype(::Type{BitSet}) = Int -Base.empty(::BitSet, ::Type{Int} = Int) = BitSet() -Base.emptymutable(::BitSet, ::Type{Int} = Int) = BitSet() -Base.isempty(set::BitSet) = set.root === CUDD.Cudd_ReadLogicZero(set.manager) -function Base.empty!(set::BitSet) - set.root = CUDD.Cudd_ReadLogicZero(set.manager) - return set -end -Base.IteratorSize(::BitSet) = Base.SizeUnknown() - -phase_rem(x, set::BitSet) = phase_rem(x, length(set.variables)) - -function Base.iterate(set::BitSet, state::Int = 0) - phase, x = phase_rem(state, set) - if iszero(x) - if _in(phase, set) - return (state, state + 1) - else - return iterate(set, state + 1) - end - else - # state would require more variables than what is in `set.variables` - # so it is necessarily not in `set`. - return nothing - end -end - -function phase!(set::BitSet, x::Int) - phase, x = phase_rem(x, set) - while x > 0 - push!(phase, iszero(x & 1) ? zero(Cint) : one(Cint)) - # As the `manager` is only used by this struct, `bddIthVar` should be - # the same as `bddAddVar`. - var = CUDD.Cudd_bddIthVar(set.manager, Cint(length(set.variables))) - push!(set.variables, var) - set.root = - CUDD.Cudd_bddAnd(set.manager, set.root, cube(set.manager, [var], [zero(Cint)])) - x >>= 1 - end - return phase -end -minterm!(set::BitSet, x::Int) = cube(set.manager, set.variables, phase!(set, x)) -function Base.push!(set::BitSet, x::Int) - # `minterm!` modifies `set.root` so we need to call it before the `bddOr` line where we access `set.root`. - minterm = minterm!(set, x) - set.root = CUDD.Cudd_bddOr(set.manager, set.root, minterm) - return set -end -function _in(phase::Vector{Cint}, set::BitSet) - return CUDD.Cudd_Eval(set.manager, set.root, phase) === CUDD.Cudd_ReadOne(set.manager) -end -function Base.in(x::Int, set::BitSet) - phase, x = phase_rem(x, set) - return iszero(x) && _in(phase, set) -end diff --git a/src/utils/data_structures/BDD/inttupleset.jl b/src/utils/data_structures/BDD/inttupleset.jl deleted file mode 100644 index d308020c3..000000000 --- a/src/utils/data_structures/BDD/inttupleset.jl +++ /dev/null @@ -1,136 +0,0 @@ -""" - mutable struct IntTupleSet <: AbstractSet{NTuple{N,Int} where N} - -Same as `Base.Set{NTuple{N,Int} where N}` but with `CUDD`. -""" -mutable struct IntTupleSet{N, T <: Integer} <: AbstractSet{NTuple{N, T}} - manager::Ptr{CUDD.DdManager} - variables::Vector{Ptr{CUDD.DdNode}} - indexes::NTuple{N, Vector{UInt16}} - root::Ptr{CUDD.DdNode} - phase_::Vector{Cint} - vars_::Vector{Ptr{CUDD.DdNode}} - z_::Vector{Cint} -end - -function IntTupleSet{N, T}() where {N, T} - manager = CUDD.initialize_cudd() - variables = Ptr{CUDD.DdNode}[] - indexes = ntuple(i -> UInt16[], N) - root = CUDD.Cudd_ReadLogicZero(manager) - phase_ = Cint[] - z_ = Cint[] - vars_ = Ptr{CUDD.DdNode}[] - return IntTupleSet{N, T}(manager, variables, indexes, root, phase_, vars_, z_) -end -IntTupleSet{N}() where {N} = IntTupleSet{N, Int}() - -Base.show(io::IO, set::IntTupleSet) = Base.summary(io, set) -function Base.summary(io::IO, set::IntTupleSet) - nbits = length.(set.indexes) - Base.showarg(io, set, true) - print(io, " with ", Base.dims2string(nbits), " bit") - return isone(prod(nbits)) || print(io, "s") -end - -Base.eltype(::Type{IntTupleSet{N, T}}) where {N, T} = NTuple{N, T} -Base.empty(::IntTupleSet{N}, ::Type{T} = Int) where {N, T} = IntTupleSet{N, T}() -Base.emptymutable(::IntTupleSet{N}, ::Type{T} = Int) where {N, T} = IntTupleSet{N, T}() -Base.isempty(set::IntTupleSet) = set.root === CUDD.Cudd_ReadLogicZero(set.manager) -function Base.empty!(set::IntTupleSet) - set.root = CUDD.Cudd_ReadLogicZero(set.manager) - return set -end -Base.IteratorSize(::IntTupleSet) = Base.SizeUnknown() - -# `x` will be used to denote a tuple of integers, and `e` to denote its elements - -function _phase_simple!(set, e, i) - for idx in set.indexes[i] - set.phase_[idx] = _bit(e) - e >>= 1 - end - while e > 0 - push!(set.phase_, _bit(e)) - # As the `manager` is only used by this struct, `bddIthVar` should be - # the same as `bddNewVar`. - newidx = length(set.variables) - newvar = CUDD.Cudd_bddIthVar(set.manager, Cint(newidx)) - push!(set.variables, newvar) - push!(set.indexes[i], newidx + 1) - push!(set.vars_, newvar) - push!(set.z_, zero(Cint)) - e >>= 1 - end -end - -function _phase!(set, x) - empty!(set.vars_) - empty!(set.z_) - for (i, e) in enumerate(x) - _phase_simple!(set, e, i) - end -end - -function Base.push!(set::IntTupleSet{N, T}, x::NTuple{N, T}) where {N, T} - _phase!(set, x) - set.root = CUDD.Cudd_bddAnd(set.manager, set.root, cube(set.manager, set.vars_, set.z_)) - set.root = - CUDD.Cudd_bddOr(set.manager, set.root, cube(set.manager, set.variables, set.phase_)) - return set -end - -function Base.delete!(set::IntTupleSet{N, T}, x::NTuple{N, T}) where {N, T <: Integer} - # ∈ updates `set.phase_` - x ∈ set || return set - # Use Nand because `Cudd_Not()` seems not implemented in CUDD - set.root = CUDD.Cudd_bddAnd( - set.manager, - set.root, - CUDD.Cudd_bddNand( - set.manager, - CUDD.Cudd_ReadOne(set.manager), - cube(set.manager, set.variables, set.phase_), - ), - ) - return set -end -Base.delete!(set::IntTupleSet, x) = set - -function _phase_simple_truncated!(set, e, i) - for idx in set.indexes[i] - set.phase_[idx] = _bit(e) - e >>= 1 - end - return iszero(e) -end - -function _phase_truncated!(set, x) - for (i, e) in enumerate(x) - _phase_simple_truncated!(set, e, i) || return i - end - return 0 -end - -function _in(phase, set) - return CUDD.Cudd_Eval(set.manager, set.root, phase) === CUDD.Cudd_ReadOne(set.manager) -end - -function Base.in(x::NTuple{N, T}, set::IntTupleSet{N, T}) where {N, T} - return iszero(_phase_truncated!(set, x)) && _in(set.phase_, set) -end - -# Can we improve this? -@inline _incr_(e::T, i, j) where {T} = i == j ? zero(T) : (i == j + 1 ? e + one(T) : e) -function _increment(x::NTuple{N}, j) where {N} - return ntuple(i -> _incr_(x[i], i, j), Val(N)) -end - -Base.iterate(set::IntTupleSet{N, T}) where {N, T} = - iterate(set, ntuple(i -> zero(T), Val(N))) -function Base.iterate(set::IntTupleSet{N}, state::NTuple{N}) where {N} - I = _phase_truncated!(set, state) - I == N && return nothing - iszero(I) && _in(set.phase_, set) && return (state, _increment(state, 0)) - return iterate(set, _increment(state, I)) -end diff --git a/test/runtests.jl b/test/runtests.jl index aff17d61b..beadad195 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -1,7 +1,3 @@ -# Two following tests temporarily removed, see https://github.com/dionysos-dev/Dionysos.jl/issues/209 -include("./utils/data_structures/BDD/test_BDD.jl") -include("./utils/data_structures/BDD/test_inttupleset.jl") - include("./utils/data_structures/test_queue.jl") include("./utils/data_structures/test_digraph.jl") include("./utils/data_structures/tree.jl") diff --git a/test/utils/data_structures/BDD/test_BDD.jl b/test/utils/data_structures/BDD/test_BDD.jl deleted file mode 100644 index d85233dc0..000000000 --- a/test/utils/data_structures/BDD/test_BDD.jl +++ /dev/null @@ -1,37 +0,0 @@ -using Test -using Dionysos -BDD = Dionysos.Utils.BDD -@testset "BDD.BitSet" begin - set = BDD.BitSet() - @test isempty(set) - @test sprint(show, MIME"text/plain"(), set) == "Dionysos.Utils.BDD.BitSet with 0 bits" - list = [1, 10, 5, 1, 4, 8, 3, 4, 2, 14, 28, 13] - m = maximum(list) - for i in 0:m - @test !(i in set) - end - @test sprint(show, MIME"text/plain"(), set) == "Dionysos.Utils.BDD.BitSet with 0 bits" - @test collect(set) isa Vector{Int} - @test isempty(collect(set)) - expected = BitSet() - for l in list - push!(expected, l) - @test push!(set, l) === set - for i in 0:m - @test (i in set) == (i in expected) - end - @test collect(set) == collect(expected) - end - @test isempty(empty(set)) - @test !isempty(set) - @test isempty(Base.emptymutable(set)) - @test !isempty(set) - @test isempty(empty!(set)) - @test isempty(set) - @test sprint(show, MIME"text/plain"(), set) == "Dionysos.Utils.BDD.BitSet with 5 bits" - push!(set, 40) - @test sprint(show, MIME"text/plain"(), set) in [ - "Dionysos.Utils.BDD.BitSet with 6 bits", # Julia v1.0 - "Dionysos.Utils.BDD.BitSet with 6 bits:\n 40", # Julia v1.5 - ] -end diff --git a/test/utils/data_structures/BDD/test_inttupleset.jl b/test/utils/data_structures/BDD/test_inttupleset.jl deleted file mode 100644 index b94011844..000000000 --- a/test/utils/data_structures/BDD/test_inttupleset.jl +++ /dev/null @@ -1,72 +0,0 @@ -module TestMain - -using Test -using Dionysos -using CUDD - -BDD = Dionysos.Utils.BDD -@testset "IntTupleSet" begin - set = BDD.IntTupleSet{3, Int16}() - @test isempty(set) - @test sprint(show, MIME"text/plain"(), set) == - "Dionysos.Utils.BDD.IntTupleSet{3, Int16} with 0×0×0 bits" - _list = [(1, 2, 3), (1, 5, 6), (1, 9, 8), (1, 6, 8), (4, 5, 6), (7, 6, 4), (1, 2, 3)] - list = [Int16.(x) for x in _list] - m = maximum(maximum(x) for x in list) - for x in Iterators.product((1:m for i in 1:3)...) - @test !(x ∈ set) - end - @test sprint(show, MIME"text/plain"(), set) == - "Dionysos.Utils.BDD.IntTupleSet{3, Int16} with 0×0×0 bits" - @test collect(set) isa Vector{NTuple{3, Int16}} - @test isempty(collect(set)) - set1 = BDD.IntTupleSet{3, Int16}() - set2 = BDD.IntTupleSet{3, UInt16}() - for x in list - push!(set1, x) - push!(set2, UInt16.(x)) - @test push!(set, x) === set - for x in Iterators.product((1:m for i in 1:3)...) - @test (x ∈ set) == (x ∈ set1) == (UInt16.(x) ∈ set2) - end - end - for x in Iterators.product((1:m for i in 1:3)...) - @test (x ∈ set) == (x ∈ list) - @test (UInt16.(x) ∈ set2) == (x ∈ list) - end - for x in set - @test (x ∈ list) - end - for x in set2 - @test eltype(x) == UInt16 - @test (Int16.(x) ∈ list) - end - @test collect(set) == sort!(unique!(list); by = x -> (x[3], x[2], x[1])) - _rem_list = [(1, 2, 3), (4, 5, 6), (1, 3, 2), (1, 2)] - rem_list = [Int16.(x) for x in _rem_list] - for x in rem_list - @test delete!(set, x) === set - end - setdiff!(list, rem_list) - @test collect(set) == sort!(unique!(list); by = x -> (x[3], x[2], x[1])) - for x in rem_list - @test delete!(set, x) === set - end - @test delete!(set, "hello") === set - @test collect(set) == list - @test isempty(empty(set)) - @test !isempty(set) - @test isempty(Base.emptymutable(set)) - @test !isempty(set) - @test isempty(empty!(set)) - @test isempty(set) - @test sprint(show, MIME"text/plain"(), set) == - "Dionysos.Utils.BDD.IntTupleSet{3, Int16} with 3×4×4 bits" - @test push!(set, Int16.((40, 1, 1))) === set - @test sprint(show, MIME"text/plain"(), set) in [ - "Dionysos.Utils.BDD.IntTupleSet{3, Int16} with 6×4×4 bits", # Julia v1.0 - "Dionysos.Utils.BDD.IntTupleSet{3, Int16} with 6×4×4 bits:\n (40, 1, 1)", # Julia v1.5 - ] -end - -end # module TestMain From fb73ea4fb8f1b44b9c0b8e30785b51c0d51efaba Mon Sep 17 00:00:00 2001 From: adrienbanse Date: Mon, 23 Oct 2023 13:22:51 +0200 Subject: [PATCH 2/3] update utils.jl --- src/utils/utils.jl | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/utils/utils.jl b/src/utils/utils.jl index c4bff2d5d..fe0653cd5 100644 --- a/src/utils/utils.jl +++ b/src/utils/utils.jl @@ -12,8 +12,6 @@ include("plotting/colorbar.jl") include("plotting/simple_plots.jl") ##### -# Temporarily remove BDDs -include("data_structures/BDD/BDD.jl") include("scalar_functions.jl") include("data_structures/sorted_vector_set.jl") include("data_structures/queue.jl") From b473f5408b3d8dbe218e61d22a00a18b876275ef Mon Sep 17 00:00:00 2001 From: Adrien Banse <45042779+adrienbanse@users.noreply.github.com> Date: Mon, 23 Oct 2023 13:52:54 +0200 Subject: [PATCH 3/3] Remove BDDs from doc --- docs/src/reference/Utils.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/docs/src/reference/Utils.md b/docs/src/reference/Utils.md index bf3ade174..148566eae 100644 --- a/docs/src/reference/Utils.md +++ b/docs/src/reference/Utils.md @@ -11,8 +11,6 @@ Dionysos.Utils.QuadraticStateControlFunction ## Search ```@docs -Dionysos.Utils.BDD.BitSet -Dionysos.Utils.BDD.IntTupleSet Dionysos.Utils.expand Dionysos.Utils.path_cost Dionysos.Utils.breadth_first_graph_search @@ -43,4 +41,4 @@ Dionysos.Utils.add_node! Dionysos.Utils.propagate_cost_to_leaves Dionysos.Utils.get_path Dionysos.Utils.Tree -``` \ No newline at end of file +```