Z3
Context.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
20 import static com.microsoft.z3.Constructor.of;
21 
23 
24 import java.util.Map;
25 
35 public class Context implements AutoCloseable {
36  private final long m_ctx;
37  static final Object creation_lock = new Object();
38 
39  public Context () {
40  synchronized (creation_lock) {
41  m_ctx = Native.mkContextRc(0);
42  init();
43  }
44  }
45 
46  protected Context (long m_ctx) {
47  synchronized (creation_lock) {
48  this.m_ctx = m_ctx;
49  init();
50  }
51  }
52 
53 
71  public Context(Map<String, String> settings) {
72  synchronized (creation_lock) {
73  long cfg = Native.mkConfig();
74  for (Map.Entry<String, String> kv : settings.entrySet()) {
75  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
76  }
77  m_ctx = Native.mkContextRc(cfg);
78  Native.delConfig(cfg);
79  init();
80  }
81  }
82 
83  private void init() {
86  }
87 
93  public IntSymbol mkSymbol(int i)
94  {
95  return new IntSymbol(this, i);
96  }
97 
102  {
103  return new StringSymbol(this, name);
104  }
105 
109  Symbol[] mkSymbols(String[] names)
110  {
111  if (names == null)
112  return null;
113  Symbol[] result = new Symbol[names.length];
114  for (int i = 0; i < names.length; ++i)
115  result[i] = mkSymbol(names[i]);
116  return result;
117  }
118 
119  private BoolSort m_boolSort = null;
120  private IntSort m_intSort = null;
121  private RealSort m_realSort = null;
122  private SeqSort m_stringSort = null;
123 
128  {
129  if (m_boolSort == null) {
130  m_boolSort = new BoolSort(this);
131  }
132  return m_boolSort;
133  }
134 
139  {
140  if (m_intSort == null) {
141  m_intSort = new IntSort(this);
142  }
143  return m_intSort;
144  }
145 
150  {
151  if (m_realSort == null) {
152  m_realSort = new RealSort(this);
153  }
154  return m_realSort;
155  }
156 
161  {
162  return new BoolSort(this);
163  }
164 
169  {
170  if (m_stringSort == null) {
171  m_stringSort = mkStringSort();
172  }
173  return m_stringSort;
174  }
175 
180  {
181  checkContextMatch(s);
182  return new UninterpretedSort(this, s);
183  }
184 
189  {
190  return mkUninterpretedSort(mkSymbol(str));
191  }
192 
197  {
198  return new IntSort(this);
199  }
200 
205  {
206  return new RealSort(this);
207  }
208 
212  public BitVecSort mkBitVecSort(int size)
213  {
214  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
215  }
216 
221  {
222  checkContextMatch(domain);
223  checkContextMatch(range);
224  return new ArraySort(this, domain, range);
225  }
226 
227 
231  public ArraySort mkArraySort(Sort[] domains, Sort range)
232  {
233  checkContextMatch(domains);
234  checkContextMatch(range);
235  return new ArraySort(this, domains, range);
236  }
237 
242  {
243  return new SeqSort(this, Native.mkStringSort(nCtx()));
244  }
245 
250  {
251  return new SeqSort(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
252  }
253 
257  public ReSort mkReSort(Sort s)
258  {
259  return new ReSort(this, Native.mkReSort(nCtx(), s.getNativeObject()));
260  }
261 
262 
266  public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames,
267  Sort[] fieldSorts)
268  {
269  checkContextMatch(name);
270  checkContextMatch(fieldNames);
271  checkContextMatch(fieldSorts);
272  return new TupleSort(this, name, fieldNames.length, fieldNames,
273  fieldSorts);
274  }
275 
279  public EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
280 
281  {
282  checkContextMatch(name);
283  checkContextMatch(enumNames);
284  return new EnumSort(this, name, enumNames);
285  }
286 
290  public EnumSort mkEnumSort(String name, String... enumNames)
291 
292  {
293  return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
294  }
295 
299  public ListSort mkListSort(Symbol name, Sort elemSort)
300  {
301  checkContextMatch(name);
302  checkContextMatch(elemSort);
303  return new ListSort(this, name, elemSort);
304  }
305 
309  public ListSort mkListSort(String name, Sort elemSort)
310  {
311  checkContextMatch(elemSort);
312  return new ListSort(this, mkSymbol(name), elemSort);
313  }
314 
319 
320  {
321  checkContextMatch(name);
322  return new FiniteDomainSort(this, name, size);
323  }
324 
329 
330  {
331  return new FiniteDomainSort(this, mkSymbol(name), size);
332  }
333 
345  public Constructor mkConstructor(Symbol name, Symbol recognizer,
346  Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
347 
348  {
349  return of(this, name, recognizer, fieldNames, sorts,
350  sortRefs);
351  }
352 
356  public Constructor mkConstructor(String name, String recognizer,
357  String[] fieldNames, Sort[] sorts, int[] sortRefs)
358  {
359  return of(this, mkSymbol(name), mkSymbol(recognizer),
360  mkSymbols(fieldNames), sorts, sortRefs);
361  }
362 
366  public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
367 
368  {
369  checkContextMatch(name);
370  checkContextMatch(constructors);
371  return new DatatypeSort(this, name, constructors);
372  }
373 
377  public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
378 
379  {
380  checkContextMatch(constructors);
381  return new DatatypeSort(this, mkSymbol(name), constructors);
382  }
383 
390 
391  {
392  checkContextMatch(names);
393  int n = names.length;
394  ConstructorList[] cla = new ConstructorList[n];
395  long[] n_constr = new long[n];
396  for (int i = 0; i < n; i++)
397  {
398  Constructor[] constructor = c[i];
399 
400  checkContextMatch(constructor);
401  cla[i] = new ConstructorList(this, constructor);
402  n_constr[i] = cla[i].getNativeObject();
403  }
404  long[] n_res = new long[n];
405  Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
406  n_constr);
407  DatatypeSort[] res = new DatatypeSort[n];
408  for (int i = 0; i < n; i++)
409  res[i] = new DatatypeSort(this, n_res[i]);
410  return res;
411  }
412 
417 
418  {
419  return mkDatatypeSorts(mkSymbols(names), c);
420  }
421 
428  public Expr mkUpdateField(FuncDecl field, Expr t, Expr v)
429  throws Z3Exception
430  {
431  return Expr.create (this,
433  (nCtx(), field.getNativeObject(),
434  t.getNativeObject(), v.getNativeObject()));
435  }
436 
437 
441  public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
442 
443  {
444  checkContextMatch(name);
445  checkContextMatch(domain);
446  checkContextMatch(range);
447  return new FuncDecl(this, name, domain, range);
448  }
449 
453  public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
454 
455  {
456  checkContextMatch(name);
457  checkContextMatch(domain);
458  checkContextMatch(range);
459  Sort[] q = new Sort[] { domain };
460  return new FuncDecl(this, name, q, range);
461  }
462 
466  public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
467 
468  {
469  checkContextMatch(domain);
470  checkContextMatch(range);
471  return new FuncDecl(this, mkSymbol(name), domain, range);
472  }
473 
477  public FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
478 
479  {
480  checkContextMatch(domain);
481  checkContextMatch(range);
482  Sort[] q = new Sort[] { domain };
483  return new FuncDecl(this, mkSymbol(name), q, range);
484  }
485 
492  public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
493 
494  {
495  checkContextMatch(domain);
496  checkContextMatch(range);
497  return new FuncDecl(this, prefix, domain, range);
498  }
499 
504  {
505  checkContextMatch(name);
506  checkContextMatch(range);
507  return new FuncDecl(this, name, null, range);
508  }
509 
514  {
515  checkContextMatch(range);
516  return new FuncDecl(this, mkSymbol(name), null, range);
517  }
518 
526 
527  {
528  checkContextMatch(range);
529  return new FuncDecl(this, prefix, null, range);
530  }
531 
537  public Expr mkBound(int index, Sort ty)
538  {
539  return Expr.create(this,
540  Native.mkBound(nCtx(), index, ty.getNativeObject()));
541  }
542 
546  public Pattern mkPattern(Expr... terms)
547  {
548  if (terms.length == 0)
549  throw new Z3Exception("Cannot create a pattern from zero terms");
550 
551  long[] termsNative = AST.arrayToNative(terms);
552  return new Pattern(this, Native.mkPattern(nCtx(), terms.length,
553  termsNative));
554  }
555 
560  public Expr mkConst(Symbol name, Sort range)
561  {
562  checkContextMatch(name);
563  checkContextMatch(range);
564 
565  return Expr.create(
566  this,
567  Native.mkConst(nCtx(), name.getNativeObject(),
568  range.getNativeObject()));
569  }
570 
575  public Expr mkConst(String name, Sort range)
576  {
577  return mkConst(mkSymbol(name), range);
578  }
579 
585  {
586  checkContextMatch(range);
587  return Expr.create(this,
588  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
589  }
590 
596  {
597  return mkApp(f, (Expr[]) null);
598  }
599 
604  {
605  return (BoolExpr) mkConst(name, getBoolSort());
606  }
607 
612  {
613  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
614  }
615 
619  public IntExpr mkIntConst(Symbol name)
620  {
621  return (IntExpr) mkConst(name, getIntSort());
622  }
623 
627  public IntExpr mkIntConst(String name)
628  {
629  return (IntExpr) mkConst(name, getIntSort());
630  }
631 
636  {
637  return (RealExpr) mkConst(name, getRealSort());
638  }
639 
644  {
645  return (RealExpr) mkConst(name, getRealSort());
646  }
647 
651  public BitVecExpr mkBVConst(Symbol name, int size)
652  {
653  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
654  }
655 
659  public BitVecExpr mkBVConst(String name, int size)
660  {
661  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
662  }
663 
667  public Expr mkApp(FuncDecl f, Expr... args)
668  {
669  checkContextMatch(f);
670  checkContextMatch(args);
671  return Expr.create(this, f, args);
672  }
673 
677  public BoolExpr mkTrue()
678  {
679  return new BoolExpr(this, Native.mkTrue(nCtx()));
680  }
681 
685  public BoolExpr mkFalse()
686  {
687  return new BoolExpr(this, Native.mkFalse(nCtx()));
688  }
689 
693  public BoolExpr mkBool(boolean value)
694  {
695  return value ? mkTrue() : mkFalse();
696  }
697 
701  public BoolExpr mkEq(Expr x, Expr y)
702  {
703  checkContextMatch(x);
704  checkContextMatch(y);
705  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
706  y.getNativeObject()));
707  }
708 
712  public BoolExpr mkDistinct(Expr... args)
713  {
714  checkContextMatch(args);
715  return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
716  AST.arrayToNative(args)));
717  }
718 
723  {
724  checkContextMatch(a);
725  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
726  }
727 
735  public Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
736  {
737  checkContextMatch(t1);
738  checkContextMatch(t2);
739  checkContextMatch(t3);
740  return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
741  t2.getNativeObject(), t3.getNativeObject()));
742  }
743 
748  {
749  checkContextMatch(t1);
750  checkContextMatch(t2);
751  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
752  t2.getNativeObject()));
753  }
754 
759  {
760  checkContextMatch(t1);
761  checkContextMatch(t2);
762  return new BoolExpr(this, Native.mkImplies(nCtx(),
763  t1.getNativeObject(), t2.getNativeObject()));
764  }
765 
770  {
771  checkContextMatch(t1);
772  checkContextMatch(t2);
773  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
774  t2.getNativeObject()));
775  }
776 
780  public BoolExpr mkAnd(BoolExpr... t)
781  {
782  checkContextMatch(t);
783  return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
784  AST.arrayToNative(t)));
785  }
786 
790  public BoolExpr mkOr(BoolExpr... t)
791  {
792  checkContextMatch(t);
793  return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
794  AST.arrayToNative(t)));
795  }
796 
800  public ArithExpr mkAdd(ArithExpr... t)
801  {
802  checkContextMatch(t);
803  return (ArithExpr) Expr.create(this,
804  Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
805  }
806 
810  public ArithExpr mkMul(ArithExpr... t)
811  {
812  checkContextMatch(t);
813  return (ArithExpr) Expr.create(this,
814  Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
815  }
816 
820  public ArithExpr mkSub(ArithExpr... t)
821  {
822  checkContextMatch(t);
823  return (ArithExpr) Expr.create(this,
824  Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
825  }
826 
831  {
832  checkContextMatch(t);
833  return (ArithExpr) Expr.create(this,
834  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
835  }
836 
841  {
842  checkContextMatch(t1);
843  checkContextMatch(t2);
844  return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
845  t1.getNativeObject(), t2.getNativeObject()));
846  }
847 
853  public IntExpr mkMod(IntExpr t1, IntExpr t2)
854  {
855  checkContextMatch(t1);
856  checkContextMatch(t2);
857  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
858  t2.getNativeObject()));
859  }
860 
866  public IntExpr mkRem(IntExpr t1, IntExpr t2)
867  {
868  checkContextMatch(t1);
869  checkContextMatch(t2);
870  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
871  t2.getNativeObject()));
872  }
873 
878  {
879  checkContextMatch(t1);
880  checkContextMatch(t2);
881  return (ArithExpr) Expr.create(
882  this,
883  Native.mkPower(nCtx(), t1.getNativeObject(),
884  t2.getNativeObject()));
885  }
886 
891  {
892  checkContextMatch(t1);
893  checkContextMatch(t2);
894  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
895  t2.getNativeObject()));
896  }
897 
902  {
903  checkContextMatch(t1);
904  checkContextMatch(t2);
905  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
906  t2.getNativeObject()));
907  }
908 
913  {
914  checkContextMatch(t1);
915  checkContextMatch(t2);
916  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
917  t2.getNativeObject()));
918  }
919 
924  {
925  checkContextMatch(t1);
926  checkContextMatch(t2);
927  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
928  t2.getNativeObject()));
929  }
930 
942  {
943  checkContextMatch(t);
944  return new RealExpr(this,
945  Native.mkInt2real(nCtx(), t.getNativeObject()));
946  }
947 
955  {
956  checkContextMatch(t);
957  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
958  }
959 
964  {
965  checkContextMatch(t);
966  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
967  }
968 
975  {
976  checkContextMatch(t);
977  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
978  }
979 
986  {
987  checkContextMatch(t);
988  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
989  t.getNativeObject()));
990  }
991 
998  {
999  checkContextMatch(t);
1000  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
1001  t.getNativeObject()));
1002  }
1003 
1010  {
1011  checkContextMatch(t1);
1012  checkContextMatch(t2);
1013  return new BitVecExpr(this, Native.mkBvand(nCtx(),
1014  t1.getNativeObject(), t2.getNativeObject()));
1015  }
1016 
1023  {
1024  checkContextMatch(t1);
1025  checkContextMatch(t2);
1026  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1027  t2.getNativeObject()));
1028  }
1029 
1036  {
1037  checkContextMatch(t1);
1038  checkContextMatch(t2);
1039  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1040  t1.getNativeObject(), t2.getNativeObject()));
1041  }
1042 
1049  {
1050  checkContextMatch(t1);
1051  checkContextMatch(t2);
1052  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1053  t1.getNativeObject(), t2.getNativeObject()));
1054  }
1055 
1062  {
1063  checkContextMatch(t1);
1064  checkContextMatch(t2);
1065  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1066  t1.getNativeObject(), t2.getNativeObject()));
1067  }
1068 
1075  {
1076  checkContextMatch(t1);
1077  checkContextMatch(t2);
1078  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1079  t1.getNativeObject(), t2.getNativeObject()));
1080  }
1081 
1088  {
1089  checkContextMatch(t);
1090  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1091  }
1092 
1099  {
1100  checkContextMatch(t1);
1101  checkContextMatch(t2);
1102  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1103  t1.getNativeObject(), t2.getNativeObject()));
1104  }
1105 
1112  {
1113  checkContextMatch(t1);
1114  checkContextMatch(t2);
1115  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1116  t1.getNativeObject(), t2.getNativeObject()));
1117  }
1118 
1125  {
1126  checkContextMatch(t1);
1127  checkContextMatch(t2);
1128  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1129  t1.getNativeObject(), t2.getNativeObject()));
1130  }
1131 
1140  {
1141  checkContextMatch(t1);
1142  checkContextMatch(t2);
1143  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1144  t1.getNativeObject(), t2.getNativeObject()));
1145  }
1146 
1161  {
1162  checkContextMatch(t1);
1163  checkContextMatch(t2);
1164  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1165  t1.getNativeObject(), t2.getNativeObject()));
1166  }
1167 
1176  {
1177  checkContextMatch(t1);
1178  checkContextMatch(t2);
1179  return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1180  t1.getNativeObject(), t2.getNativeObject()));
1181  }
1182 
1194  {
1195  checkContextMatch(t1);
1196  checkContextMatch(t2);
1197  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1198  t1.getNativeObject(), t2.getNativeObject()));
1199  }
1200 
1208  {
1209  checkContextMatch(t1);
1210  checkContextMatch(t2);
1211  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1212  t1.getNativeObject(), t2.getNativeObject()));
1213  }
1214 
1221  {
1222  checkContextMatch(t1);
1223  checkContextMatch(t2);
1224  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1225  t2.getNativeObject()));
1226  }
1227 
1234  {
1235  checkContextMatch(t1);
1236  checkContextMatch(t2);
1237  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1238  t2.getNativeObject()));
1239  }
1240 
1247  {
1248  checkContextMatch(t1);
1249  checkContextMatch(t2);
1250  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1251  t2.getNativeObject()));
1252  }
1253 
1260  {
1261  checkContextMatch(t1);
1262  checkContextMatch(t2);
1263  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1264  t2.getNativeObject()));
1265  }
1266 
1273  {
1274  checkContextMatch(t1);
1275  checkContextMatch(t2);
1276  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1277  t2.getNativeObject()));
1278  }
1279 
1286  {
1287  checkContextMatch(t1);
1288  checkContextMatch(t2);
1289  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1290  t2.getNativeObject()));
1291  }
1292 
1299  {
1300  checkContextMatch(t1);
1301  checkContextMatch(t2);
1302  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1303  t2.getNativeObject()));
1304  }
1305 
1312  {
1313  checkContextMatch(t1);
1314  checkContextMatch(t2);
1315  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1316  t2.getNativeObject()));
1317  }
1318 
1330  {
1331  checkContextMatch(t1);
1332  checkContextMatch(t2);
1333  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1334  t1.getNativeObject(), t2.getNativeObject()));
1335  }
1336 
1345  public BitVecExpr mkExtract(int high, int low, BitVecExpr t)
1346 
1347  {
1348  checkContextMatch(t);
1349  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1350  t.getNativeObject()));
1351  }
1352 
1361  {
1362  checkContextMatch(t);
1363  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1364  t.getNativeObject()));
1365  }
1366 
1375  {
1376  checkContextMatch(t);
1377  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1378  t.getNativeObject()));
1379  }
1380 
1386  public BitVecExpr mkRepeat(int i, BitVecExpr t)
1387  {
1388  checkContextMatch(t);
1389  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1390  t.getNativeObject()));
1391  }
1392 
1405  {
1406  checkContextMatch(t1);
1407  checkContextMatch(t2);
1408  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1409  t1.getNativeObject(), t2.getNativeObject()));
1410  }
1411 
1424  {
1425  checkContextMatch(t1);
1426  checkContextMatch(t2);
1427  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1428  t1.getNativeObject(), t2.getNativeObject()));
1429  }
1430 
1444  {
1445  checkContextMatch(t1);
1446  checkContextMatch(t2);
1447  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1448  t1.getNativeObject(), t2.getNativeObject()));
1449  }
1450 
1457  {
1458  checkContextMatch(t);
1459  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1460  t.getNativeObject()));
1461  }
1462 
1469  {
1470  checkContextMatch(t);
1471  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1472  t.getNativeObject()));
1473  }
1474 
1482 
1483  {
1484  checkContextMatch(t1);
1485  checkContextMatch(t2);
1486  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1487  t1.getNativeObject(), t2.getNativeObject()));
1488  }
1489 
1497 
1498  {
1499  checkContextMatch(t1);
1500  checkContextMatch(t2);
1501  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1502  t1.getNativeObject(), t2.getNativeObject()));
1503  }
1504 
1514  public BitVecExpr mkInt2BV(int n, IntExpr t)
1515  {
1516  checkContextMatch(t);
1517  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1518  t.getNativeObject()));
1519  }
1520 
1535  public IntExpr mkBV2Int(BitVecExpr t, boolean signed)
1536  {
1537  checkContextMatch(t);
1538  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1539  (signed)));
1540  }
1541 
1548  boolean isSigned)
1549  {
1550  checkContextMatch(t1);
1551  checkContextMatch(t2);
1552  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1553  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1554  }
1555 
1562 
1563  {
1564  checkContextMatch(t1);
1565  checkContextMatch(t2);
1566  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1567  t1.getNativeObject(), t2.getNativeObject()));
1568  }
1569 
1576 
1577  {
1578  checkContextMatch(t1);
1579  checkContextMatch(t2);
1580  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1581  t1.getNativeObject(), t2.getNativeObject()));
1582  }
1583 
1590  boolean isSigned)
1591  {
1592  checkContextMatch(t1);
1593  checkContextMatch(t2);
1594  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1595  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1596  }
1597 
1604 
1605  {
1606  checkContextMatch(t1);
1607  checkContextMatch(t2);
1608  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1609  t1.getNativeObject(), t2.getNativeObject()));
1610  }
1611 
1618  {
1619  checkContextMatch(t);
1620  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1621  t.getNativeObject()));
1622  }
1623 
1630  boolean isSigned)
1631  {
1632  checkContextMatch(t1);
1633  checkContextMatch(t2);
1634  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1635  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1636  }
1637 
1644 
1645  {
1646  checkContextMatch(t1);
1647  checkContextMatch(t2);
1648  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1649  t1.getNativeObject(), t2.getNativeObject()));
1650  }
1651 
1655  public ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
1656 
1657  {
1658  return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1659  }
1660 
1664  public ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
1665 
1666  {
1667  return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1668  }
1669 
1684  {
1685  checkContextMatch(a);
1686  checkContextMatch(i);
1687  return Expr.create(
1688  this,
1689  Native.mkSelect(nCtx(), a.getNativeObject(),
1690  i.getNativeObject()));
1691  }
1692 
1706  public Expr mkSelect(ArrayExpr a, Expr[] args)
1707  {
1708  checkContextMatch(a);
1709  checkContextMatch(args);
1710  return Expr.create(
1711  this,
1712  Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
1713  }
1714 
1732  {
1733  checkContextMatch(a);
1734  checkContextMatch(i);
1735  checkContextMatch(v);
1736  return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1737  i.getNativeObject(), v.getNativeObject()));
1738  }
1739 
1756  public ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
1757  {
1758  checkContextMatch(a);
1759  checkContextMatch(args);
1760  checkContextMatch(v);
1761  return new ArrayExpr(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
1762  args.length, AST.arrayToNative(args), v.getNativeObject()));
1763  }
1764 
1774  public ArrayExpr mkConstArray(Sort domain, Expr v)
1775  {
1776  checkContextMatch(domain);
1777  checkContextMatch(v);
1778  return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1779  domain.getNativeObject(), v.getNativeObject()));
1780  }
1781 
1795  public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
1796  {
1797  checkContextMatch(f);
1798  checkContextMatch(args);
1799  return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1800  f.getNativeObject(), AST.arrayLength(args),
1801  AST.arrayToNative(args)));
1802  }
1803 
1811  {
1812  checkContextMatch(array);
1813  return Expr.create(this,
1814  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1815  }
1816 
1820  public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
1821  {
1822  checkContextMatch(arg1);
1823  checkContextMatch(arg2);
1824  return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
1825  }
1826 
1827 
1832  {
1833  checkContextMatch(ty);
1834  return new SetSort(this, ty);
1835  }
1836 
1840  public ArrayExpr mkEmptySet(Sort domain)
1841  {
1842  checkContextMatch(domain);
1843  return (ArrayExpr)Expr.create(this,
1844  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1845  }
1846 
1850  public ArrayExpr mkFullSet(Sort domain)
1851  {
1852  checkContextMatch(domain);
1853  return (ArrayExpr)Expr.create(this,
1854  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1855  }
1856 
1860  public ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
1861  {
1862  checkContextMatch(set);
1863  checkContextMatch(element);
1864  return (ArrayExpr)Expr.create(this,
1865  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1866  element.getNativeObject()));
1867  }
1868 
1872  public ArrayExpr mkSetDel(ArrayExpr set, Expr element)
1873  {
1874  checkContextMatch(set);
1875  checkContextMatch(element);
1876  return (ArrayExpr)Expr.create(this,
1877  Native.mkSetDel(nCtx(), set.getNativeObject(),
1878  element.getNativeObject()));
1879  }
1880 
1885  {
1886  checkContextMatch(args);
1887  return (ArrayExpr)Expr.create(this,
1888  Native.mkSetUnion(nCtx(), args.length,
1889  AST.arrayToNative(args)));
1890  }
1891 
1896  {
1897  checkContextMatch(args);
1898  return (ArrayExpr)Expr.create(this,
1899  Native.mkSetIntersect(nCtx(), args.length,
1900  AST.arrayToNative(args)));
1901  }
1902 
1907  {
1908  checkContextMatch(arg1);
1909  checkContextMatch(arg2);
1910  return (ArrayExpr)Expr.create(this,
1911  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1912  arg2.getNativeObject()));
1913  }
1914 
1919  {
1920  checkContextMatch(arg);
1921  return (ArrayExpr)Expr.create(this,
1922  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1923  }
1924 
1929  {
1930  checkContextMatch(elem);
1931  checkContextMatch(set);
1932  return (BoolExpr) Expr.create(this,
1933  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1934  set.getNativeObject()));
1935  }
1936 
1941  {
1942  checkContextMatch(arg1);
1943  checkContextMatch(arg2);
1944  return (BoolExpr) Expr.create(this,
1945  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1946  arg2.getNativeObject()));
1947  }
1948 
1949 
1958  {
1959  checkContextMatch(s);
1960  return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
1961  }
1962 
1966  public SeqExpr mkUnit(Expr elem)
1967  {
1968  checkContextMatch(elem);
1969  return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
1970  }
1971 
1976  {
1977  return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
1978  }
1979 
1983  public SeqExpr mkConcat(SeqExpr... t)
1984  {
1985  checkContextMatch(t);
1986  return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
1987  }
1988 
1989 
1994  {
1995  checkContextMatch(s);
1996  return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
1997  }
1998 
2003  {
2004  checkContextMatch(s1, s2);
2005  return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2006  }
2007 
2012  {
2013  checkContextMatch(s1, s2);
2014  return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2015  }
2016 
2021  {
2022  checkContextMatch(s1, s2);
2023  return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2024  }
2025 
2029  public SeqExpr mkAt(SeqExpr s, IntExpr index)
2030  {
2031  checkContextMatch(s, index);
2032  return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
2033  }
2034 
2038  public SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
2039  {
2040  checkContextMatch(s, offset, length);
2041  return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
2042  }
2043 
2047  public IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
2048  {
2049  checkContextMatch(s, substr, offset);
2050  return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
2051  }
2052 
2057  {
2058  checkContextMatch(s, src, dst);
2059  return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
2060  }
2061 
2065  public ReExpr mkToRe(SeqExpr s)
2066  {
2067  checkContextMatch(s);
2068  return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
2069  }
2070 
2071 
2076  {
2077  checkContextMatch(s, re);
2078  return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
2079  }
2080 
2084  public ReExpr mkStar(ReExpr re)
2085  {
2086  checkContextMatch(re);
2087  return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
2088  }
2089 
2093  public ReExpr mkLoop(ReExpr re, int lo, int hi)
2094  {
2095  return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
2096  }
2097 
2101  public ReExpr mkLoop(ReExpr re, int lo)
2102  {
2103  return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
2104  }
2105 
2106 
2110  public ReExpr mkPlus(ReExpr re)
2111  {
2112  checkContextMatch(re);
2113  return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
2114  }
2115 
2120  {
2121  checkContextMatch(re);
2122  return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
2123  }
2124 
2125 
2130  {
2131  checkContextMatch(re);
2132  return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
2133  }
2134 
2138  public ReExpr mkConcat(ReExpr... t)
2139  {
2140  checkContextMatch(t);
2141  return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2142  }
2143 
2147  public ReExpr mkUnion(ReExpr... t)
2148  {
2149  checkContextMatch(t);
2150  return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2151  }
2152 
2157  {
2158  checkContextMatch(t);
2159  return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
2160  }
2161 
2165  public ReExpr mkRange(SeqExpr lo, SeqExpr hi)
2166  {
2167  checkContextMatch(lo, hi);
2168  return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
2169  }
2170 
2171 
2175  public BoolExpr mkAtMost(BoolExpr[] args, int k)
2176  {
2177  checkContextMatch(args);
2178  return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
2179  }
2180 
2184  public BoolExpr mkAtLeast(BoolExpr[] args, int k)
2185  {
2186  checkContextMatch(args);
2187  return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
2188  }
2189 
2193  public BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
2194  {
2195  checkContextMatch(args);
2196  return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2197  }
2198 
2202  public BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
2203  {
2204  checkContextMatch(args);
2205  return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2206  }
2207 
2211  public BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
2212  {
2213  checkContextMatch(args);
2214  return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2215  }
2216 
2217 
2229  public Expr mkNumeral(String v, Sort ty)
2230  {
2231  checkContextMatch(ty);
2232  return Expr.create(this,
2233  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
2234  }
2235 
2246  public Expr mkNumeral(int v, Sort ty)
2247  {
2248  checkContextMatch(ty);
2249  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
2250  }
2251 
2262  public Expr mkNumeral(long v, Sort ty)
2263  {
2264  checkContextMatch(ty);
2265  return Expr.create(this,
2266  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
2267  }
2268 
2278  public RatNum mkReal(int num, int den)
2279  {
2280  if (den == 0) {
2281  throw new Z3Exception("Denominator is zero");
2282  }
2283 
2284  return new RatNum(this, Native.mkReal(nCtx(), num, den));
2285  }
2286 
2294  {
2295 
2296  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2297  .getNativeObject()));
2298  }
2299 
2306  public RatNum mkReal(int v)
2307  {
2308 
2309  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2310  .getNativeObject()));
2311  }
2312 
2319  public RatNum mkReal(long v)
2320  {
2321 
2322  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2323  .getNativeObject()));
2324  }
2325 
2330  public IntNum mkInt(String v)
2331  {
2332 
2333  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2334  .getNativeObject()));
2335  }
2336 
2343  public IntNum mkInt(int v)
2344  {
2345 
2346  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2347  .getNativeObject()));
2348  }
2349 
2356  public IntNum mkInt(long v)
2357  {
2358 
2359  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2360  .getNativeObject()));
2361  }
2362 
2368  public BitVecNum mkBV(String v, int size)
2369  {
2370  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2371  }
2372 
2378  public BitVecNum mkBV(int v, int size)
2379  {
2380  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2381  }
2382 
2388  public BitVecNum mkBV(long v, int size)
2389  {
2390  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2391  }
2392 
2418  public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
2419  int weight, Pattern[] patterns, Expr[] noPatterns,
2420  Symbol quantifierID, Symbol skolemID)
2421  {
2422 
2423  return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2424  noPatterns, quantifierID, skolemID);
2425  }
2426 
2431  public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
2432  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2433  Symbol skolemID)
2434  {
2435 
2436  return Quantifier.of(this, true, boundConstants, body, weight,
2437  patterns, noPatterns, quantifierID, skolemID);
2438  }
2439 
2444  public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
2445  int weight, Pattern[] patterns, Expr[] noPatterns,
2446  Symbol quantifierID, Symbol skolemID)
2447  {
2448 
2449  return Quantifier.of(this, false, sorts, names, body, weight,
2450  patterns, noPatterns, quantifierID, skolemID);
2451  }
2452 
2457  public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
2458  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2459  Symbol skolemID)
2460  {
2461 
2462  return Quantifier.of(this, false, boundConstants, body, weight,
2463  patterns, noPatterns, quantifierID, skolemID);
2464  }
2465 
2470  public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
2471  Symbol[] names, Expr body, int weight, Pattern[] patterns,
2472  Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
2473 
2474  {
2475 
2476  if (universal)
2477  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2478  quantifierID, skolemID);
2479  else
2480  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2481  quantifierID, skolemID);
2482  }
2483 
2488  public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
2489  Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
2490  Symbol quantifierID, Symbol skolemID)
2491  {
2492 
2493  if (universal)
2494  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2495  quantifierID, skolemID);
2496  else
2497  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2498  quantifierID, skolemID);
2499  }
2500 
2515  public void setPrintMode(Z3_ast_print_mode value)
2516  {
2517  Native.setAstPrintMode(nCtx(), value.toInt());
2518  }
2519 
2534  String status, String attributes, BoolExpr[] assumptions,
2535  BoolExpr formula)
2536  {
2537 
2538  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2539  attributes, assumptions.length,
2540  AST.arrayToNative(assumptions), formula.getNativeObject());
2541  }
2542 
2549  public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
2550  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2551 
2552  {
2553 
2554  int csn = Symbol.arrayLength(sortNames);
2555  int cs = Sort.arrayLength(sorts);
2556  int cdn = Symbol.arrayLength(declNames);
2557  int cd = AST.arrayLength(decls);
2558  if (csn != cs || cdn != cd) {
2559  throw new Z3Exception("Argument size mismatch");
2560  }
2561  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2562  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2563  AST.arrayToNative(sorts), AST.arrayLength(decls),
2564  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2565  }
2566 
2571  public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
2572  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2573 
2574  {
2575  int csn = Symbol.arrayLength(sortNames);
2576  int cs = Sort.arrayLength(sorts);
2577  int cdn = Symbol.arrayLength(declNames);
2578  int cd = AST.arrayLength(decls);
2579  if (csn != cs || cdn != cd)
2580  throw new Z3Exception("Argument size mismatch");
2581  return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
2582  fileName, AST.arrayLength(sorts),
2583  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2584  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2585  AST.arrayToNative(decls)));
2586  }
2587 
2598  public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
2599 
2600  {
2601  return new Goal(this, models, unsatCores, proofs);
2602  }
2603 
2607  public Params mkParams()
2608  {
2609  return new Params(this);
2610  }
2611 
2615  public int getNumTactics()
2616  {
2617  return Native.getNumTactics(nCtx());
2618  }
2619 
2624  {
2625 
2626  int n = getNumTactics();
2627  String[] res = new String[n];
2628  for (int i = 0; i < n; i++)
2629  res[i] = Native.getTacticName(nCtx(), i);
2630  return res;
2631  }
2632 
2638  {
2639  return Native.tacticGetDescr(nCtx(), name);
2640  }
2641 
2645  public Tactic mkTactic(String name)
2646  {
2647  return new Tactic(this, name);
2648  }
2649 
2654  public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
2655 
2656  {
2657  checkContextMatch(t1);
2658  checkContextMatch(t2);
2659  checkContextMatch(ts);
2660 
2661  long last = 0;
2662  if (ts != null && ts.length > 0)
2663  {
2664  last = ts[ts.length - 1].getNativeObject();
2665  for (int i = ts.length - 2; i >= 0; i--) {
2666  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2667  last);
2668  }
2669  }
2670  if (last != 0)
2671  {
2672  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2673  return new Tactic(this, Native.tacticAndThen(nCtx(),
2674  t1.getNativeObject(), last));
2675  } else
2676  return new Tactic(this, Native.tacticAndThen(nCtx(),
2677  t1.getNativeObject(), t2.getNativeObject()));
2678  }
2679 
2686  public Tactic then(Tactic t1, Tactic t2, Tactic... ts)
2687  {
2688  return andThen(t1, t2, ts);
2689  }
2690 
2696  public Tactic orElse(Tactic t1, Tactic t2)
2697  {
2698  checkContextMatch(t1);
2699  checkContextMatch(t2);
2700  return new Tactic(this, Native.tacticOrElse(nCtx(),
2701  t1.getNativeObject(), t2.getNativeObject()));
2702  }
2703 
2710  public Tactic tryFor(Tactic t, int ms)
2711  {
2712  checkContextMatch(t);
2713  return new Tactic(this, Native.tacticTryFor(nCtx(),
2714  t.getNativeObject(), ms));
2715  }
2716 
2723  public Tactic when(Probe p, Tactic t)
2724  {
2725  checkContextMatch(t);
2726  checkContextMatch(p);
2727  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2728  t.getNativeObject()));
2729  }
2730 
2736  public Tactic cond(Probe p, Tactic t1, Tactic t2)
2737  {
2738  checkContextMatch(p);
2739  checkContextMatch(t1);
2740  checkContextMatch(t2);
2741  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2742  t1.getNativeObject(), t2.getNativeObject()));
2743  }
2744 
2749  public Tactic repeat(Tactic t, int max)
2750  {
2751  checkContextMatch(t);
2752  return new Tactic(this, Native.tacticRepeat(nCtx(),
2753  t.getNativeObject(), max));
2754  }
2755 
2759  public Tactic skip()
2760  {
2761  return new Tactic(this, Native.tacticSkip(nCtx()));
2762  }
2763 
2767  public Tactic fail()
2768  {
2769  return new Tactic(this, Native.tacticFail(nCtx()));
2770  }
2771 
2776  public Tactic failIf(Probe p)
2777  {
2778  checkContextMatch(p);
2779  return new Tactic(this,
2780  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2781  }
2782 
2788  {
2789  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2790  }
2791 
2797  {
2798  checkContextMatch(t);
2799  checkContextMatch(p);
2800  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2801  t.getNativeObject(), p.getNativeObject()));
2802  }
2803 
2810  public Tactic with(Tactic t, Params p)
2811  {
2812  return usingParams(t, p);
2813  }
2814 
2818  public Tactic parOr(Tactic... t)
2819  {
2820  checkContextMatch(t);
2821  return new Tactic(this, Native.tacticParOr(nCtx(),
2822  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2823  }
2824 
2830  {
2831  checkContextMatch(t1);
2832  checkContextMatch(t2);
2833  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2834  t1.getNativeObject(), t2.getNativeObject()));
2835  }
2836 
2842  public void interrupt()
2843  {
2844  Native.interrupt(nCtx());
2845  }
2846 
2850  public int getNumProbes()
2851  {
2852  return Native.getNumProbes(nCtx());
2853  }
2854 
2859  {
2860 
2861  int n = getNumProbes();
2862  String[] res = new String[n];
2863  for (int i = 0; i < n; i++)
2864  res[i] = Native.getProbeName(nCtx(), i);
2865  return res;
2866  }
2867 
2873  {
2874  return Native.probeGetDescr(nCtx(), name);
2875  }
2876 
2880  public Probe mkProbe(String name)
2881  {
2882  return new Probe(this, name);
2883  }
2884 
2888  public Probe constProbe(double val)
2889  {
2890  return new Probe(this, Native.probeConst(nCtx(), val));
2891  }
2892 
2897  public Probe lt(Probe p1, Probe p2)
2898  {
2899  checkContextMatch(p1);
2900  checkContextMatch(p2);
2901  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2902  p2.getNativeObject()));
2903  }
2904 
2909  public Probe gt(Probe p1, Probe p2)
2910  {
2911  checkContextMatch(p1);
2912  checkContextMatch(p2);
2913  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2914  p2.getNativeObject()));
2915  }
2916 
2922  public Probe le(Probe p1, Probe p2)
2923  {
2924  checkContextMatch(p1);
2925  checkContextMatch(p2);
2926  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2927  p2.getNativeObject()));
2928  }
2929 
2935  public Probe ge(Probe p1, Probe p2)
2936  {
2937  checkContextMatch(p1);
2938  checkContextMatch(p2);
2939  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2940  p2.getNativeObject()));
2941  }
2942 
2947  public Probe eq(Probe p1, Probe p2)
2948  {
2949  checkContextMatch(p1);
2950  checkContextMatch(p2);
2951  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2952  p2.getNativeObject()));
2953  }
2954 
2958  public Probe and(Probe p1, Probe p2)
2959  {
2960  checkContextMatch(p1);
2961  checkContextMatch(p2);
2962  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
2963  p2.getNativeObject()));
2964  }
2965 
2969  public Probe or(Probe p1, Probe p2)
2970  {
2971  checkContextMatch(p1);
2972  checkContextMatch(p2);
2973  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
2974  p2.getNativeObject()));
2975  }
2976 
2980  public Probe not(Probe p)
2981  {
2982  checkContextMatch(p);
2983  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2984  }
2985 
2993  public Solver mkSolver()
2994  {
2995  return mkSolver((Symbol) null);
2996  }
2997 
3005  public Solver mkSolver(Symbol logic)
3006  {
3007 
3008  if (logic == null)
3009  return new Solver(this, Native.mkSolver(nCtx()));
3010  else
3011  return new Solver(this, Native.mkSolverForLogic(nCtx(),
3012  logic.getNativeObject()));
3013  }
3014 
3019  public Solver mkSolver(String logic)
3020  {
3021  return mkSolver(mkSymbol(logic));
3022  }
3023 
3028  {
3029  return new Solver(this, Native.mkSimpleSolver(nCtx()));
3030  }
3031 
3039  {
3040 
3041  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3042  t.getNativeObject()));
3043  }
3044 
3049  {
3050  return new Fixedpoint(this);
3051  }
3052 
3057  {
3058  return new Optimize(this);
3059  }
3060 
3061 
3067  {
3068  return new FPRMSort(this);
3069  }
3070 
3076  {
3077  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3078  }
3079 
3084  public FPRMNum mkFPRNE()
3085  {
3086  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3087  }
3088 
3094  {
3095  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3096  }
3097 
3102  public FPRMNum mkFPRNA()
3103  {
3104  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3105  }
3106 
3112  {
3113  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3114  }
3115 
3120  public FPRMNum mkFPRTP()
3121  {
3122  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3123  }
3124 
3130  {
3131  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3132  }
3133 
3138  public FPRMNum mkFPRTN()
3139  {
3140  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3141  }
3142 
3148  {
3149  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3150  }
3151 
3156  public FPRMNum mkFPRTZ()
3157  {
3158  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3159  }
3160 
3167  public FPSort mkFPSort(int ebits, int sbits)
3168  {
3169  return new FPSort(this, ebits, sbits);
3170  }
3171 
3177  {
3178  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3179  }
3180 
3186  {
3187  return new FPSort(this, Native.mkFpaSort16(nCtx()));
3188  }
3189 
3195  {
3196  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3197  }
3198 
3204  {
3205  return new FPSort(this, Native.mkFpaSort32(nCtx()));
3206  }
3207 
3213  {
3214  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3215  }
3216 
3222  {
3223  return new FPSort(this, Native.mkFpaSort64(nCtx()));
3224  }
3225 
3231  {
3232  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3233  }
3234 
3240  {
3241  return new FPSort(this, Native.mkFpaSort128(nCtx()));
3242  }
3243 
3244 
3251  {
3252  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3253  }
3254 
3261  public FPNum mkFPInf(FPSort s, boolean negative)
3262  {
3263  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3264  }
3265 
3272  public FPNum mkFPZero(FPSort s, boolean negative)
3273  {
3274  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3275  }
3276 
3283  public FPNum mkFPNumeral(float v, FPSort s)
3284  {
3285  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3286  }
3287 
3294  public FPNum mkFPNumeral(double v, FPSort s)
3295  {
3296  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3297  }
3298 
3305  public FPNum mkFPNumeral(int v, FPSort s)
3306  {
3307  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3308  }
3309 
3318  public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
3319  {
3320  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3321  }
3322 
3331  public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
3332  {
3333  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3334  }
3335 
3342  public FPNum mkFP(float v, FPSort s)
3343  {
3344  return mkFPNumeral(v, s);
3345  }
3346 
3353  public FPNum mkFP(double v, FPSort s)
3354  {
3355  return mkFPNumeral(v, s);
3356  }
3357 
3365  public FPNum mkFP(int v, FPSort s)
3366  {
3367  return mkFPNumeral(v, s);
3368  }
3369 
3378  public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
3379  {
3380  return mkFPNumeral(sgn, sig, exp, s);
3381  }
3382 
3391  public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
3392  {
3393  return mkFPNumeral(sgn, sig, exp, s);
3394  }
3395 
3396 
3402  public FPExpr mkFPAbs(FPExpr t)
3403  {
3404  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3405  }
3406 
3412  public FPExpr mkFPNeg(FPExpr t)
3413  {
3414  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3415  }
3416 
3424  public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
3425  {
3426  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3427  }
3428 
3436  public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
3437  {
3438  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3439  }
3440 
3448  public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
3449  {
3450  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3451  }
3452 
3460  public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
3461  {
3462  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3463  }
3464 
3475  public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
3476  {
3477  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3478  }
3479 
3487  {
3488  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3489  }
3490 
3497  public FPExpr mkFPRem(FPExpr t1, FPExpr t2)
3498  {
3499  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3500  }
3501 
3510  {
3511  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3512  }
3513 
3520  public FPExpr mkFPMin(FPExpr t1, FPExpr t2)
3521  {
3522  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3523  }
3524 
3531  public FPExpr mkFPMax(FPExpr t1, FPExpr t2)
3532  {
3533  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3534  }
3535 
3542  public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
3543  {
3544  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3545  }
3546 
3553  public BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
3554  {
3555  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3556  }
3557 
3564  public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
3565  {
3566  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3567  }
3568 
3575  public BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
3576  {
3577  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3578  }
3579 
3588  public BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
3589  {
3590  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3591  }
3592 
3599  {
3600  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3601  }
3602 
3609  {
3610  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3611  }
3612 
3619  {
3620  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3621  }
3622 
3629  {
3630  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3631  }
3632 
3639  {
3640  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3641  }
3642 
3649  {
3650  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3651  }
3652 
3659  {
3660  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3661  }
3662 
3677  {
3678  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3679  }
3680 
3693  {
3694  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3695  }
3696 
3709  {
3710  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3711  }
3712 
3725  {
3726  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3727  }
3728 
3742  public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
3743  {
3744  if (signed)
3745  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3746  else
3747  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3748  }
3749 
3761  {
3762  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3763  }
3764 
3777  public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
3778  {
3779  if (signed)
3780  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3781  else
3782  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3783  }
3784 
3795  {
3796  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3797  }
3798 
3810  {
3811  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3812  }
3813 
3828  {
3829  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3830  }
3831 
3832 
3843  public AST wrapAST(long nativeObject)
3844  {
3845  return AST.create(this, nativeObject);
3846  }
3847 
3860  public long unwrapAST(AST a)
3861  {
3862  return a.getNativeObject();
3863  }
3864 
3870  {
3871  return Native.simplifyGetHelp(nCtx());
3872  }
3873 
3878  {
3879  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3880  }
3881 
3890  public void updateParamValue(String id, String value)
3891  {
3892  Native.updateParamValue(nCtx(), id, value);
3893  }
3894 
3895 
3896  long nCtx()
3897  {
3898  return m_ctx;
3899  }
3900 
3901 
3902  void checkContextMatch(Z3Object other)
3903  {
3904  if (this != other.getContext())
3905  throw new Z3Exception("Context mismatch");
3906  }
3907 
3908  void checkContextMatch(Z3Object other1, Z3Object other2)
3909  {
3910  checkContextMatch(other1);
3911  checkContextMatch(other2);
3912  }
3913 
3914  void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
3915  {
3916  checkContextMatch(other1);
3917  checkContextMatch(other2);
3918  checkContextMatch(other3);
3919  }
3920 
3921  void checkContextMatch(Z3Object[] arr)
3922  {
3923  if (arr != null)
3924  for (Z3Object a : arr)
3925  checkContextMatch(a);
3926  }
3927 
3928  private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
3929  private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
3930  private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
3931  private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
3932  private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
3933  private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
3934  private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
3935  private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
3936  private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
3937  private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
3938  private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
3939  private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
3940  private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
3941  private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
3942  private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
3943  private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
3944  private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
3945  private ConstructorListDecRefQueue m_ConstructorList_DRQ =
3946  new ConstructorListDecRefQueue();
3947 
3949  return m_Constructor_DRQ;
3950  }
3951 
3953  return m_ConstructorList_DRQ;
3954  }
3955 
3957  {
3958  return m_AST_DRQ;
3959  }
3960 
3962  {
3963  return m_ASTMap_DRQ;
3964  }
3965 
3967  {
3968  return m_ASTVector_DRQ;
3969  }
3970 
3972  {
3973  return m_ApplyResult_DRQ;
3974  }
3975 
3977  {
3978  return m_FuncEntry_DRQ;
3979  }
3980 
3982  {
3983  return m_FuncInterp_DRQ;
3984  }
3985 
3987  {
3988  return m_Goal_DRQ;
3989  }
3990 
3992  {
3993  return m_Model_DRQ;
3994  }
3995 
3997  {
3998  return m_Params_DRQ;
3999  }
4000 
4002  {
4003  return m_ParamDescrs_DRQ;
4004  }
4005 
4007  {
4008  return m_Probe_DRQ;
4009  }
4010 
4012  {
4013  return m_Solver_DRQ;
4014  }
4015 
4017  {
4018  return m_Statistics_DRQ;
4019  }
4020 
4022  {
4023  return m_Tactic_DRQ;
4024  }
4025 
4027  {
4028  return m_Fixedpoint_DRQ;
4029  }
4030 
4032  {
4033  return m_Optimize_DRQ;
4034  }
4035 
4039  @Override
4040  public void close()
4041  {
4042  m_AST_DRQ.forceClear(this);
4043  m_ASTMap_DRQ.forceClear(this);
4044  m_ASTVector_DRQ.forceClear(this);
4045  m_ApplyResult_DRQ.forceClear(this);
4046  m_FuncEntry_DRQ.forceClear(this);
4047  m_FuncInterp_DRQ.forceClear(this);
4048  m_Goal_DRQ.forceClear(this);
4049  m_Model_DRQ.forceClear(this);
4050  m_Params_DRQ.forceClear(this);
4051  m_Probe_DRQ.forceClear(this);
4052  m_Solver_DRQ.forceClear(this);
4053  m_Optimize_DRQ.forceClear(this);
4054  m_Statistics_DRQ.forceClear(this);
4055  m_Tactic_DRQ.forceClear(this);
4056  m_Fixedpoint_DRQ.forceClear(this);
4057 
4058  m_boolSort = null;
4059  m_intSort = null;
4060  m_realSort = null;
4061  m_stringSort = null;
4062 
4063  synchronized (creation_lock) {
4064  Native.delContext(m_ctx);
4065  }
4066  }
4067 }
BoolExpr mkFPIsNegative(FPExpr t)
Definition: Context.java:3648
static long mkFpaFp(long a0, long a1, long a2, long a3)
Definition: Native.java:5880
IntExpr mkIntConst(Symbol name)
Definition: Context.java:619
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6177
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1629
static long tacticRepeat(long a0, long a1, int a2)
Definition: Native.java:3969
BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
Definition: Context.java:2011
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
Definition: Context.java:735
IDecRefQueue< Probe > getProbeDRQ()
Definition: Context.java:4006
static long mkBvule(long a0, long a1, long a2)
Definition: Native.java:1536
static long mkSolver(long a0)
Definition: Native.java:4255
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6186
Tactic when(Probe p, Tactic t)
Definition: Context.java:2723
RatNum mkReal(String v)
Definition: Context.java:2293
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1074
static long mkExtract(long a0, int a1, int a2, long a3)
Definition: Native.java:1599
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
Definition: Context.java:377
static void interrupt(long a0)
Definition: Native.java:758
Pattern mkPattern(Expr... terms)
Definition: Context.java:546
def SeqSort(s)
Definition: z3py.py:9652
Probe and(Probe p1, Probe p2)
Definition: Context.java:2958
static long mkMod(long a0, long a1, long a2)
Definition: Native.java:1266
static long mkBvugt(long a0, long a1, long a2)
Definition: Native.java:1572
static long mkSeqContains(long a0, long a1, long a2)
Definition: Native.java:2157
Expr mkSelect(ArrayExpr a, Expr[] args)
Definition: Context.java:1706
static void delConfig(long a0)
Definition: Native.java:703
ArrayExpr mkConstArray(Sort domain, Expr v)
Definition: Context.java:1774
Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
Definition: Context.java:345
static long mkBvredor(long a0, long a1)
Definition: Native.java:1374
RealExpr mkFPToReal(FPExpr t)
Definition: Context.java:3794
static long tacticOrElse(long a0, long a1, long a2)
Definition: Native.java:3915
Probe lt(Probe p1, Probe p2)
Definition: Context.java:2897
static long mkFpaNeg(long a0, long a1)
Definition: Native.java:5943
FPNum mkFPNumeral(double v, FPSort s)
Definition: Context.java:3294
static int getNumProbes(long a0)
Definition: Native.java:4122
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1272
BoolExpr mkFPIsSubnormal(FPExpr t)
Definition: Context.java:3608
static long mkNumeral(long a0, String a1, long a2)
Definition: Native.java:1968
ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1906
BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1404
static long mkFpaDiv(long a0, long a1, long a2, long a3)
Definition: Native.java:5979
static void updateParamValue(long a0, String a1, String a2)
Definition: Native.java:750
ArrayExpr mkSetComplement(ArrayExpr arg)
Definition: Context.java:1918
BitVecExpr mkBVNeg(BitVecExpr t)
Definition: Context.java:1087
static long mkFreshConst(long a0, String a1, long a2)
Definition: Native.java:1113
static long mkConfig()
Definition: Native.java:697
def ReSort(s)
Definition: z3py.py:9923
ReExpr mkConcat(ReExpr... t)
Definition: Context.java:2138
def RealSort(ctx=None)
Definition: z3py.py:2762
FPNum mkFPInf(FPSort s, boolean negative)
Definition: Context.java:3261
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
Expr mkNumeral(int v, Sort ty)
Definition: Context.java:2246
BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1603
ListSort mkListSort(String name, Sort elemSort)
Definition: Context.java:309
FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t)
Definition: Context.java:3486
FPNum mkFPNumeral(int v, FPSort s)
Definition: Context.java:3305
static long mkFpaIsNegative(long a0, long a1)
Definition: Native.java:6132
StringSymbol mkSymbol(String name)
Definition: Context.java:101
static long mkSeqToRe(long a0, long a1)
Definition: Native.java:2229
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1716
FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Definition: Context.java:3708
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1098
static long mkFpaRne(long a0)
Definition: Native.java:5691
String [] getTacticNames()
Definition: Context.java:2623
Probe eq(Probe p1, Probe p2)
Definition: Context.java:2947
BitVecExpr mkZeroExt(int i, BitVecExpr t)
Definition: Context.java:1374
ReExpr mkLoop(ReExpr re, int lo)
Definition: Context.java:2101
SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
Definition: Context.java:2056
static long mkOr(long a0, int a1, long[] a2)
Definition: Native.java:1212
BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1481
Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2457
BoolExpr mkDistinct(Expr... args)
Definition: Context.java:712
String getProbeDescription(String name)
Definition: Context.java:2872
IntNum mkInt(String v)
Definition: Context.java:2330
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1139
SeqExpr mkUnit(Expr elem)
Definition: Context.java:1966
Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1820
static long mkSub(long a0, int a1, long[] a2)
Definition: Native.java:1239
static long tacticFailIf(long a0, long a1)
Definition: Native.java:3996
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1443
static long mkExtRotateLeft(long a0, long a1, long a2)
Definition: Native.java:1680
static long mkSeqReplace(long a0, long a1, long a2, long a3)
Definition: Native.java:2175
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
Definition: Context.java:3553
FPRMNum mkFPRoundTowardNegative()
Definition: Context.java:3129
BoolExpr mkInRe(SeqExpr s, ReExpr re)
Definition: Context.java:2075
FPNum mkFP(float v, FPSort s)
Definition: Context.java:3342
static long mkFpaIsPositive(long a0, long a1)
Definition: Native.java:6141
static long mkFpaSort16(long a0)
Definition: Native.java:5790
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
Definition: Context.java:758
static long mkReStar(long a0, long a1)
Definition: Native.java:2256
static long mkFpaSqrt(long a0, long a1, long a2)
Definition: Native.java:5997
static long mkBvlshr(long a0, long a1, long a2)
Definition: Native.java:1644
ReExpr mkPlus(ReExpr re)
Definition: Context.java:2110
BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2549
BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1643
BitVecExpr mkExtract(int high, int low, BitVecExpr t)
Definition: Context.java:1345
UninterpretedSort mkUninterpretedSort(String str)
Definition: Context.java:188
BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1207
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4026
static String probeGetDescr(long a0, String a1)
Definition: Native.java:4167
static long mkBvuge(long a0, long a1, long a2)
Definition: Native.java:1554
static long mkSolverForLogic(long a0, long a1)
Definition: Native.java:4273
static long mkFpaAdd(long a0, long a1, long a2, long a3)
Definition: Native.java:5952
static long simplifyGetParamDescrs(long a0)
Definition: Native.java:3246
String [] getProbeNames()
Definition: Context.java:2858
BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3588
FPNum mkFPNaN(FPSort s)
Definition: Context.java:3250
static long mkLe(long a0, long a1, long a2)
Definition: Native.java:1302
static long mkSetIntersect(long a0, int a1, long[] a2)
Definition: Native.java:1914
static long mkFpaRem(long a0, long a1, long a2)
Definition: Native.java:6006
static long mkConcat(long a0, long a1, long a2)
Definition: Native.java:1590
static long mkSelect(long a0, long a1, long a2)
Definition: Native.java:1788
static long mkBvnand(long a0, long a1, long a2)
Definition: Native.java:1410
static long mkFpaRoundTowardNegative(long a0)
Definition: Native.java:5736
static long mkFpaToReal(long a0, long a1)
Definition: Native.java:6213
Tactic then(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2686
IDecRefQueue< Statistics > getStatisticsDRQ()
Definition: Context.java:4016
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1496
BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2571
static long probeEq(long a0, long a1, long a2)
Definition: Native.java:4068
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:3956
static long mkGe(long a0, long a1, long a2)
Definition: Native.java:1320
static long mkXor(long a0, long a1, long a2)
Definition: Native.java:1194
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2229
static long mkSeqInRe(long a0, long a1, long a2)
Definition: Native.java:2238
BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1175
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Definition: Context.java:266
BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1124
static long mkBvslt(long a0, long a1, long a2)
Definition: Native.java:1527
BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
Definition: Context.java:2002
FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
Definition: Context.java:466
Definition: FuncInterp.java:31
static long mkFpaEq(long a0, long a1, long a2)
Definition: Native.java:6078
void setPrintMode(Z3_ast_print_mode value)
Definition: Context.java:2515
FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3460
static long mkReUnion(long a0, int a1, long[] a2)
Definition: Native.java:2274
static long mkAdd(long a0, int a1, long[] a2)
Definition: Native.java:1221
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
Definition: Native.java:5916
static long mkReConcat(long a0, int a1, long[] a2)
Definition: Native.java:2283
FuncDecl mkConstDecl(String name, Sort range)
Definition: Context.java:513
ReExpr mkIntersect(ReExpr... t)
Definition: Context.java:2156
static long probeOr(long a0, long a1, long a2)
Definition: Native.java:4086
SetSort mkSetSort(Sort ty)
Definition: Context.java:1831
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:890
static long mkSeqIndex(long a0, long a1, long a2, long a3)
Definition: Native.java:2202
static long mkSeqSuffix(long a0, long a1, long a2)
Definition: Native.java:2148
static long mkSeqExtract(long a0, long a1, long a2, long a3)
Definition: Native.java:2166
FPExpr mkFPNeg(FPExpr t)
Definition: Context.java:3412
IntExpr mkReal2Int(RealExpr t)
Definition: Context.java:954
RatNum mkReal(int v)
Definition: Context.java:2306
IDecRefQueue< ASTMap > getASTMapDRQ()
Definition: Context.java:3961
static long probeNot(long a0, long a1)
Definition: Native.java:4095
static long mkSignExt(long a0, int a1, long a2)
Definition: Native.java:1608
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3318
FPRMExpr mkFPRoundNearestTiesToEven()
Definition: Context.java:3075
static long mkBvsmod(long a0, long a1, long a2)
Definition: Native.java:1509
AST wrapAST(long nativeObject)
Definition: Context.java:3843
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1725
BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1940
ArithExpr mkAdd(ArithExpr... t)
Definition: Context.java:800
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long mkSetComplement(long a0, long a1)
Definition: Native.java:1932
IDecRefQueue< Tactic > getTacticDRQ()
Definition: Context.java:4021
static long mkInt(long a0, int a1, long a2)
Definition: Native.java:1986
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
Definition: Context.java:453
static long probeConst(long a0, double a1)
Definition: Native.java:4023
static long mkReIntersect(long a0, int a1, long[] a2)
Definition: Native.java:2310
static long mkSetAdd(long a0, long a1, long a2)
Definition: Native.java:1887
static long mkFpaNumeralInt(long a0, int a1, long a2)
Definition: Native.java:5907
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1770
ReExpr mkToRe(SeqExpr s)
Definition: Context.java:2065
static long mkBvneg(long a0, long a1)
Definition: Native.java:1437
static long mkInt64(long a0, long a1, long a2)
Definition: Native.java:2004
FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Definition: Context.java:3760
BoolExpr mkFPIsPositive(FPExpr t)
Definition: Context.java:3658
BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2211
static long mkBvsdiv(long a0, long a1, long a2)
Definition: Native.java:1482
static long mkMap(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1833
FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
Definition: Context.java:3676
static int getNumTactics(long a0)
Definition: Native.java:4104
ArrayExpr mkSetDel(ArrayExpr set, Expr element)
Definition: Context.java:1872
static long mkAtmost(long a0, int a1, long[] a2, int a3)
Definition: Native.java:2634
static long mkZeroExt(long a0, int a1, long a2)
Definition: Native.java:1617
static long mkBvnot(long a0, long a1)
Definition: Native.java:1356
static long mkFpaRna(long a0)
Definition: Native.java:5709
static long mkDistinct(long a0, int a1, long[] a2)
Definition: Native.java:1149
BoolExpr mkIsInteger(RealExpr t)
Definition: Context.java:963
static long mkUnaryMinus(long a0, long a1)
Definition: Native.java:1248
BoolExpr mkBVNegNoOverflow(BitVecExpr t)
Definition: Context.java:1617
Expr mkUpdateField(FuncDecl field, Expr t, Expr v)
Definition: Context.java:428
static long mkSetDifference(long a0, long a1, long a2)
Definition: Native.java:1923
static long mkBvsgt(long a0, long a1, long a2)
Definition: Native.java:1581
static long mkSetDel(long a0, long a1, long a2)
Definition: Native.java:1896
static long mkRotateRight(long a0, int a1, long a2)
Definition: Native.java:1671
ReExpr mkComplement(ReExpr re)
Definition: Context.java:2129
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1743
static long mkStore(long a0, long a1, long a2, long a3)
Definition: Native.java:1806
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2470
FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
Definition: Context.java:3742
Probe gt(Probe p1, Probe p2)
Definition: Context.java:2909
BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3542
static long mkSolverFromTactic(long a0, long a1)
Definition: Native.java:4282
BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1259
static long mkBvadd(long a0, long a1, long a2)
Definition: Native.java:1446
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1561
static void delContext(long a0)
Definition: Native.java:729
BoolExpr mkFPIsInfinite(FPExpr t)
Definition: Context.java:3628
static long mkBvsle(long a0, long a1, long a2)
Definition: Native.java:1545
BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1022
BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1035
IDecRefQueue< Model > getModelDRQ()
Definition: Context.java:3991
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
Definition: Context.java:3976
ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
Definition: Context.java:1860
BitVecExpr mkBVNot(BitVecExpr t)
Definition: Context.java:974
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6767
static long mkFpaGeq(long a0, long a1, long a2)
Definition: Native.java:6060
static long mkFpaGt(long a0, long a1, long a2)
Definition: Native.java:6069
EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
Definition: Context.java:279
BitVecExpr mkBVRedOR(BitVecExpr t)
Definition: Context.java:997
static long mkFpaToFpBv(long a0, long a1, long a2)
Definition: Native.java:6150
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2796
BitVecExpr mkBVConst(String name, int size)
Definition: Context.java:659
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:901
static void setAstPrintMode(long a0, int a1)
Definition: Native.java:3582
BoolExpr mkFPIsNaN(FPExpr t)
Definition: Context.java:3638
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1160
static long mkDiv(long a0, long a1, long a2)
Definition: Native.java:1257
SeqExpr mkAt(SeqExpr s, IntExpr index)
Definition: Context.java:2029
static long mkIte(long a0, long a1, long a2, long a3)
Definition: Native.java:1167
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6204
FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3424
static String tacticGetDescr(long a0, String a1)
Definition: Native.java:4158
static long tacticFailIfNotDecided(long a0)
Definition: Native.java:4005
static long mkSeqConcat(long a0, int a1, long[] a2)
Definition: Native.java:2130
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1311
static long mkSimpleSolver(long a0)
Definition: Native.java:4264
static long mkPbge(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2661
static long mkSetMember(long a0, long a1, long a2)
Definition: Native.java:1941
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2431
static long mkFpaSortDouble(long a0)
Definition: Native.java:5817
static long mkFpaSort64(long a0)
Definition: Native.java:5826
FPRMNum mkFPRoundNearestTiesToAway()
Definition: Context.java:3093
BoolExpr mkBoolConst(String name)
Definition: Context.java:611
FPNum mkFPZero(FPSort s, boolean negative)
Definition: Context.java:3272
BoolExpr mkAtLeast(BoolExpr[] args, int k)
Definition: Context.java:2184
BitVecExpr mkRepeat(int i, BitVecExpr t)
Definition: Context.java:1386
FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Definition: Context.java:3475
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1048
void updateParamValue(String id, String value)
Definition: Context.java:3890
Probe mkProbe(String name)
Definition: Context.java:2880
BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
Definition: Context.java:769
BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1423
static long mkStoreN(long a0, long a1, int a2, long[] a3, long a4)
Definition: Native.java:1815
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:3971
static long tacticParOr(long a0, int a1, long[] a2)
Definition: Native.java:3924
static long tacticSkip(long a0)
Definition: Native.java:3978
static long mkString(long a0, String a1)
Definition: Native.java:2085
static long mkBvurem(long a0, long a1, long a2)
Definition: Native.java:1491
Tactic repeat(Tactic t, int max)
Definition: Context.java:2749
static long mkSetSubset(long a0, long a1, long a2)
Definition: Native.java:1950
IDecRefQueue< Optimize > getOptimizeDRQ()
Definition: Context.java:4031
static long mkImplies(long a0, long a1, long a2)
Definition: Native.java:1185
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
Definition: Context.java:2533
DatatypeSort [] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:389
FPNum mkFP(int v, FPSort s)
Definition: Context.java:3365
Tactic tryFor(Tactic t, int ms)
Definition: Context.java:2710
static long probeGt(long a0, long a1, long a2)
Definition: Native.java:4041
static long mkFpaAbs(long a0, long a1)
Definition: Native.java:5934
BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2193
static long mkFpaIsNan(long a0, long a1)
Definition: Native.java:6123
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
Definition: Context.java:747
IntExpr mkIntConst(String name)
Definition: Context.java:627
BoolExpr mkOr(BoolExpr... t)
Definition: Context.java:790
static long mkFpaSortSingle(long a0)
Definition: Native.java:5799
static long mkEq(long a0, long a1, long a2)
Definition: Native.java:1140
static long mkRem(long a0, long a1, long a2)
Definition: Native.java:1275
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8850
Probe not(Probe p)
Definition: Context.java:2980
static long mkExtRotateRight(long a0, long a1, long a2)
Definition: Native.java:1689
static long mkFpaMul(long a0, long a1, long a2, long a3)
Definition: Native.java:5970
ReExpr mkRange(SeqExpr lo, SeqExpr hi)
Definition: Context.java:2165
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1246
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3378
static long mkAtleast(long a0, int a1, long[] a2, int a3)
Definition: Native.java:2643
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1285
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1061
IDecRefQueue< ASTVector > getASTVectorDRQ()
Definition: Context.java:3966
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
Definition: Context.java:441
IntExpr mkLength(SeqExpr s)
Definition: Context.java:1993
IntNum mkInt(long v)
Definition: Context.java:2356
Solver mkSolver(String logic)
Definition: Context.java:3019
static long mkInt2bv(long a0, int a1, long a2)
Definition: Native.java:1698
BitVecExpr mkBVRedAND(BitVecExpr t)
Definition: Context.java:985
IntExpr mkRem(IntExpr t1, IntExpr t2)
Definition: Context.java:866
FiniteDomainSort mkFiniteDomainSort(String name, long size)
Definition: Context.java:328
static long mkFpaRtz(long a0)
Definition: Native.java:5763
static long mkBvand(long a0, long a1, long a2)
Definition: Native.java:1383
FuncDecl mkConstDecl(Symbol name, Sort range)
Definition: Context.java:503
static long mkRepeat(long a0, int a1, long a2)
Definition: Native.java:1626
FPRMNum mkFPRoundTowardPositive()
Definition: Context.java:3111
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1589
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
Definition: Native.java:1061
static long mkReOption(long a0, long a1)
Definition: Native.java:2265
ReExpr mkUnion(ReExpr... t)
Definition: Context.java:2147
static long mkPattern(long a0, int a1, long[] a2)
Definition: Native.java:2346
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
Definition: Native.java:6015
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:179
ArithExpr mkMul(ArithExpr... t)
Definition: Context.java:810
static String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
Definition: Native.java:3635
static native void setInternalErrorHandler(long ctx)
static long mkFpaNumeralFloat(long a0, float a1, long a2)
Definition: Native.java:5889
static long mkBvult(long a0, long a1, long a2)
Definition: Native.java:1518
FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3448
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:708
SeqExpr mkString(String s)
Definition: Context.java:1975
ReExpr mkStar(ReExpr re)
Definition: Context.java:2084
BoolExpr mkAnd(BoolExpr... t)
Definition: Context.java:780
Expr mkFreshConst(String prefix, Sort range)
Definition: Context.java:584
static long mkSeqAt(long a0, long a1, long a2)
Definition: Native.java:2184
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Definition: Context.java:3509
static long mkAnd(long a0, int a1, long[] a2)
Definition: Native.java:1203
Tactic failIf(Probe p)
Definition: Context.java:2776
static long mkSeqUnit(long a0, long a1)
Definition: Native.java:2121
static long mkLt(long a0, long a1, long a2)
Definition: Native.java:1293
static long mkReLoop(long a0, long a1, int a2, int a3)
Definition: Native.java:2301
static long mkContextRc(long a0)
Definition: Native.java:721
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
Definition: Context.java:3497
IDecRefQueue< ConstructorList > getConstructorListDRQ()
Definition: Context.java:3952
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:4011
static long mkFpaRtp(long a0)
Definition: Native.java:5727
FPNum mkFP(double v, FPSort s)
Definition: Context.java:3353
ArrayExpr mkEmptySet(Sort domain)
Definition: Context.java:1840
static long mkFpaRoundTowardPositive(long a0)
Definition: Native.java:5718
static long mkPbeq(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2670
ArraySort mkArraySort(Sort[] domains, Sort range)
Definition: Context.java:231
static long mkFpaIsSubnormal(long a0, long a1)
Definition: Native.java:6096
Expr mkTermArray(ArrayExpr array)
Definition: Context.java:1810
static long mkBvsub(long a0, long a1, long a2)
Definition: Native.java:1455
static long mkFpaToIeeeBv(long a0, long a1)
Definition: Native.java:6375
static long mkConstArray(long a0, long a1, long a2)
Definition: Native.java:1824
EnumSort mkEnumSort(String name, String... enumNames)
Definition: Context.java:290
static long mkSeqSort(long a0, long a1)
Definition: Native.java:2031
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Definition: Context.java:4001
static long mkInt2real(long a0, long a1)
Definition: Native.java:1329
FPExpr mkFPMin(FPExpr t1, FPExpr t2)
Definition: Context.java:3520
BoolExpr mkBool(boolean value)
Definition: Context.java:693
static long mkConst(long a0, long a1, long a2)
Definition: Native.java:1095
static long mkFpaInf(long a0, long a1, boolean a2)
Definition: Native.java:5862
static long mkBvsge(long a0, long a1, long a2)
Definition: Native.java:1563
SeqSort mkSeqSort(Sort s)
Definition: Context.java:249
def ArraySort(d, r)
Definition: z3py.py:4199
static long mkReSort(long a0, long a1)
Definition: Native.java:2049
Probe or(Probe p1, Probe p2)
Definition: Context.java:2969
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
Definition: Native.java:6159
BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
Definition: Context.java:3827
static long mkFpaRoundNearestTiesToAway(long a0)
Definition: Native.java:5700
static long tacticParAndThen(long a0, long a1, long a2)
Definition: Native.java:3933
static String getProbeName(long a0, int a1)
Definition: Native.java:4131
FPExpr mkFPAbs(FPExpr t)
Definition: Context.java:3402
def IntSort(ctx=None)
Definition: z3py.py:2746
FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3436
Tactic with(Tactic t, Params p)
Definition: Context.java:2810
IntExpr mkMod(IntExpr t1, IntExpr t2)
Definition: Context.java:853
BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
Definition: Context.java:3777
Probe ge(Probe p1, Probe p2)
Definition: Context.java:2935
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4668
static long mkBvashr(long a0, long a1, long a2)
Definition: Native.java:1653
static long mkReRange(long a0, long a1, long a2)
Definition: Native.java:2292
static long mkGt(long a0, long a1, long a2)
Definition: Native.java:1311
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:667
ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
Definition: Context.java:1655
static long mkFullSet(long a0, long a1)
Definition: Native.java:1878
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
Definition: Context.java:318
ReExpr mkLoop(ReExpr re, int lo, int hi)
Definition: Context.java:2093
static long mkPble(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2652
BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1233
BitVecExpr mkInt2BV(int n, IntExpr t)
Definition: Context.java:1514
BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
Definition: Context.java:1468
ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
Definition: Context.java:877
IDecRefQueue< Constructor > getConstructorDRQ()
Definition: Context.java:3948
static long probeLe(long a0, long a1, long a2)
Definition: Native.java:4050
Context(Map< String, String > settings)
Definition: Context.java:71
ArrayExpr mkSetUnion(ArrayExpr... args)
Definition: Context.java:1884
BoolExpr mkBoolConst(Symbol name)
Definition: Context.java:603
static long mkFpaIsInfinite(long a0, long a1)
Definition: Native.java:6114
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
Definition: Context.java:3531
ArrayExpr mkFullSet(Sort domain)
Definition: Context.java:1850
IntSymbol mkSymbol(int i)
Definition: Context.java:93
ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
Definition: Context.java:1756
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2444
Expr mkConst(String name, Sort range)
Definition: Context.java:575
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3644
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
Definition: Context.java:366
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1779
static long mkRotateLeft(long a0, int a1, long a2)
Definition: Native.java:1662
static String simplifyGetHelp(long a0)
Definition: Native.java:3237
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
Definition: Native.java:5925
Tactic parAndThen(Tactic t1, Tactic t2)
Definition: Context.java:2829
ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
Definition: Context.java:1795
static long mkFpaMin(long a0, long a1, long a2)
Definition: Native.java:6024
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
Definition: Context.java:1456
static long mkBvredand(long a0, long a1)
Definition: Native.java:1365
static long tacticFail(long a0)
Definition: Native.java:3987
static long mkSeqLength(long a0, long a1)
Definition: Native.java:2193
Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
Definition: Context.java:356
static long mkBvxor(long a0, long a1, long a2)
Definition: Native.java:1401
SeqExpr mkConcat(SeqExpr... t)
Definition: Context.java:1983
static long tacticUsingParams(long a0, long a1, long a2)
Definition: Native.java:4014
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1220
Probe constProbe(double val)
Definition: Context.java:2888
static long probeLt(long a0, long a1, long a2)
Definition: Native.java:4032
static long mkFpaIsNormal(long a0, long a1)
Definition: Native.java:6087
static long mkBvudiv(long a0, long a1, long a2)
Definition: Native.java:1473
static long mkFpaNan(long a0, long a1)
Definition: Native.java:5853
static long probeGe(long a0, long a1, long a2)
Definition: Native.java:4059
static long mkBvshl(long a0, long a1, long a2)
Definition: Native.java:1635
static long mkFalse(long a0)
Definition: Native.java:1131
static long mkFpaRtn(long a0)
Definition: Native.java:5745
static long mkBvsrem(long a0, long a1, long a2)
Definition: Native.java:1500
BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1009
BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1575
BitVecExpr mkFPToIEEEBV(FPExpr t)
Definition: Context.java:3809
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3571
static long mkEmptySet(long a0, long a1)
Definition: Native.java:1869
static long mkFpaRoundNearestTiesToEven(long a0)
Definition: Native.java:5682
Expr mkBound(int index, Sort ty)
Definition: Context.java:537
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1752
RatNum mkReal(long v)
Definition: Context.java:2319
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3283
static String getTacticName(long a0, int a1)
Definition: Native.java:4113
static long mkRePlus(long a0, long a1)
Definition: Native.java:2247
BitVecExpr mkBVConst(Symbol name, int size)
Definition: Context.java:651
static long tacticTryFor(long a0, long a1, int a2)
Definition: Native.java:3942
static long mkArrayDefault(long a0, long a1)
Definition: Native.java:1842
static long mkBvnegNoOverflow(long a0, long a1)
Definition: Native.java:1761
static long mkArrayExt(long a0, long a1, long a2)
Definition: Native.java:1959
static long mkStringSort(long a0)
Definition: Native.java:2067
static long mkBound(long a0, int a1, long a2)
Definition: Native.java:2355
static long mkTrue(long a0)
Definition: Native.java:1122
Tactic mkTactic(String name)
Definition: Context.java:2645
static long mkFpaSort128(long a0)
Definition: Native.java:5844
static long mkMul(long a0, int a1, long[] a2)
Definition: Native.java:1230
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
Definition: Native.java:6168
static long mkSeqEmpty(long a0, long a1)
Definition: Native.java:2112
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3331
static long mkReal(long a0, int a1, int a2)
Definition: Native.java:1977
FPSort mkFPSort(int ebits, int sbits)
Definition: Context.java:3167
static long tacticAndThen(long a0, long a1, long a2)
Definition: Native.java:3906
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
Definition: Context.java:1731
SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
Definition: Context.java:2038
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212
static long mkFpaLt(long a0, long a1, long a2)
Definition: Native.java:6051
ParamDescrs getSimplifyParameterDescriptions()
Definition: Context.java:3877
IDecRefQueue< Params > getParamsDRQ()
Definition: Context.java:3996
SeqExpr mkEmptySeq(Sort s)
Definition: Context.java:1957
Fixedpoint mkFixedpoint()
Definition: Context.java:3048
BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
Definition: Context.java:2020
static long mkBvxnor(long a0, long a1, long a2)
Definition: Native.java:1428
static long mkSeqPrefix(long a0, long a1, long a2)
Definition: Native.java:2139
static long mkSelectN(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1797
static long mkFpaMax(long a0, long a1, long a2)
Definition: Native.java:6033
static long mkFpaSub(long a0, long a1, long a2, long a3)
Definition: Native.java:5961
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3391
BoolExpr mkFPIsNormal(FPExpr t)
Definition: Context.java:3598
IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Definition: Context.java:2047
static long mkSetUnion(long a0, int a1, long[] a2)
Definition: Native.java:1905
Tactic cond(Probe p, Tactic t1, Tactic t2)
Definition: Context.java:2736
static long mkPower(long a0, long a1, long a2)
Definition: Native.java:1284
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1193
static long mkFpaIsZero(long a0, long a1)
Definition: Native.java:6105
Solver mkSolver(Symbol logic)
Definition: Context.java:3005
def Map(f, args)
Definition: z3py.py:4296
FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
Definition: Context.java:3692
FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
Definition: Context.java:477
ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
Definition: Context.java:1664
static long mkBvor(long a0, long a1, long a2)
Definition: Native.java:1392
BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3564
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:220
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
Tactic parOr(Tactic... t)
Definition: Context.java:2818
BitVecNum mkBV(int v, int size)
Definition: Context.java:2378
static long mkBv2int(long a0, long a1, boolean a2)
Definition: Native.java:1707
BoolExpr mkNot(BoolExpr a)
Definition: Context.java:722
BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2202
Expr mkNumeral(long v, Sort ty)
Definition: Context.java:2262
DatatypeSort [] mkDatatypeSorts(String[] names, Constructor[][] c)
Definition: Context.java:416
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:912
FPRMSort mkFPRoundingModeSort()
Definition: Context.java:3066
ReExpr mkOption(ReExpr re)
Definition: Context.java:2119
ListSort mkListSort(Symbol name, Sort elemSort)
Definition: Context.java:299
static long mkFpaRoundTowardZero(long a0)
Definition: Native.java:5754
Tactic orElse(Tactic t1, Tactic t2)
Definition: Context.java:2696
ReSort mkReSort(Sort s)
Definition: Context.java:257
Expr mkConst(FuncDecl f)
Definition: Context.java:595
Probe le(Probe p1, Probe p2)
Definition: Context.java:2922
ArithExpr mkUnaryMinus(ArithExpr t)
Definition: Context.java:830
static long probeAnd(long a0, long a1, long a2)
Definition: Native.java:4077
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2654
RealExpr mkInt2Real(IntExpr t)
Definition: Context.java:941
RealExpr mkRealConst(Symbol name)
Definition: Context.java:635
static long mkBvmul(long a0, long a1, long a2)
Definition: Native.java:1464
static long mkFpaSortQuadruple(long a0)
Definition: Native.java:5835
static long datatypeUpdateField(long a0, long a1, long a2, long a3)
Definition: Native.java:2607
FuncDecl mkFreshConstDecl(String prefix, Sort range)
Definition: Context.java:525
Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2488
static long mkFpaNumeralDouble(long a0, double a1, long a2)
Definition: Native.java:5898
BitVecNum mkBV(String v, int size)
Definition: Context.java:2368
Solver mkSolver(Tactic t)
Definition: Context.java:3038
String getTacticDescription(String name)
Definition: Context.java:2637
Expr mkSelect(ArrayExpr a, Expr i)
Definition: Context.java:1683
static long mkFpaFma(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:5988
static long mkReal2int(long a0, long a1)
Definition: Native.java:1338
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
Definition: Context.java:492
static long mkFpaSortHalf(long a0)
Definition: Native.java:5781
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6195
BitVecNum mkBV(long v, int size)
Definition: Context.java:2388
BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1111
static long tacticWhen(long a0, long a1, long a2)
Definition: Native.java:3951
ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
Definition: Context.java:840
RealExpr mkRealConst(String name)
Definition: Context.java:643
static long mkNot(long a0, long a1)
Definition: Native.java:1158
ArrayExpr mkSetIntersection(ArrayExpr... args)
Definition: Context.java:1895
static long mkBvSort(long a0, int a1)
Definition: Native.java:955
FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Definition: Context.java:3724
static long mkFpaSort32(long a0)
Definition: Native.java:5808
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1329
RatNum mkReal(int num, int den)
Definition: Context.java:2278
BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
Definition: Context.java:3575
BitVecExpr mkSignExt(int i, BitVecExpr t)
Definition: Context.java:1360
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1298
BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
Definition: Context.java:1928
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
Definition: Context.java:1535
IDecRefQueue< FuncInterp > getFuncInterpDRQ()
Definition: Context.java:3981
static long mkIsInt(long a0, long a1)
Definition: Native.java:1347
FPRMNum mkFPRoundTowardZero()
Definition: Context.java:3147
static long mkFpaLeq(long a0, long a1, long a2)
Definition: Native.java:6042
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3653
BoolExpr mkEq(Expr x, Expr y)
Definition: Context.java:701
static long mkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:6384
static long mkReComplement(long a0, long a1)
Definition: Native.java:2319
def BoolSort(ctx=None)
Definition: z3py.py:1435
static long mkBvsubNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1734
static long mkIff(long a0, long a1, long a2)
Definition: Native.java:1176
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:923
BoolExpr mkFPIsZero(FPExpr t)
Definition: Context.java:3618
def String(name, ctx=None)
Definition: z3py.py:9738
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:3986
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2418
ArithExpr mkSub(ArithExpr... t)
Definition: Context.java:820
BoolExpr mkAtMost(BoolExpr[] args, int k)
Definition: Context.java:2175
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
Definition: Context.java:2598
static long tacticCond(long a0, long a1, long a2, long a3)
Definition: Native.java:3960
static long mkFpaZero(long a0, long a1, boolean a2)
Definition: Native.java:5871
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1547
static long mkBvnor(long a0, long a1, long a2)
Definition: Native.java:1419