# finding max of the numbers in z3 using SMTLIB2

#### Tags: python, sat, satisfiability, z3

I have 7 cups which contains some water. I need to program these cups to have different amounts of water. Once this is done I need to measure the cup which has the highest amount of water and then remove some quantity (say 2 units of water).

c implementations:

```float c1=2.0, c2= 2.6, c3 = 2.8, c4=4.4 , c5 = 2.4, c6 = 2.1, c7 = 5.8;

if((c1 > c2) && (c1 > c3) && (c1 > c4) && (c1 > c5) && (c1 > c6) && (c1 > c7)); c1=c1-2;

if((c2 > c1) && (c2 > c3) && (c2 > c4) && (c2 > c5) && (c2 > c6) && (c2 > c7)); c2=c2-2;

if((c3 > c2) && (c3 > c1) && (c3 > c4) && (c3 > c5) && (c3 > c6) && (c3 > c7)); c3=c3-2;

if((c4 > c2) && (c4 > c3) && (c4 > c1) && (c4 > c5) && (c4 > c6) && (c4 > c7)); c4=c4-2;

if((c5 > c2) && (c5 > c3) && (c5 > c4) && (c5 > c1) && (c5 > c6) && (c5 > c7)); c5=c5-2;

if((c6 > c2) && (c6 > c3) && (c6 > c4) && (c6 > c5) && (c6 > c1) && (c6 > c7)); c6=c6-2;

if((c7 > c2) && (c7 > c3) && (c7 > c4) && (c7 > c5) && (c7 > c6) && (c7 > c1)); c7=c7-2;
```

This will give an answer as `c7 = 3.8`

I was trying to implement this in z3 and I assigned the values to c1….c7

```ite( (and((> c1  c2) (> c1  c3) (> c1  c4) (> c1  c5) (> c1  c6) (> c1  c7)))  (= c1_1 (- c1 2)  (= c1_1 c1))
.
.
.repeated till c7_1
```

and when I get the model values it should give c7_1 as 3.8

Is it possible to define this in z3? When I am using the and’s of different conditions in if condition (in ite) its giving me an error. Can it not be defined like this? Is there someway around this?

[problem description][1]

I am experimenting with the Z3 tool, It was easy to get he first part However for the second part is being a bit difficult.

Sure. Here it is in SMTLib:

```; declare the cups
(declare-const c1 Real)
(declare-const c2 Real)
(declare-const c3 Real)
(declare-const c4 Real)
(declare-const c5 Real)
(declare-const c6 Real)
(declare-const c7 Real)

; each cup has a non-negative units of water
(assert (>= c1 0))
(assert (>= c2 0))
(assert (>= c3 0))
(assert (>= c4 0))
(assert (>= c5 0))
(assert (>= c6 0))
(assert (>= c7 0))

; each amount is different
(assert (distinct c1 c2 c3 c4 c5 c6 c7))

; find maximum, helper function
(define-fun max ((a Real) (b Real)) Real (ite (> a b) a b))

; find the cup with maximum water in it
(define-fun maxC () Real (max c1 (max c2 (max c3 (max c4 (max c5 (max c6 c7)))))))

; make sure there's at least 2 units in the max, per the problem
(assert (>= maxC 2))

; final value
(define-fun finalRes () Real (- maxC 2))

; solve
(check-sat)
(get-value (c1 c2 c3 c4 c5 c6 c7 maxC finalRes))
```

z3 says:

```sat
((c1 2.0)
(c2 (/ 11.0 6.0))
(c3 (/ 19.0 12.0))
(c4 (/ 7.0 4.0))
(c5 (/ 3.0 2.0))
(c6 (/ 23.0 12.0))
(c7 (/ 5.0 3.0))
(maxC 2.0)
(finalRes 0.0))
```

So, looks like it put `2` units in `c1`, less than `2` on all the others, so you ended up with a final value of `0` left.

Your question is rather vague in what other constraints might be at play here, but hopefully this will get you started.

Source: stackoverflow