00001
00018 package com.microsoft.z3;
00019
00020 import com.microsoft.z3.enumerations.Z3_ast_kind;
00021 import com.microsoft.z3.enumerations.Z3_decl_kind;
00022 import com.microsoft.z3.enumerations.Z3_lbool;
00023 import com.microsoft.z3.enumerations.Z3_sort_kind;
00024
00025
00026
00030 public class Expr extends AST
00031 {
00035 public Expr simplify() throws Z3Exception
00036 {
00037 return simplify(null);
00038 }
00039
00046 public Expr simplify(Params p) throws Z3Exception
00047 {
00048
00049 if (p == null)
00050 return Expr.create(getContext(),
00051 Native.simplify(getContext().nCtx(), getNativeObject()));
00052 else
00053 return Expr.create(
00054 getContext(),
00055 Native.simplifyEx(getContext().nCtx(), getNativeObject(),
00056 p.getNativeObject()));
00057 }
00058
00063 public FuncDecl getFuncDecl() throws Z3Exception
00064 {
00065 return new FuncDecl(getContext(), Native.getAppDecl(getContext().nCtx(),
00066 getNativeObject()));
00067 }
00068
00073 public Z3_lbool getBoolValue() throws Z3Exception
00074 {
00075 return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
00076 getNativeObject()));
00077 }
00078
00082 public int getNumArgs() throws Z3Exception
00083 {
00084 return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
00085 }
00086
00090 public Expr[] getArgs() throws Z3Exception
00091 {
00092 int n = getNumArgs();
00093 Expr[] res = new Expr[n];
00094 for (int i = 0; i < n; i++)
00095 res[i] = Expr.create(getContext(),
00096 Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
00097 return res;
00098 }
00099
00105 public void update(Expr[] args) throws Z3Exception
00106 {
00107 getContext().checkContextMatch(args);
00108 if (isApp() && args.length != getNumArgs())
00109 throw new Z3Exception("Number of arguments does not match");
00110 setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(),
00111 (int) args.length, Expr.arrayToNative(args)));
00112 }
00113
00123 public Expr substitute(Expr[] from, Expr[] to) throws Z3Exception
00124 {
00125 getContext().checkContextMatch(from);
00126 getContext().checkContextMatch(to);
00127 if (from.length != to.length)
00128 throw new Z3Exception("Argument sizes do not match");
00129 return Expr.create(getContext(), Native.substitute(getContext().nCtx(),
00130 getNativeObject(), (int) from.length, Expr.arrayToNative(from),
00131 Expr.arrayToNative(to)));
00132 }
00133
00138 public Expr substitute(Expr from, Expr to) throws Z3Exception
00139 {
00140
00141 return substitute(new Expr[] { from }, new Expr[] { to });
00142 }
00143
00150 public Expr substituteVars(Expr[] to) throws Z3Exception
00151 {
00152
00153 getContext().checkContextMatch(to);
00154 return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
00155 getNativeObject(), (int) to.length, Expr.arrayToNative(to)));
00156 }
00157
00165 public Expr translate(Context ctx) throws Z3Exception
00166 {
00167
00168 if (getContext() == ctx)
00169 return this;
00170 else
00171 return Expr.create(
00172 ctx,
00173 Native.translate(getContext().nCtx(), getNativeObject(),
00174 ctx.nCtx()));
00175 }
00176
00180 public String toString()
00181 {
00182 return super.toString();
00183 }
00184
00188 public boolean isNumeral() throws Z3Exception
00189 {
00190 return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
00191 }
00192
00198 public boolean isWellSorted() throws Z3Exception
00199 {
00200 return Native.isWellSorted(getContext().nCtx(), getNativeObject());
00201 }
00202
00206 public Sort getSort() throws Z3Exception
00207 {
00208 return Sort.create(getContext(),
00209 Native.getSort(getContext().nCtx(), getNativeObject()));
00210 }
00211
00215 public boolean isConst() throws Z3Exception
00216 {
00217 return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
00218 }
00219
00223 public boolean isIntNum() throws Z3Exception
00224 {
00225 return isNumeral() && isInt();
00226 }
00227
00231 public boolean isRatNum() throws Z3Exception
00232 {
00233 return isNumeral() && isReal();
00234 }
00235
00239 public boolean isAlgebraicNumber() throws Z3Exception
00240 {
00241 return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
00242 }
00243
00247 public boolean isBool() throws Z3Exception
00248 {
00249 return (isExpr() && Native.isEqSort(getContext().nCtx(),
00250 Native.mkBoolSort(getContext().nCtx()),
00251 Native.getSort(getContext().nCtx(), getNativeObject())));
00252 }
00253
00257 public boolean isTrue() throws Z3Exception
00258 {
00259 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TRUE;
00260 }
00261
00265 public boolean isFalse() throws Z3Exception
00266 {
00267 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FALSE;
00268 }
00269
00273 public boolean isEq() throws Z3Exception
00274 {
00275 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EQ;
00276 }
00277
00282 public boolean isDistinct() throws Z3Exception
00283 {
00284 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DISTINCT;
00285 }
00286
00290 public boolean isITE() throws Z3Exception
00291 {
00292 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ITE;
00293 }
00294
00298 public boolean isAnd() throws Z3Exception
00299 {
00300 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AND;
00301 }
00302
00306 public boolean isOr() throws Z3Exception
00307 {
00308 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OR;
00309 }
00310
00315 public boolean isIff() throws Z3Exception
00316 {
00317 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IFF;
00318 }
00319
00323 public boolean isXor() throws Z3Exception
00324 {
00325 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR;
00326 }
00327
00331 public boolean isNot() throws Z3Exception
00332 {
00333 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_NOT;
00334 }
00335
00339 public boolean isImplies() throws Z3Exception
00340 {
00341 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IMPLIES;
00342 }
00343
00347 public boolean isInt() throws Z3Exception
00348 {
00349 return (Native.isNumeralAst(getContext().nCtx(), getNativeObject()) && Native
00350 .getSortKind(getContext().nCtx(),
00351 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT
00352 .toInt());
00353 }
00354
00358 public boolean isReal() throws Z3Exception
00359 {
00360 return Native.getSortKind(getContext().nCtx(),
00361 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT
00362 .toInt();
00363 }
00364
00368 public boolean isArithmeticNumeral() throws Z3Exception
00369 {
00370 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ANUM;
00371 }
00372
00376 public boolean isLE() throws Z3Exception
00377 {
00378 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LE;
00379 }
00380
00384 public boolean isGE() throws Z3Exception
00385 {
00386 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GE;
00387 }
00388
00392 public boolean isLT() throws Z3Exception
00393 {
00394 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LT;
00395 }
00396
00400 public boolean isGT() throws Z3Exception
00401 {
00402 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_GT;
00403 }
00404
00408 public boolean isAdd() throws Z3Exception
00409 {
00410 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ADD;
00411 }
00412
00416 public boolean isSub() throws Z3Exception
00417 {
00418 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SUB;
00419 }
00420
00424 public boolean isUMinus() throws Z3Exception
00425 {
00426 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UMINUS;
00427 }
00428
00432 public boolean isMul() throws Z3Exception
00433 {
00434 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MUL;
00435 }
00436
00440 public boolean isDiv() throws Z3Exception
00441 {
00442 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_DIV;
00443 }
00444
00448 public boolean isIDiv() throws Z3Exception
00449 {
00450 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IDIV;
00451 }
00452
00456 public boolean isRemainder() throws Z3Exception
00457 {
00458 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REM;
00459 }
00460
00464 public boolean isModulus() throws Z3Exception
00465 {
00466 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_MOD;
00467 }
00468
00472 public boolean isIntToReal() throws Z3Exception
00473 {
00474 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_REAL;
00475 }
00476
00480 public boolean isRealToInt() throws Z3Exception
00481 {
00482 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_TO_INT;
00483 }
00484
00489 public boolean isRealIsInt() throws Z3Exception
00490 {
00491 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_IS_INT;
00492 }
00493
00497 public boolean isArray() throws Z3Exception
00498 {
00499 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
00500 .fromInt(Native.getSortKind(getContext().nCtx(),
00501 Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
00502 }
00503
00509 public boolean isStore() throws Z3Exception
00510 {
00511 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_STORE;
00512 }
00513
00517 public boolean isSelect() throws Z3Exception
00518 {
00519 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SELECT;
00520 }
00521
00527 public boolean isConstantArray() throws Z3Exception
00528 {
00529 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONST_ARRAY;
00530 }
00531
00536 public boolean isDefaultArray() throws Z3Exception
00537 {
00538 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT;
00539 }
00540
00545 public boolean isArrayMap() throws Z3Exception
00546 {
00547 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ARRAY_MAP;
00548 }
00549
00555 public boolean isAsArray() throws Z3Exception
00556 {
00557 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_AS_ARRAY;
00558 }
00559
00563 public boolean isSetUnion() throws Z3Exception
00564 {
00565 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_UNION;
00566 }
00567
00571 public boolean isSetIntersect() throws Z3Exception
00572 {
00573 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_INTERSECT;
00574 }
00575
00579 public boolean isSetDifference() throws Z3Exception
00580 {
00581 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_DIFFERENCE;
00582 }
00583
00587 public boolean isSetComplement() throws Z3Exception
00588 {
00589 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_COMPLEMENT;
00590 }
00591
00595 public boolean isSetSubset() throws Z3Exception
00596 {
00597 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SET_SUBSET;
00598 }
00599
00603 public boolean isBV() throws Z3Exception
00604 {
00605 return Native.getSortKind(getContext().nCtx(),
00606 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
00607 .toInt();
00608 }
00609
00613 public boolean isBVNumeral() throws Z3Exception
00614 {
00615 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNUM;
00616 }
00617
00621 public boolean isBVBitOne() throws Z3Exception
00622 {
00623 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT1;
00624 }
00625
00629 public boolean isBVBitZero() throws Z3Exception
00630 {
00631 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BIT0;
00632 }
00633
00637 public boolean isBVUMinus() throws Z3Exception
00638 {
00639 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNEG;
00640 }
00641
00645 public boolean isBVAdd() throws Z3Exception
00646 {
00647 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BADD;
00648 }
00649
00653 public boolean isBVSub() throws Z3Exception
00654 {
00655 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSUB;
00656 }
00657
00661 public boolean isBVMul() throws Z3Exception
00662 {
00663 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BMUL;
00664 }
00665
00669 public boolean isBVSDiv() throws Z3Exception
00670 {
00671 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV;
00672 }
00673
00677 public boolean isBVUDiv() throws Z3Exception
00678 {
00679 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV;
00680 }
00681
00685 public boolean isBVSRem() throws Z3Exception
00686 {
00687 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM;
00688 }
00689
00693 public boolean isBVURem() throws Z3Exception
00694 {
00695 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM;
00696 }
00697
00701 public boolean isBVSMod() throws Z3Exception
00702 {
00703 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD;
00704 }
00705
00709 boolean IsBVSDiv0() throws Z3Exception
00710 {
00711 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSDIV0;
00712 }
00713
00717 boolean IsBVUDiv0() throws Z3Exception
00718 {
00719 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUDIV0;
00720 }
00721
00725 boolean IsBVSRem0() throws Z3Exception
00726 {
00727 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSREM0;
00728 }
00729
00733 boolean IsBVURem0() throws Z3Exception
00734 {
00735 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BUREM0;
00736 }
00737
00741 boolean IsBVSMod0() throws Z3Exception
00742 {
00743 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSMOD0;
00744 }
00745
00749 public boolean isBVULE() throws Z3Exception
00750 {
00751 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULEQ;
00752 }
00753
00757 public boolean isBVSLE() throws Z3Exception
00758 {
00759 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLEQ;
00760 }
00761
00766 public boolean isBVUGE() throws Z3Exception
00767 {
00768 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGEQ;
00769 }
00770
00774 public boolean isBVSGE() throws Z3Exception
00775 {
00776 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGEQ;
00777 }
00778
00782 public boolean isBVULT() throws Z3Exception
00783 {
00784 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ULT;
00785 }
00786
00790 public boolean isBVSLT() throws Z3Exception
00791 {
00792 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SLT;
00793 }
00794
00798 public boolean isBVUGT() throws Z3Exception
00799 {
00800 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_UGT;
00801 }
00802
00806 public boolean isBVSGT() throws Z3Exception
00807 {
00808 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SGT;
00809 }
00810
00814 public boolean isBVAND() throws Z3Exception
00815 {
00816 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BAND;
00817 }
00818
00822 public boolean isBVOR() throws Z3Exception
00823 {
00824 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BOR;
00825 }
00826
00830 public boolean isBVNOT() throws Z3Exception
00831 {
00832 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOT;
00833 }
00834
00838 public boolean isBVXOR() throws Z3Exception
00839 {
00840 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXOR;
00841 }
00842
00846 public boolean isBVNAND() throws Z3Exception
00847 {
00848 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNAND;
00849 }
00850
00854 public boolean isBVNOR() throws Z3Exception
00855 {
00856 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BNOR;
00857 }
00858
00862 public boolean isBVXNOR() throws Z3Exception
00863 {
00864 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BXNOR;
00865 }
00866
00870 public boolean isBVConcat() throws Z3Exception
00871 {
00872 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CONCAT;
00873 }
00874
00878 public boolean isBVSignExtension() throws Z3Exception
00879 {
00880 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SIGN_EXT;
00881 }
00882
00886 public boolean isBVZeroExtension() throws Z3Exception
00887 {
00888 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ZERO_EXT;
00889 }
00890
00894 public boolean isBVExtract() throws Z3Exception
00895 {
00896 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXTRACT;
00897 }
00898
00902 public boolean isBVRepeat() throws Z3Exception
00903 {
00904 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_REPEAT;
00905 }
00906
00910 public boolean isBVReduceOR() throws Z3Exception
00911 {
00912 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDOR;
00913 }
00914
00918 public boolean isBVReduceAND() throws Z3Exception
00919 {
00920 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BREDAND;
00921 }
00922
00926 public boolean isBVComp() throws Z3Exception
00927 {
00928 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BCOMP;
00929 }
00930
00934 public boolean isBVShiftLeft() throws Z3Exception
00935 {
00936 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BSHL;
00937 }
00938
00942 public boolean isBVShiftRightLogical() throws Z3Exception
00943 {
00944 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BLSHR;
00945 }
00946
00950 public boolean isBVShiftRightArithmetic() throws Z3Exception
00951 {
00952 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BASHR;
00953 }
00954
00958 public boolean isBVRotateLeft() throws Z3Exception
00959 {
00960 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_LEFT;
00961 }
00962
00966 public boolean isBVRotateRight() throws Z3Exception
00967 {
00968 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_ROTATE_RIGHT;
00969 }
00970
00976 public boolean isBVRotateLeftExtended() throws Z3Exception
00977 {
00978 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT;
00979 }
00980
00986 public boolean isBVRotateRightExtended() throws Z3Exception
00987 {
00988 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT;
00989 }
00990
00997 public boolean isIntToBV() throws Z3Exception
00998 {
00999 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_INT2BV;
01000 }
01001
01008 public boolean isBVToInt() throws Z3Exception
01009 {
01010 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_BV2INT;
01011 }
01012
01018 public boolean isBVCarry() throws Z3Exception
01019 {
01020 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_CARRY;
01021 }
01022
01028 public boolean isBVXOR3() throws Z3Exception
01029 {
01030 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_XOR3;
01031 }
01032
01038 public boolean isLabel() throws Z3Exception
01039 {
01040 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL;
01041 }
01042
01048 public boolean isLabelLit() throws Z3Exception
01049 {
01050 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
01051 }
01052
01058 public boolean isOEQ() throws Z3Exception
01059 {
01060 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
01061 }
01062
01066 public boolean isProofTrue() throws Z3Exception
01067 {
01068 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRUE;
01069 }
01070
01074 public boolean isProofAsserted() throws Z3Exception
01075 {
01076 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ASSERTED;
01077 }
01078
01083 public boolean isProofGoal() throws Z3Exception
01084 {
01085 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_GOAL;
01086 }
01087
01094 public boolean isProofModusPonens() throws Z3Exception
01095 {
01096 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS;
01097 }
01098
01106 public boolean isProofReflexivity() throws Z3Exception
01107 {
01108 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY;
01109 }
01110
01117 public boolean isProofSymmetry() throws Z3Exception
01118 {
01119 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SYMMETRY;
01120 }
01121
01128 public boolean isProofTransitivity() throws Z3Exception
01129 {
01130 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY;
01131 }
01132
01146 public boolean isProofTransitivityStar() throws Z3Exception
01147 {
01148 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR;
01149 }
01150
01158 public boolean isProofMonotonicity() throws Z3Exception
01159 {
01160 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MONOTONICITY;
01161 }
01162
01168 public boolean isProofQuantIntro() throws Z3Exception
01169 {
01170 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO;
01171 }
01172
01184 public boolean isProofDistributivity() throws Z3Exception
01185 {
01186 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY;
01187 }
01188
01194 public boolean isProofAndElimination() throws Z3Exception
01195 {
01196 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_AND_ELIM;
01197 }
01198
01204 public boolean isProofOrElimination() throws Z3Exception
01205 {
01206 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM;
01207 }
01208
01221 public boolean isProofRewrite() throws Z3Exception
01222 {
01223 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE;
01224 }
01225
01237 public boolean isProofRewriteStar() throws Z3Exception
01238 {
01239 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR;
01240 }
01241
01247 public boolean isProofPullQuant() throws Z3Exception
01248 {
01249 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
01250 }
01251
01258 public boolean isProofPullQuantStar() throws Z3Exception
01259 {
01260 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR;
01261 }
01262
01270 public boolean isProofPushQuant() throws Z3Exception
01271 {
01272 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT;
01273 }
01274
01283 public boolean isProofElimUnusedVars() throws Z3Exception
01284 {
01285 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS;
01286 }
01287
01297 public boolean isProofDER() throws Z3Exception
01298 {
01299 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DER;
01300 }
01301
01306 public boolean isProofQuantInst() throws Z3Exception
01307 {
01308 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_QUANT_INST;
01309 }
01310
01315 public boolean isProofHypothesis() throws Z3Exception
01316 {
01317 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS;
01318 }
01319
01328 public boolean isProofLemma() throws Z3Exception
01329 {
01330 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_LEMMA;
01331 }
01332
01338 public boolean isProofUnitResolution() throws Z3Exception
01339 {
01340 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION;
01341 }
01342
01347 public boolean isProofIFFTrue() throws Z3Exception
01348 {
01349 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_TRUE;
01350 }
01351
01356 public boolean isProofIFFFalse() throws Z3Exception
01357 {
01358 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_FALSE;
01359 }
01360
01370 public boolean isProofCommutativity() throws Z3Exception
01371 {
01372 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY;
01373 }
01374
01393 public boolean isProofDefAxiom() throws Z3Exception
01394 {
01395 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM;
01396 }
01397
01414 public boolean isProofDefIntro() throws Z3Exception
01415 {
01416 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_DEF_INTRO;
01417 }
01418
01424 public boolean isProofApplyDef() throws Z3Exception
01425 {
01426 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_APPLY_DEF;
01427 }
01428
01433 public boolean isProofIFFOEQ() throws Z3Exception
01434 {
01435 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_IFF_OEQ;
01436 }
01437
01458 public boolean isProofNNFPos() throws Z3Exception
01459 {
01460 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_POS;
01461 }
01462
01474 public boolean isProofNNFNeg() throws Z3Exception
01475 {
01476 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
01477 }
01478
01489 public boolean isProofNNFStar() throws Z3Exception
01490 {
01491 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR;
01492 }
01493
01501 public boolean isProofCNFStar() throws Z3Exception
01502 {
01503 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR;
01504 }
01505
01515 public boolean isProofSkolemize() throws Z3Exception
01516 {
01517 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE;
01518 }
01519
01525 public boolean isProofModusPonensOEQ() throws Z3Exception
01526 {
01527 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ;
01528 }
01529
01544 public boolean isProofTheoryLemma() throws Z3Exception
01545 {
01546 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_TH_LEMMA;
01547 }
01548
01552 public boolean isRelation() throws Z3Exception
01553 {
01554 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
01555 .getSortKind(getContext().nCtx(),
01556 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
01557 .toInt());
01558 }
01559
01566 public boolean isRelationStore() throws Z3Exception
01567 {
01568 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_STORE;
01569 }
01570
01574 public boolean isEmptyRelation() throws Z3Exception
01575 {
01576 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_EMPTY;
01577 }
01578
01582 public boolean isIsEmptyRelation() throws Z3Exception
01583 {
01584 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_IS_EMPTY;
01585 }
01586
01590 public boolean isRelationalJoin() throws Z3Exception
01591 {
01592 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_JOIN;
01593 }
01594
01599 public boolean isRelationUnion() throws Z3Exception
01600 {
01601 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_UNION;
01602 }
01603
01608 public boolean isRelationWiden() throws Z3Exception
01609 {
01610 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_WIDEN;
01611 }
01612
01618 public boolean isRelationProject() throws Z3Exception
01619 {
01620 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_PROJECT;
01621 }
01622
01630 public boolean isRelationFilter() throws Z3Exception
01631 {
01632 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_FILTER;
01633 }
01634
01647 public boolean isRelationNegationFilter() throws Z3Exception
01648 {
01649 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER;
01650 }
01651
01657 public boolean isRelationRename() throws Z3Exception
01658 {
01659 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_RENAME;
01660 }
01661
01665 public boolean isRelationComplement() throws Z3Exception
01666 {
01667 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_COMPLEMENT;
01668 }
01669
01676 public boolean isRelationSelect() throws Z3Exception
01677 {
01678 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_SELECT;
01679 }
01680
01688 public boolean isRelationClone() throws Z3Exception
01689 {
01690 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_RA_CLONE;
01691 }
01692
01696 public boolean isFiniteDomain() throws Z3Exception
01697 {
01698 return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
01699 .getSortKind(getContext().nCtx(),
01700 Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
01701 .toInt());
01702 }
01703
01707 public boolean isFiniteDomainLT() throws Z3Exception
01708 {
01709 return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FD_LT;
01710 }
01711
01727 public int getIndex() throws Z3Exception
01728 {
01729 if (!isVar())
01730 throw new Z3Exception("Term is not a bound variable.");
01731
01732 return Native.getIndexValue(getContext().nCtx(), getNativeObject());
01733 }
01734
01738 protected Expr(Context ctx)
01739 {
01740 super(ctx);
01741 {
01742 }
01743 }
01744
01748 protected Expr(Context ctx, long obj) throws Z3Exception
01749 {
01750 super(ctx, obj);
01751 {
01752 }
01753 }
01754
01755 void checkNativeObject(long obj) throws Z3Exception
01756 {
01757 if (!Native.isApp(getContext().nCtx(), obj) &&
01758 Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() &&
01759 Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt())
01760 throw new Z3Exception("Underlying object is not a term");
01761 super.checkNativeObject(obj);
01762 }
01763
01764 static Expr create(Context ctx, FuncDecl f, Expr ... arguments)
01765 throws Z3Exception
01766 {
01767 long obj = Native.mkApp(ctx.nCtx(), f.getNativeObject(),
01768 AST.arrayLength(arguments), AST.arrayToNative(arguments));
01769 return create(ctx, obj);
01770 }
01771
01772 static Expr create(Context ctx, long obj) throws Z3Exception
01773 {
01774 Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
01775 if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
01776 return new Quantifier(ctx, obj);
01777 long s = Native.getSort(ctx.nCtx(), obj);
01778 Z3_sort_kind sk = Z3_sort_kind
01779 .fromInt(Native.getSortKind(ctx.nCtx(), s));
01780
01781 if (Native.isAlgebraicNumber(ctx.nCtx(), obj))
01782 return new AlgebraicNum(ctx, obj);
01783
01784 if (Native.isNumeralAst(ctx.nCtx(), obj))
01785 {
01786 switch (sk)
01787 {
01788 case Z3_INT_SORT:
01789 return new IntNum(ctx, obj);
01790 case Z3_REAL_SORT:
01791 return new RatNum(ctx, obj);
01792 case Z3_BV_SORT:
01793 return new BitVecNum(ctx, obj);
01794 default: ;
01795 }
01796 }
01797
01798 switch (sk)
01799 {
01800 case Z3_BOOL_SORT:
01801 return new BoolExpr(ctx, obj);
01802 case Z3_INT_SORT:
01803 return new IntExpr(ctx, obj);
01804 case Z3_REAL_SORT:
01805 return new RealExpr(ctx, obj);
01806 case Z3_BV_SORT:
01807 return new BitVecExpr(ctx, obj);
01808 case Z3_ARRAY_SORT:
01809 return new ArrayExpr(ctx, obj);
01810 case Z3_DATATYPE_SORT:
01811 return new DatatypeExpr(ctx, obj);
01812 default: ;
01813 }
01814
01815 return new Expr(ctx, obj);
01816 }
01817 }