使用布尔运算符在 Z3 中定义约束 [英] Defining constraints in Z3 using Boolean operators
问题描述
比方说,我想将字符串的每个字符限制为字符集:[a-zA-Z0-9_] 使用 Z3 约束,我可以使用布尔运算符来指定吗?
举个例子:
input = [BitVec("input%s" % i, 8) for i in range(10)]对于范围内的我(10):s.add(input[i] >= 0x30 and input[i] <= 0x39)s.add(input[i] >= 0x41 and input[i] <= 0x5A)s.add(input[i] >= 0x61 and input[i] <= 0x7A)
这是正确的吗?还有其他有效的方法来定义约束吗?
通常在 Python 中,我可以执行以下操作:
导入字符串charset = string.uppercase + string.lowercase + string.digits + "_"对于我在字符集中:...
可以做类似的事情来定义 Z3 中的约束吗?
谢谢.
解决这个问题的最好方法是简单地使用 z3 的正则表达式匹配工具:
from z3 import *导入字符串lower = Union([Re(c) for c in string.lowercase])upper = Union([Re(c) for c in string.uppercase])digs = Union([Re(c) for c in string.digits])uscore = Re('_')charset = Union(lower, upper, digs, uscore)lang = Plus(字符集)s = 求解器()test = String("测试")s.add(长度(测试) == 10)s.add(InRe(test, lang))打印 s.check()打印 s.model()
打印:
sat[测试=9L25ZPC1B8"]
或者您可以使用它来测试特定字符串是否属于您定义的正则表达式:
<预><代码>>>>打印(简化(InRe(hEllO_123",lang)))真的>>>打印(简化(InRe(%$",lang)))错误的Let's say, I want to restrict each character of the string to the charset: [a-zA-Z0-9_] using Z3 constraints, can I use a boolean operator to specify that?
As an example:
input = [BitVec("input%s" % i, 8) for i in range(10)]
for i in range(10):
s.add(input[i] >= 0x30 and input[i] <= 0x39)
s.add(input[i] >= 0x41 and input[i] <= 0x5A)
s.add(input[i] >= 0x61 and input[i] <= 0x7A)
Is this correct? Any other efficient way to define constraints?
Usually in Python, I could do something like:
import string
charset = string.uppercase + string.lowercase + string.digits + "_"
for i in charset:
...
Can something similar be done to define constraints in Z3?
Thanks.
The best way to go about this would be to simply use z3's regular-expression matching facilities:
from z3 import *
import string
lower = Union([Re(c) for c in string.lowercase])
upper = Union([Re(c) for c in string.uppercase])
digs = Union([Re(c) for c in string.digits])
uscore = Re('_')
charset = Union(lower, upper, digs, uscore)
lang = Plus(charset)
s = Solver()
test = String("test")
s.add(Length(test) == 10)
s.add(InRe(test, lang))
print s.check()
print s.model()
This prints:
sat
[test = "9L25ZPC1B8"]
Or you can use it to test whether particular strings belong to the regular-expression you've defined:
>>> print (simplify(InRe("hEllO_123", lang)))
True
>>> print (simplify(InRe("%$", lang)))
False
这篇关于使用布尔运算符在 Z3 中定义约束的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!