stdin/smt2経由のcheck_assumptions？

SMT2標準（またはその拡張Z3）はAPIコール "check_assumptions"と同等のコマンドを提供しますか？ Josh Berdineによれば、ガードリテラルとcheck_assumptionsはプッシュポップスコープよりも処理が速いことがよくあります。しかし、私はstdio経由でZ3を使用することに悩まされており、(check-assumoptions p)を使うとunsupportedしか得られません。stdin/smt2経由のcheck_assumptions？

出典

2012-02-27 Malte Schwerhoff

smt2コマンド言語を使用している場合は、 'z3 -smtc -in'で 'get-core'コマンドを実行するとジョブが実行されます。このコマンドはSMT-LIB 2標準にはないと思います。

乾杯、ジョシュ

出典

2012-02-27 09:25:21

ありがとう、それはトリックです！ SMT-LIB2標準では言及されていませんが、現在はZ3のみをターゲットにしています。 –

注意：-smtcオプションは非推奨パーサーを有効にします（SMT 2.0標準に準拠していません）。このフロントエンドはZ3の将来のバージョンで削除されます。新しいSMT 2.0パーサーでの不十分なコア抽出については、http://stackoverflow.com/questions/8439556/soft-hard-constraints-in-z3を参照してください。 –

SMT 2.0に準拠していることは、もちろんさらに優れています。 –

stdin/smt2経由のcheck_assumptions？

答えて

関連する問題