1

固定小数点phiの要素の制約を取得したいのですが、次の例では、制約はc2 <= c1 + 5.0、c1> = 5.0である必要があります。これは、Z3でどのように実現するかです。または、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))
4

1 に答える 1

2

Z3は、最小不動点の計算を試みません。到達可能性（派生可能性）を確立するか、クエリが到達可能ではない（派生可能）ことを伴う不動点を確立しようとします。したがって、一連のルールから最小不動点を取得する方法は提供されません。

指定することにより

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

Z3は、クエリを満たす最小不動点のメンバーに対応するものを出力します。

于 2012-09-03T12:49:14.023 に答える