The abstract syntax tree (AST) class.
More...
Data Structures |
class | DecRefQueue |
Public Member Functions |
override bool | Equals (object o) |
| Object comparison.
|
virtual int | CompareTo (object other) |
| Object Comparison.
|
override int | GetHashCode () |
| The AST's hash code.
|
AST | Translate (Context ctx) |
| Translates (copies) the AST to the Context ctx .
|
override string | ToString () |
| A string representation of the AST.
|
string | SExpr () |
| A string representation of the AST in s-expression notation.
|
Static Public Member Functions |
static bool | operator== (AST a, AST b) |
| Comparison operator.
|
static bool | operator!= (AST a, AST b) |
| Comparison operator.
|
Properties |
uint | Id [get] |
| A unique identifier for the AST (unique among all ASTs).
|
Z3_ast_kind | ASTKind [get] |
| The kind of the AST.
|
bool | IsExpr [get] |
| Indicates whether the AST is an Expr.
|
bool | IsApp [get] |
| Indicates whether the AST is an application.
|
bool | IsVar [get] |
| Indicates whether the AST is a BoundVariable.
|
bool | IsQuantifier [get] |
| Indicates whether the AST is a Quantifier.
|
bool | IsSort [get] |
| Indicates whether the AST is a Sort.
|
bool | IsFuncDecl [get] |
| Indicates whether the AST is a FunctionDeclaration.
|
Detailed Description
The abstract syntax tree (AST) class.
Definition at line 31 of file AST.cs.
Member Function Documentation
virtual int CompareTo |
( |
object |
other | ) |
[inline, virtual] |
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.
{
if (other == null) return 1;
AST oAST = other as AST;
if (oAST == null)
return 1;
else
{
if (Id < oAST.Id)
return -1;
else if (Id > oAST.Id)
return +1;
else
return 0;
}
}
override bool Equals |
( |
object |
o | ) |
[inline] |
Object comparison.
Reimplemented in Sort, and FuncDecl.
Definition at line 64 of file AST.cs.
{
AST casted = o as AST;
if (casted == null) return false;
return this == casted;
}
The AST's hash code.
- Returns:
- A hash code
Reimplemented in Sort, and FuncDecl.
Definition at line 97 of file AST.cs.
{
return (int)Native.Z3_get_ast_hash(Context.nCtx, NativeObject);
}
static bool operator!= |
( |
AST |
a, |
|
|
AST |
b |
|
) |
| [inline, static] |
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 |
|
) |
| [inline, static] |
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.
{
return Object.ReferenceEquals(a, b) ||
(!Object.ReferenceEquals(a, null) &&
!Object.ReferenceEquals(b, null) &&
a.Context.nCtx == b.Context.nCtx &&
Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
}
string SExpr |
( |
| ) |
[inline] |
A string representation of the AST in s-expression notation.
Definition at line 203 of file AST.cs.
{
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
}
A string representation of the AST.
Reimplemented in Expr, Sort, FuncDecl, and Pattern.
Definition at line 195 of file AST.cs.
{
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
Reimplemented in Expr.
Definition at line 115 of file AST.cs.
{
Contract.Requires(ctx != null);
Contract.Ensures(Contract.Result<AST>() != null);
if (ReferenceEquals(Context, ctx))
return this;
else
return new AST(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
}
Property Documentation
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.