Skip to content

Instantly share code, notes, and snippets.

@yagehu

yagehu/mapping.py

Created September 5, 2024 18:27
Show Gist options
  • Save yagehu/bf2bb7faad57a7b2466a4421f859a1a0 to your computer and use it in GitHub Desktop.
Save yagehu/bf2bb7faad57a7b2466a4421f859a1a0 to your computer and use it in GitHub Desktop.
Download ZIP
z3
Raw
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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment