z3 - Z3 から最終的な CNF 式を取得できますか?

Question

これが私の単純なエンコーディングです。これらすべての制約を提示する最終的なブール CNF を取得したいと思います。最終的なブール CNF を取得するための Z3 ソルバーのオプションはありますか?

x = Int('x')
y = Int('y')

c1 = And(x >= 1, x <= 10)
c2 = And(y >= 1, y <= 10)
c3 = Distinct(x,y)

s = Solver()
s.add(c1 , c2 , c3)
# I need the final Boolean CNF formula from Z3 solver...

ありがとうございます。それでは、お元気で

Answer 1

Ayrat が言うように、目標と戦術を使用します。以下に例を示します: http://rise4fun.com/Z3Py/4I3

x = Int('x')
y = Int('y')

c1 = And(x >= 1, x <= 10)
c2 = And(y >= 1, y <= 10)
c3 = Distinct(x,y)

g = Goal()
g.add(c1 , c2 , c3)

describe_tactics()

t = Tactic('tseitin-cnf')
print t(g)