我试图用z3中的数组类型来解决一个问题。 因为我需要使用BitVec类型,所以我将数组声明为:
numbers = [BitVec(chr(i), 8) for i in range(0, 4)]
然后:
s = Solver()
s.add(numbers[0] == 100)
s.add(numbers[1] == numbers[0] + 2)
s.add(numbers[3] == numbers[1] + numbers[0])
s.add(numbers[2] == numbers[1] - 4)
print(s.check())
print(s.model())
输出:
sat
[ = 98, = 202, = 102, = 100]
但是它不会按顺序打印结果,有没有方法按顺序打印?你知道吗
示例:
[ = 100, = 102, = 98, = 202 ]
我还有一个疑问。有没有办法限制一个数字的频率:
numbers = [BitVec(chr(i), 8) for i in range(0, 4)]
s = Solver()
s.add(numbers[0] == 100)
s.add(numbers[0] + numbers[1] + numbers[2] == 200)
s.add(collections.Counter(numbers)[100] == 1) # something like that
print(s.check())
print(s.model())
若要设置该数字,100必须仅出现在数字[0]中。你知道吗
对于您的第一个问题,我首先建议为变量提供一些可读的名称。
chr(i) for i in range(0, 4)
是4个无法打印的字符。最好用chr(i+48)
表示数字0..9,用chr(i+65)
表示字母A..Z以与数组相同的顺序打印结果的最简单方法是:
print ([s.model[n].as_long() for n in numbers])
。你知道吗对于第二个问题,我建议使用Z3的
Sum
函数。例如:哪些输出(在我的测试用例中):
相关问题 更多 >
编程相关推荐