Z3
Data Structures | Namespaces | Functions | Variables
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
 
class  FPSortRef
 FP Sorts. More...
 
class  FPRMSortRef
 
class  FPRef
 FP Expressions. More...
 
class  FPRMRef
 
class  FPNumRef
 FP Numerals. More...
 

Namespaces

 z3py
 

Functions

def enable_trace (msg)
 
def disable_trace (msg)
 
def get_version_string ()
 
def get_version ()
 
def open_log (fname)
 
def append_log (s)
 
def to_symbol
 
def main_ctx ()
 
def set_param (args, kws)
 
def reset_params ()
 
def set_option (args, kws)
 
def get_param (name)
 
def is_ast (a)
 
def eq (a, b)
 
def is_sort (s)
 
def DeclareSort
 
def is_func_decl (a)
 
def Function (name, sig)
 
def is_expr (a)
 
def is_app (a)
 
def is_const (a)
 
def is_var (a)
 
def get_var_index (a)
 
def is_app_of (a, k)
 
def If
 
def Distinct (args)
 
def Const (name, sort)
 
def Consts (names, sort)
 
def Var (idx, s)
 
def RealVar
 
def RealVarVector
 
def is_bool (a)
 
def is_true (a)
 
def is_false (a)
 
def is_and (a)
 
def is_or (a)
 
def is_not (a)
 
def is_eq (a)
 
def is_distinct (a)
 
def BoolSort
 
def BoolVal
 
def Bool
 
def Bools
 
def BoolVector
 
def FreshBool
 
def Implies
 
def Xor
 
def Not
 
def And (args)
 
def Or (args)
 
def is_pattern (a)
 
def MultiPattern (args)
 
def is_quantifier (a)
 
def ForAll
 
def Exists
 
def is_arith_sort (s)
 
def is_arith (a)
 
def is_int (a)
 
def is_real (a)
 
def is_int_value (a)
 
def is_rational_value (a)
 
def is_algebraic_value (a)
 
def is_add (a)
 
def is_mul (a)
 
def is_sub (a)
 
def is_div (a)
 
def is_idiv (a)
 
def is_mod (a)
 
def is_le (a)
 
def is_lt (a)
 
def is_ge (a)
 
def is_gt (a)
 
def is_is_int (a)
 
def is_to_real (a)
 
def is_to_int (a)
 
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 (a)
 
def ToInt (a)
 
def IsInt (a)
 
def Sqrt
 
def Cbrt
 
def is_bv_sort (s)
 
def is_bv (a)
 
def is_bv_value (a)
 
def BV2Int (a)
 
def BitVecSort
 
def BitVecVal
 
def BitVec
 
def BitVecs
 
def Concat (args)
 
def Extract (high, low, a)
 
def ULE (a, b)
 
def ULT (a, b)
 
def UGE (a, b)
 
def UGT (a, b)
 
def UDiv (a, b)
 
def URem (a, b)
 
def SRem (a, b)
 
def LShR (a, b)
 
def RotateLeft (a, b)
 
def RotateRight (a, b)
 
def SignExt (n, a)
 
def ZeroExt (n, a)
 
def RepeatBitVec (n, a)
 
def BVRedAnd (a)
 
def BVRedOr (a)
 
def is_array (a)
 
def is_const_array (a)
 
def is_K (a)
 
def is_map (a)
 
def get_map_func (a)
 
def ArraySort (d, r)
 
def Array (name, dom, rng)
 
def Update (a, i, v)
 
def Store (a, i, v)
 
def Select (a, i)
 
def Map (f, args)
 
def K (dom, v)
 
def is_select (a)
 
def is_store (a)
 
def CreateDatatypes (ds)
 
def EnumSort
 
def args2params
 
def is_as_array (n)
 
def get_as_array_func (n)
 
def SolverFor
 
def SimpleSolver
 
def AndThen (ts, ks)
 
def Then (ts, ks)
 
def OrElse (ts, ks)
 
def ParOr (ts, ks)
 
def ParThen
 
def ParAndThen
 
def With (t, args, keys)
 
def Repeat
 
def TryFor
 
def tactics
 
def tactic_description
 
def describe_tactics ()
 
def is_probe (p)
 
def probes
 
def probe_description
 
def describe_probes ()
 
def FailIf
 
def When
 
def Cond
 
def simplify (a, arguments, keywords)
 Utils. More...
 
def help_simplify ()
 
def simplify_param_descrs ()
 
def substitute (t, m)
 
def substitute_vars (t, m)
 
def Sum (args)
 
def Product (args)
 
def solve (args, keywords)
 
def solve_using (s, args, keywords)
 
def prove (claim, keywords)
 
def parse_smt2_string
 
def parse_smt2_file
 
def Interpolant
 
def tree_interpolant
 
def binary_interpolant
 
def sequence_interpolant
 
def get_default_rounding_mode
 
def set_default_rounding_mode
 
def get_default_fp_sort
 
def set_default_fp_sort
 
def Float16
 
def FloatHalf
 
def Float32
 
def FloatSingle
 
def Float64
 
def Float128
 
def is_fp_sort (s)
 
def is_fprm_sort (s)
 
def RoundNearestTiesToEven
 
def RNE
 
def RoundNearestTiesToAway
 
def RNA
 
def RoundTowardPositive
 
def RTP
 
def RoundTowardNegative
 
def RTN
 
def RoundTowardZero
 
def RTZ
 
def is_fprm (a)
 
def is_fprm_value (a)
 
def is_fp (a)
 
def is_fp_value (a)
 
def FPSort
 
def fpNaN (s)
 
def fpPlusInfinity (s)
 
def fpMinusInfinity (s)
 
def fpInfinity (s, negative)
 
def fpPlusZero (s)
 
def fpMinusZero (s)
 
def fpZero (s, negative)
 
def FPVal
 
def FP
 
def FPs
 
def fpAbs (a)
 
def fpNeg (a)
 
def fpAdd (rm, a, b)
 
def fpSub (rm, a, b)
 
def fpMul (rm, a, b)
 
def fpDiv (rm, a, b)
 
def fpRem (a, b)
 
def fpMin (a, b)
 
def fpMax (a, b)
 
def fpFMA (rm, a, b, c)
 
def fpSqrt (rm, a)
 
def fpRoundToIntegral (rm, a)
 
def fpIsNaN (a)
 
def fpIsInfinite (a)
 
def fpIsZero (a)
 
def fpIsNormal (a)
 
def fpIsSubnormal (a)
 
def fpIsNegative (a)
 
def fpIsPositive (a)
 
def fpLT (a, b)
 
def fpLEQ (a, b)
 
def fpGT (a, b)
 
def fpGEQ (a, b)
 
def fpEQ (a, b)
 
def fpNEQ (a, b)
 
def fpFP (sgn, exp, sig)
 
def fpToFP
 
def fpToFPUnsigned (rm, x, s)
 
def fpToSBV (rm, x, s)
 
def fpToUBV (rm, x, s)
 
def fpToReal (x)
 
def fpToIEEEBV (x)
 

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)
 
 _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO
 Floating-Point Arithmetic. More...
 
int _dflt_fpsort_ebits = 11
 
int _dflt_fpsort_sbits = 53