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

Question

我想得到d>=0.0这样的定点phi中元素的约束，在Z3中如何实现？

(set-option :produce-models true)
(set-option :dl_engine 1)
(set-option :dl_pdr_use_farkas true)
(declare-var c Real)
(declare-var d Real)
(declare-var lambda Real)
(declare-rel phi(Real))
(rule 
   (=>
      (and
        (>= lambda 0.0)
        (phi c)
      )
      (phi (+ c lambda))
   )
)
(rule 
    (=>
       (= c 0.0)
       (phi c)
    )
)
(rule
     (=>
        (phi c)
        (phi d)
     )
 )
(query (phi d))

Answer 1

有两个主要选项可以从 定点引擎。 :print-answer true 将导致引擎显示一个或多个实例 满足查询（取决于引擎）。 :print-certificate true 会导致引擎 打印一条线索来解释答案。如果无法满足查询，则 PDR 引擎 将打印一个查询为空的证书（当然，如果它收敛）。

目前 dl 引擎会打印答案（当查询得到满足时）
作为沿着满足查询的跟踪的谓词的合取。 所以：

(query (phi d) 
  :print-answer true)

将返回：

sat
(and (query!0 0.0) (phi 0.0))

表示可以导出0.0的值。 我计划在未来的版本中更改此格式 由于格式并不完全一致， 但我希望这对你有用。

你也可以这样调用它：

(query (phi d) 
  :print-certificate true)

它会返回一个类似的连词（但带有一个省略十进制符号的漂亮打印机）。