; EXPECT: unsat
; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
(set-logic LIA)

(define-fun get-y ((currPoint Int)) Int 
(ite (< currPoint 10) 0 (ite (< currPoint 20) 1 (ite (< currPoint 30) 2 (ite (< currPoint 40) 3 (ite (< currPoint 50) 4 (ite (< currPoint 60) 5 (ite (< currPoint 70) 6 (ite (< currPoint 80) 7 (ite (< currPoint 90) 8 9))))))))))

(define-fun get-x ((currPoint Int)) Int
	(- currPoint (* (get-y currPoint) 10)))
(define-fun interpret-move (( currPoint Int ) ( move Int)) Int
(ite (= move 0) currPoint 
(ite (= move 1)  (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10))     currPoint (+ currPoint  10)) 
(ite (= move 2)  (ite (or (< (+ (get-x currPoint) 1) 0) (>= (+ (get-x currPoint) 1) 10))     currPoint (+ currPoint  1)) 
(ite (= move 3)  (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10))     currPoint (+ currPoint  -10)) 
(ite (= move 4)  (ite (or (< (+ (get-x currPoint) -1) 0) (>= (+ (get-x currPoint) -1) 10))     currPoint (+ currPoint  -1)) 
currPoint))))))

(define-fun interpret-move-obstacle-0 (( currPoint Int ) ( move Int)) Int
(ite (= move 0)  (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10))     currPoint (+ currPoint  10)) 
(ite (= move 1)  (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10))     currPoint (+ currPoint  -10)) 
currPoint)))

(define-fun interpret-move-obstacle-1 (( currPoint Int ) ( move Int)) Int
(ite (= move 0)  (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10))     currPoint (+ currPoint  10)) 
(ite (= move 1) currPoint 
(ite (= move 2)  (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10))     currPoint (+ currPoint  -10)) 
currPoint))))

(define-fun allowable-move-obstacle-0 (( start Int ) ( end Int)) Bool
	(or (= (interpret-move-obstacle-0 start 0) end)
	(or (= (interpret-move-obstacle-0 start 1) end) false)))

(define-fun allowable-move-obstacle-1 (( start Int ) ( end Int)) Bool
	(or (= (interpret-move-obstacle-1 start 0) end)
	(or (= (interpret-move-obstacle-1 start 1) end)
	(or (= (interpret-move-obstacle-1 start 2) end) false))))

(define-fun get-move-obstacle-0 (( start Int ) ( end Int)) Int
	(ite (= (interpret-move-obstacle-0 start 0) end) 0 
	(ite (= (interpret-move-obstacle-0 start 1) end) 1  -1)))

(define-fun get-move-obstacle-1 (( start Int ) ( end Int)) Int
	(ite (= (interpret-move-obstacle-1 start 0) end) 0 
	(ite (= (interpret-move-obstacle-1 start 1) end) 1 
	(ite (= (interpret-move-obstacle-1 start 2) end) 2  -1))))

(define-fun no-overlap-one-move-combination-2-2 ((p0 Int) (p1 Int) (p2 Int) (p3 Int)) Bool
	(and (not (= p0 p2)) (and (not (= p0 p3)) (and (not (= p1 p2)) (and (not (= p1 p3)) true)))))

(define-fun no-overlaps-0 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool
	(= 1
	(ite (= move 0) 
		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
	(ite (= move 1) 
		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
	(ite (= move 2) 
		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
	(ite (= move 3) 
		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
	(ite (= move 4) 
		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) 0)))))))

(define-fun no-overlaps-1 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool
	(= 1
	(ite (= move 0) 
		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
	(ite (= move 1) 
		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
	(ite (= move 2) 
		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
	(ite (= move 3) 
		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
	(ite (= move 4) 
		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) 0)))))))

(define-fun no-overlaps-one-step-helper ((currPoint Int) (move Int) (o0-t Int) (o0move Int) (o1-t Int) (o1move Int)) Bool
	(and (no-overlaps-0 currPoint move o0-t o0move) (and (no-overlaps-1 currPoint move o1-t o1move) true)))

(define-fun no-overlaps-one-step ((currPoint Int) (move Int)  (o0-0 Int) (o0-1 Int) (o1-0 Int) (o1-1 Int)) Bool
	(no-overlaps-one-step-helper currPoint move o0-0 (get-move-obstacle-0 o0-0 o0-1) o1-0 (get-move-obstacle-1 o1-0 o1-1)))



(declare-var o0-1 Int)
(declare-var o0-2 Int)
(declare-var o0-3 Int)
(declare-var o1-1 Int)
(declare-var o1-2 Int)
(declare-var o1-3 Int)

(synth-fun move ((currPoint Int) (o0 Int) (o1 Int)) Int
	((Start Int (
		MoveId
		(ite StartBool Start Start)))
    (MoveId Int (0
		1
		2
		3
		4
  	))
	(CondInt Int (
		(get-y currPoint) ;y coord
		(get-x currPoint) ;x coord
		(get-y o0)
		(get-x o0)
		(get-y o1)
		(get-x o1)
		(+ CondInt CondInt)
		(- CondInt CondInt)
		-1
		0
		1
		2
		3
		4
		5
		6
		7
		8
		9
				))
	(StartBool Bool ((and StartBool StartBool)
		(or  StartBool StartBool)
		(not StartBool)
		(<=  CondInt CondInt)
		(=   CondInt CondInt)
		(>=  CondInt CondInt))))) 
 
 (constraint (or 
	(and
		(= (interpret-move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) (move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) o0-2 o1-2)) 30)
		(and (no-overlaps-one-step 0 (move 0 99 98) 99 o0-1 98 o1-1) (and (no-overlaps-one-step (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1) o0-1 o0-2 o1-1 o1-2) (and (no-overlaps-one-step (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) (move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) o0-2 o1-2) o0-2 o0-3 o1-2 o1-3) true))))
	(not (and (allowable-move-obstacle-0 99 o0-1) (and (allowable-move-obstacle-0 o0-1 o0-2) (and (allowable-move-obstacle-0 o0-2 o0-3) (and (allowable-move-obstacle-1 98 o1-1) (and (allowable-move-obstacle-1 o1-1 o1-2) (and (allowable-move-obstacle-1 o1-2 o1-3) true)))))))))
(check-synth)