import os
import sys
sys.path[0:0] = [os.path.join(sys.path[0], '../examples/sat')]
import sat

Howard = 0
George = 1
Virginia = 2
Dorothy = 3
mena = ['Howard', 'George', 'Virginia', 'Dorothy']
ludia = [Howard, George, Virginia, Dorothy]
zeny = [Virginia,Dorothy]
muzi = [Howard, George]

def O(x): # otec
    return 0+x+1

def M(x): # matka
    return 4+x+1

def S(x): # syn
    return 8+x+1

def D(x): # dcera
    return 12+x+1

def pp(x, y):
    return 16+4*x+y+1

def st(x, y):
    return 32+4*x+y+1

def ml(x, y):
    return 48+4*x+y+1

def hadanka():
    solver = sat.SatSolver()
    w = sat.DimacsWriter("vstup.txt")

    for x in ludia:
        for y in ludia:
            w.writeClause([-pp(x,y), -O(x), -M(x)])
            w.writeImpl(pp(x, y), pp(y, x))

##    zeny nie su otec/syn a muzi nie su matka/dcera
    for mnozina, rola, rola2 in [(Muzi, M, D), (Zeny, O, S)]:
        for x in mnozina:
            w.writeClause([-rola(x)])
            w.writeClause([-rola2(x)])

    for rola in [O, S]:
##        aspon jeden otec/syn | (OG v OH) | (SG v SH)
        w.writeClause([rola(Howard), rola(George)])
##        nie dvaja otcovia/synovia | -(OG ^ OH) | -(SG ^ SH)
        w.writeClause([-rola(Howard), -rola(George)])

##    muz nemoze byt oboje naraz | Ak je otec, nemoze byt syn
    for muz in Muzi:
        w.writeClause([-O(muz), -S(muz)])

##    w.writeClause([-O(Howard), -O(George)])

    for rola in [M, D]:
##        aspon jedna matka/dcera | (MV v MD) | (DV v DD)
        w.writeClause([rola(Virginia), rola(Dorothy)])
##        nie dve matky/dcery | -(MV ^ MD) | -(DV ^ DD)
        w.writeClause([-rola(Virginia), -rola(Dorothy)])

##    zena nemoze byt oboje naraz | Ak je matka, nemoze byt dcera
    for zena in Zeny:
        w.writeClause([-M(zena), -D(zena)])

    for z in zeny:
        w.writeClause([-O(z), -S(z)])

    for m in muzi:
        w.writeClause([-M(m), -D(m)])

##    tvrdenia
    tvr1 = pp(George, Dorothy)
    tvr2 = st(Howard, George)
    tvr3 = ml(Virginia, Howard)
    tvr4 = st(Virginia, Dorothy)
    tvr  = [tvr1, tvr2, tvr3, tvr4]

##    prave dva trdenia su pravdive
    for i in range(4):
        for j in range(4):
            for k in range(4):
                if i != j and j != k and i != k:
                    w.writeClause([-tvr[i], -tvr[j], -tvr[k]])
                    w.writeClause([tvr[i], tvr[j], tvr[k]])

    for x in ludia:
        for y in ludia:
            if x != y:
                w.writeClause([st(x, y), -st(y, x)])
                w.writeClause([st(x, y), -ml(x, y)])
                w.writeClause([-st(x, y), -O(y), -S(x)])
                w.writeClause([-st(x, y), -O(y), -D(x)])
                w.writeClause([-st(x, y), -M(y), -S(x)])
                w.writeClause([-st(x, y), -M(y), -D(x)])
                w.writeClause([-ml(x, y), -S(y), -O(x)])
                w.writeClause([-ml(x, y), -D(y), -O(x)])
                w.writeClause([-ml(x, y), -S(y), -M(x)])
                w.writeClause([-ml(x, y), -D(y), -M(x)])




    w.close()
    ok, sol = solver.solve(w, 'vystup.txt')

    if ok:
        for i in sol:
            i -= 1
            if 0 <= i <= 3:
                print("Otec: ", mena[i % 4])
            elif 4 <= i <= 7:
                print("Matka: ", mena[i % 4])
            elif 8 <= i <= 11:
                print("Syn: ", mena[i % 4])
            elif 12 <= i <= 15:
                print("Dcera: ", mena[i % 4])
    else:
        print("Nema riesenie")

hadanka()