0

我有一个未解释的函数，其值是由一些约束计算的。

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的实际值是多少。

问题 ：

  1. 如何使用 SMT2 格式打印值？
  2. 是否可以/容易使用 C API 打印它？
4

1 回答 1

1

下面的呢？

(declare-fun m05 () Int)
(declare-fun m15 () Int)
(assert (= m05 (matrix 0 5)))
(assert (= m15 (matrix 1 5)))
(check-sat)
(get-model)
于 2013-03-29T18:05:23.407 回答