位向量函数 Z3答案

【问题标题】：Bitvector function Z3位向量函数 Z3
【发布时间】：2020-04-29 08:18:36
【问题描述】：

我想用位向量 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)

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

【问题讨论】：

标签： syntax z3 smt bitvector vector-multiplication

【解决方案1】：

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

(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

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

【讨论】：

请注意，此解决方案不保证a*b 不会溢出。从您的原始帖子中，您似乎想考虑数字，在这种情况下溢出将是一个问题。要了解原因，让我们考虑 8 位数字。以a=69、b=22 和c=238 为例。我们有69 * 22 = 238 (mod 256)，但你很难将69 和22 称为238 的因式分解。当然，这实际上取决于您要达到的目标，但一般来说，仅仅因为 a 和 b 小于 c 并不意味着它们的乘积不等于 c，除非它们是适当的因素。希望这是有道理的！
是的，我正在尝试分解一个大数字，例如“12345678”。谢谢你的澄清。
如果您要进行保理，则无法避免使用bvumul_noovfl。仅仅断言a 和b 小于c 是不够的。

【解决方案2】：

看起来你已经掌握了几乎所有的部分，但可能没有完全正确地掌握语法。这是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 将始终能够进行分解，尽管速度很慢，前提是您没有先耗尽内存或耐心！

【讨论】：