Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Data Structures | Public Member Functions | Static Public Member Functions | Properties
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.

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:
otherAnother 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.

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;
        }
override int GetHashCode ( ) [inline]

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

        {
            return !(a == b);
        }
static bool operator== ( AST  a,
AST  b 
) [inline, static]

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 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);
        }
override string ToString ( ) [inline]

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

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

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

Reimplemented in Sort, and FuncDecl.

Definition at line 106 of file AST.cs.

Referenced by AST.CompareTo().

bool IsApp [get]

Indicates whether the AST is an application.

Definition at line 156 of file AST.cs.

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

bool IsQuantifier [get]

Indicates whether the AST is a Quantifier.

Definition at line 172 of file AST.cs.

bool IsSort [get]

Indicates whether the AST is a Sort.

Definition at line 180 of file AST.cs.

bool IsVar [get]

Indicates whether the AST is a BoundVariable.

Definition at line 164 of file AST.cs.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines