20using System.Diagnostics;
43 return Expr.Create(
Context, Native.Z3_simplify_ex(
Context.nCtx, NativeObject, p.NativeObject));
63 get {
return (
Z3_lbool)Native.Z3_get_bool_value(
Context.nCtx, NativeObject); }
71 get {
return Native.Z3_get_app_num_args(
Context.nCtx, NativeObject); }
84 for (uint i = 0; i < n; i++)
104 Debug.Assert(args !=
null);
105 Debug.Assert(args.All(a => a !=
null));
109 throw new Z3Exception(
"Number of arguments does not match");
110 NativeObject = Native.Z3_update_term(
Context.nCtx, NativeObject, (uint)args.Length,
Expr.ArrayToNative(args));
123 Debug.Assert(from !=
null);
124 Debug.Assert(to !=
null);
125 Debug.Assert(from.All(f => f !=
null));
126 Debug.Assert(to.All(t => t !=
null));
130 if (from.Length != to.Length)
131 throw new Z3Exception(
"Argument sizes do not match");
132 return Expr.Create(
Context, Native.Z3_substitute(
Context.nCtx, NativeObject, (uint)from.Length,
Expr.ArrayToNative(from),
Expr.ArrayToNative(to)));
141 Debug.Assert(from !=
null);
142 Debug.Assert(to !=
null);
155 Debug.Assert(to !=
null);
156 Debug.Assert(to.All(t => t !=
null));
159 return Expr.Create(
Context, Native.Z3_substitute_vars(
Context.nCtx, NativeObject, (uint)to.Length,
Expr.ArrayToNative(to)));
177 return base.ToString();
185 get {
return Native.Z3_is_numeral_ast(
Context.nCtx, NativeObject) != 0; }
194 get {
return Native.Z3_is_well_sorted(
Context.nCtx, NativeObject) != 0; }
218 #region Integer Numerals
228 #region Real Numerals
238 #region Algebraic Numbers
244 get {
return 0 != Native.Z3_is_algebraic_number(
Context.nCtx, NativeObject); }
248 #region Term Kind Tests
250 #region Boolean Terms
259 Native.Z3_is_eq_sort(
Context.nCtx,
260 Native.Z3_mk_bool_sort(
Context.nCtx),
261 Native.Z3_get_sort(
Context.nCtx, NativeObject)) != 0);
357 #region Arithmetic Terms
363 get {
return Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_INT_SORT; }
371 get {
return Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_REAL_SORT; }
463 return (Native.Z3_is_app(
Context.nCtx, NativeObject) != 0 &&
534 #region Bit-vector terms
540 get {
return Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_BV_SORT; }
823 #region Sequences and Strings
835 public string String {
get {
return Native.Z3_get_string(
Context.nCtx, NativeObject); } }
1368 #region Relational Terms
1376 return (Native.Z3_is_app(
Context.nCtx, NativeObject) != 0 &&
1377 Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject))
1490 #region Finite domain terms
1498 return (Native.Z3_is_app(
Context.nCtx, NativeObject) != 0 &&
1499 Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
1509 #region Floating-point terms
1515 get {
return Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
1523 get {
return Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
1785 #region Bound Variables
1810 throw new Z3Exception(
"Term is not a bound variable.");
1812 return Native.Z3_get_index_value(
Context.nCtx, NativeObject);
1821 internal protected Expr(
Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx !=
null); }
1824 internal override void CheckNativeObject(IntPtr obj)
1826 if (Native.Z3_is_app(
Context.nCtx, obj) == 0 &&
1829 throw new Z3Exception(
"Underlying object is not a term");
1830 base.CheckNativeObject(obj);
1834 internal static Expr Create(Context ctx,
FuncDecl f, params
Expr[] arguments)
1836 Debug.Assert(ctx !=
null);
1837 Debug.Assert(f !=
null);
1839 IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
1840 AST.ArrayLength(arguments),
1841 AST.ArrayToNative(arguments));
1842 return Create(ctx, obj);
1845 new internal static Expr Create(Context ctx, IntPtr obj)
1847 Debug.Assert(ctx !=
null);
1851 return new Quantifier(ctx, obj);
1852 IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
1855 if (0 != Native.Z3_is_algebraic_number(ctx.nCtx, obj))
1856 return new AlgebraicNum(ctx, obj);
1858 if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
1863 case Z3_sort_kind.Z3_INT_SORT:
return new IntNum(ctx, obj);
1864 case Z3_sort_kind.Z3_REAL_SORT:
return new RatNum(ctx, obj);
1865 case Z3_sort_kind.Z3_BV_SORT:
return new BitVecNum(ctx, obj);
1866 case Z3_sort_kind.Z3_FLOATING_POINT_SORT:
return new FPNum(ctx, obj);
1867 case Z3_sort_kind.Z3_ROUNDING_MODE_SORT:
return new FPRMNum(ctx, obj);
1868 case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT:
return new FiniteDomainNum(ctx, obj);
1874 case Z3_sort_kind.Z3_BOOL_SORT:
return new BoolExpr(ctx, obj);
1875 case Z3_sort_kind.Z3_INT_SORT:
return new IntExpr(ctx, obj);
1876 case Z3_sort_kind.Z3_REAL_SORT:
return new RealExpr(ctx, obj);
1877 case Z3_sort_kind.Z3_BV_SORT:
return new BitVecExpr(ctx, obj);
1878 case Z3_sort_kind.Z3_ARRAY_SORT:
return new ArrayExpr(ctx, obj);
1879 case Z3_sort_kind.Z3_DATATYPE_SORT:
return new DatatypeExpr(ctx, obj);
1880 case Z3_sort_kind.Z3_FLOATING_POINT_SORT:
return new FPExpr(ctx, obj);
1881 case Z3_sort_kind.Z3_ROUNDING_MODE_SORT:
return new FPRMExpr(ctx, obj);
1882 case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT:
return new FiniteDomainExpr(ctx, obj);
1883 case Z3_sort_kind.Z3_RE_SORT:
return new ReExpr(ctx, obj);
1884 case Z3_sort_kind.Z3_SEQ_SORT:
return new SeqExpr(ctx, obj);
1887 return new Expr(ctx, obj);
The abstract syntax tree (AST) class.
bool IsVar
Indicates whether the AST is a BoundVariable
bool IsApp
Indicates whether the AST is an application
bool IsExpr
Indicates whether the AST is an Expr
The main interaction with Z3 happens via the Context.
uint AtMostBound
Retrieve bound of at-most
bool IsContains
Check whether expression is a contains.
bool IsInt
Indicates whether the term is of integer sort.
bool IsBVXOR3
Indicates whether the term is a bit-vector ternary XOR
bool IsConst
Indicates whether the term represents a constant.
bool IsProofTransitivityStar
Indicates whether the term is a proof by condensed transitivity of a relation
bool IsXor
Indicates whether the term is an exclusive or
bool IsFPToReal
Indicates whether the term is a floating-point conversion to real term
bool IsFPMinusInfinity
Indicates whether the term is a floating-point -oo
bool IsBVSLE
Indicates whether the term is a signed bit-vector less-than-or-equal
bool IsFPRMRoundNearestTiesToAway
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
Z3_lbool BoolValue
Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF).
bool IsProofTheoryLemma
Indicates whether the term is a proof for theory lemma
bool IsFP
Indicates whether the terms is of floating-point sort.
bool IsIntNum
Indicates whether the term is an integer numeral.
bool IsRelationUnion
Indicates whether the term is the union or convex hull of two relations.
bool IsBVConcat
Indicates whether the term is a bit-vector concatenation (binary)
bool IsFiniteDomain
Indicates whether the term is of an array sort.
bool IsProofQuantIntro
Indicates whether the term is a quant-intro proof
bool IsConcat
Check whether expression is a concatenation.
bool IsAt
Check whether expression is an at.
uint Index
The de-Bruijn index of a bound variable.
bool IsProofHypothesis
Indicates whether the term is a hypothesis marker.
bool IsProofTrue
Indicates whether the term is a Proof for the expression 'true'.
bool IsBVBitZero
Indicates whether the term is a one-bit bit-vector with value zero
bool IsRelationNegationFilter
Indicates whether the term is an intersection of a relation with the negation of another.
bool IsBVZeroExtension
Indicates whether the term is a bit-vector zero extension
bool IsProofNNFPos
Indicates whether the term is a proof for a positive NNF step
bool IsFPToFpUnsigned
Indicates whether the term is a floating-point conversion from unsigned bit-vector term
bool IsFPDiv
Indicates whether the term is a floating-point division term
bool IsBVShiftRightLogical
Indicates whether the term is a bit-vector logical shift right
bool IsPbEq
Indicates whether the term is pbeq
bool IsFPLe
Indicates whether the term is a floating-point less-than or equal term
Expr Substitute(Expr from, Expr to)
Substitute every occurrence of from in the expression with to.
Expr Substitute(Expr[] from, Expr[] to)
Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs.
bool IsFPLt
Indicates whether the term is a floating-point less-than term
bool IsBVCarry
Indicates whether the term is a bit-vector carry
bool IsFPRMExprRTN
Indicates whether the term is the floating-point rounding numeral roundTowardNegative
bool IsBVRotateLeft
Indicates whether the term is a bit-vector rotate left
bool IsTrue
Indicates whether the term is the constant true.
bool IsFPRMRoundTowardPositive
Indicates whether the term is the floating-point rounding numeral roundTowardPositive
bool IsBVAdd
Indicates whether the term is a bit-vector addition (binary)
bool IsFPRoundToIntegral
Indicates whether the term is a floating-point roundToIntegral term
bool IsFPEq
Indicates whether the term is a floating-point equality term
bool IsRelationStore
Indicates whether the term is an relation store
bool IsBVSGE
Indicates whether the term is a signed bit-vector greater-than-or-equal
uint NumArgs
The number of arguments of the expression.
bool IsProofReflexivity
Indicates whether the term is a proof for (R t t), where R is a reflexive relation.
bool IsReplace
Check whether expression is a replace.
new Expr Translate(Context ctx)
Translates (copies) the term to the Context ctx .
bool IsProofModusPonensOEQ
Indicates whether the term is a proof by modus ponens for equi-satisfiability.
bool IsFPFMA
Indicates whether the term is a floating-point fused multiply-add term
bool IsRatNum
Indicates whether the term is a real numeral.
bool IsNumeral
Indicates whether the term is a numeral
bool IsBVComp
Indicates whether the term is a bit-vector comparison
bool IsFPRMExprRTZ
Indicates whether the term is the floating-point rounding numeral roundTowardZero
bool IsProofIFFFalse
Indicates whether the term is a proof by iff-false
bool IsFPRMRoundTowardZero
Indicates whether the term is the floating-point rounding numeral roundTowardZero
bool IsBVULT
Indicates whether the term is an unsigned bit-vector less-than
bool IsFPisPositive
Indicates whether the term is a floating-point isPositive predicate term
bool IsRelationSelect
Indicates whether the term is a relational select
bool IsProofElimUnusedVars
Indicates whether the term is a proof for elimination of unused variables.
bool IsFPToUBV
Indicates whether the term is a floating-point conversion to unsigned bit-vector term
bool IsFalse
Indicates whether the term is the constant false.
bool IsPbLe
Indicates whether the term is pble
bool IsEq
Indicates whether the term is an equality predicate.
bool IsProofLemma
Indicates whether the term is a proof by lemma
bool IsBVReduceOR
Indicates whether the term is a bit-vector reduce OR
bool IsArrayMap
Indicates whether the term is an array map.
bool IsProofDefIntro
Indicates whether the term is a proof for introduction of a name
bool IsBVNumeral
Indicates whether the term is a bit-vector numeral
bool IsBVAND
Indicates whether the term is a bit-wise AND
bool IsPbGe
Indicates whether the term is pbge
bool IsFPAbs
Indicates whether the term is a floating-point term absolute value term
bool IsRelationFilter
Indicates whether the term is a relation filter
bool IsProofApplyDef
Indicates whether the term is a proof for application of a definition
bool IsProofIFFTrue
Indicates whether the term is a proof by iff-true
bool IsIntToReal
Indicates whether the term is a coercion of integer to real (unary)
bool IsFPisNormal
Indicates whether the term is a floating-point isNormal term
bool IsString
Check whether expression is a string constant.
bool IsProofQuantInst
Indicates whether the term is a proof for quantifier instantiation
bool IsFPMax
Indicates whether the term is a floating-point maximum term
Expr SubstituteVars(Expr[] to)
Substitute the free variables in the expression with the expressions in to
bool IsIff
Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)
bool IsBVNOR
Indicates whether the term is a bit-wise NOR
bool IsFPNaN
Indicates whether the term is a floating-point NaN
bool IsBVXOR
Indicates whether the term is a bit-wise XOR
bool IsBVUGE
Indicates whether the term is an unsigned bit-vector greater-than-or-equal
bool IsExtract
Check whether expression is an extract.
bool IsFPisZero
Indicates whether the term is a floating-point isZero predicate term
bool IsProofDER
Indicates whether the term is a proof for destructive equality resolution
bool IsIndex
Check whether expression is a sequence index.
bool IsRelationClone
Indicates whether the term is a relational clone (copy)
bool IsFiniteDomainLT
Indicates whether the term is a less than predicate over a finite domain.
bool IsIntToBV
Indicates whether the term is a coercion from integer to bit-vector
bool IsLE
Indicates whether the term is a less-than-or-equal
Expr[] Args
The arguments of the expression.
bool IsBVUMinus
Indicates whether the term is a bit-vector unary minus
bool IsBVShiftRightArithmetic
Indicates whether the term is a bit-vector arithmetic shift left
Expr(Context ctx, IntPtr obj)
Constructor for Expr
bool IsOr
Indicates whether the term is an n-ary disjunction
bool IsFPToSBV
Indicates whether the term is a floating-point conversion to signed bit-vector term
bool IsBVXNOR
Indicates whether the term is a bit-wise XNOR
bool IsFPRMExprRNA
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
bool IsFPGe
Indicates whether the term is a floating-point greater-than or equal term
bool IsFPMin
Indicates whether the term is a floating-point minimum term
bool IsSetUnion
Indicates whether the term is set union
bool IsProofModusPonens
Indicates whether the term is proof via modus ponens
bool IsBVReduceAND
Indicates whether the term is a bit-vector reduce AND
bool IsAsArray
Indicates whether the term is an as-array term.
bool IsBVToInt
Indicates whether the term is a coercion from bit-vector to integer
bool IsIDiv
Indicates whether the term is integer division (binary)
bool IsFPMul
Indicates whether the term is a floating-point multiplication term
bool IsModulus
Indicates whether the term is modulus (binary)
bool IsFPNumeral
Indicates whether the term is a floating-point numeral
bool IsProofRewriteStar
Indicates whether the term is a proof by rewriting
bool IsSetIntersect
Indicates whether the term is set intersection
string String
Retrieve string corresponding to string constant.
bool IsBVRotateRight
Indicates whether the term is a bit-vector rotate right
bool IsFPRMRoundNearestTiesToEven
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
bool IsFPisSubnormal
Indicates whether the term is a floating-point isSubnormal predicate term
bool IsAtLeast
Indicates whether the term is at-least
bool IsITE
Indicates whether the term is a ternary if-then-else term
bool IsAdd
Indicates whether the term is addition (binary)
bool IsLT
Indicates whether the term is a less-than
bool IsFPRMNumeral
Indicates whether the term is a floating-point rounding mode numeral
bool IsStore
Indicates whether the term is an array store.
bool IsBVNAND
Indicates whether the term is a bit-wise NAND
bool IsBVShiftLeft
Indicates whether the term is a bit-vector shift left
bool IsMul
Indicates whether the term is multiplication (binary)
bool IsFPisNegative
Indicates whether the term is a floating-point isNegative predicate term
bool IsFPRem
Indicates whether the term is a floating-point remainder term
bool IsAtMost
Indicates whether the term is at-most
bool IsFPToIEEEBV
Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term
bool IsProofPullQuant
Indicates whether the term is a proof for pulling quantifiers out.
bool IsFPGt
Indicates whether the term is a floating-point greater-than term
bool IsDistinct
Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).
bool IsRelation
Indicates whether the term is of relation sort.
bool IsFPisInf
Indicates whether the term is a floating-point isInf predicate term
bool IsProofNNFNeg
Indicates whether the term is a proof for a negative NNF step
bool IsDiv
Indicates whether the term is division (binary)
bool IsBVRotateRightExtended
Indicates whether the term is a bit-vector rotate right (extended)
Expr Arg(uint i)
The i'th argument of the expression.
bool IsGT
Indicates whether the term is a greater-than
bool IsBVSDiv
Indicates whether the term is a bit-vector signed division (binary)
bool IsReal
Indicates whether the term is of sort real.
override string ToString()
Returns a string representation of the expression.
bool IsLabel
Indicates whether the term is a label (used by the Boogie Verification condition generator).
bool IsRemainder
Indicates whether the term is remainder (binary)
bool IsProofTransitivity
Indicates whether the term is a proof by transitivity of a relation
bool IsRelationalJoin
Indicates whether the term is a relational join
bool IsOEQ
Indicates whether the term is a binary equivalence modulo namings.
bool IsDefaultArray
Indicates whether the term is a default array.
bool IsConstantArray
Indicates whether the term is a constant array.
bool IsGE
Indicates whether the term is a greater-than-or-equal
bool IsRelationRename
Indicates whether the term is the renaming of a column in a relation
bool IsIsEmptyRelation
Indicates whether the term is a test for the emptiness of a relation
bool IsProofAsserted
Indicates whether the term is a proof for a fact asserted by the user.
bool IsFPRM
Indicates whether the terms is of floating-point rounding mode sort.
bool IsProofOrElimination
Indicates whether the term is a proof by elimination of not-or
bool IsRealToInt
Indicates whether the term is a coercion of real to integer (unary)
bool IsAnd
Indicates whether the term is an n-ary conjunction
bool IsFPPlusInfinity
Indicates whether the term is a floating-point +oo
bool IsBV
Indicates whether the terms is of bit-vector sort.
bool IsProofMonotonicity
Indicates whether the term is a monotonicity proof object.
bool IsFPisNaN
Indicates whether the term is a floating-point isNaN predicate term
bool IsBool
Indicates whether the term has Boolean sort.
bool IsFPRMRoundTowardNegative
Indicates whether the term is the floating-point rounding numeral roundTowardNegative
void Update(Expr[] args)
Update the arguments of the expression using the arguments args The number of new arguments should c...
bool IsProofDefAxiom
Indicates whether the term is a proof for Tseitin-like axioms
bool IsWellSorted
Indicates whether the term is well-sorted.
bool IsImplies
Indicates whether the term is an implication
bool IsSuffix
Check whether expression is a suffix.
bool IsBVSRem
Indicates whether the term is a bit-vector signed remainder (binary)
bool IsFPToFp
Indicates whether the term is a floating-point conversion term
bool IsLabelLit
Indicates whether the term is a label literal (used by the Boogie Verification condition generator).
uint AtLeastBound
Retrieve bound of at-least
bool IsProofUnitResolution
Indicates whether the term is a proof by unit resolution
bool IsProofGoal
Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
bool IsFPSqrt
Indicates whether the term is a floating-point square root term
bool IsSelect
Indicates whether the term is an array select.
bool IsNot
Indicates whether the term is a negation
bool IsFPFP
Indicates whether the term is a floating-point constructor term
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
bool IsFPMinusZero
Indicates whether the term is a floating-point -zero
bool IsRelationProject
Indicates whether the term is a projection of columns (provided as numbers in the parameters).
bool IsUMinus
Indicates whether the term is a unary minus
bool IsRelationWiden
Indicates whether the term is the widening of two relations
bool IsBVRepeat
Indicates whether the term is a bit-vector repetition
bool IsSub
Indicates whether the term is subtraction (binary)
bool IsRelationComplement
Indicates whether the term is the complement of a relation
bool IsBVOR
Indicates whether the term is a bit-wise OR
bool IsBVSub
Indicates whether the term is a bit-vector subtraction (binary)
bool IsBVRotateLeftExtended
Indicates whether the term is a bit-vector rotate left (extended)
bool IsProofSymmetry
Indicates whether the term is proof by symmetricity of a relation
bool IsProofSkolemize
Indicates whether the term is a proof for a Skolemization step
bool IsBVMul
Indicates whether the term is a bit-vector multiplication (binary)
bool IsLength
Check whether expression is a sequence length.
bool IsFPSub
Indicates whether the term is a floating-point subtraction term
bool IsBVUDiv
Indicates whether the term is a bit-vector unsigned division (binary)
bool IsProofCommutativity
Indicates whether the term is a proof by commutativity
bool IsAlgebraicNumber
Indicates whether the term is an algebraic number
bool IsProofRewrite
Indicates whether the term is a proof by rewriting
bool IsFPRMExprRNE
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
bool IsArithmeticNumeral
Indicates whether the term is an arithmetic numeral.
bool IsProofAndElimination
Indicates whether the term is a proof by elimination of AND
bool IsEmptyRelation
Indicates whether the term is an empty relation
bool IsProofPushQuant
Indicates whether the term is a proof for pushing quantifiers in.
bool IsProofDistributivity
Indicates whether the term is a distributivity proof object.
bool IsBVURem
Indicates whether the term is a bit-vector unsigned remainder (binary)
bool IsBVULE
Indicates whether the term is an unsigned bit-vector less-than-or-equal
bool IsBVSLT
Indicates whether the term is a signed bit-vector less-than
bool IsBVExtract
Indicates whether the term is a bit-vector extraction
bool IsBVSignExtension
Indicates whether the term is a bit-vector sign extension
bool IsRealIsInt
Indicates whether the term is a check that tests whether a real is integral (unary)
bool IsSetDifference
Indicates whether the term is set difference
Expr Simplify(Params p=null)
Returns a simplified version of the expression.
bool IsBVUGT
Indicates whether the term is an unsigned bit-vector greater-than
bool IsPrefix
Check whether expression is a prefix.
bool IsFPRMExprRTP
Indicates whether the term is the floating-point rounding numeral roundTowardPositive
bool IsFPAdd
Indicates whether the term is a floating-point addition term
bool IsFPRMExpr
Indicates whether the term is a floating-point rounding mode numeral
bool IsBVSMod
Indicates whether the term is a bit-vector signed modulus
bool IsBVBitOne
Indicates whether the term is a one-bit bit-vector with value one
bool IsFPNeg
Indicates whether the term is a floating-point negation term
bool IsArray
Indicates whether the term is of an array sort.
bool IsBVNOT
Indicates whether the term is a bit-wise NOT
bool IsBVSGT
Indicates whether the term is a signed bit-vector greater-than
bool IsSetSubset
Indicates whether the term is set subset
bool IsSetComplement
Indicates whether the term is set complement
bool IsProofIFFOEQ
Indicates whether the term is a proof iff-oeq
int Int
The int value of the parameter.
Parameter[] Parameters
The parameters of the function declaration
uint DomainSize
The size of the domain of the function declaration Arity
Z3_decl_kind DeclKind
The kind of the function declaration.
A Params objects represents a configuration in the form of Symbol/value pairs.
The Sort class implements type information for ASTs.
The exception base class for error reporting from Z3
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Z3_decl_kind
The different kinds of interpreted function kinds.
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Z3_lbool
Lifted Boolean type: false, undefined, true.