blob: 39e7d47754bf970fe5f54fa06bddd6649236b698 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2/solver.vim')
finish
endif
" ------------------------------------------------------------------------------
" Config
" ------------------------------------------------------------------------------
" If no command for invoking a solver is specified in ~/.vimrc, test if either
" 'z3' or 'boolector' is accessible through $PATH (in that order)
if !exists("g:smt2_solver_command")
if executable("z3")
let g:smt2_solver_command = "z3"
elseif executable("boolector")
let g:smt2_solver_command = "boolector"
endif
endif
" If no command line switch for printing the solver's version is specified in
" ~/.vimrc, use '--version'
if !exists("g:smt2_solver_version_switch")
let g:smt2_solver_version_switch = "--version"
endif
" ------------------------------------------------------------------------------
" Public functions
" ------------------------------------------------------------------------------
" Invokes the solver on current file
function! smt2#solver#Run()
silent !clear
execute "!" . g:smt2_solver_command . " " . bufname("%")
endfunction
" Puts the solver's output in new split (replaces old split)
function! smt2#solver#RunAndShowResult()
let output = system(g:smt2_solver_command . " " . bufname("%") . " 2>&1")
" Create split (or reuse existent)
if exists("s:outputbufnr") && bufwinnr(s:outputbufnr) > 0
execute bufwinnr(s:outputbufnr) . 'wincmd w'
else
silent! vnew
let s:outputbufnr=bufnr('%')
endif
" Clear & (re-)fill contents
silent! normal! ggdG
setlocal filetype=smt2 buftype=nofile nobuflisted noswapfile
call append(0, split(output, '\v\n'))
normal! gg
endfunction
" Requests the solver's version
function! smt2#solver#PrintVersion()
silent !clear
execute "!" . g:smt2_solver_command . " " . g:smt2_solver_version_switch
endfunction
|
