Code Monkey home page Code Monkey logo

vim-smt2's Introduction

Extended SMT-LIB2 support for VIM

Example

What is this?

A VIM plugin that adds syntax highlighting for the SMT-LIB2 format, i.e. *.smt2 files.

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 supports the extensions used by the Z3 SMT solver.

Note: Unlike other SMT-LIB2 syntax highlighters for VIM, this one is derived directly from the source of Z3's online demo.

The plugin also provides shortcuts for evaluating the current file, using a SMT solver of your choice (defaults to Z3 or boolector):

  • <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 and don't need shortcuts for calling a solver, you're done.

Otherwise, 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.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.