0
(SUBJ)Z3Py:两个向量的不平等
这是我尝试的约束:
#!/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?