stp.Solver

class stp.Solver(tm=None, options=None, *, ctx=None, **option_kwargs)

One solver over a term manager; any number may be live over one manager, each with its own assertion stack, options and models. with s: is push/pop (z3py). Lifetime is garbage collection; close() releases early. A check releases the GIL; interrupt() takes no lock and works from any thread; Ctrl-C reaches a check running on the main thread (KeyboardInterrupt, solver still usable).

property options

The live view: timing (the entry’s Settable window) is enforced.

set(*positional_pairs, **kwargs)

set_args(*argv)

help()

manager()

add(*fs)

append(*fs)

insert(*fs)

assertions()

push(n=1)

pop(n=1)

num_scopes()

__enter__()

__exit__(*exc)

reset_assertions()

reset()

check(*assumptions, timeout=None, conflicts=None)

check-sat(-assuming); timeout in milliseconds (z3py’s unit), overriding max-time for this call only; one iterable argument is accepted as in add().

entails(f, timeout=None, conflicts=None)

(validity, reason, message): validity 1 valid / 2 invalid / 3 unknown.

unsat_assumptions()

unsat_core()

SolverHandle.unsat_assumptions(self)

model()

candidate_model()

value(t)

reason_unknown()

last_result()

statistics()

set_terminator(fn)

from_string(text, format='smtlib2', mode='declare-and-assert')

Parse an SMT-LIB 2 script into this solver (declarations, assertions, push/pop, options). A ParseError leaves the solver unchanged. The mode is “declare-and-assert” (nothing is decided), “execute” (the input runs as the stp command line runs it: its commands answer, to the output sink), “parse-only” (read as the command line’s –parse-only reads it) or “single-query” (a script as data: declarations, definitions, assertions and one check-sat, which is not run, and nothing that changes the solver; any other command is a ParseError naming it and its line).

from_stream(stream, format='smtlib2', mode='execute')

Parse a readable stream as its data arrives (a binary stream’s read1, else a line at a time), as the stp command line reads its input; the modes are from_string’s.

from_file(path, format='auto')

to_smt2(with_check_sat=False)

sexpr()

to_string(format='smtlib2')

write_cnf(path_or_file)

Encode the assertions up to CNF without solving and write the DIMACS text. Returns how the CNF relates to them: “whole”, “partial” (a refinement still to come) or “over-approximation” (a bit-vector abstraction). Not a check: the last check’s result and model stay.

dimacs()

The DIMACS text as a str.

assert_(t)

check_sat(assumptions=None, timeout=None, conflicts=None)

(verdict, reason, message): verdict 1 sat / 2 unsat / 3 unknown. Releases the GIL. On the main thread Ctrl-C interrupts the check and raises KeyboardInterrupt.

clear_interrupt()

close()

Delete the solver now (idempotent); terms, sorts and models stay valid. From another thread while its manager is inside a check or a parse: the solver is interrupted and deleted once that returns, as the garbage collector would.

closed

declared_logic()

The logic the last successful parse named in set-logic, or “” (not the “logic” option).

get_bool(name)

get_duration_ms(name)

get_int64(name)

get_str(name)

get_uint64(name)

interrupt()

interrupt_pending()

is_set(name)

level()

options_copy()

parse(text, format)

parse_file(path, format)

parse_smt2(text, mode=None)

parse_source(source, format, mode)

Parse source (a str, bytes, or a readable stream) in any mode.

parse_term(text)

reset_all_options()

reset_option(name)

resolve_options()

resolved_str(name)

set_bool(name, value)

set_cnf_sink(fn)

set_diagnostic_sink(fn)

set_duration_ms(name, value)

set_fatal_error_handler(fn)

set_int64(name, value)

set_names(name, members)

set_output_sink(fn)

set_str(name, value)

set_uint64(name, value)

symbol(name)