如何使用z3获得Fixedpoint中变量的约束?

问题描述

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

I wish to get the constraint of the element in the fixedpoint p 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))

推荐答案

Z3 不尝试计算最小定点.它试图建立可达性(可推导性)或建立一个后定点意味着查询不可到达(可推导).所以它没有提供从一组规则中获得最小不动点的方法.

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.

通过指定

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

Z3 将打印与满足查询的最小不动点成员对应的内容.

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

这篇关于如何使用z3获得Fixedpoint中变量的约束?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！