Pattern Class Reference

Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern. More...

Inheritance diagram for Pattern:

Public Member Functions
override string	ToString ()
	A string representation of the pattern. More...
Public Member Functions inherited from AST
override bool	Equals (object o)
	Object comparison. More...
virtual int	CompareTo (object other)
	Object Comparison. More...
override int	GetHashCode ()
	The AST's hash code. More...
AST	Translate (Context ctx)
	Translates (copies) the AST to the Context ctx . More...
override string	ToString ()
	A string representation of the AST. More...
string	SExpr ()
	A string representation of the AST in s-expression notation. More...
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object. More...

Properties
uint	NumTerms [get]
	The number of terms in the pattern. More...
Expr[]	Terms [get]
	The terms in the pattern. More...
Properties inherited from AST
uint	Id [get]
	A unique identifier for the AST (unique among all ASTs). More...
Z3_ast_kind	ASTKind [get]
	The kind of the AST. More...
bool	IsExpr [get]
	Indicates whether the AST is an Expr More...
bool	IsApp [get]
	Indicates whether the AST is an application More...
bool	IsVar [get]
	Indicates whether the AST is a BoundVariable More...
bool	IsQuantifier [get]
	Indicates whether the AST is a Quantifier More...
bool	IsSort [get]
	Indicates whether the AST is a Sort More...
bool	IsFuncDecl [get]
	Indicates whether the AST is a FunctionDeclaration More...
Properties inherited from Z3Object
Context	Context [get]
	Access Context object More...

Additional Inherited Members
Static Public Member Functions inherited from AST
static bool	operator== (AST a, AST b)
	Comparison operator. More...
static bool	operator!= (AST a, AST b)
	Comparison operator. More...

Detailed Description

Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern.

Definition at line 31 of file Pattern.cs.

Member Function Documentation

ToString()

override string ToString ( )

inline

A string representation of the pattern.

Definition at line 60 of file Pattern.cs.

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

Property Documentation

NumTerms

uint NumTerms

get

The number of terms in the pattern.

Definition at line 36 of file Pattern.cs.

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

Terms

Expr [] Terms

get

The terms in the pattern.

Definition at line 44 of file Pattern.cs.

        {
            get
            {
 
                uint n = NumTerms;
                Expr[] res = new Expr[n];
                for (uint i = 0; i < n; i++)
                    res[i] = Expr.Create(Context, Native.Z3_get_pattern(Context.nCtx, NativeObject, i));
                return res;
            }
        }