mirror of
https://github.com/sheerun/vim-polyglot.git
synced 2025-11-17 07:53:40 -05:00
179
syntax/smt2.vim
Normal file
179
syntax/smt2.vim
Normal file
@@ -0,0 +1,179 @@
|
||||
if exists('g:polyglot_disabled') && index(g:polyglot_disabled, 'smt2') != -1
|
||||
finish
|
||||
endif
|
||||
|
||||
" Vim syntax file
|
||||
" " Language: SMT-LIB2 with Z3's extensions
|
||||
" " Maintainer: Dimitri Bohlender <bohlender@embedded.rwth-aachen.de>
|
||||
|
||||
" Quit if a syntax file is already loaded
|
||||
if exists("b:current_syntax")
|
||||
finish
|
||||
endif
|
||||
let b:current_syntax = "smt2"
|
||||
|
||||
" Comments
|
||||
syntax match smt2Comment ";.*$"
|
||||
|
||||
" Keywords
|
||||
syntax keyword smt2Keyword
|
||||
\ apply
|
||||
\ as
|
||||
\ assert
|
||||
\ assert
|
||||
\ assert-soft
|
||||
\ check-sat
|
||||
\ check-sat-using
|
||||
\ declare-const
|
||||
\ declare-datatype
|
||||
\ declare-datatypes
|
||||
\ declare-fun
|
||||
\ declare-map
|
||||
\ declare-rel
|
||||
\ declare-sort
|
||||
\ declare-var
|
||||
\ define-const
|
||||
\ define-fun
|
||||
\ define-sort
|
||||
\ display
|
||||
\ echo
|
||||
\ elim-quantifiers
|
||||
\ eval
|
||||
\ exists
|
||||
\ exit
|
||||
\ forall
|
||||
\ get-assignment
|
||||
\ get-info
|
||||
\ get-model
|
||||
\ get-option
|
||||
\ get-proof
|
||||
\ get-unsat-core
|
||||
\ get-user-tactics
|
||||
\ get-value
|
||||
\ help
|
||||
\ let
|
||||
\ match
|
||||
\ maximize
|
||||
\ minimize
|
||||
\ pop
|
||||
\ push
|
||||
\ query
|
||||
\ reset
|
||||
\ rule
|
||||
\ set-info
|
||||
\ set-logic
|
||||
\ set-option
|
||||
\ simplify
|
||||
syntax match smt2Keyword "!"
|
||||
|
||||
" Operators
|
||||
syntax match smt2Operator "[=\|>\|<\|<=\|>=\|=>\|+\|\-\|*\|/]"
|
||||
|
||||
" Builtins
|
||||
syntax keyword smt2Builtin
|
||||
\ and
|
||||
\ bit0
|
||||
\ bit1
|
||||
\ bvadd
|
||||
\ bvand
|
||||
\ bvashr
|
||||
\ bvcomp
|
||||
\ bvlshr
|
||||
\ bvmul
|
||||
\ bvnand
|
||||
\ bvneg
|
||||
\ bvnor
|
||||
\ bvnot
|
||||
\ bvor
|
||||
\ bvredand
|
||||
\ bvredor
|
||||
\ bvsdiv
|
||||
\ bvsge
|
||||
\ bvsgt
|
||||
\ bvshl
|
||||
\ bvsle
|
||||
\ bvslt
|
||||
\ bvsmod
|
||||
\ bvsrem
|
||||
\ bvsub
|
||||
\ bvudiv
|
||||
\ bvuge
|
||||
\ bvugt
|
||||
\ bvule
|
||||
\ bvult
|
||||
\ bvurem
|
||||
\ bvxnor
|
||||
\ bvxor
|
||||
\ concat
|
||||
\ const
|
||||
\ distinct
|
||||
\ div
|
||||
\ extract
|
||||
\ false
|
||||
\ get-assertions
|
||||
\ if
|
||||
\ is_int
|
||||
\ ite
|
||||
\ map
|
||||
\ mod
|
||||
\ not
|
||||
\ or
|
||||
\ rem
|
||||
\ repeat
|
||||
\ root-obj
|
||||
\ rotate_left
|
||||
\ rotate_right
|
||||
\ sat
|
||||
\ sat
|
||||
\ select
|
||||
\ sign_extend
|
||||
\ store
|
||||
\ to_int
|
||||
\ to_real
|
||||
\ true
|
||||
\ unsat
|
||||
\ unsat
|
||||
\ xor
|
||||
\ zero_extend
|
||||
syntax match smt2Builtin "[\^\~]"
|
||||
|
||||
" Identifier
|
||||
syntax match smt2Identifier "\<[a-z_][a-zA-Z0-9_\-\.']*\>"
|
||||
|
||||
" Types
|
||||
syntax match smt2Type "\<[A-Z][a-zA-Z0-9_\-\.']*\>"
|
||||
|
||||
" Strings
|
||||
syntax region smt2String start=+"+ skip=+\\\\\|\\"+ end=+"+
|
||||
syntax match smt2Option "\<:[a-zA-Z0-9_\-\.']*\>"
|
||||
|
||||
" Constructors
|
||||
syntax match smt2Constructor "\<\$[a-zA-Z0-9_\-\.']*\>"
|
||||
|
||||
" Number
|
||||
syntax match smt2Int "\<[0-9]\+\>"
|
||||
syntax match smt2Hex "\<[0#][xX][0-9a-fA-F]\+\>"
|
||||
syntax match smt2Binary "\<#b[01]\+\>"
|
||||
syntax match smt2Float "\<[0-9]\+\.[0-9]\+\([eE][\-+]\=[0-9]\+\)\=\>"
|
||||
|
||||
" Delimiter
|
||||
syntax match smt2Delimiter "[()]"
|
||||
|
||||
" Error
|
||||
syntax keyword smt2Error error
|
||||
|
||||
highlight def link smt2Comment Comment
|
||||
highlight def link smt2Keyword Function
|
||||
highlight def link smt2Operator Operator
|
||||
highlight def link smt2Builtin Operator
|
||||
highlight def link smt2Identifier Normal
|
||||
highlight def link smt2Type Type
|
||||
highlight def link smt2String String
|
||||
highlight def link smt2Option PreProc
|
||||
highlight def link smt2Constructor Function
|
||||
highlight def link smt2Float Float
|
||||
highlight def link smt2Hex Number
|
||||
highlight def link smt2Binary Number
|
||||
highlight def link smt2Int Number
|
||||
highlight def link smt2Delimiter Delimiter
|
||||
highlight def link smt2Error Error
|
||||
Reference in New Issue
Block a user