module Z3
class ModelParser macro
BLANK \s+ SL_COM \*\*\* IDENT [a-zA-Z_.$\#'`~^\\?][\w.$\#'`~^\\?]* SYMBOL [a-zA-Z_.$\#'`~^\\?!@%-\[\]][\w.$\#'`~^\\?!@%-\[\]]* OPERATOR ->|-|\(|\) KEYWORD \b(else)\b
rule
# {ML_COM_IN}(.|\n)*(?={ML_COM_OUT}){ML_COM_OUT} {SL_COM}.*(?=\n) # \"[^"]*\" { [:STRING, text[1..-2]]} {BLANK} {OPERATOR} { [text, text] } \d+ { [:NUMBER, text.to_i] } true|false { [:BOOLEAN, eval(text)] } # \d+bv\d+ { [:BITVECTOR, [text[/(\d+)bv/,1], text[/bv(\d+)/,1]]] } # bv\d+\b { [:BVTYPE, text[2..-1].to_i] } {KEYWORD} { [text, text] } # {IDENT} { [:IDENTIFIER, text.to_sym] } {SYMBOL} { [:SYMBOL, text.to_sym] } . { [text, text] }
end end