1

私はこの次のコードを持っています

(set-logic QF_LIA)
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (> x y))
(assert (> y z))
(push 1)
(assert (> z x))
(check-sat) ; unsat
(get-info :statistics)
(pop 1)
(push 1)
(check-sat (= x w)) ; sat

コードは最初にunsat（check-sat）を返し、2番目にsat（check-sat）を返すはずですが、不明になります。

誰かが何が問題なのか教えてもらえますか？私はWindows7を使用していますが、cygwinを使用してjSMTLIBを使用しています

ありがとうサイフ

4

1 に答える 1

3

これを解決するために使用した jSMTLIB のバックエンドがわかりません。ただし、(check-sat (= x w))SMT-LIB v2 では合法でもありません。

その行を次のように変更すると:

(assert (= x w))
(check-sat)

Z3 の Web インターフェイスから取得できます。これは期待どおりunsatです。sat

(get-info :statistics)も間違っていることに注意してください。正しいオプションは(get-info :all-statistics)です。SMT-LIB v2 標準の詳細については、ドキュメントを参照してください。

于 2012-02-23T00:15:00.457 に答える