fixed 1

[ar1516.git] / a2 / src / 1a.bash

diff --git a/a2/src/1a.bash b/a2/src/1a.bash
old mode 100755 (executable)
new mode 100644 (file)
index f157243..e39419f
--- a/a2/src/1a.bash
+++ b/a2/src/1a.bash
@@ -37,6 +37,7 @@ GEN
                        (= l$((i-1)) 0)
                        (or
                                (and ; now in A
+                                       (>= a$((i-1)) 29)
                                        (= l$i 1)
                                        (<= d$i (+ 29 (- $AMAX a$((i-1)))))
                                        (= a$i (+ (- a$((i-1)) 29) d$i))
@@ -46,6 +47,7 @@ GEN
 
                                        (= t$i (- t$((i-1)) d$i))
                                ) (and ; now in B
+                                       (>= b$((i-1)) 21)
                                        (= l$i 2)
                                        (<= d$i (+ 21 (- $BMAX b$((i-1)))))
                                        (= b$i (+ (- b$((i-1)) 21) d$i))
@@ -70,6 +72,7 @@ GEN
 
                                        (= t$i $TMAX)
                                ) (and ; now in B
+                                       (>= b$((i-1)) 17)
                                        (= l$i 2)
                                        (<= d$i (+ 17 (- $BMAX b$((i-1)))))
                                        (= b$i (+ (- b$((i-1)) 17) d$i))
@@ -79,6 +82,7 @@ GEN
 
                                        (= t$i (- t$((i-1)) d$i))
                                ) (and ; now in C
+                                       (>= c$((i-1)) 32)
                                        (= l$i 3)
 
                                        (<= d$i (+ 32 (- $CMAX c$((i-1)))))
@@ -104,6 +108,7 @@ GEN
 
                                        (= t$i $TMAX)
                                ) (and ; now in A
+                                       (>= a$((i-1)) 17)
                                        (= l$i 1)
                                        (<= d$i (+ 17 (- $AMAX a$((i-1)))))
                                        (= a$i (+ (- a$((i-1)) 17) d$i))
@@ -113,6 +118,7 @@ GEN
 
                                        (= t$i (- t$((i-1)) d$i))
                                ) (and ; now in C
+                                       (>= c$((i-1)) 37)
                                        (= l$i 3)
                                        (<= d$i (+ 37 (- $CMAX c$((i-1)))))
                                        (= c$i (+ (- c$((i-1)) 37) d$i))
@@ -128,6 +134,7 @@ GEN
                        (= l$((i-1)) 3)
                        (or
                                (and ; now in A
+                                       (>= a$((i-1)) 32)
                                        (= l$i 1)
                                        (<= d$i (+ 32 (- $AMAX a$((i-1)))))
                                        (= a$i (+ (- a$((i-1)) 32) d$i))
@@ -137,6 +144,7 @@ GEN
 
                                        (= t$i (- t$((i-1)) d$i))
                                ) (and ; now in B
+                                       (>= b$((i-1)) 37)
                                        (= l$i 2)
                                        (<= d$i (+ 37 (- $BMAX b$((i-1)))))
                                        (= b$i (+ (- b$((i-1)) 37) d$i))
@@ -151,16 +159,10 @@ GEN
        )
 GEN
        done
-       echo "(or"
-       for i in $(seq 0 $ITERATIONS); do
-               for j in $(seq $((i+1)) $ITERATIONS); do
-                       echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
-               done
-       done
-       echo ")))"
+       echo "))"
 }
 it=1
-while generate $it 300 | $YICES -m | pee sort "grep -q unsat"
+while generate $it 300 | $YICES | pee sort "grep -q \"^sat\""
 do
        echo $((it++))
 done