Can get final CNF formula from Z3?

Question

Here is my simple encoding. I would like to get the final Boolean CNF that presents all these constrains. Is there any option in Z3 solver to get the final Boolean CNF ?

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...

Thanks & Regards

Answer 1

As Ayrat says, use goals and tactics. Here is an example: 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')
r = t(g)

print(r[0].dimacs())

^{(DIMACS CNF output command 🎩-tip: CoolA1d)}