22 using System.Collections.Generic;
42 return Object.ReferenceEquals(a, b) ||
43 (!Object.ReferenceEquals(a, null) &&
44 !Object.ReferenceEquals(b, null) &&
45 a.Context.nCtx == b.Context.nCtx &&
46 Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
64 public override bool Equals(
object o)
67 if (casted == null)
return false;
68 return this == casted;
78 if (other == null)
return 1;
86 else if (Id > oAST.
Id)
99 return (
int)Native.Z3_get_ast_hash(
Context.nCtx, NativeObject);
107 get {
return Native.Z3_get_ast_id(
Context.nCtx, NativeObject); }
117 Contract.Requires(ctx != null);
118 Contract.Ensures(Contract.Result<
AST>() != null);
120 if (ReferenceEquals(
Context, ctx))
123 return new AST(ctx, Native.Z3_translate(
Context.nCtx, NativeObject, ctx.nCtx));
147 default:
return false;
157 get {
return this.ASTKind ==
Z3_ast_kind.Z3_APP_AST; }
165 get {
return this.ASTKind ==
Z3_ast_kind.Z3_VAR_AST; }
171 public bool IsQuantifier
173 get {
return this.ASTKind ==
Z3_ast_kind.Z3_QUANTIFIER_AST; }
181 get {
return this.ASTKind ==
Z3_ast_kind.Z3_SORT_AST; }
187 public bool IsFuncDecl
189 get {
return this.ASTKind ==
Z3_ast_kind.Z3_FUNC_DECL_AST; }
197 return Native.Z3_ast_to_string(
Context.nCtx, NativeObject);
205 Contract.Ensures(Contract.Result<
string>() != null);
207 return Native.Z3_ast_to_string(
Context.nCtx, NativeObject);
211 internal AST(
Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
212 internal AST(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
216 public DecRefQueue() : base() { }
217 public DecRefQueue(uint move_limit) : base(move_limit) { }
218 internal override void IncRef(
Context ctx, IntPtr obj)
220 Native.Z3_inc_ref(ctx.nCtx, obj);
223 internal override void DecRef(
Context ctx, IntPtr obj)
225 Native.Z3_dec_ref(ctx.nCtx, obj);
229 internal override void IncRef(IntPtr o)
232 if (
Context == null || o == IntPtr.Zero)
238 internal override void DecRef(IntPtr o)
241 if (
Context == null || o == IntPtr.Zero)
247 internal static AST Create(
Context ctx, IntPtr obj)
249 Contract.Requires(ctx != null);
250 Contract.Ensures(Contract.Result<
AST>() != null);
252 switch ((
Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj))
string SExpr()
A string representation of the AST in s-expression notation.
override string ToString()
A string representation of the AST.
expr operator!=(expr const &a, expr const &b)
AST Translate(Context ctx)
Translates (copies) the AST to the Context ctx .
uint Id
A unique identifier for the AST (unique among all ASTs).
override int GetHashCode()
The AST's hash code.
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
IDecRefQueue AST_DRQ
AST DRQ
expr operator==(expr const &a, expr const &b)
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
The exception base class for error reporting from Z3
override bool Equals(object o)
Object comparison.
The abstract syntax tree (AST) class.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
virtual int CompareTo(object other)
Object Comparison.