位向量函数 Z3

问题描述

我想在 z3 求解器中用位向量 48 解决这个问题:

I want to solve this in the z3 solver with bit vector 48:

(declare-fun x () Int)
(declare-fun y () Int)
(assert (= *someNumber* (* x y)))
(assert (> x 1))
(assert (> y 1))
(check-sat)
(get-model)
(exit)

我正在尝试弄清楚如何使用算术函数，但是效果并不好.与此有关的问题(对我而言)是函数的正确语法 &&如何在那里设置值.

I'm trying to figure out how to use the arithmetic function however, it does not work out very well.The problems with that (for me) are the correct Syntax of the functions && how to set the values in there.

(set-option :produce-models true)
(set-logic QF_BV)

;; Declaring all the variables
(declare-const a (_ BitVec 48))
(declare-const b (_ BitVec 48))
(declare-const c (_ BitVec 48))

;; Soft constraints to limit reuse
(assert (= c #xnumberInHex))
(assert-soft (not (= a b)))

(check-sat-using (then simplify solve-eqs bit-blast sat))
(simplify (= c (bvmul a b))
(simplify (bvugt a #b000000000001))
(simplify (bvugt b #b000000000001))
(check-sat)
(get-model)

非常感谢任何帮助.语法/如何在那里编写正确的位向量

Any help is much appreciated.Syntax / how to write the correct bit vector there

推荐答案

看起来您已经掌握了几乎所有的部分，但可能没有完全正确地使用语法.这是一个带有 c = 18 的完整编码:

Looks like you've got almost all the pieces in there, but perhaps not exactly getting the syntax right. Here's a complete encoding with c = 18:

(set-option :produce-models true)
(set-logic ALL)

;; Declaring all the variables
(declare-const a (_ BitVec 48))
(declare-const b (_ BitVec 48))
(declare-const c (_ BitVec 48))

(assert (= c #x000000000012)) ; 18 is 0x12 in hex
(assert (= c (bvmul a b)))

; don't allow overflow
(assert (bvumul_noovfl a b))
(assert (bvult #x000000000001 a))
(assert (bvult #x000000000001 b))

;; Soft constraints to limit reuse
(assert-soft (not (= a b)))

(check-sat)
(get-model)

注意ALL 逻辑和检测无符号位向量乘法溢出的函数bvumul_noovfl 的使用.(这个函数是 z3 特定的，只有当你选择逻辑为 ALL 时才可用.)因为你在做位向量算术，它会受到环绕，我猜测这是你想要避免的事情.通过明确声明我们不希望 a 和 b 的乘法溢出，我们正在实现这个目标.

Note the use of the ALL logic and the function bvumul_noovfl which detects unsigned bit-vector multiplication overflow. (This function is z3 specific, and is only available when you pick the logic to be ALL.) Since you're doing bit-vector arithmetic, it is subject to wrap-around, and I'm guessing this is something you'd like to avoid. By explicitly stating we do not want the multiplication of a and b to overflow, we're achieving that goal.

对于这个输入，z3 说:

For this input, z3 says:

sat
(model
  (define-fun b () (_ BitVec 48)
    #x000000000009)
  (define-fun a () (_ BitVec 48)
    #x000000000002)
  (define-fun c () (_ BitVec 48)
    #x000000000012)
)

将数字 18(此处以十六进制写成 12)正确分解为 2 和 9.

which correctly factors the number 18 (written here in hexadecimal as 12) into 2 and 9.

请注意，乘法是一个难题.随着您增加位大小(这里您选择了 48，但可以更大)，或者如果数字 c 本身变大，z3 将越来越难以解决问题.当然，这并不奇怪:因式分解通常是一个难题，对于 z3 而言，在不求解大量内部方程的情况下正确分解输入值并没有什么神奇之处，这些内部方程随着位宽的增加呈指数级增长.

Note that multiplication is a hard problem. As you increase the bit-size (here you picked 48, but could be larger), or if the number c itself gets larger, the problem will become harder and harder for z3 to solve. This is, of course, not surprising: Factorization is a hard problem in general, and there's no magic here for z3 to correctly factor your input value without solving a huge set of internal equations, which increase exponentially in size as the bit-width increases.

但不要害怕:位向量逻辑是完整的:这意味着 z3 将始终能够分解，尽管速度很慢，前提是您没有先耗尽内存或耐心！

But fear not: Bit-vector logic is complete: This means that z3 will always be able to factor, albeit slowly, assuming you do not run out of memory or patience first!

这篇关于位向量函数 Z3的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！