Commit 9e00d6bb authored by Adam P. Goucher's avatar Adam P. Goucher

Convert ruletree into AIGER

parent 8b1b31f1
Pipeline #56030827 passed with stages
in 7 minutes and 41 seconds
......@@ -76,6 +76,96 @@ def compress_tree(list_of_nodes, n_states, numInputs, seqonly=True):
return rt
def binarise_tree(list_of_nodes, n_states, numInputs):
n_bits = len(bin(n_states - 1)) - 2
f_states = 1 << n_bits
seqs = []
for i in range(n_bits):
seq = [[n+1, max(0, n-1), max(0, n-1)] for n in range(n_bits * (numInputs - 1))]
mapping = {}
ln = 0
for node in list_of_nodes:
depth = node[0]
children = node[1:]
if (n_states < f_states):
children += ([max(0, (depth - 1) * n_bits - 1)] * (f_states - n_states))
if (depth == 1):
children = [((x >> i) & 1) for x in children]
else:
children = [mapping[x] for x in children]
idepth = (depth - 1) * n_bits
while len(children) > 1:
idepth += 1
nc = []
for j in range(0, len(children), 2):
seq.append([idepth, children[j], children[j+1]])
nc.append(len(seq) - 1)
children = nc
mapping[ln] = len(seq) - 1
ln += 1
seq = compress_tree(seq, 2, numInputs * n_bits)
seqs.append(seq)
return seqs
def tree_to_aiger(list_of_nodes, n_states, numInputs):
seqs = binarise_tree(list_of_nodes, n_states, numInputs)
n_bits = len(seqs)
numInputs = numInputs * n_bits
inputs = [(2 * (i+1)) for i in range(numInputs)]
ands = []
outputs = []
voffset = numInputs + 1
for seq in seqs:
for (i, t) in enumerate(seq):
depth, fchild, tchild = tuple(t)
if depth > 1:
fchild = (fchild * 3 + voffset) * 2 + 5
tchild = (tchild * 3 + voffset) * 2 + 5
lit = (i * 3 + voffset) * 2
ands.append((lit, depth * 2, tchild))
ands.append((lit + 2, depth * 2 + 1, fchild))
ands.append((lit + 4, lit + 3, lit + 1))
if (i == len(seq) - 1):
outputs.append(lit + 5)
voffset += 3 * len(seq)
miloa = (voffset, len(inputs), 0, len(outputs), len(ands))
lines = ['aag %d %d %d %d %d\n' % miloa]
lines += [('%d\n' % i) for i in inputs]
lines += [('%d\n' % o) for o in outputs]
lines += [('%d %d %d\n' % a) for a in ands]
return lines
def make_tree(n_states, nhood, list_of_nodes):
numInputs = GetNumberOfInputs(nhood)
......
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