00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00028 [ContractVerification(true)]
00029 public class Expr : AST
00030 {
00036 public Expr Simplify(Params p = null)
00037 {
00038 Contract.Ensures(Contract.Result<Expr>() != null);
00039
00040 if (p == null)
00041 return Expr.Create(Context, Native.Z3_simplify(Context.nCtx, NativeObject));
00042 else
00043 return Expr.Create(Context, Native.Z3_simplify_ex(Context.nCtx, NativeObject, p.NativeObject));
00044 }
00045
00049 public FuncDecl FuncDecl
00050 {
00051 get
00052 {
00053 Contract.Ensures(Contract.Result<FuncDecl>() != null);
00054 return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject));
00055 }
00056 }
00057
00062 public Z3_lbool BoolValue
00063 {
00064 get { return (Z3_lbool)Native.Z3_get_bool_value(Context.nCtx, NativeObject); }
00065 }
00066
00070 public uint NumArgs
00071 {
00072 get { return Native.Z3_get_app_num_args(Context.nCtx, NativeObject); }
00073 }
00074
00078 public Expr[] Args
00079 {
00080 get
00081 {
00082 Contract.Ensures(Contract.Result<Expr[]>() != null);
00083
00084 uint n = NumArgs;
00085 Expr[] res = new Expr[n];
00086 for (uint i = 0; i < n; i++)
00087 res[i] = Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
00088 return res;
00089 }
00090 }
00091
00096 public void Update(Expr[] args)
00097 {
00098 Contract.Requires(args != null);
00099 Contract.Requires(Contract.ForAll(args, a => a != null));
00100
00101 Context.CheckContextMatch(args);
00102 if (IsApp && args.Length != NumArgs)
00103 throw new Z3Exception("Number of arguments does not match");
00104 NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args));
00105 }
00106
00115 public Expr Substitute(Expr[] from, Expr[] to)
00116 {
00117 Contract.Requires(from != null);
00118 Contract.Requires(to != null);
00119 Contract.Requires(Contract.ForAll(from, f => f != null));
00120 Contract.Requires(Contract.ForAll(to, t => t != null));
00121 Contract.Ensures(Contract.Result<Expr>() != null);
00122
00123 Context.CheckContextMatch(from);
00124 Context.CheckContextMatch(to);
00125 if (from.Length != to.Length)
00126 throw new Z3Exception("Argument sizes do not match");
00127 return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to)));
00128 }
00129
00134 public Expr Substitute(Expr from, Expr to)
00135 {
00136 Contract.Requires(from != null);
00137 Contract.Requires(to != null);
00138 Contract.Ensures(Contract.Result<Expr>() != null);
00139
00140 return Substitute(new Expr[] { from }, new Expr[] { to });
00141 }
00142
00149 public Expr SubstituteVars(Expr[] to)
00150 {
00151 Contract.Requires(to != null);
00152 Contract.Requires(Contract.ForAll(to, t => t != null));
00153 Contract.Ensures(Contract.Result<Expr>() != null);
00154
00155 Context.CheckContextMatch(to);
00156 return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to)));
00157 }
00158
00164 new public Expr Translate(Context ctx)
00165 {
00166 Contract.Requires(ctx != null);
00167 Contract.Ensures(Contract.Result<Expr>() != null);
00168
00169 if (ReferenceEquals(Context, ctx))
00170 return this;
00171 else
00172 return Expr.Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
00173 }
00174
00178 public override string ToString()
00179 {
00180 return base.ToString();
00181 }
00182
00186 public bool IsNumeral
00187 {
00188 get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; }
00189 }
00190
00195 public bool IsWellSorted
00196 {
00197 get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; }
00198 }
00199
00203 public Sort Sort
00204 {
00205 get
00206 {
00207 Contract.Ensures(Contract.Result<Sort>() != null);
00208 return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject));
00209 }
00210 }
00211
00212 #region Constants
00213
00214
00215
00216 public bool IsConst
00217 {
00218 get { return IsApp && NumArgs == 0 && FuncDecl.DomainSize == 0; }
00219 }
00220 #endregion
00221
00222 #region Integer Numerals
00223
00224
00225
00226 public bool IsIntNum
00227 {
00228 get { return IsNumeral && IsInt; }
00229 }
00230 #endregion
00231
00232 #region Real Numerals
00233
00234
00235
00236 public bool IsRatNum
00237 {
00238 get { return IsNumeral && IsReal; }
00239 }
00240 #endregion
00241
00242 #region Algebraic Numbers
00243
00244
00245
00246 public bool IsAlgebraicNumber
00247 {
00248 get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject) != 0; }
00249 }
00250 #endregion
00251
00252 #region Term Kind Tests
00253
00254 #region Boolean Terms
00255
00256
00257
00258 public bool IsBool
00259 {
00260 get
00261 {
00262 return (IsExpr &&
00263 Native.Z3_is_eq_sort(Context.nCtx,
00264 Native.Z3_mk_bool_sort(Context.nCtx),
00265 Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0);
00266 }
00267 }
00268
00272 public bool IsTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } }
00273
00277 public bool IsFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } }
00278
00282 public bool IsEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } }
00283
00287 public bool IsDistinct { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } }
00288
00292 public bool IsITE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } }
00293
00297 public bool IsAnd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } }
00298
00302 public bool IsOr { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } }
00303
00307 public bool IsIff { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } }
00308
00312 public bool IsXor { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } }
00313
00317 public bool IsNot { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } }
00318
00322 public bool IsImplies { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
00323
00324 #endregion
00325
00326 #region Interpolation
00327
00328
00329
00330
00331 public bool IsInterpolant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INTERP; } }
00332 #endregion
00333
00334 #region Arithmetic Terms
00335
00336
00337
00338 public bool IsInt
00339 {
00340 get
00341 {
00342 return (Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0 &&
00343 Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_INT_SORT);
00344 }
00345 }
00346
00350 public bool IsReal
00351 {
00352 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_REAL_SORT; }
00353 }
00354
00358 public bool IsArithmeticNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } }
00359
00363 public bool IsLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } }
00364
00368 public bool IsGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } }
00369
00373 public bool IsLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } }
00374
00378 public bool IsGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } }
00379
00383 public bool IsAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } }
00384
00388 public bool IsSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } }
00389
00393 public bool IsUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } }
00394
00398 public bool IsMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } }
00399
00403 public bool IsDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } }
00404
00408 public bool IsIDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } }
00409
00413 public bool IsRemainder { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } }
00414
00418 public bool IsModulus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } }
00419
00423 public bool IsIntToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } }
00424
00428 public bool IsRealToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } }
00429
00433 public bool IsRealIsInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } }
00434 #endregion
00435
00436 #region Array Terms
00437
00438
00439
00440 public bool IsArray
00441 {
00442 get
00443 {
00444 return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
00445 (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
00446 == Z3_sort_kind.Z3_ARRAY_SORT);
00447 }
00448 }
00449
00455 public bool IsStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }
00456
00460 public bool IsSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } }
00461
00466 public bool IsConstantArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } }
00467
00472 public bool IsDefaultArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } }
00473
00478 public bool IsArrayMap { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } }
00479
00485 public bool IsAsArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }
00486 #endregion
00487
00488 #region Set Terms
00489
00490
00491
00492 public bool IsSetUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } }
00493
00497 public bool IsSetIntersect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } }
00498
00502 public bool IsSetDifference { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } }
00503
00507 public bool IsSetComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } }
00508
00512 public bool IsSetSubset { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } }
00513 #endregion
00514
00515 #region Bit-vector terms
00516
00517
00518
00519 public bool IsBV
00520 {
00521 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_BV_SORT; }
00522 }
00523
00527 public bool IsBVNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } }
00528
00532 public bool IsBVBitOne { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } }
00533
00537 public bool IsBVBitZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } }
00538
00542 public bool IsBVUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } }
00543
00547 public bool IsBVAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } }
00548
00552 public bool IsBVSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } }
00553
00557 public bool IsBVMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } }
00558
00562 public bool IsBVSDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } }
00563
00567 public bool IsBVUDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } }
00568
00572 public bool IsBVSRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } }
00573
00577 public bool IsBVURem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } }
00578
00582 public bool IsBVSMod { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } }
00583
00587 internal bool IsBVSDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } }
00588
00592 internal bool IsBVUDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } }
00593
00597 internal bool IsBVSRem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } }
00598
00602 internal bool IsBVURem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } }
00603
00607 internal bool IsBVSMod0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } }
00608
00612 public bool IsBVULE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } }
00613
00617 public bool IsBVSLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } }
00618
00622 public bool IsBVUGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } }
00623
00627 public bool IsBVSGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } }
00628
00632 public bool IsBVULT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } }
00633
00637 public bool IsBVSLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } }
00638
00642 public bool IsBVUGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } }
00643
00647 public bool IsBVSGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } }
00648
00652 public bool IsBVAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } }
00653
00657 public bool IsBVOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } }
00658
00662 public bool IsBVNOT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } }
00663
00667 public bool IsBVXOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } }
00668
00672 public bool IsBVNAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } }
00673
00677 public bool IsBVNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } }
00678
00682 public bool IsBVXNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } }
00683
00687 public bool IsBVConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } }
00688
00692 public bool IsBVSignExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } }
00693
00697 public bool IsBVZeroExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } }
00698
00702 public bool IsBVExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } }
00703
00707 public bool IsBVRepeat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } }
00708
00712 public bool IsBVReduceOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } }
00713
00717 public bool IsBVReduceAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } }
00718
00722 public bool IsBVComp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } }
00723
00727 public bool IsBVShiftLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } }
00728
00732 public bool IsBVShiftRightLogical { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } }
00733
00737 public bool IsBVShiftRightArithmetic { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } }
00738
00742 public bool IsBVRotateLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } }
00743
00747 public bool IsBVRotateRight { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } }
00748
00753 public bool IsBVRotateLeftExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } }
00754
00759 public bool IsBVRotateRightExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } }
00760
00766 public bool IsIntToBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }
00767
00773 public bool IsBVToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }
00774
00780 public bool IsBVCarry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }
00781
00786 public bool IsBVXOR3 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } }
00787
00788 #endregion
00789
00790 #region Labels
00791
00792
00793
00794
00795 public bool IsLabel { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }
00796
00801 public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
00802 #endregion
00803
00804 #region Proof Terms
00805
00806
00807
00808
00809
00810 public bool IsOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } }
00811
00815 public bool IsProofTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } }
00816
00820 public bool IsProofAsserted { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } }
00821
00825 public bool IsProofGoal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } }
00826
00836 public bool IsProofModusPonens { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } }
00837
00845 public bool IsProofReflexivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }
00846
00856 public bool IsProofSymmetry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } }
00857
00868 public bool IsProofTransitivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } }
00869
00889 public bool IsProofTransitivityStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } }
00890
00891
00903 public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
00904
00913 public bool IsProofQuantIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }
00914
00931 public bool IsProofDistributivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }
00932
00941 public bool IsProofAndElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
00942
00951 public bool IsProofOrElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }
00952
00970 public bool IsProofRewrite { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }
00971
00986 public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
00987
00994 public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
00995
01004 public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
01005
01017 public bool IsProofPushQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }
01018
01029 public bool IsProofElimUnusedVars { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } }
01030
01043 public bool IsProofDER { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }
01044
01051 public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
01052
01057 public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
01058
01070 public bool IsProofLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } }
01071
01082 public bool IsProofUnitResolution { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } }
01083
01091 public bool IsProofIFFTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } }
01092
01100 public bool IsProofIFFFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } }
01101
01113 public bool IsProofCommutativity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } }
01114
01149 public bool IsProofDefAxiom { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } }
01150
01172 public bool IsProofDefIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }
01173
01182 public bool IsProofApplyDef { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } }
01183
01191 public bool IsProofIFFOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } }
01192
01219 public bool IsProofNNFPos { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } }
01220
01244 public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
01245
01256 public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
01257
01266 public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
01267
01279 public bool IsProofSkolemize { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }
01280
01290 public bool IsProofModusPonensOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }
01291
01309 public bool IsProofTheoryLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } }
01310 #endregion
01311
01312 #region Relational Terms
01313
01314
01315
01316 public bool IsRelation
01317 {
01318 get
01319 {
01320 return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
01321 Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
01322 == (uint)Z3_sort_kind.Z3_RELATION_SORT);
01323 }
01324 }
01325
01334 public bool IsRelationStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }
01335
01339 public bool IsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } }
01340
01344 public bool IsIsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } }
01345
01349 public bool IsRelationalJoin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }
01350
01355 public bool IsRelationUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }
01356
01361 public bool IsRelationWiden { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } }
01362
01367 public bool IsRelationProject { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } }
01368
01379 public bool IsRelationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } }
01380
01395 public bool IsRelationNegationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } }
01396
01404 public bool IsRelationRename { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } }
01405
01409 public bool IsRelationComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } }
01410
01419 public bool IsRelationSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } }
01420
01431 public bool IsRelationClone { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }
01432 #endregion
01433
01434 #region Finite domain terms
01435
01436
01437
01438 public bool IsFiniteDomain
01439 {
01440 get
01441 {
01442 return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
01443 Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
01444 }
01445 }
01446
01450 public bool IsFiniteDomainLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }
01451 #endregion
01452 #endregion
01453
01454 #region Bound Variables
01455
01456
01457
01458
01459
01460
01461
01462
01463
01464
01465
01466
01467
01468
01469
01470
01471
01472
01473
01474 public uint Index
01475 {
01476 get
01477 {
01478 if (!IsVar)
01479 throw new Z3Exception("Term is not a bound variable.");
01480
01481 Contract.EndContractBlock();
01482
01483 return Native.Z3_get_index_value(Context.nCtx, NativeObject);
01484 }
01485 }
01486 #endregion
01487
01488 #region Internal
01489
01490
01491
01492 internal protected Expr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
01496 internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
01497
01498 #if DEBUG
01499 [Pure]
01500 internal override void CheckNativeObject(IntPtr obj)
01501 {
01502 if (Native.Z3_is_app(Context.nCtx, obj) == 0 &&
01503 Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_VAR_AST &&
01504 Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_QUANTIFIER_AST)
01505 throw new Z3Exception("Underlying object is not a term");
01506 base.CheckNativeObject(obj);
01507 }
01508 #endif
01509
01510 [Pure]
01511 internal static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments)
01512 {
01513 Contract.Requires(ctx != null);
01514 Contract.Requires(f != null);
01515 Contract.Ensures(Contract.Result<Expr>() != null);
01516
01517 IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
01518 AST.ArrayLength(arguments),
01519 AST.ArrayToNative(arguments));
01520 return Create(ctx, obj);
01521 }
01522
01523 [Pure]
01524 new internal static Expr Create(Context ctx, IntPtr obj)
01525 {
01526 Contract.Requires(ctx != null);
01527 Contract.Ensures(Contract.Result<Expr>() != null);
01528
01529 Z3_ast_kind k = (Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj);
01530 if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
01531 return new Quantifier(ctx, obj);
01532 IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
01533 Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s);
01534
01535 if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0)
01536 return new AlgebraicNum(ctx, obj);
01537
01538 if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
01539 {
01540 switch (sk)
01541 {
01542 case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
01543 case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
01544 case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
01545 }
01546 }
01547
01548 switch (sk)
01549 {
01550 case Z3_sort_kind.Z3_BOOL_SORT: return new BoolExpr(ctx, obj);
01551 case Z3_sort_kind.Z3_INT_SORT: return new IntExpr(ctx, obj);
01552 case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj);
01553 case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
01554 case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
01555 case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
01556 }
01557
01558 return new Expr(ctx, obj);
01559 }
01560 #endregion
01561 }
01562 }