Z3
Context.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import static com.microsoft.z3.Constructor.of;
21
22import com.microsoft.z3.enumerations.Z3_ast_print_mode;
23
24import java.util.Map;
25
35public 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
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
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
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
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
620 {
621 return (IntExpr) mkConst(name, getIntSort());
622 }
623
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
678 {
679 return new BoolExpr(this, Native.mkTrue(nCtx()));
680 }
681
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
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
801 {
802 checkContextMatch(t);
803 return (ArithExpr) Expr.create(this,
804 Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
805 }
806
811 {
812 checkContextMatch(t);
813 return (ArithExpr) Expr.create(this,
814 Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
815 }
816
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
854 {
855 checkContextMatch(t1);
856 checkContextMatch(t2);
857 return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
858 t2.getNativeObject()));
859 }
860
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
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
1656
1657 {
1658 return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1659 }
1660
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
1775 {
1776 checkContextMatch(domain);
1777 checkContextMatch(v);
1778 return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1779 domain.getNativeObject(), v.getNativeObject()));
1780 }
1781
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
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
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
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
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
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
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
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
2182 {
2183 return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
2184 }
2185
2190 {
2191 return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
2192 }
2193
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
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
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
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
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
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
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
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
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
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
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
3155 {
3156 return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3157 }
3158
3164 {
3165 return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3166 }
3167
3173 {
3174 return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3175 }
3176
3182 {
3183 return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3184 }
3185
3191 {
3192 return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3193 }
3194
3200 {
3201 return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3202 }
3203
3209 {
3210 return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3211 }
3212
3218 {
3219 return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3220 }
3221
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
3473 {
3474 return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3475 }
3476
3483 {
3484 return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3485 }
3486
3495 {
3496 return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3497 }
3498
3507 {
3508 return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3509 }
3510
3519 {
3520 return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3521 }
3522
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
3591 {
3592 return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3593 }
3594
3602 {
3603 return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3604 }
3605
3613 {
3614 return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3615 }
3616
3624 {
3625 return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3626 }
3627
3635 {
3636 return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3637 }
3638
3646 {
3647 return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3648 }
3649
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[] ToBoolExprArray()
Definition: ASTVector.java:140
BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
Definition: Context.java:2018
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
Definition: Context.java:453
Expr mkConst(String name, Sort range)
Definition: Context.java:575
Probe ge(Probe p1, Probe p2)
Definition: Context.java:3005
FuncDecl mkConstDecl(String name, Sort range)
Definition: Context.java:513
RealExpr mkInt2Real(IntExpr t)
Definition: Context.java:941
BoolExpr mkEq(Expr x, Expr y)
Definition: Context.java:701
Solver mkSolver(String logic)
Definition: Context.java:3089
BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3612
Tactic repeat(Tactic t, int max)
Definition: Context.java:2819
Pattern mkPattern(Expr... terms)
Definition: Context.java:546
ArraySort mkArraySort(Sort[] domains, Sort range)
Definition: Context.java:231
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:389
FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
Definition: Context.java:3812
String getProbeDescription(String name)
Definition: Context.java:2942
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3461
BoolExpr mkBVNegNoOverflow(BitVecExpr t)
Definition: Context.java:1617
FPNum mkFPNaN(FPSort s)
Definition: Context.java:3320
FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
Definition: Context.java:3746
FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t)
Definition: Context.java:3556
BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2618
FPRMExpr mkFPRoundNearestTiesToEven()
Definition: Context.java:3145
Expr mkTermArray(ArrayExpr array)
Definition: Context.java:1810
BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
Definition: Context.java:3897
Fixedpoint mkFixedpoint()
Definition: Context.java:3118
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2866
Tactic parOr(Tactic... t)
Definition: Context.java:2888
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1220
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
Definition: Context.java:377
FiniteDomainSort mkFiniteDomainSort(String name, long size)
Definition: Context.java:328
FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Definition: Context.java:3545
Tactic then(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2756
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:923
BoolExpr mkFPIsSubnormal(FPExpr t)
Definition: Context.java:3678
FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3518
FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Definition: Context.java:3778
FPSort mkFPSort(int ebits, int sbits)
Definition: Context.java:3237
Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
Definition: Context.java:345
BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1481
ArrayExpr mkSetIntersection(ArrayExpr... args)
Definition: Context.java:1895
Probe le(Probe p1, Probe p2)
Definition: Context.java:2992
FPExpr mkFPAbs(FPExpr t)
Definition: Context.java:3472
SetSort mkSetSort(Sort ty)
Definition: Context.java:1831
Expr mkSelect(ArrayExpr a, Expr[] args)
Definition: Context.java:1706
RealExpr mkFPToReal(FPExpr t)
Definition: Context.java:3864
Expr mkConst(FuncDecl f)
Definition: Context.java:595
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1496
BitVecExpr mkZeroExt(int i, BitVecExpr t)
Definition: Context.java:1374
AST wrapAST(long nativeObject)
Definition: Context.java:3913
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:179
SeqExpr mkString(String s)
Definition: Context.java:1975
IDecRefQueue< FuncInterp > getFuncInterpDRQ()
Definition: Context.java:4053
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1048
ArithExpr mkMul(ArithExpr... t)
Definition: Context.java:810
ArithExpr mkSub(ArithExpr... t)
Definition: Context.java:820
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3388
BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
Definition: Context.java:1468
FPNum mkFP(double v, FPSort s)
Definition: Context.java:3423
SeqExpr mkEmptySeq(Sort s)
Definition: Context.java:1957
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
Definition: Context.java:735
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1139
BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1111
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
Definition: Context.java:747
SeqExpr mkUnit(Expr elem)
Definition: Context.java:1966
BoolExpr mkFPIsZero(FPExpr t)
Definition: Context.java:3688
FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3530
BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
Definition: Context.java:769
BoolExpr mkNot(BoolExpr a)
Definition: Context.java:722
FPNum mkFPInf(FPSort s, boolean negative)
Definition: Context.java:3331
ArithExpr mkUnaryMinus(ArithExpr t)
Definition: Context.java:830
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
Definition: Context.java:4048
Expr mkNumeral(int v, Sort ty)
Definition: Context.java:2278
Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1820
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1298
BitVecExpr mkBVConst(Symbol name, int size)
Definition: Context.java:651
FPRMNum mkFPRoundTowardZero()
Definition: Context.java:3217
ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
Definition: Context.java:1860
Probe or(Probe p1, Probe p2)
Definition: Context.java:3039
IDecRefQueue< ASTMap > getASTMapDRQ()
Definition: Context.java:4033
Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2489
Tactic cond(Probe p, Tactic t1, Tactic t2)
Definition: Context.java:2806
IDecRefQueue< Statistics > getStatisticsDRQ()
Definition: Context.java:4088
ReExpr mkStar(ReExpr re)
Definition: Context.java:2100
IDecRefQueue< Model > getModelDRQ()
Definition: Context.java:4063
BitVecExpr mkBVConst(String name, int size)
Definition: Context.java:659
SeqExpr mkConcat(SeqExpr... t)
Definition: Context.java:1999
IDecRefQueue< Optimize > getOptimizeDRQ()
Definition: Context.java:4103
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:890
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1547
IntNum mkInt(long v)
Definition: Context.java:2388
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
Definition: Context.java:1535
Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body)
Definition: Context.java:2550
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:4028
EnumSort mkEnumSort(String name, String... enumNames)
Definition: Context.java:290
FPNum mkFPNumeral(int v, FPSort s)
Definition: Context.java:3375
ReExpr mkComplement(ReExpr re)
Definition: Context.java:2145
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
Definition: Context.java:2599
BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2234
FuncDecl mkFreshConstDecl(String prefix, Sort range)
Definition: Context.java:525
IntExpr mkReal2Int(RealExpr t)
Definition: Context.java:954
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:4043
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3448
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1589
void updateParamValue(String id, String value)
Definition: Context.java:3960
IntExpr stringToInt(Expr e)
Definition: Context.java:1991
ReExpr mkLoop(ReExpr re, int lo, int hi)
Definition: Context.java:2109
BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1603
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:220
Tactic failIf(Probe p)
Definition: Context.java:2846
BitVecNum mkBV(long v, int size)
Definition: Context.java:2420
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3353
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Definition: Context.java:4073
BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1404
BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1175
Tactic when(Probe p, Tactic t)
Definition: Context.java:2793
ArrayExpr mkSetDel(ArrayExpr set, Expr element)
Definition: Context.java:1872
BitVecExpr mkRepeat(int i, BitVecExpr t)
Definition: Context.java:1386
BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
Definition: Context.java:1928
IntNum mkInt(String v)
Definition: Context.java:2362
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:4058
Probe mkProbe(String name)
Definition: Context.java:2950
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
Definition: Context.java:318
RealExpr mkRealConst(String name)
Definition: Context.java:643
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
Definition: Context.java:492
ReExpr mkToRe(SeqExpr s)
Definition: Context.java:2081
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1285
SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
Definition: Context.java:2072
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 mkBVSLE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1259
ParamDescrs getSimplifyParameterDescriptions()
Definition: Context.java:3947
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1098
Probe gt(Probe p1, Probe p2)
Definition: Context.java:2979
SeqExpr intToString(Expr e)
Definition: Context.java:1983
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2261
ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
Definition: Context.java:840
Tactic with(Tactic t, Params p)
Definition: Context.java:2880
ReExpr mkRange(SeqExpr lo, SeqExpr hi)
Definition: Context.java:2197
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:912
BoolExpr mkFPIsNormal(FPExpr t)
Definition: Context.java:3668
FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
Definition: Context.java:477
Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2520
ReExpr mkLoop(ReExpr re, int lo)
Definition: Context.java:2117
SeqExpr mkAt(SeqExpr s, IntExpr index)
Definition: Context.java:2045
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
Definition: Context.java:3567
FPRMNum mkFPRoundNearestTiesToAway()
Definition: Context.java:3163
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1561
BoolExpr mkBool(boolean value)
Definition: Context.java:693
BoolExpr mkAnd(BoolExpr... t)
Definition: Context.java:780
IntExpr mkMod(IntExpr t1, IntExpr t2)
Definition: Context.java:853
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Definition: Context.java:266
FPExpr mkFPMin(FPExpr t1, FPExpr t2)
Definition: Context.java:3590
BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1643
BoolExpr mkFPIsInfinite(FPExpr t)
Definition: Context.java:3698
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
Definition: Context.java:1731
ReExpr mkOption(ReExpr re)
Definition: Context.java:2135
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1160
FPRMNum mkFPRoundTowardNegative()
Definition: Context.java:3199
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1629
BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
Definition: Context.java:3645
IDecRefQueue< Params > getParamsDRQ()
Definition: Context.java:4068
Probe eq(Probe p1, Probe p2)
Definition: Context.java:3017
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
Definition: Context.java:3623
ArrayExpr mkSetUnion(ArrayExpr... args)
Definition: Context.java:1884
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:4083
BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
Definition: Context.java:2027
BoolExpr mkAtMost(BoolExpr[] args, int k)
Definition: Context.java:2207
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1193
ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
Definition: Context.java:877
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
Definition: Context.java:3601
BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1009
EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
Definition: Context.java:279
BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1575
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2463
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
Definition: Context.java:441
IntExpr mkIntConst(String name)
Definition: Context.java:627
Solver mkSolver(Tactic t)
Definition: Context.java:3108
Expr mkUpdateField(FuncDecl field, Expr t, Expr v)
Definition: Context.java:428
BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2243
Expr mkBound(int index, Sort ty)
Definition: Context.java:537
IDecRefQueue< Constructor > getConstructorDRQ()
Definition: Context.java:4020
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2724
ArrayExpr mkFullSet(Sort domain)
Definition: Context.java:1850
ReSort mkReSort(Sort s)
Definition: Context.java:257
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
Definition: Context.java:1456
IntExpr mkIntConst(Symbol name)
Definition: Context.java:619
Expr mkNumeral(long v, Sort ty)
Definition: Context.java:2294
BoolExpr mkFPIsNaN(FPExpr t)
Definition: Context.java:3708
Tactic mkTactic(String name)
Definition: Context.java:2715
BitVecExpr mkBVNot(BitVecExpr t)
Definition: Context.java:974
ReExpr mkFullRe(Sort s)
Definition: Context.java:2189
FPNum mkFPNumeral(double v, FPSort s)
Definition: Context.java:3364
Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
Definition: Context.java:356
FuncDecl mkConstDecl(Symbol name, Sort range)
Definition: Context.java:503
BoolExpr mkIsInteger(RealExpr t)
Definition: Context.java:963
FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
Definition: Context.java:466
BitVecExpr mkInt2BV(int n, IntExpr t)
Definition: Context.java:1514
ReExpr mkPlus(ReExpr re)
Definition: Context.java:2126
Tactic parAndThen(Tactic t1, Tactic t2)
Definition: Context.java:2899
RatNum mkReal(long v)
Definition: Context.java:2351
BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1124
BitVecNum mkBV(int v, int size)
Definition: Context.java:2410
Context(Map< String, String > settings)
Definition: Context.java:71
FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
Definition: Context.java:3762
ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1906
FPRMSort mkFPRoundingModeSort()
Definition: Context.java:3136
RealExpr mkRealConst(Symbol name)
Definition: Context.java:635
String getTacticDescription(String name)
Definition: Context.java:2707
IDecRefQueue< Probe > getProbeDRQ()
Definition: Context.java:4078
Solver mkSolver(Symbol logic)
Definition: Context.java:3075
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Definition: Context.java:3579
RatNum mkReal(int num, int den)
Definition: Context.java:2310
BitVecSort mkBitVecSort(int size)
Definition: Context.java:212
BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2640
SeqSort mkSeqSort(Sort s)
Definition: Context.java:249
IntExpr mkLength(SeqExpr s)
Definition: Context.java:2009
ArrayExpr mkSetComplement(ArrayExpr arg)
Definition: Context.java:1918
Probe constProbe(double val)
Definition: Context.java:2958
BoolExpr mkAtLeast(BoolExpr[] args, int k)
Definition: Context.java:2216
BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
Definition: Context.java:3847
BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
Definition: Context.java:2225
BoolExpr mkBoolConst(String name)
Definition: Context.java:611
BoolExpr mkDistinct(Expr... args)
Definition: Context.java:712
Probe not(Probe p)
Definition: Context.java:3050
ArrayExpr mkEmptySet(Sort domain)
Definition: Context.java:1840
BoolExpr mkFPIsPositive(FPExpr t)
Definition: Context.java:3728
BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1233
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1272
BitVecExpr mkExtract(int high, int low, BitVecExpr t)
Definition: Context.java:1345
BitVecExpr mkBVNeg(BitVecExpr t)
Definition: Context.java:1087
IDecRefQueue< Tactic > getTacticDRQ()
Definition: Context.java:4093
BoolExpr mkOr(BoolExpr... t)
Definition: Context.java:790
FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3494
BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1207
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3401
Lambda mkLambda(Expr[] boundConstants, Expr body)
Definition: Context.java:2561
RatNum mkReal(int v)
Definition: Context.java:2338
FPRMNum mkFPRoundTowardPositive()
Definition: Context.java:3181
FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Definition: Context.java:3830
DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
Definition: Context.java:416
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1074
ListSort mkListSort(Symbol name, Sort elemSort)
Definition: Context.java:299
BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3634
BitVecExpr mkSignExt(int i, BitVecExpr t)
Definition: Context.java:1360
ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
Definition: Context.java:1756
BoolExpr mkFPIsNegative(FPExpr t)
Definition: Context.java:3718
ListSort mkListSort(String name, Sort elemSort)
Definition: Context.java:309
BitVecExpr mkBVRedAND(BitVecExpr t)
Definition: Context.java:985
Probe and(Probe p1, Probe p2)
Definition: Context.java:3028
BitVecExpr mkFPToIEEEBV(FPExpr t)
Definition: Context.java:3879
Tactic tryFor(Tactic t, int ms)
Definition: Context.java:2780
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
Definition: Context.java:758
UninterpretedSort mkUninterpretedSort(String str)
Definition: Context.java:188
void setPrintMode(Z3_ast_print_mode value)
Definition: Context.java:2581
Expr mkSelect(ArrayExpr a, Expr i)
Definition: Context.java:1683
BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3658
ArithExpr mkAdd(ArithExpr... t)
Definition: Context.java:800
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1329
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2476
BitVecNum mkBV(String v, int size)
Definition: Context.java:2400
Probe lt(Probe p1, Probe p2)
Definition: Context.java:2967
BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1940
BitVecExpr mkBVRedOR(BitVecExpr t)
Definition: Context.java:997
ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
Definition: Context.java:1664
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
Definition: Context.java:2668
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1311
ReExpr mkIntersect(ReExpr... t)
Definition: Context.java:2172
BoolExpr mkInRe(SeqExpr s, ReExpr re)
Definition: Context.java:2091
IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Definition: Context.java:2063
FPNum mkFP(float v, FPSort s)
Definition: Context.java:3412
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:560
FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Definition: Context.java:3794
IntExpr mkRem(IntExpr t1, IntExpr t2)
Definition: Context.java:866
ReExpr mkConcat(ReExpr... t)
Definition: Context.java:2154
FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3506
ReExpr mkEmptyRe(Sort s)
Definition: Context.java:2181
FPExpr mkFPNeg(FPExpr t)
Definition: Context.java:3482
BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1423
ReExpr mkUnion(ReExpr... t)
Definition: Context.java:2163
Tactic orElse(Tactic t1, Tactic t2)
Definition: Context.java:2766
ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
Definition: Context.java:1655
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1246
SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
Definition: Context.java:2054
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1061
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4098
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1443
RatNum mkReal(String v)
Definition: Context.java:2325
FPNum mkFP(int v, FPSort s)
Definition: Context.java:3435
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2450
ArrayExpr mkConstArray(Sort domain, Expr v)
Definition: Context.java:1774
IDecRefQueue< ConstructorList > getConstructorListDRQ()
Definition: Context.java:4024
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:667
Expr mkFreshConst(String prefix, Sort range)
Definition: Context.java:584
IntSymbol mkSymbol(int i)
Definition: Context.java:93
StringSymbol mkSymbol(String name)
Definition: Context.java:101
BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1035
FPNum mkFPZero(FPSort s, boolean negative)
Definition: Context.java:3342
BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
Definition: Context.java:2036
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
Definition: Context.java:366
BoolExpr mkBoolConst(Symbol name)
Definition: Context.java:603
BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1022
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:901
IDecRefQueue< ASTVector > getASTVectorDRQ()
Definition: Context.java:4038
ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
Definition: Context.java:1795
Definition: FuncInterp.java:31
static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
Definition: Lambda.java:94
static long mkSetAdd(long a0, long a1, long a2)
Definition: Native.java:1946
static long mkBvsmod(long a0, long a1, long a2)
Definition: Native.java:1559
static long mkSimpleSolver(long a0)
Definition: Native.java:4503
static long tacticParOr(long a0, int a1, long[] a2)
Definition: Native.java:4172
static long mkXor(long a0, long a1, long a2)
Definition: Native.java:1235
static long mkSeqSuffix(long a0, long a1, long a2)
Definition: Native.java:2243
static long mkStringSort(long a0)
Definition: Native.java:2144
static long mkFpaSortQuadruple(long a0)
Definition: Native.java:6074
static long mkInt64(long a0, long a1, long a2)
Definition: Native.java:2063
static long mkSelect(long a0, long a1, long a2)
Definition: Native.java:1838
static long mkFpaNeg(long a0, long a1)
Definition: Native.java:6182
static long mkBvsub(long a0, long a1, long a2)
Definition: Native.java:1505
static long mkBvredor(long a0, long a1)
Definition: Native.java:1424
static long mkExtRotateLeft(long a0, long a1, long a2)
Definition: Native.java:1730
static native void setInternalErrorHandler(long ctx)
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1829
static long mkFpaSqrt(long a0, long a1, long a2)
Definition: Native.java:6236
static long mkFpaToReal(long a0, long a1)
Definition: Native.java:6452
static long mkFalse(long a0)
Definition: Native.java:1172
static long tacticUsingParams(long a0, long a1, long a2)
Definition: Native.java:4262
static long tacticRepeat(long a0, long a1, int a2)
Definition: Native.java:4217
static long mkFpaRoundNearestTiesToEven(long a0)
Definition: Native.java:5921
static void delContext(long a0)
Definition: Native.java:753
static long mkFpaFma(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:6227
static long mkSetComplement(long a0, long a1)
Definition: Native.java:1991
static long mkFpaSortHalf(long a0)
Definition: Native.java:6020
static long mkFpaIsSubnormal(long a0, long a1)
Definition: Native.java:6335
static long mkStrToInt(long a0, long a1)
Definition: Native.java:2342
static long mkAdd(long a0, int a1, long[] a2)
Definition: Native.java:1262
static long mkFpaRem(long a0, long a1, long a2)
Definition: Native.java:6245
static long mkBvSort(long a0, int a1)
Definition: Native.java:979
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
static long mkFpaIsNormal(long a0, long a1)
Definition: Native.java:6326
static long mkBvnegNoOverflow(long a0, long a1)
Definition: Native.java:1811
static long probeAnd(long a0, long a1, long a2)
Definition: Native.java:4325
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
Definition: Native.java:6155
static long mkBvsle(long a0, long a1, long a2)
Definition: Native.java:1595
static long mkFpaMin(long a0, long a1, long a2)
Definition: Native.java:6263
static String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
Definition: Native.java:3865
static long mkGt(long a0, long a1, long a2)
Definition: Native.java:1352
static long mkFpaNumeralDouble(long a0, double a1, long a2)
Definition: Native.java:6137
static long mkGe(long a0, long a1, long a2)
Definition: Native.java:1361
static void updateParamValue(long a0, String a1, String a2)
Definition: Native.java:774
static long tacticFailIf(long a0, long a1)
Definition: Native.java:4244
static long mkFpaMul(long a0, long a1, long a2, long a3)
Definition: Native.java:6209
static long mkFpaSort64(long a0)
Definition: Native.java:6065
static String getTacticName(long a0, int a1)
Definition: Native.java:4361
static long mkRotateRight(long a0, int a1, long a2)
Definition: Native.java:1721
static long mkReStar(long a0, long a1)
Definition: Native.java:2387
static long mkConstArray(long a0, long a1, long a2)
Definition: Native.java:1874
static long mkSeqAt(long a0, long a1, long a2)
Definition: Native.java:2297
static long probeNot(long a0, long a1)
Definition: Native.java:4343
static long mkDistinct(long a0, int a1, long[] a2)
Definition: Native.java:1190
static long mkInt2bv(long a0, int a1, long a2)
Definition: Native.java:1748
static long mkFpaToIeeeBv(long a0, long a1)
Definition: Native.java:6614
static long mkFpaRna(long a0)
Definition: Native.java:5948
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
Definition: Native.java:6254
static long mkFullSet(long a0, long a1)
Definition: Native.java:1937
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1775
static long mkSelectN(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1847
static long mkSolverForLogic(long a0, long a1)
Definition: Native.java:4512
static long probeGt(long a0, long a1, long a2)
Definition: Native.java:4289
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3874
static long mkDiv(long a0, long a1, long a2)
Definition: Native.java:1298
static long mkBvnot(long a0, long a1)
Definition: Native.java:1406
static long mkFpaNumeralInt(long a0, int a1, long a2)
Definition: Native.java:6146
static long mkSetDifference(long a0, long a1, long a2)
Definition: Native.java:1982
static long datatypeUpdateField(long a0, long a1, long a2, long a3)
Definition: Native.java:2801
static long mkFpaRoundNearestTiesToAway(long a0)
Definition: Native.java:5939
static long mkReConcat(long a0, int a1, long[] a2)
Definition: Native.java:2414
static long mkSeqToRe(long a0, long a1)
Definition: Native.java:2360
static long probeOr(long a0, long a1, long a2)
Definition: Native.java:4334
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
Definition: Native.java:6407
static long mkBvsgt(long a0, long a1, long a2)
Definition: Native.java:1631
static long mkFpaNan(long a0, long a1)
Definition: Native.java:6092
static long mkBv2int(long a0, long a1, boolean a2)
Definition: Native.java:1757
static long probeGe(long a0, long a1, long a2)
Definition: Native.java:4307
static long mkIntToStr(long a0, long a1)
Definition: Native.java:2351
static long mkReSort(long a0, long a1)
Definition: Native.java:2117
static String getProbeName(long a0, int a1)
Definition: Native.java:4379
static long tacticOrElse(long a0, long a1, long a2)
Definition: Native.java:4163
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1793
static long mkIte(long a0, long a1, long a2, long a3)
Definition: Native.java:1208
static long probeLe(long a0, long a1, long a2)
Definition: Native.java:4298
static long mkString(long a0, String a1)
Definition: Native.java:2162
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6416
static long mkFpaSort16(long a0)
Definition: Native.java:6029
static long mkBvule(long a0, long a1, long a2)
Definition: Native.java:1586
static long mkFpaRtz(long a0)
Definition: Native.java:6002
static long mkSetDel(long a0, long a1, long a2)
Definition: Native.java:1955
static long mkSolver(long a0)
Definition: Native.java:4494
static long mkIsInt(long a0, long a1)
Definition: Native.java:1397
static long mkPble(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2846
static long mkFpaSort128(long a0)
Definition: Native.java:6083
static long mkSignExt(long a0, int a1, long a2)
Definition: Native.java:1658
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
Definition: Native.java:1085
static long mkExtRotateRight(long a0, long a1, long a2)
Definition: Native.java:1739
static long mkBvashr(long a0, long a1, long a2)
Definition: Native.java:1703
static long mkFpaInf(long a0, long a1, boolean a2)
Definition: Native.java:6101
static long mkTrue(long a0)
Definition: Native.java:1163
static long mkRotateLeft(long a0, int a1, long a2)
Definition: Native.java:1712
static long mkArrayExt(long a0, long a1, long a2)
Definition: Native.java:2018
static void setAstPrintMode(long a0, int a1)
Definition: Native.java:3812
static long mkAtmost(long a0, int a1, long[] a2, int a3)
Definition: Native.java:2828
static long mkBvshl(long a0, long a1, long a2)
Definition: Native.java:1685
static long mkReRange(long a0, long a1, long a2)
Definition: Native.java:2423
static long mkFpaFp(long a0, long a1, long a2, long a3)
Definition: Native.java:6119
static long mkPbeq(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2864
static long mkSeqReplace(long a0, long a1, long a2, long a3)
Definition: Native.java:2288
static long mkBvsdiv(long a0, long a1, long a2)
Definition: Native.java:1532
static long mkConfig()
Definition: Native.java:721
static long mkBvmul(long a0, long a1, long a2)
Definition: Native.java:1514
static long mkFpaToFpBv(long a0, long a1, long a2)
Definition: Native.java:6389
static long mkFpaZero(long a0, long a1, boolean a2)
Definition: Native.java:6110
static long mkSeqUnit(long a0, long a1)
Definition: Native.java:2216
static long tacticCond(long a0, long a1, long a2, long a3)
Definition: Native.java:4208
static long mkImplies(long a0, long a1, long a2)
Definition: Native.java:1226
static long mkReal2int(long a0, long a1)
Definition: Native.java:1388
static long mkArrayDefault(long a0, long a1)
Definition: Native.java:1892
static long mkZeroExt(long a0, int a1, long a2)
Definition: Native.java:1667
static long mkBound(long a0, int a1, long a2)
Definition: Native.java:2531
static long mkNot(long a0, long a1)
Definition: Native.java:1199
static long mkFpaSortDouble(long a0)
Definition: Native.java:6056
static long mkBvugt(long a0, long a1, long a2)
Definition: Native.java:1622
static long mkReOption(long a0, long a1)
Definition: Native.java:2396
static long mkBvxnor(long a0, long a1, long a2)
Definition: Native.java:1478
static long mkFpaSortSingle(long a0)
Definition: Native.java:6038
static long mkReComplement(long a0, long a1)
Definition: Native.java:2450
static long mkStore(long a0, long a1, long a2, long a3)
Definition: Native.java:1856
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6443
static long mkSub(long a0, int a1, long[] a2)
Definition: Native.java:1280
static long mkBvsubNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1784
static long mkBvand(long a0, long a1, long a2)
Definition: Native.java:1433
static long mkFpaGt(long a0, long a1, long a2)
Definition: Native.java:6308
static long mkReFull(long a0, long a1)
Definition: Native.java:2468
static long mkStoreN(long a0, long a1, int a2, long[] a3, long a4)
Definition: Native.java:1865
static long probeEq(long a0, long a1, long a2)
Definition: Native.java:4316
static long mkBvudiv(long a0, long a1, long a2)
Definition: Native.java:1523
static long tacticParAndThen(long a0, long a1, long a2)
Definition: Native.java:4181
static long mkSeqConcat(long a0, int a1, long[] a2)
Definition: Native.java:2225
static long mkEmptySet(long a0, long a1)
Definition: Native.java:1928
static long mkAtleast(long a0, int a1, long[] a2, int a3)
Definition: Native.java:2837
static long mkMul(long a0, int a1, long[] a2)
Definition: Native.java:1271
static long mkLt(long a0, long a1, long a2)
Definition: Native.java:1334
static long mkFreshConst(long a0, String a1, long a2)
Definition: Native.java:1137
static long mkBvsrem(long a0, long a1, long a2)
Definition: Native.java:1550
static long mkSetMember(long a0, long a1, long a2)
Definition: Native.java:2000
static long mkSeqEmpty(long a0, long a1)
Definition: Native.java:2207
static long mkSolverFromTactic(long a0, long a1)
Definition: Native.java:4521
static long mkFpaAbs(long a0, long a1)
Definition: Native.java:6173
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6434
static long mkConst(long a0, long a1, long a2)
Definition: Native.java:1119
static long tacticSkip(long a0)
Definition: Native.java:4226
static void interrupt(long a0)
Definition: Native.java:782
static long mkOr(long a0, int a1, long[] a2)
Definition: Native.java:1253
static long mkBvadd(long a0, long a1, long a2)
Definition: Native.java:1496
static long mkFpaIsNan(long a0, long a1)
Definition: Native.java:6362
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1766
static long mkNumeral(long a0, String a1, long a2)
Definition: Native.java:2027
static long mkBvnor(long a0, long a1, long a2)
Definition: Native.java:1469
static long mkFpaLeq(long a0, long a1, long a2)
Definition: Native.java:6281
static int getNumTactics(long a0)
Definition: Native.java:4352
static long mkLe(long a0, long a1, long a2)
Definition: Native.java:1343
static long tacticFail(long a0)
Definition: Native.java:4235
static long mkBvsge(long a0, long a1, long a2)
Definition: Native.java:1613
static long mkBvxor(long a0, long a1, long a2)
Definition: Native.java:1451
static long tacticTryFor(long a0, long a1, int a2)
Definition: Native.java:4190
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:732
static long mkMod(long a0, long a1, long a2)
Definition: Native.java:1307
static long mkReEmpty(long a0, long a1)
Definition: Native.java:2459
static long mkFpaSort32(long a0)
Definition: Native.java:6047
static int getNumProbes(long a0)
Definition: Native.java:4370
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1820
static long mkInt(long a0, int a1, long a2)
Definition: Native.java:2045
static long mkConcat(long a0, long a1, long a2)
Definition: Native.java:1640
static long mkReLoop(long a0, long a1, int a2, int a3)
Definition: Native.java:2432
static long mkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:6623
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3883
static long mkSetSubset(long a0, long a1, long a2)
Definition: Native.java:2009
static long mkUnaryMinus(long a0, long a1)
Definition: Native.java:1289
static long mkBvuge(long a0, long a1, long a2)
Definition: Native.java:1604
static long mkFpaRoundTowardZero(long a0)
Definition: Native.java:5993
static long mkInt2real(long a0, long a1)
Definition: Native.java:1379
static long mkFpaLt(long a0, long a1, long a2)
Definition: Native.java:6290
static long mkSeqContains(long a0, long a1, long a2)
Definition: Native.java:2252
static long mkFpaIsPositive(long a0, long a1)
Definition: Native.java:6380
static long mkContextRc(long a0)
Definition: Native.java:745
static long mkFpaAdd(long a0, long a1, long a2, long a3)
Definition: Native.java:6191
static long mkPattern(long a0, int a1, long[] a2)
Definition: Native.java:2522
static long simplifyGetParamDescrs(long a0)
Definition: Native.java:3467
static long tacticFailIfNotDecided(long a0)
Definition: Native.java:4253
static long mkReIntersect(long a0, int a1, long[] a2)
Definition: Native.java:2441
static long mkBvor(long a0, long a1, long a2)
Definition: Native.java:1442
static long mkAnd(long a0, int a1, long[] a2)
Definition: Native.java:1244
static long mkSeqPrefix(long a0, long a1, long a2)
Definition: Native.java:2234
static long mkBvslt(long a0, long a1, long a2)
Definition: Native.java:1577
static long mkFpaGeq(long a0, long a1, long a2)
Definition: Native.java:6299
static long mkBvnand(long a0, long a1, long a2)
Definition: Native.java:1460
static String simplifyGetHelp(long a0)
Definition: Native.java:3458
static long mkSeqInRe(long a0, long a1, long a2)
Definition: Native.java:2369
static long mkIff(long a0, long a1, long a2)
Definition: Native.java:1217
static long mkFpaRne(long a0)
Definition: Native.java:5930
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
Definition: Native.java:6398
static long mkFpaIsNegative(long a0, long a1)
Definition: Native.java:6371
static long mkFpaRtp(long a0)
Definition: Native.java:5966
static long mkRepeat(long a0, int a1, long a2)
Definition: Native.java:1676
static long mkEq(long a0, long a1, long a2)
Definition: Native.java:1181
static long mkSeqExtract(long a0, long a1, long a2, long a3)
Definition: Native.java:2279
static long mkPbge(long a0, int a1, long[] a2, int[] a3, int a4)
Definition: Native.java:2855
static long mkFpaSub(long a0, long a1, long a2, long a3)
Definition: Native.java:6200
static long mkFpaRoundTowardPositive(long a0)
Definition: Native.java:5957
static long mkReUnion(long a0, int a1, long[] a2)
Definition: Native.java:2405
static long mkBvredand(long a0, long a1)
Definition: Native.java:1415
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6425
static long mkFpaIsInfinite(long a0, long a1)
Definition: Native.java:6353
static String tacticGetDescr(long a0, String a1)
Definition: Native.java:4406
static long mkRem(long a0, long a1, long a2)
Definition: Native.java:1316
static long mkSetUnion(long a0, int a1, long[] a2)
Definition: Native.java:1964
static long probeLt(long a0, long a1, long a2)
Definition: Native.java:4280
static void delConfig(long a0)
Definition: Native.java:727
static long mkBvneg(long a0, long a1)
Definition: Native.java:1487
static long mkBvurem(long a0, long a1, long a2)
Definition: Native.java:1541
static long mkPower(long a0, long a1, long a2)
Definition: Native.java:1325
static long mkFpaRoundTowardNegative(long a0)
Definition: Native.java:5975
static long mkSeqIndex(long a0, long a1, long a2, long a3)
Definition: Native.java:2324
static String probeGetDescr(long a0, String a1)
Definition: Native.java:4415
static long mkSetIntersect(long a0, int a1, long[] a2)
Definition: Native.java:1973
static long tacticWhen(long a0, long a1, long a2)
Definition: Native.java:4199
static long mkReal(long a0, int a1, int a2)
Definition: Native.java:2036
static long mkFpaRtn(long a0)
Definition: Native.java:5984
static long mkSeqLength(long a0, long a1)
Definition: Native.java:2315
static long probeConst(long a0, double a1)
Definition: Native.java:4271
static long mkFpaDiv(long a0, long a1, long a2, long a3)
Definition: Native.java:6218
static long mkBvlshr(long a0, long a1, long a2)
Definition: Native.java:1694
static long mkExtract(long a0, int a1, int a2, long a3)
Definition: Native.java:1649
static long mkFpaMax(long a0, long a1, long a2)
Definition: Native.java:6272
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
Definition: Native.java:6164
static long mkFpaEq(long a0, long a1, long a2)
Definition: Native.java:6317
static long mkMap(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1883
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1802
static long mkRePlus(long a0, long a1)
Definition: Native.java:2378
static long mkSeqSort(long a0, long a1)
Definition: Native.java:2090
static long tacticAndThen(long a0, long a1, long a2)
Definition: Native.java:4154
static long mkFpaIsZero(long a0, long a1)
Definition: Native.java:6344
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
expr max(expr const &a, expr const &b)
Definition: z3++.h:1591
def IntSort(ctx=None)
Definition: z3py.py:2907
def SeqSort(s)
Definition: z3py.py:9980
def RealSort(ctx=None)
Definition: z3py.py:2923
def SetSort(s)
Sets.
Definition: z3py.py:4568
def ArraySort(*sig)
Definition: z3py.py:4371
def BoolSort(ctx=None)
Definition: z3py.py:1533
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4994
def ReSort(s)
Definition: z3py.py:10294
def Map(f, *args)
Definition: z3py.py:4479
def String(name, ctx=None)
Definition: z3py.py:10085
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:7221
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9183
def TupleSort(name, sorts, ctx=None)
Definition: z3py.py:4971
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3740