Skip to content

GitLab

Commit 039dd00d authored by Luc Libralesso's avatar Luc Libralesso
Browse files

update abstract writer

parent 8f84b252
Hide whitespace changes
Inline Side-by-side
writers/abstract_constraints_atomic.rb
View file @ 039dd00d
......@@ -13,27 +13,16 @@ class UnionFind::UnionFind
end
##############
def get_abstract_constraint_model(dag)
atoms = dag.atoms()
operators = dag.operators()
# atoms2,operators2 = *[atoms,operators]
# shave dag to remove useless inputs and outputs
# atoms2,operators2 = *shave_dag(atoms, operators)
atoms2,operators2 =
*shave_equalities(
def shave_dag(atoms, operators)
return *shave_equalities(
*shave_simple_input_xor(
*shave_constants_dag(
*shave_end_dag(
atoms, operators
*shave_constants_dag(
*shave_end_dag(
atoms,operators
)
)
)
)
)
)
writefile_graphviz(atoms2, operators2, "test.dot")
puts "DOT FILE WRITEN"
# create model
model = create_abstract_model(atoms2, operators2)
return model
)
end
##
......@@ -261,7 +250,7 @@ def compute_precedences(atoms, operators)
end
def create_abstract_model(atoms, operators)
def create_abstract_model(atoms, operators, solve_instructions)
model = Model.new()
variable_dict = {} # Atom -> Variable
# add atoms as booleans
......@@ -271,7 +260,7 @@ def create_abstract_model(atoms, operators)
model.add_variables(var)
end
# add constraints
mc_xors = []
xor_clauses = []
operators.each do |op|
case op.class.name
when "XorOperator"
......@@ -279,6 +268,10 @@ def create_abstract_model(atoms, operators)
*op.inputs.map {|atom| variable_dict[atom]},
*op.outputs.map {|atom| variable_dict[atom]}
))
xor_clauses.push(Set.new(
op.inputs.map {|atom| variable_dict[atom]}+
op.outputs.map {|atom| variable_dict[atom]}
))
when "SOperator"
model.add_constraints(Equality.new(
*op.inputs.map {|atom| variable_dict[atom]},
......@@ -301,24 +294,14 @@ 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}"
end
end
# generate xors
# add objective function
s_operators = operators.filter {|op| op.class <= SOperator}
obj = Variable.new("obj", 1..20)
obj = Variable.new("obj", 1..64)
model.add_variables(obj)
model.add_constraints(
Equality.new(
......@@ -326,17 +309,9 @@ 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("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+mc_xors)
new_xors.each do |xor|
model.add_constraints(Diff1.new(*(xor.map{|v| variable_dict.fetch(v,v)})))
end
model.add_instructions(Instruction.new(solve_instructions))
return model
return [model,variable_dict,xor_clauses]
end
......@@ -359,7 +334,7 @@ def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable
diffs = []
mc_operators.each do |o1|
mc_operators.each do |o2|
if op_to_ids[o1] != op_to_ids[o2]
if op_to_ids[o1] < op_to_ids[o2]
4.times do |row|
diffs.push([op_to_ids[o1],op_to_ids[o2],row,"I"])
diffs.push([op_to_ids[o1],op_to_ids[o2],row,"O"])
......@@ -404,7 +379,7 @@ def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable
# add symmetry
diffs.each do |d1|
diffs.each do |d2|
if d1[0] == d2[1] && d1[1] == d2[0] && d1[3] == d2[3] && d1[2] == d2[2] && d1[0] != d2[0]
if d1[0] < d1[1] && d1[0] == d2[1] && d1[1] == d2[0] && d1[3] == d2[3] && d1[2] == d2[2] && d1[0] != d2[0]
model.add_constraints(Equality.new(
diffs_to_var[d1],
diffs_to_var[d2]
......@@ -413,26 +388,28 @@ def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable
end
end
# add transitivity
mc_operators.each do |o1|
mc_operators.each do |o2|
mc_operators.each do |o3|
if o1 != o2 && o2 != o3 && o1 != o3
id1, id2, id3 = op_to_ids[o1], op_to_ids[o2], op_to_ids[o3]
4.times do |row|
["I","O"].each do |t|
vars = [
diffs_to_var[[id1,id2,row,t]],
diffs_to_var[[id1,id3,row,t]],
diffs_to_var[[id2,id3,row,t]]
]
model.add_constraints(Diff1.new(*vars))
# res_xors.push(Set.new(vars))
end
end
end
end
end
end
# mc_operators.each do |o1|
# mc_operators.each do |o2|
# mc_operators.each do |o3|
# if o1 != o2 && o2 != o3 && o1 != o3
# id1, id2, id3 = op_to_ids[o1], op_to_ids[o2], op_to_ids[o3]
# if id1 < id2 && id2 < id3
# 4.times do |row|
# ["I","O"].each do |t|
# vars = [
# diffs_to_var[[id1,id2,row,t]],
# diffs_to_var[[id1,id3,row,t]],
# diffs_to_var[[id2,id3,row,t]]
# ]
# model.add_constraints(Diff1.new(*vars))
# # res_xors.push(Set.new(vars))
# end
# end
# end
# end
# end
# end
# end
# add mix columns property (sum diffs input + diffs output) for each couple of operators
mc_operators.each do |o1|
mc_operators.each do |o2|
......
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