Можно ли получить окончательную формулу CNF от Z3?

Вот моя простая кодировка. Я хотел бы получить окончательную логическую CNF, в которой представлены все эти ограничения. Есть ли в решателе Z3 возможность получить окончательную логическую 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...

С уважением


z3 z3py
person user1770051    schedule 24.07.2013    source источник
comment
stackoverflow.com/questions/10992531/convert-formula-to-cnf, используйте цели и тактики, примеры должны быть в examples папке Z3.   -  person Ayrat    schedule 25.07.2013

Ответы (1)


arrow_upward
3
arrow_downward

Как говорит Айрат, используйте цели и тактику. Вот пример: 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)
person Nikolaj Bjorner    schedule 01.08.2013