RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_func_decl.html below:

Z3: FuncDecl Class Reference

Function declarations. More...

class Parameter Function declarations can have Parameters associated with them. More...

Function declarations.

Definition at line 30 of file FuncDecl.cs.

◆ Apply()

Create expression that applies function to arguments.

Parameters

Returns

Definition at line 355 of file FuncDecl.cs.

357

Debug.Assert(

args

null

args

.All(a => a !=

null

));

Expr this[params Expr[] args

Create expression that applies function to arguments.

Context Context

Access Context object

◆ Equals() override bool Equals ( object o ) inline

Object comparison.

Definition at line 57 of file FuncDecl.cs.

59

FuncDecl casted = o as FuncDecl;

60 if

(casted ==

null

)

return false

;

61 return this

== casted;

◆ GetHashCode() override int GetHashCode ( ) inline

A hash code.

Definition at line 67 of file FuncDecl.cs.

69 return

base.GetHashCode();

◆ operator!=()

Comparison operator.

Returns: True if a and b do not share the same context or are not equal, false otherwise.

Definition at line 49 of file FuncDecl.cs.

◆ operator==()

Comparison operator.

Returns: True if a and b share the same context and are equal, false otherwise.

Definition at line 36 of file FuncDecl.cs.

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);

◆ ToString() override string ToString ( ) inline

A string representations of the function declaration.

Definition at line 75 of file FuncDecl.cs.

77 return

Native.Z3_func_decl_to_string(

Context

.nCtx, NativeObject);

◆ Translate()

Translates (copies) the function declaration to the Context ctx .

Parameters

Returns: A copy of the function declaration which is associated with ctx

Definition at line 329 of file FuncDecl.cs.

331 return

(FuncDecl) base.Translate(ctx);

Referenced by FuncDecl.Translate().

◆ args

Create expression that applies function to arguments.

Parameters

Returns

Definition at line 340 of file FuncDecl.cs.

344

Debug.Assert(

args

null

args

.All(a => a !=

null

));

Expr Apply(params Expr[] args)

Create expression that applies function to arguments.

Referenced by FuncDecl.Apply().

◆ Arity ◆ DeclKind

The kind of the function declaration.

Definition at line 136 of file FuncDecl.cs.

Z3_decl_kind

The different kinds of interpreted function kinds.

◆ Domain

The domain of the function declaration

Definition at line 108 of file FuncDecl.cs.

115

Sort[] res =

new

Sort[n];

116 for

(uint i = 0; i < n; i++)

117

res[i] = Sort.Create(

Context

, Native.Z3_get_domain(

Context

.nCtx, NativeObject, i));

uint DomainSize

The size of the domain of the function declaration Arity

◆ DomainSize

The size of the domain of the function declaration

See also: Arity

Definition at line 100 of file FuncDecl.cs.

102 get

{

return

Native.Z3_get_domain_size(

Context

.nCtx, NativeObject); }

◆ Id

Returns a unique identifier for the function declaration.

Definition at line 83 of file FuncDecl.cs.

85 get

{

return

Native.Z3_get_func_decl_id(

Context

.nCtx, NativeObject); }

◆ Name

The name of the function declaration

Definition at line 144 of file FuncDecl.cs.

148 return

Symbol.Create(

Context

, Native.Z3_get_decl_name(

Context

.nCtx, NativeObject));

◆ NumParameters

The number of parameters of the function declaration

Definition at line 155 of file FuncDecl.cs.

157 get

{

return

Native.Z3_get_decl_num_parameters(

Context

.nCtx, NativeObject); }

◆ Parameters

The parameters of the function declaration

Definition at line 163 of file FuncDecl.cs.

169

Parameter[] res =

new

Parameter[num];

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));

182

res[i] =

new

Parameter(k, Symbol.Create(

Context

, Native.Z3_get_decl_symbol_parameter(

Context

.nCtx, NativeObject, i)));

185

res[i] =

new

Parameter(k, Sort.Create(

Context

, Native.Z3_get_decl_sort_parameter(

Context

.nCtx, NativeObject, i)));

188

res[i] =

new

Parameter(k,

new

AST(

Context

, Native.Z3_get_decl_ast_parameter(

Context

.nCtx, NativeObject, i)));

191

res[i] =

new

Parameter(k,

new

FuncDecl(

Context

, Native.Z3_get_decl_func_decl_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"

);

uint NumParameters

The number of parameters of the function declaration

Z3_parameter_kind

The different kinds of parameters that can be associated with function symbols.

◆ Range

The range of the function declaration

Definition at line 125 of file FuncDecl.cs.

129 return

Sort.Create(

Context

, Native.Z3_get_range(

Context

.nCtx, NativeObject));

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4