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.
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.
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object.

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	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 )

inlinevirtual

Object Comparison.

Parameters

other

Another AST

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.

Definition at line 64 of file AST.cs.

        {
            AST casted = o as AST;
            if (casted == null) return false;
            return this == casted;
        }

override int GetHashCode ( )

inline

The AST's hash code.

Returns

A hash code

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  )

inlinestatic

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 56 of file AST.cs.

        {
            return !(a == b);
        }

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

inlinestatic

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 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 195 of file AST.cs.

        {
            Contract.Ensures(Contract.Result<string>() != null);

            return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
        }

override string ToString ( )

inline

A string representation of the AST.

Definition at line 187 of file AST.cs.

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

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

Z3_ast_kind ASTKind

get

The kind of the AST.

Definition at line 130 of file AST.cs.

uint Id

get

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

Definition at line 106 of file AST.cs.

Referenced by AST.CompareTo().

bool IsExpr

get

Indicates whether the AST is an Expr

Definition at line 138 of file AST.cs.

bool IsFuncDecl

get

Indicates whether the AST is a FunctionDeclaration

Definition at line 180 of file AST.cs.

bool IsQuantifier

get

Indicates whether the AST is a Quantifier

Definition at line 164 of file AST.cs.

bool IsSort

get

Indicates whether the AST is a Sort

Definition at line 172 of file AST.cs.

bool IsVar

get

Indicates whether the AST is a BoundVariable

Definition at line 156 of file AST.cs.