位向量函数 Z3

Question

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

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

我正在尝试弄清楚如何使用算术函数，但效果不是很好。这个问题（对我来说）是函数的正确语法&&如何在其中设置值。

(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)

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

Answer 1

看起来您几乎掌握了所有内容，但可能语法不正确。这是 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 的乘法溢出，我们正在实现该目标。

对于这个输入，z3 说：

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

正确地将数字 18（此处以十六进制表示为 12）分解为 2 和 9。

注意乘法是一道难题。随着您增加位大小（这里您选择了 48，但可以更大），或者如果数字 c 本身变大，z3 将变得越来越难解决这个问题。这当然不足为奇：一般来说，因式分解是一个难题，对于 z3 来说，在不求解大量内部方程的情况下正确分解输入值并没有什么魔力，随着位宽的增加，这些方程的大小呈指数级增长.

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

Answer 2

这就是我现在所做的。将来可能会对其他人有所帮助：

(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 #x00000000affe)) 
(assert (= c (bvmul a b)))

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

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

(check-sat)
(get-model)

我又添加了两个断言来确保a或b不超过c（十六进制输入）在此示例中，我使用了 "affe"，即十进制的 45054。它也应该适用于更大的。

输出：

sat
(model 
  (define-fun b () (_ BitVec 48)
    #x00000000138e)
  (define-fun a () (_ BitVec 48)
    #x000000000009)
  (define-fun c () (_ BitVec 48)
    #x00000000affe)
)

十六进制：138e * 9 = affe

十二月：5006 * 9 = 45054

希望这对以后的其他人有所帮助。

位向量函数 Z3

Bitvector function Z3

syntax

bitvector

smt

z3

vector-multiplication