21using System.Diagnostics;
38 return Object.ReferenceEquals(a, b) ||
39 (!Object.ReferenceEquals(a,
null) &&
40 !Object.ReferenceEquals(b,
null) &&
41 a.Context.nCtx == b.Context.nCtx &&
42 Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
57 public override bool Equals(
object o)
60 if (casted ==
null)
return false;
61 return this == casted;
69 return base.GetHashCode();
77 return Native.Z3_func_decl_to_string(
Context.nCtx, NativeObject);
85 get {
return Native.Z3_get_func_decl_id(
Context.nCtx, NativeObject); }
93 get {
return Native.Z3_get_arity(
Context.nCtx, NativeObject); }
102 get {
return Native.Z3_get_domain_size(
Context.nCtx, NativeObject); }
116 for (uint i = 0; i < n; i++)
157 get {
return Native.Z3_get_decl_num_parameters(
Context.nCtx, NativeObject); }
170 for (uint i = 0; i < num; i++)
176 res[i] =
new Parameter(k, Native.Z3_get_decl_int_parameter(
Context.nCtx, NativeObject, i));
179 res[i] =
new Parameter(k, Native.Z3_get_decl_double_parameter(
Context.nCtx, NativeObject, i));
194 res[i] =
new Parameter(k, Native.Z3_get_decl_rational_parameter(
Context.nCtx, NativeObject, i));
197 throw new Z3Exception(
"Unknown function declaration parameter kind encountered");
210 readonly
private int i;
211 readonly
private double d;
212 readonly
private Symbol sym;
213 readonly
private Sort srt;
214 readonly
private AST ast;
216 readonly
private string r;
284 internal FuncDecl(Context ctx, IntPtr obj)
287 Debug.Assert(ctx !=
null);
290 internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort
range)
291 : base(ctx, Native.
Z3_mk_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain),
range.NativeObject))
293 Debug.Assert(ctx !=
null);
294 Debug.Assert(name !=
null);
295 Debug.Assert(
range !=
null);
298 internal FuncDecl(Context ctx,
string prefix, Sort[] domain, Sort
range)
299 : base(ctx, Native.
Z3_mk_fresh_func_decl(ctx.nCtx, prefix, AST.ArrayLength(domain), AST.ArrayToNative(domain),
range.NativeObject))
301 Debug.Assert(ctx !=
null);
302 Debug.Assert(
range !=
null);
305 internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort
range,
bool is_rec)
306 : base(ctx, Native.
Z3_mk_rec_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain),
range.NativeObject))
308 Debug.Assert(ctx !=
null);
309 Debug.Assert(name !=
null);
310 Debug.Assert(
range !=
null);
315 internal override void CheckNativeObject(IntPtr obj)
317 if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)
Z3_ast_kind.Z3_FUNC_DECL_AST)
318 throw new Z3Exception(
"Underlying object is not a function declaration");
319 base.CheckNativeObject(obj);
344 Debug.Assert(
args ==
null ||
args.All(a => a !=
null));
357 Debug.Assert(
args ==
null ||
args.All(a => a !=
null));
The abstract syntax tree (AST) class.
The main interaction with Z3 happens via the Context.
Function declarations can have Parameters associated with them.
AST AST
The AST value of the parameter.
Symbol Symbol
The Symbol value of the parameter.
double Double
The double value of the parameter.
Sort Sort
The Sort value of the parameter.
string Rational
The rational string value of the parameter.
Z3_parameter_kind ParameterKind
The kind of the parameter.
int Int
The int value of the parameter.
FuncDecl FuncDecl
The FunctionDeclaration value of the parameter.
override bool Equals(object o)
Object comparison.
Parameter[] Parameters
The parameters of the function declaration
Sort Range
The range of the function declaration
uint Arity
The arity of the function declaration
Expr this[params Expr[] args
Create expression that applies function to arguments.
Expr Apply(params Expr[] args)
Create expression that applies function to arguments.
uint DomainSize
The size of the domain of the function declaration Arity
override int GetHashCode()
A hash code.
static bool operator==(FuncDecl a, FuncDecl b)
Comparison operator.
static bool operator!=(FuncDecl a, FuncDecl b)
Comparison operator.
override string ToString()
A string representations of the function declaration.
Z3_decl_kind DeclKind
The kind of the function declaration.
Sort[] Domain
The domain of the function declaration
uint NumParameters
The number of parameters of the function declaration
Symbol Name
The name of the function declaration
new uint Id
Returns a unique identifier for the function declaration.
new FuncDecl Translate(Context ctx)
Translates (copies) the function declaration to the Context ctx .
The Sort class implements type information for ASTs.
Symbols are used to name several term and type constructors.
The exception base class for error reporting from Z3
expr range(expr const &lo, expr const &hi)
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_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.