Z3
src/api/java/Expr.java
Go to the documentation of this file.
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 /* using System; */
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)) // is this a numeral ast?
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines