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 | FiniteDomainSortRef
class | FiniteDomainRef
class | FiniteDomainNumRef
class | OptimizeObjective
| Optimize. More...
class | Optimize
class | ApplyResult
class | Tactic
class | Probe
class | FPSortRef
class | FPRMSortRef
class | FPRef
class | FPRMRef
class | FPNumRef
class | SeqSortRef
| Strings, Sequences and Regular expressions. More...
class | SeqRef
class | ReSortRef
class | ReRef
class | PropClosures
class | UserPropagateBase

## Namespaces
namespace | z3py

## Functions
def | z3_debug ()
def | enable_trace (msg)
def | disable_trace (msg)
def | get_version_string ()
def | get_version ()
def | get_full_version ()
def | open_log (fname)
def | append_log (s)
def | to_symbol (s, ctx=None)
def | z3_error_handler (c, e)
def | main_ctx ()
def | get_ctx (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 (name, ctx=None)
def | is_func_decl (a)
def | Function (name, *sig)
def | FreshFunction (*sig)
def | RecFunction (name, *sig)
def | RecAddDefinition (f, args, body)
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 (a, b, c, ctx=None)
def | Distinct (*args)
def | Const (name, sort)
def | Consts (names, sort)
def | FreshConst (sort, prefix="c")
def | Var (idx, s)
def | RealVar (idx, ctx=None)
def | RealVarVector (n, ctx=None)
def | is_bool (a)
def | is_true (a)
def | is_false (a)
def | is_and (a)
def | is_or (a)
def | is_implies (a)
def | is_not (a)
def | is_eq (a)
def | is_distinct (a)
def | BoolSort (ctx=None)
def | BoolVal (val, ctx=None)
def | Bool (name, ctx=None)
def | Bools (names, ctx=None)
def | BoolVector (prefix, sz, ctx=None)
def | FreshBool (prefix="b", ctx=None)
def | Implies (a, b, ctx=None)
def | Xor (a, b, ctx=None)
def | Not (a, ctx=None)
def | mk_not (a)
def | And (*args)
def | Or (*args)
def | is_pattern (a)
def | MultiPattern (*args)
def | is_quantifier (a)
def | ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
def | Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
def | Lambda (vs, body)
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 (ctx=None)
def | RealSort (ctx=None)
def | IntVal (val, ctx=None)
def | RealVal (val, ctx=None)
def | RatVal (a, b, ctx=None)
def | Q (a, b, ctx=None)
def | Int (name, ctx=None)
def | Ints (names, ctx=None)
def | IntVector (prefix, sz, ctx=None)
def | FreshInt (prefix="x", ctx=None)
def | Real (name, ctx=None)
def | Reals (names, ctx=None)
def | RealVector (prefix, sz, ctx=None)
def | FreshReal (prefix="b", ctx=None)
def | ToReal (a)
def | ToInt (a)
def | IsInt (a)
def | Sqrt (a, ctx=None)
def | Cbrt (a, ctx=None)
def | is_bv_sort (s)
def | is_bv (a)
def | is_bv_value (a)
def | BV2Int (a, is_signed=False)
def | Int2BV (a, num_bits)
def | BitVecSort (sz, ctx=None)
def | BitVecVal (val, bv, ctx=None)
def | BitVec (name, bv, ctx=None)
def | BitVecs (names, bv, ctx=None)
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 | BVAddNoOverflow (a, b, signed)
def | BVAddNoUnderflow (a, b)
def | BVSubNoOverflow (a, b)
def | BVSubNoUnderflow (a, b, signed)
def | BVSDivNoOverflow (a, b)
def | BVSNegNoOverflow (a)
def | BVMulNoOverflow (a, b, signed)
def | BVMulNoUnderflow (a, b)
def | is_array_sort (a)
def | is_array (a)
def | is_const_array (a)
def | is_K (a)
def | is_map (a)
def | is_default (a)
def | get_map_func (a)
def | ArraySort (*sig)
def | Array (name, dom, rng)
def | Update (a, i, v)
def | Default (a)
def | Store (a, i, v)
def | Select (a, i)
def | Map (f, *args)
def | K (dom, v)
def | Ext (a, b)
def | SetHasSize (a, k)
def | is_select (a)
def | is_store (a)
def | SetSort (s)
| Sets. More...
def | EmptySet (s)
def | FullSet (s)
def | SetUnion (*args)
def | SetIntersect (*args)
def | SetAdd (s, e)
def | SetDel (s, e)
def | SetComplement (s)
def | SetDifference (a, b)
def | IsMember (e, s)
def | IsSubset (a, b)
def | CreateDatatypes (*ds)
def | TupleSort (name, sorts, ctx=None)
def | DisjointSum (name, sorts, ctx=None)
def | EnumSort (name, values, ctx=None)
def | args2params (arguments, keywords, ctx=None)
def | Model (ctx=None)
def | is_as_array (n)
def | get_as_array_func (n)
def | SolverFor (logic, ctx=None, logFile=None)
def | SimpleSolver (ctx=None, logFile=None)
def | FiniteDomainSort (name, sz, ctx=None)
def | is_finite_domain_sort (s)
def | is_finite_domain (a)
def | FiniteDomainVal (val, sort, ctx=None)
def | is_finite_domain_value (a)
def | AndThen (*ts, **ks)
def | Then (*ts, **ks)
def | OrElse (*ts, **ks)
def | ParOr (*ts, **ks)
def | ParThen (t1, t2, ctx=None)
def | ParAndThen (t1, t2, ctx=None)
def | With (t, *args, **keys)
def | WithParams (t, p)
def | Repeat (t, max=4294967295, ctx=None)
def | TryFor (t, ms, ctx=None)
def | tactics (ctx=None)
def | tactic_description (name, ctx=None)
def | describe_tactics ()
def | is_probe (p)
def | probes (ctx=None)
def | probe_description (name, ctx=None)
def | describe_probes ()
def | FailIf (p, ctx=None)
def | When (p, t, ctx=None)
def | Cond (p, t1, t2, ctx=None)
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 | AtMost (*args)
def | AtLeast (*args)
def | PbLe (args, k)
def | PbGe (args, k)
def | PbEq (args, k, ctx=None)
def | solve (*args, **keywords)
def | solve_using (s, *args, **keywords)
def | prove (claim, show=False, **keywords)
def | parse_smt2_string (s, sorts={}, decls={}, ctx=None)
def | parse_smt2_file (f, sorts={}, decls={}, ctx=None)
def | get_default_rounding_mode (ctx=None)
def | set_default_rounding_mode (rm, ctx=None)
def | get_default_fp_sort (ctx=None)
def | set_default_fp_sort (ebits, sbits, ctx=None)
def | Float16 (ctx=None)
def | FloatHalf (ctx=None)
def | Float32 (ctx=None)
def | FloatSingle (ctx=None)
def | Float64 (ctx=None)
def | FloatDouble (ctx=None)
def | Float128 (ctx=None)
def | FloatQuadruple (ctx=None)
def | is_fp_sort (s)
def | is_fprm_sort (s)
def | RoundNearestTiesToEven (ctx=None)
def | RNE (ctx=None)
def | RoundNearestTiesToAway (ctx=None)
def | RNA (ctx=None)
def | RoundTowardPositive (ctx=None)
def | RTP (ctx=None)
def | RoundTowardNegative (ctx=None)
def | RTN (ctx=None)
def | RoundTowardZero (ctx=None)
def | RTZ (ctx=None)
def | is_fprm (a)
def | is_fprm_value (a)
def | is_fp (a)
def | is_fp_value (a)
def | FPSort (ebits, sbits, ctx=None)
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 (sig, exp=None, fps=None, ctx=None)
def | FP (name, fpsort, ctx=None)
def | FPs (names, fpsort, ctx=None)
def | fpAbs (a, ctx=None)
def | fpNeg (a, ctx=None)
def | fpAdd (rm, a, b, ctx=None)
def | fpSub (rm, a, b, ctx=None)
def | fpMul (rm, a, b, ctx=None)
def | fpDiv (rm, a, b, ctx=None)
def | fpRem (a, b, ctx=None)
def | fpMin (a, b, ctx=None)
def | fpMax (a, b, ctx=None)
def | fpFMA (rm, a, b, c, ctx=None)
def | fpSqrt (rm, a, ctx=None)
def | fpRoundToIntegral (rm, a, ctx=None)
def | fpIsNaN (a, ctx=None)
def | fpIsInf (a, ctx=None)
def | fpIsZero (a, ctx=None)
def | fpIsNormal (a, ctx=None)
def | fpIsSubnormal (a, ctx=None)
def | fpIsNegative (a, ctx=None)
def | fpIsPositive (a, ctx=None)
def | fpLT (a, b, ctx=None)
def | fpLEQ (a, b, ctx=None)
def | fpGT (a, b, ctx=None)
def | fpGEQ (a, b, ctx=None)
def | fpEQ (a, b, ctx=None)
def | fpNEQ (a, b, ctx=None)
def | fpFP (sgn, exp, sig, ctx=None)
def | fpToFP (a1, a2=None, a3=None, ctx=None)
def | fpBVToFP (v, sort, ctx=None)
def | fpFPToFP (rm, v, sort, ctx=None)
def | fpRealToFP (rm, v, sort, ctx=None)
def | fpSignedToFP (rm, v, sort, ctx=None)
def | fpUnsignedToFP (rm, v, sort, ctx=None)
def | fpToFPUnsigned (rm, x, s, ctx=None)
def | fpToSBV (rm, x, s, ctx=None)
def | fpToUBV (rm, x, s, ctx=None)
def | fpToReal (x, ctx=None)
def | fpToIEEEBV (x, ctx=None)
def | StringSort (ctx=None)
def | SeqSort (s)
def | is_seq (a)
def | is_string (a)
def | is_string_value (a)
def | StringVal (s, ctx=None)
def | String (name, ctx=None)
def | Strings (names, ctx=None)
def | SubString (s, offset, length)
def | SubSeq (s, offset, length)
def | Empty (s)
def | Full (s)
def | Unit (a)
def | PrefixOf (a, b)
def | SuffixOf (a, b)
def | Contains (a, b)
def | Replace (s, src, dst)
def | IndexOf (s, substr, offset=None)
def | LastIndexOf (s, substr)
def | Length (s)
def | StrToInt (s)
def | IntToStr (s)
def | Re (s, ctx=None)
def | ReSort (s)
def | is_re (s)
def | InRe (s, re)
def | Union (*args)
def | Intersect (*args)
def | Plus (re)
def | Option (re)
def | Complement (re)
def | Star (re)
def | Loop (re, lo, hi=0)
def | Range (lo, hi, ctx=None)
def | PartialOrder (a, index)
def | LinearOrder (a, index)
def | TreeOrder (a, index)
def | PiecewiseLinearOrder (a, index)
def | TransitiveClosure (f)
def | ensure_prop_closures ()
def | user_prop_push (ctx)
def | user_prop_pop (ctx, num_scopes)
def | user_prop_fresh (id, ctx)
def | user_prop_fixed (ctx, cb, id, value)
def | user_prop_final (ctx, cb)
def | user_prop_eq (ctx, cb, x, y)
def | user_prop_diseq (ctx, cb, x, y)

## Variables
| Z3_DEBUG = __debug__
| sat = CheckSatResult(Z3_L_TRUE)
| unsat = CheckSatResult(Z3_L_FALSE)
| unknown = CheckSatResult(Z3_L_UNDEF)