38 Contract.Ensures(Contract.Result<
Expr>() != null);
43 return Expr.Create(
Context, Native.Z3_simplify_ex(
Context.nCtx, NativeObject, p.NativeObject));
53 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
64 get {
return (
Z3_lbool)Native.Z3_get_bool_value(
Context.nCtx, NativeObject); }
72 get {
return Native.Z3_get_app_num_args(
Context.nCtx, NativeObject); }
82 Contract.Ensures(Contract.Result<
Expr[]>() != null);
86 for (uint i = 0; i < n; i++)
98 Contract.Requires(args != null);
99 Contract.Requires(Contract.ForAll(args, a => a != null));
102 if (IsApp && args.Length != NumArgs)
103 throw new Z3Exception(
"Number of arguments does not match");
104 NativeObject = Native.Z3_update_term(
Context.nCtx, NativeObject, (uint)args.Length,
Expr.ArrayToNative(args));
117 Contract.Requires(from != null);
118 Contract.Requires(to != null);
119 Contract.Requires(Contract.ForAll(from, f => f != null));
120 Contract.Requires(Contract.ForAll(to, t => t != null));
121 Contract.Ensures(Contract.Result<
Expr>() != null);
125 if (from.Length != to.Length)
126 throw new Z3Exception(
"Argument sizes do not match");
127 return Expr.Create(
Context, Native.Z3_substitute(
Context.nCtx, NativeObject, (uint)from.Length,
Expr.ArrayToNative(from),
Expr.ArrayToNative(to)));
136 Contract.Requires(from != null);
137 Contract.Requires(to != null);
138 Contract.Ensures(Contract.Result<
Expr>() != null);
140 return Substitute(
new Expr[] { from },
new Expr[] { to });
151 Contract.Requires(to != null);
152 Contract.Requires(Contract.ForAll(to, t => t != null));
153 Contract.Ensures(Contract.Result<
Expr>() != null);
156 return Expr.Create(
Context, Native.Z3_substitute_vars(
Context.nCtx, NativeObject, (uint)to.Length,
Expr.ArrayToNative(to)));
166 Contract.Requires(ctx != null);
167 Contract.Ensures(Contract.Result<
Expr>() != null);
169 if (ReferenceEquals(
Context, ctx))
172 return Expr.Create(ctx, Native.Z3_translate(
Context.nCtx, NativeObject, ctx.nCtx));
180 return base.ToString();
186 public bool IsNumeral
188 get {
return Native.Z3_is_numeral_ast(
Context.nCtx, NativeObject) != 0; }
195 public bool IsWellSorted
197 get {
return Native.Z3_is_well_sorted(
Context.nCtx, NativeObject) != 0; }
207 Contract.Ensures(Contract.Result<
Sort>() != null);
222 #region Integer Numerals 228 get {
return IsNumeral &&
IsInt; }
232 #region Real Numerals 238 get {
return IsNumeral && IsReal; }
242 #region Algebraic Numbers 243 public bool IsAlgebraicNumber
248 get {
return Native.Z3_is_algebraic_number(
Context.nCtx, NativeObject) != 0; }
252 #region Term Kind Tests 254 #region Boolean Terms 263 Native.Z3_is_eq_sort(
Context.nCtx,
264 Native.Z3_mk_bool_sort(
Context.nCtx),
265 Native.Z3_get_sort(
Context.nCtx, NativeObject)) != 0);
326 #region Interpolation 334 #region Arithmetic Terms 340 get {
return Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_INT_SORT; }
348 get {
return Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_REAL_SORT; }
440 return (Native.Z3_is_app(
Context.nCtx, NativeObject) != 0 &&
511 #region Bit-vector terms 517 get {
return Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_BV_SORT; }
1308 #region Relational Terms 1309 public bool IsRelation
1316 return (Native.Z3_is_app(
Context.nCtx, NativeObject) != 0 &&
1317 Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject))
1430 #region Finite domain terms 1431 public bool IsFiniteDomain
1438 return (Native.Z3_is_app(
Context.nCtx, NativeObject) != 0 &&
1439 Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
1449 #region Floating-point terms 1455 get {
return Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
1463 get {
return Native.Z3_get_sort_kind(
Context.nCtx, Native.Z3_get_sort(
Context.nCtx, NativeObject)) == (uint)
Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
1469 public bool IsFPNumeral {
get {
return IsFP && IsNumeral; } }
1474 public bool IsFPRMNumeral {
get {
return IsFPRM && IsNumeral; } }
1529 public bool IsFPRMExpr {
1725 #region Bound Variables 1750 throw new Z3Exception(
"Term is not a bound variable.");
1752 Contract.EndContractBlock();
1754 return Native.Z3_get_index_value(
Context.nCtx, NativeObject);
1760 internal protected Expr(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
1767 internal override void CheckNativeObject(IntPtr obj)
1769 if (Native.Z3_is_app(
Context.nCtx, obj) == 0 &&
1772 throw new Z3Exception(
"Underlying object is not a term");
1773 base.CheckNativeObject(obj);
1780 Contract.Requires(ctx != null);
1781 Contract.Requires(f != null);
1782 Contract.Ensures(Contract.Result<
Expr>() != null);
1784 IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
1785 AST.ArrayLength(arguments),
1786 AST.ArrayToNative(arguments));
1787 return Create(ctx, obj);
1791 new internal static Expr Create(
Context ctx, IntPtr obj)
1793 Contract.Requires(ctx != null);
1794 Contract.Ensures(Contract.Result<
Expr>() != null);
1799 IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
1802 if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0)
1805 if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
1833 return new Expr(ctx, obj);
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Expr Simplify(Params p=null)
Returns a simplified version of the expression.
uint DomainSize
The size of the domain of the function declaration Arity
Floating-point rounding mode numerals
Expr SubstituteVars(Expr[] to)
Substitute the free variables in the expression with the expressions in 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...
Z3_decl_kind DeclKind
The kind of the function declaration.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Z3_lbool
Lifted Boolean type: false, undefined, true.
Finite-domain expressions
new Expr Translate(Context ctx)
Translates (copies) the term to the Context ctx .
override string ToString()
Returns a string representation of the expression.
FloatingPoint Expressions
A Params objects represents a configuration in the form of Symbol/value pairs.
void Update(Expr[] args)
Update the arguments of the expression using the arguments args The number of new arguments should c...
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
The exception base class for error reporting from Z3
The abstract syntax tree (AST) class.
FloatingPoint RoundingMode Expressions
Regular expression expressions
Expr Substitute(Expr from, Expr to)
Substitute every occurrence of from in the expression with to.
Z3_decl_kind
The different kinds of interpreted function kinds.