Z3
Context.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
20 import java.util.Map;
21 
23 
27 public class Context extends IDisposable
28 {
32  public Context() throws Z3Exception
33  {
34  super();
35  m_ctx = Native.mkContextRc(0);
36  initContext();
37  }
38 
57  public Context(Map<String, String> settings) throws Z3Exception
58  {
59  super();
60  long cfg = Native.mkConfig();
61  for (Map.Entry<String, String> kv : settings.entrySet())
62  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
63  m_ctx = Native.mkContextRc(cfg);
64  Native.delConfig(cfg);
65  initContext();
66  }
67 
73  public IntSymbol mkSymbol(int i) throws Z3Exception
74  {
75  return new IntSymbol(this, i);
76  }
77 
81  public StringSymbol mkSymbol(String name) throws Z3Exception
82  {
83  return new StringSymbol(this, name);
84  }
85 
89  Symbol[] MkSymbols(String[] names) throws Z3Exception
90  {
91  if (names == null)
92  return null;
93  Symbol[] result = new Symbol[names.length];
94  for (int i = 0; i < names.length; ++i)
95  result[i] = mkSymbol(names[i]);
96  return result;
97  }
98 
99  private BoolSort m_boolSort = null;
100  private IntSort m_intSort = null;
101  private RealSort m_realSort = null;
102 
107  {
108  if (m_boolSort == null)
109  m_boolSort = new BoolSort(this);
110  return m_boolSort;
111  }
112 
117  {
118  if (m_intSort == null)
119  m_intSort = new IntSort(this);
120  return m_intSort;
121  }
122 
127  {
128  if (m_realSort == null)
129  m_realSort = new RealSort(this);
130  return m_realSort;
131  }
132 
137  {
138 
139  return new BoolSort(this);
140  }
141 
146  {
147 
148  checkContextMatch(s);
149  return new UninterpretedSort(this, s);
150  }
151 
156  {
157 
158  return mkUninterpretedSort(mkSymbol(str));
159  }
160 
164  public IntSort mkIntSort() throws Z3Exception
165  {
166 
167  return new IntSort(this);
168  }
169 
174  {
175 
176  return new RealSort(this);
177  }
178 
182  public BitVecSort mkBitVecSort(int size) throws Z3Exception
183  {
184 
185  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
186  }
187 
191  public ArraySort mkArraySort(Sort domain, Sort range) throws Z3Exception
192  {
193 
194  checkContextMatch(domain);
195  checkContextMatch(range);
196  return new ArraySort(this, domain, range);
197  }
198 
202  public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames,
203  Sort[] fieldSorts) throws Z3Exception
204  {
205 
206  checkContextMatch(name);
207  checkContextMatch(fieldNames);
208  checkContextMatch(fieldSorts);
209  return new TupleSort(this, name, (int) fieldNames.length, fieldNames,
210  fieldSorts);
211  }
212 
216  public EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
217  throws Z3Exception
218  {
219 
220  checkContextMatch(name);
221  checkContextMatch(enumNames);
222  return new EnumSort(this, name, enumNames);
223  }
224 
228  public EnumSort mkEnumSort(String name, String... enumNames)
229  throws Z3Exception
230  {
231  return new EnumSort(this, mkSymbol(name), MkSymbols(enumNames));
232  }
233 
237  public ListSort mkListSort(Symbol name, Sort elemSort) throws Z3Exception
238  {
239 
240  checkContextMatch(name);
241  checkContextMatch(elemSort);
242  return new ListSort(this, name, elemSort);
243  }
244 
248  public ListSort mkListSort(String name, Sort elemSort) throws Z3Exception
249  {
250 
251  checkContextMatch(elemSort);
252  return new ListSort(this, mkSymbol(name), elemSort);
253  }
254 
259  throws Z3Exception
260  {
261 
262  checkContextMatch(name);
263  return new FiniteDomainSort(this, name, size);
264  }
265 
269  public FiniteDomainSort mkFiniteDomainSort(String name, long size)
270  throws Z3Exception
271  {
272 
273  return new FiniteDomainSort(this, mkSymbol(name), size);
274  }
275 
287  public Constructor mkConstructor(Symbol name, Symbol recognizer,
288  Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
289  throws Z3Exception
290  {
291 
292  return new Constructor(this, name, recognizer, fieldNames, sorts,
293  sortRefs);
294  }
295 
303  public Constructor mkConstructor(String name, String recognizer,
304  String[] fieldNames, Sort[] sorts, int[] sortRefs)
305  throws Z3Exception
306  {
307 
308  return new Constructor(this, mkSymbol(name), mkSymbol(recognizer),
309  MkSymbols(fieldNames), sorts, sortRefs);
310  }
311 
315  public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
316  throws Z3Exception
317  {
318 
319  checkContextMatch(name);
320  checkContextMatch(constructors);
321  return new DatatypeSort(this, name, constructors);
322  }
323 
327  public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
328  throws Z3Exception
329  {
330 
331  checkContextMatch(constructors);
332  return new DatatypeSort(this, mkSymbol(name), constructors);
333  }
334 
341  throws Z3Exception
342  {
343 
344  checkContextMatch(names);
345  int n = (int) names.length;
346  ConstructorList[] cla = new ConstructorList[n];
347  long[] n_constr = new long[n];
348  for (int i = 0; i < n; i++)
349  {
350  Constructor[] constructor = c[i];
351 
352  checkContextMatch(constructor);
353  cla[i] = new ConstructorList(this, constructor);
354  n_constr[i] = cla[i].getNativeObject();
355  }
356  long[] n_res = new long[n];
357  Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
358  n_constr);
359  DatatypeSort[] res = new DatatypeSort[n];
360  for (int i = 0; i < n; i++)
361  res[i] = new DatatypeSort(this, n_res[i]);
362  return res;
363  }
364 
371  public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
372  throws Z3Exception
373  {
374 
375  return mkDatatypeSorts(MkSymbols(names), c);
376  }
377 
381  public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
382  throws Z3Exception
383  {
384 
385  checkContextMatch(name);
386  checkContextMatch(domain);
387  checkContextMatch(range);
388  return new FuncDecl(this, name, domain, range);
389  }
390 
394  public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
395  throws Z3Exception
396  {
397 
398  checkContextMatch(name);
399  checkContextMatch(domain);
400  checkContextMatch(range);
401  Sort[] q = new Sort[] { domain };
402  return new FuncDecl(this, name, q, range);
403  }
404 
408  public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
409  throws Z3Exception
410  {
411 
412  checkContextMatch(domain);
413  checkContextMatch(range);
414  return new FuncDecl(this, mkSymbol(name), domain, range);
415  }
416 
420  public FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
421  throws Z3Exception
422  {
423 
424  checkContextMatch(domain);
425  checkContextMatch(range);
426  Sort[] q = new Sort[] { domain };
427  return new FuncDecl(this, mkSymbol(name), q, range);
428  }
429 
435  public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
436  throws Z3Exception
437  {
438 
439  checkContextMatch(domain);
440  checkContextMatch(range);
441  return new FuncDecl(this, prefix, domain, range);
442  }
443 
447  public FuncDecl mkConstDecl(Symbol name, Sort range) throws Z3Exception
448  {
449 
450  checkContextMatch(name);
451  checkContextMatch(range);
452  return new FuncDecl(this, name, null, range);
453  }
454 
458  public FuncDecl mkConstDecl(String name, Sort range) throws Z3Exception
459  {
460 
461  checkContextMatch(range);
462  return new FuncDecl(this, mkSymbol(name), null, range);
463  }
464 
470  public FuncDecl mkFreshConstDecl(String prefix, Sort range)
471  throws Z3Exception
472  {
473 
474  checkContextMatch(range);
475  return new FuncDecl(this, prefix, null, range);
476  }
477 
482  public Expr mkBound(int index, Sort ty) throws Z3Exception
483  {
484  return Expr.create(this,
485  Native.mkBound(nCtx(), index, ty.getNativeObject()));
486  }
487 
491  public Pattern mkPattern(Expr... terms) throws Z3Exception
492  {
493  if (terms.length == 0)
494  throw new Z3Exception("Cannot create a pattern from zero terms");
495 
496  long[] termsNative = AST.arrayToNative(terms);
497  return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length,
498  termsNative));
499  }
500 
505  public Expr mkConst(Symbol name, Sort range) throws Z3Exception
506  {
507 
508  checkContextMatch(name);
509  checkContextMatch(range);
510 
511  return Expr.create(
512  this,
513  Native.mkConst(nCtx(), name.getNativeObject(),
514  range.getNativeObject()));
515  }
516 
521  public Expr mkConst(String name, Sort range) throws Z3Exception
522  {
523 
524  return mkConst(mkSymbol(name), range);
525  }
526 
531  public Expr mkFreshConst(String prefix, Sort range) throws Z3Exception
532  {
533 
534  checkContextMatch(range);
535  return Expr.create(this,
536  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
537  }
538 
543  public Expr mkConst(FuncDecl f) throws Z3Exception
544  {
545 
546  return mkApp(f, (Expr[]) null);
547  }
548 
553  {
554 
555  return (BoolExpr) mkConst(name, getBoolSort());
556  }
557 
561  public BoolExpr mkBoolConst(String name) throws Z3Exception
562  {
563 
564  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
565  }
566 
570  public IntExpr mkIntConst(Symbol name) throws Z3Exception
571  {
572 
573  return (IntExpr) mkConst(name, getIntSort());
574  }
575 
579  public IntExpr mkIntConst(String name) throws Z3Exception
580  {
581 
582  return (IntExpr) mkConst(name, getIntSort());
583  }
584 
589  {
590 
591  return (RealExpr) mkConst(name, getRealSort());
592  }
593 
597  public RealExpr mkRealConst(String name) throws Z3Exception
598  {
599 
600  return (RealExpr) mkConst(name, getRealSort());
601  }
602 
606  public BitVecExpr mkBVConst(Symbol name, int size) throws Z3Exception
607  {
608 
609  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
610  }
611 
615  public BitVecExpr mkBVConst(String name, int size) throws Z3Exception
616  {
617 
618  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
619  }
620 
624  public Expr mkApp(FuncDecl f, Expr... args) throws Z3Exception
625  {
626  checkContextMatch(f);
627  checkContextMatch(args);
628  return Expr.create(this, f, args);
629  }
630 
634  public BoolExpr mkTrue() throws Z3Exception
635  {
636  return new BoolExpr(this, Native.mkTrue(nCtx()));
637  }
638 
642  public BoolExpr mkFalse() throws Z3Exception
643  {
644  return new BoolExpr(this, Native.mkFalse(nCtx()));
645  }
646 
650  public BoolExpr mkBool(boolean value) throws Z3Exception
651  {
652  return value ? mkTrue() : mkFalse();
653  }
654 
658  public BoolExpr mkEq(Expr x, Expr y) throws Z3Exception
659  {
660  checkContextMatch(x);
661  checkContextMatch(y);
662  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
663  y.getNativeObject()));
664  }
665 
669  public BoolExpr mkDistinct(Expr... args) throws Z3Exception
670  {
671  checkContextMatch(args);
672  return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length,
673  AST.arrayToNative(args)));
674  }
675 
680  {
681 
682  checkContextMatch(a);
683  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
684  }
685 
692  public Expr mkITE(BoolExpr t1, Expr t2, Expr t3) throws Z3Exception
693  {
694 
695  checkContextMatch(t1);
696  checkContextMatch(t2);
697  checkContextMatch(t3);
698  return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
699  t2.getNativeObject(), t3.getNativeObject()));
700  }
701 
706  {
707 
708  checkContextMatch(t1);
709  checkContextMatch(t2);
710  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
711  t2.getNativeObject()));
712  }
713 
718  {
719 
720  checkContextMatch(t1);
721  checkContextMatch(t2);
722  return new BoolExpr(this, Native.mkImplies(nCtx(),
723  t1.getNativeObject(), t2.getNativeObject()));
724  }
725 
730  {
731 
732  checkContextMatch(t1);
733  checkContextMatch(t2);
734  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
735  t2.getNativeObject()));
736  }
737 
741  public BoolExpr mkAnd(BoolExpr... t) throws Z3Exception
742  {
743 
744  checkContextMatch(t);
745  return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length,
746  AST.arrayToNative(t)));
747  }
748 
752  public BoolExpr mkOr(BoolExpr... t) throws Z3Exception
753  {
754 
755  checkContextMatch(t);
756  return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length,
757  AST.arrayToNative(t)));
758  }
759 
763  public ArithExpr mkAdd(ArithExpr... t) throws Z3Exception
764  {
765 
766  checkContextMatch(t);
767  return (ArithExpr) Expr.create(this,
768  Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t)));
769  }
770 
774  public ArithExpr mkMul(ArithExpr... t) throws Z3Exception
775  {
776 
777  checkContextMatch(t);
778  return (ArithExpr) Expr.create(this,
779  Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t)));
780  }
781 
785  public ArithExpr mkSub(ArithExpr... t) throws Z3Exception
786  {
787 
788  checkContextMatch(t);
789  return (ArithExpr) Expr.create(this,
790  Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t)));
791  }
792 
797  {
798 
799  checkContextMatch(t);
800  return (ArithExpr) Expr.create(this,
801  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
802  }
803 
808  {
809 
810  checkContextMatch(t1);
811  checkContextMatch(t2);
812  return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
813  t1.getNativeObject(), t2.getNativeObject()));
814  }
815 
820  public IntExpr mkMod(IntExpr t1, IntExpr t2) throws Z3Exception
821  {
822 
823  checkContextMatch(t1);
824  checkContextMatch(t2);
825  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
826  t2.getNativeObject()));
827  }
828 
833  public IntExpr mkRem(IntExpr t1, IntExpr t2) throws Z3Exception
834  {
835 
836  checkContextMatch(t1);
837  checkContextMatch(t2);
838  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
839  t2.getNativeObject()));
840  }
841 
846  {
847 
848  checkContextMatch(t1);
849  checkContextMatch(t2);
850  return (ArithExpr) Expr.create(
851  this,
852  Native.mkPower(nCtx(), t1.getNativeObject(),
853  t2.getNativeObject()));
854  }
855 
860  {
861 
862  checkContextMatch(t1);
863  checkContextMatch(t2);
864  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
865  t2.getNativeObject()));
866  }
867 
872  {
873 
874  checkContextMatch(t1);
875  checkContextMatch(t2);
876  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
877  t2.getNativeObject()));
878  }
879 
884  {
885 
886  checkContextMatch(t1);
887  checkContextMatch(t2);
888  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
889  t2.getNativeObject()));
890  }
891 
896  {
897 
898  checkContextMatch(t1);
899  checkContextMatch(t2);
900  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
901  t2.getNativeObject()));
902  }
903 
914  {
915 
916  checkContextMatch(t);
917  return new RealExpr(this,
918  Native.mkInt2real(nCtx(), t.getNativeObject()));
919  }
920 
927  {
928 
929  checkContextMatch(t);
930  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
931  }
932 
937  {
938 
939  checkContextMatch(t);
940  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
941  }
942 
948  {
949 
950  checkContextMatch(t);
951  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
952  }
953 
959  {
960 
961  checkContextMatch(t);
962  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
963  t.getNativeObject()));
964  }
965 
971  {
972 
973  checkContextMatch(t);
974  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
975  t.getNativeObject()));
976  }
977 
983  {
984 
985  checkContextMatch(t1);
986  checkContextMatch(t2);
987  return new BitVecExpr(this, Native.mkBvand(nCtx(),
988  t1.getNativeObject(), t2.getNativeObject()));
989  }
990 
996  {
997 
998  checkContextMatch(t1);
999  checkContextMatch(t2);
1000  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1001  t2.getNativeObject()));
1002  }
1003 
1009  {
1010 
1011  checkContextMatch(t1);
1012  checkContextMatch(t2);
1013  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1014  t1.getNativeObject(), t2.getNativeObject()));
1015  }
1016 
1022  {
1023 
1024  checkContextMatch(t1);
1025  checkContextMatch(t2);
1026  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1027  t1.getNativeObject(), t2.getNativeObject()));
1028  }
1029 
1035  {
1036 
1037  checkContextMatch(t1);
1038  checkContextMatch(t2);
1039  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1040  t1.getNativeObject(), t2.getNativeObject()));
1041  }
1042 
1048  {
1049 
1050  checkContextMatch(t1);
1051  checkContextMatch(t2);
1052  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1053  t1.getNativeObject(), t2.getNativeObject()));
1054  }
1055 
1061  {
1062 
1063  checkContextMatch(t);
1064  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1065  }
1066 
1072  {
1073 
1074  checkContextMatch(t1);
1075  checkContextMatch(t2);
1076  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1077  t1.getNativeObject(), t2.getNativeObject()));
1078  }
1079 
1085  {
1086 
1087  checkContextMatch(t1);
1088  checkContextMatch(t2);
1089  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1090  t1.getNativeObject(), t2.getNativeObject()));
1091  }
1092 
1098  {
1099 
1100  checkContextMatch(t1);
1101  checkContextMatch(t2);
1102  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1103  t1.getNativeObject(), t2.getNativeObject()));
1104  }
1105 
1113  {
1114 
1115  checkContextMatch(t1);
1116  checkContextMatch(t2);
1117  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1118  t1.getNativeObject(), t2.getNativeObject()));
1119  }
1120 
1134  {
1135 
1136  checkContextMatch(t1);
1137  checkContextMatch(t2);
1138  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1139  t1.getNativeObject(), t2.getNativeObject()));
1140  }
1141 
1149  {
1150 
1151  checkContextMatch(t1);
1152  checkContextMatch(t2);
1153  return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1154  t1.getNativeObject(), t2.getNativeObject()));
1155  }
1156 
1167  {
1168 
1169  checkContextMatch(t1);
1170  checkContextMatch(t2);
1171  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1172  t1.getNativeObject(), t2.getNativeObject()));
1173  }
1174 
1181  {
1182 
1183  checkContextMatch(t1);
1184  checkContextMatch(t2);
1185  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1186  t1.getNativeObject(), t2.getNativeObject()));
1187  }
1188 
1194  {
1195 
1196  checkContextMatch(t1);
1197  checkContextMatch(t2);
1198  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1199  t2.getNativeObject()));
1200  }
1201 
1207  {
1208 
1209  checkContextMatch(t1);
1210  checkContextMatch(t2);
1211  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1212  t2.getNativeObject()));
1213  }
1214 
1220  {
1221 
1222  checkContextMatch(t1);
1223  checkContextMatch(t2);
1224  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1225  t2.getNativeObject()));
1226  }
1227 
1233  {
1234 
1235  checkContextMatch(t1);
1236  checkContextMatch(t2);
1237  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1238  t2.getNativeObject()));
1239  }
1240 
1246  {
1247 
1248  checkContextMatch(t1);
1249  checkContextMatch(t2);
1250  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1251  t2.getNativeObject()));
1252  }
1253 
1259  {
1260 
1261  checkContextMatch(t1);
1262  checkContextMatch(t2);
1263  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1264  t2.getNativeObject()));
1265  }
1266 
1272  {
1273 
1274  checkContextMatch(t1);
1275  checkContextMatch(t2);
1276  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1277  t2.getNativeObject()));
1278  }
1279 
1285  {
1286 
1287  checkContextMatch(t1);
1288  checkContextMatch(t2);
1289  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1290  t2.getNativeObject()));
1291  }
1292 
1303  {
1304 
1305  checkContextMatch(t1);
1306  checkContextMatch(t2);
1307  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1308  t1.getNativeObject(), t2.getNativeObject()));
1309  }
1310 
1318  public BitVecExpr mkExtract(int high, int low, BitVecExpr t)
1319  throws Z3Exception
1320  {
1321 
1322  checkContextMatch(t);
1323  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1324  t.getNativeObject()));
1325  }
1326 
1333  public BitVecExpr mkSignExt(int i, BitVecExpr t) throws Z3Exception
1334  {
1335 
1336  checkContextMatch(t);
1337  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1338  t.getNativeObject()));
1339  }
1340 
1347  public BitVecExpr mkZeroExt(int i, BitVecExpr t) throws Z3Exception
1348  {
1349 
1350  checkContextMatch(t);
1351  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1352  t.getNativeObject()));
1353  }
1354 
1359  public BitVecExpr mkRepeat(int i, BitVecExpr t) throws Z3Exception
1360  {
1361 
1362  checkContextMatch(t);
1363  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1364  t.getNativeObject()));
1365  }
1366 
1378  {
1379 
1380  checkContextMatch(t1);
1381  checkContextMatch(t2);
1382  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1383  t1.getNativeObject(), t2.getNativeObject()));
1384  }
1385 
1397  {
1398 
1399  checkContextMatch(t1);
1400  checkContextMatch(t2);
1401  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1402  t1.getNativeObject(), t2.getNativeObject()));
1403  }
1404 
1417  {
1418 
1419  checkContextMatch(t1);
1420  checkContextMatch(t2);
1421  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1422  t1.getNativeObject(), t2.getNativeObject()));
1423  }
1424 
1430  {
1431 
1432  checkContextMatch(t);
1433  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1434  t.getNativeObject()));
1435  }
1436 
1442  {
1443 
1444  checkContextMatch(t);
1445  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1446  t.getNativeObject()));
1447  }
1448 
1455  throws Z3Exception
1456  {
1457 
1458  checkContextMatch(t1);
1459  checkContextMatch(t2);
1460  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1461  t1.getNativeObject(), t2.getNativeObject()));
1462  }
1463 
1470  throws Z3Exception
1471  {
1472 
1473  checkContextMatch(t1);
1474  checkContextMatch(t2);
1475  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1476  t1.getNativeObject(), t2.getNativeObject()));
1477  }
1478 
1487  public BitVecExpr mkInt2BV(int n, IntExpr t) throws Z3Exception
1488  {
1489 
1490  checkContextMatch(t);
1491  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1492  t.getNativeObject()));
1493  }
1494 
1509  public IntExpr mkBV2Int(BitVecExpr t, boolean signed) throws Z3Exception
1510  {
1511 
1512  checkContextMatch(t);
1513  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1514  (signed) ? true : false));
1515  }
1516 
1522  boolean isSigned) throws Z3Exception
1523  {
1524 
1525  checkContextMatch(t1);
1526  checkContextMatch(t2);
1527  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1528  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1529  : false));
1530  }
1531 
1537  throws Z3Exception
1538  {
1539 
1540  checkContextMatch(t1);
1541  checkContextMatch(t2);
1542  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1543  t1.getNativeObject(), t2.getNativeObject()));
1544  }
1545 
1551  throws Z3Exception
1552  {
1553 
1554  checkContextMatch(t1);
1555  checkContextMatch(t2);
1556  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1557  t1.getNativeObject(), t2.getNativeObject()));
1558  }
1559 
1565  boolean isSigned) throws Z3Exception
1566  {
1567 
1568  checkContextMatch(t1);
1569  checkContextMatch(t2);
1570  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1571  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1572  : false));
1573  }
1574 
1580  throws Z3Exception
1581  {
1582 
1583  checkContextMatch(t1);
1584  checkContextMatch(t2);
1585  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1586  t1.getNativeObject(), t2.getNativeObject()));
1587  }
1588 
1594  {
1595 
1596  checkContextMatch(t);
1597  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1598  t.getNativeObject()));
1599  }
1600 
1606  boolean isSigned) throws Z3Exception
1607  {
1608 
1609  checkContextMatch(t1);
1610  checkContextMatch(t2);
1611  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1612  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1613  : false));
1614  }
1615 
1621  throws Z3Exception
1622  {
1623 
1624  checkContextMatch(t1);
1625  checkContextMatch(t2);
1626  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1627  t1.getNativeObject(), t2.getNativeObject()));
1628  }
1629 
1633  public ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
1634  throws Z3Exception
1635  {
1636 
1637  return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1638  }
1639 
1643  public ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
1644  throws Z3Exception
1645  {
1646 
1647  return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1648  }
1649 
1660  {
1661 
1662  checkContextMatch(a);
1663  checkContextMatch(i);
1664  return Expr.create(
1665  this,
1666  Native.mkSelect(nCtx(), a.getNativeObject(),
1667  i.getNativeObject()));
1668  }
1669 
1684  {
1685 
1686  checkContextMatch(a);
1687  checkContextMatch(i);
1688  checkContextMatch(v);
1689  return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1690  i.getNativeObject(), v.getNativeObject()));
1691  }
1692 
1699  public ArrayExpr mkConstArray(Sort domain, Expr v) throws Z3Exception
1700  {
1701 
1702  checkContextMatch(domain);
1703  checkContextMatch(v);
1704  return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1705  domain.getNativeObject(), v.getNativeObject()));
1706  }
1707 
1717  public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args) throws Z3Exception
1718  {
1719 
1720  checkContextMatch(f);
1721  checkContextMatch(args);
1722  return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1723  f.getNativeObject(), AST.arrayLength(args),
1724  AST.arrayToNative(args)));
1725  }
1726 
1732  public Expr mkTermArray(ArrayExpr array) throws Z3Exception
1733  {
1734 
1735  checkContextMatch(array);
1736  return Expr.create(this,
1737  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1738  }
1739 
1743  public SetSort mkSetSort(Sort ty) throws Z3Exception
1744  {
1745 
1746  checkContextMatch(ty);
1747  return new SetSort(this, ty);
1748  }
1749 
1753  public Expr mkEmptySet(Sort domain) throws Z3Exception
1754  {
1755 
1756  checkContextMatch(domain);
1757  return Expr.create(this,
1758  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1759  }
1760 
1764  public Expr mkFullSet(Sort domain) throws Z3Exception
1765  {
1766 
1767  checkContextMatch(domain);
1768  return Expr.create(this,
1769  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1770  }
1771 
1775  public Expr mkSetAdd(Expr set, Expr element) throws Z3Exception
1776  {
1777 
1778  checkContextMatch(set);
1779  checkContextMatch(element);
1780  return Expr.create(
1781  this,
1782  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1783  element.getNativeObject()));
1784  }
1785 
1789  public Expr mkSetDel(Expr set, Expr element) throws Z3Exception
1790  {
1791 
1792  checkContextMatch(set);
1793  checkContextMatch(element);
1794  return Expr.create(
1795  this,
1796  Native.mkSetDel(nCtx(), set.getNativeObject(),
1797  element.getNativeObject()));
1798  }
1799 
1803  public Expr mkSetUnion(Expr... args) throws Z3Exception
1804  {
1805 
1806  checkContextMatch(args);
1807  return Expr.create(
1808  this,
1809  Native.mkSetUnion(nCtx(), (int) args.length,
1810  AST.arrayToNative(args)));
1811  }
1812 
1816  public Expr mkSetIntersection(Expr... args) throws Z3Exception
1817  {
1818 
1819  checkContextMatch(args);
1820  return Expr.create(
1821  this,
1822  Native.mkSetIntersect(nCtx(), (int) args.length,
1823  AST.arrayToNative(args)));
1824  }
1825 
1829  public Expr mkSetDifference(Expr arg1, Expr arg2) throws Z3Exception
1830  {
1831 
1832  checkContextMatch(arg1);
1833  checkContextMatch(arg2);
1834  return Expr.create(
1835  this,
1836  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1837  arg2.getNativeObject()));
1838  }
1839 
1844  {
1845 
1846  checkContextMatch(arg);
1847  return Expr.create(this,
1848  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1849  }
1850 
1854  public Expr mkSetMembership(Expr elem, Expr set) throws Z3Exception
1855  {
1856 
1857  checkContextMatch(elem);
1858  checkContextMatch(set);
1859  return Expr.create(
1860  this,
1861  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1862  set.getNativeObject()));
1863  }
1864 
1868  public Expr mkSetSubset(Expr arg1, Expr arg2) throws Z3Exception
1869  {
1870 
1871  checkContextMatch(arg1);
1872  checkContextMatch(arg2);
1873  return Expr.create(
1874  this,
1875  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1876  arg2.getNativeObject()));
1877  }
1878 
1890  public Expr mkNumeral(String v, Sort ty) throws Z3Exception
1891  {
1892 
1893  checkContextMatch(ty);
1894  return Expr.create(this,
1895  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
1896  }
1897 
1908  public Expr mkNumeral(int v, Sort ty) throws Z3Exception
1909  {
1910 
1911  checkContextMatch(ty);
1912  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
1913  }
1914 
1925  public Expr mkNumeral(long v, Sort ty) throws Z3Exception
1926  {
1927 
1928  checkContextMatch(ty);
1929  return Expr.create(this,
1930  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
1931  }
1932 
1940  public RatNum mkReal(int num, int den) throws Z3Exception
1941  {
1942  if (den == 0)
1943  throw new Z3Exception("Denominator is zero");
1944 
1945  return new RatNum(this, Native.mkReal(nCtx(), num, den));
1946  }
1947 
1954  public RatNum mkReal(String v) throws Z3Exception
1955  {
1956 
1957  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
1958  .getNativeObject()));
1959  }
1960 
1966  public RatNum mkReal(int v) throws Z3Exception
1967  {
1968 
1969  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
1970  .getNativeObject()));
1971  }
1972 
1978  public RatNum mkReal(long v) throws Z3Exception
1979  {
1980 
1981  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
1982  .getNativeObject()));
1983  }
1984 
1989  public IntNum mkInt(String v) throws Z3Exception
1990  {
1991 
1992  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
1993  .getNativeObject()));
1994  }
1995 
2001  public IntNum mkInt(int v) throws Z3Exception
2002  {
2003 
2004  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2005  .getNativeObject()));
2006  }
2007 
2013  public IntNum mkInt(long v) throws Z3Exception
2014  {
2015 
2016  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2017  .getNativeObject()));
2018  }
2019 
2025  public BitVecNum mkBV(String v, int size) throws Z3Exception
2026  {
2027 
2028  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2029  }
2030 
2035  public BitVecNum mkBV(int v, int size) throws Z3Exception
2036  {
2037 
2038  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2039  }
2040 
2045  public BitVecNum mkBV(long v, int size) throws Z3Exception
2046  {
2047 
2048  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2049  }
2050 
2070  public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
2071  int weight, Pattern[] patterns, Expr[] noPatterns,
2072  Symbol quantifierID, Symbol skolemID) throws Z3Exception
2073  {
2074 
2075  return new Quantifier(this, true, sorts, names, body, weight, patterns,
2076  noPatterns, quantifierID, skolemID);
2077  }
2078 
2082  public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
2083  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2084  Symbol skolemID) throws Z3Exception
2085  {
2086 
2087  return new Quantifier(this, true, boundConstants, body, weight,
2088  patterns, noPatterns, quantifierID, skolemID);
2089  }
2090 
2095  public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
2096  int weight, Pattern[] patterns, Expr[] noPatterns,
2097  Symbol quantifierID, Symbol skolemID) throws Z3Exception
2098  {
2099 
2100  return new Quantifier(this, false, sorts, names, body, weight,
2101  patterns, noPatterns, quantifierID, skolemID);
2102  }
2103 
2107  public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
2108  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2109  Symbol skolemID) throws Z3Exception
2110  {
2111 
2112  return new Quantifier(this, false, boundConstants, body, weight,
2113  patterns, noPatterns, quantifierID, skolemID);
2114  }
2115 
2119  public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
2120  Symbol[] names, Expr body, int weight, Pattern[] patterns,
2121  Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
2122  throws Z3Exception
2123  {
2124 
2125  if (universal)
2126  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2127  quantifierID, skolemID);
2128  else
2129  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2130  quantifierID, skolemID);
2131  }
2132 
2136  public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
2137  Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
2138  Symbol quantifierID, Symbol skolemID) throws Z3Exception
2139  {
2140 
2141  if (universal)
2142  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2143  quantifierID, skolemID);
2144  else
2145  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2146  quantifierID, skolemID);
2147  }
2148 
2160  public void setPrintMode(Z3_ast_print_mode value) throws Z3Exception
2161  {
2162  Native.setAstPrintMode(nCtx(), value.toInt());
2163  }
2164 
2177  public String benchmarkToSMTString(String name, String logic,
2178  String status, String attributes, BoolExpr[] assumptions,
2179  BoolExpr formula) throws Z3Exception
2180  {
2181 
2182  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2183  attributes, (int) assumptions.length,
2184  AST.arrayToNative(assumptions), formula.getNativeObject());
2185  }
2186 
2196  public void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts,
2197  Symbol[] declNames, FuncDecl[] decls) throws Z3Exception
2198  {
2199  int csn = Symbol.arrayLength(sortNames);
2200  int cs = Sort.arrayLength(sorts);
2201  int cdn = Symbol.arrayLength(declNames);
2202  int cd = AST.arrayLength(decls);
2203  if (csn != cs || cdn != cd)
2204  throw new Z3Exception("Argument size mismatch");
2205  Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
2206  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2207  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2208  AST.arrayToNative(decls));
2209  }
2210 
2215  public void parseSMTLIBFile(String fileName, Symbol[] sortNames,
2216  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2217  throws Z3Exception
2218  {
2219  int csn = Symbol.arrayLength(sortNames);
2220  int cs = Sort.arrayLength(sorts);
2221  int cdn = Symbol.arrayLength(declNames);
2222  int cd = AST.arrayLength(decls);
2223  if (csn != cs || cdn != cd)
2224  throw new Z3Exception("Argument size mismatch");
2225  Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
2226  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2227  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2228  AST.arrayToNative(decls));
2229  }
2230 
2235  public int getNumSMTLIBFormulas() throws Z3Exception
2236  {
2237  return Native.getSmtlibNumFormulas(nCtx());
2238  }
2239 
2245  {
2246 
2247  int n = getNumSMTLIBFormulas();
2248  BoolExpr[] res = new BoolExpr[n];
2249  for (int i = 0; i < n; i++)
2250  res[i] = (BoolExpr) Expr.create(this,
2251  Native.getSmtlibFormula(nCtx(), i));
2252  return res;
2253  }
2254 
2260  {
2261  return Native.getSmtlibNumAssumptions(nCtx());
2262  }
2263 
2269  {
2270 
2271  int n = getNumSMTLIBAssumptions();
2272  BoolExpr[] res = new BoolExpr[n];
2273  for (int i = 0; i < n; i++)
2274  res[i] = (BoolExpr) Expr.create(this,
2275  Native.getSmtlibAssumption(nCtx(), i));
2276  return res;
2277  }
2278 
2283  public int getNumSMTLIBDecls() throws Z3Exception
2284  {
2285  return Native.getSmtlibNumDecls(nCtx());
2286  }
2287 
2293  {
2294 
2295  int n = getNumSMTLIBDecls();
2296  FuncDecl[] res = new FuncDecl[n];
2297  for (int i = 0; i < n; i++)
2298  res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
2299  return res;
2300  }
2301 
2306  public int getNumSMTLIBSorts() throws Z3Exception
2307  {
2308  return Native.getSmtlibNumSorts(nCtx());
2309  }
2310 
2315  public Sort[] getSMTLIBSorts() throws Z3Exception
2316  {
2317 
2318  int n = getNumSMTLIBSorts();
2319  Sort[] res = new Sort[n];
2320  for (int i = 0; i < n; i++)
2321  res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
2322  return res;
2323  }
2324 
2332  public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
2333  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2334  throws Z3Exception
2335  {
2336 
2337  int csn = Symbol.arrayLength(sortNames);
2338  int cs = Sort.arrayLength(sorts);
2339  int cdn = Symbol.arrayLength(declNames);
2340  int cd = AST.arrayLength(decls);
2341  if (csn != cs || cdn != cd)
2342  throw new Z3Exception("Argument size mismatch");
2343  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2344  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2345  AST.arrayToNative(sorts), AST.arrayLength(decls),
2346  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2347  }
2348 
2353  public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
2354  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2355  throws Z3Exception
2356  {
2357 
2358  int csn = Symbol.arrayLength(sortNames);
2359  int cs = Sort.arrayLength(sorts);
2360  int cdn = Symbol.arrayLength(declNames);
2361  int cd = AST.arrayLength(decls);
2362  if (csn != cs || cdn != cd)
2363  throw new Z3Exception("Argument size mismatch");
2364  return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
2365  fileName, AST.arrayLength(sorts),
2366  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2367  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2368  AST.arrayToNative(decls)));
2369  }
2370 
2380  public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
2381  throws Z3Exception
2382  {
2383 
2384  return new Goal(this, models, unsatCores, proofs);
2385  }
2386 
2390  public Params mkParams() throws Z3Exception
2391  {
2392 
2393  return new Params(this);
2394  }
2395 
2399  public int getNumTactics() throws Z3Exception
2400  {
2401  return Native.getNumTactics(nCtx());
2402  }
2403 
2407  public String[] getTacticNames() throws Z3Exception
2408  {
2409 
2410  int n = getNumTactics();
2411  String[] res = new String[n];
2412  for (int i = 0; i < n; i++)
2413  res[i] = Native.getTacticName(nCtx(), i);
2414  return res;
2415  }
2416 
2421  public String getTacticDescription(String name) throws Z3Exception
2422  {
2423 
2424  return Native.tacticGetDescr(nCtx(), name);
2425  }
2426 
2430  public Tactic mkTactic(String name) throws Z3Exception
2431  {
2432 
2433  return new Tactic(this, name);
2434  }
2435 
2440  public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
2441  throws Z3Exception
2442  {
2443  checkContextMatch(t1);
2444  checkContextMatch(t2);
2445  checkContextMatch(ts);
2446 
2447  long last = 0;
2448  if (ts != null && ts.length > 0)
2449  {
2450  last = ts[ts.length - 1].getNativeObject();
2451  for (int i = ts.length - 2; i >= 0; i--)
2452  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2453  last);
2454  }
2455  if (last != 0)
2456  {
2457  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2458  return new Tactic(this, Native.tacticAndThen(nCtx(),
2459  t1.getNativeObject(), last));
2460  } else
2461  return new Tactic(this, Native.tacticAndThen(nCtx(),
2462  t1.getNativeObject(), t2.getNativeObject()));
2463  }
2464 
2470  public Tactic then(Tactic t1, Tactic t2, Tactic... ts) throws Z3Exception
2471  {
2472  return andThen(t1, t2, ts);
2473  }
2474 
2480  public Tactic orElse(Tactic t1, Tactic t2) throws Z3Exception
2481  {
2482 
2483  checkContextMatch(t1);
2484  checkContextMatch(t2);
2485  return new Tactic(this, Native.tacticOrElse(nCtx(),
2486  t1.getNativeObject(), t2.getNativeObject()));
2487  }
2488 
2495  public Tactic tryFor(Tactic t, int ms) throws Z3Exception
2496  {
2497 
2498  checkContextMatch(t);
2499  return new Tactic(this, Native.tacticTryFor(nCtx(),
2500  t.getNativeObject(), ms));
2501  }
2502 
2509  public Tactic when(Probe p, Tactic t) throws Z3Exception
2510  {
2511 
2512  checkContextMatch(t);
2513  checkContextMatch(p);
2514  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2515  t.getNativeObject()));
2516  }
2517 
2523  public Tactic cond(Probe p, Tactic t1, Tactic t2) throws Z3Exception
2524  {
2525 
2526  checkContextMatch(p);
2527  checkContextMatch(t1);
2528  checkContextMatch(t2);
2529  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2530  t1.getNativeObject(), t2.getNativeObject()));
2531  }
2532 
2538  public Tactic repeat(Tactic t, int max) throws Z3Exception
2539  {
2540 
2541  checkContextMatch(t);
2542  return new Tactic(this, Native.tacticRepeat(nCtx(),
2543  t.getNativeObject(), max));
2544  }
2545 
2549  public Tactic skip() throws Z3Exception
2550  {
2551 
2552  return new Tactic(this, Native.tacticSkip(nCtx()));
2553  }
2554 
2558  public Tactic fail() throws Z3Exception
2559  {
2560 
2561  return new Tactic(this, Native.tacticFail(nCtx()));
2562  }
2563 
2568  public Tactic failIf(Probe p) throws Z3Exception
2569  {
2570 
2571  checkContextMatch(p);
2572  return new Tactic(this,
2573  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2574  }
2575 
2581  {
2582  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2583  }
2584 
2590  {
2591  checkContextMatch(t);
2592  checkContextMatch(p);
2593  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2594  t.getNativeObject(), p.getNativeObject()));
2595  }
2596 
2602  public Tactic with(Tactic t, Params p) throws Z3Exception
2603  {
2604  return usingParams(t, p);
2605  }
2606 
2610  public Tactic parOr(Tactic... t) throws Z3Exception
2611  {
2612  checkContextMatch(t);
2613  return new Tactic(this, Native.tacticParOr(nCtx(),
2614  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2615  }
2616 
2623  {
2624 
2625  checkContextMatch(t1);
2626  checkContextMatch(t2);
2627  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2628  t1.getNativeObject(), t2.getNativeObject()));
2629  }
2630 
2635  public void interrupt() throws Z3Exception
2636  {
2637  Native.interrupt(nCtx());
2638  }
2639 
2643  public int getNumProbes() throws Z3Exception
2644  {
2645  return Native.getNumProbes(nCtx());
2646  }
2647 
2651  public String[] getProbeNames() throws Z3Exception
2652  {
2653 
2654  int n = getNumProbes();
2655  String[] res = new String[n];
2656  for (int i = 0; i < n; i++)
2657  res[i] = Native.getProbeName(nCtx(), i);
2658  return res;
2659  }
2660 
2665  public String getProbeDescription(String name) throws Z3Exception
2666  {
2667  return Native.probeGetDescr(nCtx(), name);
2668  }
2669 
2673  public Probe mkProbe(String name) throws Z3Exception
2674  {
2675  return new Probe(this, name);
2676  }
2677 
2681  public Probe constProbe(double val) throws Z3Exception
2682  {
2683  return new Probe(this, Native.probeConst(nCtx(), val));
2684  }
2685 
2691  public Probe lt(Probe p1, Probe p2) throws Z3Exception
2692  {
2693 
2694  checkContextMatch(p1);
2695  checkContextMatch(p2);
2696  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2697  p2.getNativeObject()));
2698  }
2699 
2705  public Probe gt(Probe p1, Probe p2) throws Z3Exception
2706  {
2707 
2708  checkContextMatch(p1);
2709  checkContextMatch(p2);
2710  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2711  p2.getNativeObject()));
2712  }
2713 
2719  public Probe le(Probe p1, Probe p2) throws Z3Exception
2720  {
2721 
2722  checkContextMatch(p1);
2723  checkContextMatch(p2);
2724  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2725  p2.getNativeObject()));
2726  }
2727 
2733  public Probe ge(Probe p1, Probe p2) throws Z3Exception
2734  {
2735  checkContextMatch(p1);
2736  checkContextMatch(p2);
2737  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2738  p2.getNativeObject()));
2739  }
2740 
2746  public Probe eq(Probe p1, Probe p2) throws Z3Exception
2747  {
2748  checkContextMatch(p1);
2749  checkContextMatch(p2);
2750  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2751  p2.getNativeObject()));
2752  }
2753 
2758  public Probe and(Probe p1, Probe p2) throws Z3Exception
2759  {
2760  checkContextMatch(p1);
2761  checkContextMatch(p2);
2762  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
2763  p2.getNativeObject()));
2764  }
2765 
2770  public Probe or(Probe p1, Probe p2) throws Z3Exception
2771  {
2772  checkContextMatch(p1);
2773  checkContextMatch(p2);
2774  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
2775  p2.getNativeObject()));
2776  }
2777 
2782  public Probe not(Probe p) throws Z3Exception
2783  {
2784 
2785  checkContextMatch(p);
2786  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2787  }
2788 
2795  public Solver mkSolver() throws Z3Exception
2796  {
2797  return mkSolver((Symbol) null);
2798  }
2799 
2806  public Solver mkSolver(Symbol logic) throws Z3Exception
2807  {
2808 
2809  if (logic == null)
2810  return new Solver(this, Native.mkSolver(nCtx()));
2811  else
2812  return new Solver(this, Native.mkSolverForLogic(nCtx(),
2813  logic.getNativeObject()));
2814  }
2815 
2819  public Solver mkSolver(String logic) throws Z3Exception
2820  {
2821 
2822  return mkSolver(mkSymbol(logic));
2823  }
2824 
2829  {
2830 
2831  return new Solver(this, Native.mkSimpleSolver(nCtx()));
2832  }
2833 
2840  {
2841 
2842  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
2843  t.getNativeObject()));
2844  }
2845 
2850  {
2851 
2852  return new Fixedpoint(this);
2853  }
2854 
2864  public AST wrapAST(long nativeObject) throws Z3Exception
2865  {
2866 
2867  return AST.create(this, nativeObject);
2868  }
2869 
2879  public long unwrapAST(AST a)
2880  {
2881  return a.getNativeObject();
2882  }
2883 
2888  public String SimplifyHelp() throws Z3Exception
2889  {
2890 
2891  return Native.simplifyGetHelp(nCtx());
2892  }
2893 
2898  {
2899  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
2900  }
2901 
2907  public static void ToggleWarningMessages(boolean enabled)
2908  throws Z3Exception
2909  {
2910  Native.toggleWarningMessages((enabled) ? true : false);
2911  }
2912 
2920  public void updateParamValue(String id, String value) throws Z3Exception
2921  {
2922  Native.updateParamValue(nCtx(), id, value);
2923  }
2924 
2925  long m_ctx = 0;
2926 
2927  long nCtx()
2928  {
2929  return m_ctx;
2930  }
2931 
2932  void initContext() throws Z3Exception
2933  {
2934  setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
2935  Native.setInternalErrorHandler(nCtx());
2936  }
2937 
2938  void checkContextMatch(Z3Object other) throws Z3Exception
2939  {
2940  if (this != other.getContext())
2941  throw new Z3Exception("Context mismatch");
2942  }
2943 
2944  void checkContextMatch(Z3Object[] arr) throws Z3Exception
2945  {
2946  if (arr != null)
2947  for (Z3Object a : arr)
2948  checkContextMatch(a);
2949  }
2950 
2951  private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
2952  private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
2953  private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
2954  private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
2955  private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
2956  private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
2957  private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
2958  private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
2959  private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
2960  private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
2961  private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
2962  private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
2963  private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
2964  private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
2965  private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
2966 
2967  ASTDecRefQueue ast_DRQ()
2968  {
2969  return m_AST_DRQ;
2970  }
2971 
2972  ASTMapDecRefQueue astmap_DRQ()
2973  {
2974  return m_ASTMap_DRQ;
2975  }
2976 
2977  ASTVectorDecRefQueue astvector_DRQ()
2978  {
2979  return m_ASTVector_DRQ;
2980  }
2981 
2982  ApplyResultDecRefQueue applyResult_DRQ()
2983  {
2984  return m_ApplyResult_DRQ;
2985  }
2986 
2987  FuncInterpEntryDecRefQueue funcEntry_DRQ()
2988  {
2989  return m_FuncEntry_DRQ;
2990  }
2991 
2992  FuncInterpDecRefQueue funcInterp_DRQ()
2993  {
2994  return m_FuncInterp_DRQ;
2995  }
2996 
2997  GoalDecRefQueue goal_DRQ()
2998  {
2999  return m_Goal_DRQ;
3000  }
3001 
3002  ModelDecRefQueue model_DRQ()
3003  {
3004  return m_Model_DRQ;
3005  }
3006 
3007  ParamsDecRefQueue params_DRQ()
3008  {
3009  return m_Params_DRQ;
3010  }
3011 
3012  ParamDescrsDecRefQueue paramDescrs_DRQ()
3013  {
3014  return m_ParamDescrs_DRQ;
3015  }
3016 
3017  ProbeDecRefQueue probe_DRQ()
3018  {
3019  return m_Probe_DRQ;
3020  }
3021 
3022  SolverDecRefQueue solver_DRQ()
3023  {
3024  return m_Solver_DRQ;
3025  }
3026 
3027  StatisticsDecRefQueue statistics_DRQ()
3028  {
3029  return m_Statistics_DRQ;
3030  }
3031 
3032  TacticDecRefQueue tactic_DRQ()
3033  {
3034  return m_Tactic_DRQ;
3035  }
3036 
3037  FixedpointDecRefQueue fixedpoint_DRQ()
3038  {
3039  return m_Fixedpoint_DRQ;
3040  }
3041 
3042  protected long m_refCount = 0;
3043 
3047  protected void finalize()
3048  {
3049  dispose();
3050 
3051  if (m_refCount == 0)
3052  {
3053  try
3054  {
3055  Native.delContext(m_ctx);
3056  } catch (Z3Exception e)
3057  {
3058  // OK.
3059  }
3060  m_ctx = 0;
3061  }
3062  /*
3063  else
3064  CMW: re-queue the finalizer? */
3065  }
3066 
3070  public void dispose()
3071  {
3072  m_AST_DRQ.clear(this);
3073  m_ASTMap_DRQ.clear(this);
3074  m_ASTVector_DRQ.clear(this);
3075  m_ApplyResult_DRQ.clear(this);
3076  m_FuncEntry_DRQ.clear(this);
3077  m_FuncInterp_DRQ.clear(this);
3078  m_Goal_DRQ.clear(this);
3079  m_Model_DRQ.clear(this);
3080  m_Params_DRQ.clear(this);
3081  m_Probe_DRQ.clear(this);
3082  m_Solver_DRQ.clear(this);
3083  m_Statistics_DRQ.clear(this);
3084  m_Tactic_DRQ.clear(this);
3085  m_Fixedpoint_DRQ.clear(this);
3086 
3087  m_boolSort = null;
3088  m_intSort = null;
3089  m_realSort = null;
3090  }
3091 }
IntExpr mkIntConst(Symbol name)
Definition: Context.java:570
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1605
static long tacticRepeat(long a0, long a1, int a2)
Definition: Native.java:3861
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
Definition: Context.java:692
static long mkBvule(long a0, long a1, long a2)
Definition: Native.java:1391
static long mkSolver(long a0)
Definition: Native.java:4147
def RealSort
Definition: z3py.py:2630
Tactic when(Probe p, Tactic t)
Definition: Context.java:2509
RatNum mkReal(String v)
Definition: Context.java:1954
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1047
static long mkExtract(long a0, int a1, int a2, long a3)
Definition: Native.java:1454
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
Definition: Context.java:327
static void interrupt(long a0)
Definition: Native.java:631
static long getSmtlibSort(long a0, int a1)
Definition: Native.java:3140
Probe and(Probe p1, Probe p2)
Definition: Context.java:2758
static long mkMod(long a0, long a1, long a2)
Definition: Native.java:1121
static long mkBvugt(long a0, long a1, long a2)
Definition: Native.java:1427
static void delConfig(long a0)
Definition: Native.java:576
ArrayExpr mkConstArray(Sort domain, Expr v)
Definition: Context.java:1699
static int getSmtlibNumSorts(long a0)
Definition: Native.java:3131
Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
Definition: Context.java:287
static long mkBvredor(long a0, long a1)
Definition: Native.java:1229
static long tacticOrElse(long a0, long a1, long a2)
Definition: Native.java:3807
Probe lt(Probe p1, Probe p2)
Definition: Context.java:2691
BoolExpr mkDistinct(Expr...args)
Definition: Context.java:669
static int getNumProbes(long a0)
Definition: Native.java:4014
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1245
static void parseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3069
static long mkNumeral(long a0, String a1, long a2)
Definition: Native.java:1787
BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1377
def IntSort
Definition: z3py.py:2614
static void updateParamValue(long a0, String a1, String a2)
Definition: Native.java:623
static void toggleWarningMessages(boolean a0)
Definition: Native.java:2976
def BoolSort
Definition: z3py.py:1325
BitVecExpr mkBVNeg(BitVecExpr t)
Definition: Context.java:1060
static long mkFreshConst(long a0, String a1, long a2)
Definition: Native.java:968
ArithExpr mkSub(ArithExpr...t)
Definition: Context.java:785
static long mkConfig()
Definition: Native.java:570
Expr mkNumeral(int v, Sort ty)
Definition: Context.java:1908
BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1579
ListSort mkListSort(String name, Sort elemSort)
Definition: Context.java:248
Expr mkSetAdd(Expr set, Expr element)
Definition: Context.java:1775
StringSymbol mkSymbol(String name)
Definition: Context.java:81
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1571
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1071
Probe eq(Probe p1, Probe p2)
Definition: Context.java:2746
def BitVecSort
Definition: z3py.py:3435
BitVecExpr mkZeroExt(int i, BitVecExpr t)
Definition: Context.java:1347
static long mkOr(long a0, int a1, long[] a2)
Definition: Native.java:1067
BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1454
Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2107
String getProbeDescription(String name)
Definition: Context.java:2665
IntNum mkInt(String v)
Definition: Context.java:1989
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1112
BoolExpr mkAnd(BoolExpr...t)
Definition: Context.java:741
static long mkSub(long a0, int a1, long[] a2)
Definition: Native.java:1094
static long tacticFailIf(long a0, long a1)
Definition: Native.java:3888
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1416
static long mkExtRotateLeft(long a0, long a1, long a2)
Definition: Native.java:1535
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
Definition: Context.java:717
static long mkBvlshr(long a0, long a1, long a2)
Definition: Native.java:1499
BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2332
BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1620
BitVecExpr mkExtract(int high, int low, BitVecExpr t)
Definition: Context.java:1318
UninterpretedSort mkUninterpretedSort(String str)
Definition: Context.java:155
BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1180
static String probeGetDescr(long a0, String a1)
Definition: Native.java:4059
static long mkBvuge(long a0, long a1, long a2)
Definition: Native.java:1409
static long mkSolverForLogic(long a0, long a1)
Definition: Native.java:4165
static long getSmtlibDecl(long a0, int a1)
Definition: Native.java:3122
static long simplifyGetParamDescrs(long a0)
Definition: Native.java:2687
static long mkLe(long a0, long a1, long a2)
Definition: Native.java:1157
static long mkSetIntersect(long a0, int a1, long[] a2)
Definition: Native.java:1742
static long mkConcat(long a0, long a1, long a2)
Definition: Native.java:1445
static long mkSelect(long a0, long a1, long a2)
Definition: Native.java:1643
static long mkBvnand(long a0, long a1, long a2)
Definition: Native.java:1265
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1469
BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2353
static long probeEq(long a0, long a1, long a2)
Definition: Native.java:3960
static long mkGe(long a0, long a1, long a2)
Definition: Native.java:1175
static long mkXor(long a0, long a1, long a2)
Definition: Native.java:1049
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1890
BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1148
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Definition: Context.java:202
BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1097
static long mkBvslt(long a0, long a1, long a2)
Definition: Native.java:1382
FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
Definition: Context.java:408
void setPrintMode(Z3_ast_print_mode value)
Definition: Context.java:2160
static long mkAdd(long a0, int a1, long[] a2)
Definition: Native.java:1076
static int getSmtlibNumFormulas(long a0)
Definition: Native.java:3077
FuncDecl mkConstDecl(String name, Sort range)
Definition: Context.java:458
Expr mkSetDifference(Expr arg1, Expr arg2)
Definition: Context.java:1829
static long probeOr(long a0, long a1, long a2)
Definition: Native.java:3978
SetSort mkSetSort(Sort ty)
Definition: Context.java:1743
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:859
IntExpr mkReal2Int(RealExpr t)
Definition: Context.java:926
Expr mkSetComplement(Expr arg)
Definition: Context.java:1843
RatNum mkReal(int v)
Definition: Context.java:1966
static long probeNot(long a0, long a1)
Definition: Native.java:3987
static long mkSignExt(long a0, int a1, long a2)
Definition: Native.java:1463
static long mkBvsmod(long a0, long a1, long a2)
Definition: Native.java:1364
AST wrapAST(long nativeObject)
Definition: Context.java:2864
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1580
static long mkSetComplement(long a0, long a1)
Definition: Native.java:1760
static long mkInt(long a0, int a1, long a2)
Definition: Native.java:1805
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
Definition: Context.java:394
static long probeConst(long a0, double a1)
Definition: Native.java:3915
static long mkSetAdd(long a0, long a1, long a2)
Definition: Native.java:1715
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1625
static long mkBvneg(long a0, long a1)
Definition: Native.java:1292
static long mkInt64(long a0, long a1, long a2)
Definition: Native.java:1823
static long mkBvsdiv(long a0, long a1, long a2)
Definition: Native.java:1337
static long mkMap(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1670
static int getNumTactics(long a0)
Definition: Native.java:3996
static long mkZeroExt(long a0, int a1, long a2)
Definition: Native.java:1472
static long mkBvnot(long a0, long a1)
Definition: Native.java:1211
static long mkDistinct(long a0, int a1, long[] a2)
Definition: Native.java:1004
BoolExpr mkIsInteger(RealExpr t)
Definition: Context.java:936
static long mkUnaryMinus(long a0, long a1)
Definition: Native.java:1103
BoolExpr mkBVNegNoOverflow(BitVecExpr t)
Definition: Context.java:1593
static long mkSetDifference(long a0, long a1, long a2)
Definition: Native.java:1751
static long mkBvsgt(long a0, long a1, long a2)
Definition: Native.java:1436
static long mkSetDel(long a0, long a1, long a2)
Definition: Native.java:1724
static long mkRotateRight(long a0, int a1, long a2)
Definition: Native.java:1526
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1598
static long mkStore(long a0, long a1, long a2, long a3)
Definition: Native.java:1652
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2119
Probe gt(Probe p1, Probe p2)
Definition: Context.java:2705
static long mkSolverFromTactic(long a0, long a1)
Definition: Native.java:4174
BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1232
static long mkBvadd(long a0, long a1, long a2)
Definition: Native.java:1301
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1536
static void delContext(long a0)
Definition: Native.java:602
static long mkBvsle(long a0, long a1, long a2)
Definition: Native.java:1400
BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:995
BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1008
BitVecExpr mkBVNot(BitVecExpr t)
Definition: Context.java:947
BitVecExpr mkBVRedOR(BitVecExpr t)
Definition: Context.java:970
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2589
BitVecExpr mkBVConst(String name, int size)
Definition: Context.java:615
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:871
static void setAstPrintMode(long a0, int a1)
Definition: Native.java:2981
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1133
static long mkDiv(long a0, long a1, long a2)
Definition: Native.java:1112
static long mkIte(long a0, long a1, long a2, long a3)
Definition: Native.java:1022
static String tacticGetDescr(long a0, String a1)
Definition: Native.java:4050
static long tacticFailIfNotDecided(long a0)
Definition: Native.java:3897
ArrayExpr mkMap(FuncDecl f, ArrayExpr...args)
Definition: Context.java:1717
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1284
static long mkSimpleSolver(long a0)
Definition: Native.java:4156
static long mkSetMember(long a0, long a1, long a2)
Definition: Native.java:1769
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2082
BoolExpr mkBoolConst(String name)
Definition: Context.java:561
BitVecExpr mkRepeat(int i, BitVecExpr t)
Definition: Context.java:1359
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1021
void updateParamValue(String id, String value)
Definition: Context.java:2920
Probe mkProbe(String name)
Definition: Context.java:2673
BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
Definition: Context.java:729
BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1396
static long tacticParOr(long a0, int a1, long[] a2)
Definition: Native.java:3816
static long tacticSkip(long a0)
Definition: Native.java:3870
static int getSmtlibNumDecls(long a0)
Definition: Native.java:3113
static long mkBvurem(long a0, long a1, long a2)
Definition: Native.java:1346
Tactic repeat(Tactic t, int max)
Definition: Context.java:2538
static long mkSetSubset(long a0, long a1, long a2)
Definition: Native.java:1778
static long mkImplies(long a0, long a1, long a2)
Definition: Native.java:1040
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
Definition: Context.java:2177
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:340
Tactic then(Tactic t1, Tactic t2, Tactic...ts)
Definition: Context.java:2470
Tactic tryFor(Tactic t, int ms)
Definition: Context.java:2495
static long probeGt(long a0, long a1, long a2)
Definition: Native.java:3933
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition: z3_api.h:1121
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
Definition: Context.java:705
void parseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2215
static long getSmtlibAssumption(long a0, int a1)
Definition: Native.java:3104
IntExpr mkIntConst(String name)
Definition: Context.java:579
Expr mkSetUnion(Expr...args)
Definition: Context.java:1803
static void ToggleWarningMessages(boolean enabled)
Definition: Context.java:2907
static long mkEq(long a0, long a1, long a2)
Definition: Native.java:995
static long mkRem(long a0, long a1, long a2)
Definition: Native.java:1130
Probe not(Probe p)
Definition: Context.java:2782
static long mkExtRotateRight(long a0, long a1, long a2)
Definition: Native.java:1544
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1219
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1258
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1034
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
Definition: Context.java:381
IntNum mkInt(long v)
Definition: Context.java:2013
Solver mkSolver(String logic)
Definition: Context.java:2819
static long mkInt2bv(long a0, int a1, long a2)
Definition: Native.java:1553
BitVecExpr mkBVRedAND(BitVecExpr t)
Definition: Context.java:958
ArithExpr mkAdd(ArithExpr...t)
Definition: Context.java:763
IntExpr mkRem(IntExpr t1, IntExpr t2)
Definition: Context.java:833
FiniteDomainSort mkFiniteDomainSort(String name, long size)
Definition: Context.java:269
static long mkBvand(long a0, long a1, long a2)
Definition: Native.java:1238
FuncDecl mkConstDecl(Symbol name, Sort range)
Definition: Context.java:447
Expr mkSetMembership(Expr elem, Expr set)
Definition: Context.java:1854
static long mkRepeat(long a0, int a1, long a2)
Definition: Native.java:1481
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1564
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
Definition: Native.java:916
static long mkPattern(long a0, int a1, long[] a2)
Definition: Native.java:1841
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:145
void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2196
static String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
Definition: Native.java:3034
static long mkBvult(long a0, long a1, long a2)
Definition: Native.java:1373
def EnumSort
Definition: z3py.py:4398
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:581
static void parseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3061
static int getSmtlibNumAssumptions(long a0)
Definition: Native.java:3095
Expr mkFreshConst(String prefix, Sort range)
Definition: Context.java:531
static long mkAnd(long a0, int a1, long[] a2)
Definition: Native.java:1058
Tactic failIf(Probe p)
Definition: Context.java:2568
static long mkLt(long a0, long a1, long a2)
Definition: Native.java:1148
Expr mkFullSet(Sort domain)
Definition: Context.java:1764
static long mkContextRc(long a0)
Definition: Native.java:594
BoolExpr mkOr(BoolExpr...t)
Definition: Context.java:752
Expr mkSetIntersection(Expr...args)
Definition: Context.java:1816
Expr mkTermArray(ArrayExpr array)
Definition: Context.java:1732
static long mkBvsub(long a0, long a1, long a2)
Definition: Native.java:1310
static long mkConstArray(long a0, long a1, long a2)
Definition: Native.java:1661
static long mkInt2real(long a0, long a1)
Definition: Native.java:1184
BoolExpr mkBool(boolean value)
Definition: Context.java:650
static long mkConst(long a0, long a1, long a2)
Definition: Native.java:950
static long mkBvsge(long a0, long a1, long a2)
Definition: Native.java:1418
def ArraySort(d, r)
Definition: z3py.py:3955
Probe or(Probe p1, Probe p2)
Definition: Context.java:2770
static long tacticParAndThen(long a0, long a1, long a2)
Definition: Native.java:3825
static String getProbeName(long a0, int a1)
Definition: Native.java:4023
Tactic with(Tactic t, Params p)
Definition: Context.java:2602
IntExpr mkMod(IntExpr t1, IntExpr t2)
Definition: Context.java:820
Probe ge(Probe p1, Probe p2)
Definition: Context.java:2733
static long mkBvashr(long a0, long a1, long a2)
Definition: Native.java:1508
static long mkGt(long a0, long a1, long a2)
Definition: Native.java:1166
ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
Definition: Context.java:1633
static long mkFullSet(long a0, long a1)
Definition: Native.java:1706
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
Definition: Context.java:258
BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1206
BitVecExpr mkInt2BV(int n, IntExpr t)
Definition: Context.java:1487
BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
Definition: Context.java:1441
ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
Definition: Context.java:845
static long probeLe(long a0, long a1, long a2)
Definition: Native.java:3942
Context(Map< String, String > settings)
Definition: Context.java:57
BoolExpr mkBoolConst(Symbol name)
Definition: Context.java:552
IntSymbol mkSymbol(int i)
Definition: Context.java:73
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:624
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2095
BoolExpr[] getSMTLIBAssumptions()
Definition: Context.java:2268
Expr mkConst(String name, Sort range)
Definition: Context.java:521
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3043
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
Definition: Context.java:315
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1634
static long mkRotateLeft(long a0, int a1, long a2)
Definition: Native.java:1517
static String simplifyGetHelp(long a0)
Definition: Native.java:2678
Tactic parAndThen(Tactic t1, Tactic t2)
Definition: Context.java:2622
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
Definition: Context.java:1429
static long mkBvredand(long a0, long a1)
Definition: Native.java:1220
static long tacticFail(long a0)
Definition: Native.java:3879
Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
Definition: Context.java:303
static long mkBvxor(long a0, long a1, long a2)
Definition: Native.java:1256
EnumSort mkEnumSort(String name, String...enumNames)
Definition: Context.java:228
static long tacticUsingParams(long a0, long a1, long a2)
Definition: Native.java:3906
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1193
Probe constProbe(double val)
Definition: Context.java:2681
static long probeLt(long a0, long a1, long a2)
Definition: Native.java:3924
static long mkBvudiv(long a0, long a1, long a2)
Definition: Native.java:1328
static long probeGe(long a0, long a1, long a2)
Definition: Native.java:3951
static long mkBvshl(long a0, long a1, long a2)
Definition: Native.java:1490
Expr mkSetDel(Expr set, Expr element)
Definition: Context.java:1789
static long mkFalse(long a0)
Definition: Native.java:986
static long mkBvsrem(long a0, long a1, long a2)
Definition: Native.java:1355
BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:982
BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1550
static long mkEmptySet(long a0, long a1)
Definition: Native.java:1697
Expr mkBound(int index, Sort ty)
Definition: Context.java:482
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1607
RatNum mkReal(long v)
Definition: Context.java:1978
static String getTacticName(long a0, int a1)
Definition: Native.java:4005
BitVecExpr mkBVConst(Symbol name, int size)
Definition: Context.java:606
static long tacticTryFor(long a0, long a1, int a2)
Definition: Native.java:3834
static long mkArrayDefault(long a0, long a1)
Definition: Native.java:1679
static long mkBvnegNoOverflow(long a0, long a1)
Definition: Native.java:1616
static long mkBound(long a0, int a1, long a2)
Definition: Native.java:1850
static long mkTrue(long a0)
Definition: Native.java:977
Tactic mkTactic(String name)
Definition: Context.java:2430
static long mkMul(long a0, int a1, long[] a2)
Definition: Native.java:1085
static long mkReal(long a0, int a1, int a2)
Definition: Native.java:1796
static long tacticAndThen(long a0, long a1, long a2)
Definition: Native.java:3798
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
Definition: Context.java:1683
BitVecSort mkBitVecSort(int size)
Definition: Context.java:182
ParamDescrs getSimplifyParameterDescriptions()
Definition: Context.java:2897
Fixedpoint mkFixedpoint()
Definition: Context.java:2849
static long mkBvxnor(long a0, long a1, long a2)
Definition: Native.java:1283
BoolExpr[] getSMTLIBFormulas()
Definition: Context.java:2244
Tactic parOr(Tactic...t)
Definition: Context.java:2610
static long mkSetUnion(long a0, int a1, long[] a2)
Definition: Native.java:1733
Tactic cond(Probe p, Tactic t1, Tactic t2)
Definition: Context.java:2523
static long mkPower(long a0, long a1, long a2)
Definition: Native.java:1139
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1166
Solver mkSolver(Symbol logic)
Definition: Context.java:2806
def Map(f, args)
Definition: z3py.py:4040
FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
Definition: Context.java:420
ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
Definition: Context.java:1643
static long mkBvor(long a0, long a1, long a2)
Definition: Native.java:1247
static long getSmtlibFormula(long a0, int a1)
Definition: Native.java:3086
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:191
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:505
BitVecNum mkBV(int v, int size)
Definition: Context.java:2035
static long mkBv2int(long a0, long a1, boolean a2)
Definition: Native.java:1562
BoolExpr mkNot(BoolExpr a)
Definition: Context.java:679
Expr mkNumeral(long v, Sort ty)
Definition: Context.java:1925
DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
Definition: Context.java:371
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:883
ListSort mkListSort(Symbol name, Sort elemSort)
Definition: Context.java:237
Tactic orElse(Tactic t1, Tactic t2)
Definition: Context.java:2480
Expr mkConst(FuncDecl f)
Definition: Context.java:543
Probe le(Probe p1, Probe p2)
Definition: Context.java:2719
ArithExpr mkUnaryMinus(ArithExpr t)
Definition: Context.java:796
EnumSort mkEnumSort(Symbol name, Symbol...enumNames)
Definition: Context.java:216
static long probeAnd(long a0, long a1, long a2)
Definition: Native.java:3969
RealExpr mkInt2Real(IntExpr t)
Definition: Context.java:913
RealExpr mkRealConst(Symbol name)
Definition: Context.java:588
static long mkBvmul(long a0, long a1, long a2)
Definition: Native.java:1319
Expr mkSetSubset(Expr arg1, Expr arg2)
Definition: Context.java:1868
FuncDecl mkFreshConstDecl(String prefix, Sort range)
Definition: Context.java:470
Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2136
BitVecNum mkBV(String v, int size)
Definition: Context.java:2025
Solver mkSolver(Tactic t)
Definition: Context.java:2839
ArithExpr mkMul(ArithExpr...t)
Definition: Context.java:774
String getTacticDescription(String name)
Definition: Context.java:2421
Expr mkSelect(ArrayExpr a, Expr i)
Definition: Context.java:1659
static long mkReal2int(long a0, long a1)
Definition: Native.java:1193
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
Definition: Context.java:435
BitVecNum mkBV(long v, int size)
Definition: Context.java:2045
BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1084
static long tacticWhen(long a0, long a1, long a2)
Definition: Native.java:3843
ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
Definition: Context.java:807
RealExpr mkRealConst(String name)
Definition: Context.java:597
static long mkNot(long a0, long a1)
Definition: Native.java:1013
static long mkBvSort(long a0, int a1)
Definition: Native.java:819
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1302
RatNum mkReal(int num, int den)
Definition: Context.java:1940
BitVecExpr mkSignExt(int i, BitVecExpr t)
Definition: Context.java:1333
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1271
Expr mkEmptySet(Sort domain)
Definition: Context.java:1753
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
Definition: Context.java:1509
static long mkIsInt(long a0, long a1)
Definition: Native.java:1202
Pattern mkPattern(Expr...terms)
Definition: Context.java:491
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3052
BoolExpr mkEq(Expr x, Expr y)
Definition: Context.java:658
static long mkBvsubNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1589
static long mkIff(long a0, long a1, long a2)
Definition: Native.java:1031
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:895
FuncDecl[] getSMTLIBDecls()
Definition: Context.java:2292
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2070
Tactic andThen(Tactic t1, Tactic t2, Tactic...ts)
Definition: Context.java:2440
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
Definition: Context.java:2380
static long tacticCond(long a0, long a1, long a2, long a3)
Definition: Native.java:3852
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1521
static long mkBvnor(long a0, long a1, long a2)
Definition: Native.java:1274