0

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

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

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

4

2 回答 2

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 将始终能够进行分解，尽管速度很慢，前提是您没有先耗尽内存或耐心！

于 2020-01-12T21:22:33.327 回答
0

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

(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（十六进制的输入），我使用了十进制的 45054 的“affe”。它也应该适用于更大的。

输出：

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

希望这会在未来对其他人有所帮助。

于 2020-01-13T22:35:36.853 回答