Skip to content
master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
 
 
 
 
 
 

Extended SMT-LIB2 support for VIM

Example

What is this?

A VIM plugin that provides syntax highlighting and common operations for working with SMT-LIB2 files (*.smt2).

Although SMT-LIB2 is the standard language supported by most SMT solvers, some of them introduce custom language extensions. Such extensions may range from syntactical sugar to fine-grained control over the underlying solver-procedure. Besides the base SMT-LIB2 language, this plugin also supports the extensions of Z3.

Note: To provide a familiar experience, the syntax highlighting is directly derived from the source of Z3's online demo.

Without an SMT solver being installed, both the highlighting and the following shortcuts will be available:

  • <localleader>f auto-formats the current paragraph (uses vim9script and requires VIM >= v8.2.2725)
  • <localleader>F auto-formats the current buffer/file (uses vim9script and requires VIM >= v8.2.2725)

With an SMT solver of your choice being installed (defaults to Z3 or boolector), the following shortcuts will also be available:

  • <localleader>r evaluates the current file (in a terminal)
  • <localleader>R evaluates the current file and puts the output in a new split with syntax highlighting
  • <localleader>v prints the solver's version (handy if you switch often)

Note: Unless you've set <localleader> to a custom key, it is \ (VIM default).

Here you can see it in action: asciicast

Installation

Plugin Manager Instructions
Pathogen
  1. cd ~/.vim/bundle
  2. git clone https://github.com/bohlender/vim-smt2
Vundle
  1. add Plugin 'bohlender/vim-smt2' to your ~/.vimrc file (before call vundle#end())
  2. reload your ~/.vimrc or restart VIM
  3. run :PluginInstall in VIM
manual (discouraged) Extract the archive or clone the repository into a directory in your runtimepath (e.g. ~/.vim/):
  1. cd ~/.vim/
  2. curl -L https://github.com/bohlender/vim-smt2/tarball/master | tar xz --strip 1

Configuration

If you only care about the syntax highlighting or auto-formatting, i.e. you don't need to invoke a solver, you're done. However, you can tweak the auto-formatting as follows:

  • let g:smt2_formatter_short_length = 80 defines the length of "short" S-expressions -- these are formatted without line breaks
  • let g:smt2_formatter_indent_str = " " defines two spaces as the string to use for indentation

To use the solver-oriented commands, you need to:

  • have z3 or boolector in your $PATH, or
  • set g:smt2_solver_command in your ~/.vimrc to the command for calling the solver of your choice (e.g. let g:smt2_solver_command="boolector -m") and also
  • set g:smt2_solver_version_switch to the solver's command line switch for printing it's version (default: --version).

FAQ

Why does VIM not show any syntax highlighting - neither for *.smt2 files nor for others?

Most likely syntax highlighting is simply disabled. You can enable syntax highlighting by typing :syntax on in VIM or adding syntax on to your ~/.vimrc file.

Why does the ending of a file, e.g. *.smt2, not affect the plugins loaded by VIM?

Make sure that you have filetype plugins enabled. See |filetype-plugin-on| for details, or simply add the following to your ~/.vimrc:

filetype plugin on

What do you use to get the look shown on the screenshot?

The screenshot was made with the VIM colorscheme monokai and the airline standard theme dark.

Contribute

You can always create an issue if you find bugs or think that something could be improved. If you want to tackle an issue or contribute to the plugin feel free to create a pull request.

About

A VIM plugin that adds support for the SMT-LIB2 format (including Z3's extensions)

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published