@@ -3,6 +3,17 @@ BITS = 1
33alias Vars = Array (Array (String ))
44alias Circuit = Array (Tuple (Array (String ), String ))
55
6+ def parse_input (raw : String ) : Tuple (Vars , Circuit )
7+ raw_vars, raw_circuit = raw.split(" \n\n " ).map { |r | r.lines }
8+ vars = raw_vars.map { |r | r.split(" : " ) }
9+ circuit = raw_circuit.map do |r |
10+ raw_expr, res = r.split(" -> " )
11+ expr = raw_expr.split(' ' )
12+ {expr, res}
13+ end
14+ {vars, circuit}
15+ end
16+
617def translate_to_z3 (vars : Vars , circuit : Circuit ) : String
718 [
819 * vars.map { |v | " (declare-const #{ v[0 ] } (_ BitVec #{ BITS } ))" },
@@ -58,14 +69,7 @@ positionals = ARGV.select { |a| !flags.includes?(a) }
5869
5970path = positionals[0 ]
6071raw = File .read(path)
61-
62- raw_vars, raw_circuit = raw.split(" \n\n " ).map { |r | r.lines }
63- vars = raw_vars.map { |r | r.split(" : " ) }
64- circuit = raw_circuit.map do |r |
65- raw_expr, res = r.split(" -> " )
66- expr = raw_expr.split(' ' )
67- {expr, res}
68- end
72+ vars, circuit = parse_input(raw)
6973
7074if flags.includes?(" --dump-dot" )
7175 puts translate_to_dot(vars, circuit)
0 commit comments