用BitVec [ z3 ]调整z3的大小

Question

我需要在z3中符号化一个未知长度的字节字符串。我看到了两个选项:将每个必要的字节符号化，然后在需要应用约束时将字节连在一起，或者象征一个长字节串，在需要应用约束时提取部分。

一个长字节串似乎更方便，但当需要更多的数据时，需要调整它的大小。z3有办法做到这一点吗？

Answer 1

答案取决于你所说的“调整尺寸”的确切含义。

如果您的意思是以后要将现有位向量变量的大小更改为其他变量，则答案是“否”。一旦您声明了具有特定位向量大小的变量(或任何类型的变量)，您就不能在以后更改它。

但是，如果您的意思是是否可以从旧变量中创建一个新变量，那么是的。

扩展:您可以根据需要对2的补码数或无符号位向量进行符号扩展或零扩展，以任何新的更大的大小。(使用Concat以0或原始的符号位进行扩展。见此处：https://z3prover.github.io/api/html/namespacez3py.html#a4dfadd3cb36aaa827c9202a949a506a4)

若要收缩，可以使用Extract：https://z3prover.github.io/api/html/namespacez3py.html#a40e9429ef16134a6d9914ecdc2182e8c，方法是根据需要提取任意段。

请注意，在所有情况下，新的大小必须具体知道。关于为什么会出现这种情况，下面的线程中有一些讨论：Z3 BitVec extraction using symbolic high and low的底线是SMTLib位向量逻辑是关于固定大小的位向量，因此在编译时必须具体地知道大小(任何东西都不能代表位向量的大小)。

但是，为了强调原始点，扩展或缩小位向量只是创建了一个与旧值(符号或其他值)相同的新值，假设该值适合于新的表示。(否则您将得到模块截断。)但更重要的是，原始变量和所有依赖的表达式都不会受到此更改的影响；您只是在创建一个新的位向量。从这个意义上说，在SMT-land中，调整现有位向量变量的大小是不可能的。