AST Class Reference

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

Inheritance diagram for AST:

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

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

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.

        {
            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;
            }
        }

Equals()

override bool Equals ( object  o )

inline

Object comparison.

Definition at line 63 of file AST.cs.

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

GetHashCode()

override int GetHashCode ( )

inline

The AST's hash code.

Returns

A hash code

Definition at line 96 of file AST.cs.

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

operator!=()

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

        {
            return !(a == b);
        }

operator==()

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

        {
            return Object.ReferenceEquals(a, b) ||
                   (!Object.ReferenceEquals(a, null) &&
                    !Object.ReferenceEquals(b, null) &&
                    a.Context.nCtx == b.Context.nCtx &&
                    0 != Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject));
        }

SExpr()

string SExpr ( )

inline

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

Definition at line 201 of file AST.cs.

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

ToString()

override string ToString ( )

inline

A string representation of the AST.

Definition at line 193 of file AST.cs.

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

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.

        {
            Debug.Assert(ctx != null);
 
            if (ReferenceEquals(Context, ctx))
                return this;
            else
                return Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
        }

Property Documentation

ASTKind

Z3_ast_kind ASTKind

get

The kind of the AST.

Definition at line 127 of file AST.cs.

        {
            get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); }
        }

Id

uint Id

get

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

Definition at line 104 of file AST.cs.

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

Referenced by AST.CompareTo().

IsApp

bool IsApp

get

Indicates whether the AST is an application.

Definition at line 153 of file AST.cs.

        {
            get { return this.ASTKind == Z3_ast_kind.Z3_APP_AST; }
        }

Referenced by Expr.Update().

IsExpr

bool IsExpr

get

Indicates whether the AST is an Expr.

Definition at line 135 of file AST.cs.

        {
            get
            {
                switch (ASTKind)
                {
                    case Z3_ast_kind.Z3_APP_AST:
                    case Z3_ast_kind.Z3_NUMERAL_AST:
                    case Z3_ast_kind.Z3_QUANTIFIER_AST:
                    case Z3_ast_kind.Z3_VAR_AST: return true;
                    default: return false;
                }
            }
        }

IsFuncDecl

bool IsFuncDecl

get

Indicates whether the AST is a FunctionDeclaration.

Definition at line 185 of file AST.cs.

        {
            get { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; }
        }

IsQuantifier

bool IsQuantifier

get

Indicates whether the AST is a Quantifier.

Definition at line 169 of file AST.cs.

        {
            get { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; }
        }

IsSort

bool IsSort

get

Indicates whether the AST is a Sort.

Definition at line 177 of file AST.cs.

        {
            get { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; }
        }

IsVar

bool IsVar

get

Indicates whether the AST is a BoundVariable.

Definition at line 161 of file AST.cs.

        {
            get { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; }
        }