Support for SMT literals
pieter-bos opened this issue · 1 comments
It would be nice if SMT literals are supported via the interpretations of domain (functions), so you can e.g. define literal bitvectors:
domain bv1 interpretation (SMTLIB: "(_ BitVec 1)", Boogie: "bv1") {
function bv1_mk(): bv1 interpretation "#b0"
}
Although this doesn't quite lex I can submit it via vercors, and then it nearly works. Carbon accepts it, but silicon qualifies the literal as though it is an identifier: (as #b0 (_ BitVec 1))
. (By our own fault) this is not valid smt, since you can only qualify identifiers, not literals and other expressions.
I'm reporting this at the silicon repository initially because there is a possible straightforward approach: you could drop the as
in smt function applications (as it is in carbon/boogie now). Looking at the smtlib theories, I don't think there actually is room for any type confusion for built-in smtlib types, e.g. the floating point zero includes sufficient information in the actual term:
; Plus and minus zero
:funs_description "All function symbols with declaration of the form
((_ +zero eb sb) (_ FloatingPoint eb sb))
((_ -zero eb sb) (_ FloatingPoint eb sb))
where eb and sb are numerals greater than 1."
:note
"The +zero and -zero symbols are abbreviations for the corresponding fp literals.
E.g., (_ +zero 2 4) abbreviates (fp #b0 #b00 #b000)
(_ -zero 3 2) abbreviates (fp #b1 #b000 #b0)
"
It should thus be safe to discard as
.
Silicon now omits the "as". A fix of the parser (to allow "#b0") will follow.