Z3Py：兩個向量的不平等

Question

（SUBJ）

這是我嘗試的約束：

#!/usr/bin/python 
from z3 import * 

s=Solver() 

veclen=3 

tmp_false=BoolVector ('tmp_false', veclen) 
for x in range(veclen): 
    s.add(tmp_false[x]==False) 

tmp=BoolVector ('tmp', veclen) 

s.add(tmp!=tmp_false) # not working 

# I want here tmp equals to anything except False,False,False 

print s.check() 
print s.model() 

我會用元組，但在運行時向量的長度設置。 我應該使用數組嗎？ 或Z3手冊中描述的元組內的LISP-like cons-cells？

Answer 1

BoolVector函數只是創建一個列表結構。 python列表上的！=運算符不會創建表達式。它只是評估爲「真實」。所以你不是真的發表一個表達Z3。要創建元組表達式，您可以使用代數數據類型。記錄類型是代數數據類型的特例，Z3可以理解如何推理這些類型。 因此，例如，您可以編寫：

from z3 import * 

s=Solver() 

Bv = Datatype("record") 
Bv.declare('mk', ('1', BoolSort()), ('2', BoolSort()), ('3', BoolSort())) 
Bv = Bv.create() 

tmp_false = Bv.mk(False, False, False) 
tmp = Const('tmp', Bv) 

print tmp != tmp_false 
s.add(tmp!=tmp_false) 

# I want here tmp equals to anything except False,False,False 

print s.check() 
print s.model()