いくつかの制約によって値が計算される未解釈の関数があります。
Z3 によって与えられたモデルには、次のステートメントが含まれています -
(define-fun matrix!2 ((x!1 Int) (x!2 Int)) Int
(ite (and (= x!1 0) (= x!2 5)) 10
(ite (and (= x!1 1) (= x!2 5)) 11
(ite (and (= x!1 0) (= x!2 1)) 1
(ite (and (= x!1 0) (= x!2 2)) 3
(ite (and (= x!1 0) (= x!2 3)) 5
(ite (and (= x!1 0) (= x!2 4)) 7
0)))))))
(define-fun k!0 ((x!1 Int)) Int
(ite (>= x!1 0) (ite (>= x!1 1) 1 0) (- 1)))
(define-fun k!1 ((x!1 Int)) Int
(let ((a!1 (ite (>= x!1 3) (ite (>= x!1 4) (ite (>= x!1 5) 5 4) 3) 2)))
(ite (>= x!1 1) (ite (>= x!1 2) a!1 1) 0)))
(define-fun matrix ((x!1 Int) (x!2 Int)) Int
(matrix!2 (k!0 x!1) (k!1 x!2)))
(matrix 0 0), (matrix 2 0), (matrix 2 2)
では、 etcの実際の値を確認したいと思います
。
質問 :
- SMT2 フォーマットを使用して値を出力する方法は?
- C APIを使用して印刷することは可能ですか/簡単ですか?