20using System.Diagnostics;
22using System.Collections;
23using System.Collections.Generic;
41 return Object.ReferenceEquals(a, b) ||
42 (!Object.ReferenceEquals(a,
null) &&
43 !Object.ReferenceEquals(b,
null) &&
44 a.Context.nCtx == b.Context.nCtx &&
45 0 != Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject));
63 public override bool Equals(
object o)
66 if (casted ==
null)
return false;
67 return this == casted;
77 if (other ==
null)
return 1;
85 else if (
Id > oAST.
Id)
98 return (
int)Native.Z3_get_ast_hash(
Context.nCtx, NativeObject);
106 get {
return Native.Z3_get_ast_id(
Context.nCtx, NativeObject); }
116 Debug.Assert(ctx !=
null);
118 if (ReferenceEquals(
Context, ctx))
121 return Create(ctx, Native.Z3_translate(
Context.nCtx, NativeObject, ctx.nCtx));
145 default:
return false;
195 return Native.Z3_ast_to_string(
Context.nCtx, NativeObject);
204 return Native.Z3_ast_to_string(
Context.nCtx, NativeObject);
208 internal AST(
Context ctx) : base(ctx) { Debug.Assert(ctx !=
null); }
209 internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx !=
null); }
211 internal class DecRefQueue : IDecRefQueue
213 public DecRefQueue() : base() { }
214 public DecRefQueue(uint move_limit) : base(move_limit) { }
215 internal override void IncRef(Context ctx, IntPtr obj)
217 Native.Z3_inc_ref(ctx.nCtx, obj);
220 internal override void DecRef(Context ctx, IntPtr obj)
222 Native.Z3_dec_ref(ctx.nCtx, obj);
226 internal override void IncRef(IntPtr o)
229 if (Context ==
null || o == IntPtr.Zero)
231 Context.
AST_DRQ.IncAndClear(Context, o);
235 internal override void DecRef(IntPtr o)
238 if (Context ==
null || o == IntPtr.Zero)
244 internal static AST Create(Context ctx, IntPtr obj)
246 Debug.Assert(ctx !=
null);
248 switch ((
Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj))
250 case Z3_ast_kind.Z3_FUNC_DECL_AST:
return new FuncDecl(ctx, obj);
251 case Z3_ast_kind.Z3_QUANTIFIER_AST:
return new Quantifier(ctx, obj);
252 case Z3_ast_kind.Z3_SORT_AST:
return Sort.Create(ctx, obj);
255 case Z3_ast_kind.Z3_VAR_AST:
return Expr.Create(ctx, obj);
257 throw new Z3Exception(
"Unknown AST kind");
The abstract syntax tree (AST) class.
override bool Equals(object o)
Object comparison.
static bool operator==(AST a, AST b)
Comparison operator.
virtual int CompareTo(object other)
Object Comparison.
bool IsFuncDecl
Indicates whether the AST is a FunctionDeclaration
static bool operator!=(AST a, AST b)
Comparison operator.
bool IsSort
Indicates whether the AST is a Sort
bool IsVar
Indicates whether the AST is a BoundVariable
Z3_ast_kind ASTKind
The kind of the AST.
override int GetHashCode()
The AST's hash code.
uint Id
A unique identifier for the AST (unique among all ASTs).
bool IsQuantifier
Indicates whether the AST is a Quantifier
override string ToString()
A string representation of the AST.
string SExpr()
A string representation of the AST in s-expression notation.
bool IsApp
Indicates whether the AST is an application
AST Translate(Context ctx)
Translates (copies) the AST to the Context ctx .
bool IsExpr
Indicates whether the AST is an Expr
The main interaction with Z3 happens via the Context.
IDecRefQueue AST_DRQ
AST DRQ
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.