37 return Object.ReferenceEquals(a, b) ||
38 (!Object.ReferenceEquals(a, null) &&
39 !Object.ReferenceEquals(b, null) &&
40 a.Context.nCtx == b.Context.nCtx &&
41 Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
56 public override bool Equals(
object o)
59 if (casted == null)
return false;
60 return this == casted;
68 return base.GetHashCode();
76 return Native.Z3_func_decl_to_string(
Context.nCtx, NativeObject);
84 get {
return Native.Z3_get_func_decl_id(
Context.nCtx, NativeObject); }
92 get {
return Native.Z3_get_arity(
Context.nCtx, NativeObject); }
99 public uint DomainSize
101 get {
return Native.Z3_get_domain_size(
Context.nCtx, NativeObject); }
111 Contract.Ensures(Contract.Result<
Sort[]>() != null);
116 for (uint i = 0; i < n; i++)
129 Contract.Ensures(Contract.Result<
Sort>() != null);
149 Contract.Ensures(Contract.Result<
Symbol>() != null);
157 public uint NumParameters
159 get {
return Native.Z3_get_decl_num_parameters(
Context.nCtx, NativeObject); }
169 Contract.Ensures(Contract.Result<
Parameter[]>() != null);
171 uint num = NumParameters;
173 for (uint i = 0; i < num; i++)
179 res[i] =
new Parameter(k, Native.Z3_get_decl_int_parameter(
Context.nCtx, NativeObject, i));
182 res[i] =
new Parameter(k, Native.Z3_get_decl_double_parameter(
Context.nCtx, NativeObject, i));
197 res[i] =
new Parameter(k, Native.Z3_get_decl_rational_parameter(
Context.nCtx, NativeObject, i));
200 throw new Z3Exception(
"Unknown function declaration parameter kind encountered");
213 readonly
private int i;
214 readonly
private double d;
215 readonly
private Symbol sym;
216 readonly
private Sort srt;
217 readonly
private AST ast;
219 readonly
private string r;
224 public double Double {
get {
if (ParameterKind !=
Z3_parameter_kind.Z3_PARAMETER_DOUBLE)
throw new Z3Exception(
"parameter is not a double ");
return d; } }
234 public string Rational {
get {
if (ParameterKind !=
Z3_parameter_kind.Z3_PARAMETER_RATIONAL)
throw new Z3Exception(
"parameter is not a rational string");
return r; } }
290 Contract.Requires(ctx != null);
294 : base(ctx, Native.Z3_mk_func_decl(ctx.nCtx, name.NativeObject,
AST.ArrayLength(domain),
AST.ArrayToNative(domain), range.NativeObject))
296 Contract.Requires(ctx != null);
297 Contract.Requires(name != null);
298 Contract.Requires(range != null);
302 : base(ctx, Native.Z3_mk_fresh_func_decl(ctx.nCtx, prefix,
AST.ArrayLength(domain),
AST.ArrayToNative(domain), range.NativeObject))
304 Contract.Requires(ctx != null);
305 Contract.Requires(range != null);
309 internal override void CheckNativeObject(IntPtr obj)
312 throw new Z3Exception(
"Underlying object is not a function declaration");
313 base.CheckNativeObject(obj);
323 public Expr this[params
Expr[] args]
327 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
340 Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
expr operator!=(expr const &a, expr const &b)
override bool Equals(object o)
Object comparison.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
override int GetHashCode()
A hash code.
Function declarations can have Parameters associated with them.
Expr Apply(params Expr[] args)
Create expression that applies function to arguments.
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
expr operator==(expr const &a, expr const &b)
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.
Symbols are used to name several term and type constructors.
override string ToString()
A string representations of the function declaration.
Z3_decl_kind
The different kinds of interpreted function kinds.