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 
2552  public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
2553  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2554  {
2555  int csn = Symbol.arrayLength(sortNames);
2556  int cs = Sort.arrayLength(sorts);
2557  int cdn = Symbol.arrayLength(declNames);
2558  int cd = AST.arrayLength(decls);
2559  if (csn != cs || cdn != cd) {
2560  throw new Z3Exception("Argument size mismatch");
2561  }
2562  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2563  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2564  AST.arrayToNative(sorts), AST.arrayLength(decls),
2565  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2566  }
2567 
2572  public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
2573  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2574 
2575  {
2576  int csn = Symbol.arrayLength(sortNames);
2577  int cs = Sort.arrayLength(sorts);
2578  int cdn = Symbol.arrayLength(declNames);
2579  int cd = AST.arrayLength(decls);
2580  if (csn != cs || cdn != cd)
2581  throw new Z3Exception("Argument size mismatch");
2582  return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
2583  fileName, AST.arrayLength(sorts),
2584  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2585  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2586  AST.arrayToNative(decls)));
2587  }
2588 
2599  public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
2600 
2601  {
2602  return new Goal(this, models, unsatCores, proofs);
2603  }
2604 
2608  public Params mkParams()
2609  {
2610  return new Params(this);
2611  }
2612 
2616  public int getNumTactics()
2617  {
2618  return Native.getNumTactics(nCtx());
2619  }
2620 
2625  {
2626 
2627  int n = getNumTactics();
2628  String[] res = new String[n];
2629  for (int i = 0; i < n; i++)
2630  res[i] = Native.getTacticName(nCtx(), i);
2631  return res;
2632  }
2633 
2639  {
2640  return Native.tacticGetDescr(nCtx(), name);
2641  }
2642 
2646  public Tactic mkTactic(String name)
2647  {
2648  return new Tactic(this, name);
2649  }
2650 
2655  public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
2656 
2657  {
2658  checkContextMatch(t1);
2659  checkContextMatch(t2);
2660  checkContextMatch(ts);
2661 
2662  long last = 0;
2663  if (ts != null && ts.length > 0)
2664  {
2665  last = ts[ts.length - 1].getNativeObject();
2666  for (int i = ts.length - 2; i >= 0; i--) {
2667  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2668  last);
2669  }
2670  }
2671  if (last != 0)
2672  {
2673  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2674  return new Tactic(this, Native.tacticAndThen(nCtx(),
2675  t1.getNativeObject(), last));
2676  } else
2677  return new Tactic(this, Native.tacticAndThen(nCtx(),
2678  t1.getNativeObject(), t2.getNativeObject()));
2679  }
2680 
2687  public Tactic then(Tactic t1, Tactic t2, Tactic... ts)
2688  {
2689  return andThen(t1, t2, ts);
2690  }
2691 
2697  public Tactic orElse(Tactic t1, Tactic t2)
2698  {
2699  checkContextMatch(t1);
2700  checkContextMatch(t2);
2701  return new Tactic(this, Native.tacticOrElse(nCtx(),
2702  t1.getNativeObject(), t2.getNativeObject()));
2703  }
2704 
2711  public Tactic tryFor(Tactic t, int ms)
2712  {
2713  checkContextMatch(t);
2714  return new Tactic(this, Native.tacticTryFor(nCtx(),
2715  t.getNativeObject(), ms));
2716  }
2717 
2724  public Tactic when(Probe p, Tactic t)
2725  {
2726  checkContextMatch(t);
2727  checkContextMatch(p);
2728  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2729  t.getNativeObject()));
2730  }
2731 
2737  public Tactic cond(Probe p, Tactic t1, Tactic t2)
2738  {
2739  checkContextMatch(p);
2740  checkContextMatch(t1);
2741  checkContextMatch(t2);
2742  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2743  t1.getNativeObject(), t2.getNativeObject()));
2744  }
2745 
2750  public Tactic repeat(Tactic t, int max)
2751  {
2752  checkContextMatch(t);
2753  return new Tactic(this, Native.tacticRepeat(nCtx(),
2754  t.getNativeObject(), max));
2755  }
2756 
2760  public Tactic skip()
2761  {
2762  return new Tactic(this, Native.tacticSkip(nCtx()));
2763  }
2764 
2768  public Tactic fail()
2769  {
2770  return new Tactic(this, Native.tacticFail(nCtx()));
2771  }
2772 
2777  public Tactic failIf(Probe p)
2778  {
2779  checkContextMatch(p);
2780  return new Tactic(this,
2781  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2782  }
2783 
2789  {
2790  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2791  }
2792 
2798  {
2799  checkContextMatch(t);
2800  checkContextMatch(p);
2801  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2802  t.getNativeObject(), p.getNativeObject()));
2803  }
2804 
2811  public Tactic with(Tactic t, Params p)
2812  {
2813  return usingParams(t, p);
2814  }
2815 
2819  public Tactic parOr(Tactic... t)
2820  {
2821  checkContextMatch(t);
2822  return new Tactic(this, Native.tacticParOr(nCtx(),
2823  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2824  }
2825 
2831  {
2832  checkContextMatch(t1);
2833  checkContextMatch(t2);
2834  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2835  t1.getNativeObject(), t2.getNativeObject()));
2836  }
2837 
2843  public void interrupt()
2844  {
2845  Native.interrupt(nCtx());
2846  }
2847 
2851  public int getNumProbes()
2852  {
2853  return Native.getNumProbes(nCtx());
2854  }
2855 
2860  {
2861 
2862  int n = getNumProbes();
2863  String[] res = new String[n];
2864  for (int i = 0; i < n; i++)
2865  res[i] = Native.getProbeName(nCtx(), i);
2866  return res;
2867  }
2868 
2874  {
2875  return Native.probeGetDescr(nCtx(), name);
2876  }
2877 
2881  public Probe mkProbe(String name)
2882  {
2883  return new Probe(this, name);
2884  }
2885 
2889  public Probe constProbe(double val)
2890  {
2891  return new Probe(this, Native.probeConst(nCtx(), val));
2892  }
2893 
2898  public Probe lt(Probe p1, Probe p2)
2899  {
2900  checkContextMatch(p1);
2901  checkContextMatch(p2);
2902  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2903  p2.getNativeObject()));
2904  }
2905 
2910  public Probe gt(Probe p1, Probe p2)
2911  {
2912  checkContextMatch(p1);
2913  checkContextMatch(p2);
2914  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2915  p2.getNativeObject()));
2916  }
2917 
2923  public Probe le(Probe p1, Probe p2)
2924  {
2925  checkContextMatch(p1);
2926  checkContextMatch(p2);
2927  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2928  p2.getNativeObject()));
2929  }
2930 
2936  public Probe ge(Probe p1, Probe p2)
2937  {
2938  checkContextMatch(p1);
2939  checkContextMatch(p2);
2940  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2941  p2.getNativeObject()));
2942  }
2943 
2948  public Probe eq(Probe p1, Probe p2)
2949  {
2950  checkContextMatch(p1);
2951  checkContextMatch(p2);
2952  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2953  p2.getNativeObject()));
2954  }
2955 
2959  public Probe and(Probe p1, Probe p2)
2960  {
2961  checkContextMatch(p1);
2962  checkContextMatch(p2);
2963  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
2964  p2.getNativeObject()));
2965  }
2966 
2970  public Probe or(Probe p1, Probe p2)
2971  {
2972  checkContextMatch(p1);
2973  checkContextMatch(p2);
2974  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
2975  p2.getNativeObject()));
2976  }
2977 
2981  public Probe not(Probe p)
2982  {
2983  checkContextMatch(p);
2984  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2985  }
2986 
2994  public Solver mkSolver()
2995  {
2996  return mkSolver((Symbol) null);
2997  }
2998 
3006  public Solver mkSolver(Symbol logic)
3007  {
3008 
3009  if (logic == null)
3010  return new Solver(this, Native.mkSolver(nCtx()));
3011  else
3012  return new Solver(this, Native.mkSolverForLogic(nCtx(),
3013  logic.getNativeObject()));
3014  }
3015 
3020  public Solver mkSolver(String logic)
3021  {
3022  return mkSolver(mkSymbol(logic));
3023  }
3024 
3029  {
3030  return new Solver(this, Native.mkSimpleSolver(nCtx()));
3031  }
3032 
3040  {
3041 
3042  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3043  t.getNativeObject()));
3044  }
3045 
3050  {
3051  return new Fixedpoint(this);
3052  }
3053 
3058  {
3059  return new Optimize(this);
3060  }
3061 
3062 
3068  {
3069  return new FPRMSort(this);
3070  }
3071 
3077  {
3078  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3079  }
3080 
3085  public FPRMNum mkFPRNE()
3086  {
3087  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3088  }
3089 
3095  {
3096  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3097  }
3098 
3103  public FPRMNum mkFPRNA()
3104  {
3105  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3106  }
3107 
3113  {
3114  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3115  }
3116 
3121  public FPRMNum mkFPRTP()
3122  {
3123  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3124  }
3125 
3131  {
3132  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3133  }
3134 
3139  public FPRMNum mkFPRTN()
3140  {
3141  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3142  }
3143 
3149  {
3150  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3151  }
3152 
3157  public FPRMNum mkFPRTZ()
3158  {
3159  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3160  }
3161 
3168  public FPSort mkFPSort(int ebits, int sbits)
3169  {
3170  return new FPSort(this, ebits, sbits);
3171  }
3172 
3178  {
3179  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3180  }
3181 
3187  {
3188  return new FPSort(this, Native.mkFpaSort16(nCtx()));
3189  }
3190 
3196  {
3197  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3198  }
3199 
3205  {
3206  return new FPSort(this, Native.mkFpaSort32(nCtx()));
3207  }
3208 
3214  {
3215  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3216  }
3217 
3223  {
3224  return new FPSort(this, Native.mkFpaSort64(nCtx()));
3225  }
3226 
3232  {
3233  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3234  }
3235 
3241  {
3242  return new FPSort(this, Native.mkFpaSort128(nCtx()));
3243  }
3244 
3245 
3252  {
3253  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3254  }
3255 
3262  public FPNum mkFPInf(FPSort s, boolean negative)
3263  {
3264  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3265  }
3266 
3273  public FPNum mkFPZero(FPSort s, boolean negative)
3274  {
3275  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3276  }
3277 
3284  public FPNum mkFPNumeral(float v, FPSort s)
3285  {
3286  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3287  }
3288 
3295  public FPNum mkFPNumeral(double v, FPSort s)
3296  {
3297  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3298  }
3299 
3306  public FPNum mkFPNumeral(int v, FPSort s)
3307  {
3308  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3309  }
3310 
3319  public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
3320  {
3321  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3322  }
3323 
3332  public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
3333  {
3334  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3335  }
3336 
3343  public FPNum mkFP(float v, FPSort s)
3344  {
3345  return mkFPNumeral(v, s);
3346  }
3347 
3354  public FPNum mkFP(double v, FPSort s)
3355  {
3356  return mkFPNumeral(v, s);
3357  }
3358 
3366  public FPNum mkFP(int v, FPSort s)
3367  {
3368  return mkFPNumeral(v, s);
3369  }
3370 
3379  public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
3380  {
3381  return mkFPNumeral(sgn, sig, exp, s);
3382  }
3383 
3392  public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
3393  {
3394  return mkFPNumeral(sgn, sig, exp, s);
3395  }
3396 
3397 
3403  public FPExpr mkFPAbs(FPExpr t)
3404  {
3405  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3406  }
3407 
3413  public FPExpr mkFPNeg(FPExpr t)
3414  {
3415  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3416  }
3417 
3425  public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
3426  {
3427  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3428  }
3429 
3437  public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
3438  {
3439  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3440  }
3441 
3449  public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
3450  {
3451  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3452  }
3453 
3461  public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
3462  {
3463  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3464  }
3465 
3476  public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
3477  {
3478  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3479  }
3480 
3488  {
3489  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3490  }
3491 
3498  public FPExpr mkFPRem(FPExpr t1, FPExpr t2)
3499  {
3500  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3501  }
3502 
3511  {
3512  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3513  }
3514 
3521  public FPExpr mkFPMin(FPExpr t1, FPExpr t2)
3522  {
3523  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3524  }
3525 
3532  public FPExpr mkFPMax(FPExpr t1, FPExpr t2)
3533  {
3534  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3535  }
3536 
3543  public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
3544  {
3545  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3546  }
3547 
3554  public BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
3555  {
3556  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3557  }
3558 
3565  public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
3566  {
3567  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3568  }
3569 
3576  public BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
3577  {
3578  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3579  }
3580 
3589  public BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
3590  {
3591  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3592  }
3593 
3600  {
3601  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3602  }
3603 
3610  {
3611  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3612  }
3613 
3620  {
3621  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3622  }
3623 
3630  {
3631  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3632  }
3633 
3640  {
3641  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3642  }
3643 
3650  {
3651  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3652  }
3653 
3660  {
3661  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3662  }
3663 
3678  {
3679  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3680  }
3681 
3694  {
3695  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3696  }
3697 
3710  {
3711  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3712  }
3713 
3726  {
3727  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3728  }
3729 
3743  public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
3744  {
3745  if (signed)
3746  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3747  else
3748  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3749  }
3750 
3762  {
3763  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3764  }
3765 
3778  public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
3779  {
3780  if (signed)
3781  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3782  else
3783  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3784  }
3785 
3796  {
3797  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3798  }
3799 
3811  {
3812  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3813  }
3814 
3829  {
3830  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3831  }
3832 
3833 
3844  public AST wrapAST(long nativeObject)
3845  {
3846  return AST.create(this, nativeObject);
3847  }
3848 
3861  public long unwrapAST(AST a)
3862  {
3863  return a.getNativeObject();
3864  }
3865 
3871  {
3872  return Native.simplifyGetHelp(nCtx());
3873  }
3874 
3879  {
3880  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3881  }
3882 
3891  public void updateParamValue(String id, String value)
3892  {
3893  Native.updateParamValue(nCtx(), id, value);
3894  }
3895 
3896 
3897  long nCtx()
3898  {
3899  return m_ctx;
3900  }
3901 
3902 
3903  void checkContextMatch(Z3Object other)
3904  {
3905  if (this != other.getContext())
3906  throw new Z3Exception("Context mismatch");
3907  }
3908 
3909  void checkContextMatch(Z3Object other1, Z3Object other2)
3910  {
3911  checkContextMatch(other1);
3912  checkContextMatch(other2);
3913  }
3914 
3915  void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
3916  {
3917  checkContextMatch(other1);
3918  checkContextMatch(other2);
3919  checkContextMatch(other3);
3920  }
3921 
3922  void checkContextMatch(Z3Object[] arr)
3923  {
3924  if (arr != null)
3925  for (Z3Object a : arr)
3926  checkContextMatch(a);
3927  }
3928 
3929  private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
3930  private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
3931  private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
3932  private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
3933  private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
3934  private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
3935  private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
3936  private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
3937  private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
3938  private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
3939  private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
3940  private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
3941  private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
3942  private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
3943  private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
3944  private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
3945  private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
3946  private ConstructorListDecRefQueue m_ConstructorList_DRQ =
3947  new ConstructorListDecRefQueue();
3948 
3950  return m_Constructor_DRQ;
3951  }
3952 
3954  return m_ConstructorList_DRQ;
3955  }
3956 
3958  {
3959  return m_AST_DRQ;
3960  }
3961 
3963  {
3964  return m_ASTMap_DRQ;
3965  }
3966 
3968  {
3969  return m_ASTVector_DRQ;
3970  }
3971 
3973  {
3974  return m_ApplyResult_DRQ;
3975  }
3976 
3978  {
3979  return m_FuncEntry_DRQ;
3980  }
3981 
3983  {
3984  return m_FuncInterp_DRQ;
3985  }
3986 
3988  {
3989  return m_Goal_DRQ;
3990  }
3991 
3993  {
3994  return m_Model_DRQ;
3995  }
3996 
3998  {
3999  return m_Params_DRQ;
4000  }
4001 
4003  {
4004  return m_ParamDescrs_DRQ;
4005  }
4006 
4008  {
4009  return m_Probe_DRQ;
4010  }
4011 
4013  {
4014  return m_Solver_DRQ;
4015  }
4016 
4018  {
4019  return m_Statistics_DRQ;
4020  }
4021 
4023  {
4024  return m_Tactic_DRQ;
4025  }
4026 
4028  {
4029  return m_Fixedpoint_DRQ;
4030  }
4031 
4033  {
4034  return m_Optimize_DRQ;
4035  }
4036 
4040  @Override
4041  public void close()
4042  {
4043  m_AST_DRQ.forceClear(this);
4044  m_ASTMap_DRQ.forceClear(this);
4045  m_ASTVector_DRQ.forceClear(this);
4046  m_ApplyResult_DRQ.forceClear(this);
4047  m_FuncEntry_DRQ.forceClear(this);
4048  m_FuncInterp_DRQ.forceClear(this);
4049  m_Goal_DRQ.forceClear(this);
4050  m_Model_DRQ.forceClear(this);
4051  m_Params_DRQ.forceClear(this);
4052  m_Probe_DRQ.forceClear(this);
4053  m_Solver_DRQ.forceClear(this);
4054  m_Optimize_DRQ.forceClear(this);
4055  m_Statistics_DRQ.forceClear(this);
4056  m_Tactic_DRQ.forceClear(this);
4057  m_Fixedpoint_DRQ.forceClear(this);
4058 
4059  m_boolSort = null;
4060  m_intSort = null;
4061  m_realSort = null;
4062  m_stringSort = null;
4063 
4064  synchronized (creation_lock) {
4065  Native.delContext(m_ctx);
4066  }
4067  }
4068 }
BoolExpr mkFPIsNegative(FPExpr t)
Definition: Context.java:3649
static long mkFpaFp(long a0, long a1, long a2, long a3)
Definition: Native.java:5900
IntExpr mkIntConst(Symbol name)
Definition: Context.java:619
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6197
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1629
static long tacticRepeat(long a0, long a1, int a2)
Definition: Native.java:3989
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:4007
static long mkBvule(long a0, long a1, long a2)
Definition: Native.java:1538
static long mkSolver(long a0)
Definition: Native.java:4275
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6206
Tactic when(Probe p, Tactic t)
Definition: Context.java:2724
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:1601
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
Definition: Context.java:377
static void interrupt(long a0)
Definition: Native.java:760
Pattern mkPattern(Expr... terms)
Definition: Context.java:546
def SeqSort(s)
Definition: z3py.py:9735
Probe and(Probe p1, Probe p2)
Definition: Context.java:2959
static long mkMod(long a0, long a1, long a2)
Definition: Native.java:1268
static long mkBvugt(long a0, long a1, long a2)
Definition: Native.java:1574
static long mkSeqContains(long a0, long a1, long a2)
Definition: Native.java:2159
Expr mkSelect(ArrayExpr a, Expr[] args)
Definition: Context.java:1706
static void delConfig(long a0)
Definition: Native.java:705
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:1376
RealExpr mkFPToReal(FPExpr t)
Definition: Context.java:3795
static long tacticOrElse(long a0, long a1, long a2)
Definition: Native.java:3935
Probe lt(Probe p1, Probe p2)
Definition: Context.java:2898
static long mkFpaNeg(long a0, long a1)
Definition: Native.java:5963
FPNum mkFPNumeral(double v, FPSort s)
Definition: Context.java:3295
static int getNumProbes(long a0)
Definition: Native.java:4142
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1272
BoolExpr mkFPIsSubnormal(FPExpr t)
Definition: Context.java:3609
static long mkNumeral(long a0, String a1, long a2)
Definition: Native.java:1970
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:5999
static void updateParamValue(long a0, String a1, String a2)
Definition: Native.java:752
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:1115
static long mkConfig()
Definition: Native.java:699
def ReSort(s)
Definition: z3py.py:10014
ReExpr mkConcat(ReExpr... t)
Definition: Context.java:2138
def RealSort(ctx=None)
Definition: z3py.py:2776
FPNum mkFPInf(FPSort s, boolean negative)
Definition: Context.java:3262
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2868
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:3487
FPNum mkFPNumeral(int v, FPSort s)
Definition: Context.java:3306
static long mkFpaIsNegative(long a0, long a1)
Definition: Native.java:6152
StringSymbol mkSymbol(String name)
Definition: Context.java:101
static long mkSeqToRe(long a0, long a1)
Definition: Native.java:2231
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1718
FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Definition: Context.java:3709
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1098
static long mkFpaRne(long a0)
Definition: Native.java:5711
String [] getTacticNames()
Definition: Context.java:2624
Probe eq(Probe p1, Probe p2)
Definition: Context.java:2948
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:1214
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:2873
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:1241
static long tacticFailIf(long a0, long a1)
Definition: Native.java:4016
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1443
static long mkExtRotateLeft(long a0, long a1, long a2)
Definition: Native.java:1682
static long mkSeqReplace(long a0, long a1, long a2, long a3)
Definition: Native.java:2177
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
Definition: Context.java:3554
FPRMNum mkFPRoundTowardNegative()
Definition: Context.java:3130
BoolExpr mkInRe(SeqExpr s, ReExpr re)
Definition: Context.java:2075
FPNum mkFP(float v, FPSort s)
Definition: Context.java:3343
static long mkFpaIsPositive(long a0, long a1)
Definition: Native.java:6161
static long mkFpaSort16(long a0)
Definition: Native.java:5810
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
Definition: Context.java:758
static long mkReStar(long a0, long a1)
Definition: Native.java:2258
static long mkFpaSqrt(long a0, long a1, long a2)
Definition: Native.java:6017
static long mkBvlshr(long a0, long a1, long a2)
Definition: Native.java:1646
ReExpr mkPlus(ReExpr re)
Definition: Context.java:2110
BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2552
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:4027
static String probeGetDescr(long a0, String a1)
Definition: Native.java:4187
static long mkBvuge(long a0, long a1, long a2)
Definition: Native.java:1556
static long mkSolverForLogic(long a0, long a1)
Definition: Native.java:4293
static long mkFpaAdd(long a0, long a1, long a2, long a3)
Definition: Native.java:5972
static long simplifyGetParamDescrs(long a0)
Definition: Native.java:3248
String [] getProbeNames()
Definition: Context.java:2859
BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3589
FPNum mkFPNaN(FPSort s)
Definition: Context.java:3251
static long mkLe(long a0, long a1, long a2)
Definition: Native.java:1304
static long mkSetIntersect(long a0, int a1, long[] a2)
Definition: Native.java:1916
static long mkFpaRem(long a0, long a1, long a2)
Definition: Native.java:6026
static long mkConcat(long a0, long a1, long a2)
Definition: Native.java:1592
static long mkSelect(long a0, long a1, long a2)
Definition: Native.java:1790
static long mkBvnand(long a0, long a1, long a2)
Definition: Native.java:1412
static long mkFpaRoundTowardNegative(long a0)
Definition: Native.java:5756
static long mkFpaToReal(long a0, long a1)
Definition: Native.java:6233
Tactic then(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2687
IDecRefQueue< Statistics > getStatisticsDRQ()
Definition: Context.java:4017
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:2572
static long probeEq(long a0, long a1, long a2)
Definition: Native.java:4088
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:3957
static long mkGe(long a0, long a1, long a2)
Definition: Native.java:1322
static long mkXor(long a0, long a1, long a2)
Definition: Native.java:1196
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2229
static long mkSeqInRe(long a0, long a1, long a2)
Definition: Native.java:2240
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:1529
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:6098
void setPrintMode(Z3_ast_print_mode value)
Definition: Context.java:2515
FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3461
static long mkReUnion(long a0, int a1, long[] a2)
Definition: Native.java:2276
static long mkAdd(long a0, int a1, long[] a2)
Definition: Native.java:1223
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
Definition: Native.java:5936
static long mkReConcat(long a0, int a1, long[] a2)
Definition: Native.java:2285
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:4106
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:2204
static long mkSeqSuffix(long a0, long a1, long a2)
Definition: Native.java:2150
static long mkSeqExtract(long a0, long a1, long a2, long a3)
Definition: Native.java:2168
FPExpr mkFPNeg(FPExpr t)
Definition: Context.java:3413
IntExpr mkReal2Int(RealExpr t)
Definition: Context.java:954
RatNum mkReal(int v)
Definition: Context.java:2306
IDecRefQueue< ASTMap > getASTMapDRQ()
Definition: Context.java:3962
static long probeNot(long a0, long a1)
Definition: Native.java:4115
static long mkSignExt(long a0, int a1, long a2)
Definition: Native.java:1610
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3319
FPRMExpr mkFPRoundNearestTiesToEven()
Definition: Context.java:3076
static long mkBvsmod(long a0, long a1, long a2)
Definition: Native.java:1511
AST wrapAST(long nativeObject)
Definition: Context.java:3844
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1727
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:1934
IDecRefQueue< Tactic > getTacticDRQ()
Definition: Context.java:4022
static long mkInt(long a0, int a1, long a2)
Definition: Native.java:1988
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
Definition: Context.java:453
static long probeConst(long a0, double a1)
Definition: Native.java:4043
static long mkReIntersect(long a0, int a1, long[] a2)
Definition: Native.java:2312
static long mkSetAdd(long a0, long a1, long a2)
Definition: Native.java:1889
static long mkFpaNumeralInt(long a0, int a1, long a2)
Definition: Native.java:5927
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1772
ReExpr mkToRe(SeqExpr s)
Definition: Context.java:2065
static long mkBvneg(long a0, long a1)
Definition: Native.java:1439
static long mkInt64(long a0, long a1, long a2)
Definition: Native.java:2006
FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Definition: Context.java:3761
BoolExpr mkFPIsPositive(FPExpr t)
Definition: Context.java:3659
BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2211
static long mkBvsdiv(long a0, long a1, long a2)
Definition: Native.java:1484
static long mkMap(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1835
FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
Definition: Context.java:3677
static int getNumTactics(long a0)
Definition: Native.java:4124
ArrayExpr mkSetDel(ArrayExpr set, Expr element)
Definition: Context.java:1872
static long mkAtmost(long a0, int a1, long[] a2, int a3)
Definition: Native.java:2636
static long mkZeroExt(long a0, int a1, long a2)
Definition: Native.java:1619
static long mkBvnot(long a0, long a1)
Definition: Native.java:1358
static long mkFpaRna(long a0)
Definition: Native.java:5729
static long mkDistinct(long a0, int a1, long[] a2)
Definition: Native.java:1151
BoolExpr mkIsInteger(RealExpr t)
Definition: Context.java:963
static long mkUnaryMinus(long a0, long a1)
Definition: Native.java:1250
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:1925
static long mkBvsgt(long a0, long a1, long a2)
Definition: Native.java:1583
static long mkSetDel(long a0, long a1, long a2)
Definition: Native.java:1898
static long mkRotateRight(long a0, int a1, long a2)
Definition: Native.java:1673
ReExpr mkComplement(ReExpr re)
Definition: Context.java:2129
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1745
static long mkStore(long a0, long a1, long a2, long a3)
Definition: Native.java:1808
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:3743
Probe gt(Probe p1, Probe p2)
Definition: Context.java:2910
BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3543
static long mkSolverFromTactic(long a0, long a1)
Definition: Native.java:4302
BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1259
static long mkBvadd(long a0, long a1, long a2)
Definition: Native.java:1448
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1561
static void delContext(long a0)
Definition: Native.java:731
BoolExpr mkFPIsInfinite(FPExpr t)
Definition: Context.java:3629
static long mkBvsle(long a0, long a1, long a2)
Definition: Native.java:1547
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:3992
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
Definition: Context.java:3977
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:6835
static long mkFpaGeq(long a0, long a1, long a2)
Definition: Native.java:6080
static long mkFpaGt(long a0, long a1, long a2)
Definition: Native.java:6089
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:6170
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2797
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:3593
BoolExpr mkFPIsNaN(FPExpr t)
Definition: Context.java:3639
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1160
static long mkDiv(long a0, long a1, long a2)
Definition: Native.java:1259
SeqExpr mkAt(SeqExpr s, IntExpr index)
Definition: Context.java:2029
static long mkIte(long a0, long a1, long a2, long a3)
Definition: Native.java:1169
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6224
FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3425
static String tacticGetDescr(long a0, String a1)
Definition: Native.java:4178
static long tacticFailIfNotDecided(long a0)
Definition: Native.java:4025
static long mkSeqConcat(long a0, int a1, long[] a2)
Definition: Native.java:2132
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1311
static long mkSimpleSolver(long a0)
Definition: Native.java:4284
static long mkPbge(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2663
static long mkSetMember(long a0, long a1, long a2)
Definition: Native.java:1943
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:5837
static long mkFpaSort64(long a0)
Definition: Native.java:5846
FPRMNum mkFPRoundNearestTiesToAway()
Definition: Context.java:3094
BoolExpr mkBoolConst(String name)
Definition: Context.java:611
FPNum mkFPZero(FPSort s, boolean negative)
Definition: Context.java:3273
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:3476
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1048
void updateParamValue(String id, String value)
Definition: Context.java:3891
Probe mkProbe(String name)
Definition: Context.java:2881
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:1817
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:3972
static long tacticParOr(long a0, int a1, long[] a2)
Definition: Native.java:3944
static long tacticSkip(long a0)
Definition: Native.java:3998
static long mkString(long a0, String a1)
Definition: Native.java:2087
static long mkBvurem(long a0, long a1, long a2)
Definition: Native.java:1493
Tactic repeat(Tactic t, int max)
Definition: Context.java:2750
static long mkSetSubset(long a0, long a1, long a2)
Definition: Native.java:1952
IDecRefQueue< Optimize > getOptimizeDRQ()
Definition: Context.java:4032
static long mkImplies(long a0, long a1, long a2)
Definition: Native.java:1187
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:3366
Tactic tryFor(Tactic t, int ms)
Definition: Context.java:2711
static long probeGt(long a0, long a1, long a2)
Definition: Native.java:4061
static long mkFpaAbs(long a0, long a1)
Definition: Native.java:5954
BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2193
static long mkFpaIsNan(long a0, long a1)
Definition: Native.java:6143
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:5819
static long mkEq(long a0, long a1, long a2)
Definition: Native.java:1142
static long mkRem(long a0, long a1, long a2)
Definition: Native.java:1277
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8933
Probe not(Probe p)
Definition: Context.java:2981
static long mkExtRotateRight(long a0, long a1, long a2)
Definition: Native.java:1691
static long mkFpaMul(long a0, long a1, long a2, long a3)
Definition: Native.java:5990
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:3379
static long mkAtleast(long a0, int a1, long[] a2, int a3)
Definition: Native.java:2645
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:3967
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:3020
static long mkInt2bv(long a0, int a1, long a2)
Definition: Native.java:1700
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:5783
static long mkBvand(long a0, long a1, long a2)
Definition: Native.java:1385
FuncDecl mkConstDecl(Symbol name, Sort range)
Definition: Context.java:503
static long mkRepeat(long a0, int a1, long a2)
Definition: Native.java:1628
FPRMNum mkFPRoundTowardPositive()
Definition: Context.java:3112
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:1063
static long mkReOption(long a0, long a1)
Definition: Native.java:2267
ReExpr mkUnion(ReExpr... t)
Definition: Context.java:2147
static long mkPattern(long a0, int a1, long[] a2)
Definition: Native.java:2348
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
Definition: Native.java:6035
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:3646
static native void setInternalErrorHandler(long ctx)
static long mkFpaNumeralFloat(long a0, float a1, long a2)
Definition: Native.java:5909
static long mkBvult(long a0, long a1, long a2)
Definition: Native.java:1520
FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3449
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:710
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:2186
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Definition: Context.java:3510
static long mkAnd(long a0, int a1, long[] a2)
Definition: Native.java:1205
Tactic failIf(Probe p)
Definition: Context.java:2777
static long mkSeqUnit(long a0, long a1)
Definition: Native.java:2123
static long mkLt(long a0, long a1, long a2)
Definition: Native.java:1295
static long mkReLoop(long a0, long a1, int a2, int a3)
Definition: Native.java:2303
static long mkContextRc(long a0)
Definition: Native.java:723
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
Definition: Context.java:3498
IDecRefQueue< ConstructorList > getConstructorListDRQ()
Definition: Context.java:3953
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:4012
static long mkFpaRtp(long a0)
Definition: Native.java:5747
FPNum mkFP(double v, FPSort s)
Definition: Context.java:3354
ArrayExpr mkEmptySet(Sort domain)
Definition: Context.java:1840
static long mkFpaRoundTowardPositive(long a0)
Definition: Native.java:5738
static long mkPbeq(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2672
ArraySort mkArraySort(Sort[] domains, Sort range)
Definition: Context.java:231
static long mkFpaIsSubnormal(long a0, long a1)
Definition: Native.java:6116
Expr mkTermArray(ArrayExpr array)
Definition: Context.java:1810
static long mkBvsub(long a0, long a1, long a2)
Definition: Native.java:1457
static long mkFpaToIeeeBv(long a0, long a1)
Definition: Native.java:6395
static long mkConstArray(long a0, long a1, long a2)
Definition: Native.java:1826
EnumSort mkEnumSort(String name, String... enumNames)
Definition: Context.java:290
static long mkSeqSort(long a0, long a1)
Definition: Native.java:2033
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Definition: Context.java:4002
static long mkInt2real(long a0, long a1)
Definition: Native.java:1331
FPExpr mkFPMin(FPExpr t1, FPExpr t2)
Definition: Context.java:3521
BoolExpr mkBool(boolean value)
Definition: Context.java:693
static long mkConst(long a0, long a1, long a2)
Definition: Native.java:1097
static long mkFpaInf(long a0, long a1, boolean a2)
Definition: Native.java:5882
static long mkBvsge(long a0, long a1, long a2)
Definition: Native.java:1565
SeqSort mkSeqSort(Sort s)
Definition: Context.java:249
def ArraySort(d, r)
Definition: z3py.py:4221
static long mkReSort(long a0, long a1)
Definition: Native.java:2051
Probe or(Probe p1, Probe p2)
Definition: Context.java:2970
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
Definition: Native.java:6179
BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
Definition: Context.java:3828
static long mkFpaRoundNearestTiesToAway(long a0)
Definition: Native.java:5720
static long tacticParAndThen(long a0, long a1, long a2)
Definition: Native.java:3953
static String getProbeName(long a0, int a1)
Definition: Native.java:4151
FPExpr mkFPAbs(FPExpr t)
Definition: Context.java:3403
def IntSort(ctx=None)
Definition: z3py.py:2760
FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3437
Tactic with(Tactic t, Params p)
Definition: Context.java:2811
IntExpr mkMod(IntExpr t1, IntExpr t2)
Definition: Context.java:853
BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
Definition: Context.java:3778
Probe ge(Probe p1, Probe p2)
Definition: Context.java:2936
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4690
static long mkBvashr(long a0, long a1, long a2)
Definition: Native.java:1655
static long mkReRange(long a0, long a1, long a2)
Definition: Native.java:2294
static long mkGt(long a0, long a1, long a2)
Definition: Native.java:1313
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:1880
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:2654
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:3949
static long probeLe(long a0, long a1, long a2)
Definition: Native.java:4070
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:6134
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
Definition: Context.java:3532
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:3655
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
Definition: Context.java:366
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1781
static long mkRotateLeft(long a0, int a1, long a2)
Definition: Native.java:1664
static String simplifyGetHelp(long a0)
Definition: Native.java:3239
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
Definition: Native.java:5945
Tactic parAndThen(Tactic t1, Tactic t2)
Definition: Context.java:2830
ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
Definition: Context.java:1795
static long mkFpaMin(long a0, long a1, long a2)
Definition: Native.java:6044
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
Definition: Context.java:1456
static long mkBvredand(long a0, long a1)
Definition: Native.java:1367
static long tacticFail(long a0)
Definition: Native.java:4007
static long mkSeqLength(long a0, long a1)
Definition: Native.java:2195
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:1403
SeqExpr mkConcat(SeqExpr... t)
Definition: Context.java:1983
static long tacticUsingParams(long a0, long a1, long a2)
Definition: Native.java:4034
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1220
Probe constProbe(double val)
Definition: Context.java:2889
static long probeLt(long a0, long a1, long a2)
Definition: Native.java:4052
static long mkFpaIsNormal(long a0, long a1)
Definition: Native.java:6107
static long mkBvudiv(long a0, long a1, long a2)
Definition: Native.java:1475
static long mkFpaNan(long a0, long a1)
Definition: Native.java:5873
static long probeGe(long a0, long a1, long a2)
Definition: Native.java:4079
static long mkBvshl(long a0, long a1, long a2)
Definition: Native.java:1637
static long mkFalse(long a0)
Definition: Native.java:1133
static long mkFpaRtn(long a0)
Definition: Native.java:5765
static long mkBvsrem(long a0, long a1, long a2)
Definition: Native.java:1502
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:3810
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3593
static long mkEmptySet(long a0, long a1)
Definition: Native.java:1871
static long mkFpaRoundNearestTiesToEven(long a0)
Definition: Native.java:5702
Expr mkBound(int index, Sort ty)
Definition: Context.java:537
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1754
RatNum mkReal(long v)
Definition: Context.java:2319
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3284
static String getTacticName(long a0, int a1)
Definition: Native.java:4133
static long mkRePlus(long a0, long a1)
Definition: Native.java:2249
BitVecExpr mkBVConst(Symbol name, int size)
Definition: Context.java:651
static long tacticTryFor(long a0, long a1, int a2)
Definition: Native.java:3962
static long mkArrayDefault(long a0, long a1)
Definition: Native.java:1844
static long mkBvnegNoOverflow(long a0, long a1)
Definition: Native.java:1763
static long mkArrayExt(long a0, long a1, long a2)
Definition: Native.java:1961
static long mkStringSort(long a0)
Definition: Native.java:2069
static long mkBound(long a0, int a1, long a2)
Definition: Native.java:2357
static long mkTrue(long a0)
Definition: Native.java:1124
Tactic mkTactic(String name)
Definition: Context.java:2646
static long mkFpaSort128(long a0)
Definition: Native.java:5864
static long mkMul(long a0, int a1, long[] a2)
Definition: Native.java:1232
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
Definition: Native.java:6188
static long mkSeqEmpty(long a0, long a1)
Definition: Native.java:2114
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3332
static long mkReal(long a0, int a1, int a2)
Definition: Native.java:1979
FPSort mkFPSort(int ebits, int sbits)
Definition: Context.java:3168
static long tacticAndThen(long a0, long a1, long a2)
Definition: Native.java:3926
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:6071
ParamDescrs getSimplifyParameterDescriptions()
Definition: Context.java:3878
IDecRefQueue< Params > getParamsDRQ()
Definition: Context.java:3997
SeqExpr mkEmptySeq(Sort s)
Definition: Context.java:1957
Fixedpoint mkFixedpoint()
Definition: Context.java:3049
BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
Definition: Context.java:2020
static long mkBvxnor(long a0, long a1, long a2)
Definition: Native.java:1430
static long mkSeqPrefix(long a0, long a1, long a2)
Definition: Native.java:2141
static long mkSelectN(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1799
static long mkFpaMax(long a0, long a1, long a2)
Definition: Native.java:6053
static long mkFpaSub(long a0, long a1, long a2, long a3)
Definition: Native.java:5981
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3392
BoolExpr mkFPIsNormal(FPExpr t)
Definition: Context.java:3599
IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Definition: Context.java:2047
static long mkSetUnion(long a0, int a1, long[] a2)
Definition: Native.java:1907
Tactic cond(Probe p, Tactic t1, Tactic t2)
Definition: Context.java:2737
static long mkPower(long a0, long a1, long a2)
Definition: Native.java:1286
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1193
static long mkFpaIsZero(long a0, long a1)
Definition: Native.java:6125
Solver mkSolver(Symbol logic)
Definition: Context.java:3006
def Map(f, args)
Definition: z3py.py:4318
FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
Definition: Context.java:3693
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:1394
BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3565
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:2819
BitVecNum mkBV(int v, int size)
Definition: Context.java:2378
static long mkBv2int(long a0, long a1, boolean a2)
Definition: Native.java:1709
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:3067
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:5774
Tactic orElse(Tactic t1, Tactic t2)
Definition: Context.java:2697
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:2923
ArithExpr mkUnaryMinus(ArithExpr t)
Definition: Context.java:830
static long probeAnd(long a0, long a1, long a2)
Definition: Native.java:4097
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2655
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:1466
static long mkFpaSortQuadruple(long a0)
Definition: Native.java:5855
static long datatypeUpdateField(long a0, long a1, long a2, long a3)
Definition: Native.java:2609
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:5918
BitVecNum mkBV(String v, int size)
Definition: Context.java:2368
Solver mkSolver(Tactic t)
Definition: Context.java:3039
String getTacticDescription(String name)
Definition: Context.java:2638
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:6008
static long mkReal2int(long a0, long a1)
Definition: Native.java:1340
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
Definition: Context.java:492
static long mkFpaSortHalf(long a0)
Definition: Native.java:5801
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6215
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:3971
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:1160
ArrayExpr mkSetIntersection(ArrayExpr... args)
Definition: Context.java:1895
static long mkBvSort(long a0, int a1)
Definition: Native.java:957
FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Definition: Context.java:3725
static long mkFpaSort32(long a0)
Definition: Native.java:5828
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:3576
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:3982
static long mkIsInt(long a0, long a1)
Definition: Native.java:1349
FPRMNum mkFPRoundTowardZero()
Definition: Context.java:3148
static long mkFpaLeq(long a0, long a1, long a2)
Definition: Native.java:6062
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3664
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:6404
static long mkReComplement(long a0, long a1)
Definition: Native.java:2321
def BoolSort(ctx=None)
Definition: z3py.py:1449
static long mkBvsubNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1736
static long mkIff(long a0, long a1, long a2)
Definition: Native.java:1178
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:923
BoolExpr mkFPIsZero(FPExpr t)
Definition: Context.java:3619
def String(name, ctx=None)
Definition: z3py.py:9821
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:3987
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:2599
static long tacticCond(long a0, long a1, long a2, long a3)
Definition: Native.java:3980
static long mkFpaZero(long a0, long a1, boolean a2)
Definition: Native.java:5891
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1547
static long mkBvnor(long a0, long a1, long a2)
Definition: Native.java:1421