Z3
Data Structures | Namespaces | Functions | Variables
doc/tmp/z3py.py File Reference

Go to the source code of this file.

Data Structures

class  Context
class  Z3PPObject
 ASTs base class. More...
class  AstRef
class  SortRef
class  FuncDeclRef
 Function Declarations. More...
class  ExprRef
 Expressions. More...
class  BoolSortRef
 Booleans. More...
class  BoolRef
class  PatternRef
 Patterns. More...
class  QuantifierRef
 Quantifiers. More...
class  ArithSortRef
 Arithmetic. More...
class  ArithRef
class  IntNumRef
class  RatNumRef
class  AlgebraicNumRef
class  BitVecSortRef
 Bit-Vectors. More...
class  BitVecRef
class  BitVecNumRef
class  ArraySortRef
 Arrays. More...
class  ArrayRef
class  Datatype
class  ScopedConstructor
class  ScopedConstructorList
class  DatatypeSortRef
class  DatatypeRef
class  ParamsRef
 Parameter Sets. More...
class  ParamDescrsRef
class  Goal
class  AstVector
class  AstMap
class  FuncEntry
class  FuncInterp
class  ModelRef
class  Statistics
 Statistics. More...
class  CheckSatResult
class  Solver
class  Fixedpoint
 Fixedpoint. More...
class  ApplyResult
class  Tactic
class  Probe

Namespaces

namespace  z3py

Functions

def enable_trace
def disable_trace
def get_version_string
def get_version
def open_log
def append_log
def to_symbol
def main_ctx
def set_param
def reset_params
def set_option
def get_param
def is_ast
def eq
def is_sort
def DeclareSort
def is_func_decl
def Function
def is_expr
def is_app
def is_const
def is_var
def get_var_index
def is_app_of
def If
def Distinct
def Const
def Consts
def Var
def RealVar
def RealVarVector
def is_bool
def is_true
def is_false
def is_and
def is_or
def is_not
def is_eq
def is_distinct
def BoolSort
def BoolVal
def Bool
def Bools
def BoolVector
def FreshBool
def Implies
def Xor
def Not
def And
def Or
def is_pattern
def MultiPattern
def is_quantifier
def ForAll
def Exists
def is_arith_sort
def is_arith
def is_int
def is_real
def is_int_value
def is_rational_value
def is_algebraic_value
def is_add
def is_mul
def is_sub
def is_div
def is_idiv
def is_mod
def is_le
def is_lt
def is_ge
def is_gt
def is_is_int
def is_to_real
def is_to_int
def IntSort
def RealSort
def IntVal
def RealVal
def RatVal
def Q
def Int
def Ints
def IntVector
def FreshInt
def Real
def Reals
def RealVector
def FreshReal
def ToReal
def ToInt
def IsInt
def Sqrt
def Cbrt
def is_bv_sort
def is_bv
def is_bv_value
def BV2Int
def BitVecSort
def BitVecVal
def BitVec
def BitVecs
def Concat
def Extract
def ULE
def ULT
def UGE
def UGT
def UDiv
def URem
def SRem
def LShR
def RotateLeft
def RotateRight
def SignExt
def ZeroExt
def RepeatBitVec
def is_array
def is_const_array
def is_K
def is_map
def get_map_func
def ArraySort
def Array
def Update
def Store
def Select
def Map
def K
def is_select
def is_store
def CreateDatatypes
def EnumSort
def args2params
def is_as_array
def get_as_array_func
def SolverFor
def SimpleSolver
def AndThen
def Then
def OrElse
def ParOr
def ParThen
def ParAndThen
def With
def Repeat
def TryFor
def tactics
def tactic_description
def describe_tactics
def is_probe
def probes
def probe_description
def describe_probes
def FailIf
def When
def Cond
def simplify
 Utils.
def help_simplify
def simplify_param_descrs
def substitute
def substitute_vars
def Sum
def Product
def solve
def solve_using
def prove
def parse_smt2_string
def parse_smt2_file
def Interpolant
def tree_interpolant
def binary_interpolant
def sequence_interpolant

Variables

tuple _error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
tuple _Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)
 _main_ctx = None
tuple sat = CheckSatResult(Z3_L_TRUE)
tuple unsat = CheckSatResult(Z3_L_FALSE)
tuple unknown = CheckSatResult(Z3_L_UNDEF)
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines