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 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 
1984  {
1985  return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
1986  }
1987 
1992  {
1993  return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
1994  }
1995 
1999  public SeqExpr mkConcat(SeqExpr... t)
2000  {
2001  checkContextMatch(t);
2002  return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
2003  }
2004 
2005 
2010  {
2011  checkContextMatch(s);
2012  return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
2013  }
2014 
2019  {
2020  checkContextMatch(s1, s2);
2021  return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2022  }
2023 
2028  {
2029  checkContextMatch(s1, s2);
2030  return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2031  }
2032 
2037  {
2038  checkContextMatch(s1, s2);
2039  return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2040  }
2041 
2045  public SeqExpr mkAt(SeqExpr s, IntExpr index)
2046  {
2047  checkContextMatch(s, index);
2048  return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
2049  }
2050 
2054  public SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
2055  {
2056  checkContextMatch(s, offset, length);
2057  return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
2058  }
2059 
2063  public IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
2064  {
2065  checkContextMatch(s, substr, offset);
2066  return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
2067  }
2068 
2073  {
2074  checkContextMatch(s, src, dst);
2075  return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
2076  }
2077 
2081  public ReExpr mkToRe(SeqExpr s)
2082  {
2083  checkContextMatch(s);
2084  return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
2085  }
2086 
2087 
2092  {
2093  checkContextMatch(s, re);
2094  return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
2095  }
2096 
2100  public ReExpr mkStar(ReExpr re)
2101  {
2102  checkContextMatch(re);
2103  return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
2104  }
2105 
2109  public ReExpr mkLoop(ReExpr re, int lo, int hi)
2110  {
2111  return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
2112  }
2113 
2117  public ReExpr mkLoop(ReExpr re, int lo)
2118  {
2119  return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
2120  }
2121 
2122 
2126  public ReExpr mkPlus(ReExpr re)
2127  {
2128  checkContextMatch(re);
2129  return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
2130  }
2131 
2136  {
2137  checkContextMatch(re);
2138  return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
2139  }
2140 
2141 
2146  {
2147  checkContextMatch(re);
2148  return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
2149  }
2150 
2154  public ReExpr mkConcat(ReExpr... t)
2155  {
2156  checkContextMatch(t);
2157  return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2158  }
2159 
2163  public ReExpr mkUnion(ReExpr... t)
2164  {
2165  checkContextMatch(t);
2166  return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2167  }
2168 
2173  {
2174  checkContextMatch(t);
2175  return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
2176  }
2177 
2181  public ReExpr mkEmptyRe(Sort s)
2182  {
2183  return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
2184  }
2185 
2189  public ReExpr mkFullRe(Sort s)
2190  {
2191  return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
2192  }
2193 
2197  public ReExpr mkRange(SeqExpr lo, SeqExpr hi)
2198  {
2199  checkContextMatch(lo, hi);
2200  return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
2201  }
2202 
2203 
2207  public BoolExpr mkAtMost(BoolExpr[] args, int k)
2208  {
2209  checkContextMatch(args);
2210  return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
2211  }
2212 
2216  public BoolExpr mkAtLeast(BoolExpr[] args, int k)
2217  {
2218  checkContextMatch(args);
2219  return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
2220  }
2221 
2225  public BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
2226  {
2227  checkContextMatch(args);
2228  return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2229  }
2230 
2234  public BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
2235  {
2236  checkContextMatch(args);
2237  return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2238  }
2239 
2243  public BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
2244  {
2245  checkContextMatch(args);
2246  return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2247  }
2248 
2249 
2261  public Expr mkNumeral(String v, Sort ty)
2262  {
2263  checkContextMatch(ty);
2264  return Expr.create(this,
2265  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
2266  }
2267 
2278  public Expr mkNumeral(int v, Sort ty)
2279  {
2280  checkContextMatch(ty);
2281  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
2282  }
2283 
2294  public Expr mkNumeral(long v, Sort ty)
2295  {
2296  checkContextMatch(ty);
2297  return Expr.create(this,
2298  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
2299  }
2300 
2310  public RatNum mkReal(int num, int den)
2311  {
2312  if (den == 0) {
2313  throw new Z3Exception("Denominator is zero");
2314  }
2315 
2316  return new RatNum(this, Native.mkReal(nCtx(), num, den));
2317  }
2318 
2326  {
2327 
2328  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2329  .getNativeObject()));
2330  }
2331 
2338  public RatNum mkReal(int v)
2339  {
2340 
2341  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2342  .getNativeObject()));
2343  }
2344 
2351  public RatNum mkReal(long v)
2352  {
2353 
2354  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2355  .getNativeObject()));
2356  }
2357 
2362  public IntNum mkInt(String v)
2363  {
2364 
2365  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2366  .getNativeObject()));
2367  }
2368 
2375  public IntNum mkInt(int v)
2376  {
2377 
2378  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2379  .getNativeObject()));
2380  }
2381 
2388  public IntNum mkInt(long v)
2389  {
2390 
2391  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2392  .getNativeObject()));
2393  }
2394 
2400  public BitVecNum mkBV(String v, int size)
2401  {
2402  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2403  }
2404 
2410  public BitVecNum mkBV(int v, int size)
2411  {
2412  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2413  }
2414 
2420  public BitVecNum mkBV(long v, int size)
2421  {
2422  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2423  }
2424 
2450  public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
2451  int weight, Pattern[] patterns, Expr[] noPatterns,
2452  Symbol quantifierID, Symbol skolemID)
2453  {
2454 
2455  return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2456  noPatterns, quantifierID, skolemID);
2457  }
2458 
2463  public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
2464  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2465  Symbol skolemID)
2466  {
2467 
2468  return Quantifier.of(this, true, boundConstants, body, weight,
2469  patterns, noPatterns, quantifierID, skolemID);
2470  }
2471 
2476  public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
2477  int weight, Pattern[] patterns, Expr[] noPatterns,
2478  Symbol quantifierID, Symbol skolemID)
2479  {
2480 
2481  return Quantifier.of(this, false, sorts, names, body, weight,
2482  patterns, noPatterns, quantifierID, skolemID);
2483  }
2484 
2489  public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
2490  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2491  Symbol skolemID)
2492  {
2493 
2494  return Quantifier.of(this, false, boundConstants, body, weight,
2495  patterns, noPatterns, quantifierID, skolemID);
2496  }
2497 
2502  public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
2503  Symbol[] names, Expr body, int weight, Pattern[] patterns,
2504  Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
2505 
2506  {
2507 
2508  if (universal)
2509  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2510  quantifierID, skolemID);
2511  else
2512  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2513  quantifierID, skolemID);
2514  }
2515 
2520  public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
2521  Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
2522  Symbol quantifierID, Symbol skolemID)
2523  {
2524 
2525  if (universal)
2526  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2527  quantifierID, skolemID);
2528  else
2529  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2530  quantifierID, skolemID);
2531  }
2532 
2550  public Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body)
2551  {
2552  return Lambda.of(this, sorts, names, body);
2553  }
2554 
2561  public Lambda mkLambda(Expr[] boundConstants, Expr body)
2562  {
2563  return Lambda.of(this, boundConstants, body);
2564  }
2565 
2566 
2581  public void setPrintMode(Z3_ast_print_mode value)
2582  {
2583  Native.setAstPrintMode(nCtx(), value.toInt());
2584  }
2585 
2600  String status, String attributes, BoolExpr[] assumptions,
2601  BoolExpr formula)
2602  {
2603 
2604  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2605  attributes, assumptions.length,
2606  AST.arrayToNative(assumptions), formula.getNativeObject());
2607  }
2608 
2618  public BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames,
2619  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2620 
2621  {
2622  int csn = Symbol.arrayLength(sortNames);
2623  int cs = Sort.arrayLength(sorts);
2624  int cdn = Symbol.arrayLength(declNames);
2625  int cd = AST.arrayLength(decls);
2626  if (csn != cs || cdn != cd) {
2627  throw new Z3Exception("Argument size mismatch");
2628  }
2629  ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
2630  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2631  AST.arrayToNative(sorts), AST.arrayLength(decls),
2632  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2633  return v.ToBoolExprArray();
2634  }
2635 
2640  public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames,
2641  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2642 
2643  {
2644  int csn = Symbol.arrayLength(sortNames);
2645  int cs = Sort.arrayLength(sorts);
2646  int cdn = Symbol.arrayLength(declNames);
2647  int cd = AST.arrayLength(decls);
2648  if (csn != cs || cdn != cd)
2649  throw new Z3Exception("Argument size mismatch");
2650  ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
2651  fileName, AST.arrayLength(sorts),
2652  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2653  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2654  AST.arrayToNative(decls)));
2655  return v.ToBoolExprArray();
2656  }
2657 
2668  public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
2669 
2670  {
2671  return new Goal(this, models, unsatCores, proofs);
2672  }
2673 
2677  public Params mkParams()
2678  {
2679  return new Params(this);
2680  }
2681 
2685  public int getNumTactics()
2686  {
2687  return Native.getNumTactics(nCtx());
2688  }
2689 
2694  {
2695 
2696  int n = getNumTactics();
2697  String[] res = new String[n];
2698  for (int i = 0; i < n; i++)
2699  res[i] = Native.getTacticName(nCtx(), i);
2700  return res;
2701  }
2702 
2708  {
2709  return Native.tacticGetDescr(nCtx(), name);
2710  }
2711 
2715  public Tactic mkTactic(String name)
2716  {
2717  return new Tactic(this, name);
2718  }
2719 
2724  public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
2725 
2726  {
2727  checkContextMatch(t1);
2728  checkContextMatch(t2);
2729  checkContextMatch(ts);
2730 
2731  long last = 0;
2732  if (ts != null && ts.length > 0)
2733  {
2734  last = ts[ts.length - 1].getNativeObject();
2735  for (int i = ts.length - 2; i >= 0; i--) {
2736  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2737  last);
2738  }
2739  }
2740  if (last != 0)
2741  {
2742  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2743  return new Tactic(this, Native.tacticAndThen(nCtx(),
2744  t1.getNativeObject(), last));
2745  } else
2746  return new Tactic(this, Native.tacticAndThen(nCtx(),
2747  t1.getNativeObject(), t2.getNativeObject()));
2748  }
2749 
2756  public Tactic then(Tactic t1, Tactic t2, Tactic... ts)
2757  {
2758  return andThen(t1, t2, ts);
2759  }
2760 
2766  public Tactic orElse(Tactic t1, Tactic t2)
2767  {
2768  checkContextMatch(t1);
2769  checkContextMatch(t2);
2770  return new Tactic(this, Native.tacticOrElse(nCtx(),
2771  t1.getNativeObject(), t2.getNativeObject()));
2772  }
2773 
2780  public Tactic tryFor(Tactic t, int ms)
2781  {
2782  checkContextMatch(t);
2783  return new Tactic(this, Native.tacticTryFor(nCtx(),
2784  t.getNativeObject(), ms));
2785  }
2786 
2793  public Tactic when(Probe p, Tactic t)
2794  {
2795  checkContextMatch(t);
2796  checkContextMatch(p);
2797  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2798  t.getNativeObject()));
2799  }
2800 
2806  public Tactic cond(Probe p, Tactic t1, Tactic t2)
2807  {
2808  checkContextMatch(p);
2809  checkContextMatch(t1);
2810  checkContextMatch(t2);
2811  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2812  t1.getNativeObject(), t2.getNativeObject()));
2813  }
2814 
2819  public Tactic repeat(Tactic t, int max)
2820  {
2821  checkContextMatch(t);
2822  return new Tactic(this, Native.tacticRepeat(nCtx(),
2823  t.getNativeObject(), max));
2824  }
2825 
2829  public Tactic skip()
2830  {
2831  return new Tactic(this, Native.tacticSkip(nCtx()));
2832  }
2833 
2837  public Tactic fail()
2838  {
2839  return new Tactic(this, Native.tacticFail(nCtx()));
2840  }
2841 
2846  public Tactic failIf(Probe p)
2847  {
2848  checkContextMatch(p);
2849  return new Tactic(this,
2850  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2851  }
2852 
2858  {
2859  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2860  }
2861 
2867  {
2868  checkContextMatch(t);
2869  checkContextMatch(p);
2870  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2871  t.getNativeObject(), p.getNativeObject()));
2872  }
2873 
2880  public Tactic with(Tactic t, Params p)
2881  {
2882  return usingParams(t, p);
2883  }
2884 
2888  public Tactic parOr(Tactic... t)
2889  {
2890  checkContextMatch(t);
2891  return new Tactic(this, Native.tacticParOr(nCtx(),
2892  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2893  }
2894 
2900  {
2901  checkContextMatch(t1);
2902  checkContextMatch(t2);
2903  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2904  t1.getNativeObject(), t2.getNativeObject()));
2905  }
2906 
2912  public void interrupt()
2913  {
2914  Native.interrupt(nCtx());
2915  }
2916 
2920  public int getNumProbes()
2921  {
2922  return Native.getNumProbes(nCtx());
2923  }
2924 
2929  {
2930 
2931  int n = getNumProbes();
2932  String[] res = new String[n];
2933  for (int i = 0; i < n; i++)
2934  res[i] = Native.getProbeName(nCtx(), i);
2935  return res;
2936  }
2937 
2943  {
2944  return Native.probeGetDescr(nCtx(), name);
2945  }
2946 
2950  public Probe mkProbe(String name)
2951  {
2952  return new Probe(this, name);
2953  }
2954 
2958  public Probe constProbe(double val)
2959  {
2960  return new Probe(this, Native.probeConst(nCtx(), val));
2961  }
2962 
2967  public Probe lt(Probe p1, Probe p2)
2968  {
2969  checkContextMatch(p1);
2970  checkContextMatch(p2);
2971  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2972  p2.getNativeObject()));
2973  }
2974 
2979  public Probe gt(Probe p1, Probe p2)
2980  {
2981  checkContextMatch(p1);
2982  checkContextMatch(p2);
2983  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2984  p2.getNativeObject()));
2985  }
2986 
2992  public Probe le(Probe p1, Probe p2)
2993  {
2994  checkContextMatch(p1);
2995  checkContextMatch(p2);
2996  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2997  p2.getNativeObject()));
2998  }
2999 
3005  public Probe ge(Probe p1, Probe p2)
3006  {
3007  checkContextMatch(p1);
3008  checkContextMatch(p2);
3009  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
3010  p2.getNativeObject()));
3011  }
3012 
3017  public Probe eq(Probe p1, Probe p2)
3018  {
3019  checkContextMatch(p1);
3020  checkContextMatch(p2);
3021  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
3022  p2.getNativeObject()));
3023  }
3024 
3028  public Probe and(Probe p1, Probe p2)
3029  {
3030  checkContextMatch(p1);
3031  checkContextMatch(p2);
3032  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
3033  p2.getNativeObject()));
3034  }
3035 
3039  public Probe or(Probe p1, Probe p2)
3040  {
3041  checkContextMatch(p1);
3042  checkContextMatch(p2);
3043  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
3044  p2.getNativeObject()));
3045  }
3046 
3050  public Probe not(Probe p)
3051  {
3052  checkContextMatch(p);
3053  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
3054  }
3055 
3063  public Solver mkSolver()
3064  {
3065  return mkSolver((Symbol) null);
3066  }
3067 
3075  public Solver mkSolver(Symbol logic)
3076  {
3077 
3078  if (logic == null)
3079  return new Solver(this, Native.mkSolver(nCtx()));
3080  else
3081  return new Solver(this, Native.mkSolverForLogic(nCtx(),
3082  logic.getNativeObject()));
3083  }
3084 
3089  public Solver mkSolver(String logic)
3090  {
3091  return mkSolver(mkSymbol(logic));
3092  }
3093 
3098  {
3099  return new Solver(this, Native.mkSimpleSolver(nCtx()));
3100  }
3101 
3109  {
3110 
3111  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3112  t.getNativeObject()));
3113  }
3114 
3119  {
3120  return new Fixedpoint(this);
3121  }
3122 
3127  {
3128  return new Optimize(this);
3129  }
3130 
3131 
3137  {
3138  return new FPRMSort(this);
3139  }
3140 
3146  {
3147  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3148  }
3149 
3154  public FPRMNum mkFPRNE()
3155  {
3156  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3157  }
3158 
3164  {
3165  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3166  }
3167 
3172  public FPRMNum mkFPRNA()
3173  {
3174  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3175  }
3176 
3182  {
3183  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3184  }
3185 
3190  public FPRMNum mkFPRTP()
3191  {
3192  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3193  }
3194 
3200  {
3201  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3202  }
3203 
3208  public FPRMNum mkFPRTN()
3209  {
3210  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3211  }
3212 
3218  {
3219  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3220  }
3221 
3226  public FPRMNum mkFPRTZ()
3227  {
3228  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3229  }
3230 
3237  public FPSort mkFPSort(int ebits, int sbits)
3238  {
3239  return new FPSort(this, ebits, sbits);
3240  }
3241 
3247  {
3248  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3249  }
3250 
3256  {
3257  return new FPSort(this, Native.mkFpaSort16(nCtx()));
3258  }
3259 
3265  {
3266  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3267  }
3268 
3274  {
3275  return new FPSort(this, Native.mkFpaSort32(nCtx()));
3276  }
3277 
3283  {
3284  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3285  }
3286 
3292  {
3293  return new FPSort(this, Native.mkFpaSort64(nCtx()));
3294  }
3295 
3301  {
3302  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3303  }
3304 
3310  {
3311  return new FPSort(this, Native.mkFpaSort128(nCtx()));
3312  }
3313 
3314 
3321  {
3322  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3323  }
3324 
3331  public FPNum mkFPInf(FPSort s, boolean negative)
3332  {
3333  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3334  }
3335 
3342  public FPNum mkFPZero(FPSort s, boolean negative)
3343  {
3344  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3345  }
3346 
3353  public FPNum mkFPNumeral(float v, FPSort s)
3354  {
3355  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3356  }
3357 
3364  public FPNum mkFPNumeral(double v, FPSort s)
3365  {
3366  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3367  }
3368 
3375  public FPNum mkFPNumeral(int v, FPSort s)
3376  {
3377  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3378  }
3379 
3388  public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
3389  {
3390  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3391  }
3392 
3401  public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
3402  {
3403  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3404  }
3405 
3412  public FPNum mkFP(float v, FPSort s)
3413  {
3414  return mkFPNumeral(v, s);
3415  }
3416 
3423  public FPNum mkFP(double v, FPSort s)
3424  {
3425  return mkFPNumeral(v, s);
3426  }
3427 
3435  public FPNum mkFP(int v, FPSort s)
3436  {
3437  return mkFPNumeral(v, s);
3438  }
3439 
3448  public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
3449  {
3450  return mkFPNumeral(sgn, exp, sig, s);
3451  }
3452 
3461  public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
3462  {
3463  return mkFPNumeral(sgn, exp, sig, s);
3464  }
3465 
3466 
3472  public FPExpr mkFPAbs(FPExpr t)
3473  {
3474  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3475  }
3476 
3482  public FPExpr mkFPNeg(FPExpr t)
3483  {
3484  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3485  }
3486 
3494  public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
3495  {
3496  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3497  }
3498 
3506  public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
3507  {
3508  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3509  }
3510 
3518  public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
3519  {
3520  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3521  }
3522 
3530  public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
3531  {
3532  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3533  }
3534 
3545  public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
3546  {
3547  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3548  }
3549 
3557  {
3558  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3559  }
3560 
3567  public FPExpr mkFPRem(FPExpr t1, FPExpr t2)
3568  {
3569  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3570  }
3571 
3580  {
3581  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3582  }
3583 
3590  public FPExpr mkFPMin(FPExpr t1, FPExpr t2)
3591  {
3592  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3593  }
3594 
3601  public FPExpr mkFPMax(FPExpr t1, FPExpr t2)
3602  {
3603  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3604  }
3605 
3612  public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
3613  {
3614  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3615  }
3616 
3623  public BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
3624  {
3625  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3626  }
3627 
3634  public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
3635  {
3636  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3637  }
3638 
3645  public BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
3646  {
3647  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3648  }
3649 
3658  public BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
3659  {
3660  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3661  }
3662 
3669  {
3670  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3671  }
3672 
3679  {
3680  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3681  }
3682 
3689  {
3690  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3691  }
3692 
3699  {
3700  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3701  }
3702 
3709  {
3710  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3711  }
3712 
3719  {
3720  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3721  }
3722 
3729  {
3730  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3731  }
3732 
3747  {
3748  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3749  }
3750 
3763  {
3764  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3765  }
3766 
3779  {
3780  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3781  }
3782 
3795  {
3796  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3797  }
3798 
3812  public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
3813  {
3814  if (signed)
3815  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3816  else
3817  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3818  }
3819 
3831  {
3832  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3833  }
3834 
3847  public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
3848  {
3849  if (signed)
3850  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3851  else
3852  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3853  }
3854 
3865  {
3866  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3867  }
3868 
3880  {
3881  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3882  }
3883 
3898  {
3899  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3900  }
3901 
3902 
3913  public AST wrapAST(long nativeObject)
3914  {
3915  return AST.create(this, nativeObject);
3916  }
3917 
3930  public long unwrapAST(AST a)
3931  {
3932  return a.getNativeObject();
3933  }
3934 
3940  {
3941  return Native.simplifyGetHelp(nCtx());
3942  }
3943 
3948  {
3949  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3950  }
3951 
3960  public void updateParamValue(String id, String value)
3961  {
3962  Native.updateParamValue(nCtx(), id, value);
3963  }
3964 
3965 
3966  long nCtx()
3967  {
3968  if (m_ctx == 0)
3969  throw new Z3Exception("Context closed");
3970  return m_ctx;
3971  }
3972 
3973 
3974  void checkContextMatch(Z3Object other)
3975  {
3976  if (this != other.getContext())
3977  throw new Z3Exception("Context mismatch");
3978  }
3979 
3980  void checkContextMatch(Z3Object other1, Z3Object other2)
3981  {
3982  checkContextMatch(other1);
3983  checkContextMatch(other2);
3984  }
3985 
3986  void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
3987  {
3988  checkContextMatch(other1);
3989  checkContextMatch(other2);
3990  checkContextMatch(other3);
3991  }
3992 
3993  void checkContextMatch(Z3Object[] arr)
3994  {
3995  if (arr != null)
3996  for (Z3Object a : arr)
3997  checkContextMatch(a);
3998  }
3999 
4000  private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
4001  private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
4002  private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
4003  private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
4004  private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
4005  private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
4006  private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
4007  private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
4008  private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
4009  private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
4010  private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
4011  private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
4012  private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
4013  private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
4014  private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
4015  private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
4016  private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
4017  private ConstructorListDecRefQueue m_ConstructorList_DRQ =
4018  new ConstructorListDecRefQueue();
4019 
4021  return m_Constructor_DRQ;
4022  }
4023 
4025  return m_ConstructorList_DRQ;
4026  }
4027 
4029  {
4030  return m_AST_DRQ;
4031  }
4032 
4034  {
4035  return m_ASTMap_DRQ;
4036  }
4037 
4039  {
4040  return m_ASTVector_DRQ;
4041  }
4042 
4044  {
4045  return m_ApplyResult_DRQ;
4046  }
4047 
4049  {
4050  return m_FuncEntry_DRQ;
4051  }
4052 
4054  {
4055  return m_FuncInterp_DRQ;
4056  }
4057 
4059  {
4060  return m_Goal_DRQ;
4061  }
4062 
4064  {
4065  return m_Model_DRQ;
4066  }
4067 
4069  {
4070  return m_Params_DRQ;
4071  }
4072 
4074  {
4075  return m_ParamDescrs_DRQ;
4076  }
4077 
4079  {
4080  return m_Probe_DRQ;
4081  }
4082 
4084  {
4085  return m_Solver_DRQ;
4086  }
4087 
4089  {
4090  return m_Statistics_DRQ;
4091  }
4092 
4094  {
4095  return m_Tactic_DRQ;
4096  }
4097 
4099  {
4100  return m_Fixedpoint_DRQ;
4101  }
4102 
4104  {
4105  return m_Optimize_DRQ;
4106  }
4107 
4111  @Override
4112  public void close()
4113  {
4114  m_AST_DRQ.forceClear(this);
4115  m_ASTMap_DRQ.forceClear(this);
4116  m_ASTVector_DRQ.forceClear(this);
4117  m_ApplyResult_DRQ.forceClear(this);
4118  m_FuncEntry_DRQ.forceClear(this);
4119  m_FuncInterp_DRQ.forceClear(this);
4120  m_Goal_DRQ.forceClear(this);
4121  m_Model_DRQ.forceClear(this);
4122  m_Params_DRQ.forceClear(this);
4123  m_Probe_DRQ.forceClear(this);
4124  m_Solver_DRQ.forceClear(this);
4125  m_Optimize_DRQ.forceClear(this);
4126  m_Statistics_DRQ.forceClear(this);
4127  m_Tactic_DRQ.forceClear(this);
4128  m_Fixedpoint_DRQ.forceClear(this);
4129 
4130  m_boolSort = null;
4131  m_intSort = null;
4132  m_realSort = null;
4133  m_stringSort = null;
4134 
4135  synchronized (creation_lock) {
4136  Native.delContext(m_ctx);
4137  }
4138  m_ctx = 0;
4139  }
4140 }
BoolExpr mkFPIsNegative(FPExpr t)
Definition: Context.java:3718
static long mkFpaFp(long a0, long a1, long a2, long a3)
Definition: Native.java:6119
IntExpr mkIntConst(Symbol name)
Definition: Context.java:619
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6416
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1629
static long tacticRepeat(long a0, long a1, int a2)
Definition: Native.java:4217
BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
Definition: Context.java:2027
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
Definition: Context.java:735
IDecRefQueue< Probe > getProbeDRQ()
Definition: Context.java:4078
static long mkBvule(long a0, long a1, long a2)
Definition: Native.java:1586
static long mkSolver(long a0)
Definition: Native.java:4494
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6425
Tactic when(Probe p, Tactic t)
Definition: Context.java:2793
RatNum mkReal(String v)
Definition: Context.java:2325
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1074
static long mkExtract(long a0, int a1, int a2, long a3)
Definition: Native.java:1649
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
Definition: Context.java:377
static void interrupt(long a0)
Definition: Native.java:782
Pattern mkPattern(Expr... terms)
Definition: Context.java:546
def SeqSort(s)
Definition: z3py.py:9980
Probe and(Probe p1, Probe p2)
Definition: Context.java:3028
static long mkMod(long a0, long a1, long a2)
Definition: Native.java:1307
def Map(f, *args)
Definition: z3py.py:4479
static long mkBvugt(long a0, long a1, long a2)
Definition: Native.java:1622
static long mkSeqContains(long a0, long a1, long a2)
Definition: Native.java:2252
Expr mkSelect(ArrayExpr a, Expr[] args)
Definition: Context.java:1706
static void delConfig(long a0)
Definition: Native.java:727
ArrayExpr mkConstArray(Sort domain, Expr v)
Definition: Context.java:1774
def TupleSort(name, sorts, ctx=None)
Definition: z3py.py:4971
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:1424
RealExpr mkFPToReal(FPExpr t)
Definition: Context.java:3864
static long tacticOrElse(long a0, long a1, long a2)
Definition: Native.java:4163
Probe lt(Probe p1, Probe p2)
Definition: Context.java:2967
static long mkFpaNeg(long a0, long a1)
Definition: Native.java:6182
FPNum mkFPNumeral(double v, FPSort s)
Definition: Context.java:3364
static int getNumProbes(long a0)
Definition: Native.java:4370
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1272
BoolExpr mkFPIsSubnormal(FPExpr t)
Definition: Context.java:3678
static long mkNumeral(long a0, String a1, long a2)
Definition: Native.java:2027
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:6218
static void updateParamValue(long a0, String a1, String a2)
Definition: Native.java:774
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:1137
static long mkConfig()
Definition: Native.java:721
def ReSort(s)
Definition: z3py.py:10294
ReExpr mkConcat(ReExpr... t)
Definition: Context.java:2154
def RealSort(ctx=None)
Definition: z3py.py:2923
FPNum mkFPInf(FPSort s, boolean negative)
Definition: Context.java:3331
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
Expr mkNumeral(int v, Sort ty)
Definition: Context.java:2278
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:3556
FPNum mkFPNumeral(int v, FPSort s)
Definition: Context.java:3375
static long mkFpaIsNegative(long a0, long a1)
Definition: Native.java:6371
StringSymbol mkSymbol(String name)
Definition: Context.java:101
static long mkSeqToRe(long a0, long a1)
Definition: Native.java:2360
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1766
FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Definition: Context.java:3778
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1098
static long mkFpaRne(long a0)
Definition: Native.java:5930
String [] getTacticNames()
Definition: Context.java:2693
Probe eq(Probe p1, Probe p2)
Definition: Context.java:3017
BitVecExpr mkZeroExt(int i, BitVecExpr t)
Definition: Context.java:1374
ReExpr mkLoop(ReExpr re, int lo)
Definition: Context.java:2117
SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
Definition: Context.java:2072
static long mkReEmpty(long a0, long a1)
Definition: Native.java:2459
static long mkOr(long a0, int a1, long[] a2)
Definition: Native.java:1253
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:2489
BoolExpr mkDistinct(Expr... args)
Definition: Context.java:712
String getProbeDescription(String name)
Definition: Context.java:2942
IntNum mkInt(String v)
Definition: Context.java:2362
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:1280
static long tacticFailIf(long a0, long a1)
Definition: Native.java:4244
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1443
static long mkExtRotateLeft(long a0, long a1, long a2)
Definition: Native.java:1730
static long mkSeqReplace(long a0, long a1, long a2, long a3)
Definition: Native.java:2288
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
Definition: Context.java:3623
FPRMNum mkFPRoundTowardNegative()
Definition: Context.java:3199
BoolExpr mkInRe(SeqExpr s, ReExpr re)
Definition: Context.java:2091
SeqExpr intToString(Expr e)
Definition: Context.java:1983
FPNum mkFP(float v, FPSort s)
Definition: Context.java:3412
static long mkFpaIsPositive(long a0, long a1)
Definition: Native.java:6380
static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
Definition: Lambda.java:94
static long mkFpaSort16(long a0)
Definition: Native.java:6029
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
Definition: Context.java:758
static long mkReStar(long a0, long a1)
Definition: Native.java:2387
static long mkFpaSqrt(long a0, long a1, long a2)
Definition: Native.java:6236
static long mkBvlshr(long a0, long a1, long a2)
Definition: Native.java:1694
ReExpr mkPlus(ReExpr re)
Definition: Context.java:2126
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:4098
static String probeGetDescr(long a0, String a1)
Definition: Native.java:4415
static long mkBvuge(long a0, long a1, long a2)
Definition: Native.java:1604
static long mkSolverForLogic(long a0, long a1)
Definition: Native.java:4512
static long mkFpaAdd(long a0, long a1, long a2, long a3)
Definition: Native.java:6191
static long simplifyGetParamDescrs(long a0)
Definition: Native.java:3467
String [] getProbeNames()
Definition: Context.java:2928
BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3658
FPNum mkFPNaN(FPSort s)
Definition: Context.java:3320
static long mkLe(long a0, long a1, long a2)
Definition: Native.java:1343
static long mkSetIntersect(long a0, int a1, long[] a2)
Definition: Native.java:1973
static long mkFpaRem(long a0, long a1, long a2)
Definition: Native.java:6245
static long mkStrToInt(long a0, long a1)
Definition: Native.java:2342
static long mkConcat(long a0, long a1, long a2)
Definition: Native.java:1640
static long mkSelect(long a0, long a1, long a2)
Definition: Native.java:1838
static long mkBvnand(long a0, long a1, long a2)
Definition: Native.java:1460
static long mkFpaRoundTowardNegative(long a0)
Definition: Native.java:5975
static long mkFpaToReal(long a0, long a1)
Definition: Native.java:6452
Tactic then(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2756
IDecRefQueue< Statistics > getStatisticsDRQ()
Definition: Context.java:4088
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1496
static long probeEq(long a0, long a1, long a2)
Definition: Native.java:4316
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:4028
static long mkGe(long a0, long a1, long a2)
Definition: Native.java:1361
static long mkXor(long a0, long a1, long a2)
Definition: Native.java:1235
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2261
static long mkSeqInRe(long a0, long a1, long a2)
Definition: Native.java:2369
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:1577
BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
Definition: Context.java:2018
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:6317
void setPrintMode(Z3_ast_print_mode value)
Definition: Context.java:2581
FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3530
static long mkReUnion(long a0, int a1, long[] a2)
Definition: Native.java:2405
static long mkAdd(long a0, int a1, long[] a2)
Definition: Native.java:1262
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
Definition: Native.java:6155
static long mkReConcat(long a0, int a1, long[] a2)
Definition: Native.java:2414
FuncDecl mkConstDecl(String name, Sort range)
Definition: Context.java:513
ReExpr mkIntersect(ReExpr... t)
Definition: Context.java:2172
static long probeOr(long a0, long a1, long a2)
Definition: Native.java:4334
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:2324
static long mkSeqSuffix(long a0, long a1, long a2)
Definition: Native.java:2243
static long mkSeqExtract(long a0, long a1, long a2, long a3)
Definition: Native.java:2279
FPExpr mkFPNeg(FPExpr t)
Definition: Context.java:3482
IntExpr mkReal2Int(RealExpr t)
Definition: Context.java:954
RatNum mkReal(int v)
Definition: Context.java:2338
IDecRefQueue< ASTMap > getASTMapDRQ()
Definition: Context.java:4033
static long probeNot(long a0, long a1)
Definition: Native.java:4343
static long mkSignExt(long a0, int a1, long a2)
Definition: Native.java:1658
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3388
FPRMExpr mkFPRoundNearestTiesToEven()
Definition: Context.java:3145
static long mkBvsmod(long a0, long a1, long a2)
Definition: Native.java:1559
AST wrapAST(long nativeObject)
Definition: Context.java:3913
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1775
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:1991
IDecRefQueue< Tactic > getTacticDRQ()
Definition: Context.java:4093
static long mkInt(long a0, int a1, long a2)
Definition: Native.java:2045
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
Definition: Context.java:453
static long probeConst(long a0, double a1)
Definition: Native.java:4271
static long mkReIntersect(long a0, int a1, long[] a2)
Definition: Native.java:2441
static long mkSetAdd(long a0, long a1, long a2)
Definition: Native.java:1946
static long mkFpaNumeralInt(long a0, int a1, long a2)
Definition: Native.java:6146
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1820
ReExpr mkToRe(SeqExpr s)
Definition: Context.java:2081
static long mkBvneg(long a0, long a1)
Definition: Native.java:1487
static long mkInt64(long a0, long a1, long a2)
Definition: Native.java:2063
FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Definition: Context.java:3830
BoolExpr mkFPIsPositive(FPExpr t)
Definition: Context.java:3728
BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2243
static long mkBvsdiv(long a0, long a1, long a2)
Definition: Native.java:1532
static long mkMap(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1883
FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
Definition: Context.java:3746
static int getNumTactics(long a0)
Definition: Native.java:4352
ArrayExpr mkSetDel(ArrayExpr set, Expr element)
Definition: Context.java:1872
static long mkAtmost(long a0, int a1, long[] a2, int a3)
Definition: Native.java:2828
static long mkZeroExt(long a0, int a1, long a2)
Definition: Native.java:1667
static long mkBvnot(long a0, long a1)
Definition: Native.java:1406
static long mkFpaRna(long a0)
Definition: Native.java:5948
static long mkDistinct(long a0, int a1, long[] a2)
Definition: Native.java:1190
BoolExpr mkIsInteger(RealExpr t)
Definition: Context.java:963
static long mkUnaryMinus(long a0, long a1)
Definition: Native.java:1289
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:1982
static long mkBvsgt(long a0, long a1, long a2)
Definition: Native.java:1631
static long mkSetDel(long a0, long a1, long a2)
Definition: Native.java:1955
static long mkRotateRight(long a0, int a1, long a2)
Definition: Native.java:1721
ReExpr mkComplement(ReExpr re)
Definition: Context.java:2145
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1793
static long mkStore(long a0, long a1, long a2, long a3)
Definition: Native.java:1856
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2502
BoolExpr [] ToBoolExprArray()
Definition: ASTVector.java:140
FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
Definition: Context.java:3812
Probe gt(Probe p1, Probe p2)
Definition: Context.java:2979
BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3612
static long mkSolverFromTactic(long a0, long a1)
Definition: Native.java:4521
BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1259
static long mkBvadd(long a0, long a1, long a2)
Definition: Native.java:1496
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1561
static void delContext(long a0)
Definition: Native.java:753
BoolExpr mkFPIsInfinite(FPExpr t)
Definition: Context.java:3698
static long mkBvsle(long a0, long a1, long a2)
Definition: Native.java:1595
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:4063
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
Definition: Context.java:4048
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:7221
static long mkFpaGeq(long a0, long a1, long a2)
Definition: Native.java:6299
static long mkFpaGt(long a0, long a1, long a2)
Definition: Native.java:6308
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:6389
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2866
BitVecExpr mkBVConst(String name, int size)
Definition: Context.java:659
BoolExpr [] parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2640
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:901
static void setAstPrintMode(long a0, int a1)
Definition: Native.java:3812
BoolExpr mkFPIsNaN(FPExpr t)
Definition: Context.java:3708
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1160
static long mkDiv(long a0, long a1, long a2)
Definition: Native.java:1298
SeqExpr mkAt(SeqExpr s, IntExpr index)
Definition: Context.java:2045
static long mkReFull(long a0, long a1)
Definition: Native.java:2468
static long mkIte(long a0, long a1, long a2, long a3)
Definition: Native.java:1208
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6443
FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3494
static String tacticGetDescr(long a0, String a1)
Definition: Native.java:4406
static long tacticFailIfNotDecided(long a0)
Definition: Native.java:4253
static long mkSeqConcat(long a0, int a1, long[] a2)
Definition: Native.java:2225
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1311
static long mkSimpleSolver(long a0)
Definition: Native.java:4503
static long mkPbge(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2855
static long mkSetMember(long a0, long a1, long a2)
Definition: Native.java:2000
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2463
static long mkFpaSortDouble(long a0)
Definition: Native.java:6056
static long mkFpaSort64(long a0)
Definition: Native.java:6065
FPRMNum mkFPRoundNearestTiesToAway()
Definition: Context.java:3163
BoolExpr mkBoolConst(String name)
Definition: Context.java:611
Lambda mkLambda(Expr[] boundConstants, Expr body)
Definition: Context.java:2561
FPNum mkFPZero(FPSort s, boolean negative)
Definition: Context.java:3342
BoolExpr mkAtLeast(BoolExpr[] args, int k)
Definition: Context.java:2216
BitVecExpr mkRepeat(int i, BitVecExpr t)
Definition: Context.java:1386
FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Definition: Context.java:3545
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1048
void updateParamValue(String id, String value)
Definition: Context.java:3960
Probe mkProbe(String name)
Definition: Context.java:2950
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:1865
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:4043
static long tacticParOr(long a0, int a1, long[] a2)
Definition: Native.java:4172
static long tacticSkip(long a0)
Definition: Native.java:4226
static long mkString(long a0, String a1)
Definition: Native.java:2162
static long mkBvurem(long a0, long a1, long a2)
Definition: Native.java:1541
Tactic repeat(Tactic t, int max)
Definition: Context.java:2819
static long mkSetSubset(long a0, long a1, long a2)
Definition: Native.java:2009
IDecRefQueue< Optimize > getOptimizeDRQ()
Definition: Context.java:4103
static long mkImplies(long a0, long a1, long a2)
Definition: Native.java:1226
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
Definition: Context.java:2599
DatatypeSort [] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:389
FPNum mkFP(int v, FPSort s)
Definition: Context.java:3435
Tactic tryFor(Tactic t, int ms)
Definition: Context.java:2780
static long probeGt(long a0, long a1, long a2)
Definition: Native.java:4289
static long mkFpaAbs(long a0, long a1)
Definition: Native.java:6173
BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2225
static long mkFpaIsNan(long a0, long a1)
Definition: Native.java:6362
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
Definition: Context.java:747
def SetSort(s)
Sets.
Definition: z3py.py:4568
ReExpr mkEmptyRe(Sort s)
Definition: Context.java:2181
IntExpr mkIntConst(String name)
Definition: Context.java:627
BoolExpr mkOr(BoolExpr... t)
Definition: Context.java:790
static long mkIntToStr(long a0, long a1)
Definition: Native.java:2351
static long mkFpaSortSingle(long a0)
Definition: Native.java:6038
static long mkEq(long a0, long a1, long a2)
Definition: Native.java:1181
static long mkRem(long a0, long a1, long a2)
Definition: Native.java:1316
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9183
Probe not(Probe p)
Definition: Context.java:3050
static long mkExtRotateRight(long a0, long a1, long a2)
Definition: Native.java:1739
static long mkFpaMul(long a0, long a1, long a2, long a3)
Definition: Native.java:6209
ReExpr mkRange(SeqExpr lo, SeqExpr hi)
Definition: Context.java:2197
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1246
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3448
static long mkAtleast(long a0, int a1, long[] a2, int a3)
Definition: Native.java:2837
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:4038
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
Definition: Context.java:441
IntExpr mkLength(SeqExpr s)
Definition: Context.java:2009
IntNum mkInt(long v)
Definition: Context.java:2388
Solver mkSolver(String logic)
Definition: Context.java:3089
static long mkInt2bv(long a0, int a1, long a2)
Definition: Native.java:1748
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:6002
static long mkBvand(long a0, long a1, long a2)
Definition: Native.java:1433
FuncDecl mkConstDecl(Symbol name, Sort range)
Definition: Context.java:503
static long mkRepeat(long a0, int a1, long a2)
Definition: Native.java:1676
FPRMNum mkFPRoundTowardPositive()
Definition: Context.java:3181
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1589
ReExpr mkFullRe(Sort s)
Definition: Context.java:2189
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
Definition: Native.java:1085
static long mkReOption(long a0, long a1)
Definition: Native.java:2396
ReExpr mkUnion(ReExpr... t)
Definition: Context.java:2163
static long mkPattern(long a0, int a1, long[] a2)
Definition: Native.java:2522
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
Definition: Native.java:6254
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:3865
static native void setInternalErrorHandler(long ctx)
static long mkFpaNumeralFloat(long a0, float a1, long a2)
Definition: Native.java:6128
static long mkBvult(long a0, long a1, long a2)
Definition: Native.java:1568
FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3518
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:732
SeqExpr mkString(String s)
Definition: Context.java:1975
ReExpr mkStar(ReExpr re)
Definition: Context.java:2100
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:2297
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Definition: Context.java:3579
static long mkAnd(long a0, int a1, long[] a2)
Definition: Native.java:1244
Tactic failIf(Probe p)
Definition: Context.java:2846
static long mkSeqUnit(long a0, long a1)
Definition: Native.java:2216
Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body)
Definition: Context.java:2550
static long mkLt(long a0, long a1, long a2)
Definition: Native.java:1334
static long mkReLoop(long a0, long a1, int a2, int a3)
Definition: Native.java:2432
static long mkContextRc(long a0)
Definition: Native.java:745
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
Definition: Context.java:3567
IDecRefQueue< ConstructorList > getConstructorListDRQ()
Definition: Context.java:4024
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:4083
static long mkFpaRtp(long a0)
Definition: Native.java:5966
FPNum mkFP(double v, FPSort s)
Definition: Context.java:3423
ArrayExpr mkEmptySet(Sort domain)
Definition: Context.java:1840
static long mkFpaRoundTowardPositive(long a0)
Definition: Native.java:5957
static long mkPbeq(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2864
ArraySort mkArraySort(Sort[] domains, Sort range)
Definition: Context.java:231
static long mkFpaIsSubnormal(long a0, long a1)
Definition: Native.java:6335
Expr mkTermArray(ArrayExpr array)
Definition: Context.java:1810
static long mkBvsub(long a0, long a1, long a2)
Definition: Native.java:1505
static long mkFpaToIeeeBv(long a0, long a1)
Definition: Native.java:6614
static long mkConstArray(long a0, long a1, long a2)
Definition: Native.java:1874
EnumSort mkEnumSort(String name, String... enumNames)
Definition: Context.java:290
static long mkSeqSort(long a0, long a1)
Definition: Native.java:2090
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Definition: Context.java:4073
static long mkInt2real(long a0, long a1)
Definition: Native.java:1379
FPExpr mkFPMin(FPExpr t1, FPExpr t2)
Definition: Context.java:3590
BoolExpr mkBool(boolean value)
Definition: Context.java:693
static long mkConst(long a0, long a1, long a2)
Definition: Native.java:1119
static long mkFpaInf(long a0, long a1, boolean a2)
Definition: Native.java:6101
static long mkBvsge(long a0, long a1, long a2)
Definition: Native.java:1613
SeqSort mkSeqSort(Sort s)
Definition: Context.java:249
static long mkReSort(long a0, long a1)
Definition: Native.java:2117
Probe or(Probe p1, Probe p2)
Definition: Context.java:3039
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
Definition: Native.java:6398
BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
Definition: Context.java:3897
static long mkFpaRoundNearestTiesToAway(long a0)
Definition: Native.java:5939
static long tacticParAndThen(long a0, long a1, long a2)
Definition: Native.java:4181
static String getProbeName(long a0, int a1)
Definition: Native.java:4379
FPExpr mkFPAbs(FPExpr t)
Definition: Context.java:3472
def IntSort(ctx=None)
Definition: z3py.py:2907
FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3506
Tactic with(Tactic t, Params p)
Definition: Context.java:2880
IntExpr mkMod(IntExpr t1, IntExpr t2)
Definition: Context.java:853
BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
Definition: Context.java:3847
Probe ge(Probe p1, Probe p2)
Definition: Context.java:3005
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4994
static long mkBvashr(long a0, long a1, long a2)
Definition: Native.java:1703
static long mkReRange(long a0, long a1, long a2)
Definition: Native.java:2423
static long mkGt(long a0, long a1, long a2)
Definition: Native.java:1352
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:1937
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
Definition: Context.java:318
ReExpr mkLoop(ReExpr re, int lo, int hi)
Definition: Context.java:2109
static long mkPble(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2846
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:4020
static long probeLe(long a0, long a1, long a2)
Definition: Native.java:4298
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:6353
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
Definition: Context.java:3601
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:2476
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:3874
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
Definition: Context.java:366
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1829
static long mkRotateLeft(long a0, int a1, long a2)
Definition: Native.java:1712
static String simplifyGetHelp(long a0)
Definition: Native.java:3458
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
Definition: Native.java:6164
Tactic parAndThen(Tactic t1, Tactic t2)
Definition: Context.java:2899
ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
Definition: Context.java:1795
static long mkFpaMin(long a0, long a1, long a2)
Definition: Native.java:6263
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
Definition: Context.java:1456
static long mkBvredand(long a0, long a1)
Definition: Native.java:1415
static long tacticFail(long a0)
Definition: Native.java:4235
static long mkSeqLength(long a0, long a1)
Definition: Native.java:2315
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:1451
SeqExpr mkConcat(SeqExpr... t)
Definition: Context.java:1999
static long tacticUsingParams(long a0, long a1, long a2)
Definition: Native.java:4262
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1220
Probe constProbe(double val)
Definition: Context.java:2958
static long probeLt(long a0, long a1, long a2)
Definition: Native.java:4280
static long mkFpaIsNormal(long a0, long a1)
Definition: Native.java:6326
static long mkBvudiv(long a0, long a1, long a2)
Definition: Native.java:1523
static long mkFpaNan(long a0, long a1)
Definition: Native.java:6092
static long probeGe(long a0, long a1, long a2)
Definition: Native.java:4307
static long mkBvshl(long a0, long a1, long a2)
Definition: Native.java:1685
IntExpr stringToInt(Expr e)
Definition: Context.java:1991
static long mkFalse(long a0)
Definition: Native.java:1172
static long mkFpaRtn(long a0)
Definition: Native.java:5984
static long mkBvsrem(long a0, long a1, long a2)
Definition: Native.java:1550
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:3879
def ArraySort(*sig)
Definition: z3py.py:4371
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3740
static long mkEmptySet(long a0, long a1)
Definition: Native.java:1928
static long mkFpaRoundNearestTiesToEven(long a0)
Definition: Native.java:5921
Expr mkBound(int index, Sort ty)
Definition: Context.java:537
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1802
RatNum mkReal(long v)
Definition: Context.java:2351
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3353
static String getTacticName(long a0, int a1)
Definition: Native.java:4361
static long mkRePlus(long a0, long a1)
Definition: Native.java:2378
BitVecExpr mkBVConst(Symbol name, int size)
Definition: Context.java:651
static long tacticTryFor(long a0, long a1, int a2)
Definition: Native.java:4190
static long mkArrayDefault(long a0, long a1)
Definition: Native.java:1892
static long mkBvnegNoOverflow(long a0, long a1)
Definition: Native.java:1811
static long mkArrayExt(long a0, long a1, long a2)
Definition: Native.java:2018
static long mkStringSort(long a0)
Definition: Native.java:2144
static long mkBound(long a0, int a1, long a2)
Definition: Native.java:2531
static long mkTrue(long a0)
Definition: Native.java:1163
Tactic mkTactic(String name)
Definition: Context.java:2715
static long mkFpaSort128(long a0)
Definition: Native.java:6083
static long mkMul(long a0, int a1, long[] a2)
Definition: Native.java:1271
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
Definition: Native.java:6407
static long mkSeqEmpty(long a0, long a1)
Definition: Native.java:2207
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3401
static long mkReal(long a0, int a1, int a2)
Definition: Native.java:2036
FPSort mkFPSort(int ebits, int sbits)
Definition: Context.java:3237
static long tacticAndThen(long a0, long a1, long a2)
Definition: Native.java:4154
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
Definition: Context.java:1731
SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
Definition: Context.java:2054
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212
static long mkFpaLt(long a0, long a1, long a2)
Definition: Native.java:6290
ParamDescrs getSimplifyParameterDescriptions()
Definition: Context.java:3947
IDecRefQueue< Params > getParamsDRQ()
Definition: Context.java:4068
SeqExpr mkEmptySeq(Sort s)
Definition: Context.java:1957
Fixedpoint mkFixedpoint()
Definition: Context.java:3118
BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
Definition: Context.java:2036
static long mkBvxnor(long a0, long a1, long a2)
Definition: Native.java:1478
static long mkSeqPrefix(long a0, long a1, long a2)
Definition: Native.java:2234
static long mkSelectN(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1847
static long mkFpaMax(long a0, long a1, long a2)
Definition: Native.java:6272
static long mkFpaSub(long a0, long a1, long a2, long a3)
Definition: Native.java:6200
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3461
BoolExpr mkFPIsNormal(FPExpr t)
Definition: Context.java:3668
IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Definition: Context.java:2063
static long mkSetUnion(long a0, int a1, long[] a2)
Definition: Native.java:1964
Tactic cond(Probe p, Tactic t1, Tactic t2)
Definition: Context.java:2806
static long mkPower(long a0, long a1, long a2)
Definition: Native.java:1325
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1193
static long mkFpaIsZero(long a0, long a1)
Definition: Native.java:6344
Solver mkSolver(Symbol logic)
Definition: Context.java:3075
FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
Definition: Context.java:3762
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:1442
BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3634
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:2888
BitVecNum mkBV(int v, int size)
Definition: Context.java:2410
static long mkBv2int(long a0, long a1, boolean a2)
Definition: Native.java:1757
expr max(expr const &a, expr const &b)
Definition: z3++.h:1591
BoolExpr mkNot(BoolExpr a)
Definition: Context.java:722
BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2234
Expr mkNumeral(long v, Sort ty)
Definition: Context.java:2294
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:3136
ReExpr mkOption(ReExpr re)
Definition: Context.java:2135
ListSort mkListSort(Symbol name, Sort elemSort)
Definition: Context.java:299
static long mkFpaRoundTowardZero(long a0)
Definition: Native.java:5993
Tactic orElse(Tactic t1, Tactic t2)
Definition: Context.java:2766
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:2992
ArithExpr mkUnaryMinus(ArithExpr t)
Definition: Context.java:830
static long probeAnd(long a0, long a1, long a2)
Definition: Native.java:4325
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2724
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:1514
static long mkFpaSortQuadruple(long a0)
Definition: Native.java:6074
static long datatypeUpdateField(long a0, long a1, long a2, long a3)
Definition: Native.java:2801
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:2520
static long mkFpaNumeralDouble(long a0, double a1, long a2)
Definition: Native.java:6137
BitVecNum mkBV(String v, int size)
Definition: Context.java:2400
Solver mkSolver(Tactic t)
Definition: Context.java:3108
String getTacticDescription(String name)
Definition: Context.java:2707
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:6227
static long mkReal2int(long a0, long a1)
Definition: Native.java:1388
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
Definition: Context.java:492
static long mkFpaSortHalf(long a0)
Definition: Native.java:6020
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6434
BitVecNum mkBV(long v, int size)
Definition: Context.java:2420
BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1111
static long tacticWhen(long a0, long a1, long a2)
Definition: Native.java:4199
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:1199
ArrayExpr mkSetIntersection(ArrayExpr... args)
Definition: Context.java:1895
static long mkBvSort(long a0, int a1)
Definition: Native.java:979
FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Definition: Context.java:3794
static long mkFpaSort32(long a0)
Definition: Native.java:6047
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1329
RatNum mkReal(int num, int den)
Definition: Context.java:2310
BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
Definition: Context.java:3645
BitVecExpr mkSignExt(int i, BitVecExpr t)
Definition: Context.java:1360
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1298
BoolExpr [] parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2618
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:4053
static long mkIsInt(long a0, long a1)
Definition: Native.java:1397
FPRMNum mkFPRoundTowardZero()
Definition: Context.java:3217
static long mkFpaLeq(long a0, long a1, long a2)
Definition: Native.java:6281
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3883
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:6623
static long mkReComplement(long a0, long a1)
Definition: Native.java:2450
def BoolSort(ctx=None)
Definition: z3py.py:1533
static long mkBvsubNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1784
static long mkIff(long a0, long a1, long a2)
Definition: Native.java:1217
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:923
BoolExpr mkFPIsZero(FPExpr t)
Definition: Context.java:3688
def String(name, ctx=None)
Definition: z3py.py:10085
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:4058
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2450
ArithExpr mkSub(ArithExpr... t)
Definition: Context.java:820
BoolExpr mkAtMost(BoolExpr[] args, int k)
Definition: Context.java:2207
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
Definition: Context.java:2668
static long tacticCond(long a0, long a1, long a2, long a3)
Definition: Native.java:4208
static long mkFpaZero(long a0, long a1, boolean a2)
Definition: Native.java:6110
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1547
static long mkBvnor(long a0, long a1, long a2)
Definition: Native.java:1469