C C++ SMT Yacc CMake Objective-C Other
Latest commit 9f367bc Jun 13, 2017 @msoos msoos committed on GitHub Merge pull request #259 from fkutzner/win64cmake_pr2
Fixed Python binding tests on Windows
Permalink
Failed to load latest commit information.
bindings cleaned up a fixme comment Jun 12, 2017
cmake Fixing static compilation of tests May 1, 2017
examples/simple Trying to fix shared/static library building May 1, 2017
include/stp Removing unused code&variables, reducing scope May 29, 2017
lib Merge pull request #259 from fkutzner/win64cmake_pr2 Jun 13, 2017
papers No commit message Aug 14, 2009
scripts No need to build CMS's python interface. This will fix TravisCI Jun 13, 2017
tests removed the pre-check target Jun 9, 2017
tools Merge pull request #259 from fkutzner/win64cmake_pr2 Jun 13, 2017
utils Adding copyright to coverty_model.c Sep 30, 2015
windows refactored gettimeofday() for Win32 Apr 17, 2017
.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 Specify OS for Travis May 3, 2017
AUTHORS Thanking Steve Poland for the STP organization name Mar 2, 2015
CMakeLists.txt fixed output directory setup (thanks @delcypher) Jun 12, 2017
INSTALL.md Trying to fix shared/static library building May 1, 2017
LICENSE Moving COPYRIGHT into LICENSE file Sep 18, 2015
LICENSE_COMPONENTS Cleaning up the LICENSE_COMPONENTS file Sep 10, 2015
README.markdown Adding coverity badge May 29, 2017
STPConfig.cmake.in Trying to fix shared/static library building May 1, 2017
STPConfigVersion.cmake.in Provide STPConfigVersion file which allows clients to request a Apr 23, 2015
appveyor.yml disabled test execution on AppVeyor Jun 13, 2017

README.markdown

License: MIT Linux build Windows build Coverity Scan Build Status Codacy Badge Coverage

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

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