stp.unsat¶

stp.unsat = unsat¶: sat, unsat or unknown, with the reason attached. Hashable; bool(r) raises TypeError: compare with sat/unsat/unknown.

STP

The Simple Theorem Prover

Overview

Building STP
Architecture

Running STP

The 3.x API (C++, C and Python)
API reference
- C++ API
- C API
- Python API
2.x C API handle lifetime
Array extensionality
Uninterpreted functions
Incremental solving
Bit-vector abstraction
Floating-point abstraction
Linear real arithmetic
SMT-LIB 2.7 compatibility

Source code layout
Testing
Developer tools
Making a release

Benchmarks

Source code on GitHub

©2018-2026, The STP Project. | Page source