Z3 |

Data Structures | Public Member Functions | Static Public Member Functions | Properties
AST Class Reference

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

Inheritance diagram for AST:

## Data Structures
class | DecRefQueue

## Public Member Functions
override bool | Equals (object o)
| Object comparison. More...
virtual int | CompareTo (object other)
| Object Comparison. More...
override int | GetHashCode ()
| The AST's hash code. More...
AST | Translate (Context ctx)
| Translates (copies) the AST to the Context ctx . More...
override string | ToString ()
| A string representation of the AST. More...
string | SExpr ()
| A string representation of the AST in s-expression notation. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Static Public Member Functions
static bool | operator== (AST a, AST b)
| Comparison operator. More...
static bool | operator!= (AST a, AST b)
| Comparison operator. More...

## Properties
uint | Id`[get]`
| A unique identifier for the AST (unique among all ASTs). More...
Z3_ast_kind | ASTKind`[get]`
| The kind of the AST. More...
bool | IsExpr`[get]`
| Indicates whether the AST is an Expr More...
bool | IsApp`[get]`
| Indicates whether the AST is an application More...
bool | IsVar`[get]`
| Indicates whether the AST is a BoundVariable More...
bool | IsQuantifier`[get]`
| Indicates whether the AST is a Quantifier More...
bool | IsSort`[get]`
| Indicates whether the AST is a Sort More...
bool | IsFuncDecl`[get]`
| Indicates whether the AST is a FunctionDeclaration More...

## Detailed Description

The abstract syntax tree (AST) class.

Definition at line 30 of file AST.cs.

## Member Function Documentation

## ◆ CompareTo()

virtual int CompareTo | ( | object | other | ) |
| inline virtual

Object Comparison.

Parameters

  other | Another AST

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

Definition at line 75 of file AST.cs.

76 {
77 if (other == null) return 1;
78 AST oAST = other as AST;
79 if (oAST == null)
80 return 1;
81 else
82 {
83 if (Id < oAST.Id)
84 return -1;
85 else if (Id > oAST.Id)
86 return +1;
87 else
88 return 0;
89 }
90 }
Microsoft.Z3.AST.Id
uint Id
A unique identifier for the AST (unique among all ASTs).
Definition: AST.cs:105

## ◆ Equals()

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

Object comparison.

Definition at line 63 of file AST.cs.

64 {
65 AST casted = o as AST;
66 if (casted == null) return false;
67 return this == casted;
68 }

## ◆ GetHashCode()

override int GetHashCode | ( |  | ) |
| inline

The AST's hash code.

Returns
  A hash code

Definition at line 96 of file AST.cs.

97 {
98 return (int)Native.Z3_get_ast_hash(Context.nCtx, NativeObject);
99 }

## ◆ operator!=()

static bool operator!= | ( | AST | a,
|  | AST | b
| ) |  |
| inline static

Comparison operator.

Parameters

  a | An AST
  b | An AST

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.

56 {
57 return !(a == b);
58 }

## ◆ operator==()

static bool operator== | ( | AST | a,
|  | AST | b
| ) |  |
| inline static

Comparison operator.

Parameters

  a | An AST
  b | An AST

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.

40 {
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));
46 }

## ◆ SExpr()

string SExpr | ( |  | ) |
| inline

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

Definition at line 201 of file AST.cs.

202 {
203
204 return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
205 }

## ◆ ToString()

override string ToString | ( |  | ) |
| inline

A string representation of the AST.

Definition at line 193 of file AST.cs.

194 {
195 return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
196 }

## ◆ Translate()

AST Translate | ( | Context | ctx | ) |
| inline

Translates (copies) the AST to the Context ctx .

Parameters

  ctx | A context

Returns
  A copy of the AST which is associated with ctx

Definition at line 114 of file AST.cs.

115 {
116 Debug.Assert(ctx != null);
117
118 if (ReferenceEquals(Context, ctx))
119 return this;
120 else
121 return Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
122 }

## Property Documentation

## ◆ ASTKind

Z3_ast_kind ASTKind
| get

The kind of the AST.

Definition at line 127 of file AST.cs.

128 {
129 get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); }
130 }
Z3_ast_kind
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180

## ◆ Id

uint Id
| get

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

Definition at line 104 of file AST.cs.

105 {
106 get { return Native.Z3_get_ast_id(Context.nCtx, NativeObject); }
107 }

Referenced by AST.CompareTo().

## ◆ IsApp

bool IsApp
| get

Indicates whether the AST is an application

Definition at line 153 of file AST.cs.

154 {
155 get { return this.ASTKind == Z3_ast_kind.Z3_APP_AST; }
156 }
Microsoft.Z3.AST.ASTKind
Z3_ast_kind ASTKind
The kind of the AST.
Definition: AST.cs:128

Referenced by Expr.Update().

## ◆ IsExpr

bool IsExpr
| get

Indicates whether the AST is an Expr

Definition at line 135 of file AST.cs.

136 {
137 get
138 {
139 switch (ASTKind)
140 {
141 case Z3_ast_kind.Z3_APP_AST:
142 case Z3_ast_kind.Z3_NUMERAL_AST:
143 case Z3_ast_kind.Z3_QUANTIFIER_AST:
144 case Z3_ast_kind.Z3_VAR_AST: return true;
145 default: return false;
146 }
147 }
148 }

## ◆ IsFuncDecl

bool IsFuncDecl
| get

Indicates whether the AST is a FunctionDeclaration

Definition at line 185 of file AST.cs.

186 {
187 get { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; }
188 }

## ◆ IsQuantifier

bool IsQuantifier
| get

Indicates whether the AST is a Quantifier

Definition at line 169 of file AST.cs.

170 {
171 get { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; }
172 }

## ◆ IsSort

bool IsSort
| get

Indicates whether the AST is a Sort

Definition at line 177 of file AST.cs.

178 {
179 get { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; }
180 }

## ◆ IsVar

bool IsVar
| get

Indicates whether the AST is a BoundVariable

Definition at line 161 of file AST.cs.

162 {
163 get { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; }
164 }