add shave_dag function (needs testing)

writers/abstract_constraints_atomic.rb

@@ -5,7 +5,101 @@ require_relative '../constraints/all.rb'
 def get_abstract_constraint_model(dag)
     atoms = dag.atoms()
     operators = dag.operators()
+    # shave dag to remove useless inputs and outputs
+    atoms2,operators2 = shave_dag(atoms, operators)
     # create model
+    model = create_abstract_model(atoms, operators)
+    return model
+end
+
+
+##
+# removes operators and atoms before the initial S-box
+# this function is used to simplify as possible step1 models (less equivalent solutions)
+# @param atoms [Vec<CryptoAtom=Variable>]
+# @param operators [Vec<CryptoOperators>]
+# @return [new_atoms, new_operators]
+def shave_dag(atoms, operators)
+    # compute precedence and successors relations
+    preds, succs = *compute_precedences(atoms, operators)
+    # get input nodes (should be CryptoAtoms)
+    inputs = atoms.filter{ |n| preds.fetch(n, []).empty? }
+    # iterates over nodes to be removed
+    openlist = []
+    inputs.each do |input|
+        openlist.push(input)
+    end
+    to_shave = Set.new() # nodes to remove in the shaved model
+    s_op_to_update = Set.new() # set of SOperators to update (change their inputs)
+    visited = Set.new() # set of visited vertices (used to check if all preds are visited)
+    while !openlist.empty? do
+        n = openlist.pop
+        visited.add(n)
+        # check that all preds are visited (otherwise, delete from openlist)
+        if preds.fetch(n, []).filter{|p| !visited.include?(p)}.empty?
+            if n.class <= SOperator
+                s_op_to_update.add(n)
+            else
+                to_shave.add(n)
+                # add successors to the openlist
+                succs.fetch(n,[]).each do |s|
+                    openlist.push(s)
+                end
+            end
+        end
+    end
+    # create new dag with shaved nodes
+    atom_map = {}
+    new_atoms = []
+    atoms.each do |atom|
+        if !to_shave.include?(atom)
+            new_atom = Variable.new(atom.name, 0..1)
+            atom_map[atom] = new_atom
+            new_atoms.push(new_atom)
+        end
+    end
+    new_operators = []
+    operators.each do |op|
+        if !to_shave.include?(op)
+            new_op = op.dup
+            new_op.outputs = op.outputs.map{|ovar| atom_map[ovar]}
+            if s_op_to_update.include?(op) # if SOperator to be updated, create new input 
+                new_input = Variable.new(op.inputs[0].name, 0..1)
+                new_atoms.push(new_input)
+                new_op.inputs = [new_input]
+            else
+                new_op.inputs = op.inputs.map{|ivar| atom_map[ivar]}
+            end
+            new_operators.push(new_op)
+        end
+    end
+    # p new_atoms.map{|n| n.name.name}
+    # p new_operators.map{|n| n.class.name}
+    # p to_shave.map{|n| n.class}
+    # puts "===="
+    # p s_op_to_update.map{|n| n.class}
+    return [new_atoms, new_operators]
+end
+
+
+def compute_precedences(atoms, operators)
+    preds = {}
+    succs = {}
+    operators.each do |op|
+        op.inputs.each do |inp|
+            preds[op] = preds.fetch(op, []).push(inp)
+            succs[inp] = succs.fetch(inp, []).push(op)
+        end
+        op.outputs.each do |out|
+            preds[out] = preds.fetch(out, []).push(op)
+            succs[op] = succs.fetch(op, []).push(out)
+        end
+    end
+    return [preds, succs]
+end
+
+
+def create_abstract_model(atoms, operators)
     model = Model.new()
     variable_dict = {} # Atom -> Variable
     # add atoms as booleans