stp.NotAValue¶

class stp.NotAValue(message='', **fields)¶: NOT_A_VALUE: a reader was applied to a term that is not a value.

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