docs/ext/smtliblexer.py

   1 from pygments.lexer import RegexLexer
   2 from pygments import token
   3
   4
   5 class SmtLibLexer(RegexLexer):
   6     """This class implements a lexer for SMT-LIBv2.
   7     It tries to be very close to the SMT-LIBv2 standard while providing proper
   8     highlighting for everything cvc5 supports.
   9     The lexer implements the SMT-LIBv2 lexicon (section 3.1 of the standard)
  10     directly in the root state, as well as the commands, sorts and operators.
  11     Note that commands, sorts and operators are used to build regular
  12     expressions and, thus, can contain character classes (e.g. "[0-9]+"), but
  13     also need to escape certain characters (e.g. "\." or "\+").
  14     """
  15
  16     name = 'smtlib'
  17
  18     COMMANDS = [
  19         'assert', 'check-sat', 'check-sat-assuming', 'declare-const',
  20         'declare-datatype', 'declare-datatypes', 'declare-codatatypes',
  21         'declare-fun', 'declare-sort', 'define-fun', 'define-fun-rec',
  22         'define-funs-rec', 'define-sort', 'echo', 'exit', 'get-assertions',
  23         'get-assignment', 'get-info', 'get-model', 'get-option', 'get-proof',
  24         'get-unsat-assumptions', 'get-unsat-core', 'get-value', 'pop', 'push',
  25         'reset', 'reset-assertions', 'set-info', 'set-logic', 'set-option',
  26         # SyGuS v2
  27         'declare-var', 'constraint', 'inv-constraint', 'synth-fun',
  28         'check-synth', 'synth-inv', 'declare-pool',
  29     ]
  30     SORTS = [
  31         'Array', 'BitVec', 'Bool', 'FloatingPoint', 'Float[0-9]+', 'Int',
  32         'Real', 'RegLan', 'RoundingMode', 'Set', 'String', 'Tuple',
  33     ]
  34     OPERATORS = [
  35         # array
  36         'select', 'store',
  37         # bv
  38         'concat', 'extract', 'repeat', 'zero_extend', 'sign_extend',
  39         'rotate_left', 'rotate_right', 'bvnot', 'bvand', 'bvor', 'bvneg',
  40         'bvadd', 'bvmul', 'bvudiv', 'bvurem', 'bvshl', 'bvlshr', 'bvult',
  41         'bvnand', 'bvnor', 'bvxor', 'bvxnor', 'bvcomp', 'bvsub', 'bvsdiv',
  42         'bvsrem', 'bvsmod', 'bvashr', 'bvule', 'bvugt', 'bvuge', 'bvslt',
  43         'bvsle', 'bvsgt', 'bvsge',
  44         # core
  45         '=>', '=', 'true', 'false', 'not', 'and', 'or', 'xor', 'distinct',
  46         'ite',
  47         # datatypes
  48         'mkTuple', 'tupSel',
  49         # fp
  50         'RNE', 'RNA', 'RTP', 'RTN', 'RTZ', 'fp', 'NaN', 'fp\.abs', 'fp\.neg',
  51         'fp\.add', 'fp\.sub', 'fp\.mul', 'fp\.div', 'fp\.fma', 'fp\.sqrt',
  52         'fp\.rem', 'fp\.roundToIntegral', 'fp\.min', 'fp\.max', 'fp\.leq',
  53         'fp\.lt', 'fp\.geq', 'fp\.gt', 'fp\.eq', 'fp\.isNormal',
  54         'fp\.isSubnormal', 'fp\.isZero', 'fp\.isInfinite', 'fp\.isNaN',
  55         'fp\.isNegative', 'fp\.isPositive', 'to_fp', 'to_fp_unsigned',
  56         'fp\.to_ubv', 'fp\.to_sbv', 'fp\.to_real', '\+oo', '-oo', '\+zero',
  57         '-zero',
  58         # int / real
  59         '<', '>', '<=', '>=', '!=', '\+', '-', '\*', '/', 'div', 'mod', 'abs',
  60         'divisible', 'to_real', 'to_int', 'is_int',
  61         # separation logic
  62         'emp', 'pto', 'sep', 'wand', 'nil',
  63         # sets / relations
  64         'union', 'setminus', 'member', 'subset', 'emptyset', 'singleton',
  65         'card', 'insert', 'complement', 'univset', 'transpose', 'tclosure',
  66         'join', 'product', 'intersection',
  67         # string
  68         'char', 'str\.\+\+', 'str\.len', 'str\.<', 'str\.to_re', 'str\.in_re',
  69         're\.none', 're\.all', 're\.allchar', 're\.\+\+', 're\.union',
  70         're\.inter', 're\.*', 'str\.<=', 'str\.at', 'str\.substr',
  71         'str\.prefixof', 'str\.suffixof', 'str\.contains', 'str\.indexof',
  72         'str\.replace', 'str\.replace_all', 'str\.replace_re',
  73         'str\.replace_re_all', 're\.comp', 're\.diff', 're\.\+', 're\.opt',
  74         're\.range', 're\.^', 're\.loop', 'str\.is_digit', 'str\.to_code',
  75         'str\.from_code', 'str\.to_int', 'str\.from_int',
  76     ]
  77
  78     tokens = {
  79         'root': [
  80             # comment (see lexicon)
  81             (r';.*$', token.Comment),
  82             # whitespace
  83             (r'\s+', token.Text),
  84             # numeral (decimal, hexadecimal, binary, see lexicon)
  85             (r'[0-9]+', token.Number),
  86             (r'#x[0-9a-fA-F]+', token.Number),
  87             (r'#b[01]+', token.Number),
  88             # bv constant (see BV theory specification)
  89             (r'bv[0-9]+', token.Number),
  90             # string constant (including escaped "", see lexicon)
  91             (r'".*?"', token.String),
  92             # reserved words (non-word and regular, see lexicon)
  93             (r'[!_](?=\s)', token.Name.Attribute),
  94             ('(as|let|exists|forall|match|per)\\b', token.Keyword),
  95             # Keywords (:foo, see lexicon)
  96             (r':[a-zA-Z~!@$%^&*_+=<>.?/-][a-zA-Z0-9~!@$%^&*_+=<>.?/-]*',
  97              token.Name.Attribute),
  98             # parentheses
  99             (r'\(', token.Text),
 100             (r'\)', token.Text),
 101             # commands (terminated by whitespace or ")")
 102             ('(' + '|'.join(COMMANDS) + ')(?=(\s|\)))', token.Keyword),
 103             # sorts (terminated by whitespace or ")")
 104             ('(' + '|'.join(SORTS) + ')(?=(\s|\)))', token.Name.Attribute),
 105             # operators (terminated by whitespace or ")")
 106             ('(' + '|'.join(OPERATORS) + ')(?=(\s|\)))', token.Operator),
 107             # symbols (regular and quoted, see lexicon)
 108             (r'[a-zA-Z~!@$%^&*_+=<>.?/-][a-zA-Z0-9~!@$%^&*_+=<>.?/-]*', token.Name),
 109             (r'\|[^|\\]*\|', token.Name),
 110         ],
 111     }