CODEWITHSUNDEEP
z3smt
langlauf.io
langlauf.io

Reputation: 3191

SMTLIB / z3 / stp: Meaning of underscore?

I don't understand the meaning of the underscore, e.g. in these (unrelated) expressions

[source]

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

or this:

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

[source]

What does the "_" mean?

Upvotes: 4

Views: 498

Answers (1)

coredump
coredump

Reputation: 38789

According to the §3.3 Identifiers section of the SMTLIB manual, (_ <symbol> <index>+) is a way to define indexed identifiers. I think that this is equivalent to encoding information inside identifiers in other languages, such as int_64, except that the data has a more explicit structure.

Upvotes: 4

Related Questions