Z3
Context.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
20 import java.util.Map;
21 
23 
27 public class Context extends IDisposable
28 {
32  public Context()
33  {
34  super();
35  m_ctx = Native.mkContextRc(0);
36  initContext();
37  }
38 
56  public Context(Map<String, String> settings)
57  {
58  super();
59  long cfg = Native.mkConfig();
60  for (Map.Entry<String, String> kv : settings.entrySet())
61  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
62  m_ctx = Native.mkContextRc(cfg);
63  Native.delConfig(cfg);
64  initContext();
65  }
66 
72  public IntSymbol mkSymbol(int i)
73  {
74  return new IntSymbol(this, i);
75  }
76 
80  public StringSymbol mkSymbol(String name)
81  {
82  return new StringSymbol(this, name);
83  }
84 
88  Symbol[] mkSymbols(String[] names)
89  {
90  if (names == null)
91  return null;
92  Symbol[] result = new Symbol[names.length];
93  for (int i = 0; i < names.length; ++i)
94  result[i] = mkSymbol(names[i]);
95  return result;
96  }
97 
98  private BoolSort m_boolSort = null;
99  private IntSort m_intSort = null;
100  private RealSort m_realSort = null;
101 
106  {
107  if (m_boolSort == null)
108  m_boolSort = new BoolSort(this);
109  return m_boolSort;
110  }
111 
116  {
117  if (m_intSort == null)
118  m_intSort = new IntSort(this);
119  return m_intSort;
120  }
121 
126  {
127  if (m_realSort == null)
128  m_realSort = new RealSort(this);
129  return m_realSort;
130  }
131 
136  {
137  return new BoolSort(this);
138  }
139 
144  {
145  checkContextMatch(s);
146  return new UninterpretedSort(this, s);
147  }
148 
153  {
154  return mkUninterpretedSort(mkSymbol(str));
155  }
156 
161  {
162  return new IntSort(this);
163  }
164 
169  {
170  return new RealSort(this);
171  }
172 
176  public BitVecSort mkBitVecSort(int size)
177  {
178  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
179  }
180 
184  public ArraySort mkArraySort(Sort domain, Sort range)
185  {
186  checkContextMatch(domain);
187  checkContextMatch(range);
188  return new ArraySort(this, domain, range);
189  }
190 
194  public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames,
195  Sort[] fieldSorts)
196  {
197  checkContextMatch(name);
198  checkContextMatch(fieldNames);
199  checkContextMatch(fieldSorts);
200  return new TupleSort(this, name, (int) fieldNames.length, fieldNames,
201  fieldSorts);
202  }
203 
207  public EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
208 
209  {
210  checkContextMatch(name);
211  checkContextMatch(enumNames);
212  return new EnumSort(this, name, enumNames);
213  }
214 
218  public EnumSort mkEnumSort(String name, String... enumNames)
219 
220  {
221  return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
222  }
223 
227  public ListSort mkListSort(Symbol name, Sort elemSort)
228  {
229  checkContextMatch(name);
230  checkContextMatch(elemSort);
231  return new ListSort(this, name, elemSort);
232  }
233 
237  public ListSort mkListSort(String name, Sort elemSort)
238  {
239  checkContextMatch(elemSort);
240  return new ListSort(this, mkSymbol(name), elemSort);
241  }
242 
247 
248  {
249  checkContextMatch(name);
250  return new FiniteDomainSort(this, name, size);
251  }
252 
256  public FiniteDomainSort mkFiniteDomainSort(String name, long size)
257 
258  {
259  return new FiniteDomainSort(this, mkSymbol(name), size);
260  }
261 
273  public Constructor mkConstructor(Symbol name, Symbol recognizer,
274  Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
275 
276  {
277 
278  return new Constructor(this, name, recognizer, fieldNames, sorts,
279  sortRefs);
280  }
281 
292  public Constructor mkConstructor(String name, String recognizer,
293  String[] fieldNames, Sort[] sorts, int[] sortRefs)
294 
295  {
296 
297  return new Constructor(this, mkSymbol(name), mkSymbol(recognizer),
298  mkSymbols(fieldNames), sorts, sortRefs);
299  }
300 
304  public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
305 
306  {
307  checkContextMatch(name);
308  checkContextMatch(constructors);
309  return new DatatypeSort(this, name, constructors);
310  }
311 
315  public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
316 
317  {
318  checkContextMatch(constructors);
319  return new DatatypeSort(this, mkSymbol(name), constructors);
320  }
321 
328 
329  {
330  checkContextMatch(names);
331  int n = (int) names.length;
332  ConstructorList[] cla = new ConstructorList[n];
333  long[] n_constr = new long[n];
334  for (int i = 0; i < n; i++)
335  {
336  Constructor[] constructor = c[i];
337 
338  checkContextMatch(constructor);
339  cla[i] = new ConstructorList(this, constructor);
340  n_constr[i] = cla[i].getNativeObject();
341  }
342  long[] n_res = new long[n];
343  Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
344  n_constr);
345  DatatypeSort[] res = new DatatypeSort[n];
346  for (int i = 0; i < n; i++)
347  res[i] = new DatatypeSort(this, n_res[i]);
348  return res;
349  }
350 
358  public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
359 
360  {
361  return mkDatatypeSorts(mkSymbols(names), c);
362  }
363 
370  public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
371  throws Z3Exception
372  {
373  return Expr.create
374  (this,
376  (nCtx(), field.getNativeObject(),
377  t.getNativeObject(), v.getNativeObject()));
378  }
379 
380 
384  public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
385 
386  {
387  checkContextMatch(name);
388  checkContextMatch(domain);
389  checkContextMatch(range);
390  return new FuncDecl(this, name, domain, range);
391  }
392 
396  public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
397 
398  {
399  checkContextMatch(name);
400  checkContextMatch(domain);
401  checkContextMatch(range);
402  Sort[] q = new Sort[] { domain };
403  return new FuncDecl(this, name, q, range);
404  }
405 
409  public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
410 
411  {
412  checkContextMatch(domain);
413  checkContextMatch(range);
414  return new FuncDecl(this, mkSymbol(name), domain, range);
415  }
416 
420  public FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
421 
422  {
423  checkContextMatch(domain);
424  checkContextMatch(range);
425  Sort[] q = new Sort[] { domain };
426  return new FuncDecl(this, mkSymbol(name), q, range);
427  }
428 
435  public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
436 
437  {
438  checkContextMatch(domain);
439  checkContextMatch(range);
440  return new FuncDecl(this, prefix, domain, range);
441  }
442 
446  public FuncDecl mkConstDecl(Symbol name, Sort range)
447  {
448  checkContextMatch(name);
449  checkContextMatch(range);
450  return new FuncDecl(this, name, null, range);
451  }
452 
456  public FuncDecl mkConstDecl(String name, Sort range)
457  {
458  checkContextMatch(range);
459  return new FuncDecl(this, mkSymbol(name), null, range);
460  }
461 
468  public FuncDecl mkFreshConstDecl(String prefix, Sort range)
469 
470  {
471  checkContextMatch(range);
472  return new FuncDecl(this, prefix, null, range);
473  }
474 
480  public Expr mkBound(int index, Sort ty)
481  {
482  return Expr.create(this,
483  Native.mkBound(nCtx(), index, ty.getNativeObject()));
484  }
485 
489  public Pattern mkPattern(Expr... terms)
490  {
491  if (terms.length == 0)
492  throw new Z3Exception("Cannot create a pattern from zero terms");
493 
494  long[] termsNative = AST.arrayToNative(terms);
495  return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length,
496  termsNative));
497  }
498 
503  public Expr mkConst(Symbol name, Sort range)
504  {
505  checkContextMatch(name);
506  checkContextMatch(range);
507 
508  return Expr.create(
509  this,
510  Native.mkConst(nCtx(), name.getNativeObject(),
511  range.getNativeObject()));
512  }
513 
518  public Expr mkConst(String name, Sort range)
519  {
520  return mkConst(mkSymbol(name), range);
521  }
522 
527  public Expr mkFreshConst(String prefix, Sort range)
528  {
529  checkContextMatch(range);
530  return Expr.create(this,
531  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
532  }
533 
539  {
540  return mkApp(f, (Expr[]) null);
541  }
542 
547  {
548  return (BoolExpr) mkConst(name, getBoolSort());
549  }
550 
554  public BoolExpr mkBoolConst(String name)
555  {
556  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
557  }
558 
562  public IntExpr mkIntConst(Symbol name)
563  {
564  return (IntExpr) mkConst(name, getIntSort());
565  }
566 
570  public IntExpr mkIntConst(String name)
571  {
572  return (IntExpr) mkConst(name, getIntSort());
573  }
574 
579  {
580  return (RealExpr) mkConst(name, getRealSort());
581  }
582 
586  public RealExpr mkRealConst(String name)
587  {
588  return (RealExpr) mkConst(name, getRealSort());
589  }
590 
594  public BitVecExpr mkBVConst(Symbol name, int size)
595  {
596  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
597  }
598 
602  public BitVecExpr mkBVConst(String name, int size)
603  {
604  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
605  }
606 
610  public Expr mkApp(FuncDecl f, Expr... args)
611  {
612  checkContextMatch(f);
613  checkContextMatch(args);
614  return Expr.create(this, f, args);
615  }
616 
620  public BoolExpr mkTrue()
621  {
622  return new BoolExpr(this, Native.mkTrue(nCtx()));
623  }
624 
628  public BoolExpr mkFalse()
629  {
630  return new BoolExpr(this, Native.mkFalse(nCtx()));
631  }
632 
636  public BoolExpr mkBool(boolean value)
637  {
638  return value ? mkTrue() : mkFalse();
639  }
640 
644  public BoolExpr mkEq(Expr x, Expr y)
645  {
646  checkContextMatch(x);
647  checkContextMatch(y);
648  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
649  y.getNativeObject()));
650  }
651 
655  public BoolExpr mkDistinct(Expr... args)
656  {
657  checkContextMatch(args);
658  return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length,
659  AST.arrayToNative(args)));
660  }
661 
666  {
667  checkContextMatch(a);
668  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
669  }
670 
678  public Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
679  {
680  checkContextMatch(t1);
681  checkContextMatch(t2);
682  checkContextMatch(t3);
683  return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
684  t2.getNativeObject(), t3.getNativeObject()));
685  }
686 
691  {
692  checkContextMatch(t1);
693  checkContextMatch(t2);
694  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
695  t2.getNativeObject()));
696  }
697 
702  {
703  checkContextMatch(t1);
704  checkContextMatch(t2);
705  return new BoolExpr(this, Native.mkImplies(nCtx(),
706  t1.getNativeObject(), t2.getNativeObject()));
707  }
708 
713  {
714  checkContextMatch(t1);
715  checkContextMatch(t2);
716  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
717  t2.getNativeObject()));
718  }
719 
723  public BoolExpr mkAnd(BoolExpr... t)
724  {
725  checkContextMatch(t);
726  return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length,
727  AST.arrayToNative(t)));
728  }
729 
733  public BoolExpr mkOr(BoolExpr... t)
734  {
735  checkContextMatch(t);
736  return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length,
737  AST.arrayToNative(t)));
738  }
739 
743  public ArithExpr mkAdd(ArithExpr... t)
744  {
745  checkContextMatch(t);
746  return (ArithExpr) Expr.create(this,
747  Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t)));
748  }
749 
753  public ArithExpr mkMul(ArithExpr... t)
754  {
755  checkContextMatch(t);
756  return (ArithExpr) Expr.create(this,
757  Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t)));
758  }
759 
763  public ArithExpr mkSub(ArithExpr... t)
764  {
765  checkContextMatch(t);
766  return (ArithExpr) Expr.create(this,
767  Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t)));
768  }
769 
774  {
775  checkContextMatch(t);
776  return (ArithExpr) Expr.create(this,
777  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
778  }
779 
784  {
785  checkContextMatch(t1);
786  checkContextMatch(t2);
787  return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
788  t1.getNativeObject(), t2.getNativeObject()));
789  }
790 
796  public IntExpr mkMod(IntExpr t1, IntExpr t2)
797  {
798  checkContextMatch(t1);
799  checkContextMatch(t2);
800  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
801  t2.getNativeObject()));
802  }
803 
809  public IntExpr mkRem(IntExpr t1, IntExpr t2)
810  {
811  checkContextMatch(t1);
812  checkContextMatch(t2);
813  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
814  t2.getNativeObject()));
815  }
816 
821  {
822  checkContextMatch(t1);
823  checkContextMatch(t2);
824  return (ArithExpr) Expr.create(
825  this,
826  Native.mkPower(nCtx(), t1.getNativeObject(),
827  t2.getNativeObject()));
828  }
829 
834  {
835  checkContextMatch(t1);
836  checkContextMatch(t2);
837  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
838  t2.getNativeObject()));
839  }
840 
845  {
846  checkContextMatch(t1);
847  checkContextMatch(t2);
848  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
849  t2.getNativeObject()));
850  }
851 
856  {
857  checkContextMatch(t1);
858  checkContextMatch(t2);
859  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
860  t2.getNativeObject()));
861  }
862 
867  {
868  checkContextMatch(t1);
869  checkContextMatch(t2);
870  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
871  t2.getNativeObject()));
872  }
873 
885  {
886  checkContextMatch(t);
887  return new RealExpr(this,
888  Native.mkInt2real(nCtx(), t.getNativeObject()));
889  }
890 
898  {
899  checkContextMatch(t);
900  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
901  }
902 
907  {
908  checkContextMatch(t);
909  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
910  }
911 
918  {
919  checkContextMatch(t);
920  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
921  }
922 
929  {
930  checkContextMatch(t);
931  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
932  t.getNativeObject()));
933  }
934 
941  {
942  checkContextMatch(t);
943  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
944  t.getNativeObject()));
945  }
946 
953  {
954  checkContextMatch(t1);
955  checkContextMatch(t2);
956  return new BitVecExpr(this, Native.mkBvand(nCtx(),
957  t1.getNativeObject(), t2.getNativeObject()));
958  }
959 
966  {
967  checkContextMatch(t1);
968  checkContextMatch(t2);
969  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
970  t2.getNativeObject()));
971  }
972 
979  {
980  checkContextMatch(t1);
981  checkContextMatch(t2);
982  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
983  t1.getNativeObject(), t2.getNativeObject()));
984  }
985 
992  {
993  checkContextMatch(t1);
994  checkContextMatch(t2);
995  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
996  t1.getNativeObject(), t2.getNativeObject()));
997  }
998 
1005  {
1006  checkContextMatch(t1);
1007  checkContextMatch(t2);
1008  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1009  t1.getNativeObject(), t2.getNativeObject()));
1010  }
1011 
1018  {
1019  checkContextMatch(t1);
1020  checkContextMatch(t2);
1021  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1022  t1.getNativeObject(), t2.getNativeObject()));
1023  }
1024 
1031  {
1032  checkContextMatch(t);
1033  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1034  }
1035 
1042  {
1043  checkContextMatch(t1);
1044  checkContextMatch(t2);
1045  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1046  t1.getNativeObject(), t2.getNativeObject()));
1047  }
1048 
1055  {
1056  checkContextMatch(t1);
1057  checkContextMatch(t2);
1058  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1059  t1.getNativeObject(), t2.getNativeObject()));
1060  }
1061 
1068  {
1069  checkContextMatch(t1);
1070  checkContextMatch(t2);
1071  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1072  t1.getNativeObject(), t2.getNativeObject()));
1073  }
1074 
1083  {
1084  checkContextMatch(t1);
1085  checkContextMatch(t2);
1086  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1087  t1.getNativeObject(), t2.getNativeObject()));
1088  }
1089 
1104  {
1105  checkContextMatch(t1);
1106  checkContextMatch(t2);
1107  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1108  t1.getNativeObject(), t2.getNativeObject()));
1109  }
1110 
1119  {
1120  checkContextMatch(t1);
1121  checkContextMatch(t2);
1122  return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1123  t1.getNativeObject(), t2.getNativeObject()));
1124  }
1125 
1137  {
1138  checkContextMatch(t1);
1139  checkContextMatch(t2);
1140  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1141  t1.getNativeObject(), t2.getNativeObject()));
1142  }
1143 
1151  {
1152  checkContextMatch(t1);
1153  checkContextMatch(t2);
1154  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1155  t1.getNativeObject(), t2.getNativeObject()));
1156  }
1157 
1164  {
1165  checkContextMatch(t1);
1166  checkContextMatch(t2);
1167  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1168  t2.getNativeObject()));
1169  }
1170 
1177  {
1178  checkContextMatch(t1);
1179  checkContextMatch(t2);
1180  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1181  t2.getNativeObject()));
1182  }
1183 
1190  {
1191  checkContextMatch(t1);
1192  checkContextMatch(t2);
1193  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1194  t2.getNativeObject()));
1195  }
1196 
1203  {
1204  checkContextMatch(t1);
1205  checkContextMatch(t2);
1206  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1207  t2.getNativeObject()));
1208  }
1209 
1216  {
1217  checkContextMatch(t1);
1218  checkContextMatch(t2);
1219  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1220  t2.getNativeObject()));
1221  }
1222 
1229  {
1230  checkContextMatch(t1);
1231  checkContextMatch(t2);
1232  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1233  t2.getNativeObject()));
1234  }
1235 
1242  {
1243  checkContextMatch(t1);
1244  checkContextMatch(t2);
1245  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1246  t2.getNativeObject()));
1247  }
1248 
1255  {
1256  checkContextMatch(t1);
1257  checkContextMatch(t2);
1258  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1259  t2.getNativeObject()));
1260  }
1261 
1273  {
1274  checkContextMatch(t1);
1275  checkContextMatch(t2);
1276  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1277  t1.getNativeObject(), t2.getNativeObject()));
1278  }
1279 
1288  public BitVecExpr mkExtract(int high, int low, BitVecExpr t)
1289 
1290  {
1291  checkContextMatch(t);
1292  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1293  t.getNativeObject()));
1294  }
1295 
1304  {
1305  checkContextMatch(t);
1306  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1307  t.getNativeObject()));
1308  }
1309 
1318  {
1319  checkContextMatch(t);
1320  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1321  t.getNativeObject()));
1322  }
1323 
1329  public BitVecExpr mkRepeat(int i, BitVecExpr t)
1330  {
1331  checkContextMatch(t);
1332  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1333  t.getNativeObject()));
1334  }
1335 
1348  {
1349  checkContextMatch(t1);
1350  checkContextMatch(t2);
1351  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1352  t1.getNativeObject(), t2.getNativeObject()));
1353  }
1354 
1367  {
1368  checkContextMatch(t1);
1369  checkContextMatch(t2);
1370  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1371  t1.getNativeObject(), t2.getNativeObject()));
1372  }
1373 
1387  {
1388  checkContextMatch(t1);
1389  checkContextMatch(t2);
1390  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1391  t1.getNativeObject(), t2.getNativeObject()));
1392  }
1393 
1400  {
1401  checkContextMatch(t);
1402  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1403  t.getNativeObject()));
1404  }
1405 
1412  {
1413  checkContextMatch(t);
1414  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1415  t.getNativeObject()));
1416  }
1417 
1425 
1426  {
1427  checkContextMatch(t1);
1428  checkContextMatch(t2);
1429  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1430  t1.getNativeObject(), t2.getNativeObject()));
1431  }
1432 
1440 
1441  {
1442  checkContextMatch(t1);
1443  checkContextMatch(t2);
1444  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1445  t1.getNativeObject(), t2.getNativeObject()));
1446  }
1447 
1457  public BitVecExpr mkInt2BV(int n, IntExpr t)
1458  {
1459  checkContextMatch(t);
1460  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1461  t.getNativeObject()));
1462  }
1463 
1478  public IntExpr mkBV2Int(BitVecExpr t, boolean signed)
1479  {
1480  checkContextMatch(t);
1481  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1482  (signed) ? true : false));
1483  }
1484 
1491  boolean isSigned)
1492  {
1493  checkContextMatch(t1);
1494  checkContextMatch(t2);
1495  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1496  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1497  : false));
1498  }
1499 
1506 
1507  {
1508  checkContextMatch(t1);
1509  checkContextMatch(t2);
1510  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1511  t1.getNativeObject(), t2.getNativeObject()));
1512  }
1513 
1520 
1521  {
1522  checkContextMatch(t1);
1523  checkContextMatch(t2);
1524  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1525  t1.getNativeObject(), t2.getNativeObject()));
1526  }
1527 
1534  boolean isSigned)
1535  {
1536  checkContextMatch(t1);
1537  checkContextMatch(t2);
1538  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1539  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1540  : false));
1541  }
1542 
1549 
1550  {
1551  checkContextMatch(t1);
1552  checkContextMatch(t2);
1553  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1554  t1.getNativeObject(), t2.getNativeObject()));
1555  }
1556 
1563  {
1564  checkContextMatch(t);
1565  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1566  t.getNativeObject()));
1567  }
1568 
1575  boolean isSigned)
1576  {
1577  checkContextMatch(t1);
1578  checkContextMatch(t2);
1579  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1580  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1581  : false));
1582  }
1583 
1590 
1591  {
1592  checkContextMatch(t1);
1593  checkContextMatch(t2);
1594  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1595  t1.getNativeObject(), t2.getNativeObject()));
1596  }
1597 
1601  public ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
1602 
1603  {
1604  return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1605  }
1606 
1610  public ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
1611 
1612  {
1613  return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1614  }
1615 
1630  {
1631  checkContextMatch(a);
1632  checkContextMatch(i);
1633  return Expr.create(
1634  this,
1635  Native.mkSelect(nCtx(), a.getNativeObject(),
1636  i.getNativeObject()));
1637  }
1638 
1656  {
1657  checkContextMatch(a);
1658  checkContextMatch(i);
1659  checkContextMatch(v);
1660  return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1661  i.getNativeObject(), v.getNativeObject()));
1662  }
1663 
1673  public ArrayExpr mkConstArray(Sort domain, Expr v)
1674  {
1675  checkContextMatch(domain);
1676  checkContextMatch(v);
1677  return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1678  domain.getNativeObject(), v.getNativeObject()));
1679  }
1680 
1694  public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
1695  {
1696  checkContextMatch(f);
1697  checkContextMatch(args);
1698  return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1699  f.getNativeObject(), AST.arrayLength(args),
1700  AST.arrayToNative(args)));
1701  }
1702 
1710  {
1711  checkContextMatch(array);
1712  return Expr.create(this,
1713  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1714  }
1715 
1720  {
1721  checkContextMatch(ty);
1722  return new SetSort(this, ty);
1723  }
1724 
1728  public ArrayExpr mkEmptySet(Sort domain)
1729  {
1730  checkContextMatch(domain);
1731  return (ArrayExpr)Expr.create(this,
1732  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1733  }
1734 
1738  public ArrayExpr mkFullSet(Sort domain)
1739  {
1740  checkContextMatch(domain);
1741  return (ArrayExpr)Expr.create(this,
1742  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1743  }
1744 
1748  public ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
1749  {
1750  checkContextMatch(set);
1751  checkContextMatch(element);
1752  return (ArrayExpr)Expr.create(this,
1753  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1754  element.getNativeObject()));
1755  }
1756 
1760  public ArrayExpr mkSetDel(ArrayExpr set, Expr element)
1761  {
1762  checkContextMatch(set);
1763  checkContextMatch(element);
1764  return (ArrayExpr)Expr.create(this,
1765  Native.mkSetDel(nCtx(), set.getNativeObject(),
1766  element.getNativeObject()));
1767  }
1768 
1773  {
1774  checkContextMatch(args);
1775  return (ArrayExpr)Expr.create(this,
1776  Native.mkSetUnion(nCtx(), (int) args.length,
1777  AST.arrayToNative(args)));
1778  }
1779 
1784  {
1785  checkContextMatch(args);
1786  return (ArrayExpr)Expr.create(this,
1787  Native.mkSetIntersect(nCtx(), (int) args.length,
1788  AST.arrayToNative(args)));
1789  }
1790 
1795  {
1796  checkContextMatch(arg1);
1797  checkContextMatch(arg2);
1798  return (ArrayExpr)Expr.create(this,
1799  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1800  arg2.getNativeObject()));
1801  }
1802 
1807  {
1808  checkContextMatch(arg);
1809  return (ArrayExpr)Expr.create(this,
1810  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1811  }
1812 
1817  {
1818  checkContextMatch(elem);
1819  checkContextMatch(set);
1820  return (BoolExpr) Expr.create(this,
1821  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1822  set.getNativeObject()));
1823  }
1824 
1829  {
1830  checkContextMatch(arg1);
1831  checkContextMatch(arg2);
1832  return (BoolExpr) Expr.create(this,
1833  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1834  arg2.getNativeObject()));
1835  }
1836 
1848  public Expr mkNumeral(String v, Sort ty)
1849  {
1850  checkContextMatch(ty);
1851  return Expr.create(this,
1852  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
1853  }
1854 
1865  public Expr mkNumeral(int v, Sort ty)
1866  {
1867  checkContextMatch(ty);
1868  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
1869  }
1870 
1881  public Expr mkNumeral(long v, Sort ty)
1882  {
1883  checkContextMatch(ty);
1884  return Expr.create(this,
1885  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
1886  }
1887 
1897  public RatNum mkReal(int num, int den)
1898  {
1899  if (den == 0)
1900  throw new Z3Exception("Denominator is zero");
1901 
1902  return new RatNum(this, Native.mkReal(nCtx(), num, den));
1903  }
1904 
1911  public RatNum mkReal(String v)
1912  {
1913 
1914  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
1915  .getNativeObject()));
1916  }
1917 
1924  public RatNum mkReal(int v)
1925  {
1926 
1927  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
1928  .getNativeObject()));
1929  }
1930 
1937  public RatNum mkReal(long v)
1938  {
1939 
1940  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
1941  .getNativeObject()));
1942  }
1943 
1948  public IntNum mkInt(String v)
1949  {
1950 
1951  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
1952  .getNativeObject()));
1953  }
1954 
1961  public IntNum mkInt(int v)
1962  {
1963 
1964  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
1965  .getNativeObject()));
1966  }
1967 
1974  public IntNum mkInt(long v)
1975  {
1976 
1977  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
1978  .getNativeObject()));
1979  }
1980 
1986  public BitVecNum mkBV(String v, int size)
1987  {
1988  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
1989  }
1990 
1996  public BitVecNum mkBV(int v, int size)
1997  {
1998  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
1999  }
2000 
2006  public BitVecNum mkBV(long v, int size)
2007  {
2008  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2009  }
2010 
2030  public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
2031  int weight, Pattern[] patterns, Expr[] noPatterns,
2032  Symbol quantifierID, Symbol skolemID)
2033  {
2034 
2035  return new Quantifier(this, true, sorts, names, body, weight, patterns,
2036  noPatterns, quantifierID, skolemID);
2037  }
2038 
2042  public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
2043  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2044  Symbol skolemID)
2045  {
2046 
2047  return new Quantifier(this, true, boundConstants, body, weight,
2048  patterns, noPatterns, quantifierID, skolemID);
2049  }
2050 
2055  public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
2056  int weight, Pattern[] patterns, Expr[] noPatterns,
2057  Symbol quantifierID, Symbol skolemID)
2058  {
2059 
2060  return new Quantifier(this, false, sorts, names, body, weight,
2061  patterns, noPatterns, quantifierID, skolemID);
2062  }
2063 
2067  public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
2068  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2069  Symbol skolemID)
2070  {
2071 
2072  return new Quantifier(this, false, boundConstants, body, weight,
2073  patterns, noPatterns, quantifierID, skolemID);
2074  }
2075 
2079  public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
2080  Symbol[] names, Expr body, int weight, Pattern[] patterns,
2081  Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
2082 
2083  {
2084 
2085  if (universal)
2086  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2087  quantifierID, skolemID);
2088  else
2089  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2090  quantifierID, skolemID);
2091  }
2092 
2096  public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
2097  Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
2098  Symbol quantifierID, Symbol skolemID)
2099  {
2100 
2101  if (universal)
2102  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2103  quantifierID, skolemID);
2104  else
2105  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2106  quantifierID, skolemID);
2107  }
2108 
2123  public void setPrintMode(Z3_ast_print_mode value)
2124  {
2125  Native.setAstPrintMode(nCtx(), value.toInt());
2126  }
2127 
2141  public String benchmarkToSMTString(String name, String logic,
2142  String status, String attributes, BoolExpr[] assumptions,
2143  BoolExpr formula)
2144  {
2145 
2146  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2147  attributes, (int) assumptions.length,
2148  AST.arrayToNative(assumptions), formula.getNativeObject());
2149  }
2150 
2160  public void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts,
2161  Symbol[] declNames, FuncDecl[] decls)
2162  {
2163  int csn = Symbol.arrayLength(sortNames);
2164  int cs = Sort.arrayLength(sorts);
2165  int cdn = Symbol.arrayLength(declNames);
2166  int cd = AST.arrayLength(decls);
2167  if (csn != cs || cdn != cd)
2168  throw new Z3Exception("Argument size mismatch");
2169  Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
2170  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2171  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2172  AST.arrayToNative(decls));
2173  }
2174 
2179  public void parseSMTLIBFile(String fileName, Symbol[] sortNames,
2180  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2181 
2182  {
2183  int csn = Symbol.arrayLength(sortNames);
2184  int cs = Sort.arrayLength(sorts);
2185  int cdn = Symbol.arrayLength(declNames);
2186  int cd = AST.arrayLength(decls);
2187  if (csn != cs || cdn != cd)
2188  throw new Z3Exception("Argument size mismatch");
2189  Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
2190  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2191  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2192  AST.arrayToNative(decls));
2193  }
2194 
2200  {
2201  return Native.getSmtlibNumFormulas(nCtx());
2202  }
2203 
2209  {
2210 
2211  int n = getNumSMTLIBFormulas();
2212  BoolExpr[] res = new BoolExpr[n];
2213  for (int i = 0; i < n; i++)
2214  res[i] = (BoolExpr) Expr.create(this,
2215  Native.getSmtlibFormula(nCtx(), i));
2216  return res;
2217  }
2218 
2224  {
2225  return Native.getSmtlibNumAssumptions(nCtx());
2226  }
2227 
2233  {
2234 
2235  int n = getNumSMTLIBAssumptions();
2236  BoolExpr[] res = new BoolExpr[n];
2237  for (int i = 0; i < n; i++)
2238  res[i] = (BoolExpr) Expr.create(this,
2239  Native.getSmtlibAssumption(nCtx(), i));
2240  return res;
2241  }
2242 
2247  public int getNumSMTLIBDecls()
2248  {
2249  return Native.getSmtlibNumDecls(nCtx());
2250  }
2251 
2257  {
2258 
2259  int n = getNumSMTLIBDecls();
2260  FuncDecl[] res = new FuncDecl[n];
2261  for (int i = 0; i < n; i++)
2262  res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
2263  return res;
2264  }
2265 
2270  public int getNumSMTLIBSorts()
2271  {
2272  return Native.getSmtlibNumSorts(nCtx());
2273  }
2274 
2280  {
2281 
2282  int n = getNumSMTLIBSorts();
2283  Sort[] res = new Sort[n];
2284  for (int i = 0; i < n; i++)
2285  res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
2286  return res;
2287  }
2288 
2296  public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
2297  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2298 
2299  {
2300 
2301  int csn = Symbol.arrayLength(sortNames);
2302  int cs = Sort.arrayLength(sorts);
2303  int cdn = Symbol.arrayLength(declNames);
2304  int cd = AST.arrayLength(decls);
2305  if (csn != cs || cdn != cd)
2306  throw new Z3Exception("Argument size mismatch");
2307  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2308  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2309  AST.arrayToNative(sorts), AST.arrayLength(decls),
2310  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2311  }
2312 
2317  public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
2318  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2319 
2320  {
2321 
2322  int csn = Symbol.arrayLength(sortNames);
2323  int cs = Sort.arrayLength(sorts);
2324  int cdn = Symbol.arrayLength(declNames);
2325  int cd = AST.arrayLength(decls);
2326  if (csn != cs || cdn != cd)
2327  throw new Z3Exception("Argument size mismatch");
2328  return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
2329  fileName, AST.arrayLength(sorts),
2330  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2331  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2332  AST.arrayToNative(decls)));
2333  }
2334 
2345  public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
2346 
2347  {
2348  return new Goal(this, models, unsatCores, proofs);
2349  }
2350 
2354  public Params mkParams()
2355  {
2356  return new Params(this);
2357  }
2358 
2362  public int getNumTactics()
2363  {
2364  return Native.getNumTactics(nCtx());
2365  }
2366 
2370  public String[] getTacticNames()
2371  {
2372 
2373  int n = getNumTactics();
2374  String[] res = new String[n];
2375  for (int i = 0; i < n; i++)
2376  res[i] = Native.getTacticName(nCtx(), i);
2377  return res;
2378  }
2379 
2384  public String getTacticDescription(String name)
2385  {
2386  return Native.tacticGetDescr(nCtx(), name);
2387  }
2388 
2392  public Tactic mkTactic(String name)
2393  {
2394  return new Tactic(this, name);
2395  }
2396 
2401  public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
2402 
2403  {
2404  checkContextMatch(t1);
2405  checkContextMatch(t2);
2406  checkContextMatch(ts);
2407 
2408  long last = 0;
2409  if (ts != null && ts.length > 0)
2410  {
2411  last = ts[ts.length - 1].getNativeObject();
2412  for (int i = ts.length - 2; i >= 0; i--)
2413  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2414  last);
2415  }
2416  if (last != 0)
2417  {
2418  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2419  return new Tactic(this, Native.tacticAndThen(nCtx(),
2420  t1.getNativeObject(), last));
2421  } else
2422  return new Tactic(this, Native.tacticAndThen(nCtx(),
2423  t1.getNativeObject(), t2.getNativeObject()));
2424  }
2425 
2432  public Tactic then(Tactic t1, Tactic t2, Tactic... ts)
2433  {
2434  return andThen(t1, t2, ts);
2435  }
2436 
2442  public Tactic orElse(Tactic t1, Tactic t2)
2443  {
2444  checkContextMatch(t1);
2445  checkContextMatch(t2);
2446  return new Tactic(this, Native.tacticOrElse(nCtx(),
2447  t1.getNativeObject(), t2.getNativeObject()));
2448  }
2449 
2456  public Tactic tryFor(Tactic t, int ms)
2457  {
2458  checkContextMatch(t);
2459  return new Tactic(this, Native.tacticTryFor(nCtx(),
2460  t.getNativeObject(), ms));
2461  }
2462 
2469  public Tactic when(Probe p, Tactic t)
2470  {
2471  checkContextMatch(t);
2472  checkContextMatch(p);
2473  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2474  t.getNativeObject()));
2475  }
2476 
2482  public Tactic cond(Probe p, Tactic t1, Tactic t2)
2483  {
2484  checkContextMatch(p);
2485  checkContextMatch(t1);
2486  checkContextMatch(t2);
2487  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2488  t1.getNativeObject(), t2.getNativeObject()));
2489  }
2490 
2495  public Tactic repeat(Tactic t, int max)
2496  {
2497  checkContextMatch(t);
2498  return new Tactic(this, Native.tacticRepeat(nCtx(),
2499  t.getNativeObject(), max));
2500  }
2501 
2505  public Tactic skip()
2506  {
2507  return new Tactic(this, Native.tacticSkip(nCtx()));
2508  }
2509 
2513  public Tactic fail()
2514  {
2515  return new Tactic(this, Native.tacticFail(nCtx()));
2516  }
2517 
2522  public Tactic failIf(Probe p)
2523  {
2524  checkContextMatch(p);
2525  return new Tactic(this,
2526  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2527  }
2528 
2534  {
2535  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2536  }
2537 
2543  {
2544  checkContextMatch(t);
2545  checkContextMatch(p);
2546  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2547  t.getNativeObject(), p.getNativeObject()));
2548  }
2549 
2556  public Tactic with(Tactic t, Params p)
2557  {
2558  return usingParams(t, p);
2559  }
2560 
2564  public Tactic parOr(Tactic... t)
2565  {
2566  checkContextMatch(t);
2567  return new Tactic(this, Native.tacticParOr(nCtx(),
2568  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2569  }
2570 
2576  {
2577  checkContextMatch(t1);
2578  checkContextMatch(t2);
2579  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2580  t1.getNativeObject(), t2.getNativeObject()));
2581  }
2582 
2588  public void interrupt()
2589  {
2590  Native.interrupt(nCtx());
2591  }
2592 
2596  public int getNumProbes()
2597  {
2598  return Native.getNumProbes(nCtx());
2599  }
2600 
2604  public String[] getProbeNames()
2605  {
2606 
2607  int n = getNumProbes();
2608  String[] res = new String[n];
2609  for (int i = 0; i < n; i++)
2610  res[i] = Native.getProbeName(nCtx(), i);
2611  return res;
2612  }
2613 
2618  public String getProbeDescription(String name)
2619  {
2620  return Native.probeGetDescr(nCtx(), name);
2621  }
2622 
2626  public Probe mkProbe(String name)
2627  {
2628  return new Probe(this, name);
2629  }
2630 
2634  public Probe constProbe(double val)
2635  {
2636  return new Probe(this, Native.probeConst(nCtx(), val));
2637  }
2638 
2643  public Probe lt(Probe p1, Probe p2)
2644  {
2645  checkContextMatch(p1);
2646  checkContextMatch(p2);
2647  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2648  p2.getNativeObject()));
2649  }
2650 
2655  public Probe gt(Probe p1, Probe p2)
2656  {
2657  checkContextMatch(p1);
2658  checkContextMatch(p2);
2659  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2660  p2.getNativeObject()));
2661  }
2662 
2668  public Probe le(Probe p1, Probe p2)
2669  {
2670  checkContextMatch(p1);
2671  checkContextMatch(p2);
2672  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2673  p2.getNativeObject()));
2674  }
2675 
2681  public Probe ge(Probe p1, Probe p2)
2682  {
2683  checkContextMatch(p1);
2684  checkContextMatch(p2);
2685  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2686  p2.getNativeObject()));
2687  }
2688 
2693  public Probe eq(Probe p1, Probe p2)
2694  {
2695  checkContextMatch(p1);
2696  checkContextMatch(p2);
2697  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2698  p2.getNativeObject()));
2699  }
2700 
2704  public Probe and(Probe p1, Probe p2)
2705  {
2706  checkContextMatch(p1);
2707  checkContextMatch(p2);
2708  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
2709  p2.getNativeObject()));
2710  }
2711 
2715  public Probe or(Probe p1, Probe p2)
2716  {
2717  checkContextMatch(p1);
2718  checkContextMatch(p2);
2719  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
2720  p2.getNativeObject()));
2721  }
2722 
2726  public Probe not(Probe p)
2727  {
2728  checkContextMatch(p);
2729  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2730  }
2731 
2739  public Solver mkSolver()
2740  {
2741  return mkSolver((Symbol) null);
2742  }
2743 
2751  public Solver mkSolver(Symbol logic)
2752  {
2753 
2754  if (logic == null)
2755  return new Solver(this, Native.mkSolver(nCtx()));
2756  else
2757  return new Solver(this, Native.mkSolverForLogic(nCtx(),
2758  logic.getNativeObject()));
2759  }
2760 
2765  public Solver mkSolver(String logic)
2766  {
2767  return mkSolver(mkSymbol(logic));
2768  }
2769 
2774  {
2775  return new Solver(this, Native.mkSimpleSolver(nCtx()));
2776  }
2777 
2785  {
2786 
2787  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
2788  t.getNativeObject()));
2789  }
2790 
2795  {
2796  return new Fixedpoint(this);
2797  }
2798 
2803  {
2804  return new Optimize(this);
2805  }
2806 
2807 
2813  {
2814  return new FPRMSort(this);
2815  }
2816 
2822  {
2823  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
2824  }
2825 
2830  public FPRMNum mkFPRNE()
2831  {
2832  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
2833  }
2834 
2840  {
2841  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
2842  }
2843 
2848  public FPRMNum mkFPRNA()
2849  {
2850  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
2851  }
2852 
2858  {
2859  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
2860  }
2861 
2866  public FPRMNum mkFPRTP()
2867  {
2868  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
2869  }
2870 
2876  {
2877  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
2878  }
2879 
2884  public FPRMNum mkFPRTN()
2885  {
2886  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
2887  }
2888 
2894  {
2895  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
2896  }
2897 
2902  public FPRMNum mkFPRTZ()
2903  {
2904  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
2905  }
2906 
2913  public FPSort mkFPSort(int ebits, int sbits)
2914  {
2915  return new FPSort(this, ebits, sbits);
2916  }
2917 
2923  {
2924  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
2925  }
2926 
2932  {
2933  return new FPSort(this, Native.mkFpaSort16(nCtx()));
2934  }
2935 
2941  {
2942  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
2943  }
2944 
2950  {
2951  return new FPSort(this, Native.mkFpaSort32(nCtx()));
2952  }
2953 
2959  {
2960  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
2961  }
2962 
2968  {
2969  return new FPSort(this, Native.mkFpaSort64(nCtx()));
2970  }
2971 
2977  {
2978  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
2979  }
2980 
2986  {
2987  return new FPSort(this, Native.mkFpaSort128(nCtx()));
2988  }
2989 
2990 
2997  {
2998  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
2999  }
3000 
3007  public FPNum mkFPInf(FPSort s, boolean negative)
3008  {
3009  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3010  }
3011 
3018  public FPNum mkFPZero(FPSort s, boolean negative)
3019  {
3020  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3021  }
3022 
3029  public FPNum mkFPNumeral(float v, FPSort s)
3030  {
3031  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3032  }
3033 
3040  public FPNum mkFPNumeral(double v, FPSort s)
3041  {
3042  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3043  }
3044 
3051  public FPNum mkFPNumeral(int v, FPSort s)
3052  {
3053  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3054  }
3055 
3064  public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
3065  {
3066  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3067  }
3068 
3077  public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
3078  {
3079  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3080  }
3081 
3088  public FPNum mkFP(float v, FPSort s)
3089  {
3090  return mkFPNumeral(v, s);
3091  }
3092 
3099  public FPNum mkFP(double v, FPSort s)
3100  {
3101  return mkFPNumeral(v, s);
3102  }
3103 
3111  public FPNum mkFP(int v, FPSort s)
3112  {
3113  return mkFPNumeral(v, s);
3114  }
3115 
3124  public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
3125  {
3126  return mkFPNumeral(sgn, sig, exp, s);
3127  }
3128 
3137  public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
3138  {
3139  return mkFPNumeral(sgn, sig, exp, s);
3140  }
3141 
3142 
3148  public FPExpr mkFPAbs(FPExpr t)
3149  {
3150  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3151  }
3152 
3158  public FPExpr mkFPNeg(FPExpr t)
3159  {
3160  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3161  }
3162 
3170  public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
3171  {
3172  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3173  }
3174 
3182  public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
3183  {
3184  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3185  }
3186 
3194  public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
3195  {
3196  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3197  }
3198 
3206  public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
3207  {
3208  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3209  }
3210 
3221  public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
3222  {
3223  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3224  }
3225 
3233  {
3234  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3235  }
3236 
3243  public FPExpr mkFPRem(FPExpr t1, FPExpr t2)
3244  {
3245  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3246  }
3247 
3256  {
3257  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3258  }
3259 
3266  public FPExpr mkFPMin(FPExpr t1, FPExpr t2)
3267  {
3268  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3269  }
3270 
3277  public FPExpr mkFPMax(FPExpr t1, FPExpr t2)
3278  {
3279  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3280  }
3281 
3288  public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
3289  {
3290  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3291  }
3292 
3299  public BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
3300  {
3301  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3302  }
3303 
3310  public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
3311  {
3312  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3313  }
3314 
3321  public BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
3322  {
3323  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3324  }
3325 
3334  public BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
3335  {
3336  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3337  }
3338 
3345  {
3346  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3347  }
3348 
3355  {
3356  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3357  }
3358 
3365  {
3366  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3367  }
3368 
3375  {
3376  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3377  }
3378 
3385  {
3386  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3387  }
3388 
3395  {
3396  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3397  }
3398 
3405  {
3406  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3407  }
3408 
3423  {
3424  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3425  }
3426 
3439  {
3440  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3441  }
3442 
3455  {
3456  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3457  }
3458 
3471  {
3472  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3473  }
3474 
3488  public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
3489  {
3490  if (signed)
3491  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3492  else
3493  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3494  }
3495 
3507  {
3508  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3509  }
3510 
3523  public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
3524  {
3525  if (signed)
3526  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3527  else
3528  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3529  }
3530 
3541  {
3542  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3543  }
3544 
3556  {
3557  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3558  }
3559 
3574  {
3575  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3576  }
3577 
3578 
3589  public AST wrapAST(long nativeObject)
3590  {
3591  return AST.create(this, nativeObject);
3592  }
3593 
3606  public long unwrapAST(AST a)
3607  {
3608  return a.getNativeObject();
3609  }
3610 
3615  public String SimplifyHelp()
3616  {
3617  return Native.simplifyGetHelp(nCtx());
3618  }
3619 
3624  {
3625  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3626  }
3627 
3636  public void updateParamValue(String id, String value)
3637  {
3638  Native.updateParamValue(nCtx(), id, value);
3639  }
3640 
3641  long m_ctx = 0;
3642 
3643  long nCtx()
3644  {
3645  return m_ctx;
3646  }
3647 
3648  void initContext()
3649  {
3652  }
3653 
3654  void checkContextMatch(Z3Object other)
3655  {
3656  if (this != other.getContext())
3657  throw new Z3Exception("Context mismatch");
3658  }
3659 
3660  void checkContextMatch(Z3Object[] arr)
3661  {
3662  if (arr != null)
3663  for (Z3Object a : arr)
3664  checkContextMatch(a);
3665  }
3666 
3667  private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
3668  private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(10);
3669  private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(10);
3670  private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(10);
3671  private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(10);
3672  private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(10);
3673  private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(10);
3674  private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(10);
3675  private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(10);
3676  private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(10);
3677  private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(10);
3678  private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(10);
3679  private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(10);
3680  private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10);
3681  private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10);
3682  private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(10);
3683 
3685  {
3686  return m_AST_DRQ;
3687  }
3688 
3690  {
3691  return m_ASTMap_DRQ;
3692  }
3693 
3695  {
3696  return m_ASTVector_DRQ;
3697  }
3698 
3700  {
3701  return m_ApplyResult_DRQ;
3702  }
3703 
3705  {
3706  return m_FuncEntry_DRQ;
3707  }
3708 
3710  {
3711  return m_FuncInterp_DRQ;
3712  }
3713 
3715  {
3716  return m_Goal_DRQ;
3717  }
3718 
3720  {
3721  return m_Model_DRQ;
3722  }
3723 
3725  {
3726  return m_Params_DRQ;
3727  }
3728 
3730  {
3731  return m_ParamDescrs_DRQ;
3732  }
3733 
3735  {
3736  return m_Probe_DRQ;
3737  }
3738 
3740  {
3741  return m_Solver_DRQ;
3742  }
3743 
3745  {
3746  return m_Statistics_DRQ;
3747  }
3748 
3750  {
3751  return m_Tactic_DRQ;
3752  }
3753 
3755  {
3756  return m_Fixedpoint_DRQ;
3757  }
3758 
3760  {
3761  return m_Optimize_DRQ;
3762  }
3763 
3764  protected long m_refCount = 0;
3765 
3769  protected void finalize()
3770  {
3771  dispose();
3772 
3773  if (m_refCount == 0)
3774  {
3775  try
3776  {
3777  Native.delContext(m_ctx);
3778  } catch (Z3Exception e)
3779  {
3780  // OK.
3781  }
3782  m_ctx = 0;
3783  }
3784  /*
3785  else
3786  CMW: re-queue the finalizer? */
3787  }
3788 
3792  public void dispose()
3793  {
3794  m_AST_DRQ.clear(this);
3795  m_ASTMap_DRQ.clear(this);
3796  m_ASTVector_DRQ.clear(this);
3797  m_ApplyResult_DRQ.clear(this);
3798  m_FuncEntry_DRQ.clear(this);
3799  m_FuncInterp_DRQ.clear(this);
3800  m_Goal_DRQ.clear(this);
3801  m_Model_DRQ.clear(this);
3802  m_Params_DRQ.clear(this);
3803  m_Probe_DRQ.clear(this);
3804  m_Solver_DRQ.clear(this);
3805  m_Statistics_DRQ.clear(this);
3806  m_Tactic_DRQ.clear(this);
3807  m_Fixedpoint_DRQ.clear(this);
3808 
3809  m_boolSort = null;
3810  m_intSort = null;
3811  m_realSort = null;
3812  }
3813 }
BoolExpr mkFPIsNegative(FPExpr t)
Definition: Context.java:3394
static long mkFpaFp(long a0, long a1, long a2, long a3)
Definition: Native.java:5745
IntExpr mkIntConst(Symbol name)
Definition: Context.java:562
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6042
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1574
static long tacticRepeat(long a0, long a1, int a2)
Definition: Native.java:4154
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
Definition: Context.java:678
static long mkBvule(long a0, long a1, long a2)
Definition: Native.java:1487
static long mkSolver(long a0)
Definition: Native.java:4440
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6051
Tactic when(Probe p, Tactic t)
Definition: Context.java:2469
RatNum mkReal(String v)
Definition: Context.java:1911
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1017
static long mkExtract(long a0, int a1, int a2, long a3)
Definition: Native.java:1550
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
Definition: Context.java:315
static void interrupt(long a0)
Definition: Native.java:727
static long getSmtlibSort(long a0, int a1)
Definition: Native.java:3263
IDecRefQueue getOptimizeDRQ()
Definition: Context.java:3759
Probe and(Probe p1, Probe p2)
Definition: Context.java:2704
static long mkMod(long a0, long a1, long a2)
Definition: Native.java:1217
static long mkBvugt(long a0, long a1, long a2)
Definition: Native.java:1523
static void delConfig(long a0)
Definition: Native.java:672
ArrayExpr mkConstArray(Sort domain, Expr v)
Definition: Context.java:1673
static int getSmtlibNumSorts(long a0)
Definition: Native.java:3254
Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
Definition: Context.java:273
static long mkBvredor(long a0, long a1)
Definition: Native.java:1325
RealExpr mkFPToReal(FPExpr t)
Definition: Context.java:3540
static long tacticOrElse(long a0, long a1, long a2)
Definition: Native.java:4100
Probe lt(Probe p1, Probe p2)
Definition: Context.java:2643
BoolExpr mkDistinct(Expr...args)
Definition: Context.java:655
static long mkFpaNeg(long a0, long a1)
Definition: Native.java:5808
FPNum mkFPNumeral(double v, FPSort s)
Definition: Context.java:3040
static int getNumProbes(long a0)
Definition: Native.java:4307
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1215
BoolExpr mkFPIsSubnormal(FPExpr t)
Definition: Context.java:3354
static void parseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3192
static long mkNumeral(long a0, String a1, long a2)
Definition: Native.java:1883
ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1794
BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1347
static long mkFpaDiv(long a0, long a1, long a2, long a3)
Definition: Native.java:5844
static void updateParamValue(long a0, String a1, String a2)
Definition: Native.java:719
ArrayExpr mkSetComplement(ArrayExpr arg)
Definition: Context.java:1806
BitVecExpr mkBVNeg(BitVecExpr t)
Definition: Context.java:1030
static long mkFreshConst(long a0, String a1, long a2)
Definition: Native.java:1064
ArithExpr mkSub(ArithExpr...t)
Definition: Context.java:763
static long mkConfig()
Definition: Native.java:666
def RealSort(ctx=None)
Definition: z3py.py:2655
FPNum mkFPInf(FPSort s, boolean negative)
Definition: Context.java:3007
Expr mkNumeral(int v, Sort ty)
Definition: Context.java:1865
BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1548
ListSort mkListSort(String name, Sort elemSort)
Definition: Context.java:237
FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t)
Definition: Context.java:3232
FPNum mkFPNumeral(int v, FPSort s)
Definition: Context.java:3051
static long mkFpaIsNegative(long a0, long a1)
Definition: Native.java:5997
StringSymbol mkSymbol(String name)
Definition: Context.java:80
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1667
FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Definition: Context.java:3454
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1041
static long mkFpaRne(long a0)
Definition: Native.java:5556
Probe eq(Probe p1, Probe p2)
Definition: Context.java:2693
BitVecExpr mkZeroExt(int i, BitVecExpr t)
Definition: Context.java:1317
static long mkOr(long a0, int a1, long[] a2)
Definition: Native.java:1163
BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1424
Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2067
IDecRefQueue getModelDRQ()
Definition: Context.java:3719
String getProbeDescription(String name)
Definition: Context.java:2618
IntNum mkInt(String v)
Definition: Context.java:1948
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1082
BoolExpr mkAnd(BoolExpr...t)
Definition: Context.java:723
ArrayExpr mkSetUnion(ArrayExpr...args)
Definition: Context.java:1772
static long mkSub(long a0, int a1, long[] a2)
Definition: Native.java:1190
static long tacticFailIf(long a0, long a1)
Definition: Native.java:4181
IDecRefQueue getStatisticsDRQ()
Definition: Context.java:3744
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1386
static long mkExtRotateLeft(long a0, long a1, long a2)
Definition: Native.java:1631
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
Definition: Context.java:3299
FPRMNum mkFPRoundTowardNegative()
Definition: Context.java:2875
FPNum mkFP(float v, FPSort s)
Definition: Context.java:3088
static long mkFpaIsPositive(long a0, long a1)
Definition: Native.java:6006
static long mkFpaSort16(long a0)
Definition: Native.java:5655
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
Definition: Context.java:701
IDecRefQueue getFuncInterpDRQ()
Definition: Context.java:3709
static long mkFpaSqrt(long a0, long a1, long a2)
Definition: Native.java:5862
static long mkBvlshr(long a0, long a1, long a2)
Definition: Native.java:1595
BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2296
BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1589
BitVecExpr mkExtract(int high, int low, BitVecExpr t)
Definition: Context.java:1288
UninterpretedSort mkUninterpretedSort(String str)
Definition: Context.java:152
BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1150
static String probeGetDescr(long a0, String a1)
Definition: Native.java:4352
static long mkBvuge(long a0, long a1, long a2)
Definition: Native.java:1505
static long mkSolverForLogic(long a0, long a1)
Definition: Native.java:4458
static long getSmtlibDecl(long a0, int a1)
Definition: Native.java:3245
static long mkFpaAdd(long a0, long a1, long a2, long a3)
Definition: Native.java:5817
static long simplifyGetParamDescrs(long a0)
Definition: Native.java:2810
BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3334
FPNum mkFPNaN(FPSort s)
Definition: Context.java:2996
static long mkLe(long a0, long a1, long a2)
Definition: Native.java:1253
static long mkSetIntersect(long a0, int a1, long[] a2)
Definition: Native.java:1838
static long mkFpaRem(long a0, long a1, long a2)
Definition: Native.java:5871
static long mkConcat(long a0, long a1, long a2)
Definition: Native.java:1541
static long mkSelect(long a0, long a1, long a2)
Definition: Native.java:1739
static long mkBvnand(long a0, long a1, long a2)
Definition: Native.java:1361
static long mkFpaRoundTowardNegative(long a0)
Definition: Native.java:5601
static long mkFpaToReal(long a0, long a1)
Definition: Native.java:6078
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1439
BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2317
static long probeEq(long a0, long a1, long a2)
Definition: Native.java:4253
static long mkGe(long a0, long a1, long a2)
Definition: Native.java:1271
static long mkXor(long a0, long a1, long a2)
Definition: Native.java:1145
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1848
BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1118
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Definition: Context.java:194
BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1067
static long mkBvslt(long a0, long a1, long a2)
Definition: Native.java:1478
FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
Definition: Context.java:409
static long mkFpaEq(long a0, long a1, long a2)
Definition: Native.java:5943
void setPrintMode(Z3_ast_print_mode value)
Definition: Context.java:2123
FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3206
static long mkAdd(long a0, int a1, long[] a2)
Definition: Native.java:1172
static int getSmtlibNumFormulas(long a0)
Definition: Native.java:3200
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
Definition: Native.java:5781
FuncDecl mkConstDecl(String name, Sort range)
Definition: Context.java:456
static long probeOr(long a0, long a1, long a2)
Definition: Native.java:4271
SetSort mkSetSort(Sort ty)
Definition: Context.java:1719
IDecRefQueue getApplyResultDRQ()
Definition: Context.java:3699
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:833
FPExpr mkFPNeg(FPExpr t)
Definition: Context.java:3158
IntExpr mkReal2Int(RealExpr t)
Definition: Context.java:897
IDecRefQueue getParamDescrsDRQ()
Definition: Context.java:3729
RatNum mkReal(int v)
Definition: Context.java:1924
static long probeNot(long a0, long a1)
Definition: Native.java:4280
static long mkSignExt(long a0, int a1, long a2)
Definition: Native.java:1559
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3064
FPRMExpr mkFPRoundNearestTiesToEven()
Definition: Context.java:2821
static long mkBvsmod(long a0, long a1, long a2)
Definition: Native.java:1460
AST wrapAST(long nativeObject)
Definition: Context.java:3589
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1676
BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1828
static long mkSetComplement(long a0, long a1)
Definition: Native.java:1856
static long mkInt(long a0, int a1, long a2)
Definition: Native.java:1901
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
Definition: Context.java:396
static long probeConst(long a0, double a1)
Definition: Native.java:4208
static long mkSetAdd(long a0, long a1, long a2)
Definition: Native.java:1811
static long mkFpaNumeralInt(long a0, int a1, long a2)
Definition: Native.java:5772
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1721
static long mkBvneg(long a0, long a1)
Definition: Native.java:1388
static long mkInt64(long a0, long a1, long a2)
Definition: Native.java:1919
FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Definition: Context.java:3506
BoolExpr mkFPIsPositive(FPExpr t)
Definition: Context.java:3404
static long mkBvsdiv(long a0, long a1, long a2)
Definition: Native.java:1433
static long mkMap(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1766
FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
Definition: Context.java:3422
static int getNumTactics(long a0)
Definition: Native.java:4289
ArrayExpr mkSetDel(ArrayExpr set, Expr element)
Definition: Context.java:1760
static long mkZeroExt(long a0, int a1, long a2)
Definition: Native.java:1568
static long mkBvnot(long a0, long a1)
Definition: Native.java:1307
static long mkFpaRna(long a0)
Definition: Native.java:5574
static long mkDistinct(long a0, int a1, long[] a2)
Definition: Native.java:1100
BoolExpr mkIsInteger(RealExpr t)
Definition: Context.java:906
static long mkUnaryMinus(long a0, long a1)
Definition: Native.java:1199
BoolExpr mkBVNegNoOverflow(BitVecExpr t)
Definition: Context.java:1562
static long mkSetDifference(long a0, long a1, long a2)
Definition: Native.java:1847
static long mkBvsgt(long a0, long a1, long a2)
Definition: Native.java:1532
static long mkSetDel(long a0, long a1, long a2)
Definition: Native.java:1820
static long mkRotateRight(long a0, int a1, long a2)
Definition: Native.java:1622
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1694
static long mkStore(long a0, long a1, long a2, long a3)
Definition: Native.java:1748
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2079
FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
Definition: Context.java:3488
Probe gt(Probe p1, Probe p2)
Definition: Context.java:2655
BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3288
static long mkSolverFromTactic(long a0, long a1)
Definition: Native.java:4467
BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1202
static long mkBvadd(long a0, long a1, long a2)
Definition: Native.java:1397
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1505
static void delContext(long a0)
Definition: Native.java:698
BoolExpr mkFPIsInfinite(FPExpr t)
Definition: Context.java:3374
static long mkBvsle(long a0, long a1, long a2)
Definition: Native.java:1496
BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:965
BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:978
ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
Definition: Context.java:1748
BitVecExpr mkBVNot(BitVecExpr t)
Definition: Context.java:917
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6389
static long mkFpaGeq(long a0, long a1, long a2)
Definition: Native.java:5925
static long mkFpaGt(long a0, long a1, long a2)
Definition: Native.java:5934
BitVecExpr mkBVRedOR(BitVecExpr t)
Definition: Context.java:940
static long mkFpaToFpBv(long a0, long a1, long a2)
Definition: Native.java:6015
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2542
BitVecExpr mkBVConst(String name, int size)
Definition: Context.java:602
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:844
static void setAstPrintMode(long a0, int a1)
Definition: Native.java:3104
BoolExpr mkFPIsNaN(FPExpr t)
Definition: Context.java:3384
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1103
IDecRefQueue getTacticDRQ()
Definition: Context.java:3749
static long mkDiv(long a0, long a1, long a2)
Definition: Native.java:1208
static long mkIte(long a0, long a1, long a2, long a3)
Definition: Native.java:1118
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6069
FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3170
static String tacticGetDescr(long a0, String a1)
Definition: Native.java:4343
static long tacticFailIfNotDecided(long a0)
Definition: Native.java:4190
ArrayExpr mkMap(FuncDecl f, ArrayExpr...args)
Definition: Context.java:1694
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1254
static long mkSimpleSolver(long a0)
Definition: Native.java:4449
static long mkSetMember(long a0, long a1, long a2)
Definition: Native.java:1865
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2042
static long mkFpaSortDouble(long a0)
Definition: Native.java:5682
static long mkFpaSort64(long a0)
Definition: Native.java:5691
FPRMNum mkFPRoundNearestTiesToAway()
Definition: Context.java:2839
BoolExpr mkBoolConst(String name)
Definition: Context.java:554
FPNum mkFPZero(FPSort s, boolean negative)
Definition: Context.java:3018
BitVecExpr mkRepeat(int i, BitVecExpr t)
Definition: Context.java:1329
FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Definition: Context.java:3221
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:991
void updateParamValue(String id, String value)
Definition: Context.java:3636
Probe mkProbe(String name)
Definition: Context.java:2626
BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
Definition: Context.java:712
BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1366
static long tacticParOr(long a0, int a1, long[] a2)
Definition: Native.java:4109
static long tacticSkip(long a0)
Definition: Native.java:4163
static int getSmtlibNumDecls(long a0)
Definition: Native.java:3236
static long mkBvurem(long a0, long a1, long a2)
Definition: Native.java:1442
Tactic repeat(Tactic t, int max)
Definition: Context.java:2495
static long mkSetSubset(long a0, long a1, long a2)
Definition: Native.java:1874
static long mkImplies(long a0, long a1, long a2)
Definition: Native.java:1136
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
Definition: Context.java:2141
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:327
Tactic then(Tactic t1, Tactic t2, Tactic...ts)
Definition: Context.java:2432
FPNum mkFP(int v, FPSort s)
Definition: Context.java:3111
Tactic tryFor(Tactic t, int ms)
Definition: Context.java:2456
static long probeGt(long a0, long a1, long a2)
Definition: Native.java:4226
static long mkFpaAbs(long a0, long a1)
Definition: Native.java:5799
static long mkFpaIsNan(long a0, long a1)
Definition: Native.java:5988
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
Definition: Context.java:690
void parseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2179
static long getSmtlibAssumption(long a0, int a1)
Definition: Native.java:3227
IntExpr mkIntConst(String name)
Definition: Context.java:570
IDecRefQueue getASTVectorDRQ()
Definition: Context.java:3694
static long mkFpaSortSingle(long a0)
Definition: Native.java:5664
static long mkEq(long a0, long a1, long a2)
Definition: Native.java:1091
static long mkRem(long a0, long a1, long a2)
Definition: Native.java:1226
IDecRefQueue getASTMapDRQ()
Definition: Context.java:3689
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8119
Probe not(Probe p)
Definition: Context.java:2726
static long mkExtRotateRight(long a0, long a1, long a2)
Definition: Native.java:1640
static long mkFpaMul(long a0, long a1, long a2, long a3)
Definition: Native.java:5835
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1189
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3124
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1228
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1004
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
Definition: Context.java:384
IntNum mkInt(long v)
Definition: Context.java:1974
Solver mkSolver(String logic)
Definition: Context.java:2765
static long mkInt2bv(long a0, int a1, long a2)
Definition: Native.java:1649
BitVecExpr mkBVRedAND(BitVecExpr t)
Definition: Context.java:928
ArithExpr mkAdd(ArithExpr...t)
Definition: Context.java:743
IntExpr mkRem(IntExpr t1, IntExpr t2)
Definition: Context.java:809
FiniteDomainSort mkFiniteDomainSort(String name, long size)
Definition: Context.java:256
static long mkFpaRtz(long a0)
Definition: Native.java:5628
static long mkBvand(long a0, long a1, long a2)
Definition: Native.java:1334
FuncDecl mkConstDecl(Symbol name, Sort range)
Definition: Context.java:446
static long mkRepeat(long a0, int a1, long a2)
Definition: Native.java:1577
FPRMNum mkFPRoundTowardPositive()
Definition: Context.java:2857
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1533
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
Definition: Native.java:1012
IDecRefQueue getParamsDRQ()
Definition: Context.java:3724
static long mkPattern(long a0, int a1, long[] a2)
Definition: Native.java:1937
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
Definition: Native.java:5880
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:143
void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2160
static String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
Definition: Native.java:3157
static native void setInternalErrorHandler(long ctx)
static long mkFpaNumeralFloat(long a0, float a1, long a2)
Definition: Native.java:5754
static long mkBvult(long a0, long a1, long a2)
Definition: Native.java:1469
FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3194
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:677
static void parseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3184
static int getSmtlibNumAssumptions(long a0)
Definition: Native.java:3218
Expr mkFreshConst(String prefix, Sort range)
Definition: Context.java:527
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Definition: Context.java:3255
static long mkAnd(long a0, int a1, long[] a2)
Definition: Native.java:1154
Tactic failIf(Probe p)
Definition: Context.java:2522
static long mkLt(long a0, long a1, long a2)
Definition: Native.java:1244
static long mkContextRc(long a0)
Definition: Native.java:690
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
Definition: Context.java:3243
BoolExpr mkOr(BoolExpr...t)
Definition: Context.java:733
static long mkFpaRtp(long a0)
Definition: Native.java:5592
FPNum mkFP(double v, FPSort s)
Definition: Context.java:3099
ArrayExpr mkEmptySet(Sort domain)
Definition: Context.java:1728
static long mkFpaRoundTowardPositive(long a0)
Definition: Native.java:5583
static long mkFpaIsSubnormal(long a0, long a1)
Definition: Native.java:5961
Expr mkTermArray(ArrayExpr array)
Definition: Context.java:1709
static long mkBvsub(long a0, long a1, long a2)
Definition: Native.java:1406
static long mkFpaToIeeeBv(long a0, long a1)
Definition: Native.java:6150
static long mkConstArray(long a0, long a1, long a2)
Definition: Native.java:1757
static long mkInt2real(long a0, long a1)
Definition: Native.java:1280
FPExpr mkFPMin(FPExpr t1, FPExpr t2)
Definition: Context.java:3266
BoolExpr mkBool(boolean value)
Definition: Context.java:636
static long mkConst(long a0, long a1, long a2)
Definition: Native.java:1046
static long mkFpaInf(long a0, long a1, boolean a2)
Definition: Native.java:5727
static long mkBvsge(long a0, long a1, long a2)
Definition: Native.java:1514
def ArraySort(d, r)
Definition: z3py.py:4004
Probe or(Probe p1, Probe p2)
Definition: Context.java:2715
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
Definition: Native.java:6024
BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
Definition: Context.java:3573
static long mkFpaRoundNearestTiesToAway(long a0)
Definition: Native.java:5565
static long tacticParAndThen(long a0, long a1, long a2)
Definition: Native.java:4118
static String getProbeName(long a0, int a1)
Definition: Native.java:4316
FPExpr mkFPAbs(FPExpr t)
Definition: Context.java:3148
def IntSort(ctx=None)
Definition: z3py.py:2639
FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3182
Tactic with(Tactic t, Params p)
Definition: Context.java:2556
IntExpr mkMod(IntExpr t1, IntExpr t2)
Definition: Context.java:796
BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
Definition: Context.java:3523
Probe ge(Probe p1, Probe p2)
Definition: Context.java:2681
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4458
static long mkBvashr(long a0, long a1, long a2)
Definition: Native.java:1604
static long mkGt(long a0, long a1, long a2)
Definition: Native.java:1262
IDecRefQueue getGoalDRQ()
Definition: Context.java:3714
ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
Definition: Context.java:1601
static long mkFullSet(long a0, long a1)
Definition: Native.java:1802
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
Definition: Context.java:246
BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1176
BitVecExpr mkInt2BV(int n, IntExpr t)
Definition: Context.java:1457
BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
Definition: Context.java:1411
ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
Definition: Context.java:820
static long probeLe(long a0, long a1, long a2)
Definition: Native.java:4235
Context(Map< String, String > settings)
Definition: Context.java:56
BoolExpr mkBoolConst(Symbol name)
Definition: Context.java:546
static long mkFpaIsInfinite(long a0, long a1)
Definition: Native.java:5979
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
Definition: Context.java:3277
ArrayExpr mkFullSet(Sort domain)
Definition: Context.java:1738
IntSymbol mkSymbol(int i)
Definition: Context.java:72
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:610
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2055
BoolExpr[] getSMTLIBAssumptions()
Definition: Context.java:2232
Expr mkConst(String name, Sort range)
Definition: Context.java:518
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3166
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
Definition: Context.java:304
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1730
static long mkRotateLeft(long a0, int a1, long a2)
Definition: Native.java:1613
static String simplifyGetHelp(long a0)
Definition: Native.java:2801
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
Definition: Native.java:5790
Tactic parAndThen(Tactic t1, Tactic t2)
Definition: Context.java:2575
static long mkFpaMin(long a0, long a1, long a2)
Definition: Native.java:5889
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
Definition: Context.java:1399
static long mkBvredand(long a0, long a1)
Definition: Native.java:1316
static long tacticFail(long a0)
Definition: Native.java:4172
Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
Definition: Context.java:292
static long mkBvxor(long a0, long a1, long a2)
Definition: Native.java:1352
EnumSort mkEnumSort(String name, String...enumNames)
Definition: Context.java:218
static long tacticUsingParams(long a0, long a1, long a2)
Definition: Native.java:4199
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1163
Probe constProbe(double val)
Definition: Context.java:2634
static long probeLt(long a0, long a1, long a2)
Definition: Native.java:4217
static long mkFpaIsNormal(long a0, long a1)
Definition: Native.java:5952
static long mkBvudiv(long a0, long a1, long a2)
Definition: Native.java:1424
static long mkFpaNan(long a0, long a1)
Definition: Native.java:5718
static long probeGe(long a0, long a1, long a2)
Definition: Native.java:4244
static long mkBvshl(long a0, long a1, long a2)
Definition: Native.java:1586
static long mkFalse(long a0)
Definition: Native.java:1082
static long mkFpaRtn(long a0)
Definition: Native.java:5610
static long mkBvsrem(long a0, long a1, long a2)
Definition: Native.java:1451
BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:952
BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1519
BitVecExpr mkFPToIEEEBV(FPExpr t)
Definition: Context.java:3555
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3460
static long mkEmptySet(long a0, long a1)
Definition: Native.java:1793
static long mkFpaRoundNearestTiesToEven(long a0)
Definition: Native.java:5547
Expr mkBound(int index, Sort ty)
Definition: Context.java:480
IDecRefQueue getSolverDRQ()
Definition: Context.java:3739
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1703
RatNum mkReal(long v)
Definition: Context.java:1937
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3029
static String getTacticName(long a0, int a1)
Definition: Native.java:4298
BitVecExpr mkBVConst(Symbol name, int size)
Definition: Context.java:594
static long tacticTryFor(long a0, long a1, int a2)
Definition: Native.java:4127
static long mkArrayDefault(long a0, long a1)
Definition: Native.java:1775
static long mkBvnegNoOverflow(long a0, long a1)
Definition: Native.java:1712
IDecRefQueue getASTDRQ()
Definition: Context.java:3684
static long mkBound(long a0, int a1, long a2)
Definition: Native.java:1946
static long mkTrue(long a0)
Definition: Native.java:1073
Tactic mkTactic(String name)
Definition: Context.java:2392
static long mkFpaSort128(long a0)
Definition: Native.java:5709
static long mkMul(long a0, int a1, long[] a2)
Definition: Native.java:1181
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
Definition: Native.java:6033
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3077
static long mkReal(long a0, int a1, int a2)
Definition: Native.java:1892
FPSort mkFPSort(int ebits, int sbits)
Definition: Context.java:2913
static long tacticAndThen(long a0, long a1, long a2)
Definition: Native.java:4091
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
Definition: Context.java:1655
BitVecSort mkBitVecSort(int size)
Definition: Context.java:176
static long mkFpaLt(long a0, long a1, long a2)
Definition: Native.java:5916
ParamDescrs getSimplifyParameterDescriptions()
Definition: Context.java:3623
Fixedpoint mkFixedpoint()
Definition: Context.java:2794
static long mkBvxnor(long a0, long a1, long a2)
Definition: Native.java:1379
BoolExpr[] getSMTLIBFormulas()
Definition: Context.java:2208
Tactic parOr(Tactic...t)
Definition: Context.java:2564
static long mkFpaMax(long a0, long a1, long a2)
Definition: Native.java:5898
static long mkFpaSub(long a0, long a1, long a2, long a3)
Definition: Native.java:5826
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3137
BoolExpr mkFPIsNormal(FPExpr t)
Definition: Context.java:3344
static long mkSetUnion(long a0, int a1, long[] a2)
Definition: Native.java:1829
Tactic cond(Probe p, Tactic t1, Tactic t2)
Definition: Context.java:2482
static long mkPower(long a0, long a1, long a2)
Definition: Native.java:1235
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1136
static long mkFpaIsZero(long a0, long a1)
Definition: Native.java:5970
Solver mkSolver(Symbol logic)
Definition: Context.java:2751
def Map(f, args)
Definition: z3py.py:4100
FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
Definition: Context.java:3438
FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
Definition: Context.java:420
ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
Definition: Context.java:1610
static long mkBvor(long a0, long a1, long a2)
Definition: Native.java:1343
BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3310
static long getSmtlibFormula(long a0, int a1)
Definition: Native.java:3209
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:184
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:503
BitVecNum mkBV(int v, int size)
Definition: Context.java:1996
static long mkBv2int(long a0, long a1, boolean a2)
Definition: Native.java:1658
BoolExpr mkNot(BoolExpr a)
Definition: Context.java:665
Expr mkNumeral(long v, Sort ty)
Definition: Context.java:1881
DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
Definition: Context.java:358
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:855
FPRMSort mkFPRoundingModeSort()
Definition: Context.java:2812
ListSort mkListSort(Symbol name, Sort elemSort)
Definition: Context.java:227
static long mkFpaRoundTowardZero(long a0)
Definition: Native.java:5619
Tactic orElse(Tactic t1, Tactic t2)
Definition: Context.java:2442
Expr mkConst(FuncDecl f)
Definition: Context.java:538
Probe le(Probe p1, Probe p2)
Definition: Context.java:2668
ArithExpr mkUnaryMinus(ArithExpr t)
Definition: Context.java:773
EnumSort mkEnumSort(Symbol name, Symbol...enumNames)
Definition: Context.java:207
static long probeAnd(long a0, long a1, long a2)
Definition: Native.java:4262
RealExpr mkInt2Real(IntExpr t)
Definition: Context.java:884
RealExpr mkRealConst(Symbol name)
Definition: Context.java:578
ArrayExpr mkSetIntersection(ArrayExpr...args)
Definition: Context.java:1783
static long mkBvmul(long a0, long a1, long a2)
Definition: Native.java:1415
static long mkFpaSortQuadruple(long a0)
Definition: Native.java:5700
static long datatypeUpdateField(long a0, long a1, long a2, long a3)
Definition: Native.java:2198
FuncDecl mkFreshConstDecl(String prefix, Sort range)
Definition: Context.java:468
Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2096
static long mkFpaNumeralDouble(long a0, double a1, long a2)
Definition: Native.java:5763
BitVecNum mkBV(String v, int size)
Definition: Context.java:1986
Solver mkSolver(Tactic t)
Definition: Context.java:2784
ArithExpr mkMul(ArithExpr...t)
Definition: Context.java:753
String getTacticDescription(String name)
Definition: Context.java:2384
Expr mkSelect(ArrayExpr a, Expr i)
Definition: Context.java:1629
static long mkFpaFma(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:5853
static long mkReal2int(long a0, long a1)
Definition: Native.java:1289
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
Definition: Context.java:435
static long mkFpaSortHalf(long a0)
Definition: Native.java:5646
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6060
BitVecNum mkBV(long v, int size)
Definition: Context.java:2006
BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1054
static long tacticWhen(long a0, long a1, long a2)
Definition: Native.java:4136
ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
Definition: Context.java:783
RealExpr mkRealConst(String name)
Definition: Context.java:586
static long mkNot(long a0, long a1)
Definition: Native.java:1109
Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
Definition: Context.java:370
static long mkBvSort(long a0, int a1)
Definition: Native.java:915
FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Definition: Context.java:3470
static long mkFpaSort32(long a0)
Definition: Native.java:5673
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1272
RatNum mkReal(int num, int den)
Definition: Context.java:1897
BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
Definition: Context.java:3321
BitVecExpr mkSignExt(int i, BitVecExpr t)
Definition: Context.java:1303
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1241
BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
Definition: Context.java:1816
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
Definition: Context.java:1478
static long mkIsInt(long a0, long a1)
Definition: Native.java:1298
FPRMNum mkFPRoundTowardZero()
Definition: Context.java:2893
Pattern mkPattern(Expr...terms)
Definition: Context.java:489
static long mkFpaLeq(long a0, long a1, long a2)
Definition: Native.java:5907
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3175
BoolExpr mkEq(Expr x, Expr y)
Definition: Context.java:644
static long mkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:6159
def BoolSort(ctx=None)
Definition: z3py.py:1346
static long mkBvsubNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1685
static long mkIff(long a0, long a1, long a2)
Definition: Native.java:1127
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:866
BoolExpr mkFPIsZero(FPExpr t)
Definition: Context.java:3364
FuncDecl[] getSMTLIBDecls()
Definition: Context.java:2256
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2030
IDecRefQueue getProbeDRQ()
Definition: Context.java:3734
Tactic andThen(Tactic t1, Tactic t2, Tactic...ts)
Definition: Context.java:2401
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
Definition: Context.java:2345
IDecRefQueue getFixedpointDRQ()
Definition: Context.java:3754
static long tacticCond(long a0, long a1, long a2, long a3)
Definition: Native.java:4145
IDecRefQueue getFuncEntryDRQ()
Definition: Context.java:3704
static long mkFpaZero(long a0, long a1, boolean a2)
Definition: Native.java:5736
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1490
static long mkBvnor(long a0, long a1, long a2)
Definition: Native.java:1370