module LogicTools

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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

# 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