Z3のシンボリック表現全体をどのように表示するのですか？

Question

私はZ3Pyをいくつかの分析作業に使用していますが、何度も象徴的な表現をプリントアウトしたいと思います。例えば、

a = BitVecVal("test", 32) + 13 
print a 

はしかし、私はZ3表現が非常に大きくなると、それだけで完全にプリントアウトすることができないことがわかります。代わりに、「省略記号は、」どのように私は完全にZ3表現をプリントアウトすることができ、だからここに私の質問は...式を簡素化するためにかなり頻繁に

を使用するのでしょうか？私が利用できる特定のAPIはありますか？

Answer 1

最もスケーラブルな方法は、SMT-LIBのプリンタを使用することです。 例えば：

x = Int('x') 
for i in range(12): 
    x = x + x 

print x.sexpr() 

が印刷されます：

(let ((a!1 (+ (+ (+ x x) (+ x x)) (+ (+ x x) (+ x x))))) 
(let ((a!2 (+ (+ (+ a!1 a!1) (+ a!1 a!1)) (+ (+ a!1 a!1) (+ a!1 a!1))))) 
(let ((a!3 (+ (+ (+ a!2 a!2) (+ a!2 a!2)) (+ (+ a!2 a!2) (+ a!2 a!2))))) 
    (+ (+ (+ a!3 a!3) (+ a!3 a!3)) (+ (+ a!3 a!3) (+ a!3 a!3)))))) 

あなたは関数「set_pp_option」を使用して、かなりのプリンタで使用されるフォーマッタのパラメータを制御することができます。 z3printer.pyのソースコードを調べて、そのトリックを行うオプションを判断する必要があります。