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

固定小数点エンジンから情報を取得するには、主に 2 つのオプションがあります。:print-answer true を指定すると、エンジンはクエリを満たす 1 つ以上のインスタンスを表示します (エンジンによって異なります)。:print-certificate true を指定すると、エンジンは答えを説明する証跡を出力します。クエリが満たされない場合、PDR エンジンはクエリが空であるという証明書を出力します (もちろん、収束した場合)。

現在、dl-engine は (クエリが満たされたときに) クエリを満たす
トレースに沿った述語の結合として回答を出力します。そう：

(query (phi d) 
  :print-answer true)

戻ります：

sat
(and (query!0 0.0) (phi 0.0))

つまり、値 0.0 を導き出すことができます。この形式は実際には一貫していないため、将来のリリースでこの形式を変更する予定ですが、現時点ではこれが機能することを願っています。

次のように呼び出すこともできます。

(query (phi d) 
  :print-certificate true)

同様の接続詞を返します (ただし、10 進数表記を省略したプリティ プリンターを使用します)。

于 2012-09-02T22:23:17.567 に答える