用户定义的 z3 排序问题答案

【问题标题】：Problems with user defined z3 sorts用户定义的 z3 排序问题
【发布时间】：2018-02-10 10:59:40
【问题描述】：

我正在尝试在 z3 中定义一个新的分数排序，以便更好地了解 z3 的工作原理。我正在使用此查询并定义两个分数之间的相等性：

;;;;;;;;;;;;;;;;;;;
;; TEMPLATE CTOR ;;
;;;;;;;;;;;;;;;;;;;
(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))

;;;;;;;;;;;;;;;;;;;;;;
;; SORT DEFINITIONS ;;
;;;;;;;;;;;;;;;;;;;;;;
(define-sort Fraction () (Pair Int Int))

;;;;;;;;;;;;;;;;;;;;;;;;;;
;; FUNCTION DEFINITIONS ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-fun Fraction_Eq ((f1 Fraction) (f2 Fraction)) Bool
    (if (= (* (first f1) (second f2))
           (* (first f2) (second f1)))
        true
        false
    )
)

(declare-const x1 Fraction)
(declare-const x2 Fraction)
(declare-const x3 Fraction)

(assert (Fraction_Eq x1 (mk-pair 3 5)))
(assert (Fraction_Eq x2 (mk-pair 4 7)))
(assert (Fraction_Eq x3 (mk-pair 8 9)))

(check-sat)
(get-value (x1 x2 x3))

我预计 x1 将等于 3/5，但事实并非如此。这是我得到的答案：

sat
((x1 (mk-pair 0 0))
 (x2 (mk-pair 1304 2282))
 (x3 (mk-pair 0 0)))

有人可以帮忙吗？谢谢！

【问题讨论】：

标签： z3 smt

【解决方案1】：

等式

 n * 5 = d * 3

n = d = 0 非常满意。

由于除以零在普通算术中没有意义，你应该丰富你的陈述，并要求d不同于0。

请注意，这并不能保证 n, d 等于 3, 5，因为该方程有无数个解。但是，x1 的 标准化 值应该对应于 3/5。

解决方法如下：

;;;;;;;;;;;;;;;;;;;
;; TEMPLATE CTOR ;;
;;;;;;;;;;;;;;;;;;;
(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))

;;;;;;;;;;;;;;;;;;;;;;
;; SORT DEFINITIONS ;;
;;;;;;;;;;;;;;;;;;;;;;
(define-sort Fraction () (Pair Int Int))

;;;;;;;;;;;;;;;;;;;;;;;;;;
;; FUNCTION DEFINITIONS ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-fun Fraction_Eq ((f1 Fraction) (f2 Fraction)) Bool
    (if (= (* (first f1) (second f2))
           (* (first f2) (second f1)))
        true
        false
    )
)

(define-fun Fraction_Valid ((f1 Fraction)) Bool
    (not (= 0 (second f1)))
)

(declare-const x1 Fraction)
(declare-const x2 Fraction)
(declare-const x3 Fraction)

(assert (Fraction_Valid x1))
(assert (Fraction_Valid x2))
(assert (Fraction_Valid x3))

(assert (Fraction_Eq x1 (mk-pair 3 5)))
(assert (Fraction_Eq x2 (mk-pair 4 7)))
(assert (Fraction_Eq x3 (mk-pair 8 9)))

(check-sat)
(get-value (x1 x2 x3))

结果：

sat
((x1 (mk-pair 3 5))
 (x2 (mk-pair 4 7))
 (x3 (mk-pair (- 8) (- 9))))

新引入的 Fraction_Valid SmtLibv2 谓词应该防止任何分数，它所应用的分母等于零。

【讨论】：