Merge branch 'optimize_ctree' into 'master'

Optimize ctree

See merge request !2

Gemfile

 source 'https://rubygems.org'
 gem 'slop'
-gem 'pry'
\ No newline at end of file
+gem 'pry'
+gem 'union_find'

constraints/all.rb

@@ -5,5 +5,7 @@ require_relative "tables"
 require_relative "constraints"
 require_relative "comment"
 
+require_relative "expression"
+
 require_relative "model"
 # require_relative "variable_store"

constraints/constraints.rb

@@ -18,6 +18,8 @@ class Binary < Constraint
     super()
     @v1 = v1
     @v2 = v2
+    @v1.above << self
+    @v2.above << self
   end
 
   def accept(visitor)
@@ -25,20 +27,41 @@ class Binary < Constraint
     @v1.accept(visitor)
     @v2.accept(visitor)
   end
+
+  def substitute(from, to)
+    if @v1 == from
+      @v1 = to
+      @v1.above << self
+    end
+
+    if @v2 == from
+      @v2 = to
+      @v2.above << self
+    end
+  end
 end
 
 # Equality constraint - Functionnal form : a = b
 class Equality < Binary
+  def to_s
+    "#{v1} == #{v2}"
+  end
 end
 
 ## Binary constraint - Functionnal form : a = b
 class Different < Binary
+  def to_s
+    "#{v1} != #{v2}"
+  end
 end
 
 # Equivalence:   a <=> b
 #
 # @param parameters [ list of parameters ] parameters to XORed
 class Equivalence < Binary
+  def to_s
+    "#{v1} <=> #{v2}"
+  end
 end
 
 ## Diff1(variables) => Sum(variables) != 1
@@ -65,4 +88,8 @@ class IncludedIn < Constraint
     set = SetValue.new(set) unless set.kind_of?(SetValue)
     @set = set
   end
+
+  def to_s
+    "#{v1} In {#{v2}}"
+  end
 end

constraints/expression.rb

 class Expression
+  attr_accessor :above
+
+  def initialize
+    @above = []
+  end
 end
 
 # Functionnal form : f(a,b)
@@ -12,13 +17,43 @@ class Function < Expression
   def initialize(name, *parameters)
     super()
     @name = name
-    @parameters = parameters
+    @parameters = parameters.map do |p|
+      basic = [Integer, Float]
+      if basic.include?(p.class)
+        LitteralValue.new(p)
+      else
+        p
+      end
+    end
+    @parameters.each { |e|
+      e.above.push(self)
+    }
   end
 
   def accept(visitor)
     visitor.visit(self)
     accept_elements(visitor, @parameters)
   end
+
+  def substitute(from, to)
+    @parameters.map! do |param|
+      if param == from
+        to.above << self
+        to
+      else
+        param
+      end
+    end
+  end
+
+  def be_replaced_by(expr)
+    above.each { |e| e.substitute(self, expr) }
+    above = []
+  end
+
+  def to_s
+    "#{@name}( #{@parameters.join(" , ")} )"
+  end
 end
 
 # Abstract class Operation. An operation has an infix operator
@@ -28,13 +63,11 @@ end
 # Priority form : (a,b)
 #
 # @param parameters [ list of parameters ] parameters of the priority
-class Priority < Expression
+class Priority < Function
   include Visited
-  attr_reader :parameter
 
   def initialize(parameter)
-    super()
-    @parameter = parameter
+    super("()", [parameter])
   end
 end
 
@@ -49,6 +82,10 @@ class Operator < Expression
     super()
     @operator = operator
   end
+
+  def to_s
+    @operator.to_s
+  end
 end
 
 # Operation XOR
@@ -114,7 +151,6 @@ class Sub < Operation
   end
 end
 
-
 ## Equals
 #
 # @param parameters [ list of parameters ] parameters to be compared
@@ -122,4 +158,26 @@ class Equals < Operation
   def initialize(*parameters)
     super(Operator.new("="), *parameters)
   end
-end
\ No newline at end of file
+end
+
+## A litteral value (int, number...)
+class LitteralValue < Expression
+  include Visited
+  attr_reader :value
+
+  ## Ctor
+  #
+  # @param value [ Any numeric value ] Any value
+  def initialize(value)
+    @value = value
+    super()
+  end
+
+  def accept(visitor)
+    visitor.visit(self)
+  end
+
+  def to_s
+    "#{value}"
+  end
+end

constraints/tables.rb

@@ -86,6 +86,7 @@ class VariableInTable < Variable
   def initialize(table, indexes)
     @table = table
     @indexes = indexes
+    super(name, table.type)
   end
 
   ## VariableInTable has no declaration
@@ -103,7 +104,7 @@ end
 
 ## Table of variable with dynamic Instanciation choice
 class DTable < AbstractTable
-  attr_reader :declarationMode, :constant
+  attr_reader :declarationMode, :constant, :variables
 
   ## Ctor
   def initialize(*params, constant: false)

constraints/types.rb

@@ -81,16 +81,3 @@ class SetValue
     @values = values
   end
 end
-
-## A litteral value (int, number...)
-class LitteralValue
-  include Visited
-  attr_reader :value
-
-  ## Ctor
-  #
-  # @param value [ Any numeric value ] Any value
-  def initialize(value)
-    @value = value
-  end
-end

constraints/variables.rb

@@ -41,6 +41,15 @@ class Variable < Expression
     variable == self ? 1 : 0
   end
 
+  ## Does nothing!
+  def substitute(from, to)
+  end
+
+  def be_replaced_by(expr)
+    above.each { |e| e.substitute(self, expr) }
+    above = []
+  end
+
   ## Create a Multimatrix full of variables
   #
   # @param name [ String ] : Base name for the variables
@@ -87,7 +96,7 @@ class Variable < Expression
   public
 
   def self.new_array(name, type, dimensions, value = nil)
-    raise "Should not be called"
+    raise "Should not be called. Use"
     matrix = MultiMatrix.build(type, dimensions)
     matrix.each_with_index do |v, *dim|
       name_dim = name + "_" + dim.join("_")

main.rb

@@ -14,48 +14,53 @@ require_relative "writers/step1diff"
 require_relative "backends/minizinc"
 
 def main
-	# create DAG
-	nb_rounds = 4
-	dag = Midori128_Dag.new(nb_rounds = nb_rounds)
-
-	# visualize DAG
-	# print_graphviz(dag)
-	writefile_graphviz(dag, "tmp/midori128.dot")
-
-	if $options[:countdown]
-		require_relative "constraints/model"
-
-		# model = Step1OptConstraintWriter.new.generate_model(dag)
-		model = Step1Diff.new.generate_extended_model(dag, nb_rounds)
-		puts Minizinc.new.generate_code(model)
-	else
-
-		# write minizinc
-		print_minizinc_dk_step1opt(dag, mc_improvements = false)
-
-		# simulate behavior
-		# output = dag.simulate_behavior(
-		#     [
-		#         [0x51,0xe7,0xec,0xbc],
-		#         [0x08,0x3a,0x87,0x29],
-		#         [0x4c,0x5c,0xd7,0x75],
-		#         [0xe6,0xa2,0xba,0x43]
-		#     ],
-		#     [
-		#         [0x68,0x3c,0x5b,0x3e],
-		#         [0x7d,0x85,0x10,0x2a],
-		#         [0xed,0xb3,0x09,0x8c],
-		#         [0x3b,0xf3,0x86,0xbf]
-		#     ]
-		# )
-		# nodes = dag.find_all_nodes()
-		# nodes.each do |n|
-		#     if n.class.name != "ConstantNode"
-		#         puts "=== #{n.name} ==="
-		#         matrix_pretty_print(n.compute())
-		#     end
-		# end
-	end
+  # create DAG
+  dag = Midori128_Dag.new(nb_rounds = 10)
+
+  # visualize DAG
+  # print_graphviz(dag)
+  writefile_graphviz(dag, "tmp/midori128.dot")
+
+  if $options[:countdown]
+    require_relative "constraints/model"
+
+    model = Step1OptConstraintWriter.new.generate_model(dag)
+
+    if $options[:optimize]
+      require_relative "model_manipulations/detect_duplicate_variables"
+      simplify = Simplificator.new(model)
+      simplify.remove_duplicate_variables
+    end
+
+    puts Minizinc.new.generate_code(model)
+  else
+
+    # write minizinc
+    print_minizinc_dk_step1opt(dag, mc_improvements = false)
+
+    # simulate behavior
+    # output = dag.simulate_behavior(
+    #     [
+    #         [0x51,0xe7,0xec,0xbc],
+    #         [0x08,0x3a,0x87,0x29],
+    #         [0x4c,0x5c,0xd7,0x75],
+    #         [0xe6,0xa2,0xba,0x43]
+    #     ],
+    #     [
+    #         [0x68,0x3c,0x5b,0x3e],
+    #         [0x7d,0x85,0x10,0x2a],
+    #         [0xed,0xb3,0x09,0x8c],
+    #         [0x3b,0xf3,0x86,0xbf]
+    #     ]
+    # )
+    # nodes = dag.find_all_nodes()
+    # nodes.each do |n|
+    #     if n.class.name != "ConstantNode"
+    #         puts "=== #{n.name} ==="
+    #         matrix_pretty_print(n.compute())
+    #     end
+    # end
+  end
 end
 
 main

model_manipulations/detect_duplicate_variables.rb

+require "union_find"
+require "set"
+require_relative "../constraints/all"
+
+unless UnionFind::UnionFind.public_method_defined?(:get_root)
+  class UnionFind::UnionFind
+    def get_root(component)
+      find_root(component)
+    end
+  end
+end
+
+class Simplificator
+  def initialize(model)
+    @model = model
+    @union_find = nil
+    @aliasing_constraints = []
+    @byRoot = Hash.new { |hash, key| hash[key] = [] }
+
+    find_duplicate_variables()
+  end
+
+  def remove_duplicate_variables()
+    @byRoot.each_pair do |root, targets|
+      targets.each do |target|
+        target.be_replaced_by(root) if target != root
+      end
+    end
+    @model.constraints.reject! { |e| @aliasing_constraints.include?(e) }
+  end
+
+  protected def find_duplicate_variables()
+    vars = @model.variables.to_set
+
+    @union_find = UnionFind::UnionFind.new(vars)
+
+    find_equalities
+
+    vars.each do |v|
+      @byRoot[@union_find.get_root(v)].push(v)
+    end
+    vars
+  end
+
+  def find_equalities
+    @model.constraints.select { |c| c.instance_of?(Equality) }.each do |c|
+      if c.v1.kind_of?(Variable) && c.v2.kind_of?(Variable) &&
+         !c.v1.kind_of?(VariableInTable) && !c.v2.kind_of?(VariableInTable)
+        #$stderr.puts("#{c.v1.class} == #{c.v2.class}")
+        @union_find.union(c.v1, c.v2)
+        @aliasing_constraints << c
+      end
+    end
+  end
+end

model_manipulations/minitest/test_duplicate_variables.rb

+require "minitest/autorun"
+require "pry"
+
+require_relative "../detect_duplicate_variables"
+
+class TestDuplicates < MiniTest::Unit::TestCase
+  def setup
+    @model = Model.new
+
+    vars = (0..3).to_a.map { |i| Variable.new("v_#{i}", "int") }
+    @model.add_variables(*vars)
+    @model.add_constraints(
+      Equality.new(vars[0], vars[1]),
+      Equality.new(vars[0], vars[2]),
+      Equality.new(Sum.new(*vars), Sum.new(*vars))
+    )
+    @tableModel = Model.new
+    @t = DTable.new("plouf", "int", [2, 2])
+    @tableModel.add_variables(@t)
+    vs = @t.variables
+    @tableModel.add_variables(*vs)
+
+    @tableModel.add_constraints(
+      Equality.new(@t[0, 0], @t[0, 1]),
+      Equality.new(@t[0, 0], @t[1, 1]),
+      Equality.new(@t[1, 1], @t[1, 1]),
+      Equality.new(Sum.new(*vs), Sum.new(*vs))
+    )
+  end
+
+  def test_variable_substitution()
+    v = @model.variables
+
+    v[1].be_replaced_by(v[0])
+
+    assert_match("+( v_0 , v_0 , v_2 , v_3 ) == +( v_0 , v_0 , v_2 , v_3 )",
+                 @model.constraints[2].to_s)
+  end
+
+  def test_variable_substitution_complex
+    simplify = Simplificator.new(@tableModel)
+    simplify.remove_duplicate_variables
+    assert_match("+( plouf_0_0 , plouf_0_0 , plouf_1_0 , plouf_0_0 ) == +( plouf_0_0 , plouf_0_0 , plouf_1_0 , plouf_0_0 )",
+                 @tableModel.constraints.join("\n"))
+  end
+
+  def test_detects_duplicataes
+    simplify = Simplificator.new(@model)
+    simplify.remove_duplicate_variables
+    assert_match("+( v_0 , v_0 , v_0 , v_3 ) == +( v_0 , v_0 , v_0 , v_3 )",
+                 @model.constraints.join("\n"))
+  end
+end

options.rb

-require 'slop'
+require "slop"
 
 def process_options(arg)
-begin
-  opts = Slop.parse(arg) do |o|
-    o.string '-l', '--language', 'Modeling Language (Supported: minizinc (default) or picat)', default: 'minizinc'
-    o.bool '-c', '--countdown', 'Use Countdown Backup', default: false
+  begin
+    opts = Slop.parse(arg) do |o|
+      o.string "-l", "--language", "Modeling Language (Supported: minizinc (default) or picat)", default: "minizinc"
+      o.bool "-c", "--countdown", "Use Countdown Backup", default: false
+      o.bool "-o", "--optimize", "Suppress duplicate variables"
 
-    o.on '--help', 'print the help' do
-      puts o
-      exit
+      o.on "--help", "print the help" do
+        puts o
+        exit
+      end
     end
-  end  
-rescue Slop::Error => error
-  $stderr.puts error
-  exit(2)
-end
+  rescue Slop::Error => error
+    $stderr.puts error
+    exit(2)
+  end
   opts
 end
-$options = process_options(ARGV)
\ No newline at end of file
+
+$options = process_options(ARGV)

writers/constraintwriter.rb

-require 'set'
+require "set"
 
 require_relative "abstractwriter"
 require_relative "../constraints/all"
 
 class Step1OptConstraintWriter < AbstractWriter
   def add_node_variables(node)
-    name = node.name
-    case node
-    when ConstantNode
-      matrix = ConstantTable.new(name, "int", [node.y, node.x], Array.new(node.x * node.y, 0))
-      @model.add_variables(matrix)
-      @variable_dict[node] = matrix
+    if node.kind_of?(ConstantNode)
+      table = DTable.new(node.name, "int", [node.y, node.x], Array.new(node.x * node.y, 0), constant: true)
     else
-      table = Table.new(name, "bool", [node.y, node.x])
-      @model.add_variables(table)
-      @variable_dict[node] = table
+      table = DTable.new(node.name, "bool", [node.y, node.x])
     end
+
+    @variable_dict[node] = table
+    @model.add_variables(table)
+    @model.add_variables(*table.variables)
   end
 
   def add_node_constraints(node)
@@ -80,18 +78,18 @@ class Step1OptConstraintWriter < AbstractWriter
       end
       v = modelinputvars[0]
       w = outputvar
-      4.times do |j| 
+      4.times do |j|
         model.add_constraints(IncludedIn.new(
           Sum.new(
-            v[0,j],v[1,j],v[2,j],v[3,j], w[0,j],w[1,j],w[2,j],w[3,j]
+            v[0, j], v[1, j], v[2, j], v[3, j], w[0, j], w[1, j], w[2, j], w[3, j]
           ),
-          Set[0,4,5,6,7,8]
+          Set[0, 4, 5, 6, 7, 8]
         ))
       end
       4.times do |j|
         model.add_constraints(Equivalence.new(
-          Equals.new(Sum.new(v[0,j],v[1,j],v[2,j],v[3,j]), 0),
-          Equals.new(Sum.new(w[0,j],w[1,j],w[2,j],w[3,j]), 0)
+          Equals.new(Sum.new(v[0, j], v[1, j], v[2, j], v[3, j]), 0),
+          Equals.new(Sum.new(w[0, j], w[1, j], w[2, j], w[3, j]), 0)
         ))
       end
       # res += "constraint forall(j in 0..3) (\n";