Skip to content

rbonichon/smtpp

Repository files navigation

About

smtpp is a preprocessor for SMT-LIB 2.0 scripts with extensions for lambda-terms and polymorphic types in scripts.

Dependencies

For developers only:

  • headache for license header generation

Compilation

The usual incantation

% ./configure
% make
% make

should produce one of two binaries in src

  • smtpp.byt : a bytecode executable software
  • smtpp.opt : a native code executable

Developers

Generating a configuration script

Generate a configure using autoconf in the src directory. This uses the file configure.ac

% autoconf
% ./configure

Compiling from src

If you are working in the src directory, you might not want to recompile everything for every change, assuming you have not changed your development environment.

If there is no .depend file, do a touch .depend first. Otherwise:

  • If you have just changed a file and not added any, a simple make should suffice
  • If you have added a file, add it to the Makefile in the proper file list, and do a make depend && make.

Documentation

Options are detailed on stdout by executing smtpp.opt -help or smtpp.byt -help.

Code source documentation can be generated by typing make doc either at the root or in the src directory. This phase needs ocamldoc.

About

Preprocessors and analyzers for SMT-LIB

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages