0
関数定義をソルバにアサーションとして追加する方法はありますか？z3：アサーションで変数宣言を追加
私は現在、C++ファイルの限定モデル検査に取り組んでおり、assert文がソルバアサーションとコード行に一対一に対応するように定義を追加できるようになっています。例えば
私は次のおもちゃのプログラムを持っている：
(declare-fun |main::1::[email protected]#1|() (_ BitVec 32))
(define-fun |main::1::[email protected]#2|() (_ BitVec 32) (bvadd (_ bv1 32) |main::1::[email protected]#1|))
(define-fun |B0|() Bool (= |main::1::[email protected]#1| |main::1::[email protected]#1|))
(assert (not (not (= |main::1::[email protected]#2| (_ bv0 32)))))
次の式を返しz3_parse_string：
int x, y;
x = y + 1;
assert(x != 0)
CBMCは、次のSMT2ファイルを生成します。
Not(Not(1 + main::1::[email protected]#1 == 0))
私はそれの線に沿って何か、ならびにソルバーに関数宣言を追加することが可能であるかどうかを疑問に思った。
([email protected]#2 == 1 + [email protected]#1) AND !([email protected]#2 == 0)
は、したがって、各句は、ソースコードの一行に緩く対応します。
私は（私が間違っているなら、私を修正してください） 私は考えることができる唯一のソリューションを定義するようなファイルを変更している現在、z3_parse_string APIは唯一の（主張...ラインにアクセスし、そこから折りたたみないことを理解-funを宣言し、楽しくなって、定義のような新しいアサーションラインに押し込まれる：事前に
(declare-fun |main::1::[email protected]#2|() (_ BitVec 32))
(assert (= |main::1::[email protected]#2| (bvadd (_ bv1 32) |main::1::[email protected]#1|)))
感謝
ええ、z3_parse_stringはユーザフレンドリーではありません。宣言ビットを新しいアサーション句にシフトするために自分のパーサを考え出す必要がありました。 CBMCはsmt2ファイルを生成し、z3をネイティブに呼び出すだけで、関連する変数の割り当てを取得し、それを使用してエラートレースを生成します。 ありがとう – user3146687