21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
37 return Object.ReferenceEquals(a, b) ||
38 (!Object.ReferenceEquals(a, null) &&
39 !Object.ReferenceEquals(b, null) &&
40 a.Context.nCtx == b.Context.nCtx &&
56 public override bool Equals(
object o)
59 if (casted == null)
return false;
60 return this == casted;
68 return base.GetHashCode();
99 public uint DomainSize
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
165 public Parameter[] Parameters
169 Contract.Ensures(Contract.Result<
Parameter[]>() != null);
171 uint num = NumParameters;
173 for (uint i = 0; i < num; 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; } }
287 internal FuncDecl(Context ctx, IntPtr obj)
290 Contract.Requires(ctx != null);
293 internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
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);
301 internal FuncDecl(Context ctx,
string prefix, Sort[] domain, Sort range)
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)
311 if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)
Z3_ast_kind.Z3_FUNC_DECL_AST)
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));
342 Context.CheckContextMatch(args);
static IntPtr Z3_get_decl_symbol_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static IntPtr Z3_get_decl_name(Z3_context a0, Z3_func_decl a1)
static Z3_sort Z3_get_decl_sort_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static int Z3_is_eq_func_decl(Z3_context a0, Z3_func_decl a1, Z3_func_decl a2)
static uint Z3_get_decl_num_parameters(Z3_context a0, Z3_func_decl a1)
static int Z3_get_decl_int_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
override bool Equals(object o)
Object comparison.
static uint Z3_get_domain_size(Z3_context a0, Z3_func_decl a1)
static string Z3_func_decl_to_string(Z3_context a0, Z3_func_decl a1)
static uint Z3_get_decl_kind(Z3_context a0, Z3_func_decl a1)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
override int GetHashCode()
A hash code.
static uint Z3_get_func_decl_id(Z3_context a0, Z3_func_decl a1)
Function declarations can have Parameters associated with them.
static string Z3_get_decl_rational_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Expr Apply(params Expr[] args)
Create expression that applies function to arguments.
static uint Z3_get_decl_parameter_kind(Z3_context a0, Z3_func_decl a1, uint a2)
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
static double Z3_get_decl_double_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(__in Z3_context c, __in Z3_string prefix, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a fresh constant or function.
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_func_decl Z3_get_decl_func_decl_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
The abstract syntax tree (AST) class.
static Z3_sort Z3_get_range(Z3_context a0, Z3_func_decl a1)
Z3_func_decl Z3_API Z3_mk_func_decl(__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in Z3_sort range)
Declare a constant or function.
static Z3_sort Z3_get_domain(Z3_context a0, Z3_func_decl a1, uint a2)
Symbols are used to name several term and type constructors.
override string ToString()
A string representations of the function declaration.
Z3_parameter_kind
Z3_parameter_kind
static uint Z3_get_arity(Z3_context a0, Z3_func_decl a1)
static Z3_ast Z3_get_decl_ast_parameter(Z3_context a0, Z3_func_decl a1, uint a2)