首页 文章

用户定义的z3排序问题

提问于
浏览 次
2

我正在尝试在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 回答

  • 3

    等式

    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谓词应该防止应用它的任何分数具有等于零的分母 .

    回复于

相关问题