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
35@SuppressWarnings("unchecked")
36public class Context implements AutoCloseable {
37 private long m_ctx;
38 static final Object creation_lock = new Object();
39
40 public Context () {
41 synchronized (creation_lock) {
42 m_ctx = Native.mkContextRc(0);
43 init();
44 }
45 }
46
47 protected Context (long m_ctx) {
48 synchronized (creation_lock) {
49 this.m_ctx = m_ctx;
50 init();
51 }
52 }
53
54
72 public Context(Map<String, String> settings) {
73 synchronized (creation_lock) {
74 long cfg = Native.mkConfig();
75 for (Map.Entry<String, String> kv : settings.entrySet()) {
76 Native.setParamValue(cfg, kv.getKey(), kv.getValue());
77 }
78 m_ctx = Native.mkContextRc(cfg);
79 Native.delConfig(cfg);
80 init();
81 }
82 }
83
84 private void init() {
85 setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
86 Native.setInternalErrorHandler(m_ctx);
87 }
88
94 public IntSymbol mkSymbol(int i)
95 {
96 return new IntSymbol(this, i);
97 }
98
103 {
104 return new StringSymbol(this, name);
105 }
106
110 Symbol[] mkSymbols(String[] names)
111 {
112 if (names == null)
113 return null;
114 Symbol[] result = new Symbol[names.length];
115 for (int i = 0; i < names.length; ++i)
116 result[i] = mkSymbol(names[i]);
117 return result;
118 }
119
120 private BoolSort m_boolSort = null;
121 private IntSort m_intSort = null;
122 private RealSort m_realSort = null;
123 private SeqSort<BitVecSort> m_stringSort = null;
124
129 {
130 if (m_boolSort == null) {
131 m_boolSort = new BoolSort(this);
132 }
133 return m_boolSort;
134 }
135
140 {
141 if (m_intSort == null) {
142 m_intSort = new IntSort(this);
143 }
144 return m_intSort;
145 }
146
151 {
152 if (m_realSort == null) {
153 m_realSort = new RealSort(this);
154 }
155 return m_realSort;
156 }
157
162 {
163 return new BoolSort(this);
164 }
165
170 {
171 if (m_stringSort == null) {
172 m_stringSort = mkStringSort();
173 }
174 return m_stringSort;
175 }
176
181 {
182 checkContextMatch(s);
183 return new UninterpretedSort(this, s);
184 }
185
190 {
191 return mkUninterpretedSort(mkSymbol(str));
192 }
193
198 {
199 return new IntSort(this);
200 }
201
206 {
207 return new RealSort(this);
208 }
209
213 public BitVecSort mkBitVecSort(int size)
214 {
215 return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
216 }
217
221 public <D extends Sort, R extends Sort> ArraySort<D, R> mkArraySort(D domain, R range)
222 {
223 checkContextMatch(domain);
224 checkContextMatch(range);
225 return new ArraySort<>(this, domain, range);
226 }
227
228
232 public <R extends Sort> ArraySort<Sort, R> mkArraySort(Sort[] domains, R range)
233 {
234 checkContextMatch(domains);
235 checkContextMatch(range);
236 return new ArraySort<>(this, domains, range);
237 }
238
243 {
244 return new SeqSort<>(this, Native.mkStringSort(nCtx()));
245 }
246
250 public <R extends Sort> SeqSort<R> mkSeqSort(R s)
251 {
252 return new SeqSort<>(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
253 }
254
258 public <R extends Sort> ReSort<R> mkReSort(R s)
259 {
260 return new ReSort<>(this, Native.mkReSort(nCtx(), s.getNativeObject()));
261 }
262
263
267 public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames,
268 Sort[] fieldSorts)
269 {
270 checkContextMatch(name);
271 checkContextMatch(fieldNames);
272 checkContextMatch(fieldSorts);
273 return new TupleSort(this, name, fieldNames.length, fieldNames,
274 fieldSorts);
275 }
276
280 public <R> EnumSort<R> mkEnumSort(Symbol name, Symbol... enumNames)
281
282 {
283 checkContextMatch(name);
284 checkContextMatch(enumNames);
285 return new EnumSort<>(this, name, enumNames);
286 }
287
291 public <R> EnumSort<R> mkEnumSort(String name, String... enumNames)
292
293 {
294 return new EnumSort<>(this, mkSymbol(name), mkSymbols(enumNames));
295 }
296
300 public <R extends Sort> ListSort<R> mkListSort(Symbol name, R elemSort)
301 {
302 checkContextMatch(name);
303 checkContextMatch(elemSort);
304 return new ListSort<>(this, name, elemSort);
305 }
306
310 public <R extends Sort> ListSort<R> mkListSort(String name, R elemSort)
311 {
312 checkContextMatch(elemSort);
313 return new ListSort<>(this, mkSymbol(name), elemSort);
314 }
315
319 public <R> FiniteDomainSort<R> mkFiniteDomainSort(Symbol name, long size)
320
321 {
322 checkContextMatch(name);
323 return new FiniteDomainSort<>(this, name, size);
324 }
325
329 public <R> FiniteDomainSort<R> mkFiniteDomainSort(String name, long size)
330
331 {
332 return new FiniteDomainSort<>(this, mkSymbol(name), size);
333 }
334
346 public <R> Constructor<R> mkConstructor(Symbol name, Symbol recognizer,
347 Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
348
349 {
350 return of(this, name, recognizer, fieldNames, sorts, sortRefs);
351 }
352
356 public <R> Constructor<R> mkConstructor(String name, String recognizer,
357 String[] fieldNames, Sort[] sorts, int[] sortRefs)
358 {
359 return of(this, mkSymbol(name), mkSymbol(recognizer), mkSymbols(fieldNames), sorts, sortRefs);
360 }
361
365 public <R> DatatypeSort<R> mkDatatypeSort(Symbol name, Constructor<R>[] constructors)
366 {
367 checkContextMatch(name);
368 checkContextMatch(constructors);
369 return new DatatypeSort<>(this, name, constructors);
370 }
371
375 public <R> DatatypeSort<R> mkDatatypeSort(String name, Constructor<R>[] constructors)
376
377 {
378 checkContextMatch(constructors);
379 return new DatatypeSort<>(this, mkSymbol(name), constructors);
380 }
381
388 {
389 checkContextMatch(names);
390 int n = names.length;
392 long[] n_constr = new long[n];
393 for (int i = 0; i < n; i++)
394 {
395 Constructor<Object>[] constructor = c[i];
396
397 checkContextMatch(constructor);
398 cla[i] = new ConstructorList<>(this, constructor);
399 n_constr[i] = cla[i].getNativeObject();
400 }
401 long[] n_res = new long[n];
402 Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
403 n_constr);
404 DatatypeSort<Object>[] res = new DatatypeSort[n];
405 for (int i = 0; i < n; i++)
406 res[i] = new DatatypeSort<>(this, n_res[i]);
407 return res;
408 }
409
414
415 {
416 return mkDatatypeSorts(mkSymbols(names), c);
417 }
418
425 public <F extends Sort, R extends Sort> Expr<R> mkUpdateField(FuncDecl<F> field, Expr<R> t, Expr<F> v)
426 throws Z3Exception
427 {
428 return (Expr<R>) Expr.create(this,
429 Native.datatypeUpdateField
430 (nCtx(), field.getNativeObject(),
431 t.getNativeObject(), v.getNativeObject()));
432 }
433
434
438 public <R extends Sort> FuncDecl<R> mkFuncDecl(Symbol name, Sort[] domain, R range)
439 {
440 checkContextMatch(name);
441 checkContextMatch(domain);
442 checkContextMatch(range);
443 return new FuncDecl<>(this, name, domain, range);
444 }
445
449 public <R extends Sort> FuncDecl<R> mkFuncDecl(Symbol name, Sort domain, R range)
450
451 {
452 checkContextMatch(name);
453 checkContextMatch(domain);
454 checkContextMatch(range);
455 Sort[] q = new Sort[] { domain };
456 return new FuncDecl<>(this, name, q, range);
457 }
458
462 public <R extends Sort> FuncDecl<R> mkFuncDecl(String name, Sort[] domain, R range)
463
464 {
465 checkContextMatch(domain);
466 checkContextMatch(range);
467 return new FuncDecl<>(this, mkSymbol(name), domain, range);
468 }
469
473 public <R extends Sort> FuncDecl<R> mkFuncDecl(String name, Sort domain, R range)
474
475 {
476 checkContextMatch(domain);
477 checkContextMatch(range);
478 Sort[] q = new Sort[] { domain };
479 return new FuncDecl<>(this, mkSymbol(name), q, range);
480 }
481
485 public <R extends Sort> FuncDecl<R> mkRecFuncDecl(Symbol name, Sort[] domain, R range)
486 {
487 checkContextMatch(name);
488 checkContextMatch(domain);
489 checkContextMatch(range);
490 return new FuncDecl<>(this, name, domain, range, true);
491 }
492
493
500 public <R extends Sort> void AddRecDef(FuncDecl<R> f, Expr<?>[] args, Expr<R> body)
501 {
502 checkContextMatch(f);
503 checkContextMatch(args);
504 checkContextMatch(body);
505 long[] argsNative = AST.arrayToNative(args);
506 Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject());
507 }
508
515 public <R extends Sort> FuncDecl<R> mkFreshFuncDecl(String prefix, Sort[] domain, R range)
516
517 {
518 checkContextMatch(domain);
519 checkContextMatch(range);
520 return new FuncDecl<>(this, prefix, domain, range);
521 }
522
526 public <R extends Sort> FuncDecl<R> mkConstDecl(Symbol name, R range)
527 {
528 checkContextMatch(name);
529 checkContextMatch(range);
530 return new FuncDecl<>(this, name, null, range);
531 }
532
536 public <R extends Sort> FuncDecl<R> mkConstDecl(String name, R range)
537 {
538 checkContextMatch(range);
539 return new FuncDecl<>(this, mkSymbol(name), null, range);
540 }
541
548 public <R extends Sort> FuncDecl<R> mkFreshConstDecl(String prefix, R range)
549
550 {
551 checkContextMatch(range);
552 return new FuncDecl<>(this, prefix, null, range);
553 }
554
560 public <R extends Sort> Expr<R> mkBound(int index, R ty)
561 {
562 return (Expr<R>) Expr.create(this,
563 Native.mkBound(nCtx(), index, ty.getNativeObject()));
564 }
565
569 @SafeVarargs
570 public final Pattern mkPattern(Expr<?>... terms)
571 {
572 if (terms.length == 0)
573 throw new Z3Exception("Cannot create a pattern from zero terms");
574
575 long[] termsNative = AST.arrayToNative(terms);
576 return new Pattern(this, Native.mkPattern(nCtx(), terms.length,
577 termsNative));
578 }
579
584 public <R extends Sort> Expr<R> mkConst(Symbol name, R range)
585 {
586 checkContextMatch(name);
587 checkContextMatch(range);
588
589 return (Expr<R>) Expr.create(
590 this,
591 Native.mkConst(nCtx(), name.getNativeObject(),
592 range.getNativeObject()));
593 }
594
599 public <R extends Sort> Expr<R> mkConst(String name, R range)
600 {
601 return mkConst(mkSymbol(name), range);
602 }
603
608 public <R extends Sort> Expr<R> mkFreshConst(String prefix, R range)
609 {
610 checkContextMatch(range);
611 return (Expr<R>) Expr.create(this,
612 Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
613 }
614
619 public <R extends Sort> Expr<R> mkConst(FuncDecl<R> f)
620 {
621 return mkApp(f, (Expr<?>[]) null);
622 }
623
628 {
629 return (BoolExpr) mkConst(name, getBoolSort());
630 }
631
636 {
637 return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
638 }
639
644 {
645 return (IntExpr) mkConst(name, getIntSort());
646 }
647
652 {
653 return (IntExpr) mkConst(name, getIntSort());
654 }
655
660 {
661 return (RealExpr) mkConst(name, getRealSort());
662 }
663
668 {
669 return (RealExpr) mkConst(name, getRealSort());
670 }
671
675 public BitVecExpr mkBVConst(Symbol name, int size)
676 {
677 return (BitVecExpr) mkConst(name, mkBitVecSort(size));
678 }
679
683 public BitVecExpr mkBVConst(String name, int size)
684 {
685 return (BitVecExpr) mkConst(name, mkBitVecSort(size));
686 }
687
691 @SafeVarargs
692 public final <R extends Sort> Expr<R> mkApp(FuncDecl<R> f, Expr<?>... args)
693 {
694 checkContextMatch(f);
695 checkContextMatch(args);
696 return Expr.create(this, f, args);
697 }
698
703 {
704 return new BoolExpr(this, Native.mkTrue(nCtx()));
705 }
706
711 {
712 return new BoolExpr(this, Native.mkFalse(nCtx()));
713 }
714
718 public BoolExpr mkBool(boolean value)
719 {
720 return value ? mkTrue() : mkFalse();
721 }
722
727 {
728 checkContextMatch(x);
729 checkContextMatch(y);
730 return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
731 y.getNativeObject()));
732 }
733
737 @SafeVarargs
738 public final BoolExpr mkDistinct(Expr<?>... args)
739 {
740 checkContextMatch(args);
741 return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
742 AST.arrayToNative(args)));
743 }
744
749 {
750 checkContextMatch(a);
751 return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
752 }
753
761 public <R extends Sort> Expr<R> mkITE(Expr<BoolSort> t1, Expr<? extends R> t2, Expr<? extends R> t3)
762 {
763 checkContextMatch(t1);
764 checkContextMatch(t2);
765 checkContextMatch(t3);
766 return (Expr<R>) Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
767 t2.getNativeObject(), t3.getNativeObject()));
768 }
769
774 {
775 checkContextMatch(t1);
776 checkContextMatch(t2);
777 return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
778 t2.getNativeObject()));
779 }
780
785 {
786 checkContextMatch(t1);
787 checkContextMatch(t2);
788 return new BoolExpr(this, Native.mkImplies(nCtx(),
789 t1.getNativeObject(), t2.getNativeObject()));
790 }
791
796 {
797 checkContextMatch(t1);
798 checkContextMatch(t2);
799 return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
800 t2.getNativeObject()));
801 }
802
806 @SafeVarargs
807 public final BoolExpr mkAnd(Expr<BoolSort>... t)
808 {
809 checkContextMatch(t);
810 return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
811 AST.arrayToNative(t)));
812 }
813
817 @SafeVarargs
818 public final BoolExpr mkOr(Expr<BoolSort>... t)
819 {
820 checkContextMatch(t);
821 return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
822 AST.arrayToNative(t)));
823 }
824
828 @SafeVarargs
829 public final <R extends ArithSort> ArithExpr<R> mkAdd(Expr<? extends R>... t)
830 {
831 checkContextMatch(t);
832 return (ArithExpr<R>) Expr.create(this,
833 Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
834 }
835
839 @SafeVarargs
840 public final <R extends ArithSort> ArithExpr<R> mkMul(Expr<? extends R>... t)
841 {
842 checkContextMatch(t);
843 return (ArithExpr<R>) Expr.create(this,
844 Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
845 }
846
850 @SafeVarargs
851 public final <R extends ArithSort> ArithExpr<R> mkSub(Expr<? extends R>... t)
852 {
853 checkContextMatch(t);
854 return (ArithExpr<R>) Expr.create(this,
855 Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
856 }
857
861 public <R extends ArithSort> ArithExpr<R> mkUnaryMinus(Expr<R> t)
862 {
863 checkContextMatch(t);
864 return (ArithExpr<R>) Expr.create(this,
865 Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
866 }
867
871 public <R extends ArithSort> ArithExpr<R> mkDiv(Expr<? extends R> t1, Expr<? extends R> t2)
872 {
873 checkContextMatch(t1);
874 checkContextMatch(t2);
875 return (ArithExpr<R>) Expr.create(this, Native.mkDiv(nCtx(),
876 t1.getNativeObject(), t2.getNativeObject()));
877 }
878
885 {
886 checkContextMatch(t1);
887 checkContextMatch(t2);
888 return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
889 t2.getNativeObject()));
890 }
891
898 {
899 checkContextMatch(t1);
900 checkContextMatch(t2);
901 return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
902 t2.getNativeObject()));
903 }
904
908 public <R extends ArithSort> ArithExpr<R> mkPower(Expr<? extends R> t1,
910 {
911 checkContextMatch(t1);
912 checkContextMatch(t2);
913 return (ArithExpr<R>) Expr.create(
914 this,
915 Native.mkPower(nCtx(), t1.getNativeObject(),
916 t2.getNativeObject()));
917 }
918
923 {
924 checkContextMatch(t1);
925 checkContextMatch(t2);
926 return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
927 t2.getNativeObject()));
928 }
929
934 {
935 checkContextMatch(t1);
936 checkContextMatch(t2);
937 return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
938 t2.getNativeObject()));
939 }
940
945 {
946 checkContextMatch(t1);
947 checkContextMatch(t2);
948 return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
949 t2.getNativeObject()));
950 }
951
956 {
957 checkContextMatch(t1);
958 checkContextMatch(t2);
959 return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
960 t2.getNativeObject()));
961 }
962
974 {
975 checkContextMatch(t);
976 return new RealExpr(this,
977 Native.mkInt2real(nCtx(), t.getNativeObject()));
978 }
979
987 {
988 checkContextMatch(t);
989 return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
990 }
991
996 {
997 checkContextMatch(t);
998 return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
999 }
1000
1007 {
1008 checkContextMatch(t);
1009 return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
1010 }
1011
1018 {
1019 checkContextMatch(t);
1020 return new BitVecExpr(this, Native.mkBvredand(nCtx(),
1021 t.getNativeObject()));
1022 }
1023
1030 {
1031 checkContextMatch(t);
1032 return new BitVecExpr(this, Native.mkBvredor(nCtx(),
1033 t.getNativeObject()));
1034 }
1035
1042 {
1043 checkContextMatch(t1);
1044 checkContextMatch(t2);
1045 return new BitVecExpr(this, Native.mkBvand(nCtx(),
1046 t1.getNativeObject(), t2.getNativeObject()));
1047 }
1048
1055 {
1056 checkContextMatch(t1);
1057 checkContextMatch(t2);
1058 return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1059 t2.getNativeObject()));
1060 }
1061
1068 {
1069 checkContextMatch(t1);
1070 checkContextMatch(t2);
1071 return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1072 t1.getNativeObject(), t2.getNativeObject()));
1073 }
1074
1081 {
1082 checkContextMatch(t1);
1083 checkContextMatch(t2);
1084 return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1085 t1.getNativeObject(), t2.getNativeObject()));
1086 }
1087
1094 {
1095 checkContextMatch(t1);
1096 checkContextMatch(t2);
1097 return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1098 t1.getNativeObject(), t2.getNativeObject()));
1099 }
1100
1107 {
1108 checkContextMatch(t1);
1109 checkContextMatch(t2);
1110 return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1111 t1.getNativeObject(), t2.getNativeObject()));
1112 }
1113
1120 {
1121 checkContextMatch(t);
1122 return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1123 }
1124
1131 {
1132 checkContextMatch(t1);
1133 checkContextMatch(t2);
1134 return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1135 t1.getNativeObject(), t2.getNativeObject()));
1136 }
1137
1144 {
1145 checkContextMatch(t1);
1146 checkContextMatch(t2);
1147 return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1148 t1.getNativeObject(), t2.getNativeObject()));
1149 }
1150
1157 {
1158 checkContextMatch(t1);
1159 checkContextMatch(t2);
1160 return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1161 t1.getNativeObject(), t2.getNativeObject()));
1162 }
1163
1172 {
1173 checkContextMatch(t1);
1174 checkContextMatch(t2);
1175 return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1176 t1.getNativeObject(), t2.getNativeObject()));
1177 }
1178
1193 {
1194 checkContextMatch(t1);
1195 checkContextMatch(t2);
1196 return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1197 t1.getNativeObject(), t2.getNativeObject()));
1198 }
1199
1208 {
1209 checkContextMatch(t1);
1210 checkContextMatch(t2);
1211 return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1212 t1.getNativeObject(), t2.getNativeObject()));
1213 }
1214
1226 {
1227 checkContextMatch(t1);
1228 checkContextMatch(t2);
1229 return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1230 t1.getNativeObject(), t2.getNativeObject()));
1231 }
1232
1240 {
1241 checkContextMatch(t1);
1242 checkContextMatch(t2);
1243 return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1244 t1.getNativeObject(), t2.getNativeObject()));
1245 }
1246
1253 {
1254 checkContextMatch(t1);
1255 checkContextMatch(t2);
1256 return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1257 t2.getNativeObject()));
1258 }
1259
1266 {
1267 checkContextMatch(t1);
1268 checkContextMatch(t2);
1269 return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1270 t2.getNativeObject()));
1271 }
1272
1279 {
1280 checkContextMatch(t1);
1281 checkContextMatch(t2);
1282 return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1283 t2.getNativeObject()));
1284 }
1285
1292 {
1293 checkContextMatch(t1);
1294 checkContextMatch(t2);
1295 return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1296 t2.getNativeObject()));
1297 }
1298
1305 {
1306 checkContextMatch(t1);
1307 checkContextMatch(t2);
1308 return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1309 t2.getNativeObject()));
1310 }
1311
1318 {
1319 checkContextMatch(t1);
1320 checkContextMatch(t2);
1321 return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1322 t2.getNativeObject()));
1323 }
1324
1331 {
1332 checkContextMatch(t1);
1333 checkContextMatch(t2);
1334 return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1335 t2.getNativeObject()));
1336 }
1337
1344 {
1345 checkContextMatch(t1);
1346 checkContextMatch(t2);
1347 return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1348 t2.getNativeObject()));
1349 }
1350
1362 {
1363 checkContextMatch(t1);
1364 checkContextMatch(t2);
1365 return new BitVecExpr(this, Native.mkConcat(nCtx(),
1366 t1.getNativeObject(), t2.getNativeObject()));
1367 }
1368
1377 public BitVecExpr mkExtract(int high, int low, Expr<BitVecSort> t)
1378
1379 {
1380 checkContextMatch(t);
1381 return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1382 t.getNativeObject()));
1383 }
1384
1393 {
1394 checkContextMatch(t);
1395 return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1396 t.getNativeObject()));
1397 }
1398
1407 {
1408 checkContextMatch(t);
1409 return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1410 t.getNativeObject()));
1411 }
1412
1419 {
1420 checkContextMatch(t);
1421 return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1422 t.getNativeObject()));
1423 }
1424
1437 {
1438 checkContextMatch(t1);
1439 checkContextMatch(t2);
1440 return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1441 t1.getNativeObject(), t2.getNativeObject()));
1442 }
1443
1456 {
1457 checkContextMatch(t1);
1458 checkContextMatch(t2);
1459 return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1460 t1.getNativeObject(), t2.getNativeObject()));
1461 }
1462
1476 {
1477 checkContextMatch(t1);
1478 checkContextMatch(t2);
1479 return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1480 t1.getNativeObject(), t2.getNativeObject()));
1481 }
1482
1489 {
1490 checkContextMatch(t);
1491 return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1492 t.getNativeObject()));
1493 }
1494
1501 {
1502 checkContextMatch(t);
1503 return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1504 t.getNativeObject()));
1505 }
1506
1514
1515 {
1516 checkContextMatch(t1);
1517 checkContextMatch(t2);
1518 return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1519 t1.getNativeObject(), t2.getNativeObject()));
1520 }
1521
1529
1530 {
1531 checkContextMatch(t1);
1532 checkContextMatch(t2);
1533 return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1534 t1.getNativeObject(), t2.getNativeObject()));
1535 }
1536
1547 {
1548 checkContextMatch(t);
1549 return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1550 t.getNativeObject()));
1551 }
1552
1567 public IntExpr mkBV2Int(Expr<BitVecSort> t, boolean signed)
1568 {
1569 checkContextMatch(t);
1570 return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1571 (signed)));
1572 }
1573
1580 boolean isSigned)
1581 {
1582 checkContextMatch(t1);
1583 checkContextMatch(t2);
1584 return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1585 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1586 }
1587
1594
1595 {
1596 checkContextMatch(t1);
1597 checkContextMatch(t2);
1598 return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1599 t1.getNativeObject(), t2.getNativeObject()));
1600 }
1601
1608
1609 {
1610 checkContextMatch(t1);
1611 checkContextMatch(t2);
1612 return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1613 t1.getNativeObject(), t2.getNativeObject()));
1614 }
1615
1622 boolean isSigned)
1623 {
1624 checkContextMatch(t1);
1625 checkContextMatch(t2);
1626 return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1627 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1628 }
1629
1636
1637 {
1638 checkContextMatch(t1);
1639 checkContextMatch(t2);
1640 return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1641 t1.getNativeObject(), t2.getNativeObject()));
1642 }
1643
1650 {
1651 checkContextMatch(t);
1652 return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1653 t.getNativeObject()));
1654 }
1655
1662 boolean isSigned)
1663 {
1664 checkContextMatch(t1);
1665 checkContextMatch(t2);
1666 return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1667 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1668 }
1669
1676
1677 {
1678 checkContextMatch(t1);
1679 checkContextMatch(t2);
1680 return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1681 t1.getNativeObject(), t2.getNativeObject()));
1682 }
1683
1687 public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkArrayConst(Symbol name, D domain, R range)
1688
1689 {
1690 return (ArrayExpr<D, R>) mkConst(name, mkArraySort(domain, range));
1691 }
1692
1696 public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkArrayConst(String name, D domain, R range)
1697
1698 {
1699 return (ArrayExpr<D, R>) mkConst(mkSymbol(name), mkArraySort(domain, range));
1700 }
1701
1715 public <D extends Sort, R extends Sort> Expr<R> mkSelect(Expr<ArraySort<D, R>> a, Expr<D> i)
1716 {
1717 checkContextMatch(a);
1718 checkContextMatch(i);
1719 return (Expr<R>) Expr.create(
1720 this,
1721 Native.mkSelect(nCtx(), a.getNativeObject(),
1722 i.getNativeObject()));
1723 }
1724
1737 public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort, R>> a, Expr<?>[] args)
1738 {
1739 checkContextMatch(a);
1740 checkContextMatch(args);
1741 return (Expr<R>) Expr.create(
1742 this,
1743 Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
1744 }
1745
1762 public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkStore(Expr<ArraySort<D, R>> a, Expr<D> i, Expr<R> v)
1763 {
1764 checkContextMatch(a);
1765 checkContextMatch(i);
1766 checkContextMatch(v);
1767 return new ArrayExpr<>(this, Native.mkStore(nCtx(), a.getNativeObject(),
1768 i.getNativeObject(), v.getNativeObject()));
1769 }
1770
1787 public <R extends Sort> ArrayExpr<Sort, R> mkStore(Expr<ArraySort<Sort, R>> a, Expr<?>[] args, Expr<R> v)
1788 {
1789 checkContextMatch(a);
1790 checkContextMatch(args);
1791 checkContextMatch(v);
1792 return new ArrayExpr<>(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
1793 args.length, AST.arrayToNative(args), v.getNativeObject()));
1794 }
1795
1805 public <D extends Sort, R extends Sort> ArrayExpr<D, R> mkConstArray(D domain, Expr<R> v)
1806 {
1807 checkContextMatch(domain);
1808 checkContextMatch(v);
1809 return new ArrayExpr<>(this, Native.mkConstArray(nCtx(),
1810 domain.getNativeObject(), v.getNativeObject()));
1811 }
1812
1826 @SafeVarargs
1827 public final <D extends Sort, R1 extends Sort, R2 extends Sort> ArrayExpr<D, R2> mkMap(FuncDecl<R2> f, Expr<ArraySort<D, R1>>... args)
1828 {
1829 checkContextMatch(f);
1830 checkContextMatch(args);
1831 return (ArrayExpr<D, R2>) Expr.create(this, Native.mkMap(nCtx(),
1832 f.getNativeObject(), AST.arrayLength(args),
1833 AST.arrayToNative(args)));
1834 }
1835
1842 public <D extends Sort, R extends Sort> Expr<R> mkTermArray(Expr<ArraySort<D, R>> array)
1843 {
1844 checkContextMatch(array);
1845 return (Expr<R>) Expr.create(this,
1846 Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1847 }
1848
1852 public <D extends Sort, R extends Sort> Expr<D> mkArrayExt(Expr<ArraySort<D, R>> arg1, Expr<ArraySort<D, R>> arg2)
1853 {
1854 checkContextMatch(arg1);
1855 checkContextMatch(arg2);
1856 return (Expr<D>) Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
1857 }
1858
1859
1863 public <D extends Sort> SetSort<D> mkSetSort(D ty)
1864 {
1865 checkContextMatch(ty);
1866 return new SetSort<>(this, ty);
1867 }
1868
1872 public <D extends Sort> ArrayExpr<D, BoolSort> mkEmptySet(D domain)
1873 {
1874 checkContextMatch(domain);
1875 return (ArrayExpr<D, BoolSort>) Expr.create(this,
1876 Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1877 }
1878
1882 public <D extends Sort> ArrayExpr<D, BoolSort> mkFullSet(D domain)
1883 {
1884 checkContextMatch(domain);
1885 return (ArrayExpr<D, BoolSort>) Expr.create(this,
1886 Native.mkFullSet(nCtx(), domain.getNativeObject()));
1887 }
1888
1892 public <D extends Sort> ArrayExpr<D, BoolSort> mkSetAdd(Expr<ArraySort<D, BoolSort>> set, Expr<D> element)
1893 {
1894 checkContextMatch(set);
1895 checkContextMatch(element);
1896 return (ArrayExpr<D, BoolSort>) Expr.create(this,
1897 Native.mkSetAdd(nCtx(), set.getNativeObject(),
1898 element.getNativeObject()));
1899 }
1900
1904 public <D extends Sort> ArrayExpr<D, BoolSort> mkSetDel(Expr<ArraySort<D, BoolSort>> set, Expr<D> element)
1905 {
1906 checkContextMatch(set);
1907 checkContextMatch(element);
1908 return (ArrayExpr<D, BoolSort>)Expr.create(this,
1909 Native.mkSetDel(nCtx(), set.getNativeObject(),
1910 element.getNativeObject()));
1911 }
1912
1916 @SafeVarargs
1917 public final <D extends Sort> ArrayExpr<D, BoolSort> mkSetUnion(Expr<ArraySort<D, BoolSort>>... args)
1918 {
1919 checkContextMatch(args);
1920 return (ArrayExpr<D, BoolSort>)Expr.create(this,
1921 Native.mkSetUnion(nCtx(), args.length,
1922 AST.arrayToNative(args)));
1923 }
1924
1928 @SafeVarargs
1930 {
1931 checkContextMatch(args);
1932 return (ArrayExpr<D, BoolSort>) Expr.create(this,
1933 Native.mkSetIntersect(nCtx(), args.length,
1934 AST.arrayToNative(args)));
1935 }
1936
1940 public <D extends Sort> ArrayExpr<D, BoolSort> mkSetDifference(Expr<ArraySort<D, BoolSort>> arg1, Expr<ArraySort<D, BoolSort>> arg2)
1941 {
1942 checkContextMatch(arg1);
1943 checkContextMatch(arg2);
1944 return (ArrayExpr<D, BoolSort>) Expr.create(this,
1945 Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1946 arg2.getNativeObject()));
1947 }
1948
1952 public <D extends Sort> ArrayExpr<D, BoolSort> mkSetComplement(Expr<ArraySort<D, BoolSort>> arg)
1953 {
1954 checkContextMatch(arg);
1955 return (ArrayExpr<D, BoolSort>)Expr.create(this,
1956 Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1957 }
1958
1962 public <D extends Sort> BoolExpr mkSetMembership(Expr<D> elem, Expr<ArraySort<D, BoolSort>> set)
1963 {
1964 checkContextMatch(elem);
1965 checkContextMatch(set);
1966 return (BoolExpr) Expr.create(this,
1967 Native.mkSetMember(nCtx(), elem.getNativeObject(),
1968 set.getNativeObject()));
1969 }
1970
1974 public <D extends Sort> BoolExpr mkSetSubset(Expr<ArraySort<D, BoolSort>> arg1, Expr<ArraySort<D, BoolSort>> arg2)
1975 {
1976 checkContextMatch(arg1);
1977 checkContextMatch(arg2);
1978 return (BoolExpr) Expr.create(this,
1979 Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1980 arg2.getNativeObject()));
1981 }
1982
1983
1991 public <R extends Sort> SeqExpr<R> mkEmptySeq(R s)
1992 {
1993 checkContextMatch(s);
1994 return (SeqExpr<R>) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
1995 }
1996
2000 public <R extends Sort> SeqExpr<R> mkUnit(Expr<R> elem)
2001 {
2002 checkContextMatch(elem);
2003 return (SeqExpr<R>) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
2004 }
2005
2010 {
2011 return (SeqExpr<BitVecSort>) Expr.create(this, Native.mkString(nCtx(), s));
2012 }
2013
2018 {
2019 return (SeqExpr<BitVecSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
2020 }
2021
2026 {
2027 return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
2028 }
2029
2033 @SafeVarargs
2034 public final <R extends Sort> SeqExpr<R> mkConcat(Expr<SeqSort<R>>... t)
2035 {
2036 checkContextMatch(t);
2037 return (SeqExpr<R>) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
2038 }
2039
2040
2044 public <R extends Sort> IntExpr mkLength(Expr<SeqSort<BitVecSort>> s)
2045 {
2046 checkContextMatch(s);
2047 return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
2048 }
2049
2053 public <R extends Sort> BoolExpr mkPrefixOf(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
2054 {
2055 checkContextMatch(s1, s2);
2056 return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2057 }
2058
2062 public <R extends Sort> BoolExpr mkSuffixOf(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
2063 {
2064 checkContextMatch(s1, s2);
2065 return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2066 }
2067
2071 public <R extends Sort> BoolExpr mkContains(Expr<SeqSort<BitVecSort>> s1, Expr<SeqSort<BitVecSort>> s2)
2072 {
2073 checkContextMatch(s1, s2);
2074 return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
2075 }
2076
2080 public <R extends Sort> SeqExpr<R> mkAt(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> index)
2081 {
2082 checkContextMatch(s, index);
2083 return (SeqExpr<R>) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
2084 }
2085
2089 public <R extends Sort> Expr<R> MkNth(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> index)
2090 {
2091 checkContextMatch(s, index);
2092 return (Expr<R>) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
2093 }
2094
2095
2099 public <R extends Sort> SeqExpr<R> mkExtract(Expr<SeqSort<BitVecSort>> s, Expr<IntSort> offset, Expr<IntSort> length)
2100 {
2101 checkContextMatch(s, offset, length);
2102 return (SeqExpr<R>) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
2103 }
2104
2108 public <R extends Sort> IntExpr mkIndexOf(Expr<SeqSort<BitVecSort>> s, Expr<SeqSort<BitVecSort>> substr, Expr<IntSort> offset)
2109 {
2110 checkContextMatch(s, substr, offset);
2111 return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
2112 }
2113
2117 public <R extends Sort> SeqExpr<R> mkReplace(Expr<SeqSort<BitVecSort>> s, Expr<SeqSort<BitVecSort>> src, Expr<SeqSort<BitVecSort>> dst)
2118 {
2119 checkContextMatch(s, src, dst);
2120 return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
2121 }
2122
2126 public <R extends Sort> ReExpr<R> mkToRe(Expr<SeqSort<BitVecSort>> s)
2127 {
2128 checkContextMatch(s);
2129 return (ReExpr<R>) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
2130 }
2131
2132
2136 public <R extends Sort> BoolExpr mkInRe(Expr<SeqSort<BitVecSort>> s, Expr<ReSort<R>> re)
2137 {
2138 checkContextMatch(s, re);
2139 return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
2140 }
2141
2145 public <R extends Sort> ReExpr<R> mkStar(Expr<ReSort<R>> re)
2146 {
2147 checkContextMatch(re);
2148 return (ReExpr<R>) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
2149 }
2150
2154 public <R extends Sort> ReExpr<R> mkLoop(Expr<ReSort<R>> re, int lo, int hi)
2155 {
2156 return (ReExpr<R>) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
2157 }
2158
2162 public <R extends Sort> ReExpr<R> mkLoop(Expr<ReSort<R>> re, int lo)
2163 {
2164 return (ReExpr<R>) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
2165 }
2166
2167
2171 public <R extends Sort> ReExpr<R> mkPlus(Expr<ReSort<R>> re)
2172 {
2173 checkContextMatch(re);
2174 return (ReExpr<R>) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
2175 }
2176
2180 public <R extends Sort> ReExpr<R> mkOption(Expr<ReSort<R>> re)
2181 {
2182 checkContextMatch(re);
2183 return (ReExpr<R>) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
2184 }
2185
2189 public <R extends Sort> ReExpr<R> mkComplement(Expr<ReSort<R>> re)
2190 {
2191 checkContextMatch(re);
2192 return (ReExpr<R>) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
2193 }
2194
2198 @SafeVarargs
2199 public final <R extends Sort> ReExpr<R> mkConcat(ReExpr<R>... t)
2200 {
2201 checkContextMatch(t);
2202 return (ReExpr<R>) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2203 }
2204
2208 @SafeVarargs
2209 public final <R extends Sort> ReExpr<R> mkUnion(Expr<ReSort<R>>... t)
2210 {
2211 checkContextMatch(t);
2212 return (ReExpr<R>) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2213 }
2214
2218 @SafeVarargs
2219 public final <R extends Sort> ReExpr<R> mkIntersect(Expr<ReSort<R>>... t)
2220 {
2221 checkContextMatch(t);
2222 return (ReExpr<R>) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
2223 }
2224
2228 public <R extends Sort> ReExpr<R> mkEmptyRe(R s)
2229 {
2230 return (ReExpr<R>) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
2231 }
2232
2236 public <R extends Sort> ReExpr<R> mkFullRe(R s)
2237 {
2238 return (ReExpr<R>) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
2239 }
2240
2244 public <R extends Sort> ReExpr<R> mkRange(Expr<SeqSort<BitVecSort>> lo, Expr<SeqSort<BitVecSort>> hi)
2245 {
2246 checkContextMatch(lo, hi);
2247 return (ReExpr<R>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
2248 }
2249
2250
2254 public BoolExpr mkAtMost(Expr<BoolSort>[] args, int k)
2255 {
2256 checkContextMatch(args);
2257 return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
2258 }
2259
2263 public BoolExpr mkAtLeast(Expr<BoolSort>[] args, int k)
2264 {
2265 checkContextMatch(args);
2266 return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
2267 }
2268
2272 public BoolExpr mkPBLe(int[] coeffs, Expr<BoolSort>[] args, int k)
2273 {
2274 checkContextMatch(args);
2275 return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2276 }
2277
2281 public BoolExpr mkPBGe(int[] coeffs, Expr<BoolSort>[] args, int k)
2282 {
2283 checkContextMatch(args);
2284 return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2285 }
2286
2290 public BoolExpr mkPBEq(int[] coeffs, Expr<BoolSort>[] args, int k)
2291 {
2292 checkContextMatch(args);
2293 return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
2294 }
2295
2307 public <R extends Sort> Expr<R> mkNumeral(String v, R ty)
2308 {
2309 checkContextMatch(ty);
2310 return (Expr<R>) Expr.create(this,
2311 Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
2312 }
2313
2324 public <R extends Sort> Expr<R> mkNumeral(int v, R ty)
2325 {
2326 checkContextMatch(ty);
2327 return (Expr<R>) Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
2328 }
2329
2340 public <R extends Sort> Expr<R> mkNumeral(long v, R ty)
2341 {
2342 checkContextMatch(ty);
2343 return (Expr<R>) Expr.create(this,
2344 Native.mkInt64(nCtx(), v, ty.getNativeObject()));
2345 }
2346
2356 public RatNum mkReal(int num, int den)
2357 {
2358 if (den == 0) {
2359 throw new Z3Exception("Denominator is zero");
2360 }
2361
2362 return new RatNum(this, Native.mkReal(nCtx(), num, den));
2363 }
2364
2372 {
2373
2374 return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2375 .getNativeObject()));
2376 }
2377
2384 public RatNum mkReal(int v)
2385 {
2386
2387 return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2388 .getNativeObject()));
2389 }
2390
2397 public RatNum mkReal(long v)
2398 {
2399
2400 return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2401 .getNativeObject()));
2402 }
2403
2409 {
2410
2411 return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2412 .getNativeObject()));
2413 }
2414
2421 public IntNum mkInt(int v)
2422 {
2423
2424 return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2425 .getNativeObject()));
2426 }
2427
2434 public IntNum mkInt(long v)
2435 {
2436
2437 return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2438 .getNativeObject()));
2439 }
2440
2446 public BitVecNum mkBV(String v, int size)
2447 {
2448 return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2449 }
2450
2456 public BitVecNum mkBV(int v, int size)
2457 {
2458 return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2459 }
2460
2466 public BitVecNum mkBV(long v, int size)
2467 {
2468 return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2469 }
2470
2496 public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr<BoolSort> body,
2497 int weight, Pattern[] patterns, Expr<?>[] noPatterns,
2498 Symbol quantifierID, Symbol skolemID)
2499 {
2500 return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2501 noPatterns, quantifierID, skolemID);
2502 }
2503
2508 public Quantifier mkForall(Expr<?>[] boundConstants, Expr<BoolSort> body, int weight,
2509 Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID,
2510 Symbol skolemID)
2511 {
2512
2513 return Quantifier.of(this, true, boundConstants, body, weight,
2514 patterns, noPatterns, quantifierID, skolemID);
2515 }
2516
2521 public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr<BoolSort> body,
2522 int weight, Pattern[] patterns, Expr<?>[] noPatterns,
2523 Symbol quantifierID, Symbol skolemID)
2524 {
2525
2526 return Quantifier.of(this, false, sorts, names, body, weight,
2527 patterns, noPatterns, quantifierID, skolemID);
2528 }
2529
2534 public Quantifier mkExists(Expr<?>[] boundConstants, Expr<BoolSort> body, int weight,
2535 Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID,
2536 Symbol skolemID)
2537 {
2538
2539 return Quantifier.of(this, false, boundConstants, body, weight,
2540 patterns, noPatterns, quantifierID, skolemID);
2541 }
2542
2547 public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
2548 Symbol[] names, Expr<BoolSort> body, int weight, Pattern[] patterns,
2549 Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
2550
2551 {
2552
2553 if (universal)
2554 return mkForall(sorts, names, body, weight, patterns, noPatterns,
2555 quantifierID, skolemID);
2556 else
2557 return mkExists(sorts, names, body, weight, patterns, noPatterns,
2558 quantifierID, skolemID);
2559 }
2560
2565 public Quantifier mkQuantifier(boolean universal, Expr<?>[] boundConstants,
2566 Expr<BoolSort> body, int weight, Pattern[] patterns, Expr<?>[] noPatterns,
2567 Symbol quantifierID, Symbol skolemID)
2568 {
2569
2570 if (universal)
2571 return mkForall(boundConstants, body, weight, patterns, noPatterns,
2572 quantifierID, skolemID);
2573 else
2574 return mkExists(boundConstants, body, weight, patterns, noPatterns,
2575 quantifierID, skolemID);
2576 }
2577
2595 public <R extends Sort> Lambda<R> mkLambda(Sort[] sorts, Symbol[] names, Expr<R> body)
2596 {
2597 return Lambda.of(this, sorts, names, body);
2598 }
2599
2606 public <R extends Sort> Lambda<R> mkLambda(Expr<?>[] boundConstants, Expr<R> body)
2607 {
2608 return Lambda.of(this, boundConstants, body);
2609 }
2610
2611
2627 {
2628 Native.setAstPrintMode(nCtx(), value.toInt());
2629 }
2630
2645 String status, String attributes, Expr<BoolSort>[] assumptions,
2646 Expr<BoolSort> formula)
2647 {
2648
2649 return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2650 attributes, assumptions.length,
2651 AST.arrayToNative(assumptions), formula.getNativeObject());
2652 }
2653
2663 public BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames,
2664 Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
2665 {
2666 int csn = Symbol.arrayLength(sortNames);
2667 int cs = Sort.arrayLength(sorts);
2668 int cdn = Symbol.arrayLength(declNames);
2669 int cd = AST.arrayLength(decls);
2670 if (csn != cs || cdn != cd) {
2671 throw new Z3Exception("Argument size mismatch");
2672 }
2673 ASTVector v = new ASTVector(this, Native.parseSmtlib2String(nCtx(),
2674 str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2675 AST.arrayToNative(sorts), AST.arrayLength(decls),
2676 Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2677 return v.ToBoolExprArray();
2678 }
2679
2684 public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames,
2685 Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
2686 {
2687 int csn = Symbol.arrayLength(sortNames);
2688 int cs = Sort.arrayLength(sorts);
2689 int cdn = Symbol.arrayLength(declNames);
2690 int cd = AST.arrayLength(decls);
2691 if (csn != cs || cdn != cd)
2692 throw new Z3Exception("Argument size mismatch");
2693 ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
2694 fileName, AST.arrayLength(sorts),
2695 Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2696 AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2697 AST.arrayToNative(decls)));
2698 return v.ToBoolExprArray();
2699 }
2700
2711 public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
2712 {
2713 return new Goal(this, models, unsatCores, proofs);
2714 }
2715
2720 {
2721 return new Params(this);
2722 }
2723
2727 public int getNumTactics()
2728 {
2729 return Native.getNumTactics(nCtx());
2730 }
2731
2736 {
2737
2738 int n = getNumTactics();
2739 String[] res = new String[n];
2740 for (int i = 0; i < n; i++)
2741 res[i] = Native.getTacticName(nCtx(), i);
2742 return res;
2743 }
2744
2750 {
2751 return Native.tacticGetDescr(nCtx(), name);
2752 }
2753
2758 {
2759 return new Tactic(this, name);
2760 }
2761
2766 public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
2767
2768 {
2769 checkContextMatch(t1);
2770 checkContextMatch(t2);
2771 checkContextMatch(ts);
2772
2773 long last = 0;
2774 if (ts != null && ts.length > 0)
2775 {
2776 last = ts[ts.length - 1].getNativeObject();
2777 for (int i = ts.length - 2; i >= 0; i--) {
2778 last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2779 last);
2780 }
2781 }
2782 if (last != 0)
2783 {
2784 last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2785 return new Tactic(this, Native.tacticAndThen(nCtx(),
2786 t1.getNativeObject(), last));
2787 } else
2788 return new Tactic(this, Native.tacticAndThen(nCtx(),
2789 t1.getNativeObject(), t2.getNativeObject()));
2790 }
2791
2798 public Tactic then(Tactic t1, Tactic t2, Tactic... ts)
2799 {
2800 return andThen(t1, t2, ts);
2801 }
2802
2809 {
2810 checkContextMatch(t1);
2811 checkContextMatch(t2);
2812 return new Tactic(this, Native.tacticOrElse(nCtx(),
2813 t1.getNativeObject(), t2.getNativeObject()));
2814 }
2815
2822 public Tactic tryFor(Tactic t, int ms)
2823 {
2824 checkContextMatch(t);
2825 return new Tactic(this, Native.tacticTryFor(nCtx(),
2826 t.getNativeObject(), ms));
2827 }
2828
2836 {
2837 checkContextMatch(t);
2838 checkContextMatch(p);
2839 return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2840 t.getNativeObject()));
2841 }
2842
2848 public Tactic cond(Probe p, Tactic t1, Tactic t2)
2849 {
2850 checkContextMatch(p);
2851 checkContextMatch(t1);
2852 checkContextMatch(t2);
2853 return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2854 t1.getNativeObject(), t2.getNativeObject()));
2855 }
2856
2861 public Tactic repeat(Tactic t, int max)
2862 {
2863 checkContextMatch(t);
2864 return new Tactic(this, Native.tacticRepeat(nCtx(),
2865 t.getNativeObject(), max));
2866 }
2867
2871 public Tactic skip()
2872 {
2873 return new Tactic(this, Native.tacticSkip(nCtx()));
2874 }
2875
2879 public Tactic fail()
2880 {
2881 return new Tactic(this, Native.tacticFail(nCtx()));
2882 }
2883
2889 {
2890 checkContextMatch(p);
2891 return new Tactic(this,
2892 Native.tacticFailIf(nCtx(), p.getNativeObject()));
2893 }
2894
2900 {
2901 return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2902 }
2903
2909 {
2910 checkContextMatch(t);
2911 checkContextMatch(p);
2912 return new Tactic(this, Native.tacticUsingParams(nCtx(),
2913 t.getNativeObject(), p.getNativeObject()));
2914 }
2915
2923 {
2924 return usingParams(t, p);
2925 }
2926
2930 public Tactic parOr(Tactic... t)
2931 {
2932 checkContextMatch(t);
2933 return new Tactic(this, Native.tacticParOr(nCtx(),
2935 }
2936
2942 {
2943 checkContextMatch(t1);
2944 checkContextMatch(t2);
2945 return new Tactic(this, Native.tacticParAndThen(nCtx(),
2946 t1.getNativeObject(), t2.getNativeObject()));
2947 }
2948
2954 public void interrupt()
2955 {
2956 Native.interrupt(nCtx());
2957 }
2958
2962 public int getNumProbes()
2963 {
2964 return Native.getNumProbes(nCtx());
2965 }
2966
2971 {
2972
2973 int n = getNumProbes();
2974 String[] res = new String[n];
2975 for (int i = 0; i < n; i++)
2976 res[i] = Native.getProbeName(nCtx(), i);
2977 return res;
2978 }
2979
2985 {
2986 return Native.probeGetDescr(nCtx(), name);
2987 }
2988
2992 public Probe mkProbe(String name)
2993 {
2994 return new Probe(this, name);
2995 }
2996
3000 public Probe constProbe(double val)
3001 {
3002 return new Probe(this, Native.probeConst(nCtx(), val));
3003 }
3004
3009 public Probe lt(Probe p1, Probe p2)
3010 {
3011 checkContextMatch(p1);
3012 checkContextMatch(p2);
3013 return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
3014 p2.getNativeObject()));
3015 }
3016
3021 public Probe gt(Probe p1, Probe p2)
3022 {
3023 checkContextMatch(p1);
3024 checkContextMatch(p2);
3025 return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
3026 p2.getNativeObject()));
3027 }
3028
3034 public Probe le(Probe p1, Probe p2)
3035 {
3036 checkContextMatch(p1);
3037 checkContextMatch(p2);
3038 return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
3039 p2.getNativeObject()));
3040 }
3041
3047 public Probe ge(Probe p1, Probe p2)
3048 {
3049 checkContextMatch(p1);
3050 checkContextMatch(p2);
3051 return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
3052 p2.getNativeObject()));
3053 }
3054
3059 public Probe eq(Probe p1, Probe p2)
3060 {
3061 checkContextMatch(p1);
3062 checkContextMatch(p2);
3063 return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
3064 p2.getNativeObject()));
3065 }
3066
3070 public Probe and(Probe p1, Probe p2)
3071 {
3072 checkContextMatch(p1);
3073 checkContextMatch(p2);
3074 return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
3075 p2.getNativeObject()));
3076 }
3077
3081 public Probe or(Probe p1, Probe p2)
3082 {
3083 checkContextMatch(p1);
3084 checkContextMatch(p2);
3085 return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
3086 p2.getNativeObject()));
3087 }
3088
3092 public Probe not(Probe p)
3093 {
3094 checkContextMatch(p);
3095 return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
3096 }
3097
3106 {
3107 return mkSolver((Symbol) null);
3108 }
3109
3117 public Solver mkSolver(Symbol logic)
3118 {
3119
3120 if (logic == null)
3121 return new Solver(this, Native.mkSolver(nCtx()));
3122 else
3123 return new Solver(this, Native.mkSolverForLogic(nCtx(),
3124 logic.getNativeObject()));
3125 }
3126
3131 public Solver mkSolver(String logic)
3132 {
3133 return mkSolver(mkSymbol(logic));
3134 }
3135
3140 {
3141 return new Solver(this, Native.mkSimpleSolver(nCtx()));
3142 }
3143
3151 {
3152
3153 return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3154 t.getNativeObject()));
3155 }
3156
3161 {
3162 return new Fixedpoint(this);
3163 }
3164
3169 {
3170 return new Optimize(this);
3171 }
3172
3173
3179 {
3180 return new FPRMSort(this);
3181 }
3182
3188 {
3189 return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3190 }
3191
3197 {
3198 return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3199 }
3200
3206 {
3207 return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3208 }
3209
3215 {
3216 return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3217 }
3218
3224 {
3225 return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3226 }
3227
3233 {
3234 return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3235 }
3236
3242 {
3243 return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3244 }
3245
3251 {
3252 return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3253 }
3254
3260 {
3261 return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3262 }
3263
3269 {
3270 return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3271 }
3272
3279 public FPSort mkFPSort(int ebits, int sbits)
3280 {
3281 return new FPSort(this, ebits, sbits);
3282 }
3283
3289 {
3290 return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3291 }
3292
3298 {
3299 return new FPSort(this, Native.mkFpaSort16(nCtx()));
3300 }
3301
3307 {
3308 return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3309 }
3310
3316 {
3317 return new FPSort(this, Native.mkFpaSort32(nCtx()));
3318 }
3319
3325 {
3326 return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3327 }
3328
3334 {
3335 return new FPSort(this, Native.mkFpaSort64(nCtx()));
3336 }
3337
3343 {
3344 return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3345 }
3346
3352 {
3353 return new FPSort(this, Native.mkFpaSort128(nCtx()));
3354 }
3355
3356
3363 {
3364 return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3365 }
3366
3373 public FPNum mkFPInf(FPSort s, boolean negative)
3374 {
3375 return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3376 }
3377
3384 public FPNum mkFPZero(FPSort s, boolean negative)
3385 {
3386 return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3387 }
3388
3395 public FPNum mkFPNumeral(float v, FPSort s)
3396 {
3397 return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3398 }
3399
3406 public FPNum mkFPNumeral(double v, FPSort s)
3407 {
3408 return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3409 }
3410
3417 public FPNum mkFPNumeral(int v, FPSort s)
3418 {
3419 return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3420 }
3421
3430 public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
3431 {
3432 return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3433 }
3434
3443 public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
3444 {
3445 return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3446 }
3447
3454 public FPNum mkFP(float v, FPSort s)
3455 {
3456 return mkFPNumeral(v, s);
3457 }
3458
3465 public FPNum mkFP(double v, FPSort s)
3466 {
3467 return mkFPNumeral(v, s);
3468 }
3469
3477 public FPNum mkFP(int v, FPSort s)
3478 {
3479 return mkFPNumeral(v, s);
3480 }
3481
3490 public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
3491 {
3492 return mkFPNumeral(sgn, exp, sig, s);
3493 }
3494
3503 public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
3504 {
3505 return mkFPNumeral(sgn, exp, sig, s);
3506 }
3507
3508
3515 {
3516 return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3517 }
3518
3525 {
3526 return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3527 }
3528
3537 {
3538 return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3539 }
3540
3549 {
3550 return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3551 }
3552
3561 {
3562 return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3563 }
3564
3573 {
3574 return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3575 }
3576
3588 {
3589 return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3590 }
3591
3599 {
3600 return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3601 }
3602
3610 {
3611 return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3612 }
3613
3622 {
3623 return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3624 }
3625
3633 {
3634 return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3635 }
3636
3644 {
3645 return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3646 }
3647
3655 {
3656 return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3657 }
3658
3666 {
3667 return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3668 }
3669
3677 {
3678 return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3679 }
3680
3688 {
3689 return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3690 }
3691
3701 {
3702 return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3703 }
3704
3711 {
3712 return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3713 }
3714
3721 {
3722 return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3723 }
3724
3731 {
3732 return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3733 }
3734
3741 {
3742 return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3743 }
3744
3751 {
3752 return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3753 }
3754
3761 {
3762 return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3763 }
3764
3771 {
3772 return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3773 }
3774
3789 {
3790 return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3791 }
3792
3805 {
3806 return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3807 }
3808
3821 {
3822 return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3823 }
3824
3837 {
3838 return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3839 }
3840
3854 public FPExpr mkFPToFP(Expr<FPRMSort> rm, Expr<BitVecSort> t, FPSort s, boolean signed)
3855 {
3856 if (signed)
3857 return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3858 else
3859 return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3860 }
3861
3873 {
3874 return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3875 }
3876
3889 public BitVecExpr mkFPToBV(Expr<FPRMSort> rm, Expr<FPSort> t, int sz, boolean signed)
3890 {
3891 if (signed)
3892 return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3893 else
3894 return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3895 }
3896
3907 {
3908 return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3909 }
3910
3922 {
3923 return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3924 }
3925
3940 {
3941 return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3942 }
3943
3944
3955 public AST wrapAST(long nativeObject)
3956 {
3957 return AST.create(this, nativeObject);
3958 }
3959
3972 public long unwrapAST(AST a)
3973 {
3974 return a.getNativeObject();
3975 }
3976
3982 {
3983 return Native.simplifyGetHelp(nCtx());
3984 }
3985
3990 {
3991 return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3992 }
3993
4002 public void updateParamValue(String id, String value)
4003 {
4004 Native.updateParamValue(nCtx(), id, value);
4005 }
4006
4007
4008 public long nCtx()
4009 {
4010 if (m_ctx == 0)
4011 throw new Z3Exception("Context closed");
4012 return m_ctx;
4013 }
4014
4015
4016 void checkContextMatch(Z3Object other)
4017 {
4018 if (this != other.getContext())
4019 throw new Z3Exception("Context mismatch");
4020 }
4021
4022 void checkContextMatch(Z3Object other1, Z3Object other2)
4023 {
4024 checkContextMatch(other1);
4025 checkContextMatch(other2);
4026 }
4027
4028 void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
4029 {
4030 checkContextMatch(other1);
4031 checkContextMatch(other2);
4032 checkContextMatch(other3);
4033 }
4034
4035 void checkContextMatch(Z3Object[] arr)
4036 {
4037 if (arr != null)
4038 for (Z3Object a : arr)
4039 checkContextMatch(a);
4040 }
4041
4042 private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
4043 private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
4044 private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
4045 private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
4046 private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
4047 private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
4048 private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
4049 private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
4050 private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
4051 private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
4052 private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
4053 private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
4054 private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
4055 private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
4056 private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
4057 private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
4058 private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
4059 private ConstructorListDecRefQueue m_ConstructorList_DRQ =
4060 new ConstructorListDecRefQueue();
4061
4063 return m_Constructor_DRQ;
4064 }
4065
4067 return m_ConstructorList_DRQ;
4068 }
4069
4071 {
4072 return m_AST_DRQ;
4073 }
4074
4076 {
4077 return m_ASTMap_DRQ;
4078 }
4079
4081 {
4082 return m_ASTVector_DRQ;
4083 }
4084
4086 {
4087 return m_ApplyResult_DRQ;
4088 }
4089
4091 {
4092 return m_FuncEntry_DRQ;
4093 }
4094
4096 {
4097 return m_FuncInterp_DRQ;
4098 }
4099
4101 {
4102 return m_Goal_DRQ;
4103 }
4104
4106 {
4107 return m_Model_DRQ;
4108 }
4109
4111 {
4112 return m_Params_DRQ;
4113 }
4114
4116 {
4117 return m_ParamDescrs_DRQ;
4118 }
4119
4121 {
4122 return m_Probe_DRQ;
4123 }
4124
4126 {
4127 return m_Solver_DRQ;
4128 }
4129
4131 {
4132 return m_Statistics_DRQ;
4133 }
4134
4136 {
4137 return m_Tactic_DRQ;
4138 }
4139
4141 {
4142 return m_Fixedpoint_DRQ;
4143 }
4144
4146 {
4147 return m_Optimize_DRQ;
4148 }
4149
4153 @Override
4154 public void close()
4155 {
4156 m_AST_DRQ.forceClear(this);
4157 m_ASTMap_DRQ.forceClear(this);
4158 m_ASTVector_DRQ.forceClear(this);
4159 m_ApplyResult_DRQ.forceClear(this);
4160 m_FuncEntry_DRQ.forceClear(this);
4161 m_FuncInterp_DRQ.forceClear(this);
4162 m_Goal_DRQ.forceClear(this);
4163 m_Model_DRQ.forceClear(this);
4164 m_Params_DRQ.forceClear(this);
4165 m_Probe_DRQ.forceClear(this);
4166 m_Solver_DRQ.forceClear(this);
4167 m_Optimize_DRQ.forceClear(this);
4168 m_Statistics_DRQ.forceClear(this);
4169 m_Tactic_DRQ.forceClear(this);
4170 m_Fixedpoint_DRQ.forceClear(this);
4171
4172 m_boolSort = null;
4173 m_intSort = null;
4174 m_realSort = null;
4175 m_stringSort = null;
4176
4177 synchronized (creation_lock) {
4178 Native.delContext(m_ctx);
4179 }
4180 m_ctx = 0;
4181 }
4182}
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
Probe ge(Probe p1, Probe p2)
Definition: Context.java:3047
Solver mkSolver(String logic)
Definition: Context.java:3131
Tactic repeat(Tactic t, int max)
Definition: Context.java:2861
BitVecExpr mkBVXOR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1067
final BoolExpr mkDistinct(Expr<?>... args)
Definition: Context.java:738
BitVecExpr mkBVUDiv(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1171
String getProbeDescription(String name)
Definition: Context.java:2984
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3503
final< D extends Sort > ArrayExpr< D, BoolSort > mkSetIntersection(Expr< ArraySort< D, BoolSort > >... args)
Definition: Context.java:1929
SeqExpr< BitVecSort > mkString(String s)
Definition: Context.java:2009
FPNum mkFPNaN(FPSort s)
Definition: Context.java:3362
BoolExpr mkFPIsPositive(Expr< FPSort > t)
Definition: Context.java:3770
BitVecExpr mkBVNOR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1093
FPExpr mkFPToFP(Expr< FPRMSort > rm, Expr< BitVecSort > t, FPSort s, boolean signed)
Definition: Context.java:3854
FPRMExpr mkFPRoundNearestTiesToEven()
Definition: Context.java:3187
Fixedpoint mkFixedpoint()
Definition: Context.java:3160
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2908
Tactic parOr(Tactic... t)
Definition: Context.java:2930
BoolExpr mkBVULE(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1278
BoolExpr mkBVSubNoOverflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1607
BoolExpr mkBVNegNoOverflow(Expr< BitVecSort > t)
Definition: Context.java:1649
Tactic then(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2798
FPExpr mkFPMax(Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3643
IntExpr mkBV2Int(Expr< BitVecSort > t, boolean signed)
Definition: Context.java:1567
FPSort mkFPSort(int ebits, int sbits)
Definition: Context.java:3279
BoolExpr mkBVSDivNoOverflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1635
Probe le(Probe p1, Probe p2)
Definition: Context.java:3034
AST wrapAST(long nativeObject)
Definition: Context.java:3955
SeqSort< BitVecSort > getStringSort()
Definition: Context.java:169
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:180
BitVecExpr mkBVXNOR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1106
BoolExpr mkImplies(Expr< BoolSort > t1, Expr< BoolSort > t2)
Definition: Context.java:784
BoolExpr mkBVAddNoOverflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
Definition: Context.java:1579
BitVecExpr mkBVRotateRight(int i, Expr< BitVecSort > t)
Definition: Context.java:1500
RealExpr mkInt2Real(Expr< IntSort > t)
Definition: Context.java:973
BitVecExpr mkBVLSHR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1455
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3430
FPNum mkFP(double v, FPSort s)
Definition: Context.java:3465
BoolExpr mkLe(Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
Definition: Context.java:933
IDecRefQueue< FuncInterp<?> > getFuncInterpDRQ()
Definition: Context.java:4095
IntExpr mkReal2Int(Expr< RealSort > t)
Definition: Context.java:986
FPNum mkFPInf(FPSort s, boolean negative)
Definition: Context.java:3373
FPExpr mkFPRoundToIntegral(Expr< FPRMSort > rm, Expr< FPSort > t)
Definition: Context.java:3621
BoolExpr mkAtLeast(Expr< BoolSort >[] args, int k)
Definition: Context.java:2263
BitVecExpr mkBVSMod(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1239
BitVecExpr mkInt2BV(int n, Expr< IntSort > t)
Definition: Context.java:1546
BoolExpr mkBVSGE(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1317
BitVecExpr mkBVConst(Symbol name, int size)
Definition: Context.java:675
BitVecExpr mkExtract(int high, int low, Expr< BitVecSort > t)
Definition: Context.java:1377
FPRMNum mkFPRoundTowardZero()
Definition: Context.java:3259
BoolExpr mkFPGEq(Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3676
Probe or(Probe p1, Probe p2)
Definition: Context.java:3081
IDecRefQueue< ASTMap > getASTMapDRQ()
Definition: Context.java:4075
BitVecExpr mkBVURem(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1207
final< D extends Sort, R1 extends Sort, R2 extends Sort > ArrayExpr< D, R2 > mkMap(FuncDecl< R2 > f, Expr< ArraySort< D, R1 > >... args)
Definition: Context.java:1827
Tactic cond(Probe p, Tactic t1, Tactic t2)
Definition: Context.java:2848
IDecRefQueue< Statistics > getStatisticsDRQ()
Definition: Context.java:4130
BoolExpr mkBVSGT(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1343
IDecRefQueue< Model > getModelDRQ()
Definition: Context.java:4105
BitVecExpr mkBVConst(String name, int size)
Definition: Context.java:683
IDecRefQueue< Optimize > getOptimizeDRQ()
Definition: Context.java:4145
IntNum mkInt(long v)
Definition: Context.java:2434
BoolExpr mkAtMost(Expr< BoolSort >[] args, int k)
Definition: Context.java:2254
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:4070
BoolExpr mkFPIsSubnormal(Expr< FPSort > t)
Definition: Context.java:3720
IntExpr mkMod(Expr< IntSort > t1, Expr< IntSort > t2)
Definition: Context.java:884
FPExpr mkFPToFP(Expr< FPRMSort > rm, RealExpr t, FPSort s)
Definition: Context.java:3836
BoolExpr mkNot(Expr< BoolSort > a)
Definition: Context.java:748
FPExpr mkFPSub(Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3548
BoolExpr mkBVMulNoOverflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
Definition: Context.java:1661
FPExpr mkFPSqrt(Expr< FPRMSort > rm, Expr< FPSort > t)
Definition: Context.java:3598
FPNum mkFPNumeral(int v, FPSort s)
Definition: Context.java:3417
FPExpr mkFPMul(Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3560
BitVecExpr mkConcat(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1361
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:4085
BitVecExpr mkSignExt(int i, Expr< BitVecSort > t)
Definition: Context.java:1392
BitVecExpr mkBVAdd(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1130
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3490
void updateParamValue(String id, String value)
Definition: Context.java:4002
BitVecExpr mkZeroExt(int i, Expr< BitVecSort > t)
Definition: Context.java:1406
final< R extends Sort > ReExpr< R > mkConcat(ReExpr< R >... t)
Definition: Context.java:2199
Tactic failIf(Probe p)
Definition: Context.java:2888
BoolExpr mkFPLt(Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3665
IntExpr stringToInt(Expr< SeqSort< BitVecSort > > e)
Definition: Context.java:2025
BitVecExpr mkBVRedAND(Expr< BitVecSort > t)
Definition: Context.java:1017
BitVecNum mkBV(long v, int size)
Definition: Context.java:2466
BitVecExpr mkBVSRem(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1225
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3395
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Definition: Context.java:4115
Tactic when(Probe p, Tactic t)
Definition: Context.java:2835
IntNum mkInt(String v)
Definition: Context.java:2408
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:4100
Probe mkProbe(String name)
Definition: Context.java:2992
BoolExpr mkPBLe(int[] coeffs, Expr< BoolSort >[] args, int k)
Definition: Context.java:2272
RealExpr mkRealConst(String name)
Definition: Context.java:667
final< R extends ArithSort > ArithExpr< R > mkAdd(Expr<? extends R >... t)
Definition: Context.java:829
ParamDescrs getSimplifyParameterDescriptions()
Definition: Context.java:3989
BitVecExpr mkBVRotateRight(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1528
SeqSort< BitVecSort > mkStringSort()
Definition: Context.java:242
Probe gt(Probe p1, Probe p2)
Definition: Context.java:3021
BoolExpr mkFPIsNaN(Expr< FPSort > t)
Definition: Context.java:3750
BoolExpr mkEq(Expr<?> x, Expr<?> y)
Definition: Context.java:726
Tactic with(Tactic t, Params p)
Definition: Context.java:2922
BitVecExpr mkBVASHR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1475
BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
Definition: Context.java:2663
String benchmarkToSMTString(String name, String logic, String status, String attributes, Expr< BoolSort >[] assumptions, Expr< BoolSort > formula)
Definition: Context.java:2644
FPRMNum mkFPRoundNearestTiesToAway()
Definition: Context.java:3205
BoolExpr mkBool(boolean value)
Definition: Context.java:718
BitVecExpr mkBVMul(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1156
BitVecExpr mkBVSub(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1143
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Definition: Context.java:267
BitVecExpr mkBVOR(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1054
BoolExpr mkLt(Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
Definition: Context.java:922
final Pattern mkPattern(Expr<?>... terms)
Definition: Context.java:570
BitVecExpr mkRepeat(int i, Expr< BitVecSort > t)
Definition: Context.java:1418
BoolExpr mkXor(Expr< BoolSort > t1, Expr< BoolSort > t2)
Definition: Context.java:795
FPRMNum mkFPRoundTowardNegative()
Definition: Context.java:3241
IDecRefQueue< Params > getParamsDRQ()
Definition: Context.java:4110
Probe eq(Probe p1, Probe p2)
Definition: Context.java:3059
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2496
BitVecExpr mkBVRotateLeft(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1513
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:4125
Quantifier mkQuantifier(boolean universal, Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2565
BitVecExpr mkBVRedOR(Expr< BitVecSort > t)
Definition: Context.java:1029
BoolExpr mkBVUGE(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1304
FPExpr mkFPDiv(Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3572
BitVecExpr mkBVNAND(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1080
FPExpr mkFPRem(Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3609
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2547
IntExpr mkIntConst(String name)
Definition: Context.java:651
Solver mkSolver(Tactic t)
Definition: Context.java:3150
BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
Definition: Context.java:2684
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2766
final< R extends Sort > Expr< R > mkApp(FuncDecl< R > f, Expr<?>... args)
Definition: Context.java:692
BoolExpr mkBVAddNoUnderflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1593
BoolExpr mkBVSubNoUnderflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2, boolean isSigned)
Definition: Context.java:1621
BoolExpr mkFPIsZero(Expr< FPSort > t)
Definition: Context.java:3730
IntExpr mkIntConst(Symbol name)
Definition: Context.java:643
IDecRefQueue< ConstructorList<?> > getConstructorListDRQ()
Definition: Context.java:4066
BitVecExpr mkBVNeg(Expr< BitVecSort > t)
Definition: Context.java:1119
Tactic mkTactic(String name)
Definition: Context.java:2757
SeqExpr< BitVecSort > intToString(Expr< IntSort > e)
Definition: Context.java:2017
BoolExpr mkBVSLE(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1291
FPNum mkFPNumeral(double v, FPSort s)
Definition: Context.java:3406
Tactic parAndThen(Tactic t1, Tactic t2)
Definition: Context.java:2941
RatNum mkReal(long v)
Definition: Context.java:2397
BoolExpr mkGt(Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
Definition: Context.java:944
BitVecNum mkBV(int v, int size)
Definition: Context.java:2456
Context(Map< String, String > settings)
Definition: Context.java:72
IDecRefQueue< FuncInterp.Entry<?> > getFuncEntryDRQ()
Definition: Context.java:4090
final< R extends Sort > ReExpr< R > mkIntersect(Expr< ReSort< R > >... t)
Definition: Context.java:2219
final< R extends ArithSort > ArithExpr< R > mkMul(Expr<? extends R >... t)
Definition: Context.java:840
BoolExpr mkBVMulNoUnderflow(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1675
BitVecExpr mkBVSDiv(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1192
FPRMSort mkFPRoundingModeSort()
Definition: Context.java:3178
RealExpr mkRealConst(Symbol name)
Definition: Context.java:659
String getTacticDescription(String name)
Definition: Context.java:2749
IDecRefQueue< Probe > getProbeDRQ()
Definition: Context.java:4120
Solver mkSolver(Symbol logic)
Definition: Context.java:3117
BoolExpr mkFPEq(Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3700
BoolExpr mkFPLEq(Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3654
RatNum mkReal(int num, int den)
Definition: Context.java:2356
BitVecSort mkBitVecSort(int size)
Definition: Context.java:213
FPExpr mkFPToFP(Expr< BitVecSort > bv, FPSort s)
Definition: Context.java:3804
BoolExpr mkBVSLT(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1265
BoolExpr mkFPGt(Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3687
BoolExpr mkIff(Expr< BoolSort > t1, Expr< BoolSort > t2)
Definition: Context.java:773
BoolExpr mkGe(Expr<? extends ArithSort > t1, Expr<? extends ArithSort > t2)
Definition: Context.java:955
BitVecExpr mkFPToFP(Expr< FPRMSort > rm, Expr< IntSort > exp, Expr< RealSort > sig, FPSort s)
Definition: Context.java:3939
BoolExpr mkIsInteger(Expr< RealSort > t)
Definition: Context.java:995
FPExpr mkFPToFP(Expr< FPRMSort > rm, FPExpr t, FPSort s)
Definition: Context.java:3820
Probe constProbe(double val)
Definition: Context.java:3000
BoolExpr mkFPIsNegative(Expr< FPSort > t)
Definition: Context.java:3760
BoolExpr mkBoolConst(String name)
Definition: Context.java:635
RealExpr mkFPToReal(Expr< FPSort > t)
Definition: Context.java:3906
Probe not(Probe p)
Definition: Context.java:3092
FPExpr mkFP(Expr< BitVecSort > sgn, Expr< BitVecSort > sig, Expr< BitVecSort > exp)
Definition: Context.java:3788
FPExpr mkFPToFP(FPSort s, Expr< FPRMSort > rm, Expr< FPSort > t)
Definition: Context.java:3872
FPExpr mkFPNeg(Expr< FPSort > t)
Definition: Context.java:3524
IDecRefQueue< Tactic > getTacticDRQ()
Definition: Context.java:4135
final< R extends Sort > SeqExpr< R > mkConcat(Expr< SeqSort< R > >... t)
Definition: Context.java:2034
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3443
RatNum mkReal(int v)
Definition: Context.java:2384
FPRMNum mkFPRoundTowardPositive()
Definition: Context.java:3223
Quantifier mkExists(Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2534
final< D extends Sort > ArrayExpr< D, BoolSort > mkSetUnion(Expr< ArraySort< D, BoolSort > >... args)
Definition: Context.java:1917
BoolExpr mkBVULT(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1252
BoolExpr mkFPIsNormal(Expr< FPSort > t)
Definition: Context.java:3710
DatatypeSort< Object >[] mkDatatypeSorts(String[] names, Constructor< Object >[][] c)
Definition: Context.java:413
Probe and(Probe p1, Probe p2)
Definition: Context.java:3070
Tactic tryFor(Tactic t, int ms)
Definition: Context.java:2822
FPExpr mkFPFMA(Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2, Expr< FPSort > t3)
Definition: Context.java:3587
UninterpretedSort mkUninterpretedSort(String str)
Definition: Context.java:189
void setPrintMode(Z3_ast_print_mode value)
Definition: Context.java:2626
DatatypeSort< Object >[] mkDatatypeSorts(Symbol[] names, Constructor< Object >[][] c)
Definition: Context.java:387
final BoolExpr mkAnd(Expr< BoolSort >... t)
Definition: Context.java:807
BitVecNum mkBV(String v, int size)
Definition: Context.java:2446
BitVecExpr mkBVRotateLeft(int i, Expr< BitVecSort > t)
Definition: Context.java:1488
Probe lt(Probe p1, Probe p2)
Definition: Context.java:3009
Quantifier mkForall(Expr<?>[] boundConstants, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2508
IntExpr mkRem(Expr< IntSort > t1, Expr< IntSort > t2)
Definition: Context.java:897
BitVecExpr mkBVNot(Expr< BitVecSort > t)
Definition: Context.java:1006
final< R extends ArithSort > ArithExpr< R > mkSub(Expr<? extends R >... t)
Definition: Context.java:851
BitVecExpr mkBVAND(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1041
FPExpr mkFPAbs(Expr< FPSort > t)
Definition: Context.java:3514
BoolExpr mkPBEq(int[] coeffs, Expr< BoolSort >[] args, int k)
Definition: Context.java:2290
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
Definition: Context.java:2711
IDecRefQueue< Constructor<?> > getConstructorDRQ()
Definition: Context.java:4062
FPExpr mkFPAdd(Expr< FPRMSort > rm, Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3536
BoolExpr mkBVUGT(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1330
FPNum mkFP(float v, FPSort s)
Definition: Context.java:3454
final BoolExpr mkOr(Expr< BoolSort >... t)
Definition: Context.java:818
BitVecExpr mkBVSHL(Expr< BitVecSort > t1, Expr< BitVecSort > t2)
Definition: Context.java:1436
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2521
BitVecExpr mkFPToIEEEBV(Expr< FPSort > t)
Definition: Context.java:3921
FPExpr mkFPMin(Expr< FPSort > t1, Expr< FPSort > t2)
Definition: Context.java:3632
Tactic orElse(Tactic t1, Tactic t2)
Definition: Context.java:2808
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4140
RatNum mkReal(String v)
Definition: Context.java:2371
FPNum mkFP(int v, FPSort s)
Definition: Context.java:3477
final< R extends Sort > ReExpr< R > mkUnion(Expr< ReSort< R > >... t)
Definition: Context.java:2209
IntSymbol mkSymbol(int i)
Definition: Context.java:94
StringSymbol mkSymbol(String name)
Definition: Context.java:102
FPNum mkFPZero(FPSort s, boolean negative)
Definition: Context.java:3384
BoolExpr mkFPIsInfinite(Expr< FPSort > t)
Definition: Context.java:3740
BoolExpr mkBoolConst(Symbol name)
Definition: Context.java:627
IDecRefQueue< ASTVector > getASTVectorDRQ()
Definition: Context.java:4080
BitVecExpr mkFPToBV(Expr< FPRMSort > rm, Expr< FPSort > t, int sz, boolean signed)
Definition: Context.java:3889
BoolExpr mkPBGe(int[] coeffs, Expr< BoolSort >[] args, int k)
Definition: Context.java:2281
Definition: FuncInterp.java:32
static< R extends Sort > Lambda< R > of(Context ctx, Sort[] sorts, Symbol[] names, Expr< R > body)
Definition: Lambda.java:94
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
static int arrayLength(Z3Object[] a)
Definition: Z3Object.java:83
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
expr max(expr const &a, expr const &b)
Definition: z3++.h:1836
def IntSort(ctx=None)
Definition: z3py.py:3100
def Lambda(vs, body)
Definition: z3py.py:2226
def RealSort(ctx=None)
Definition: z3py.py:3117
def BoolSort(ctx=None)
Definition: z3py.py:1655
def Map(f, *args)
Definition: z3py.py:4757
def String(name, ctx=None)
Definition: z3py.py:10693
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:9727
def TupleSort(name, sorts, ctx=None)
Definition: z3py.py:5293
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3967
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition: z3_api.h:1334