z3 - 如何使用 z3 在定点中获得变量约束？

Question

我想得到定点phi中元素的约束，在下面的例子中，约束应该是c2<=c1+5.0, c1>=5.0 在Z3中应该如何实现呢？或者有什么办法不使用 Z3 中的定点

(set-option :produce-models true)
(set-option :dl_engine 1)
(set-option :dl_pdr_use_farkas true)
(declare-var c1 Real)
(declare-var c2 Real)
(declare-var lambda Real)
(declare-rel phi(Real Real))
(rule 
   (=>
      (and
        (>= lambda 0.0)
        (phi c1 c2)
      )
      (phi (+ c1 lambda) (+ c2 lambda))
   )
)
(rule 
    (=>
       (>= c1 5.0)
       (<= c2 10.0)
       (phi c1 c2)
    )
)

(query (phi c1 c2))

Answer 1

Z3 不会尝试计算最小不动点。它试图建立可达性（derivability）或建立一个后定点，即查询不可到达（derivable）。所以它没有提供一种从一组规则中获得最小不动点的方法。

通过指定

 (query (phi c1 c2) :print-certificate true)

Z3 将打印满足查询的最小定点成员对应的内容。