The 3.x API (C++, C and Python)¶

STP 3.x replaces the vc_* interface of c_interface.h with one API designed together for three languages: <stp/stp.hpp> for C++17, <stp/stp.h> for C, and the stp Python package (a Cython module under a z3py-style shell). The three surfaces share one object model and one option registry, so a program reads the same way in each. libstp carries this API alone, and STP’s own command line, bindings and tests are written against it. The 2.x interface survives as libstp2, a separate compatibility library implemented over the C API (see Compatibility with 2.x).

Objects¶

TermManager: Owns terms and sorts. Terms are hash-consed: building the same term twice gives the same node. Copies of a manager handle share one manager; it lives while anything that came from it lives. Three settings are fixed per manager: whether construction folds constants (simplify, default on), the default rounding mode used by floating-point operators, and the carrier width of declared sorts.
Sort / Term: Values, cheap to copy. A term knows its kind() (one of the 102 public kinds of kinds.toml), its sort(), its children() and indices() ((_ extract 7 0) has one child and two indices). A value term (kind() == VALUE) is decoded with typed readers: to_uint64, to_bv_string(16), to_bv_limbs, to_fp(), to_rm(), to_rational().
Solver: Assertions, push/pop, check_sat (optionally under assumptions and a per-check budget), entails, the Model of the last satisfiable check, interrupt() (safe from any thread), parsing of SMT-LIB 2 input, printing, statistics.
Model: A detached snapshot: it survives every later assertion, push or pop, and it evaluates any term of its manager, including terms built after the check. Symbols the solver never assigned are completed with their sort’s default; try_value refuses to complete instead. An array’s value is a term, the constant array of its default under a store per cell; a function has no value term, and function_value reads its interpretation.
Options: The whole option registry of the stp binary, settable by name with the text form the command line uses, or through typed setters. Every entry has a tier (stable, expert, experimental, diagnostic) and a settable window (anytime, before the first check, at construction); a write outside the window is a recoverable error, never silent. The binary registers its own command line from the same registry, so an option has one spelling and one meaning whether it arrives as --name or through Options::set, and the binary’s only additions are its frontend switches (input format, printing, --parse-only, --interactive). Three things differ on the command line, as stp --help shows: produce-models and lra-verify-canonical default to off there, a duration such as --max-time is a bare number of seconds, and --logic sets only the logic’s switches for the uninterpreted functions and extensional arrays.

Errors are exceptions in C++ and Python and a per-manager error record in C. Every precondition is checked in every build type; a recoverable error leaves every object as it was. The library never calls exit() or abort(): a script the frontend refuses (a sort error, a wrong arity, a constant that does not fit its width) is a PARSE error with the solver as it was, and an engine failure inside any call is INTERNAL and poisons the manager, after which every call on it, its solvers, models and terms is refused with STATE naming the failure.

Names supplied to declare, declare_sort and bind_symbol, and prefixes supplied to mk_fresh and mk_fresh_sort, must be representable as SMT-LIB quoted symbols. Spaces, non-ASCII bytes (including UTF-8), tabs, newlines and carriage returns are allowed. NUL, |, backslash, DEL and other ASCII control characters are rejected, as are names or prefixes beginning with @ or . (reserved for solver use). Names must be nonempty; fresh-name prefixes may be empty. A rejected name gives INVALID_ARGUMENT before any declaration or binding is recorded. Python raises ArgumentError, except for its existing NUL check, which raises ValueError. C strings end at their first NUL; C++ counted strings are checked in full. Theory-predefined names such as true and bvadd cannot be declared or bound, and predefined sort names such as Bool cannot be declared, because quoting does not distinguish them.

SMT-LIB define-fun names surviving a successful parse belong to the manager too. Later scripts, parse_term and other solvers of that manager can use them. symbol(name) returns the body of a nullary definition, or a callable function term for a parameterized definition. Applying that term expands the body with the supplied arguments. symbols() includes parameterized definitions; nullary bodies are expressions, not additional declared symbols. bind_symbol can give a function another name.

Definitions popped or reset within their original script are not retained; after adoption they survive API pops and resets, like declarations. A failed parse commits no new definitions. A retained definition cannot be redefined or replaced by a declaration; use a fresh manager for a new namespace. Solver::to_smt2 includes the definitions and their dependencies.

Model::function_value evaluates a defined function’s body in the saved snapshot, including its free symbols and calls to uninterpreted functions. FunctionValue::is_tabular() distinguishes an uninterpreted function’s finite table from a definition’s symbolic body. For the latter, apply evaluates the body; size, entry, entries and else_value report UNSUPPORTED. as_ite_term substitutes the snapshot’s values for free symbols and function interpretations, leaving the supplied arguments open; the result may be a general expression. It reports UNSUPPORTED for parameter-dependent partial FP operations (fp.min, fp.max, fp.to_ubv and fp.to_sbv), which apply can still evaluate.

Python exposes these as is_defined_function(), is_tabular(), callable FuncInterp objects and as_ite. Pickling or translating a defined function handle reports UNSUPPORTED rather than discarding its body; expanded applications support those operations, and a solver’s SMT-LIB export preserves definitions across managers.

C++¶

#include <stp/stp.hpp>
using namespace stp;

TermManager tm;
Sort bv32 = tm.mk_bv_sort(32);
Term x = tm.declare("x", bv32), y = tm.declare("y", bv32);

Solver s(tm);
s.add(x * 3 == 7);                 // literals take the term's sort and must fit
s.add(bvult(y, 10));               // no <,> on terms: signedness is explicit
if (s.check_sat().is_sat())
{
  Model m = s.model();
  std::cout << m.uint64_value(x) << "\n";   // 2863311533
  std::cout << m.value(x * 3) << "\n";      // #x00000007
}

Arrays, floating point, uninterpreted functions and Reals use the same shapes:

Sort arr = tm.mk_array_sort(bv32, tm.mk_bv_sort(8));
Term a = tm.declare("a", arr), i = tm.declare("i", bv32);
s.add(a[i] == 42);                 // select; store(a, i, v) for the update
s.add(a == store(tm.declare("b", arr), i, tm.mk_bv(8, 42)));  // extensional
s.add(a != tm.mk_const_array(arr, tm.mk_bv(8, 0)));          // ((as const ...) #x00)

Sort f32 = tm.mk_fp32_sort();
Term fx = tm.declare("fx", f32);
s.add(fp_add(RoundingMode::RNE, fx, 1.0) == tm.mk_fp(f32, RoundingMode::RNE, 3.0));

Term f = tm.declare("f", tm.mk_fun_sort({bv32}, bv32));
s.add(f(x) == f(y));

Term r = tm.declare("r", tm.mk_real_sort());
s.add(real_lt(r + 1, tm.mk_real("3/2")));

if (s.check_sat().is_sat())
{
  Model m = s.model();
  FloatValue v = m.fp_value(fx);           // sign, exponent, significand, class
  FunctionValue fv = m.function_value(f);  // entries and a default
  RationalValue q = m.real_value(r);       // numerator and denominator
}

Options are set at construction or on the live solver:

Options o;
o.set("max-time", "2s");           // the text form: a duration needs its unit here
o.set_str("sat-backend", "cadical");
o.set_args({"--fp-abstraction", "--bb.div-v3=false"});
Solver s(tm, o);
s.options().set_bool("check-sanity", true);   // anytime
Result r = s.check_sat({assumption}, CheckBudget{std::chrono::milliseconds(500), std::nullopt});
if (r.is_unknown()) std::cout << r.reason_message();

A duration option’s none (no limit; max-time’s default) is -1ms to get_duration and set_duration, and STP_DURATION_NONE to the C *_duration_ms functions, so a value read back can be written back.

C¶

The C header mirrors the C++ one function for function. Handles are retained engine nodes: every returned term carries a reference that stp_term_release gives back, or that a scope (stp_tm_scope_push / stp_tm_scope_pop) releases in bulk. A failing call returns NULL or STP_ERROR and records the first error since stp_tm_clear_error in the manager (stp_tm_error); a NULL term argument propagates without a record so a chain of constructions can be checked once.

#include <stp/stp.h>

stp_tm tm = stp_tm_new(NULL);
stp_sort bv32 = stp_mk_bv_sort(tm, 32);
stp_term x = stp_declare(tm, "x", bv32);
stp_term c = stp_eq(tm, stp_bvmul(tm, x, stp_mk_bv_uint64(tm, 32, 3)),
                    stp_mk_bv_uint64(tm, 32, 7));
stp_solver s = stp_solver_new(tm, NULL);
stp_solver_assert(s, c);
stp_result r;
if (stp_solver_check_sat(s, &r) == STP_OK && r.kind == STP_SAT)
{
  stp_model m = stp_solver_model(s);
  uint64_t v;
  stp_model_uint64(m, x, &v);
  stp_model_release(m);
}
if (stp_tm_error(tm))
  fprintf(stderr, "%s\n", stp_tm_error(tm)->message);
stp_solver_delete(s);
stp_tm_release_all(tm);
stp_tm_release(tm);

Python¶

The Python package is the z3py idiom over the same objects:

from stp import *

x, y = BitVecs('x y', 32)
s = Solver()
s.add(x * 3 == 7, ULT(y, 10))
if s.check() == sat:
    m = s.model()
    print(m[x].as_long(), m.eval(x * 3))

a = Array('a', BitVecSort(32), BitVecSort(8))
s.add(a[y] == 42)
f = FP('f', Float32())
s.add(fpAdd(RNE(), f, 1.0) == 3.0)

The package’s own rules, documented in it: == builds a term on every sort (fpEQ is IEEE equality); bool(term) raises unless the term is a ground Boolean value, so x in [y, x], list.index and list.remove over terms raise too; bit-vector < and >> are signed and arithmetic (ULT, LShR and the rest are the unsigned and logical forms), and / on bit-vectors raises (use UDiv/SDiv), except inside the @stp decorator, which keeps STP 2.x’s unsigned meanings; literals are strict (BitVecVal(256, 8) raises; wrap=True wraps); Model.eval completes by default (model_completion=False leaves a symbol the model does not fix in place); as_decimal(k) always gives k digits (Q(1, 2).as_decimal(3) is "0.500"); and fpToFP takes a rounding mode first, the bits of a bit-vector read as a float being fpBVToFP. Options are keyword arguments with - and . spelled _: Solver(max_time='2s', bb_div_v3=False).

The package installs with STP when it is built with ENABLE_PYTHON_API (the default when the interpreter can import Cython), or on its own, once per interpreter, against an STP that is already installed: python3 -m pip install ./bindings/python compiles its extension there. bindings/python/README.md says how that finds the installation.

Running an input as `stp` does¶

Solver::parse and parse_smt2 take a ParseMode. DECLARE_AND_ASSERT, the default, adds an input’s declarations and assertions to the solver and decides nothing: the solver’s own check_sat answers its question. EXECUTE runs the input as the stp binary does: a script’s commands answer as they are read. PARSE_ONLY reads it as --parse-only does. An input can also come from a std::istream, read as its data arrives, so a script driven over a pipe is answered command by command (in C a stp_text_source callback, in Python Solver.from_stream).

SINGLE_QUERY (C STP_PARSE_SINGLE_QUERY, Python "single-query") reads a script as data: it applies declarations, definitions and assertions as DECLARE_AND_ASSERT does, and nothing in the script may change the solver’s configuration or state. The script must be one query: set-logic at most once, before any declaration or assertion; set-info, ignored; set-option for :print-success and :produce-models only, ignored too (the output channels would open files, and every other option is the caller’s to set); declare-const, declare-fun, declare-sort, define-fun, define-sort, define-const and assert; exactly one check-sat, which is recorded and not run; after it, only exit, any number of times. Anything else – push, pop, either reset, check-sat-assuming, a get- request, echo, a second check-sat, a declaration after the check-sat – or a script without a check-sat is a PARSE error that names the command and its line. The caller then decides the query with its own check_sat, under its own options. Solver::declared_logic() (C stp_solver_declared_logic, Python declared_logic()) is the logic the last successful parse named in set-logic, empty when it named none; it is not the logic option.

A parse that fails part way, in any mode, leaves the solver as it was: its assertion stack, without the symbols the script declared, and its declared logic. A NUL byte in an input is INVALID_ARGUMENT: in a text before anything is read, in a stream when the reader reaches it, since the lexer would stop or end a token there.

A script’s reset or reset-assertions can discard its declarations, but the term manager retains declarations from the API and earlier parses, and existing handles remain valid. Reusing a retained name for a different symbol or sort is a recoverable PARSE error; the solver’s assertion stack is restored. An ordinary symbol redeclared at the same sort keeps its identity. A declare-sort always introduces a new sort identity, so it cannot reuse a retained sort name even after reset. Use the existing sort without redeclaring it in a subsequent parse, or use a fresh term manager and solver when a script needs a new namespace. Declarations created and discarded within one script still follow SMT-LIB scope and reset rules.

Named assertion cores are available through SMT-LIB get-unsat-core in EXECUTE mode; see SMT-LIB 2.7 compatibility. Assertion labels survive separate parse calls on the same solver and follow both scripted and native push, pop and reset operations. The native unsat_assumptions() API continues to report assumption terms.

STP writes nothing to the process’s streams. The answers, and what the printing options print, go to the solver’s output sink, where an empty chunk asks for a flush; statistics, warnings and a fatal error’s report go to its diagnostic sink; without a sink the text is dropped. The one exception is a SAT backend’s own report, which print-functionstat switches on: CaDiCaL and MiniSat print theirs to standard output themselves (CryptoMiniSat’s reaches the output sink). Two more hooks complete what a command line needs: the CNF sink receives every CNF a check hands to the SAT solver, with whether it is the whole query, partial (array read refinement adds its axioms as the search asks for them) or an over-approximation (the bit-vector abstractions); and the fatal error handler hears of an engine fatal error before anything unwinds, and may end the process. The option end-after-cnf ends a run at its first CNF, as --exit-after-CNF does. tools/stp/run.cpp, the binary’s own use of these calls, is a complete example.

s = Solver()
s.set_output_sink(sys.stdout.write)
s.from_string("(declare-fun x () (_ BitVec 8))\n(assert (distinct x x))\n(check-sat)\n",
              mode="execute")   # unsat

Compatibility with 2.x¶

libstp2 implements c_interface.h over stp.h, and is the only library that provides it: KLEE and other 2.x clients link it unchanged (-lstp2 instead of -lstp; with CMake, the target stp2, which the package’s STP_C_INTERFACE_LIBRARY, STP_SHARED_LIBRARY and STP_STATIC_LIBRARY variables name). The header-only fp.hpp and uf.hpp over c_interface.h come with it. It reproduces the 2.x ownership modes, the error handler and the model-lifetime rules, with four documented exceptions: reading a counterexample after a VALID answer returns NULL with a diagnostic instead of an invented value, an unmatched vc_pop is an error instead of deleting the base assertions, a Real constant or term beyond the exact-arithmetic budget is a fatal refusal, as any constructor’s is, where 2.x returned NULL, and a parsed text that declares a name the checker already has at another type is refused, where 2.x made a second symbol of that name. lib/Compat2/NOTES.md records how each 2.x function, option letter and ifaceflag_t ordinal maps onto the 3.x API.

Limits of the alpha¶

CryptoMiniSat is interrupted between its solver calls only, and so is MiniSat when the MiniSat it was built with lacks the terminator hook of stp/minisat (capabilities() says which, under interrupt.minisat).
The model’s evaluator, simplify, substitute and str() take a term of any depth. The engine’s printers – to_string with let-sharing, the DOT and GDL forms, and Solver::to_smt2 and to_string – recurse once per level of a term, as 2.x’s did, and a term some ten thousand levels deep can overflow the stack there.
fp.to_real takes formats whose exponent has at most 16 bits (the exact arithmetic’s number limits), and a Real converts to a float only when it and the rounding mode are both values. Relating two conversions costs about four times more per exponent bit: well under a second at binary64, a minute or more at binary128; at 16 bits it can exceed the number limits, and the check then answers unknown (INCOMPLETE). Whether it does depends on the models the SAT backend proposes – a NaN or an infinity converts to a Real constant of its own, and a model that uses one need not relate the two at all – and so does whether a check over a single conversion exceeds them.
The float literal constructors (mk_fp from a double or from text) and SMT-LIB real-literal conversions need an exponent field of at least 3 bits. Wider fields, including those larger than a machine word, accept ordinary values with the requested rounding mode. For fields wider than LibBF supports directly (29 bits with 32-bit limbs, 61 with 64-bit limbs), a nonzero result’s unbiased exponent must fit its working normal range: 2 - 2^28 through 2^28 - 1 with 32-bit limbs, or 2 - 2^60 through 2^60 - 1 with 64-bit limbs. Magnitudes outside that range are refused; they are not rounded to the narrower working format’s zero, infinity or largest finite value. mk_fp_from_bits builds a value of any format without these conversion limits.
Arrays support Booleans, bit-vectors, floats, rounding modes and values of declared sorts as indices and elements. Real and nested array components remain unsupported.
unsat_assumptions after a batch check reports every assumption; the failed subset comes from a check the incremental driver ran.
stop-after-cnf stops the batch pipeline only: once pushes have made the session incremental, a check the incremental driver runs is answered.
Under simplify = false a few kinds still come back lowered, having no engine node of their own: BV_NAND, BV_NOR and BV_XNOR as BV_NOT over the operation, BV_REPEAT and the rotations as concatenations, BV_COMP, BV_REDAND and BV_REDOR as an ITE over an equality, and DISTINCT over floats, Reals or arrays as the negation of an equality or a conjunction of them, among others.
A script run with ParseMode::EXECUTE answers its (check-sat) inside the frontend, where the answer is printed; model() and unsat_assumptions() do not see it. Scripted checks preserve the original assertion occurrences reported by assertions().
A value of a declared sort prints as S!k, which the parser does not read back.
A constant array’s default must be a value, a term with no symbol in it: mk_const_array over a variable, or over a term that contains one, is UNSUPPORTED, and so is a script’s ((as const S) v) (a PARSE error). An array of a declared sort’s values takes one a model gave.
A constant array indexed by a declared sort: a refutation that counts the sort’s elements by its carrier (two constant arrays with different defaults, one reaching the other through writes) is answered unknown (INCOMPLETE), since a model may give the sort just the elements the writes name.
A function over Reals is modelled from the applications the check saw; one it never saw completes to the codomain’s default. A Real argument with a bit-vector result under a comparison is refused at assertion.
A Real comparison belongs at the Boolean level: one that stays inside a bit-vector term – the condition of a bit-vector ite, bool_to_bv1 of it – is refused at assertion (UNSUPPORTED) unless simplification brings it up (bool_to_bv1(r == 1) == 1 is r == 1).
An option’s exclusions are checked when a solver is made, whenever both entries are set, whatever their values; set_args accepts --no-name for every Boolean option.

capabilities() reports the ones that depend on the build or the sort: interrupt.cryptominisat, interrupt.minisat (in a build with MiniSat), array.element-sorts and kind.FP_TO_FP_FROM_REAL.

Several solvers, several threads¶

Any number of solvers may be live over one manager, each with its own assertion stack, options, models and statistics; switching between them replays the assertion stack, which is the one cost. A manager and everything created from it may be used from any thread, one call at a time: the caller serialises, and interrupt() is the one call that may overlap a running check.

Independent managers run concurrently, with one exception: the parsers keep process-wide state, so every parse takes one lock for its whole length. A check that an EXECUTE input runs, and a wait on the stream or text source a parse reads, hold it too, and a parse on another manager waits for them.

A callback – an output, diagnostic or CNF sink, the terminator, the fatal-error handler, the stream a parse reads, C’s error callback – runs in the middle of a call, and must not call the library: every call from one is refused with STATE, but interrupt(), clear_interrupt() and interrupt_pending().