The abstract syntax tree (AST) class.
More...
The abstract syntax tree (AST) class.
Definition at line 31 of file AST.cs.
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 76 of file AST.cs.
78 if (other == null)
return 1;
79 AST oAST = other as AST;
86 else if (
Id > oAST.Id)
uint Id
A unique identifier for the AST (unique among all ASTs).
override bool Equals |
( |
object |
o | ) |
|
|
inline |
Object comparison.
Definition at line 64 of file AST.cs.
66 AST casted = o as AST;
67 if (casted == null)
return false;
68 return this == casted;
override int GetHashCode |
( |
| ) |
|
|
inline |
The AST's hash code.
- Returns
- A hash code
Definition at line 97 of file AST.cs.
99 return (
int)Native.Z3_get_ast_hash(Context.nCtx, NativeObject);
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 56 of file AST.cs.
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 40 of file AST.cs.
42 return Object.ReferenceEquals(a, b) ||
43 (!Object.ReferenceEquals(a, null) &&
44 !Object.ReferenceEquals(b, null) &&
45 a.Context.nCtx == b.Context.nCtx &&
46 Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
A string representation of the AST in s-expression notation.
Definition at line 203 of file AST.cs.
205 Contract.Ensures(Contract.Result<
string>() != null);
207 return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
override string ToString |
( |
| ) |
|
|
inline |
A string representation of the AST.
Definition at line 195 of file AST.cs.
197 return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
Translates (copies) the AST to the Context ctx .
- Parameters
-
- Returns
- A copy of the AST which is associated with ctx
Definition at line 115 of file AST.cs.
117 Contract.Requires(ctx != null);
118 Contract.Ensures(Contract.Result<AST>() != null);
120 if (ReferenceEquals(Context, ctx))
123 return new AST(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
Indicates whether the AST is an application
Definition at line 156 of file AST.cs.
Indicates whether the AST is a FunctionDeclaration
Definition at line 188 of file AST.cs.
Indicates whether the AST is a BoundVariable
Definition at line 164 of file AST.cs.