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
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; } }
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);
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));
342 Context.CheckContextMatch(args);
static IntPtr Z3_get_decl_symbol_parameter(Z3_context a0, Z3_func_decl a1, uint a2)
static Z3_func_decl Z3_mk_fresh_func_decl(Z3_context a0, string a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4)
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)
static Z3_func_decl Z3_mk_func_decl(Z3_context a0, IntPtr a1, uint a2, [In] Z3_sort[] a3, Z3_sort a4)
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)
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
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)
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)