z3

mapping.py

from z3 import *

solver = Solver()

r1 = Int("r1")
r2 = Int("r2")
r3 = Int("r3")

ra = String("ra")
rb = String("rb")
rc = String("rc")

solver.push()

solver.add(And(
    r1 == 1,
    r2 == 2,
    r3 == 3,
    ra == "a",
    rb == "b",
    rc == "c",
))

cat1_map = Function("cat1_map", IntSort(), StringSort(), BoolSort())

src = Int("src")
src1 = Int("src1")
dst = String("dst")

cat1_ok = And(
    ForAll(
        [src, src1, dst],
        Implies(
            And(src != src1, cat1_map(src, dst)),
            Not(cat1_map(src1, dst))
        ),
    ),
    ForAll(
        [src, dst],
        Implies(
            Or(And(src != r1, src != r2), And(dst != ra, dst != rb)),
            Not(cat1_map(src, dst)),
        ),
    ),
    ForAll(
        [src],
        Implies(
            src == r1,
            Or(cat1_map(src, ra), cat1_map(src, rb)),
        ),
    ),
    ForAll(
        [src],
        Implies(
            And(src == r1, cat1_map(src, ra)),
            Not(cat1_map(src, rb)),
        ),
    ),
    ForAll(
        [src],
        Implies(
            src == r2,
            Or(cat1_map(src, ra), cat1_map(src, rb)),
        ),
    ),
    ForAll(
        [src],
        Implies(
            And(src == r2, cat1_map(src, ra)),
            Not(cat1_map(src, rb)),
        ),
    ),
)

solver.add(cat1_ok)

print(solver.check())

m = solver.model()

print(m)
print("r1 -> ra", m.eval(cat1_map(r1, ra)))
print("r1 -> rb", m.eval(cat1_map(r1, rb)))
print("r1 -> rc", m.eval(cat1_map(r1, rc)))
print("r2 -> ra", m.eval(cat1_map(r2, ra)))
print("r2 -> rb", m.eval(cat1_map(r2, rb)))
print("r2 -> rc", m.eval(cat1_map(r2, rc)))