我的代码是
def test():
s = Solver()
a = Int('x')
b = Int('y')
s.add(a*b==22)
print s.check()
return s.model()[a], s.model()[b]
这将打印数字，但是当你看到type(s.model()[a])or时type(s.model()[b])，它会给出<type 'instance'>. 如何以它会返回的方式投射它<type 'int'>？我无法在我的代码中进一步使用返回类型，因为它返回实例，即使它print s.model()[a]看起来像一个整数，但事实并非如此。
这是一个由三部分组成的问题，涉及 Z3 (Z3Py) 的 Python API 的使用。
我以为我知道常量和变量之间的区别，但显然不知道。我想我可以声明一种排序并实例化该排序的变量，如下所示：
Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Node('n1') # c.f. x = Int('x')
但是 python 抛出一个异常，说你不能“调用 Node”。似乎唯一有效的是声明n1一个常量
Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Const('n1',Node)
但我对此感到困惑，因为我认为 a1,a2,a3 是常数。也许 n1 是一个符号常量，但我如何声明一个实际变量？
如何创建常量集？我尝试从一个空集开始并添加到其中，但这不起作用
Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Const('n1',Node)
nodes = EmptySet(Node)
SetAdd(nodes, a1) #<-- want to create a set {a1}
solve([IsMember(n1,nodes)])
但这不起作用 Z3 没有返回任何解决方案。另一方面，将第三行替换为
nodes = Const('nodes',SetSort(Node))
现在过于宽松，允许 Z3 将节点解释为满足公式所需的任何节点集。如何只创建集合 {a1}？
除了看起来有点麻烦的数据类型声明之外，是否有一种简单的方法来创建对？例如
Edge = Datatype('Edge')
Edge.declare('pr', ('fst', Node), ('snd',Node)) …有没有办法对 a 中的元素进行索引BitVec？我想要这样的事情：
s = Solver()
x = BitVec('x', 8)
s.add(Not(And(x[0], x[2])))
或者屏蔽是隔离位的唯一方法：
s.add(x & 5 != 5)
我是 Z3 的新手，正在尝试制作一个求解器，将每个可满足的解决方案返回到布尔公式。从其他 SO 帖子中记下笔记，我已经编写了我希望能起作用的代码，但事实并非如此。问题似乎是，通过添加以前的解决方案，我删除了一些变量，但它们又在后面的解决方案中返回了？
目前我只是想解决a或b或c。
如果我解释得不好，请告诉我，我会尽力进一步解释。
预先感谢您的回复:)
我的代码：
from z3 import *
a, b, c = Bools('a b c')
s = Solver()
s.add(Or([a, b, c]))
while (s.check() == sat):
print(s.check())
print(s)
print(s.model())
print(s.model().decls())
print("\n")
s.add(Or([ f() != s.model()[f] for f in s.model().decls() if f.arity() == 0]))
我的输出：
sat
[Or(a, b, c)]
[c = False, b = False, a = True]
[c, b, a]
sat
[Or(a, b, c), Or(c != False, b != False, a != True)]
[b = True, …我对 SAT 和 Z3 很陌生（甚至还没有开始使用 SMT）。我一直在玩gophersat（一个很好的 Go 实现，可以解决一系列很好的 SAT 问题），我在那里发现了 DIMACS 格式。尽管我同意这不是使用变量的最佳方式，但对于一些简单的测试，我发现它非常方便。我尝试检查是否有直接方法从 Z3 中的 DIMACS 文件读取、解析和构造 SAT 公式。我没有找到任何（如上所述，我很新，所以我可能不知道它的存在）。所以我最终编写了以下代码。我想知道人们对此有何看法以及是否有更好的方法来实现同样的目标。
\n（注意：我没有对公式的子句数量和/或变量数量进行任何检查）
\nfrom z3 import *\n\n\ndef read_dimacs_and_make_SAT_formula(file_name: str):\n vars = dict()\n base_name = "x"\n with open(file_name, "r") as f:\n for idx, line in enumerate(f):\n if line.strip() != "\\n" and line.strip() != "" and line.strip() != "\\r" and line.strip() != None and idx > 0:\n splitted_vals = line.split()\n for element in splitted_vals:\n if int(element) != 0:\n if int(element) > 0 …采取这个简单的代码：
from z3 import *
a, b, c, d = Ints('a b c d')
s = Solver()
s.add(a>0)
s.add(b>1)
s.add(c>0)
s.add(d>0)
s.add(a*b - c*d< 20)
s.add(d/a+b/d > 2)
s.add((a*c)/(b*d) > 3)
s.check()
s.model()
这给了我：
[d = 8,
a = 4,
c = 64,
b = 8,
div0 = [(8, 4) -> 2, (256, 64) -> 4, else -> 1],
mod0 = [else -> 0]]
这是版本 4.8.12。
div0 和 mod0 行是什么意思？
我试图用Skolemization去除我的理论中的存在量词.这意味着我用存在量词范围内的通用量化变量参数化的函数替换存在量词.
在这里我找到了如何在Z3中做到这一点的解释,但我仍然遇到麻烦.假设有以下两个函数:
(define-fun f1 ((t Int)) Bool (= t 3))
(define-fun f2 () Bool (exists ((t Int)) (f1 t)))
我认为f2应该是真的,因为存在一个t这样的整数(f1 t),即t=3.我通过引入存在量化公式的常数来应用Skolemization:
(define-const c Int)
然后将具有存在量词的公式重写为:
(define-fun f2 () Bool (f1 c))
这不起作用,也就是说,常量c没有值3.我怀疑这是因为我们没有对常量给出解释c,因为如果我们添加(assert (= c 3))它就可以正常工作,但这会夺走存在的整个想法量词.有没有一种方法我可以给出一个不那么明确的解释,c以便这样做？
有没有办法在SMTLIB2中转换BitVector和FP,比如int2bv和bv2int函数？
为了澄清,我正在寻找位的原始表示,而不是例如BitVec形式的舍入整数.
理想情况下,可以将'或'两个数字表示为位向量,但我无法做到.请告诉我们代码中是否有错误或其他错误
line1 = BitVec('line1', 1)
line2 = BitVec('line2', 1)
s = Solver()
s.add(Or(line1, line2) == 0)
print s.check()
给出的错误是
error: 'type error'
WARNING: invalid function application for or, sort mismatch on argument at position 1, expected Bool but given (_ BitVec 1)
WARNING: (declare-fun or (Bool Bool) Bool) applied to:
line1 of sort (_ BitVec 1)
line2 of sort (_ BitVec 1)
从这个错误我明白,或者只能为bool变量做.我的问题是如何或为BitVectors
我正在尝试连接两个8位字节和一个16字:
from z3 import *
byte1 = BitVec('byte1', 8)
byte2 = BitVec('byte2', 8)
word = BitVec('word', 16)
s = Solver()
s.add(word==(byte1<<8) | byte2)
但是我收到了错误:
WARNING: invalid function application, sort mismatch on argument at position 2
WARNING: (define = (bv 16) (bv 16) Bool) applied to:
word of sort (bv 16)
(bvor (bvshl byte1 bv[8:8]) byte2) of sort (bv 8)
...
z3types.Z3Exception: 'type error'
这样做的正确方法是什么？