Module: Cudd::Interface::BDD

Defined in:
lib/cudd-rb/interfaces/bdd.rb

Instance Method Summary collapse

Instance Method Details

#all_cubes(bdd) ⇒ Object

Returns an array with all cubes satisfying ‘bdd`.



312
313
314
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 312

def all_cubes(bdd)
  each_cube(bdd).to_a
end

#and(f, g) ⇒ Object

See Also:

  • Cudd_bddAnd


144
145
146
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 144

def and(f, g)
  bdd Wrapper.bddAnd(native_manager, f, g)
end

#bdd(pointer, &error_handler) ⇒ Object

Coerce ‘pointer` to a BDD



8
9
10
11
12
13
14
15
16
17
18
19
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 8

def bdd(pointer, &error_handler)
  return pointer if Cudd::BDD===pointer
  if FFI::Pointer::NULL==pointer
    raise Cudd::Error, "NULL pointer for BDD" unless error_handler
    error_handler.call
  end
  m = self
  pointer.tap do |p|
    p.instance_eval{ @manager = m }
    p.extend(Cudd::BDD)
  end
end

#bdd2cube(bdd) ⇒ Object

See Also:

  • Cudd_BddToCubeArray


245
246
247
248
249
250
251
252
253
254
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 245

def bdd2cube(bdd)
  s = size
  with_ffi_pointer(:int, s) do |ptr|
    if Wrapper.BddToCubeArray(native_manager, bdd, ptr)==1
      ptr.read_array_of_int(s)
    else
      raise NotACubeError
    end
  end
end

#bdd2dnf(bdd, operators = {:not => :'!', :or => :'|', :and => :'&'}) ⇒ Object

Converts a bdd to a disjunctive normal form



257
258
259
260
261
262
263
264
265
266
267
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 257

def bdd2dnf(bdd, operators = {:not => :'!', :or => :'|', :and => :'&'})
  return "true"  if bdd==one
  return "false" if bdd==zero
  buf, size = "", 0
  each_cube(bdd) do |cube|
    size += 1
    buf << " #{operators[:or]} " unless buf.empty?
    buf << "(" << cube.to_dnf(operators) << ")"
  end
  size == 1 ? buf[1...-1] : buf
end

#cofactor(bdd, cube) ⇒ Object

See Also:

  • Cudd_Cofactor


183
184
185
186
187
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 183

def cofactor(bdd, cube)
  with_bdd_cube(cube) do |c|
    bdd Wrapper.Cofactor(native_manager, bdd, c)
  end
end

#cube(arg, as = :cube) ⇒ Object

Coerces ‘arg` to a cube.

Example (suppose three BDD variables: x, y and z):

cube([1, 0, 2])              # => [1, 0, 2]
cube([1, 0])                 # same
cube([true, false])          # same
cube([x, !y])                # same
cube(x => true, y => false)  # same



227
228
229
230
231
232
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 227

def cube(arg, as = :cube)
  cube = Cube.new(self, arg)
  cube.send(:"to_#{as}")
rescue NoMethodError
  raise ArgumentError, "Invalid 'as' option `#{as}`"
end

#cube2bdd(cube_array) ⇒ Object

See Also:

  • Cudd_CubeArrayToBdd


235
236
237
238
239
240
241
242
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 235

def cube2bdd(cube_array)
  with_ffi_pointer(:int, cube_array.size) do |ptr|
    ptr.write_array_of_int(cube_array)
    bdd Wrapper.CubeArrayToBdd(native_manager, ptr) do
      raise Cudd::Error, "Cudd_CubeArrayToBdd failed on `#{cube_array.inspect}`"
    end
  end
end

#deref(f, recursive = true) ⇒ Object

Uses ‘Cudd_RecursiveDeref` if `recursive` is true (defauts), decreasing reference counts of all children of `f`. Uses `Cudd_Deref` otherwise (use only if your are sure).

See Also:

  • Cudd_RecursiveDeref


34
35
36
37
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 34

def deref(f, recursive = true)
  recursive ? Wrapper.RecursiveDeref(native_manager, f) : Wrapper.Deref(f)
  f
end

#each_cube(bdd) ⇒ Object

See Also:

  • Cudd_ForEachCube


295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 295

def each_cube(bdd)
  return self.enum_for(:each_cube, bdd) unless block_given?
  return unless satisfiable?(bdd)
  size, gen = self.size, nil
  with_ffi_pointer(:pointer) do |cube_pointer|
    with_ffi_pointer(:double) do |value_pointer|
      gen = Wrapper.FirstCube(native_manager, bdd, cube_pointer, value_pointer)
      begin
        yield cube(cube_pointer.read_pointer.read_array_of_int(size))
      end until Wrapper.NextCube(gen, cube_pointer, value_pointer)==0
    end
  end
ensure
  Wrapper.GenFree(gen) if gen
end

#eval(f, cube) ⇒ Object

See Also:

  • Cudd_Eval


272
273
274
275
276
277
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 272

def eval(f, cube)
  with_ffi_pointer(:int, size) do |ptr|
    ptr.write_array_of_int(cube(cube, :a012))
    bdd Wrapper.Eval(native_manager, f, ptr)
  end
end

#exist_abstract(bdd, cube) ⇒ Object Also known as: exist

See Also:

  • Cudd_bddExistAbstract


199
200
201
202
203
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 199

def exist_abstract(bdd, cube)
  with_bdd_cube(cube) do |c|
    bdd Wrapper.bddExistAbstract(native_manager, bdd, c)
  end
end

#is_complement?(bdd) ⇒ Boolean

Returns:

  • (Boolean)

See Also:

  • Cudd_IsComplement


127
128
129
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 127

def is_complement?(bdd)
  (bdd.address & 1)==1
end

#ite(f, g, h) ⇒ Object

See Also:

  • Cudd_bddIte


134
135
136
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 134

def ite(f, g, h)
  bdd Wrapper.bddIte(native_manager, f, g, h)
end

#ith_var(i) ⇒ Object

See Also:

  • Cudd_bddIthVar


75
76
77
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 75

def ith_var(i)
  bdd Wrapper.bddIthVar(native_manager, i)
end

#ith_vars(*args) ⇒ Object

Returns the ith-vars denoted by ‘arg` as an Array of BDDs.

Example:

x, y, z = manager.ith_vars(0, 1, 2)
x, y, z = manager.ith_vars(0..2)
x, y, z = manager.ith_vars([0, 1, 2])



86
87
88
89
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 86

def ith_vars(*args)
  args = args.first if args.size==1
  Array(args).map(&:to_i).map{|i| ith_var(i)}
end

#nand(f, g) ⇒ Object

See Also:

  • Cudd_bddNand


154
155
156
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 154

def nand(f, g)
  bdd Wrapper.bddNand(native_manager, f, g)
end

#new_var(name = nil) ⇒ Object

See Also:

  • Cudd_bddNewVar


92
93
94
95
96
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 92

def new_var(name = nil)
  var = bdd Wrapper.bddNewVar(native_manager)
  var_names[var_index(var)] = name if name
  var
end

#new_vars(first, *args) ⇒ Object

Creates new variables and returns them as an Array.

Example:

x, y, z = manager.new_vars(3)
x, y, z = manager.new_vars(:x, :y, :z)



104
105
106
107
108
109
110
111
112
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 104

def new_vars(first, *args)
  _, first = args.unshift(first), args unless args.empty?
  case first
  when Integer    then (0...first).map{ new_var }
  when Enumerable then first.map{|x| new_var(x) }
  else
    [ new_var(first) ]
  end
end

#nor(f, g) ⇒ Object

See Also:

  • Cudd_bddNor


159
160
161
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 159

def nor(f, g)
  bdd Wrapper.bddNor(native_manager, f, g)
end

#not(f) ⇒ Object

See Also:

  • Cudd_bddNot


139
140
141
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 139

def not(f)
  bdd Wrapper.bddNot(native_manager, f)
end

#one ⇒ Object

See Also:

  • Cudd_ReadOne


117
118
119
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 117

def one
  @one ||= bdd Wrapper.ReadOne(native_manager)
end

#one_cube(bdd) ⇒ Object

Returns the first cube satisfying ‘bdd`.



290
291
292
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 290

def one_cube(bdd)
  each_cube(bdd).first
end

#or(f, g) ⇒ Object

See Also:

  • Cudd_bddOr


149
150
151
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 149

def or(f, g)
  bdd Wrapper.bddOr(native_manager, f, g)
end

#ref(f) ⇒ Object

See Also:

  • Cudd_Ref


24
25
26
27
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 24

def ref(f)
  Wrapper.Ref(f)
  f
end

#restrict(f, g) ⇒ Object

See Also:

  • Cudd_bddRestrict


190
191
192
193
194
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 190

def restrict(f, g)
  with_bdd_cube(g) do |c|
    bdd Wrapper.bddRestrict(native_manager, f, c)
  end
end

#satisfiable?(bdd) ⇒ Boolean

Returns true if ‘bdd` is satisfiable, false otherwise.

Returns:

  • (Boolean) 


280
281
282
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 280

def satisfiable?(bdd)
  !(zero == bdd)
end

#satisfied?(bdd, cube) ⇒ Boolean

Returns true if ‘bdd` is satisfied by a given assignment, false otherwise.

Returns:

  • (Boolean) 


285
286
287
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 285

def satisfied?(bdd, cube)
  one == eval(bdd, cube)
end

#size ⇒ Object Also known as: bdd_count

See Also:

  • Cudd_ReadSize


63
64
65
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 63

def size
  Wrapper.ReadSize(native_manager)
end

#support(bdd) ⇒ Object

See Also:

  • Cudd_Support


176
177
178
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 176

def support(bdd)
  Wrapper.Support(native_manager, bdd)
end

#univ_abstract(bdd, cube) ⇒ Object Also known as: univ, forall

See Also:

  • Cudd_bddUnivAbstract


207
208
209
210
211
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 207

def univ_abstract(bdd, cube)
  with_bdd_cube(cube) do |c|
    bdd Wrapper.bddUnivAbstract(native_manager, bdd, c)
  end
end

#var_index(bdd) ⇒ Object

See Also:

  • Cudd_NodeReadIndex


69
70
71
72
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 69

def var_index(bdd)
  return nil if bdd==zero or bdd==one
  Wrapper.NodeReadIndex(bdd)
end

#var_name(bdd) ⇒ Object

Returns the variable name of a given bdd



56
57
58
59
60
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 56

def var_name(bdd)
  return :zero if bdd==zero
  return :one  if bdd==one
  var_names[var_index(bdd)]
end

#var_names ⇒ Object

Returns the variable names



42
43
44
45
46
47
48
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 42

def var_names
  @var_names ||= []
  (@var_names.size...size).each do |i|
    @var_names[i] = :"v#{i}"
  end if @var_names.size < size
  @var_names
end

#var_names=(names) ⇒ Object

Sets the variable names



51
52
53
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 51

def var_names=(names)
  @var_names = names
end

#xnor(f, g) ⇒ Object

See Also:

  • Cudd_bddXnor


169
170
171
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 169

def xnor(f, g)
  bdd Wrapper.bddXnor(native_manager, f, g)
end

#xor(f, g) ⇒ Object

See Also:

  • Cudd_bddXor


164
165
166
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 164

def xor(f, g)
  bdd Wrapper.bddXor(native_manager, f, g)
end

#zero ⇒ Object

See Also:

  • Cudd_ReadLogicZero


122
123
124
 
# File 'lib/cudd-rb/interfaces/bdd.rb', line 122

def zero
  @zero ||= bdd Wrapper.ReadLogicZero(native_manager)
end