prophesy.smt package¶

Interfaces and convenience functions¶

prophesy.smt.smt module¶

class Answer(value)¶

Bases: enum.Enum

An enumeration.

killed = 3¶

memout = 4¶

sat = 0¶

timeout = 5¶

unknown = 2¶

unsat = 1¶

class SMTSolver¶

Bases: object

abstract add_variable()¶

abstract assert_constraint(c, name)¶

abstract assert_guarded_constraint(g, c, name)¶

abstract check()¶

abstract fix_guards(guard, value)¶

abstract from_file(p)¶

abstract name()¶

abstract pop()¶

abstract push()¶

abstract set_guard(g, v)¶

abstract to_file(p)¶

abstract version()¶

class VariableDomain(value)¶

Bases: enum.Enum

An enumeration.

Bool = 0¶

Int = 2¶

Real = 1¶

prophesy.smt.smtlib module¶

class SmtlibSolver(location, memout, timeout, incremental=True)¶

Bases: prophesy.smt.smt.SMTSolver

Abstract class for smt-lib based command line interfaces for SMT solvers.

add_variable(symbol, domain=<VariableDomain.Real: 1>)¶

Declare variable as a constant function with given domain.

symbol must be a string, not a Variable object or similar.

assert_constraint(constraint, name=None)¶

assert_guarded_constraint(guard, constraint, name=None)¶

check()¶

fix_guard(guard, value)¶

from_file(path)¶

get_model()¶

name()¶

pop()¶

print_calls()¶

push()¶

run()¶

set_guard(guard, value)¶

stop(store_exit=True)¶

to_file(path)¶

version()¶

parse_smt_command(command)¶: Breaks the given SMT command “(CMD ARG ARG ARG)” into tuple (CMD, [ARG]), where ARG again can be a (non-parsed) command

parse_smt_expr(expr)¶: Calculates given SMT expression “(OP ARG ARG)” as ARG OP ARG. Expression may be of arbitrary arity

Solver bindings¶

prophesy.smt.Z3cli_solver module¶

class Z3CliSolver(location=None, memout=None, timeout=None)¶

Bases: prophesy.smt.smtlib.SmtlibSolver

TODO: support the soft timeout kill.

name()¶

prophesy.smt.YicesCli_solver module¶

class YicesCLISolver(location=None, memout=None, timeout=None)¶