module LogicTools
LogicTools
¶ ↑
This module includes all the classes and methods used by the logic_tools set of tools.
TODO: bdd representation.
Constants
- VERSION
Public Instance Methods
Generates the generalized cofactor of cover
from cube
while keeping the cubes indexes in the cover.
NOTE: for irreduntant only since the resulting cover is not in a valid state!
# File lib/logic_tools/logicsimplify_es.rb, line 274 def cofactor_cube_indexed(cover,cube) # Create the new cover. ncover = Cover.new(*@variables) # Set its cubes. cover.each_cube do |scube| scube = scube.to_s scube.size.times do |i| # if scube.getbyte(i) == cube[i] then if scube.getbyte(i) == cube.getbyte(i) then # scube[i] = "-" scube.setbyte(i,45) # elsif (scube[i] != "-" and cube[i] != "-") then elsif (scube.getbyte(i) != 45 and cube.getbyte(i) != 45) then # The cube is to remove from the cover. scube = nil break end end if scube then # The cube is to keep in the cofactor. ncover << Cube.new(scube,false) # No need to clone scube. else # Add an empty cube for keeping the index. ncover << VoidCube.new(ncover.width) end end return ncover end
Generates the cofactor of cover
obtained when var
is set to val
while keeping the cubes indexes in the cover.
NOTE: for irreduntant only since the resulting cover is not in a valid state!
# File lib/logic_tools/logicsimplify_es.rb, line 244 def cofactor_indexed(cover,var,val) # if val != "0" and val != "1" then if val != 48 and val != 49 then raise "Invalid value for generating a cofactor: #{val}" end # Get the index of the variable. i = cover.variable_index(var) # Create the new cover. ncover = Cover.new(*@variables) # Set its cubes. cover.each_cube do |cube| cube = cube.to_s # cube[i] = "-" if cube[i] == val cube.setbyte(i,45) if cube.getbyte(i) == val # if cube[i] == "-" then if cube.getbyte(i) == 45 then ncover << Cube.new(cube,false) # No need to clone cube. else # Add an empty cube for keeping the index. ncover << VoidCube.new(ncover.width) end end return ncover end
Computes the cost of a cover
.
The cost of the cover is sum of the number of variable of each cube.
# File lib/logic_tools/logicsimplify_es.rb, line 489 def cost(cover) return cover.each_cube.reduce(0) do |sum, cube| # sum + cube.each_bit.count { |b| b != "-" } sum + cube.each_byte.count { |b| b != 45 } end end
Gets an iterator over the input expression (obtained either through options or a through file).
# File lib/logic_tools/logicinput.rb, line 19 def each_input # No block? Return an enumerator return enum_for(:each_input) unless block_given? # A block? Interrate with it # Process the arguments if ($*.empty?) then # No arguments, shows the help and end. help_short exit(1) end if $*[0] == "-f" or $*[0] == "--file" then # Work from a file, iterate on each line exprs = File.read($*[1]) exprs.gsub!(/\r\n?/, "\n") exprs.each_line do |line| yield(line) end elsif $*[0] == "-h" or $*[0] == "--help" then help_short else # Work directly on the arguments as an expression yield($*.join) end end
Get the essential cubes from the on
cover which are not covered by the dc
(don't care) cover.
Returns the new cover.
# File lib/logic_tools/logicsimplify_es.rb, line 439 def essentials(on,dc) # Create the essential list. es = [] # For each cube of on, check if it is essential. on.each_cube do |cube| # Step 1: build the +cover+ (on-cube)+dc. # NOTE: could be done without allocating multiple covers, # but this is much readable this way, so kept as is as long # as there do not seem to be any much performance penalty. cover = (on-cube)+dc # Step 2: Gather the concensus beteen each cube of +cover+ # and their sharp with +cube+. cons = Cover.new(*on.each_variable) cover.each_cube do |ccube| # Depending on the distance. dist = cube.distance(ccube) # If the distance is >1 there is no consensus. # Otherwise: if (dist == 1) then # The distance is 1, the consensus is computed directly. cons << ccube.consensus(cube) elsif (dist == 0) # The distance is 0, sharp ccube from cube and # compute the concensus from each resulting prime cube. ccube.sharp(cube).each do |scube| scube = scube.consensus(cube) cons << scube if scube end end end # Step 3: check if +cube+ is covered by cover+cons. # This is done by checking is the cofactor with cube # is not a tautology. unless (cons+dc).cofactor_cube(cube).is_tautology? # +cube+ is not covered by cover+cons, it is an essential. es << cube end end # Create the resulting cover. result = Cover.new(*on.each_variable) es.each { |es| result << es } return result end
Expands cover on
as long it does not intersects with off
.
NOTE: this step requires to find the minimal column set cover of a matrix, this algorthim can be very slow and is therefore terminate before an optimal solution is found is a deadline
is exceeded.
Returns the resulting cover.
# File lib/logic_tools/logicsimplify_es.rb, line 101 def expand(on,off,deadline) # Step 1: sort the cubes by weight. on = order(on) # print "#3.1 #{Time.now}\n" # print "on=[#{on.to_s}]\n" # Create the resulting cover. cover = Cover.new(*on.each_variable) # Step 2: Expand the cubes in order of their weights. on.each_cube do |cube| # print "#3.2 #{Time.now} cube=#{cube}\n" # Builds the blocking matrix blocking = cube.blocking_matrix(off) # print "blocking=[#{blocking}]\n" # Select the smallest minimal column cover of the blocking # matrix: it will be the expansion col_cover = minimal_column_covers(blocking[1..-1],true,deadline) # print "col_cover=#{col_cover}\n" # This is the new cube bits = "-" * cube.width col_cover.each do |col| # The first row of the blocking matrix give the actual # column of the litteral col = blocking[0][col] # bits[col] = cube[col] bits.setbyte(col,cube.getbyte(col)) end # print "expand result=#{bits}\n" # Create and add the new expanded cube. cover << Cube.new(bits,false) # No need to clone bits. end return cover end
Displays a short help message.
# File lib/logic_tools/logicinput.rb, line 11 def help_short name = File.basename($0) puts "Usage: #{name} <\"logic expression\">" puts " or: #{name} -f <file name>" end
Removes the cubes of the on
cover that are redundant for the joint on
and dc
covers.
NOTE: this step requires to find the minimal column set cover of a matrix, this algorthim can be very slow and is therefore terminate before an optimal solution is found is a deadline
is exceeded.
Returns the new cover.
# File lib/logic_tools/logicsimplify_es.rb, line 357 def irredundant(on,dc,deadline) # Step 1: get the relatively essential. # print "on=#{on}\n" cubes, es_rel = on.each_cube.partition do |cube| ((on+dc) - cube).cofactor_cube(cube).is_tautology? end return on.clone if cubes.empty? # There were only relatively essentials. # print "cubes = #{cubes}\n" # print "es_rel = #{es_rel}\n" # Step 2: get the partially and totally redundants. es_rel_dc = Cover.new(*on.each_variable) es_rel.each { |cube| es_rel_dc << cube } dc.each { |cube| es_rel_dc << cube } red_tot, red_par = cubes.partition do |cube| es_rel_dc.cofactor_cube(cube).is_tautology? end # red_par is to be used as a cover. red_par_cover = Cover.new(*on.each_variable) red_par.each { |cube| red_par_cover << cube } # print "es_rel_dc = #{es_rel_dc}\n" # print "red_tot = #{red_tot}\n" # print "red_par = #{red_par}\n" # Step 3: get the minimal sets of partially redundant. red_par_sets = red_par.map do |cube| # print "for cube=#{cube}\n" minimal_set_covers( cofactor_cube_indexed(red_par_cover,cube), cofactor_cube_indexed(es_rel_dc,cube) ) end # red_par_sets.each { |set| set.map! {|i| red_par[i] } } # print "red_par_sets=#{red_par_sets}\n" # Step 4: find the smallest minimal set using the minimal column covers # algorithm. # For that purpose build the boolean matrix whose columns are for the # partially redundant cubes and the rows are for the sets, "1" # indication the cube is the in set. matrix = [] red_par_sets.each do |sets| sets.each do |set| row = "0" * red_par.size # set.each { |i| row[i] = "1" } set.each { |i| row.setbyte(i,49) } matrix << row end end # print "matrix=#{matrix}\n" smallest_set_cols = minimal_column_covers(matrix,true,deadline) # print "smallest_set_cols=#{smallest_set_cols}\n" # Creates a new cover with the relative essential cubes and the # smallest set of partially redundant cubes. cover = Cover.new(*on.each_variable) es_rel.each { |cube| cover << cube.clone } # smallest_set_cols.each do |set| # set.each { |col| cover << red_par[col].clone } # end smallest_set_cols.each { |col| cover << red_par[col].clone } # print "cover=#{cover}\n" return cover end
Remove quickly some cubes of the on
cover that are redundant.
Returns the new cover.
# File lib/logic_tools/logicsimplify_es.rb, line 423 def irredundant_partial(on) result = Cover.new(*on.each_variable) on.each.with_index do |cube,i| # Is cube included somewhere? unless on.each.with_index.find {|cube1,j| j != i and cube1.include?(cube) } # No, keep the cube. result << cube end end end
Compute the maximum reduction of a cube from an on
cover which does not intersect with another dc
cover.
# File lib/logic_tools/logicsimplify_es.rb, line 498 def max_reduce(cube,on,dc) # print "max_reduce with cube=#{cube} on=#{on} dc=#{dc}\n" # Step 1: create the cover to get the reduction from. cover = ((on + dc) - cube).cofactor_cube(cube) # print "cover=#{cover}, taut=#{cover.is_tautology?}\n" # Step 2: complement it compl = cover.complement # print "compl=#{compl}\n" # Step 3: get the smallest cube containing the complemented cover sccc = compl.smallest_containing_cube # print "sccc=#{sccc}\n" # The result is the intersection of this cube with +cube+. return cube.intersect(sccc) end
Computes the minimal column covers of a boolean matrix
.
If smallest
is set to one, the method returns the smallest minimal column cover instead.
The matrix
is assumed to be an array of string, each string representing a boolean row (“0” for false and “1” for true).
# File lib/logic_tools/minimal_column_covers.rb, line 195 def minimal_column_covers(matrix, smallest = false, deadline = Float::INFINITY) # print "matrix=#{matrix}\n" # Step 1: reduce the matrix for faster processing. # First put appart the essential columns. essentials = [] matrix.each do |row| col = nil row.each_byte.with_index do |c,i| # if c == "1" then if c == 49 then if col then # The row has several "1", no essential column there. col = nil break end col = i end end # An essential column is found. essentials << col if col end essentials.uniq! # print "essentials = #{essentials}\n" # The remove the rows covered by essential columns. keep = [ true ] * matrix.size essentials.each do |col| matrix.each.with_index do |row,i| # keep[i] = false if row[col] == "1" keep[i] = false if row.getbyte(col) == 49 end end # print "keep = #{keep}\n" reduced = matrix.select.with_index {|row,i| keep[i] } # print "matrix = #{matrix}\n" # print "reduced = #{reduced}\n" if reduced.empty? then # Essentials columns are enough for the cover, end here. if smallest then return essentials else return [ essentials ] end end to_optimize = false removed_columns = [] begin to_optimize = false # Then remove the dominating rows reduced.uniq! reduced = reduced.select.with_index do |row0,i| ! reduced.find.with_index do |row1,j| if i == j then false else # The row is dominating if in includes another row. res = row0.each_byte.with_index.find do |c,j| # row1[j] == "1" and c == "0" row1.getbyte(j) == 49 and c == 48 end # Not dominating if res !res end end end # # Finally remove the dominated columns if only one column cover # # is required. # if smallest and reduced.size >= 1 then # size = reduced[0].size # size.times.reverse_each do |col0| # next if removed_columns.include?(col0) # size.times do |col1| # next if col0 == col1 # # The column is dominated if it is included into another. # res = reduced.find do |row| # row[col0] == "1" and row[col1] == "0" # end # # Not dominated if res # unless res # to_optimize = true # # print "removing column=#{col0}\n" # # Dominated, remove it # reduced.each { |row| row[col0] = "0" } # removed_columns << col0 # end # end # end # end end while(to_optimize) # print "now reduced=#{reduced}\n" # Step 2: Generate the Petrick's product. product = [] reduced.each do |row| term = [] # Get the columns covering the row. row.each_byte.with_index do |bit,i| # term << i if bit == "1" term << i if bit == 49 end product << term unless term.empty? end if smallest then if product.empty? then return essentials end cover = smallest_sum_term(product,deadline) if essentials then # print "essentials =#{essentials} cover=#{cover}\n" essentials.each {|cube| cover.unshift(cube) } return cover else return cover end end # print "product=#{product}\n" if product.empty? then sum = product else product.each {|fact| fact.sort!.uniq! } product.sort!.uniq! # print "product=#{product}\n" sum = to_sum_product_array(product) # print "sum=#{sum}\n" sum.each {|term| term.uniq! } sum.uniq! sum.sort_by! {|term| term.size } # print "sum=#{sum}\n" end # # Add the essentials to the result and return it. # if smallest then # # print "smallest_cover=#{smallest_cover}, essentials=#{essentials}\n" # return essentials if sum.empty? # # Look for the smallest cover # sum.sort_by! { |cover| cover.size } # if essentials then # return sum[0] + essentials # else # return sum[0] # end # else sum.map! { |cover| essentials + cover } return sum # end end
Computes the minimal set cover of a cover
along with a dc
(don't care) cover.
Return the set as a list of cube indexes in the cover.
# File lib/logic_tools/logicsimplify_es.rb, line 307 def minimal_set_covers(cover,dc) # print "minimal_set_cover with cover=#{cover} and dc=#{dc}\n" # Look for a binate variable to split on. binate = (cover+dc).find_binate # binate = cover.find_binate # # Gets its index # i = cover.variable_index(binate) unless binate then # The cover is actually unate, process it the fast way. # Look for "-" only cubes. # First in +dc+: if there is an "-" only cube, there cannot # be any minimal set cover. dc.each_cube do |cube| # return [] unless cube.each.find { |b| b != "-" } return [] unless cube.each_byte.find { |b| b != 45 } end # Then in +cover+: each "-" only cube correspond to a cube in the # minimal set cover. result = [] cover.each.with_index do |cube,i| # print "cube=#{cube} i=#{i}\n" # result << i unless cube.each.find { |b| b != "-" } result << i unless cube.each_byte.find { |b| b != 45 } end # print "result=#{result}\n" return [ result ] else # Compute the cofactors over the binate variables. # cf0 = cofactor_indexed(cover,binate,"0") cf0 = cofactor_indexed(cover,binate,48) # cf1 = cofactor_indexed(cover,binate,"1") cf1 = cofactor_indexed(cover,binate,49) # df0 = cofactor_indexed(dc,binate,"0") df0 = cofactor_indexed(dc,binate,48) # df1 = cofactor_indexed(dc,binate,"1") df1 = cofactor_indexed(dc,binate,49) # Process each cofactor and merge their results return [ minimal_set_covers(cf0,df0), minimal_set_covers(cf1,df1) ].flatten(1) end end
Sorts the cubes of a cover
by weight.
Returns a new cover containing the sorted cubes.
# File lib/logic_tools/logicsimplify_es.rb, line 63 def order(cover) # Step 1: Compute the weight of each cube weights = [ 0 ] * cover.size # For that purpose first compute the weight of each column # (number of ones) col_weights = [ 0 ] * cover.width cover.width.times do |i| # cover.each_cube { |cube| col_weights[i] += 1 if cube[i] == "1" } cover.each_cube do |cube| col_weights[i] += 1 if cube.getbyte(i) == 49 end end # Then the weight of a cube is the scalar product of its # bits with the column weights. cover.each_cube.with_index do |cube,j| cube.each_byte.with_index do |bit,i| # weights[j] += col_weights[i] if bit == "1" weights[j] += col_weights[i] if bit == 49 end end # Step 2: stort the cubes by weight new_cubes = cover.each_cube.sort_by.with_index { |cube,i| weights[i] } # Creates a new cover with the sorted cubes and return it. sorted = Cover.new(*cover.each_variable) new_cubes.each { |cube| sorted << cube } return sorted end
Reduces cover on
esuring dc
(don't care) is not intersected.
Returns the resulting cover.
# File lib/logic_tools/logicsimplify_es.rb, line 516 def reduce(on,dc) # Step 1: sorts on's cubes to achieve a better reduce. on = order(on) # print "ordered on=#{on.to_s}\n" # Step 2: reduce each cube and add it to the resulting cover. cover = Cover.new(*on.each_variable) on.each_cube.to_a.reverse_each do |cube| reduced = max_reduce(cube,on,dc) # print "cube=#{cube} reduced to #{reduced}\n" cover << reduced if reduced # Add the cube if not empty on = (on - cube) on << reduced if reduced # Add the cube if not empty end return cover end
Extracts from a product
of sums the smallest term of the corresponding sum of products.
NOTE: * Both the input are outputs are represented as array of arrays.
* Uses a branch and bound algorithm.
# File lib/logic_tools/minimal_column_covers.rb, line 181 def smallest_sum_term(product, deadline = Float::INFINITY) return [product[0][0]] if product.size == 1 # Create the solver and applies it return SmallestSumTerm.new(product,deadline).solve end
The parser/gerator main fuction: converts the text in str
to a logic tree.
# File lib/logic_tools/logicparse.rb, line 90 def string2logic(str) # Remove the spaces str = str.gsub(/\s+/, "") # Parse the string return Transform.new.apply(Parser.new.parse(str)) end
Converts a product
of sum to a sum of product.
NOTE: * Both the input are outputs are represented as array of arrays.
# File lib/logic_tools/minimal_column_covers.rb, line 13 def to_sum_product_array(product) return product[0].map {|term| [term] } if product.size == 1 # Generate the initial terms. sum = product[0].product(product[1]) sum.each {|term| term.sort!.uniq! } sum.uniq! # Fill then with each factor to the resulting sum of product. # print "sum = #{sum}, product=#{product}\n" (2..(product.size-1)).each do |i| sum.map! do |term| # # print "mapping #{product[i]}\n" set = [] product[i].each do |fact| if term.include?(fact) then set << term unless set.include?(term) else nterm = term.clone nterm << fact nterm.sort! set << nterm end end set end sum.flatten!(1) # print "then sum=#{sum}\n" sum.uniq! # print "now sum=#{sum}\n" # pid, size = `ps ax -o pid,rss | grep -E "^[[:space:]]*#{$$}"`.strip.split.map(&:to_i) # print "memory usage=#{size}\n" end # print "\n" return sum end
Converts the array of variables var
to a bit vector according to their values.
# File lib/logic_tools/logicsimplify_qm.rb, line 17 def vars2int(vars) res = "" vars.each_with_index do |var,i| res[i] = var.value ? "1" : "0" end res end