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

Z3: AST Class Reference

The abstract syntax tree (AST) class. More...

The abstract syntax tree (AST) class.

Definition at line 30 of file AST.cs.

◆ CompareTo() virtual int CompareTo ( object other ) inlinevirtual

Object Comparison.

Parameters

Returns: Negative if the object should be sorted before other , positive if after else zero.

Definition at line 75 of file AST.cs.

77 if

(other ==

null

)

return

78

AST oAST = other as AST;

85 else if

(

> oAST.Id)

uint Id

A unique identifier for the AST (unique among all ASTs).

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

Object comparison.

Definition at line 63 of file AST.cs.

65

AST casted = o as AST;

66 if

(casted ==

null

)

return false

;

67 return this

== casted;

◆ GetHashCode() override int GetHashCode ( ) inline

The AST's hash code.

Returns: A hash code

Definition at line 96 of file AST.cs.

98 return

(

int

)Native.Z3_get_ast_hash(

Context

.nCtx, NativeObject);

Context Context

Access Context object

◆ operator!=() static bool operator!= ( AST a, AST 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 55 of file AST.cs.

◆ operator==() static bool operator== ( AST a, AST 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 39 of file AST.cs.

41 return

Object.ReferenceEquals(a, b) ||

42

(!Object.ReferenceEquals(a,

null

) &&

43

!Object.ReferenceEquals(b,

null

) &&

44

a.Context.nCtx == b.Context.nCtx &&

45

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

◆ SExpr()

A string representation of the AST in s-expression notation.

Definition at line 201 of file AST.cs.

204 return

Native.Z3_ast_to_string(

Context

.nCtx, NativeObject);

◆ ToString() override string ToString ( ) inline

A string representation of the AST.

Definition at line 193 of file AST.cs.

195 return

Native.Z3_ast_to_string(

Context

.nCtx, NativeObject);

◆ Translate()

Translates (copies) the AST to the Context ctx .

Parameters

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

Definition at line 114 of file AST.cs.

116

Debug.Assert(ctx !=

null

);

118 if

(ReferenceEquals(

Context

, ctx))

121 return

Create(ctx, Native.Z3_translate(

Context

.nCtx, NativeObject, ctx.nCtx));

◆ ASTKind

The kind of the AST.

Definition at line 127 of file AST.cs.

Z3_ast_kind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

◆ Id

A unique identifier for the AST (unique among all ASTs).

Definition at line 104 of file AST.cs.

106 get

{

return

Native.Z3_get_ast_id(

Context

.nCtx, NativeObject); }

Referenced by AST.CompareTo().

◆ IsApp

Indicates whether the AST is an application

Definition at line 153 of file AST.cs.

Z3_ast_kind ASTKind

The kind of the AST.

Referenced by Expr.Update().

◆ IsExpr

Indicates whether the AST is an Expr

Definition at line 135 of file AST.cs.

145 default

return false

;

◆ IsFuncDecl

Indicates whether the AST is a FunctionDeclaration

Definition at line 185 of file AST.cs.

◆ IsQuantifier ◆ IsSort ◆ IsVar

Indicates whether the AST is a BoundVariable

Definition at line 161 of file AST.cs.

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