From 12facee82f0bfdbda62fd422d2959cb04b497026 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 20 Oct 2015 14:44:52 +0200 Subject: [PATCH] add ar --- ar/assignments/src/2.py | 39 +++++++++++++++++++++------------------ 1 file changed, 21 insertions(+), 18 deletions(-) diff --git a/ar/assignments/src/2.py b/ar/assignments/src/2.py index f276fcb..0d935af 100644 --- a/ar/assignments/src/2.py +++ b/ar/assignments/src/2.py @@ -1,13 +1,16 @@ #!/usr/bin/env python3 -pc = [(4, 22), (4, 22), (4, 22)] +pc = [(4, 2), (4, 2), (4, 2)] rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)] +mx = 29 +my = 22 +pd = 17 -##Print preamble +# Print preamble print("(benchmark a4.smt") print(":logic QF_UFLIA") -##Print variables +# Print variables print(":extrafuns (") for i, (w, h) in enumerate(pc+rc, 1): print("(c{:02d}x Int)".format(i), end=' ') @@ -16,26 +19,26 @@ for i, (w, h) in enumerate(pc+rc, 1): print("(c{:02d}h Int)".format(i), end=' ') print(")") -##Preamble2 +# Preamble2 print(":formula") print("(and") -##Print the PC and RC subformulas +# Print the PC and RC subformulas for i, (w, h) in enumerate(pc+rc, 1): - ##Print the width and height + # Print the width and height print(( '\t(or ' '(and (= c{0:02d}w {1}) (= c{0:02d}h {2})) ' '(and (= c{0:02d}w {2}) (= c{0:02d}h {1}))' ')').format(i, w, h)) - ##Print the bounds of the coordinates + # Print the bounds of the coordinates print(( '\t(> c{0:02d}x 0) (> c{0:02d}y 0)\n' - '\t(<= (+ c{0:02d}x c{0:02d}w) 29) (<= (+ c{0:02d}y c{0:02d}h) 22)\n' - ).format(i, w, h)) + '\t(<= (+ c{0:02d}x c{0:02d}w) {1}) (<= (+ c{0:02d}y c{0:02d}h) {2})\n' + ).format(i, mx, my)) - ##Print the non overlap with others + # Print the non overlap with others for j in range(1, 1+len(pc+rc)): print(( '\t(or (= {0} {1})\n' @@ -45,18 +48,18 @@ for i, (w, h) in enumerate(pc+rc, 1): '(< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)' ')').format(i, j)) -##Print the PC distance to eachother +# Print the PC distance to eachother for i, _ in enumerate(pc, 1): for j, _ in enumerate(pc, 1): print(( '\t(or (= {0} {1})\n' - '\t\t(> (- (/ (+ c{0:02d}x c{0:02d}w) 2) (/ (+ c{1:02d}x c{1:02d}w) 2)) 17)\n' - '\t\t(> (- (/ (+ c{1:02d}x c{1:02d}w) 2) (/ (+ c{0:02d}x c{0:02d}w) 2)) 17)\n' - '\t\t(> (- (/ (+ c{0:02d}y c{0:02d}h) 2) (/ (+ c{1:02d}y c{1:02d}h) 2)) 17)\n' - '\t\t(> (- (/ (+ c{1:02d}y c{1:02d}h) 2) (/ (+ c{0:02d}y c{0:02d}h) 2)) 17)' - ')').format(i, j)) + '\t\t(> (- (/ (+ c{0:02d}x c{0:02d}w) 2) (/ (+ c{1:02d}x c{1:02d}w) 2)) {2})\n' + '\t\t(> (- (/ (+ c{1:02d}x c{1:02d}w) 2) (/ (+ c{0:02d}x c{0:02d}w) 2)) {2})\n' + '\t\t(> (- (/ (+ c{0:02d}y c{0:02d}h) 2) (/ (+ c{1:02d}y c{1:02d}h) 2)) {2})\n' + '\t\t(> (- (/ (+ c{1:02d}y c{1:02d}h) 2) (/ (+ c{0:02d}y c{0:02d}h) 2)) {2})' + ')').format(i, j, pd)) -#Print the constraint that they have to be connected to a ps +# Print the constraint that they have to be connected to a ps for i, _ in enumerate(rc, 1+len(pc)): print('\t(or') for j, _ in enumerate(pc, 1): @@ -68,5 +71,5 @@ for i, _ in enumerate(rc, 1+len(pc)): ).format(i, j)) print('\t)') -## Close the and,benchmark parenthesis +# Close the and,benchmark parenthesis print("))") -- 2.20.1