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 override void IncRef(Context ctx, IntPtr obj)
218 Native.Z3_inc_ref(ctx.nCtx, obj);
221 public override void DecRef(Context ctx, IntPtr obj)
223 Native.Z3_dec_ref(ctx.nCtx, obj);
227 internal override void IncRef(IntPtr o)
231 throw new Z3Exception(
"inc() called on null context");
232 if (o == IntPtr.Zero)
233 throw new Z3Exception(
"inc() called on null AST");
234 Context.AST_DRQ.IncAndClear(Context, o);
238 internal override void DecRef(IntPtr o)
242 throw new Z3Exception(
"dec() called on null context");
243 if (o == IntPtr.Zero)
244 throw new Z3Exception(
"dec() called on null AST");
245 Context.AST_DRQ.Add(o);
249 internal static AST Create(Context ctx, IntPtr obj)
251 Contract.Requires(ctx != null);
252 Contract.Ensures(Contract.Result<AST>() != null);
254 switch ((
Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj))
256 case Z3_ast_kind.Z3_FUNC_DECL_AST:
return new FuncDecl(ctx, obj);
257 case Z3_ast_kind.Z3_QUANTIFIER_AST:
return new Quantifier(ctx, obj);
258 case Z3_ast_kind.Z3_SORT_AST:
return Sort.Create(ctx, obj);
261 case Z3_ast_kind.Z3_VAR_AST:
return Expr.Create(ctx, obj);
263 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.