1

我希望得到像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))
4

1 回答 1

2

从定点引擎获取信息有两个主要选项。: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)

并且它返回一个类似的连词(但带有一个省略十进制符号的漂亮打印机)。

于 2012-09-02T22:23:17.567 回答