Module: LogicTools

Defined in:
lib/logic_tools.rb,
lib/logic_tools/traces.rb,
lib/logic_tools/version.rb,
lib/logic_tools/logictree.rb,
lib/logic_tools/logiccover.rb,
lib/logic_tools/logicinput.rb,
lib/logic_tools/logicparse.rb,
lib/logic_tools/logicconvert.rb,
lib/logic_tools/logicfunction.rb,
lib/logic_tools/logicgenerator.rb,
lib/logic_tools/logicsimplify_es.rb,
lib/logic_tools/logicsimplify_qm.rb,
lib/logic_tools/minimal_column_covers.rb

Overview

TODO: bdd representation.

Defined Under Namespace

Modules: Traces Classes: Cover, Cube, Function, Generator, HashCounter, Implicant, Indenter, Node, NodeAnd, NodeFalse, NodeNary, NodeNot, NodeOr, NodeTrue, NodeUnary, NodeValue, NodeVar, Parser, SameXImplicants, SmallestSumTerm, Transform, Variable, VoidCube

Constant Summary collapse

VERSION =
"0.3.9"

Instance Method Summary collapse

Instance Method Details

#cofactor_cube_indexed(cover, cube) ⇒ Object

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!


274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
# 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

#cofactor_indexed(cover, var, val) ⇒ Object

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!


244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
# 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

#cost(cover) ⇒ Object

Computes the cost of a cover.

The cost of the cover is sum of the number of variable of each cube.


489
490
491
492
493
494
# 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

#each_inputObject

Gets an iterator over the input expression

(obtained either through options or a through file).


19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
# 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

#essentials(on, dc) ⇒ Object

Get the essential cubes from the on cover which are not covered

by the +dc+ (don't care) cover.

Returns the new cover.


439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
# 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

#expand(on, off, deadline) ⇒ Object

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.


101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
# 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

#help_shortObject

Displays a short help message.



11
12
13
14
15
# 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

#irredundant(on, dc, deadline) ⇒ Object

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.


357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
# 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

#irredundant_partial(on) ⇒ Object

Remove quickly some cubes of the on cover that are redundant.

Returns the new cover.


423
424
425
426
427
428
429
430
431
432
# 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

#max_reduce(cube, on, dc) ⇒ Object

Compute the maximum reduction of a cube from an on cover

which does not intersect with another +dc+ cover.


498
499
500
501
502
503
504
505
506
507
508
509
510
511
# 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

#minimal_column_covers(matrix, smallest = false, deadline = Float::INFINITY) ⇒ Object

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).


195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
# 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

#minimal_set_covers(cover, dc) ⇒ Object

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.


307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
# 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

#order(cover) ⇒ Object

Sorts the cubes of a cover by weight.

Returns a new cover containing the sorted cubes.


63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
# 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

#reduce(on, dc) ⇒ Object

Reduces cover on esuring dc (don’t care) is not intersected.

Returns the resulting cover.


516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
# 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

#smallest_sum_term(product, deadline = Float::INFINITY) ⇒ Object

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.


181
182
183
184
185
186
# 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

#string2logic(str) ⇒ Object

The parser/gerator main fuction: converts the text in str to a

logic tree.


90
91
92
93
94
95
# 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

#to_sum_product_array(product) ⇒ Object

Converts a product of sum to a sum of product.

NOTE: * Both the input are outputs are represented as array of arrays.


13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
# 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

#vars2int(vars) ⇒ Object

Converts the array of variables var to a bit vector according to

their values.


17
18
19
20
21
22
23
# 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