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
03059 }
03060 m_ctx = 0;
03061 }
03062
03063
03064
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 }