#!/bin/bash
YICES=~/projects/yices-2.4.2/bin/yices-smt
AI=40
BI=30
CI=145
AMAX=120
BMAX=120
CMAX=200

function generate {
	ITERATIONS=$1
	TMAX=$2
	cat<<GEN
(benchmark a1.smt
:logic QF_UFLIA
:extrafuns (
$(	for i in $(seq 0 $ITERATIONS); do
		echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int)"
	done)
)
:formula
(and
	;-- PRECONDITION
	(and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TMAX) (= l0 0) (= d0 0))
GEN
	for i in $(seq 1 $ITERATIONS); do
		cat<<GEN
	(> a$i 0)
	(> b$i 0)
	(> c$i 0)
	(>= d$i 0)
	(<= d$i $TMAX)
	(>= t$i 0)
	(<= t$i $TMAX)
	(or ;-- ITERATION $i
		(and ;-- WAS IN S
			(= 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))

					(= b$i (- b$((i-1)) 29))
					(= c$i (- c$((i-1)) 29))

					(= 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))

					(= a$i (- a$((i-1)) 21))
					(= c$i (- c$((i-1)) 21))

					(= t$i (- t$((i-1)) d$i))
				)
			)
		)
		(and ;-- WAS IN A
			(= l$((i-1)) 1)
			(or
				(and ; now in S
					(= l$i 0)
					(= d$i 0)

					(= a$i (- a$((i-1)) 29))
					(= b$i (- b$((i-1)) 29))
					(= c$i (- c$((i-1)) 29))

					(= 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))

					(= a$i (- a$((i-1)) 17))
					(= c$i (- c$((i-1)) 17))

					(= 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)))))
					(= c$i (+ (- c$((i-1)) 32) d$i))

					(= a$i (- a$((i-1)) 32))
					(= b$i (- b$((i-1)) 32))

					(= t$i (- t$((i-1)) d$i))
				)
			)
		)
		(and ;-- WAS IN B
			(= l$((i-1)) 2)
			(or
				(and ; now in S
					(= l$i 0)
					(= d$i 0)

					(= a$i (- a$((i-1)) 21))
					(= b$i (- b$((i-1)) 21))
					(= c$i (- c$((i-1)) 21))

					(= 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))

					(= b$i (- b$((i-1)) 17))
					(= c$i (- c$((i-1)) 17))

					(= 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))

					(= a$i (- a$((i-1)) 37))
					(= b$i (- b$((i-1)) 37))

					(= t$i (- t$((i-1)) d$i))
				)
			)
		)
		(and ;-- WAS IN C
			(= 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))

					(= b$i (- b$((i-1)) 32))
					(= c$i (- c$((i-1)) 32))

					(= 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))

					(= a$i (- a$((i-1)) 37))
					(= c$i (- c$((i-1)) 37))

					(= t$i (- t$((i-1)) d$i))
				)
			)
		)
	)
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 318 | $YICES -m | pee sort "grep -q \"^unsat\""
do
	echo $((it++))
done