22 using System.Collections.Generic;
23 using System.Diagnostics.Contracts;
30 [ContractVerification(
true)]
40 public static bool operator ==(
AST a,
AST b)
42 return Object.ReferenceEquals(a, b) ||
43 (!Object.ReferenceEquals(a, null) &&
44 !Object.ReferenceEquals(b, null) &&
45 a.Context.nCtx == b.Context.nCtx &&
56 public static bool operator !=(
AST a,
AST b)
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)
117 Contract.Requires(ctx != null);
118 Contract.Ensures(Contract.Result<
AST>() != null);
120 if (ReferenceEquals(
Context, ctx))
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; }
205 Contract.Ensures(Contract.Result<
string>() != null);
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); }
214 internal class DecRefQueue : IDecRefQueue
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)
234 Context.AST_DRQ.IncAndClear(Context, o);
238 internal override void DecRef(IntPtr o)
241 if (Context == null || o == IntPtr.Zero)
243 Context.AST_DRQ.Add(o);
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))
254 case Z3_ast_kind.Z3_FUNC_DECL_AST:
return new FuncDecl(ctx, obj);
255 case Z3_ast_kind.Z3_QUANTIFIER_AST:
return new Quantifier(ctx, obj);
256 case Z3_ast_kind.Z3_SORT_AST:
return Sort.Create(ctx, obj);
259 case Z3_ast_kind.Z3_VAR_AST:
return Expr.Create(ctx, obj);
261 throw new Z3Exception(
"Unknown AST kind");
string SExpr()
A string representation of the AST in s-expression notation.
override string ToString()
A string representation of the AST.
AST Translate(Context ctx)
Translates (copies) the AST to the Context ctx .
uint Id
A unique identifier for the AST (unique among all ASTs).
static string Z3_ast_to_string(Z3_context a0, Z3_ast a1)
override int GetHashCode()
The AST's hash code.
static Z3_ast Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2)
static uint Z3_get_ast_id(Z3_context a0, Z3_ast a1)
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
static uint Z3_get_ast_hash(Z3_context a0, Z3_ast a1)
static int Z3_is_eq_ast(Z3_context a0, Z3_ast a1, Z3_ast a2)
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
The main interaction with Z3 happens via the Context.
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.