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