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_sort.html below:

Z3: Sort Class Reference

The Sort class implements type information for ASTs. More...

The Sort class implements type information for ASTs.

Definition at line 28 of file Sort.cs.

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

Equality operator for objects of type Sort.

Parameters

Returns

Definition at line 63 of file Sort.cs.

65

Sort casted = o as Sort;

66 if

(casted ==

null

)

return false

;

67 return this

== casted;

◆ GetHashCode() override int GetHashCode ( ) inline

Hash code generation for Sorts

Returns: A hash code

Definition at line 74 of file Sort.cs.

76 return

base.GetHashCode();

◆ operator!=() static bool operator!= ( Sort a, Sort b ) inlinestatic

Comparison operator.

Parameters

Returns: True if a and b are not from the same context or represent different sorts; false otherwise.

Definition at line 53 of file Sort.cs.

◆ operator==() static bool operator== ( Sort a, Sort b ) inlinestatic

Comparison operator.

Parameters

Returns: True if a and b are from the same context and represent the same sort; false otherwise.

Definition at line 37 of file Sort.cs.

39 return

Object.ReferenceEquals(a, b) ||

40

(!Object.ReferenceEquals(a,

null

) &&

41

!Object.ReferenceEquals(b,

null

) &&

42

a.Context == b.Context &&

43

0 != Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject));

◆ ToString() override string ToString ( ) inline

A string representation of the sort.

Definition at line 109 of file Sort.cs.

111 return

Native.Z3_sort_to_string(

Context

.nCtx, NativeObject);

Context Context

Access Context object

◆ Translate()

Translates (copies) the sort to the Context ctx .

Parameters

Returns: A copy of the sort which is associated with ctx

Definition at line 119 of file Sort.cs.

121 return

(Sort)base.Translate(ctx);

Referenced by Sort.Translate().

◆ Id

Returns a unique identifier for the sort.

Definition at line 82 of file Sort.cs.

84 get

{

return

Native.Z3_get_sort_id(

Context

.nCtx, NativeObject); }

◆ Name

The name of the sort

Definition at line 98 of file Sort.cs.

102 return

Symbol.Create(

Context

, Native.Z3_get_sort_name(

Context

.nCtx, NativeObject));

◆ SortKind

The kind of the sort.

Definition at line 90 of file Sort.cs.

Z3_sort_kind

The different kinds of Z3 types (See Z3_get_sort_kind).

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