how to get constraint of variables in Fixedpoint u

问题:

I wish to get the constraint of the element in the fixedpoint phi, in the following example, the constraint should be c2<=c1+5.0, c1>=5.0 it should be how to realize it in Z3? Or is there any way to do it not using fixedpoint in 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))

回答1:

Z3 does not attempt to compute a least fixed-point. It attempts to establish reachability (derivability) or establish a post fixed-point that entails that a query is not reachable (derivable). So it does not provide a way to obtain a least fixed-point from a set of rules.

By specifying

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

Z3 will print what corresponds to a member of the least fixed-point which satisfies the query.