21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
38 Contract.Ensures(Contract.Result<
Expr>() != null);
53 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
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));
101 Context.CheckContextMatch(args);
102 if (IsApp && args.Length != NumArgs)
103 throw new Z3Exception(
"Number of arguments does not match");
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);
123 Context.CheckContextMatch(from);
125 if (from.Length != to.Length)
126 throw new Z3Exception(
"Argument sizes do not match");
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);
166 Contract.Requires(ctx != null);
167 Contract.Ensures(Contract.Result<
Expr>() != null);
169 if (ReferenceEquals(
Context, ctx))
180 return base.ToString();
186 public bool IsNumeral
195 public bool IsWellSorted
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
252 #region Term Kind Tests 254 #region Boolean Terms 326 #region Interpolation 334 #region Arithmetic Terms 515 #region Bit-vector terms 1312 #region Relational Terms 1313 public bool IsRelation
1434 #region Finite domain terms 1435 public bool IsFiniteDomain
1453 #region Floating-point terms 1473 public bool IsFPNumeral {
get {
return IsFP && IsNumeral; } }
1478 public bool IsFPRMNumeral {
get {
return IsFPRM && IsNumeral; } }
1533 public bool IsFPRMExpr {
1729 #region Bound Variables 1754 throw new Z3Exception(
"Term is not a bound variable.");
1756 Contract.EndContractBlock();
1764 internal protected Expr(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
1771 internal override void CheckNativeObject(IntPtr obj)
1776 throw new Z3Exception(
"Underlying object is not a term");
1777 base.CheckNativeObject(obj);
1784 Contract.Requires(ctx != null);
1785 Contract.Requires(f != null);
1786 Contract.Ensures(Contract.Result<
Expr>() != null);
1789 AST.ArrayLength(arguments),
1790 AST.ArrayToNative(arguments));
1791 return Create(ctx, obj);
1795 new internal static Expr Create(
Context ctx, IntPtr obj)
1797 Contract.Requires(ctx != null);
1798 Contract.Ensures(Contract.Result<
Expr>() != null);
1833 return new Expr(ctx, obj);
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
static Z3_ast Z3_update_term(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
Expr Simplify(Params p=null)
Returns a simplified version of the expression.
static uint Z3_get_app_num_args(Z3_context a0, Z3_app a1)
uint DomainSize
The size of the domain of the function declaration Arity
static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1)
static uint Z3_get_bool_value(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_substitute(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3, [In] Z3_ast[] a4)
Floating-point rounding mode numerals
static Z3_ast Z3_substitute_vars(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
static Z3_ast Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2)
static Z3_ast Z3_mk_app(Z3_context a0, Z3_func_decl a1, uint a2, [In] Z3_ast[] a3)
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.
static int Z3_is_well_sorted(Z3_context a0, Z3_ast a1)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
static uint Z3_get_index_value(Z3_context a0, Z3_ast a1)
static Z3_sort Z3_get_sort(Z3_context a0, Z3_ast a1)
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
static Z3_ast Z3_get_app_arg(Z3_context a0, Z3_app a1, uint a2)
static int Z3_is_eq_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
static Z3_ast Z3_simplify_ex(Z3_context a0, Z3_ast a1, Z3_params a2)
A Params objects represents a configuration in the form of Symbol/value pairs.
static int Z3_is_algebraic_number(Z3_context a0, Z3_ast a1)
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
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
static Z3_ast Z3_simplify(Z3_context a0, Z3_ast a1)
The abstract syntax tree (AST) class.
FloatingPoint RoundingMode Expressions
static int Z3_is_app(Z3_context a0, Z3_ast a1)
Expr Substitute(Expr from, Expr to)
Substitute every occurrence of from in the expression with to.
static Z3_func_decl Z3_get_app_decl(Z3_context a0, Z3_app a1)
static Z3_sort Z3_mk_bool_sort(Z3_context a0)
static int Z3_is_numeral_ast(Z3_context a0, Z3_ast a1)