CODEWITHSUNDEEP
pythonz3z3py
Guo Xian HO
Guo Xian HO

Reputation: 89

z3 encoding table of relations for parameters

Say I have parameters relation table for A,B,C shown below

╔══════════╦═══╦════════════╗
║    A     ║ B ║     C      ║
╠══════════╬═══╬════════════╣
║ [0...10] ║ 2 ║ [0...10]%4 ║
║ [0...10] ║ 3 ║ [0...10]%3 ║
╚══════════╩═══╩════════════╝

which means for any value of A,B,C, it must satisfy at least one row of the table. This does implicitly means that B is bounded by 2 <= B <= 3 for example. How would I encode this in z3 solver?

My current approach is using z3.Implies and take the combinations of parameters:

import z3
# encode only the first row
A_cond = z3.And(A>=0, A<=10)
B_cond = B==2
C_cond = z3.And(z3.And(C>=0, C<=10), C%4==0)
s = z3.Solver()
s.add([z3.Implies(z3.And(A_cond, B_cond), C_cond),
       z3.Implies(z3.And(A_cond, C_cond), B_cond),
       z3.Implies(z3.And(B_cond, C_cond), A_cond),]
# solve some real constraint
s.add(A + B - C > 0)
s.check()

The model returned didn't fall into the first row of the conditions since it's just implies. Is there any working and cleaner approach for this type of situation?

Upvotes: 1

Views: 122

Answers (1)

alias
alias

Reputation: 30428

I think it's much easier to just state each row separately, and take their disjunction:

from z3 import *

A, B, C = Ints('A B C')

row1 = And(A >= 0, A <= 10, B == 2, C >= 0, C <= 10, C % 4 == 0);
row2 = And(A >= 0, A <= 10, B == 3, C >= 0, C <= 10, C % 3 == 0);
rows = [row1, row2]

s = Solver()
s.add(Or(rows))

s.add(A+B-C > 0)
print (s.check())
print (s.model())

This easily extends to many rows, and you can programmatically simplify common conditions as you see fit. When run, it prints:

sat
[A = 10, B = 2, C = 4]

You can even find out which row was satisfied by running:

m = s.model()
print([i+1 for i, row in enumerate(rows) if m.evaluate(row)])

which prints:

[1]

This means row1 was satisfied, but row2 wasn't.

Upvotes: 1

Related Questions