本文介绍了可以从 Z3 得到最终的 CNF 公式吗?的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
这是我的简单编码.我想得到呈现所有这些约束的最终布尔 CNF.Z3求解器中是否有任何选项可以获得最终的布尔CNF?
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...
谢谢&问候
推荐答案
正如 Ayrat 所说，使用目标和策略.这是一个例子:http://rise4fun.com/Z3Py/4I3
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')
print t(g)
这篇关于可以从 Z3 得到最终的 CNF 公式吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！