SMTLIB/z3/stp：下劃線的含義？

Question

我不明白下劃線的意思，例如在這些（無關）表達

[source]

(display (_ bv20 8)) 
(declare-const x (_ BitVec 64)) 

或本：

(declare-fun a() (Array (_ BitVec 32) (_ BitVec 7))) 

[source]

什麼是 「_」 是什麼意思？

Answer 1

根據SMTLIB手冊的§3.3 Identifiers部分，(_ <symbol> <index>+)是一種定義索引標識符的方法。我認爲這相當於編碼其他語言標識符內部的信息，如int_64，除了數據具有更明確的結構。