z3がどのように機能するかをよりよく理解するために、z3で新しい分数ソートを定義しようとしています。私はこのクエリを使用して、2つの分数の間の同等性を定義しています。
;;;;;;;;;;;;;;;;;;;
;; 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)))
誰か助けてもらえますか？ありがとう！
方程式
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述語は、それが適用される分数がゼロに等しい分母を持つことを防ぐ必要があります。
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加