Z3
src/api/dotnet/Expr.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (<c>) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Expr.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Expressions
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-20
00015 
00016 Notes:
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) // is this a numeral ast?
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines