Permalink
Browse files

Rephrase in terms of Cubes, for which a class is implemented.

  • Loading branch information...
1 parent a5aaf83 commit ca9f2c1aea31574d6c072c318793851e4656159d @blambeau committed Jul 19, 2012
View
3 lib/cudd-rb.rb
@@ -42,4 +42,5 @@ def self.manager(opts = {})
require_relative "cudd-rb/errors"
require_relative "cudd-rb/wrapper"
require_relative "cudd-rb/manager"
-require_relative "cudd-rb/bdd"
+require_relative "cudd-rb/bdd"
+require_relative "cudd-rb/cube"
View
2 lib/cudd-rb/bdd.rb
@@ -41,7 +41,7 @@ def one?
define_delegate_methods(:* => :and, :+ => :or, :~ => :not)
define_delegate_methods(:eval, :satisfiable?, :satisfied?)
- define_delegate_methods(:each_sat, :one_sat, :all_sat)
+ define_delegate_methods(:each_cube, :one_cube, :all_cubes)
define_delegate_methods(:support)
View
80 lib/cudd-rb/cube.rb
@@ -0,0 +1,80 @@
+module Cudd
+ class Cube
+
+ attr_reader :interface
+
+ def initialize(interface, a012)
+ @interface = interface
+ @a012 = a012.freeze
+ end
+
+ def self.new(interface, arg)
+ return arg if arg.is_a?(Cube)
+ if arg.is_a?(BDD)
+ super(interface, interface.bdd2cube(arg))
+ else
+ a012 = Array.new(interface.size, 2)
+ enum = arg.is_a?(Hash) ? arg.each_pair : arg.each_with_index
+ enum.each do |k,v|
+ k,v = v,k unless arg.is_a?(Hash)
+ index = [k, v].find{|x| x.is_a?(Cudd::BDD) }.index rescue k
+ a012[index] = truth_to_012(v)
+ end
+ super(interface, a012)
+ end
+ end
+
+ def hash
+ @hash ||= to_a012.hash + 37*interface.hash
+ end
+
+ def ==(other)
+ return nil unless other.is_a?(Cube) && other.interface==interface
+ to_a012 == other.to_a012
+ end
+
+ def to_cube
+ self
+ end
+
+ def to_a012
+ @a012
+ end
+
+ def to_bdd
+ interface.cube2bdd(to_a012)
+ end
+
+ def to_truths
+ to_a012.map{|x| Cube.arg012_to_truth(x)}
+ end
+
+ def to_hash
+ h = {}
+ to_a012.each_with_index do |val,index|
+ truth = Cube.arg012_to_truth(val)
+ h[interface.ith_var(index)] = truth unless truth.nil?
+ end
+ h
+ end
+
+ private
+
+ def self.arg012_to_truth(arg012)
+ arg012 <= 1 ? (arg012 == 1) : nil
+ end
+
+ def self.truth_to_012(truth)
+ case truth
+ when Cudd::BDD then truth.is_complement? ? 0 : 1
+ when Integer then (truth >= 0 and truth <= 1) ? truth : 2
+ when TrueClass then 1
+ when FalseClass then 0
+ when NilClass then 2
+ else
+ raise ArgumentError, "Invalid truth value #{truth}"
+ end
+ end
+
+ end # class Cube
+end # module Cudd
View
66 lib/cudd-rb/interfaces/bdd.rb
@@ -213,18 +213,6 @@ def support(bdd)
### COERCIONS from & to Cubes ######################################################
- def truth_value_as_012(truth)
- case truth
- when Cudd::BDD then is_complement?(truth) ? 0 : 1
- when Integer then (truth >= 0 and truth <= 1) ? truth : 2
- when TrueClass then 1
- when FalseClass then 0
- when NilClass then 2
- else
- raise ArgumentError, "Invalid truth value #{truth}"
- end
- end
-
# Coerces `arg` to a cube.
#
# Example (suppose three BDD variables: x, y and z):
@@ -235,26 +223,11 @@ def truth_value_as_012(truth)
# cube([x, !y]) # same
# cube(x => true, y => false) # same
#
- def cube(arg, as = :a012)
- a012 = nil
- if arg.is_a?(Cudd::BDD)
- a012 = bdd2cube(arg)
- else
- a012 = Array.new(size, 2)
- enum = arg.is_a?(Hash) ? arg.each_pair : arg.each_with_index
- enum.each do |k,v|
- k,v = v,k unless arg.is_a?(Hash)
- index = [k, v].find{|x| x.is_a?(Cudd::BDD) }.index rescue k
- a012[index] = truth_value_as_012(v)
- end
- end
- case as
- when :a012 then a012
- when :bdd then cube2bdd(a012)
- when :hash then cube2hash(a012)
- else
- raise ArgumentError, "Invalid 'as' option `#{as}`"
- end
+ def cube(arg, as = :cube)
+ cube = Cube.new(self, arg)
+ cube.send(:"to_#{as}")
+ rescue NoMethodError
+ raise ArgumentError, "Invalid 'as' option `#{as}`"
end
# Converts a cube array to a bdd
@@ -269,15 +242,6 @@ def cube2bdd(cube_array)
end
end
- # Converts a cube array to a Hash
- def cube2hash(cube_array)
- h = {}
- cube_array.each_with_index do |value, index|
- h[ ith_var(index) ] = (value == 1) if value < 2
- end
- h
- end
-
# Converts a bdd to a cube array
#
# @see Cudd_BddToCubeArray
@@ -314,31 +278,31 @@ def satisfied?(bdd, cube)
one == eval(bdd, cube)
end
- # Returns one satisfying assignment for `bdd`.
- def one_sat(bdd)
- each_sat(bdd).first
+ # Returns one satisfying cube for `bdd`.
+ def one_cube(bdd)
+ each_cube(bdd).first
end
- # Yields each assignment that satisfies `bdd` in turn.
- def each_sat(bdd)
- return self.enum_for(:each_sat, bdd) unless block_given?
+ # Yields each cube that satisfies `bdd` in turn.
+ 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_pointer.read_pointer.read_array_of_int(size)
+ 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
- # Returns an array with each assignement satisfying `bdd`.
- def all_sat(bdd)
- each_sat(bdd).to_a
+ # Returns an array with each cube satisfying `bdd`.
+ def all_cubes(bdd)
+ each_cube(bdd).to_a
end
end # module BDD
View
22 spec/cube/test_equality.rb
@@ -0,0 +1,22 @@
+require 'spec_helper'
+module Cudd
+ describe Cube, '==' do
+
+ subject{ cube1 == cube2 }
+
+ before{ x; y; z }
+
+ context 'on equal cubes' do
+ let(:cube1){ cube(x => true, y => false) }
+ let(:cube2){ cube(x => true, y => false) }
+ it{ should be_true }
+ end
+
+ context 'on non equal cubes' do
+ let(:cube1){ cube(x => true, y => false) }
+ let(:cube2){ cube(x => false) }
+ it{ should be_false }
+ end
+
+ end
+end
View
34 spec/cube/test_hash.rb
@@ -0,0 +1,34 @@
+require 'spec_helper'
+module Cudd
+ describe Cube, 'to_truths' do
+
+ subject{ c.to_truths }
+
+ before{ x; y; z }
+
+ context 'on x' do
+ let(:c){ cube(x => true) }
+
+ it 'returns the expected bdd' do
+ subject.should eq([true, nil, nil])
+ end
+ end
+
+ context 'on !x' do
+ let(:c){ cube(x => false) }
+
+ it 'returns the expected bdd' do
+ subject.should eq([false, nil, nil])
+ end
+ end
+
+ context 'on x & y' do
+ let(:c){ cube(x => true, y => true) }
+
+ it 'returns the expected bdd' do
+ subject.should eq([true, true, nil])
+ end
+ end
+
+ end
+end
View
49 spec/cube/test_new.rb
@@ -0,0 +1,49 @@
+require 'spec_helper'
+module Cudd
+ describe Cube, 'new' do
+
+ subject{ Cube.new(bdd_interface, arg) }
+
+ before{
+ x; y; z
+ subject.should be_a(Cube)
+ }
+
+ shared_examples_for "A cube for x=1,y=0,z=2" do
+ it 'has [1,0,2] has to_a012' do
+ subject.to_a012.should eq([1, 0, 2])
+ end
+ end
+
+ context 'when an array of 012' do
+ let(:arg){ [ 1, 0, 2 ] }
+ it_behaves_like "A cube for x=1,y=0,z=2"
+ end
+
+ context 'when an incomplete array of 012' do
+ let(:arg){ [ 1, 0 ] }
+ it_behaves_like "A cube for x=1,y=0,z=2"
+ end
+
+ context 'when truth values' do
+ let(:arg){ [ true, false, nil ] }
+ it_behaves_like "A cube for x=1,y=0,z=2"
+ end
+
+ context 'when an array of BDD variables' do
+ let(:arg){ [!y, x] }
+ it_behaves_like "A cube for x=1,y=0,z=2"
+ end
+
+ context 'when a Hash' do
+ let(:arg){ {x => 1, y => false} }
+ it_behaves_like "A cube for x=1,y=0,z=2"
+ end
+
+ context 'when a BDD' do
+ let(:arg){ x & !y }
+ it_behaves_like "A cube for x=1,y=0,z=2"
+ end
+
+ end
+end
View
34 spec/cube/test_to_a012.rb
@@ -0,0 +1,34 @@
+require 'spec_helper'
+module Cudd
+ describe Cube, 'to_a012' do
+
+ subject{ c.to_a012 }
+
+ before{ x; y; z }
+
+ context 'on x' do
+ let(:c){ cube(x => true) }
+
+ it 'returns the expected bdd' do
+ subject.should eq([1, 2, 2])
+ end
+ end
+
+ context 'on !x' do
+ let(:c){ cube(x => false) }
+
+ it 'returns the expected bdd' do
+ subject.should eq([0, 2, 2])
+ end
+ end
+
+ context 'on x & y' do
+ let(:c){ cube(x => true, y => true) }
+
+ it 'returns the expected bdd' do
+ subject.should eq([1, 1, 2])
+ end
+ end
+
+ end
+end
View
34 spec/cube/test_to_bdd.rb
@@ -0,0 +1,34 @@
+require 'spec_helper'
+module Cudd
+ describe Cube, 'to_bdd' do
+
+ subject{ c.to_bdd }
+
+ before{ x; y; z }
+
+ context 'on x' do
+ let(:c){ cube(x => true) }
+
+ it 'returns the expected bdd' do
+ subject.should eq(x)
+ end
+ end
+
+ context 'on !x' do
+ let(:c){ cube(x => false) }
+
+ it 'returns the expected bdd' do
+ subject.should eq(!x)
+ end
+ end
+
+ context 'on x & y' do
+ let(:c){ cube(x => true, y => true) }
+
+ it 'returns the expected bdd' do
+ subject.should eq(x & y)
+ end
+ end
+
+ end
+end
View
18 spec/cube/test_to_cube.rb
@@ -0,0 +1,18 @@
+require 'spec_helper'
+module Cudd
+ describe Cube, 'to_cube' do
+
+ subject{ c.to_bdd }
+
+ before{ x; y; z }
+
+ context 'on x & y' do
+ let(:c){ cube(x => true, y => true) }
+
+ it 'returns itself' do
+ subject.should eq(subject)
+ end
+ end
+
+ end
+end
View
34 spec/cube/test_to_hash.rb
@@ -0,0 +1,34 @@
+require 'spec_helper'
+module Cudd
+ describe Cube, 'to_hash' do
+
+ subject{ c.to_hash }
+
+ before{ x; y; z }
+
+ context 'on x' do
+ let(:c){ cube(x => true) }
+
+ it 'returns the expected bdd' do
+ subject.should eq(x => true)
+ end
+ end
+
+ context 'on !x' do
+ let(:c){ cube(x => false) }
+
+ it 'returns the expected bdd' do
+ subject.should eq(x => false)
+ end
+ end
+
+ context 'on x & y' do
+ let(:c){ cube(x => true, y => true) }
+
+ it 'returns the expected bdd' do
+ subject.should eq(x => true, y => true)
+ end
+ end
+
+ end
+end
View
34 spec/cube/test_to_truths.rb
@@ -0,0 +1,34 @@
+require 'spec_helper'
+module Cudd
+ describe Cube, 'to_truths' do
+
+ subject{ c.to_truths }
+
+ before{ x; y; z }
+
+ context 'on x' do
+ let(:c){ cube(x => true) }
+
+ it 'returns the expected bdd' do
+ subject.should eq([true, nil, nil])
+ end
+ end
+
+ context 'on !x' do
+ let(:c){ cube(x => false) }
+
+ it 'returns the expected bdd' do
+ subject.should eq([false, nil, nil])
+ end
+ end
+
+ context 'on x & y' do
+ let(:c){ cube(x => true, y => true) }
+
+ it 'returns the expected bdd' do
+ subject.should eq([true, true, nil])
+ end
+ end
+
+ end
+end
View
22 spec/interfaces/bdd/test_each_sat.rb → spec/interfaces/bdd/test_each_cube.rb
@@ -1,19 +1,19 @@
require 'spec_helper'
module Cudd
module Interfaces
- describe BDD, "each_sat" do
+ describe BDD, "each_cube" do
- subject{ formula.all_sat } # formula.each_sat.to_a
+ subject{ formula.all_cubes } # formula.each_cube.to_a
before do
x; y; z;
formula.ref
end
after do
- subject.each do |sat|
- sat.should be_a(Array)
- formula.satisfied?(sat).should be_true
+ subject.each do |cube|
+ cube.should be_a(Cube)
+ formula.satisfied?(cube).should be_true
end
formula.deref if formula
end
@@ -22,7 +22,7 @@ module Interfaces
let(:formula){ x & y }
it 'returns an enumerator' do
- formula.each_sat.should be_a(Enumerator)
+ formula.each_cube.should be_a(Enumerator)
end
end
@@ -38,39 +38,39 @@ module Interfaces
let(:formula){ one }
it 'yields one empty assignment' do
- subject.should eq([[2,2,2]])
+ subject.should eq([cube([2,2,2])])
end
end
context "on x" do
let(:formula){ x }
it 'yields one assignment with x=true' do
- subject.should eq([[1,2,2]])
+ subject.should eq([cube([1,2,2])])
end
end
context "on !x" do
let(:formula){ !x }
it 'yields one assignment with x=false' do
- subject.should eq([[0,2,2]])
+ subject.should eq([cube([0,2,2])])
end
end
context 'on (x & y)' do
let(:formula){ x & y }
it 'returns one assignment with both x and y to true' do
- subject.should eq([[1,1,2]])
+ subject.should eq([cube([1,1,2])])
end
end
context 'on (x | y)' do
let(:formula){ x | y }
it 'returns two assignments' do
- subject.should eq([[0,1,2], [1,2,2]])
+ subject.should eq([cube([0,1,2]), cube([1,2,2])])
end
end
View
5 spec/interfaces/bdd/test_one_sat.rb → spec/interfaces/bdd/test_one_cube.rb
@@ -1,12 +1,13 @@
require 'spec_helper'
module Cudd
module Interfaces
- describe BDD, "one_sat" do
+ describe BDD, "one_cube" do
- subject{ formula.one_sat }
+ subject{ formula.one_cube }
before do
formula.ref
+ subject.should be_a(Cube)
end
after do

0 comments on commit ca9f2c1

Please sign in to comment.