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); }
216 public DecRefQueue() : base() { }
217 public DecRefQueue(uint move_limit) : base(move_limit) { }
218 internal override void IncRef(
Context ctx, IntPtr obj)
223 internal override void DecRef(
Context ctx, IntPtr 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);
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 void Z3_dec_ref(Z3_context a0, Z3_ast a1)
static void Z3_inc_ref(Z3_context a0, Z3_ast a1)
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)
IDecRefQueue AST_DRQ
AST DRQ
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.
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.