#!/usr/bin/env python3

from z3 import *

def _try (POURINGS):
    print ("* try %d" % POURINGS)
    STATES=POURINGS+1

    A=[Int('A_%d' % i) for i in range(STATES)]
    B=[Int('B_%d' % i) for i in range(STATES)]
    C=[Int('C_%d' % i) for i in range(STATES)]
    op=[Int('op_%d' % i) for i in range(STATES)]

    def Z3_min(a,b):
        return If(a<b, a, b)

    s=Solver()

    # volumes (not states):
    jug_A, jug_B, jug_C = 8,5,3

    # "columns": If(And(op==..., preconditions), And(what next state will have), ...)
    for cur in range(STATES-1):
        next=cur+1
        s.add(If(And(op[cur]==0, A[cur]>0, B[cur]<jug_B), And(B[next]==Z3_min(jug_B, B[cur]+A[cur]), A[next]==A[cur]-(B[next]-B[cur]), C[next]==C[cur]),
            If(And(op[cur]==1, A[cur]>0, C[cur]<jug_C), And(C[next]==Z3_min(jug_C, C[cur]+A[cur]), A[next]==A[cur]-(C[next]-C[cur]), B[next]==B[cur]),
            If(And(op[cur]==2, B[cur]>0), And(A[next]==A[cur]+B[cur], C[next]==C[cur], B[next]==0),
            If(And(op[cur]==3, B[cur]>0, C[cur]<jug_C), And(A[next]==A[cur], C[next]==Z3_min(jug_C, C[cur]+B[cur]), B[next]==B[cur]-(C[next]-C[cur])),
            If(And(op[cur]==4, C[cur]>0), And(A[next]==A[cur]+C[cur], B[next]==B[cur], C[next]==0),
            If(And(op[cur]==5, C[cur]>0), And(A[next]==A[cur], B[next]==Z3_min(jug_B, B[cur]+C[cur]), C[next]==C[cur]-(B[next]-B[cur])),
            False)))))))

    # no state must repeat:
    for i in range(STATES):
        for j in range(i):
            s.add(Or(A[i]!=A[j], B[i]!=B[j], C[i]!=C[j]))

    # initial and final state:
    s.add(And(A[0]==8, B[0]==0, C[0]==0))
    s.add(And(A[STATES-1]==4, B[STATES-1]==4, C[STATES-1]==0))

    if s.check()==unsat:
        return

    m=s.model()

    ops_names=["A->B", "A->C", "B->A", "B->C", "C->A", "C->B"]
    for i in range(STATES):
        print ("state %d, %d-%d-%d" % (i, m[A[i]].as_long(), m[B[i]].as_long(), m[C[i]].as_long()))
        if i!=STATES-1:
            print ("op_%d = %s" % (i, ops_names[m[op[i]].as_long()]))
    exit(0)

#_try(7)
#exit(0)

for i in range(20):
    _try(i)