Module: Gisele::Analysis::Mixin::BddManagement

Included in:
Compiling::Processor, Ghmsc, Glts, Glts::Determinize, Glts::Eclosure, Glts::Invariants, Glts::Minimize, Session, Variable
Defined in:
lib/gisele/analysis/mixin/bdd_management.rb

Instance Method Summary collapse

Instance Method Details

#bdd(expr) ⇒ Object 



28
29
30
31
32
33
34
35
36
37
38
39
40
 
# File 'lib/gisele/analysis/mixin/bdd_management.rb', line 28

def bdd(expr)
  case expr
  when Cudd::BDD  then expr
  when Variable   then expr.bdd
  when Symbol     then variable(expr, true).bdd
  when Sexpr      then Compiling::Boolexpr2BDD.call(self, expr)
  when String     then bdd(Gisele.sexpr Gisele.parse(expr, :root => :bool_expr))
  when TrueClass  then bdd_interface.one
  when FalseClass then bdd_interface.zero
  else
    raise ArgumentError, "Unable to compile `#{expr}` to a BDD"
  end
end

#bdd_interface ⇒ Object 



9
10
11
 
# File 'lib/gisele/analysis/mixin/bdd_management.rb', line 9

def bdd_interface
  cudd_manager.interface(:BDD)
end

#cudd_manager ⇒ Object 



5
6
7
 
# File 'lib/gisele/analysis/mixin/bdd_management.rb', line 5

def cudd_manager
  session.cudd_manager
end

#one ⇒ Object 



13
14
15
 
# File 'lib/gisele/analysis/mixin/bdd_management.rb', line 13

def one
  bdd_interface.one
end

#with_bdd(*bdds) ⇒ Object 



21
22
23
24
25
26
 
# File 'lib/gisele/analysis/mixin/bdd_management.rb', line 21

def with_bdd(*bdds)
  bdds.each{|bdd| bdd.ref}
  yield(*bdds)
ensure
  bdds.each{|bdd| bdd.deref}
end

#zero ⇒ Object 



17
18
19
 
# File 'lib/gisele/analysis/mixin/bdd_management.rb', line 17

def zero
  bdd_interface.zero
end