Z3
Public Member Functions | Static Public Member Functions | Properties
AST Class Reference

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

+ Inheritance diagram for AST:

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...
 
- Properties inherited from Z3Object
Context Context [get]
 Access Context object 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)
inlinevirtual

Object Comparison.

Parameters
otherAnother 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  }
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  }
Context Context
Access Context object
Definition: Z3Object.cs:111

◆ operator!=()

static bool operator!= ( AST  a,
AST  b 
)
inlinestatic

Comparison operator.

Parameters
aAn AST
bAn 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 
)
inlinestatic

Comparison operator.

Parameters
aAn AST
bAn 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
ctxA 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
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:139

◆ 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  }
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  }