Z3
src/api/java/Context.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00020 import java.util.Map;
00021 
00022 import com.microsoft.z3.enumerations.Z3_ast_print_mode;
00023 
00027 public class Context extends IDisposable
00028 {
00032     public Context() throws Z3Exception
00033     {
00034         super();
00035         m_ctx = Native.mkContextRc(0);
00036         initContext();
00037     }
00038 
00057     public Context(Map<String, String> settings) throws Z3Exception
00058     {
00059         super();
00060         long cfg = Native.mkConfig();
00061         for (Map.Entry<String, String> kv : settings.entrySet())
00062             Native.setParamValue(cfg, kv.getKey(), kv.getValue());
00063         m_ctx = Native.mkContextRc(cfg);
00064         Native.delConfig(cfg);
00065         initContext();
00066     }
00067 
00073     public IntSymbol mkSymbol(int i) throws Z3Exception
00074     {
00075         return new IntSymbol(this, i);
00076     }
00077 
00081     public StringSymbol mkSymbol(String name) throws Z3Exception
00082     {
00083         return new StringSymbol(this, name);
00084     }
00085 
00089     Symbol[] MkSymbols(String[] names) throws Z3Exception
00090     {
00091         if (names == null)
00092             return null;
00093         Symbol[] result = new Symbol[names.length];
00094         for (int i = 0; i < names.length; ++i)
00095             result[i] = mkSymbol(names[i]);
00096         return result;
00097     }
00098 
00099     private BoolSort m_boolSort = null;
00100     private IntSort m_intSort = null;
00101     private RealSort m_realSort = null;
00102 
00106     public BoolSort getBoolSort() throws Z3Exception
00107     {
00108         if (m_boolSort == null)
00109             m_boolSort = new BoolSort(this);
00110         return m_boolSort;
00111     }
00112 
00116     public IntSort getIntSort() throws Z3Exception
00117     {
00118         if (m_intSort == null)
00119             m_intSort = new IntSort(this);
00120         return m_intSort;
00121     }
00122 
00126     public RealSort getRealSort() throws Z3Exception
00127     {
00128         if (m_realSort == null)
00129             m_realSort = new RealSort(this);
00130         return m_realSort;
00131     }
00132 
00136     public BoolSort mkBoolSort() throws Z3Exception
00137     {
00138 
00139         return new BoolSort(this);
00140     }
00141 
00145     public UninterpretedSort mkUninterpretedSort(Symbol s) throws Z3Exception
00146     {
00147 
00148         checkContextMatch(s);
00149         return new UninterpretedSort(this, s);
00150     }
00151 
00155     public UninterpretedSort mkUninterpretedSort(String str) throws Z3Exception
00156     {
00157 
00158         return mkUninterpretedSort(mkSymbol(str));
00159     }
00160 
00164     public IntSort mkIntSort() throws Z3Exception
00165     {
00166 
00167         return new IntSort(this);
00168     }
00169 
00173     public RealSort mkRealSort() throws Z3Exception
00174     {
00175 
00176         return new RealSort(this);
00177     }
00178 
00182     public BitVecSort mkBitVecSort(int size) throws Z3Exception
00183     {
00184 
00185         return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
00186     }
00187 
00191     public ArraySort mkArraySort(Sort domain, Sort range) throws Z3Exception
00192     {
00193 
00194         checkContextMatch(domain);
00195         checkContextMatch(range);
00196         return new ArraySort(this, domain, range);
00197     }
00198 
00202     public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames,
00203             Sort[] fieldSorts) throws Z3Exception
00204     {
00205 
00206         checkContextMatch(name);
00207         checkContextMatch(fieldNames);
00208         checkContextMatch(fieldSorts);
00209         return new TupleSort(this, name, (int) fieldNames.length, fieldNames,
00210                 fieldSorts);
00211     }
00212 
00216     public EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
00217             throws Z3Exception
00218     {
00219 
00220         checkContextMatch(name);
00221         checkContextMatch(enumNames);
00222         return new EnumSort(this, name, enumNames);
00223     }
00224 
00228     public EnumSort mkEnumSort(String name, String... enumNames)
00229             throws Z3Exception
00230     {
00231         return new EnumSort(this, mkSymbol(name), MkSymbols(enumNames));
00232     }
00233 
00237     public ListSort mkListSort(Symbol name, Sort elemSort) throws Z3Exception
00238     {
00239 
00240         checkContextMatch(name);
00241         checkContextMatch(elemSort);
00242         return new ListSort(this, name, elemSort);
00243     }
00244 
00248     public ListSort mkListSort(String name, Sort elemSort) throws Z3Exception
00249     {
00250 
00251         checkContextMatch(elemSort);
00252         return new ListSort(this, mkSymbol(name), elemSort);
00253     }
00254 
00258     public FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
00259             throws Z3Exception
00260     {
00261 
00262         checkContextMatch(name);
00263         return new FiniteDomainSort(this, name, size);
00264     }
00265 
00269     public FiniteDomainSort mkFiniteDomainSort(String name, long size)
00270             throws Z3Exception
00271     {
00272 
00273         return new FiniteDomainSort(this, mkSymbol(name), size);
00274     }
00275 
00287     public Constructor mkConstructor(Symbol name, Symbol recognizer,
00288             Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
00289             throws Z3Exception
00290     {
00291 
00292         return new Constructor(this, name, recognizer, fieldNames, sorts,
00293                 sortRefs);
00294     }
00295 
00303     public Constructor mkConstructor(String name, String recognizer,
00304             String[] fieldNames, Sort[] sorts, int[] sortRefs)
00305             throws Z3Exception
00306     {
00307 
00308         return new Constructor(this, mkSymbol(name), mkSymbol(recognizer),
00309                 MkSymbols(fieldNames), sorts, sortRefs);
00310     }
00311 
00315     public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
00316             throws Z3Exception
00317     {
00318 
00319         checkContextMatch(name);
00320         checkContextMatch(constructors);
00321         return new DatatypeSort(this, name, constructors);
00322     }
00323 
00327     public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
00328             throws Z3Exception
00329     {
00330 
00331         checkContextMatch(constructors);
00332         return new DatatypeSort(this, mkSymbol(name), constructors);
00333     }
00334 
00340     public DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
00341             throws Z3Exception
00342     {
00343 
00344         checkContextMatch(names);
00345         int n = (int) names.length;
00346         ConstructorList[] cla = new ConstructorList[n];
00347         long[] n_constr = new long[n];
00348         for (int i = 0; i < n; i++)
00349         {
00350             Constructor[] constructor = c[i];
00351 
00352             checkContextMatch(constructor);
00353             cla[i] = new ConstructorList(this, constructor);
00354             n_constr[i] = cla[i].getNativeObject();
00355         }
00356         long[] n_res = new long[n];
00357         Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
00358                 n_constr);
00359         DatatypeSort[] res = new DatatypeSort[n];
00360         for (int i = 0; i < n; i++)
00361             res[i] = new DatatypeSort(this, n_res[i]);
00362         return res;
00363     }
00364 
00371     public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
00372             throws Z3Exception
00373     {
00374 
00375         return mkDatatypeSorts(MkSymbols(names), c);
00376     }
00377 
00381     public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
00382             throws Z3Exception
00383     {
00384 
00385         checkContextMatch(name);
00386         checkContextMatch(domain);
00387         checkContextMatch(range);
00388         return new FuncDecl(this, name, domain, range);
00389     }
00390 
00394     public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
00395             throws Z3Exception
00396     {
00397 
00398         checkContextMatch(name);
00399         checkContextMatch(domain);
00400         checkContextMatch(range);
00401         Sort[] q = new Sort[] { domain };
00402         return new FuncDecl(this, name, q, range);
00403     }
00404 
00408     public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
00409             throws Z3Exception
00410     {
00411 
00412         checkContextMatch(domain);
00413         checkContextMatch(range);
00414         return new FuncDecl(this, mkSymbol(name), domain, range);
00415     }
00416 
00420     public FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
00421             throws Z3Exception
00422     {
00423 
00424         checkContextMatch(domain);
00425         checkContextMatch(range);
00426         Sort[] q = new Sort[] { domain };
00427         return new FuncDecl(this, mkSymbol(name), q, range);
00428     }
00429 
00435     public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
00436             throws Z3Exception
00437     {
00438 
00439         checkContextMatch(domain);
00440         checkContextMatch(range);
00441         return new FuncDecl(this, prefix, domain, range);
00442     }
00443 
00447     public FuncDecl mkConstDecl(Symbol name, Sort range) throws Z3Exception
00448     {
00449 
00450         checkContextMatch(name);
00451         checkContextMatch(range);
00452         return new FuncDecl(this, name, null, range);
00453     }
00454 
00458     public FuncDecl mkConstDecl(String name, Sort range) throws Z3Exception
00459     {
00460 
00461         checkContextMatch(range);
00462         return new FuncDecl(this, mkSymbol(name), null, range);
00463     }
00464 
00470     public FuncDecl mkFreshConstDecl(String prefix, Sort range)
00471             throws Z3Exception
00472     {
00473 
00474         checkContextMatch(range);
00475         return new FuncDecl(this, prefix, null, range);
00476     }
00477 
00482     public Expr mkBound(int index, Sort ty) throws Z3Exception
00483     {
00484         return Expr.create(this,
00485                 Native.mkBound(nCtx(), index, ty.getNativeObject()));
00486     }
00487 
00491     public Pattern mkPattern(Expr... terms) throws Z3Exception
00492     {
00493         if (terms.length == 0)
00494             throw new Z3Exception("Cannot create a pattern from zero terms");
00495 
00496         long[] termsNative = AST.arrayToNative(terms);
00497         return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length,
00498                 termsNative));
00499     }
00500 
00505     public Expr mkConst(Symbol name, Sort range) throws Z3Exception
00506     {
00507 
00508         checkContextMatch(name);
00509         checkContextMatch(range);
00510 
00511         return Expr.create(
00512                 this,
00513                 Native.mkConst(nCtx(), name.getNativeObject(),
00514                         range.getNativeObject()));
00515     }
00516 
00521     public Expr mkConst(String name, Sort range) throws Z3Exception
00522     {
00523 
00524         return mkConst(mkSymbol(name), range);
00525     }
00526 
00531     public Expr mkFreshConst(String prefix, Sort range) throws Z3Exception
00532     {
00533 
00534         checkContextMatch(range);
00535         return Expr.create(this,
00536                 Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
00537     }
00538 
00543     public Expr mkConst(FuncDecl f) throws Z3Exception
00544     {
00545 
00546         return mkApp(f, (Expr[]) null);
00547     }
00548 
00552     public BoolExpr mkBoolConst(Symbol name) throws Z3Exception
00553     {
00554 
00555         return (BoolExpr) mkConst(name, getBoolSort());
00556     }
00557 
00561     public BoolExpr mkBoolConst(String name) throws Z3Exception
00562     {
00563 
00564         return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
00565     }
00566 
00570     public IntExpr mkIntConst(Symbol name) throws Z3Exception
00571     {
00572 
00573         return (IntExpr) mkConst(name, getIntSort());
00574     }
00575 
00579     public IntExpr mkIntConst(String name) throws Z3Exception
00580     {
00581 
00582         return (IntExpr) mkConst(name, getIntSort());
00583     }
00584 
00588     public RealExpr mkRealConst(Symbol name) throws Z3Exception
00589     {
00590 
00591         return (RealExpr) mkConst(name, getRealSort());
00592     }
00593 
00597     public RealExpr mkRealConst(String name) throws Z3Exception
00598     {
00599 
00600         return (RealExpr) mkConst(name, getRealSort());
00601     }
00602 
00606     public BitVecExpr mkBVConst(Symbol name, int size) throws Z3Exception
00607     {
00608 
00609         return (BitVecExpr) mkConst(name, mkBitVecSort(size));
00610     }
00611 
00615     public BitVecExpr mkBVConst(String name, int size) throws Z3Exception
00616     {
00617 
00618         return (BitVecExpr) mkConst(name, mkBitVecSort(size));
00619     }
00620 
00624     public Expr mkApp(FuncDecl f, Expr... args) throws Z3Exception
00625     {
00626         checkContextMatch(f);
00627         checkContextMatch(args);
00628         return Expr.create(this, f, args);
00629     }
00630 
00634     public BoolExpr mkTrue() throws Z3Exception
00635     {
00636         return new BoolExpr(this, Native.mkTrue(nCtx()));
00637     }
00638 
00642     public BoolExpr mkFalse() throws Z3Exception
00643     {
00644         return new BoolExpr(this, Native.mkFalse(nCtx()));
00645     }
00646 
00650     public BoolExpr mkBool(boolean value) throws Z3Exception
00651     {
00652         return value ? mkTrue() : mkFalse();
00653     }
00654 
00658     public BoolExpr mkEq(Expr x, Expr y) throws Z3Exception
00659     {
00660         checkContextMatch(x);
00661         checkContextMatch(y);
00662         return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
00663                 y.getNativeObject()));
00664     }
00665 
00669     public BoolExpr mkDistinct(Expr... args) throws Z3Exception
00670     {
00671         checkContextMatch(args);
00672         return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length,
00673                 AST.arrayToNative(args)));
00674     }
00675 
00679     public BoolExpr mkNot(BoolExpr a) throws Z3Exception
00680     {
00681 
00682         checkContextMatch(a);
00683         return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
00684     }
00685 
00692     public Expr mkITE(BoolExpr t1, Expr t2, Expr t3) throws Z3Exception
00693     {
00694 
00695         checkContextMatch(t1);
00696         checkContextMatch(t2);
00697         checkContextMatch(t3);
00698         return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
00699                 t2.getNativeObject(), t3.getNativeObject()));
00700     }
00701 
00705     public BoolExpr mkIff(BoolExpr t1, BoolExpr t2) throws Z3Exception
00706     {
00707 
00708         checkContextMatch(t1);
00709         checkContextMatch(t2);
00710         return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
00711                 t2.getNativeObject()));
00712     }
00713 
00717     public BoolExpr mkImplies(BoolExpr t1, BoolExpr t2) throws Z3Exception
00718     {
00719 
00720         checkContextMatch(t1);
00721         checkContextMatch(t2);
00722         return new BoolExpr(this, Native.mkImplies(nCtx(),
00723                 t1.getNativeObject(), t2.getNativeObject()));
00724     }
00725 
00729     public BoolExpr mkXor(BoolExpr t1, BoolExpr t2) throws Z3Exception
00730     {
00731 
00732         checkContextMatch(t1);
00733         checkContextMatch(t2);
00734         return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
00735                 t2.getNativeObject()));
00736     }
00737 
00741     public BoolExpr mkAnd(BoolExpr... t) throws Z3Exception
00742     {
00743 
00744         checkContextMatch(t);
00745         return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length,
00746                 AST.arrayToNative(t)));
00747     }
00748 
00752     public BoolExpr mkOr(BoolExpr... t) throws Z3Exception
00753     {
00754 
00755         checkContextMatch(t);
00756         return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length,
00757                 AST.arrayToNative(t)));
00758     }
00759 
00763     public ArithExpr mkAdd(ArithExpr... t) throws Z3Exception
00764     {
00765 
00766         checkContextMatch(t);
00767         return (ArithExpr) Expr.create(this,
00768                 Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t)));
00769     }
00770 
00774     public ArithExpr mkMul(ArithExpr... t) throws Z3Exception
00775     {
00776 
00777         checkContextMatch(t);
00778         return (ArithExpr) Expr.create(this,
00779                 Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t)));
00780     }
00781 
00785     public ArithExpr mkSub(ArithExpr... t) throws Z3Exception
00786     {
00787 
00788         checkContextMatch(t);
00789         return (ArithExpr) Expr.create(this,
00790                 Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t)));
00791     }
00792 
00796     public ArithExpr mkUnaryMinus(ArithExpr t) throws Z3Exception
00797     {
00798 
00799         checkContextMatch(t);
00800         return (ArithExpr) Expr.create(this,
00801                 Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
00802     }
00803 
00807     public ArithExpr mkDiv(ArithExpr t1, ArithExpr t2) throws Z3Exception
00808     {
00809 
00810         checkContextMatch(t1);
00811         checkContextMatch(t2);
00812         return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
00813                 t1.getNativeObject(), t2.getNativeObject()));
00814     }
00815 
00820     public IntExpr mkMod(IntExpr t1, IntExpr t2) throws Z3Exception
00821     {
00822 
00823         checkContextMatch(t1);
00824         checkContextMatch(t2);
00825         return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
00826                 t2.getNativeObject()));
00827     }
00828 
00833     public IntExpr mkRem(IntExpr t1, IntExpr t2) throws Z3Exception
00834     {
00835 
00836         checkContextMatch(t1);
00837         checkContextMatch(t2);
00838         return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
00839                 t2.getNativeObject()));
00840     }
00841 
00845     public ArithExpr mkPower(ArithExpr t1, ArithExpr t2) throws Z3Exception
00846     {
00847 
00848         checkContextMatch(t1);
00849         checkContextMatch(t2);
00850         return (ArithExpr) Expr.create(
00851                 this,
00852                 Native.mkPower(nCtx(), t1.getNativeObject(),
00853                         t2.getNativeObject()));
00854     }
00855 
00859     public BoolExpr mkLt(ArithExpr t1, ArithExpr t2) throws Z3Exception
00860     {
00861 
00862         checkContextMatch(t1);
00863         checkContextMatch(t2);
00864         return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
00865                 t2.getNativeObject()));
00866     }
00867 
00871     public BoolExpr mkLe(ArithExpr t1, ArithExpr t2) throws Z3Exception
00872     {
00873 
00874         checkContextMatch(t1);
00875         checkContextMatch(t2);
00876         return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
00877                 t2.getNativeObject()));
00878     }
00879 
00883     public BoolExpr mkGt(ArithExpr t1, ArithExpr t2) throws Z3Exception
00884     {
00885 
00886         checkContextMatch(t1);
00887         checkContextMatch(t2);
00888         return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
00889                 t2.getNativeObject()));
00890     }
00891 
00895     public BoolExpr mkGe(ArithExpr t1, ArithExpr t2) throws Z3Exception
00896     {
00897 
00898         checkContextMatch(t1);
00899         checkContextMatch(t2);
00900         return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
00901                 t2.getNativeObject()));
00902     }
00903 
00913     public RealExpr mkInt2Real(IntExpr t) throws Z3Exception
00914     {
00915 
00916         checkContextMatch(t);
00917         return new RealExpr(this,
00918                 Native.mkInt2real(nCtx(), t.getNativeObject()));
00919     }
00920 
00926     public IntExpr mkReal2Int(RealExpr t) throws Z3Exception
00927     {
00928 
00929         checkContextMatch(t);
00930         return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
00931     }
00932 
00936     public BoolExpr mkIsInteger(RealExpr t) throws Z3Exception
00937     {
00938 
00939         checkContextMatch(t);
00940         return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
00941     }
00942 
00947     public BitVecExpr mkBVNot(BitVecExpr t) throws Z3Exception
00948     {
00949 
00950         checkContextMatch(t);
00951         return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
00952     }
00953 
00958     public BitVecExpr mkBVRedAND(BitVecExpr t) throws Z3Exception
00959     {
00960 
00961         checkContextMatch(t);
00962         return new BitVecExpr(this, Native.mkBvredand(nCtx(),
00963                 t.getNativeObject()));
00964     }
00965 
00970     public BitVecExpr mkBVRedOR(BitVecExpr t) throws Z3Exception
00971     {
00972 
00973         checkContextMatch(t);
00974         return new BitVecExpr(this, Native.mkBvredor(nCtx(),
00975                 t.getNativeObject()));
00976     }
00977 
00982     public BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
00983     {
00984 
00985         checkContextMatch(t1);
00986         checkContextMatch(t2);
00987         return new BitVecExpr(this, Native.mkBvand(nCtx(),
00988                 t1.getNativeObject(), t2.getNativeObject()));
00989     }
00990 
00995     public BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
00996     {
00997 
00998         checkContextMatch(t1);
00999         checkContextMatch(t2);
01000         return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
01001                 t2.getNativeObject()));
01002     }
01003 
01008     public BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01009     {
01010 
01011         checkContextMatch(t1);
01012         checkContextMatch(t2);
01013         return new BitVecExpr(this, Native.mkBvxor(nCtx(),
01014                 t1.getNativeObject(), t2.getNativeObject()));
01015     }
01016 
01021     public BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01022     {
01023 
01024         checkContextMatch(t1);
01025         checkContextMatch(t2);
01026         return new BitVecExpr(this, Native.mkBvnand(nCtx(),
01027                 t1.getNativeObject(), t2.getNativeObject()));
01028     }
01029 
01034     public BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01035     {
01036 
01037         checkContextMatch(t1);
01038         checkContextMatch(t2);
01039         return new BitVecExpr(this, Native.mkBvnor(nCtx(),
01040                 t1.getNativeObject(), t2.getNativeObject()));
01041     }
01042 
01047     public BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01048     {
01049 
01050         checkContextMatch(t1);
01051         checkContextMatch(t2);
01052         return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
01053                 t1.getNativeObject(), t2.getNativeObject()));
01054     }
01055 
01060     public BitVecExpr mkBVNeg(BitVecExpr t) throws Z3Exception
01061     {
01062 
01063         checkContextMatch(t);
01064         return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
01065     }
01066 
01071     public BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01072     {
01073 
01074         checkContextMatch(t1);
01075         checkContextMatch(t2);
01076         return new BitVecExpr(this, Native.mkBvadd(nCtx(),
01077                 t1.getNativeObject(), t2.getNativeObject()));
01078     }
01079 
01084     public BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01085     {
01086 
01087         checkContextMatch(t1);
01088         checkContextMatch(t2);
01089         return new BitVecExpr(this, Native.mkBvsub(nCtx(),
01090                 t1.getNativeObject(), t2.getNativeObject()));
01091     }
01092 
01097     public BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01098     {
01099 
01100         checkContextMatch(t1);
01101         checkContextMatch(t2);
01102         return new BitVecExpr(this, Native.mkBvmul(nCtx(),
01103                 t1.getNativeObject(), t2.getNativeObject()));
01104     }
01105 
01112     public BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01113     {
01114 
01115         checkContextMatch(t1);
01116         checkContextMatch(t2);
01117         return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
01118                 t1.getNativeObject(), t2.getNativeObject()));
01119     }
01120 
01133     public BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01134     {
01135 
01136         checkContextMatch(t1);
01137         checkContextMatch(t2);
01138         return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
01139                 t1.getNativeObject(), t2.getNativeObject()));
01140     }
01141 
01148     public BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01149     {
01150 
01151         checkContextMatch(t1);
01152         checkContextMatch(t2);
01153         return new BitVecExpr(this, Native.mkBvurem(nCtx(),
01154                 t1.getNativeObject(), t2.getNativeObject()));
01155     }
01156 
01166     public BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01167     {
01168 
01169         checkContextMatch(t1);
01170         checkContextMatch(t2);
01171         return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
01172                 t1.getNativeObject(), t2.getNativeObject()));
01173     }
01174 
01180     public BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01181     {
01182 
01183         checkContextMatch(t1);
01184         checkContextMatch(t2);
01185         return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
01186                 t1.getNativeObject(), t2.getNativeObject()));
01187     }
01188 
01193     public BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01194     {
01195 
01196         checkContextMatch(t1);
01197         checkContextMatch(t2);
01198         return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
01199                 t2.getNativeObject()));
01200     }
01201 
01206     public BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01207     {
01208 
01209         checkContextMatch(t1);
01210         checkContextMatch(t2);
01211         return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
01212                 t2.getNativeObject()));
01213     }
01214 
01219     public BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01220     {
01221 
01222         checkContextMatch(t1);
01223         checkContextMatch(t2);
01224         return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
01225                 t2.getNativeObject()));
01226     }
01227 
01232     public BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01233     {
01234 
01235         checkContextMatch(t1);
01236         checkContextMatch(t2);
01237         return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
01238                 t2.getNativeObject()));
01239     }
01240 
01245     public BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01246     {
01247 
01248         checkContextMatch(t1);
01249         checkContextMatch(t2);
01250         return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
01251                 t2.getNativeObject()));
01252     }
01253 
01258     public BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01259     {
01260 
01261         checkContextMatch(t1);
01262         checkContextMatch(t2);
01263         return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
01264                 t2.getNativeObject()));
01265     }
01266 
01271     public BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01272     {
01273 
01274         checkContextMatch(t1);
01275         checkContextMatch(t2);
01276         return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
01277                 t2.getNativeObject()));
01278     }
01279 
01284     public BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01285     {
01286 
01287         checkContextMatch(t1);
01288         checkContextMatch(t2);
01289         return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
01290                 t2.getNativeObject()));
01291     }
01292 
01302     public BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01303     {
01304 
01305         checkContextMatch(t1);
01306         checkContextMatch(t2);
01307         return new BitVecExpr(this, Native.mkConcat(nCtx(),
01308                 t1.getNativeObject(), t2.getNativeObject()));
01309     }
01310 
01318     public BitVecExpr mkExtract(int high, int low, BitVecExpr t)
01319             throws Z3Exception
01320     {
01321 
01322         checkContextMatch(t);
01323         return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
01324                 t.getNativeObject()));
01325     }
01326 
01333     public BitVecExpr mkSignExt(int i, BitVecExpr t) throws Z3Exception
01334     {
01335 
01336         checkContextMatch(t);
01337         return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
01338                 t.getNativeObject()));
01339     }
01340 
01347     public BitVecExpr mkZeroExt(int i, BitVecExpr t) throws Z3Exception
01348     {
01349 
01350         checkContextMatch(t);
01351         return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
01352                 t.getNativeObject()));
01353     }
01354 
01359     public BitVecExpr mkRepeat(int i, BitVecExpr t) throws Z3Exception
01360     {
01361 
01362         checkContextMatch(t);
01363         return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
01364                 t.getNativeObject()));
01365     }
01366 
01377     public BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01378     {
01379 
01380         checkContextMatch(t1);
01381         checkContextMatch(t2);
01382         return new BitVecExpr(this, Native.mkBvshl(nCtx(),
01383                 t1.getNativeObject(), t2.getNativeObject()));
01384     }
01385 
01396     public BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01397     {
01398 
01399         checkContextMatch(t1);
01400         checkContextMatch(t2);
01401         return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
01402                 t1.getNativeObject(), t2.getNativeObject()));
01403     }
01404 
01416     public BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2) throws Z3Exception
01417     {
01418 
01419         checkContextMatch(t1);
01420         checkContextMatch(t2);
01421         return new BitVecExpr(this, Native.mkBvashr(nCtx(),
01422                 t1.getNativeObject(), t2.getNativeObject()));
01423     }
01424 
01429     public BitVecExpr mkBVRotateLeft(int i, BitVecExpr t) throws Z3Exception
01430     {
01431 
01432         checkContextMatch(t);
01433         return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
01434                 t.getNativeObject()));
01435     }
01436 
01441     public BitVecExpr mkBVRotateRight(int i, BitVecExpr t) throws Z3Exception
01442     {
01443 
01444         checkContextMatch(t);
01445         return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
01446                 t.getNativeObject()));
01447     }
01448 
01454     public BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
01455             throws Z3Exception
01456     {
01457 
01458         checkContextMatch(t1);
01459         checkContextMatch(t2);
01460         return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
01461                 t1.getNativeObject(), t2.getNativeObject()));
01462     }
01463 
01469     public BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
01470             throws Z3Exception
01471     {
01472 
01473         checkContextMatch(t1);
01474         checkContextMatch(t2);
01475         return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
01476                 t1.getNativeObject(), t2.getNativeObject()));
01477     }
01478 
01487     public BitVecExpr mkInt2BV(int n, IntExpr t) throws Z3Exception
01488     {
01489 
01490         checkContextMatch(t);
01491         return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
01492                 t.getNativeObject()));
01493     }
01494 
01509     public IntExpr mkBV2Int(BitVecExpr t, boolean signed) throws Z3Exception
01510     {
01511 
01512         checkContextMatch(t);
01513         return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
01514                 (signed) ? true : false));
01515     }
01516 
01521     public BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2,
01522             boolean isSigned) throws Z3Exception
01523     {
01524 
01525         checkContextMatch(t1);
01526         checkContextMatch(t2);
01527         return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
01528                 .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
01529                 : false));
01530     }
01531 
01536     public BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
01537             throws Z3Exception
01538     {
01539 
01540         checkContextMatch(t1);
01541         checkContextMatch(t2);
01542         return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
01543                 t1.getNativeObject(), t2.getNativeObject()));
01544     }
01545 
01550     public BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
01551             throws Z3Exception
01552     {
01553 
01554         checkContextMatch(t1);
01555         checkContextMatch(t2);
01556         return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
01557                 t1.getNativeObject(), t2.getNativeObject()));
01558     }
01559 
01564     public BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2,
01565             boolean isSigned) throws Z3Exception
01566     {
01567 
01568         checkContextMatch(t1);
01569         checkContextMatch(t2);
01570         return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
01571                 .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
01572                 : false));
01573     }
01574 
01579     public BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
01580             throws Z3Exception
01581     {
01582 
01583         checkContextMatch(t1);
01584         checkContextMatch(t2);
01585         return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
01586                 t1.getNativeObject(), t2.getNativeObject()));
01587     }
01588 
01593     public BoolExpr mkBVNegNoOverflow(BitVecExpr t) throws Z3Exception
01594     {
01595 
01596         checkContextMatch(t);
01597         return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
01598                 t.getNativeObject()));
01599     }
01600 
01605     public BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2,
01606             boolean isSigned) throws Z3Exception
01607     {
01608 
01609         checkContextMatch(t1);
01610         checkContextMatch(t2);
01611         return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
01612                 .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
01613                 : false));
01614     }
01615 
01620     public BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
01621             throws Z3Exception
01622     {
01623 
01624         checkContextMatch(t1);
01625         checkContextMatch(t2);
01626         return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
01627                 t1.getNativeObject(), t2.getNativeObject()));
01628     }
01629 
01633     public ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
01634             throws Z3Exception
01635     {
01636 
01637         return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
01638     }
01639 
01643     public ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
01644             throws Z3Exception
01645     {
01646 
01647         return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
01648     }
01649 
01659     public Expr mkSelect(ArrayExpr a, Expr i) throws Z3Exception
01660     {
01661 
01662         checkContextMatch(a);
01663         checkContextMatch(i);
01664         return Expr.create(
01665                 this,
01666                 Native.mkSelect(nCtx(), a.getNativeObject(),
01667                         i.getNativeObject()));
01668     }
01669 
01683     public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v) throws Z3Exception
01684     {
01685 
01686         checkContextMatch(a);
01687         checkContextMatch(i);
01688         checkContextMatch(v);
01689         return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
01690                 i.getNativeObject(), v.getNativeObject()));
01691     }
01692 
01699     public ArrayExpr mkConstArray(Sort domain, Expr v) throws Z3Exception
01700     {
01701 
01702         checkContextMatch(domain);
01703         checkContextMatch(v);
01704         return new ArrayExpr(this, Native.mkConstArray(nCtx(),
01705                 domain.getNativeObject(), v.getNativeObject()));
01706     }
01707 
01717     public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args) throws Z3Exception
01718     {
01719 
01720         checkContextMatch(f);
01721         checkContextMatch(args);
01722         return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
01723                 f.getNativeObject(), AST.arrayLength(args),
01724                 AST.arrayToNative(args)));
01725     }
01726 
01732     public Expr mkTermArray(ArrayExpr array) throws Z3Exception
01733     {
01734 
01735         checkContextMatch(array);
01736         return Expr.create(this,
01737                 Native.mkArrayDefault(nCtx(), array.getNativeObject()));
01738     }
01739 
01743     public SetSort mkSetSort(Sort ty) throws Z3Exception
01744     {
01745 
01746         checkContextMatch(ty);
01747         return new SetSort(this, ty);
01748     }
01749 
01753     public Expr mkEmptySet(Sort domain) throws Z3Exception
01754     {
01755 
01756         checkContextMatch(domain);
01757         return Expr.create(this,
01758                 Native.mkEmptySet(nCtx(), domain.getNativeObject()));
01759     }
01760 
01764     public Expr mkFullSet(Sort domain) throws Z3Exception
01765     {
01766 
01767         checkContextMatch(domain);
01768         return Expr.create(this,
01769                 Native.mkFullSet(nCtx(), domain.getNativeObject()));
01770     }
01771 
01775     public Expr mkSetAdd(Expr set, Expr element) throws Z3Exception
01776     {
01777 
01778         checkContextMatch(set);
01779         checkContextMatch(element);
01780         return Expr.create(
01781                 this,
01782                 Native.mkSetAdd(nCtx(), set.getNativeObject(),
01783                         element.getNativeObject()));
01784     }
01785 
01789     public Expr mkSetDel(Expr set, Expr element) throws Z3Exception
01790     {
01791 
01792         checkContextMatch(set);
01793         checkContextMatch(element);
01794         return Expr.create(
01795                 this,
01796                 Native.mkSetDel(nCtx(), set.getNativeObject(),
01797                         element.getNativeObject()));
01798     }
01799 
01803     public Expr mkSetUnion(Expr... args) throws Z3Exception
01804     {
01805 
01806         checkContextMatch(args);
01807         return Expr.create(
01808                 this,
01809                 Native.mkSetUnion(nCtx(), (int) args.length,
01810                         AST.arrayToNative(args)));
01811     }
01812 
01816     public Expr mkSetIntersection(Expr... args) throws Z3Exception
01817     {
01818 
01819         checkContextMatch(args);
01820         return Expr.create(
01821                 this,
01822                 Native.mkSetIntersect(nCtx(), (int) args.length,
01823                         AST.arrayToNative(args)));
01824     }
01825 
01829     public Expr mkSetDifference(Expr arg1, Expr arg2) throws Z3Exception
01830     {
01831 
01832         checkContextMatch(arg1);
01833         checkContextMatch(arg2);
01834         return Expr.create(
01835                 this,
01836                 Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
01837                         arg2.getNativeObject()));
01838     }
01839 
01843     public Expr mkSetComplement(Expr arg) throws Z3Exception
01844     {
01845 
01846         checkContextMatch(arg);
01847         return Expr.create(this,
01848                 Native.mkSetComplement(nCtx(), arg.getNativeObject()));
01849     }
01850 
01854     public Expr mkSetMembership(Expr elem, Expr set) throws Z3Exception
01855     {
01856 
01857         checkContextMatch(elem);
01858         checkContextMatch(set);
01859         return Expr.create(
01860                 this,
01861                 Native.mkSetMember(nCtx(), elem.getNativeObject(),
01862                         set.getNativeObject()));
01863     }
01864 
01868     public Expr mkSetSubset(Expr arg1, Expr arg2) throws Z3Exception
01869     {
01870 
01871         checkContextMatch(arg1);
01872         checkContextMatch(arg2);
01873         return Expr.create(
01874                 this,
01875                 Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
01876                         arg2.getNativeObject()));
01877     }
01878 
01890     public Expr mkNumeral(String v, Sort ty) throws Z3Exception
01891     {
01892 
01893         checkContextMatch(ty);
01894         return Expr.create(this,
01895                 Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
01896     }
01897 
01908     public Expr mkNumeral(int v, Sort ty) throws Z3Exception
01909     {
01910 
01911         checkContextMatch(ty);
01912         return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
01913     }
01914 
01925     public Expr mkNumeral(long v, Sort ty) throws Z3Exception
01926     {
01927 
01928         checkContextMatch(ty);
01929         return Expr.create(this,
01930                 Native.mkInt64(nCtx(), v, ty.getNativeObject()));
01931     }
01932 
01940     public RatNum mkReal(int num, int den) throws Z3Exception
01941     {
01942         if (den == 0)
01943             throw new Z3Exception("Denominator is zero");
01944 
01945         return new RatNum(this, Native.mkReal(nCtx(), num, den));
01946     }
01947 
01954     public RatNum mkReal(String v) throws Z3Exception
01955     {
01956 
01957         return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
01958                 .getNativeObject()));
01959     }
01960 
01966     public RatNum mkReal(int v) throws Z3Exception
01967     {
01968 
01969         return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
01970                 .getNativeObject()));
01971     }
01972 
01978     public RatNum mkReal(long v) throws Z3Exception
01979     {
01980 
01981         return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
01982                 .getNativeObject()));
01983     }
01984 
01989     public IntNum mkInt(String v) throws Z3Exception
01990     {
01991 
01992         return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
01993                 .getNativeObject()));
01994     }
01995 
02001     public IntNum mkInt(int v) throws Z3Exception
02002     {
02003 
02004         return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
02005                 .getNativeObject()));
02006     }
02007 
02013     public IntNum mkInt(long v) throws Z3Exception
02014     {
02015 
02016         return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
02017                 .getNativeObject()));
02018     }
02019 
02025     public BitVecNum mkBV(String v, int size) throws Z3Exception
02026     {
02027 
02028         return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
02029     }
02030 
02035     public BitVecNum mkBV(int v, int size) throws Z3Exception
02036     {
02037 
02038         return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
02039     }
02040 
02045     public BitVecNum mkBV(long v, int size) throws Z3Exception
02046     {
02047 
02048         return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
02049     }
02050 
02070     public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
02071             int weight, Pattern[] patterns, Expr[] noPatterns,
02072             Symbol quantifierID, Symbol skolemID) throws Z3Exception
02073     {
02074 
02075         return new Quantifier(this, true, sorts, names, body, weight, patterns,
02076                 noPatterns, quantifierID, skolemID);
02077     }
02078 
02082     public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
02083             Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
02084             Symbol skolemID) throws Z3Exception
02085     {
02086 
02087         return new Quantifier(this, true, boundConstants, body, weight,
02088                 patterns, noPatterns, quantifierID, skolemID);
02089     }
02090 
02095     public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
02096             int weight, Pattern[] patterns, Expr[] noPatterns,
02097             Symbol quantifierID, Symbol skolemID) throws Z3Exception
02098     {
02099 
02100         return new Quantifier(this, false, sorts, names, body, weight,
02101                 patterns, noPatterns, quantifierID, skolemID);
02102     }
02103 
02107     public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
02108             Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
02109             Symbol skolemID) throws Z3Exception
02110     {
02111 
02112         return new Quantifier(this, false, boundConstants, body, weight,
02113                 patterns, noPatterns, quantifierID, skolemID);
02114     }
02115 
02119     public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
02120             Symbol[] names, Expr body, int weight, Pattern[] patterns,
02121             Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
02122             throws Z3Exception
02123     {
02124 
02125         if (universal)
02126             return mkForall(sorts, names, body, weight, patterns, noPatterns,
02127                     quantifierID, skolemID);
02128         else
02129             return mkExists(sorts, names, body, weight, patterns, noPatterns,
02130                     quantifierID, skolemID);
02131     }
02132 
02136     public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
02137             Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
02138             Symbol quantifierID, Symbol skolemID) throws Z3Exception
02139     {
02140 
02141         if (universal)
02142             return mkForall(boundConstants, body, weight, patterns, noPatterns,
02143                     quantifierID, skolemID);
02144         else
02145             return mkExists(boundConstants, body, weight, patterns, noPatterns,
02146                     quantifierID, skolemID);
02147     }
02148 
02160     public void setPrintMode(Z3_ast_print_mode value) throws Z3Exception
02161     {
02162         Native.setAstPrintMode(nCtx(), value.toInt());
02163     }
02164 
02177     public String benchmarkToSMTString(String name, String logic,
02178             String status, String attributes, BoolExpr[] assumptions,
02179             BoolExpr formula) throws Z3Exception
02180     {
02181 
02182         return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
02183                 attributes, (int) assumptions.length,
02184                 AST.arrayToNative(assumptions), formula.getNativeObject());
02185     }
02186 
02196     public void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts,
02197             Symbol[] declNames, FuncDecl[] decls) throws Z3Exception
02198     {
02199         int csn = Symbol.arrayLength(sortNames);
02200         int cs = Sort.arrayLength(sorts);
02201         int cdn = Symbol.arrayLength(declNames);
02202         int cd = AST.arrayLength(decls);
02203         if (csn != cs || cdn != cd)
02204             throw new Z3Exception("Argument size mismatch");
02205         Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
02206                 Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
02207                 AST.arrayLength(decls), Symbol.arrayToNative(declNames),
02208                 AST.arrayToNative(decls));
02209     }
02210 
02215     public void parseSMTLIBFile(String fileName, Symbol[] sortNames,
02216             Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
02217             throws Z3Exception
02218     {
02219         int csn = Symbol.arrayLength(sortNames);
02220         int cs = Sort.arrayLength(sorts);
02221         int cdn = Symbol.arrayLength(declNames);
02222         int cd = AST.arrayLength(decls);
02223         if (csn != cs || cdn != cd)
02224             throw new Z3Exception("Argument size mismatch");
02225         Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
02226                 Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
02227                 AST.arrayLength(decls), Symbol.arrayToNative(declNames),
02228                 AST.arrayToNative(decls));
02229     }
02230 
02235     public int getNumSMTLIBFormulas() throws Z3Exception
02236     {
02237         return Native.getSmtlibNumFormulas(nCtx());
02238     }
02239 
02244     public BoolExpr[] getSMTLIBFormulas() throws Z3Exception
02245     {
02246 
02247         int n = getNumSMTLIBFormulas();
02248         BoolExpr[] res = new BoolExpr[n];
02249         for (int i = 0; i < n; i++)
02250             res[i] = (BoolExpr) Expr.create(this,
02251                     Native.getSmtlibFormula(nCtx(), i));
02252         return res;
02253     }
02254 
02259     public int getNumSMTLIBAssumptions() throws Z3Exception
02260     {
02261         return Native.getSmtlibNumAssumptions(nCtx());
02262     }
02263 
02268     public BoolExpr[] getSMTLIBAssumptions() throws Z3Exception
02269     {
02270 
02271         int n = getNumSMTLIBAssumptions();
02272         BoolExpr[] res = new BoolExpr[n];
02273         for (int i = 0; i < n; i++)
02274             res[i] = (BoolExpr) Expr.create(this,
02275                     Native.getSmtlibAssumption(nCtx(), i));
02276         return res;
02277     }
02278 
02283     public int getNumSMTLIBDecls() throws Z3Exception
02284     {
02285         return Native.getSmtlibNumDecls(nCtx());
02286     }
02287 
02292     public FuncDecl[] getSMTLIBDecls() throws Z3Exception
02293     {
02294 
02295         int n = getNumSMTLIBDecls();
02296         FuncDecl[] res = new FuncDecl[n];
02297         for (int i = 0; i < n; i++)
02298             res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
02299         return res;
02300     }
02301 
02306     public int getNumSMTLIBSorts() throws Z3Exception
02307     {
02308         return Native.getSmtlibNumSorts(nCtx());
02309     }
02310 
02315     public Sort[] getSMTLIBSorts() throws Z3Exception
02316     {
02317 
02318         int n = getNumSMTLIBSorts();
02319         Sort[] res = new Sort[n];
02320         for (int i = 0; i < n; i++)
02321             res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
02322         return res;
02323     }
02324 
02332     public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
02333             Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
02334             throws Z3Exception
02335     {
02336 
02337         int csn = Symbol.arrayLength(sortNames);
02338         int cs = Sort.arrayLength(sorts);
02339         int cdn = Symbol.arrayLength(declNames);
02340         int cd = AST.arrayLength(decls);
02341         if (csn != cs || cdn != cd)
02342             throw new Z3Exception("Argument size mismatch");
02343         return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
02344                 str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
02345                 AST.arrayToNative(sorts), AST.arrayLength(decls),
02346                 Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
02347     }
02348 
02353     public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
02354             Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
02355             throws Z3Exception
02356     {
02357 
02358         int csn = Symbol.arrayLength(sortNames);
02359         int cs = Sort.arrayLength(sorts);
02360         int cdn = Symbol.arrayLength(declNames);
02361         int cd = AST.arrayLength(decls);
02362         if (csn != cs || cdn != cd)
02363             throw new Z3Exception("Argument size mismatch");
02364         return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
02365                 fileName, AST.arrayLength(sorts),
02366                 Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
02367                 AST.arrayLength(decls), Symbol.arrayToNative(declNames),
02368                 AST.arrayToNative(decls)));
02369     }
02370 
02380     public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
02381             throws Z3Exception
02382     {
02383 
02384         return new Goal(this, models, unsatCores, proofs);
02385     }
02386 
02390     public Params mkParams() throws Z3Exception
02391     {
02392 
02393         return new Params(this);
02394     }
02395 
02399     public int getNumTactics() throws Z3Exception
02400     {
02401         return Native.getNumTactics(nCtx());
02402     }
02403 
02407     public String[] getTacticNames() throws Z3Exception
02408     {
02409 
02410         int n = getNumTactics();
02411         String[] res = new String[n];
02412         for (int i = 0; i < n; i++)
02413             res[i] = Native.getTacticName(nCtx(), i);
02414         return res;
02415     }
02416 
02421     public String getTacticDescription(String name) throws Z3Exception
02422     {
02423 
02424         return Native.tacticGetDescr(nCtx(), name);
02425     }
02426 
02430     public Tactic mkTactic(String name) throws Z3Exception
02431     {
02432 
02433         return new Tactic(this, name);
02434     }
02435 
02440     public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
02441             throws Z3Exception
02442     {
02443         checkContextMatch(t1);
02444         checkContextMatch(t2);
02445         checkContextMatch(ts);
02446 
02447         long last = 0;
02448         if (ts != null && ts.length > 0)
02449         {
02450             last = ts[ts.length - 1].getNativeObject();
02451             for (int i = ts.length - 2; i >= 0; i--)
02452                 last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
02453                         last);
02454         }
02455         if (last != 0)
02456         {
02457             last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
02458             return new Tactic(this, Native.tacticAndThen(nCtx(),
02459                     t1.getNativeObject(), last));
02460         } else
02461             return new Tactic(this, Native.tacticAndThen(nCtx(),
02462                     t1.getNativeObject(), t2.getNativeObject()));
02463     }
02464 
02470     public Tactic then(Tactic t1, Tactic t2, Tactic... ts) throws Z3Exception
02471     {
02472         return andThen(t1, t2, ts);
02473     }
02474 
02480     public Tactic orElse(Tactic t1, Tactic t2) throws Z3Exception
02481     {
02482 
02483         checkContextMatch(t1);
02484         checkContextMatch(t2);
02485         return new Tactic(this, Native.tacticOrElse(nCtx(),
02486                 t1.getNativeObject(), t2.getNativeObject()));
02487     }
02488 
02495     public Tactic tryFor(Tactic t, int ms) throws Z3Exception
02496     {
02497 
02498         checkContextMatch(t);
02499         return new Tactic(this, Native.tacticTryFor(nCtx(),
02500                 t.getNativeObject(), ms));
02501     }
02502 
02509     public Tactic when(Probe p, Tactic t) throws Z3Exception
02510     {
02511 
02512         checkContextMatch(t);
02513         checkContextMatch(p);
02514         return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
02515                 t.getNativeObject()));
02516     }
02517 
02523     public Tactic cond(Probe p, Tactic t1, Tactic t2) throws Z3Exception
02524     {
02525 
02526         checkContextMatch(p);
02527         checkContextMatch(t1);
02528         checkContextMatch(t2);
02529         return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
02530                 t1.getNativeObject(), t2.getNativeObject()));
02531     }
02532 
02538     public Tactic repeat(Tactic t, int max) throws Z3Exception
02539     {
02540 
02541         checkContextMatch(t);
02542         return new Tactic(this, Native.tacticRepeat(nCtx(),
02543                 t.getNativeObject(), max));
02544     }
02545 
02549     public Tactic skip() throws Z3Exception
02550     {
02551 
02552         return new Tactic(this, Native.tacticSkip(nCtx()));
02553     }
02554 
02558     public Tactic fail() throws Z3Exception
02559     {
02560 
02561         return new Tactic(this, Native.tacticFail(nCtx()));
02562     }
02563 
02568     public Tactic failIf(Probe p) throws Z3Exception
02569     {
02570 
02571         checkContextMatch(p);
02572         return new Tactic(this,
02573                 Native.tacticFailIf(nCtx(), p.getNativeObject()));
02574     }
02575 
02580     public Tactic failIfNotDecided() throws Z3Exception
02581     {
02582         return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
02583     }
02584 
02589     public Tactic usingParams(Tactic t, Params p) throws Z3Exception
02590     {
02591         checkContextMatch(t);
02592         checkContextMatch(p);
02593         return new Tactic(this, Native.tacticUsingParams(nCtx(),
02594                 t.getNativeObject(), p.getNativeObject()));
02595     }
02596 
02602     public Tactic with(Tactic t, Params p) throws Z3Exception
02603     {
02604         return usingParams(t, p);
02605     }
02606 
02610     public Tactic parOr(Tactic... t) throws Z3Exception
02611     {
02612         checkContextMatch(t);
02613         return new Tactic(this, Native.tacticParOr(nCtx(),
02614                 Tactic.arrayLength(t), Tactic.arrayToNative(t)));
02615     }
02616 
02622     public Tactic parAndThen(Tactic t1, Tactic t2) throws Z3Exception
02623     {
02624 
02625         checkContextMatch(t1);
02626         checkContextMatch(t2);
02627         return new Tactic(this, Native.tacticParAndThen(nCtx(),
02628                 t1.getNativeObject(), t2.getNativeObject()));
02629     }
02630 
02635     public void interrupt() throws Z3Exception
02636     {
02637         Native.interrupt(nCtx());
02638     }
02639 
02643     public int getNumProbes() throws Z3Exception
02644     {
02645         return Native.getNumProbes(nCtx());
02646     }
02647 
02651     public String[] getProbeNames() throws Z3Exception
02652     {
02653 
02654         int n = getNumProbes();
02655         String[] res = new String[n];
02656         for (int i = 0; i < n; i++)
02657             res[i] = Native.getProbeName(nCtx(), i);
02658         return res;
02659     }
02660 
02665     public String getProbeDescription(String name) throws Z3Exception
02666     {
02667         return Native.probeGetDescr(nCtx(), name);
02668     }
02669 
02673     public Probe mkProbe(String name) throws Z3Exception
02674     {
02675         return new Probe(this, name);
02676     }
02677 
02681     public Probe constProbe(double val) throws Z3Exception
02682     {
02683         return new Probe(this, Native.probeConst(nCtx(), val));
02684     }
02685 
02691     public Probe lt(Probe p1, Probe p2) throws Z3Exception
02692     {
02693 
02694         checkContextMatch(p1);
02695         checkContextMatch(p2);
02696         return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
02697                 p2.getNativeObject()));
02698     }
02699 
02705     public Probe gt(Probe p1, Probe p2) throws Z3Exception
02706     {
02707 
02708         checkContextMatch(p1);
02709         checkContextMatch(p2);
02710         return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
02711                 p2.getNativeObject()));
02712     }
02713 
02719     public Probe le(Probe p1, Probe p2) throws Z3Exception
02720     {
02721 
02722         checkContextMatch(p1);
02723         checkContextMatch(p2);
02724         return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
02725                 p2.getNativeObject()));
02726     }
02727 
02733     public Probe ge(Probe p1, Probe p2) throws Z3Exception
02734     {
02735         checkContextMatch(p1);
02736         checkContextMatch(p2);
02737         return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
02738                 p2.getNativeObject()));
02739     }
02740 
02746     public Probe eq(Probe p1, Probe p2) throws Z3Exception
02747     {
02748         checkContextMatch(p1);
02749         checkContextMatch(p2);
02750         return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
02751                 p2.getNativeObject()));
02752     }
02753 
02758     public Probe and(Probe p1, Probe p2) throws Z3Exception
02759     {
02760         checkContextMatch(p1);
02761         checkContextMatch(p2);
02762         return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
02763                 p2.getNativeObject()));
02764     }
02765 
02770     public Probe or(Probe p1, Probe p2) throws Z3Exception
02771     {
02772         checkContextMatch(p1);
02773         checkContextMatch(p2);
02774         return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
02775                 p2.getNativeObject()));
02776     }
02777 
02782     public Probe not(Probe p) throws Z3Exception
02783     {
02784 
02785         checkContextMatch(p);
02786         return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
02787     }
02788 
02795     public Solver mkSolver() throws Z3Exception
02796     {
02797         return mkSolver((Symbol) null);
02798     }
02799 
02806     public Solver mkSolver(Symbol logic) throws Z3Exception
02807     {
02808 
02809         if (logic == null)
02810             return new Solver(this, Native.mkSolver(nCtx()));
02811         else
02812             return new Solver(this, Native.mkSolverForLogic(nCtx(),
02813                     logic.getNativeObject()));
02814     }
02815 
02819     public Solver mkSolver(String logic) throws Z3Exception
02820     {
02821 
02822         return mkSolver(mkSymbol(logic));
02823     }
02824 
02828     public Solver mkSimpleSolver() throws Z3Exception
02829     {
02830 
02831         return new Solver(this, Native.mkSimpleSolver(nCtx()));
02832     }
02833 
02839     public Solver mkSolver(Tactic t) throws Z3Exception
02840     {
02841 
02842         return new Solver(this, Native.mkSolverFromTactic(nCtx(),
02843                 t.getNativeObject()));
02844     }
02845 
02849     public Fixedpoint mkFixedpoint() throws Z3Exception
02850     {
02851 
02852         return new Fixedpoint(this);
02853     }
02854 
02864     public AST wrapAST(long nativeObject) throws Z3Exception
02865     {
02866 
02867         return AST.create(this, nativeObject);
02868     }
02869 
02879     public long unwrapAST(AST a)
02880     {
02881         return a.getNativeObject();
02882     }
02883 
02888     public String SimplifyHelp() throws Z3Exception
02889     {
02890 
02891         return Native.simplifyGetHelp(nCtx());
02892     }
02893 
02897     public ParamDescrs getSimplifyParameterDescriptions() throws Z3Exception
02898     {
02899         return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
02900     }
02901 
02907     public static void ToggleWarningMessages(boolean enabled)
02908             throws Z3Exception
02909     {
02910         Native.toggleWarningMessages((enabled) ? true : false);
02911     }
02912 
02920     public void updateParamValue(String id, String value) throws Z3Exception
02921     {
02922         Native.updateParamValue(nCtx(), id, value);
02923     }
02924 
02925     long m_ctx = 0;
02926 
02927     long nCtx()
02928     {
02929         return m_ctx;
02930     }
02931 
02932     void initContext() throws Z3Exception
02933     {
02934         setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
02935         Native.setInternalErrorHandler(nCtx());
02936     }
02937 
02938     void checkContextMatch(Z3Object other) throws Z3Exception
02939     {
02940         if (this != other.getContext())
02941             throw new Z3Exception("Context mismatch");
02942     }
02943 
02944     void checkContextMatch(Z3Object[] arr) throws Z3Exception
02945     {
02946         if (arr != null)
02947             for (Z3Object a : arr)
02948                 checkContextMatch(a);
02949     }
02950 
02951     private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
02952     private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
02953     private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
02954     private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
02955     private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
02956     private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
02957     private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
02958     private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
02959     private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
02960     private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
02961     private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
02962     private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
02963     private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
02964     private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
02965     private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
02966 
02967     ASTDecRefQueue ast_DRQ()
02968     {
02969         return m_AST_DRQ;
02970     }
02971 
02972     ASTMapDecRefQueue astmap_DRQ()
02973     {
02974         return m_ASTMap_DRQ;
02975     }
02976 
02977     ASTVectorDecRefQueue astvector_DRQ()
02978     {
02979         return m_ASTVector_DRQ;
02980     }
02981 
02982     ApplyResultDecRefQueue applyResult_DRQ()
02983     {
02984         return m_ApplyResult_DRQ;
02985     }
02986 
02987     FuncInterpEntryDecRefQueue funcEntry_DRQ()
02988     {
02989         return m_FuncEntry_DRQ;
02990     }
02991 
02992     FuncInterpDecRefQueue funcInterp_DRQ()
02993     {
02994         return m_FuncInterp_DRQ;
02995     }
02996 
02997     GoalDecRefQueue goal_DRQ()
02998     {
02999         return m_Goal_DRQ;
03000     }
03001 
03002     ModelDecRefQueue model_DRQ()
03003     {
03004         return m_Model_DRQ;
03005     }
03006 
03007     ParamsDecRefQueue params_DRQ()
03008     {
03009         return m_Params_DRQ;
03010     }
03011 
03012     ParamDescrsDecRefQueue paramDescrs_DRQ()
03013     {
03014         return m_ParamDescrs_DRQ;
03015     }
03016 
03017     ProbeDecRefQueue probe_DRQ()
03018     {
03019         return m_Probe_DRQ;
03020     }
03021 
03022     SolverDecRefQueue solver_DRQ()
03023     {
03024         return m_Solver_DRQ;
03025     }
03026 
03027     StatisticsDecRefQueue statistics_DRQ()
03028     {
03029         return m_Statistics_DRQ;
03030     }
03031 
03032     TacticDecRefQueue tactic_DRQ()
03033     {
03034         return m_Tactic_DRQ;
03035     }
03036 
03037     FixedpointDecRefQueue fixedpoint_DRQ()
03038     {
03039         return m_Fixedpoint_DRQ;
03040     }
03041 
03042     protected long m_refCount = 0;
03043 
03047     protected void finalize()
03048     {
03049         dispose();
03050 
03051         if (m_refCount == 0)
03052         {
03053             try
03054             {
03055                 Native.delContext(m_ctx);
03056             } catch (Z3Exception e)
03057             {
03058                 // OK.
03059             }
03060             m_ctx = 0;
03061         } 
03062         /*
03063         else
03064             CMW: re-queue the finalizer? */
03065     }
03066 
03070     public void dispose()
03071     {
03072         m_AST_DRQ.clear(this);
03073         m_ASTMap_DRQ.clear(this);
03074         m_ASTVector_DRQ.clear(this);
03075         m_ApplyResult_DRQ.clear(this);
03076         m_FuncEntry_DRQ.clear(this);
03077         m_FuncInterp_DRQ.clear(this);
03078         m_Goal_DRQ.clear(this);
03079         m_Model_DRQ.clear(this);
03080         m_Params_DRQ.clear(this);
03081         m_Probe_DRQ.clear(this);
03082         m_Solver_DRQ.clear(this);
03083         m_Statistics_DRQ.clear(this);
03084         m_Tactic_DRQ.clear(this);
03085         m_Fixedpoint_DRQ.clear(this);
03086 
03087         m_boolSort = null;
03088         m_intSort = null;
03089         m_realSort = null;
03090     }
03091 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines