Commit 8f84b252 authored by Luc Libralesso's avatar Luc Libralesso
Browse files

new xor generation procedure (few times faster than before)

parent c99b494f
......@@ -10,14 +10,13 @@ require "minitest/autorun"
require "pry"
class TestWriterGraphviz < Minitest::Unit::TestCase
def test_a()
dag = Midori128_Dag.new(nb_rounds=3)
model = get_abstract_constraint_model(dag)
file = File.open("test.mzn", "w")
file.puts(Minizinc.new.generate_code(model))
file.close
assert_equal(true,true)
end
end
\ No newline at end of file
def test_a()
dag = Midori128_Dag.new(nb_rounds = 4)
model = get_abstract_constraint_model(dag)
file = File.open("test.mzn", "w")
file.puts(Minizinc.new.generate_code(model))
file.close
assert_equal(true, true)
end
end
......@@ -87,53 +87,48 @@ end
# @param to_shave [Set<CryptoAtom|CryptoOperator>]
# @return [new_atoms, new_operators]
def generate_xors(atoms, operators, custom_xors, max_size=4)
new_xors = Set.new(operators.filter{|op| op.class <= XorOperator}.map{|op| Set.new(op.inputs+op.outputs)}+custom_xors)
# new_xors.each do |x|
# p x.map{|e| e.name.name}
# end
initial_xors = Set.new(operators.filter{|op| op.class <= XorOperator}.map{|op| Set.new(op.inputs+op.outputs)}+custom_xors)
new_xors = initial_xors.dup
variables = Set.new()
variable_adj = {}
new_xors.each do |op|
op.each do |v|
variables.add(v)
variable_adj[v] = variable_adj.fetch(v, Set.new()).add(op)
end
end
puts "GENERATE_XORS(limit=#{max_size}): found #{new_xors.length} initial xors"
puts "\t#{variables.length} variables"
initial_xors = Set.new()
while new_xors.length > initial_xors.length
initial_xors = new_xors
variable_adj = {}
nb_links = 0
new_xors.each do |op|
op.each do |v|
variable_adj[v] = variable_adj.fetch(v, Set.new()).add(op)
nb_links += 1
end
end
puts "\tnb links: #{nb_links}"
new_xors = initial_xors.dup
xor_to_check = new_xors.dup
puts "GENERATE_XORS(limit=#{max_size}): with #{new_xors.length} initial xors"
to_continue = true
while to_continue
to_continue = false
new_xor_to_check = Set.new()
variables.each do |v|
variable_adj[v].each do |a|
variable_adj[v].each do |b|
if a != b
c = (a+b)-(a&b)
# check that c does not contain more than 2 diff variables
nb_diffs = c.filter{|v| v.name.name.start_with?("diff_")}.length
if nb_diffs <= 1
if xor_to_check.include?(a)
variable_adj[v].each do |b|
if a != b
c = (a+b)-(a&b)
if c.length >= 1 && c.length <= max_size
# p c.map{|v|v.name.name}
new_xors.add(c)
nb_diffs = c.filter{|v| v.name.name.start_with?("diff_")}.length
if nb_diffs <= 1 && !new_xors.include?(c)
new_xors.add(c)
new_xor_to_check.add(c)
to_continue = true
c.each do |v|
variable_adj[v] = variable_adj.fetch(v, Set.new()).add(c)
end
end
end
end
end
end
end
end
puts "\tround finished: #{new_xors.length-initial_xors.length} added"
xor_to_check = new_xor_to_check
puts "\tround finished with: #{new_xors.length} clauses"
end
result = new_xors - (Set.new(operators.filter{|op| op.class <= XorOperator}.map{|op| Set.new(op.inputs+op.outputs)})+custom_xors)
return result
return new_xors
end
......@@ -276,6 +271,7 @@ def create_abstract_model(atoms, operators)
model.add_variables(var)
end
# add constraints
mc_xors = []
operators.each do |op|
case op.class.name
when "XorOperator"
......@@ -305,6 +301,15 @@ def create_abstract_model(atoms, operators)
Equals.new(Sum.new(*op.inputs.map {|atom| variable_dict[atom]}), 0),
Equals.new(Sum.new(*op.outputs.map {|atom| variable_dict[atom]}), 0)
))
# midori specific
model.add_constraints(Diff1.new(op.outputs[0], op.inputs[1], op.inputs[2], op.inputs[3]))
model.add_constraints(Diff1.new(op.outputs[1], op.inputs[0], op.inputs[2], op.inputs[3]))
model.add_constraints(Diff1.new(op.outputs[2], op.inputs[0], op.inputs[1], op.inputs[3]))
model.add_constraints(Diff1.new(op.outputs[3], op.inputs[0], op.inputs[1], op.inputs[2]))
mc_xors.push(Set.new([op.outputs[0], op.inputs[1], op.inputs[2], op.inputs[3]]))
mc_xors.push(Set.new([op.outputs[1], op.inputs[0], op.inputs[2], op.inputs[3]]))
mc_xors.push(Set.new([op.outputs[2], op.inputs[0], op.inputs[1], op.inputs[3]]))
mc_xors.push(Set.new([op.outputs[3], op.inputs[0], op.inputs[1], op.inputs[2]]))
else
# p c.class
raise "gen_abstract_constraint_model: unknown operator: #{op.class.name}"
......@@ -321,11 +326,12 @@ def create_abstract_model(atoms, operators)
Sum.new(*s_operators.map{|op| variable_dict[op.outputs[0]]})
)
)
model.add_instructions(Instruction.new("solve minimize obj"))
# model.add_instructions(Instruction.new("solve minimize obj"))
model.add_instructions(Instruction.new("constraint obj=4; solve satisfy"))
diff_xors = add_diff_variables_mixcolumn_lines(model, atoms, operators, variable_dict)
new_xors = generate_xors(atoms, operators, diff_xors)
new_xors = generate_xors(atoms, operators, diff_xors+mc_xors)
new_xors.each do |xor|
model.add_constraints(Diff1.new(*(xor.map{|v| variable_dict.fetch(v,v)})))
end
......@@ -420,7 +426,7 @@ def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable
diffs_to_var[[id2,id3,row,t]]
]
model.add_constraints(Diff1.new(*vars))
res_xors.push(Set.new(vars))
# res_xors.push(Set.new(vars))
end
end
end
......@@ -441,9 +447,9 @@ def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable
Equals.new(Sum.new(*4.times.map{|row| diffs_to_var[[id1,id2,row,"I"]]}), 0),
Equals.new(Sum.new(*4.times.map{|row| diffs_to_var[[id1,id2,row,"O"]]}), 0)
))
model.add_constraints()
end
end
end
# XOR(DIFFZ[i1, j, k, i2], X[i1 + 1, j, k], X[i2 + 1, j, k])
return res_xors
end
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment