3

「repeat」および「rotate_left」ビットベクトル操作はどのように使用しますか?

より一般的に言えば、Z3 で使用される SMT2 スクリプト形式でのビットベクター操作の詳細なドキュメントはどこにありますか?

私が見つけたものはすべて、チュートリアルまたは壊れたリンクに行くようです:
https://github.com/Z3Prover/z3/wiki/Documentation
http://research.microsoft.com/en-us/um/redmond/projects/z3 /old/documentation.html

「repeat」、「rotate_left」、「rotate_right」を当て推量で理解しようとすると、イライラしてしまいます。それらの使い方がわかりません。例えば

(display (repeat #b01))
(display (repeat #b01 3))
(display (repeat 3))
(display (rotate_left #b0001 2))

与える

"repeat expects one non-zero integer parameter"
"repeat expects one argument"
"operator is applied to arguments of the wrong sort"
"rotate left expects one argument"

ドキュメントはどこにありますか? これはすべて標準であるため、彼らが説明していないことを願って、smt-lib.orgも見ましたが、これらの詳細もリストされていません。とてもイライラします。

4

2 に答える 2

3

dejvuthの答えに加えて：

SMT 言語は十分に文書化されています (smt-lib.org を参照)。この特定の問題については、FixedSizeBitVectors 理論とQF_BV ロジック定義が関連しています。後者には、繰り返しの定義が含まれています。

((_ repeat i) (_ BitVec m) (_ BitVec i*m))
- ((_ repeat i) x) means concatenate i copies of x

それらとは別に、David Cok は優れたSMT2 チュートリアルを書きました。

Z3 API の関数の名前は、構文が許可されている場合は SMT2 と同じです。この場合、Z3 式を構築する関数であることを示すために Z3_mk_ というプレフィックスが付けられています。

于 2015-05-20T11:43:17.733 に答える