Simple Theorem Prover.
C C++ SMT CMake Yacc Python Other
Failed to load latest commit information.
bindings Making some asserts look better Jun 27, 2016
cmake Adding copyright information for cmake_uninstall Sep 22, 2015
examples/simple
include/stp Get extra tools working again. Jul 22, 2016
lib Get propagate with assumptions working better. Jul 25, 2016
papers
scripts
tests Remove old flags. Jul 21, 2016
tools Get development utility building again. Jul 25, 2016
utils Adding copyright to coverty_model.c Sep 30, 2015
windows/winports Fixing some copyright headers Nov 8, 2014
.clang-format Clang-format the code base. STP's code was a big mess of diferent Nov 10, 2014
.gitignore Added .gitignore file to ignore python .pyc files and Vim swap files. Mar 14, 2014
.gitmodules Include our own copy of GTest as a git submodule. The rationale for Mar 14, 2014
.travis.yml Cleaning up some builds for TravisCI May 19, 2016
AUTHORS Thanking Steve Poland for the STP organization name Mar 2, 2015
CMakeLists.txt Adding policy checks to fix debug messages during cmake Jul 17, 2016
INSTALL.md Fix documentation Jul 18, 2016
LICENSE Moving COPYRIGHT into LICENSE file Sep 18, 2015
LICENSE_COMPONENTS Cleaning up the LICENSE_COMPONENTS file Sep 10, 2015
README.markdown Fixing typo in README.md Sep 14, 2015
STPConfig.cmake.in Provide STPConfigVersion file which allows clients to request a Apr 24, 2015
STPConfigVersion.cmake.in Provide STPConfigVersion file which allows clients to request a Apr 23, 2015

README.markdown

STP

STP is a constraint solver (or SMT solver) aimed at solving constraints of bitvectors and arrays. These types of constraints can be generated by program analysis tools, theorem provers, automated bug finders, cryptographic attack tools, intelligent fuzzers, model checkers, and by many other applications.

Homepage: http://stp.github.io/

Ubuntu PPA: https://launchpad.net/~simple-theorem-prover/+archive/ubuntu/ppa/+packages

Documentation: https://github.com/stp/stp/wiki

Build Status

Coverity Scan Build Status

Coverage Status

Build, install and test:

See the INSTALL file

Input format

The file based input formats that STP reads are the: CVC, SMT-LIB1, and SMT-LIB2 formats. The SMT-LIB2 format is the recommended file format, because it is parsed by all modern bitvector solvers. Only quantifier-free bitvectors and arrays are implemented from the SMTLibv2 format.

Usage

Fun use case, STP overflowing a 32b integer:

import stp
In [1]: import stp
In [2]: a = stp.Solver()
In [3]: x = a.bitvec('x')
In [4]: y = a.bitvec('y')
In [5]: a.add(x + y < 20)
In [6]: a.add(x  > 10)
In [7]: a.add(y  > 10)
In [8]: a.check()
Out[8]: True
In [9]: a.model()
Out[9]: {'x': 4294967287L, 'y': 11L}

Traditional use-case:

stp myproblem.smt

Architecture

The system performs word-level preprocessing followed by translation to SAT which is then solved by a SAT solver. In particular, we introduce several new heuristics for the preprocessing step, including abstraction-refinement in the context of arrays, a new bitvector linear arithmetic equation solver, and some interesting simplifications. These heuristics help us achieve several magnitudes of order performance over other tools, and also over straight-forward translation to SAT. STP has been heavily tested on thousands of examples sourced from various real-world applications such as program analysis and bug-finding tools like EXE, and equivalence checking tools and theorem-provers.

Authors

  • Vijay Ganesh
  • Trevor Hansen