44 echo "(benchmark a4.smt"
45 echo ":logic QF_UFLIA"
48 echo "(c${i}x Int) (c${i}y Int) (c${i}w Int) (c${i}h Int)"
55 echo "(and (= c${i}w $(wp $i)) (= c${i}h $(hp $i)))"
56 echo "(and (= c${i}w $(hp $i)) (= c${i}h $(wp $i)))"
59 echo "(> c${i}x 0) (> c${i}y 0)"
60 echo "(<= (+ c${i}x c${i}w) $MAXX) (<= (+ c${i}y c${i}h) $MAXY)"
65 echo "(> c${i}x (+ c${j}x c${j}w)) (< (+ c${i}x c${i}w) c${j}x)"
66 echo "(> c${i}y (+ c${j}y c${j}h)) (< (+ c${i}y c${i}h) c${j}y)"
76 echo "(> (- (+ c${i}x (/ c${i}w 2)) (+ c${j}x (/ c${j}w 2))) $PD)"
77 echo "(> (- (+ c${j}x (/ c${j}w 2)) (+ c${i}x (/ c${i}w 2))) $PD)"
78 echo "(> (- (+ c${i}y (/ c${i}h 2)) (+ c${j}y (/ c${j}h 2))) $PD)"
79 echo "(> (- (+ c${j}y (/ c${j}h 2)) (+ c${i}y (/ c${i}h 2))) $PD)"
90 echo "(> c${i}x (+ c${j}x 1 c${j}w)) (< (+ c${i}x c${i}w) (- c${j}x 1))"
91 echo "(> c${i}y (+ c${j}y 1 c${j}h)) (< (+ c${i}y c${i}h) (- c${j}y 1))"
99 time generate | yices-smt
-m | python3 src
/a2.py
> $1