Support for SMT literals

[pieter-bos]

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.

[marcoeilers]

Silicon now omits the "as". A fix of the parser (to allow "#b0") will follow.