diff options
Diffstat (limited to 'chip_design/generate-chipdesign.py')
| -rwxr-xr-x | chip_design/generate-chipdesign.py | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/chip_design/generate-chipdesign.py b/chip_design/generate-chipdesign.py index d231c8d..862053e 100755 --- a/chip_design/generate-chipdesign.py +++ b/chip_design/generate-chipdesign.py @@ -27,7 +27,6 @@ chip_w, chip_h = (30, 30) # Minimum distance between centers power_distance = 17 - all_components = powers + regulars def fillin(cases, template_vars): @@ -55,8 +54,8 @@ for i, (w, h) in enumerate(all_components): newpreds = [ '(>= {var_x} 0)', '(>= {var_y} 0)', - '(<= {var_x} {chip_w})', - '(<= {var_y} {chip_h})', + '(<= (+ {var_x} {var_w}) {chip_w})', + '(<= (+ {var_y} {var_h}) {chip_h})', ] # Dimensions are restricted: # either width and height are w, h; or they are rotated. @@ -78,10 +77,10 @@ for i in range(len(all_components)): # other (j) must be below, on the left of pivot (i). # or above or on the right (mind the width/height!). altpreds = [ - '(<= y{j} y{i})', - '(<= x{j} x{i})', + '(<= (+ y{j} h{j}) y{i})', + '(<= (+ x{j} w{j}) x{i})', '(>= y{j} (+ y{i} h{i}))', - '(>= x{j} (+ x{i} x{i}))', + '(>= x{j} (+ x{i} w{i}))', ] preds += ['(or %s)' % ' '.join(fillin(altpreds, vars()))] @@ -107,11 +106,11 @@ for i in range(len(powers)): # Begin generator s = """(benchmark test.smt -:logic QF_UFLRA +:logic QF_UFLIA :extrafuns ( """ -s += "\n".join("(%s Real)" % x for x in literals) +s += "\n".join("(%s Int)" % x for x in literals) s += """ ) :formula |