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 
367  public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
368 
369  {
370  checkContextMatch(name);
371  checkContextMatch(domain);
372  checkContextMatch(range);
373  return new FuncDecl(this, name, domain, range);
374  }
375 
379  public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
380 
381  {
382  checkContextMatch(name);
383  checkContextMatch(domain);
384  checkContextMatch(range);
385  Sort[] q = new Sort[] { domain };
386  return new FuncDecl(this, name, q, range);
387  }
388 
392  public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
393 
394  {
395  checkContextMatch(domain);
396  checkContextMatch(range);
397  return new FuncDecl(this, mkSymbol(name), domain, range);
398  }
399 
403  public FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
404 
405  {
406  checkContextMatch(domain);
407  checkContextMatch(range);
408  Sort[] q = new Sort[] { domain };
409  return new FuncDecl(this, mkSymbol(name), q, range);
410  }
411 
418  public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
419 
420  {
421  checkContextMatch(domain);
422  checkContextMatch(range);
423  return new FuncDecl(this, prefix, domain, range);
424  }
425 
429  public FuncDecl mkConstDecl(Symbol name, Sort range)
430  {
431  checkContextMatch(name);
432  checkContextMatch(range);
433  return new FuncDecl(this, name, null, range);
434  }
435 
439  public FuncDecl mkConstDecl(String name, Sort range)
440  {
441  checkContextMatch(range);
442  return new FuncDecl(this, mkSymbol(name), null, range);
443  }
444 
451  public FuncDecl mkFreshConstDecl(String prefix, Sort range)
452 
453  {
454  checkContextMatch(range);
455  return new FuncDecl(this, prefix, null, range);
456  }
457 
463  public Expr mkBound(int index, Sort ty)
464  {
465  return Expr.create(this,
466  Native.mkBound(nCtx(), index, ty.getNativeObject()));
467  }
468 
472  public Pattern mkPattern(Expr... terms)
473  {
474  if (terms.length == 0)
475  throw new Z3Exception("Cannot create a pattern from zero terms");
476 
477  long[] termsNative = AST.arrayToNative(terms);
478  return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length,
479  termsNative));
480  }
481 
486  public Expr mkConst(Symbol name, Sort range)
487  {
488  checkContextMatch(name);
489  checkContextMatch(range);
490 
491  return Expr.create(
492  this,
493  Native.mkConst(nCtx(), name.getNativeObject(),
494  range.getNativeObject()));
495  }
496 
501  public Expr mkConst(String name, Sort range)
502  {
503  return mkConst(mkSymbol(name), range);
504  }
505 
510  public Expr mkFreshConst(String prefix, Sort range)
511  {
512  checkContextMatch(range);
513  return Expr.create(this,
514  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
515  }
516 
522  {
523  return mkApp(f, (Expr[]) null);
524  }
525 
530  {
531  return (BoolExpr) mkConst(name, getBoolSort());
532  }
533 
537  public BoolExpr mkBoolConst(String name)
538  {
539  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
540  }
541 
545  public IntExpr mkIntConst(Symbol name)
546  {
547  return (IntExpr) mkConst(name, getIntSort());
548  }
549 
553  public IntExpr mkIntConst(String name)
554  {
555  return (IntExpr) mkConst(name, getIntSort());
556  }
557 
562  {
563  return (RealExpr) mkConst(name, getRealSort());
564  }
565 
569  public RealExpr mkRealConst(String name)
570  {
571  return (RealExpr) mkConst(name, getRealSort());
572  }
573 
577  public BitVecExpr mkBVConst(Symbol name, int size)
578  {
579  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
580  }
581 
585  public BitVecExpr mkBVConst(String name, int size)
586  {
587  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
588  }
589 
593  public Expr mkApp(FuncDecl f, Expr... args)
594  {
595  checkContextMatch(f);
596  checkContextMatch(args);
597  return Expr.create(this, f, args);
598  }
599 
603  public BoolExpr mkTrue()
604  {
605  return new BoolExpr(this, Native.mkTrue(nCtx()));
606  }
607 
611  public BoolExpr mkFalse()
612  {
613  return new BoolExpr(this, Native.mkFalse(nCtx()));
614  }
615 
619  public BoolExpr mkBool(boolean value)
620  {
621  return value ? mkTrue() : mkFalse();
622  }
623 
627  public BoolExpr mkEq(Expr x, Expr y)
628  {
629  checkContextMatch(x);
630  checkContextMatch(y);
631  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
632  y.getNativeObject()));
633  }
634 
638  public BoolExpr mkDistinct(Expr... args)
639  {
640  checkContextMatch(args);
641  return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length,
642  AST.arrayToNative(args)));
643  }
644 
649  {
650  checkContextMatch(a);
651  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
652  }
653 
661  public Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
662  {
663  checkContextMatch(t1);
664  checkContextMatch(t2);
665  checkContextMatch(t3);
666  return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
667  t2.getNativeObject(), t3.getNativeObject()));
668  }
669 
674  {
675  checkContextMatch(t1);
676  checkContextMatch(t2);
677  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
678  t2.getNativeObject()));
679  }
680 
685  {
686  checkContextMatch(t1);
687  checkContextMatch(t2);
688  return new BoolExpr(this, Native.mkImplies(nCtx(),
689  t1.getNativeObject(), t2.getNativeObject()));
690  }
691 
696  {
697  checkContextMatch(t1);
698  checkContextMatch(t2);
699  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
700  t2.getNativeObject()));
701  }
702 
706  public BoolExpr mkAnd(BoolExpr... t)
707  {
708  checkContextMatch(t);
709  return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length,
710  AST.arrayToNative(t)));
711  }
712 
716  public BoolExpr mkOr(BoolExpr... t)
717  {
718  checkContextMatch(t);
719  return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length,
720  AST.arrayToNative(t)));
721  }
722 
726  public ArithExpr mkAdd(ArithExpr... t)
727  {
728  checkContextMatch(t);
729  return (ArithExpr) Expr.create(this,
730  Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t)));
731  }
732 
736  public ArithExpr mkMul(ArithExpr... t)
737  {
738  checkContextMatch(t);
739  return (ArithExpr) Expr.create(this,
740  Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t)));
741  }
742 
746  public ArithExpr mkSub(ArithExpr... t)
747  {
748  checkContextMatch(t);
749  return (ArithExpr) Expr.create(this,
750  Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t)));
751  }
752 
757  {
758  checkContextMatch(t);
759  return (ArithExpr) Expr.create(this,
760  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
761  }
762 
767  {
768  checkContextMatch(t1);
769  checkContextMatch(t2);
770  return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
771  t1.getNativeObject(), t2.getNativeObject()));
772  }
773 
779  public IntExpr mkMod(IntExpr t1, IntExpr t2)
780  {
781  checkContextMatch(t1);
782  checkContextMatch(t2);
783  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
784  t2.getNativeObject()));
785  }
786 
792  public IntExpr mkRem(IntExpr t1, IntExpr t2)
793  {
794  checkContextMatch(t1);
795  checkContextMatch(t2);
796  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
797  t2.getNativeObject()));
798  }
799 
804  {
805  checkContextMatch(t1);
806  checkContextMatch(t2);
807  return (ArithExpr) Expr.create(
808  this,
809  Native.mkPower(nCtx(), t1.getNativeObject(),
810  t2.getNativeObject()));
811  }
812 
817  {
818  checkContextMatch(t1);
819  checkContextMatch(t2);
820  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
821  t2.getNativeObject()));
822  }
823 
828  {
829  checkContextMatch(t1);
830  checkContextMatch(t2);
831  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
832  t2.getNativeObject()));
833  }
834 
839  {
840  checkContextMatch(t1);
841  checkContextMatch(t2);
842  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
843  t2.getNativeObject()));
844  }
845 
850  {
851  checkContextMatch(t1);
852  checkContextMatch(t2);
853  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
854  t2.getNativeObject()));
855  }
856 
868  {
869  checkContextMatch(t);
870  return new RealExpr(this,
871  Native.mkInt2real(nCtx(), t.getNativeObject()));
872  }
873 
881  {
882  checkContextMatch(t);
883  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
884  }
885 
890  {
891  checkContextMatch(t);
892  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
893  }
894 
901  {
902  checkContextMatch(t);
903  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
904  }
905 
912  {
913  checkContextMatch(t);
914  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
915  t.getNativeObject()));
916  }
917 
924  {
925  checkContextMatch(t);
926  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
927  t.getNativeObject()));
928  }
929 
936  {
937  checkContextMatch(t1);
938  checkContextMatch(t2);
939  return new BitVecExpr(this, Native.mkBvand(nCtx(),
940  t1.getNativeObject(), t2.getNativeObject()));
941  }
942 
949  {
950  checkContextMatch(t1);
951  checkContextMatch(t2);
952  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
953  t2.getNativeObject()));
954  }
955 
962  {
963  checkContextMatch(t1);
964  checkContextMatch(t2);
965  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
966  t1.getNativeObject(), t2.getNativeObject()));
967  }
968 
975  {
976  checkContextMatch(t1);
977  checkContextMatch(t2);
978  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
979  t1.getNativeObject(), t2.getNativeObject()));
980  }
981 
988  {
989  checkContextMatch(t1);
990  checkContextMatch(t2);
991  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
992  t1.getNativeObject(), t2.getNativeObject()));
993  }
994 
1001  {
1002  checkContextMatch(t1);
1003  checkContextMatch(t2);
1004  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1005  t1.getNativeObject(), t2.getNativeObject()));
1006  }
1007 
1014  {
1015  checkContextMatch(t);
1016  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1017  }
1018 
1025  {
1026  checkContextMatch(t1);
1027  checkContextMatch(t2);
1028  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1029  t1.getNativeObject(), t2.getNativeObject()));
1030  }
1031 
1038  {
1039  checkContextMatch(t1);
1040  checkContextMatch(t2);
1041  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1042  t1.getNativeObject(), t2.getNativeObject()));
1043  }
1044 
1051  {
1052  checkContextMatch(t1);
1053  checkContextMatch(t2);
1054  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1055  t1.getNativeObject(), t2.getNativeObject()));
1056  }
1057 
1066  {
1067  checkContextMatch(t1);
1068  checkContextMatch(t2);
1069  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1070  t1.getNativeObject(), t2.getNativeObject()));
1071  }
1072 
1087  {
1088  checkContextMatch(t1);
1089  checkContextMatch(t2);
1090  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1091  t1.getNativeObject(), t2.getNativeObject()));
1092  }
1093 
1102  {
1103  checkContextMatch(t1);
1104  checkContextMatch(t2);
1105  return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1106  t1.getNativeObject(), t2.getNativeObject()));
1107  }
1108 
1120  {
1121  checkContextMatch(t1);
1122  checkContextMatch(t2);
1123  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1124  t1.getNativeObject(), t2.getNativeObject()));
1125  }
1126 
1134  {
1135  checkContextMatch(t1);
1136  checkContextMatch(t2);
1137  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1138  t1.getNativeObject(), t2.getNativeObject()));
1139  }
1140 
1147  {
1148  checkContextMatch(t1);
1149  checkContextMatch(t2);
1150  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1151  t2.getNativeObject()));
1152  }
1153 
1160  {
1161  checkContextMatch(t1);
1162  checkContextMatch(t2);
1163  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1164  t2.getNativeObject()));
1165  }
1166 
1173  {
1174  checkContextMatch(t1);
1175  checkContextMatch(t2);
1176  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1177  t2.getNativeObject()));
1178  }
1179 
1186  {
1187  checkContextMatch(t1);
1188  checkContextMatch(t2);
1189  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1190  t2.getNativeObject()));
1191  }
1192 
1199  {
1200  checkContextMatch(t1);
1201  checkContextMatch(t2);
1202  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1203  t2.getNativeObject()));
1204  }
1205 
1212  {
1213  checkContextMatch(t1);
1214  checkContextMatch(t2);
1215  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1216  t2.getNativeObject()));
1217  }
1218 
1225  {
1226  checkContextMatch(t1);
1227  checkContextMatch(t2);
1228  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1229  t2.getNativeObject()));
1230  }
1231 
1238  {
1239  checkContextMatch(t1);
1240  checkContextMatch(t2);
1241  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1242  t2.getNativeObject()));
1243  }
1244 
1256  {
1257  checkContextMatch(t1);
1258  checkContextMatch(t2);
1259  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1260  t1.getNativeObject(), t2.getNativeObject()));
1261  }
1262 
1271  public BitVecExpr mkExtract(int high, int low, BitVecExpr t)
1272 
1273  {
1274  checkContextMatch(t);
1275  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1276  t.getNativeObject()));
1277  }
1278 
1287  {
1288  checkContextMatch(t);
1289  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1290  t.getNativeObject()));
1291  }
1292 
1301  {
1302  checkContextMatch(t);
1303  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1304  t.getNativeObject()));
1305  }
1306 
1312  public BitVecExpr mkRepeat(int i, BitVecExpr t)
1313  {
1314  checkContextMatch(t);
1315  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1316  t.getNativeObject()));
1317  }
1318 
1331  {
1332  checkContextMatch(t1);
1333  checkContextMatch(t2);
1334  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1335  t1.getNativeObject(), t2.getNativeObject()));
1336  }
1337 
1350  {
1351  checkContextMatch(t1);
1352  checkContextMatch(t2);
1353  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1354  t1.getNativeObject(), t2.getNativeObject()));
1355  }
1356 
1370  {
1371  checkContextMatch(t1);
1372  checkContextMatch(t2);
1373  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1374  t1.getNativeObject(), t2.getNativeObject()));
1375  }
1376 
1383  {
1384  checkContextMatch(t);
1385  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1386  t.getNativeObject()));
1387  }
1388 
1395  {
1396  checkContextMatch(t);
1397  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1398  t.getNativeObject()));
1399  }
1400 
1408 
1409  {
1410  checkContextMatch(t1);
1411  checkContextMatch(t2);
1412  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1413  t1.getNativeObject(), t2.getNativeObject()));
1414  }
1415 
1423 
1424  {
1425  checkContextMatch(t1);
1426  checkContextMatch(t2);
1427  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1428  t1.getNativeObject(), t2.getNativeObject()));
1429  }
1430 
1440  public BitVecExpr mkInt2BV(int n, IntExpr t)
1441  {
1442  checkContextMatch(t);
1443  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1444  t.getNativeObject()));
1445  }
1446 
1461  public IntExpr mkBV2Int(BitVecExpr t, boolean signed)
1462  {
1463  checkContextMatch(t);
1464  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1465  (signed) ? true : false));
1466  }
1467 
1474  boolean isSigned)
1475  {
1476  checkContextMatch(t1);
1477  checkContextMatch(t2);
1478  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1479  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1480  : false));
1481  }
1482 
1489 
1490  {
1491  checkContextMatch(t1);
1492  checkContextMatch(t2);
1493  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1494  t1.getNativeObject(), t2.getNativeObject()));
1495  }
1496 
1503 
1504  {
1505  checkContextMatch(t1);
1506  checkContextMatch(t2);
1507  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1508  t1.getNativeObject(), t2.getNativeObject()));
1509  }
1510 
1517  boolean isSigned)
1518  {
1519  checkContextMatch(t1);
1520  checkContextMatch(t2);
1521  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1522  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1523  : false));
1524  }
1525 
1532 
1533  {
1534  checkContextMatch(t1);
1535  checkContextMatch(t2);
1536  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1537  t1.getNativeObject(), t2.getNativeObject()));
1538  }
1539 
1546  {
1547  checkContextMatch(t);
1548  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1549  t.getNativeObject()));
1550  }
1551 
1558  boolean isSigned)
1559  {
1560  checkContextMatch(t1);
1561  checkContextMatch(t2);
1562  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1563  .getNativeObject(), t2.getNativeObject(), (isSigned) ? true
1564  : false));
1565  }
1566 
1573 
1574  {
1575  checkContextMatch(t1);
1576  checkContextMatch(t2);
1577  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1578  t1.getNativeObject(), t2.getNativeObject()));
1579  }
1580 
1584  public ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
1585 
1586  {
1587  return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1588  }
1589 
1593  public ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
1594 
1595  {
1596  return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1597  }
1598 
1613  {
1614  checkContextMatch(a);
1615  checkContextMatch(i);
1616  return Expr.create(
1617  this,
1618  Native.mkSelect(nCtx(), a.getNativeObject(),
1619  i.getNativeObject()));
1620  }
1621 
1639  {
1640  checkContextMatch(a);
1641  checkContextMatch(i);
1642  checkContextMatch(v);
1643  return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1644  i.getNativeObject(), v.getNativeObject()));
1645  }
1646 
1656  public ArrayExpr mkConstArray(Sort domain, Expr v)
1657  {
1658  checkContextMatch(domain);
1659  checkContextMatch(v);
1660  return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1661  domain.getNativeObject(), v.getNativeObject()));
1662  }
1663 
1677  public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
1678  {
1679  checkContextMatch(f);
1680  checkContextMatch(args);
1681  return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1682  f.getNativeObject(), AST.arrayLength(args),
1683  AST.arrayToNative(args)));
1684  }
1685 
1693  {
1694  checkContextMatch(array);
1695  return Expr.create(this,
1696  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1697  }
1698 
1703  {
1704  checkContextMatch(ty);
1705  return new SetSort(this, ty);
1706  }
1707 
1711  public Expr mkEmptySet(Sort domain)
1712  {
1713  checkContextMatch(domain);
1714  return Expr.create(this,
1715  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1716  }
1717 
1721  public Expr mkFullSet(Sort domain)
1722  {
1723  checkContextMatch(domain);
1724  return Expr.create(this,
1725  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1726  }
1727 
1731  public Expr mkSetAdd(Expr set, Expr element)
1732  {
1733  checkContextMatch(set);
1734  checkContextMatch(element);
1735  return Expr.create(
1736  this,
1737  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1738  element.getNativeObject()));
1739  }
1740 
1744  public Expr mkSetDel(Expr set, Expr element)
1745  {
1746  checkContextMatch(set);
1747  checkContextMatch(element);
1748  return Expr.create(
1749  this,
1750  Native.mkSetDel(nCtx(), set.getNativeObject(),
1751  element.getNativeObject()));
1752  }
1753 
1757  public Expr mkSetUnion(Expr... args)
1758  {
1759  checkContextMatch(args);
1760  return Expr.create(
1761  this,
1762  Native.mkSetUnion(nCtx(), (int) args.length,
1763  AST.arrayToNative(args)));
1764  }
1765 
1769  public Expr mkSetIntersection(Expr... args)
1770  {
1771  checkContextMatch(args);
1772  return Expr.create(
1773  this,
1774  Native.mkSetIntersect(nCtx(), (int) args.length,
1775  AST.arrayToNative(args)));
1776  }
1777 
1781  public Expr mkSetDifference(Expr arg1, Expr arg2)
1782  {
1783  checkContextMatch(arg1);
1784  checkContextMatch(arg2);
1785  return Expr.create(
1786  this,
1787  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1788  arg2.getNativeObject()));
1789  }
1790 
1795  {
1796  checkContextMatch(arg);
1797  return Expr.create(this,
1798  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1799  }
1800 
1804  public Expr mkSetMembership(Expr elem, Expr set)
1805  {
1806  checkContextMatch(elem);
1807  checkContextMatch(set);
1808  return Expr.create(
1809  this,
1810  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1811  set.getNativeObject()));
1812  }
1813 
1817  public Expr mkSetSubset(Expr arg1, Expr arg2)
1818  {
1819  checkContextMatch(arg1);
1820  checkContextMatch(arg2);
1821  return Expr.create(
1822  this,
1823  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1824  arg2.getNativeObject()));
1825  }
1826 
1838  public Expr mkNumeral(String v, Sort ty)
1839  {
1840  checkContextMatch(ty);
1841  return Expr.create(this,
1842  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
1843  }
1844 
1855  public Expr mkNumeral(int v, Sort ty)
1856  {
1857  checkContextMatch(ty);
1858  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
1859  }
1860 
1871  public Expr mkNumeral(long v, Sort ty)
1872  {
1873  checkContextMatch(ty);
1874  return Expr.create(this,
1875  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
1876  }
1877 
1887  public RatNum mkReal(int num, int den)
1888  {
1889  if (den == 0)
1890  throw new Z3Exception("Denominator is zero");
1891 
1892  return new RatNum(this, Native.mkReal(nCtx(), num, den));
1893  }
1894 
1901  public RatNum mkReal(String v)
1902  {
1903 
1904  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
1905  .getNativeObject()));
1906  }
1907 
1914  public RatNum mkReal(int v)
1915  {
1916 
1917  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
1918  .getNativeObject()));
1919  }
1920 
1927  public RatNum mkReal(long v)
1928  {
1929 
1930  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
1931  .getNativeObject()));
1932  }
1933 
1938  public IntNum mkInt(String v)
1939  {
1940 
1941  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
1942  .getNativeObject()));
1943  }
1944 
1951  public IntNum mkInt(int v)
1952  {
1953 
1954  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
1955  .getNativeObject()));
1956  }
1957 
1964  public IntNum mkInt(long v)
1965  {
1966 
1967  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
1968  .getNativeObject()));
1969  }
1970 
1976  public BitVecNum mkBV(String v, int size)
1977  {
1978  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
1979  }
1980 
1986  public BitVecNum mkBV(int v, int size)
1987  {
1988  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
1989  }
1990 
1996  public BitVecNum mkBV(long v, int size)
1997  {
1998  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
1999  }
2000 
2020  public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
2021  int weight, Pattern[] patterns, Expr[] noPatterns,
2022  Symbol quantifierID, Symbol skolemID)
2023  {
2024 
2025  return new Quantifier(this, true, sorts, names, body, weight, patterns,
2026  noPatterns, quantifierID, skolemID);
2027  }
2028 
2032  public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
2033  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2034  Symbol skolemID)
2035  {
2036 
2037  return new Quantifier(this, true, boundConstants, body, weight,
2038  patterns, noPatterns, quantifierID, skolemID);
2039  }
2040 
2045  public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
2046  int weight, Pattern[] patterns, Expr[] noPatterns,
2047  Symbol quantifierID, Symbol skolemID)
2048  {
2049 
2050  return new Quantifier(this, false, sorts, names, body, weight,
2051  patterns, noPatterns, quantifierID, skolemID);
2052  }
2053 
2057  public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
2058  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2059  Symbol skolemID)
2060  {
2061 
2062  return new Quantifier(this, false, boundConstants, body, weight,
2063  patterns, noPatterns, quantifierID, skolemID);
2064  }
2065 
2069  public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
2070  Symbol[] names, Expr body, int weight, Pattern[] patterns,
2071  Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
2072 
2073  {
2074 
2075  if (universal)
2076  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2077  quantifierID, skolemID);
2078  else
2079  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2080  quantifierID, skolemID);
2081  }
2082 
2086  public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
2087  Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
2088  Symbol quantifierID, Symbol skolemID)
2089  {
2090 
2091  if (universal)
2092  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2093  quantifierID, skolemID);
2094  else
2095  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2096  quantifierID, skolemID);
2097  }
2098 
2113  public void setPrintMode(Z3_ast_print_mode value)
2114  {
2115  Native.setAstPrintMode(nCtx(), value.toInt());
2116  }
2117 
2131  public String benchmarkToSMTString(String name, String logic,
2132  String status, String attributes, BoolExpr[] assumptions,
2133  BoolExpr formula)
2134  {
2135 
2136  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2137  attributes, (int) assumptions.length,
2138  AST.arrayToNative(assumptions), formula.getNativeObject());
2139  }
2140 
2150  public void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts,
2151  Symbol[] declNames, FuncDecl[] decls)
2152  {
2153  int csn = Symbol.arrayLength(sortNames);
2154  int cs = Sort.arrayLength(sorts);
2155  int cdn = Symbol.arrayLength(declNames);
2156  int cd = AST.arrayLength(decls);
2157  if (csn != cs || cdn != cd)
2158  throw new Z3Exception("Argument size mismatch");
2159  Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
2160  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2161  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2162  AST.arrayToNative(decls));
2163  }
2164 
2169  public void parseSMTLIBFile(String fileName, Symbol[] sortNames,
2170  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2171 
2172  {
2173  int csn = Symbol.arrayLength(sortNames);
2174  int cs = Sort.arrayLength(sorts);
2175  int cdn = Symbol.arrayLength(declNames);
2176  int cd = AST.arrayLength(decls);
2177  if (csn != cs || cdn != cd)
2178  throw new Z3Exception("Argument size mismatch");
2179  Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
2180  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2181  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2182  AST.arrayToNative(decls));
2183  }
2184 
2190  {
2191  return Native.getSmtlibNumFormulas(nCtx());
2192  }
2193 
2199  {
2200 
2201  int n = getNumSMTLIBFormulas();
2202  BoolExpr[] res = new BoolExpr[n];
2203  for (int i = 0; i < n; i++)
2204  res[i] = (BoolExpr) Expr.create(this,
2205  Native.getSmtlibFormula(nCtx(), i));
2206  return res;
2207  }
2208 
2214  {
2215  return Native.getSmtlibNumAssumptions(nCtx());
2216  }
2217 
2223  {
2224 
2225  int n = getNumSMTLIBAssumptions();
2226  BoolExpr[] res = new BoolExpr[n];
2227  for (int i = 0; i < n; i++)
2228  res[i] = (BoolExpr) Expr.create(this,
2229  Native.getSmtlibAssumption(nCtx(), i));
2230  return res;
2231  }
2232 
2237  public int getNumSMTLIBDecls()
2238  {
2239  return Native.getSmtlibNumDecls(nCtx());
2240  }
2241 
2247  {
2248 
2249  int n = getNumSMTLIBDecls();
2250  FuncDecl[] res = new FuncDecl[n];
2251  for (int i = 0; i < n; i++)
2252  res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
2253  return res;
2254  }
2255 
2260  public int getNumSMTLIBSorts()
2261  {
2262  return Native.getSmtlibNumSorts(nCtx());
2263  }
2264 
2270  {
2271 
2272  int n = getNumSMTLIBSorts();
2273  Sort[] res = new Sort[n];
2274  for (int i = 0; i < n; i++)
2275  res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
2276  return res;
2277  }
2278 
2286  public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
2287  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2288 
2289  {
2290 
2291  int csn = Symbol.arrayLength(sortNames);
2292  int cs = Sort.arrayLength(sorts);
2293  int cdn = Symbol.arrayLength(declNames);
2294  int cd = AST.arrayLength(decls);
2295  if (csn != cs || cdn != cd)
2296  throw new Z3Exception("Argument size mismatch");
2297  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2298  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2299  AST.arrayToNative(sorts), AST.arrayLength(decls),
2300  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2301  }
2302 
2307  public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
2308  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2309 
2310  {
2311 
2312  int csn = Symbol.arrayLength(sortNames);
2313  int cs = Sort.arrayLength(sorts);
2314  int cdn = Symbol.arrayLength(declNames);
2315  int cd = AST.arrayLength(decls);
2316  if (csn != cs || cdn != cd)
2317  throw new Z3Exception("Argument size mismatch");
2318  return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
2319  fileName, AST.arrayLength(sorts),
2320  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2321  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2322  AST.arrayToNative(decls)));
2323  }
2324 
2335  public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
2336 
2337  {
2338  return new Goal(this, models, unsatCores, proofs);
2339  }
2340 
2344  public Params mkParams()
2345  {
2346  return new Params(this);
2347  }
2348 
2352  public int getNumTactics()
2353  {
2354  return Native.getNumTactics(nCtx());
2355  }
2356 
2360  public String[] getTacticNames()
2361  {
2362 
2363  int n = getNumTactics();
2364  String[] res = new String[n];
2365  for (int i = 0; i < n; i++)
2366  res[i] = Native.getTacticName(nCtx(), i);
2367  return res;
2368  }
2369 
2374  public String getTacticDescription(String name)
2375  {
2376  return Native.tacticGetDescr(nCtx(), name);
2377  }
2378 
2382  public Tactic mkTactic(String name)
2383  {
2384  return new Tactic(this, name);
2385  }
2386 
2391  public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
2392 
2393  {
2394  checkContextMatch(t1);
2395  checkContextMatch(t2);
2396  checkContextMatch(ts);
2397 
2398  long last = 0;
2399  if (ts != null && ts.length > 0)
2400  {
2401  last = ts[ts.length - 1].getNativeObject();
2402  for (int i = ts.length - 2; i >= 0; i--)
2403  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2404  last);
2405  }
2406  if (last != 0)
2407  {
2408  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2409  return new Tactic(this, Native.tacticAndThen(nCtx(),
2410  t1.getNativeObject(), last));
2411  } else
2412  return new Tactic(this, Native.tacticAndThen(nCtx(),
2413  t1.getNativeObject(), t2.getNativeObject()));
2414  }
2415 
2422  public Tactic then(Tactic t1, Tactic t2, Tactic... ts)
2423  {
2424  return andThen(t1, t2, ts);
2425  }
2426 
2432  public Tactic orElse(Tactic t1, Tactic t2)
2433  {
2434  checkContextMatch(t1);
2435  checkContextMatch(t2);
2436  return new Tactic(this, Native.tacticOrElse(nCtx(),
2437  t1.getNativeObject(), t2.getNativeObject()));
2438  }
2439 
2446  public Tactic tryFor(Tactic t, int ms)
2447  {
2448  checkContextMatch(t);
2449  return new Tactic(this, Native.tacticTryFor(nCtx(),
2450  t.getNativeObject(), ms));
2451  }
2452 
2459  public Tactic when(Probe p, Tactic t)
2460  {
2461  checkContextMatch(t);
2462  checkContextMatch(p);
2463  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2464  t.getNativeObject()));
2465  }
2466 
2472  public Tactic cond(Probe p, Tactic t1, Tactic t2)
2473  {
2474  checkContextMatch(p);
2475  checkContextMatch(t1);
2476  checkContextMatch(t2);
2477  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2478  t1.getNativeObject(), t2.getNativeObject()));
2479  }
2480 
2485  public Tactic repeat(Tactic t, int max)
2486  {
2487  checkContextMatch(t);
2488  return new Tactic(this, Native.tacticRepeat(nCtx(),
2489  t.getNativeObject(), max));
2490  }
2491 
2495  public Tactic skip()
2496  {
2497  return new Tactic(this, Native.tacticSkip(nCtx()));
2498  }
2499 
2503  public Tactic fail()
2504  {
2505  return new Tactic(this, Native.tacticFail(nCtx()));
2506  }
2507 
2512  public Tactic failIf(Probe p)
2513  {
2514  checkContextMatch(p);
2515  return new Tactic(this,
2516  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2517  }
2518 
2524  {
2525  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2526  }
2527 
2533  {
2534  checkContextMatch(t);
2535  checkContextMatch(p);
2536  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2537  t.getNativeObject(), p.getNativeObject()));
2538  }
2539 
2546  public Tactic with(Tactic t, Params p)
2547  {
2548  return usingParams(t, p);
2549  }
2550 
2554  public Tactic parOr(Tactic... t)
2555  {
2556  checkContextMatch(t);
2557  return new Tactic(this, Native.tacticParOr(nCtx(),
2558  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2559  }
2560 
2566  {
2567  checkContextMatch(t1);
2568  checkContextMatch(t2);
2569  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2570  t1.getNativeObject(), t2.getNativeObject()));
2571  }
2572 
2578  public void interrupt()
2579  {
2580  Native.interrupt(nCtx());
2581  }
2582 
2586  public int getNumProbes()
2587  {
2588  return Native.getNumProbes(nCtx());
2589  }
2590 
2594  public String[] getProbeNames()
2595  {
2596 
2597  int n = getNumProbes();
2598  String[] res = new String[n];
2599  for (int i = 0; i < n; i++)
2600  res[i] = Native.getProbeName(nCtx(), i);
2601  return res;
2602  }
2603 
2608  public String getProbeDescription(String name)
2609  {
2610  return Native.probeGetDescr(nCtx(), name);
2611  }
2612 
2616  public Probe mkProbe(String name)
2617  {
2618  return new Probe(this, name);
2619  }
2620 
2624  public Probe constProbe(double val)
2625  {
2626  return new Probe(this, Native.probeConst(nCtx(), val));
2627  }
2628 
2633  public Probe lt(Probe p1, Probe p2)
2634  {
2635  checkContextMatch(p1);
2636  checkContextMatch(p2);
2637  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2638  p2.getNativeObject()));
2639  }
2640 
2645  public Probe gt(Probe p1, Probe p2)
2646  {
2647  checkContextMatch(p1);
2648  checkContextMatch(p2);
2649  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2650  p2.getNativeObject()));
2651  }
2652 
2658  public Probe le(Probe p1, Probe p2)
2659  {
2660  checkContextMatch(p1);
2661  checkContextMatch(p2);
2662  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2663  p2.getNativeObject()));
2664  }
2665 
2671  public Probe ge(Probe p1, Probe p2)
2672  {
2673  checkContextMatch(p1);
2674  checkContextMatch(p2);
2675  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2676  p2.getNativeObject()));
2677  }
2678 
2683  public Probe eq(Probe p1, Probe p2)
2684  {
2685  checkContextMatch(p1);
2686  checkContextMatch(p2);
2687  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2688  p2.getNativeObject()));
2689  }
2690 
2694  public Probe and(Probe p1, Probe p2)
2695  {
2696  checkContextMatch(p1);
2697  checkContextMatch(p2);
2698  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
2699  p2.getNativeObject()));
2700  }
2701 
2705  public Probe or(Probe p1, Probe p2)
2706  {
2707  checkContextMatch(p1);
2708  checkContextMatch(p2);
2709  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
2710  p2.getNativeObject()));
2711  }
2712 
2716  public Probe not(Probe p)
2717  {
2718  checkContextMatch(p);
2719  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2720  }
2721 
2729  public Solver mkSolver()
2730  {
2731  return mkSolver((Symbol) null);
2732  }
2733 
2741  public Solver mkSolver(Symbol logic)
2742  {
2743 
2744  if (logic == null)
2745  return new Solver(this, Native.mkSolver(nCtx()));
2746  else
2747  return new Solver(this, Native.mkSolverForLogic(nCtx(),
2748  logic.getNativeObject()));
2749  }
2750 
2755  public Solver mkSolver(String logic)
2756  {
2757  return mkSolver(mkSymbol(logic));
2758  }
2759 
2764  {
2765  return new Solver(this, Native.mkSimpleSolver(nCtx()));
2766  }
2767 
2775  {
2776 
2777  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
2778  t.getNativeObject()));
2779  }
2780 
2785  {
2786  return new Fixedpoint(this);
2787  }
2788 
2789 
2795  {
2796  return new FPRMSort(this);
2797  }
2798 
2804  {
2805  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
2806  }
2807 
2812  public FPRMNum mkFPRNE()
2813  {
2814  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
2815  }
2816 
2822  {
2823  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
2824  }
2825 
2830  public FPRMNum mkFPRNA()
2831  {
2832  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
2833  }
2834 
2840  {
2841  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
2842  }
2843 
2848  public FPRMNum mkFPRTP()
2849  {
2850  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
2851  }
2852 
2858  {
2859  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
2860  }
2861 
2866  public FPRMNum mkFPRTN()
2867  {
2868  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
2869  }
2870 
2876  {
2877  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
2878  }
2879 
2884  public FPRMNum mkFPRTZ()
2885  {
2886  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
2887  }
2888 
2895  public FPSort mkFPSort(int ebits, int sbits)
2896  {
2897  return new FPSort(this, ebits, sbits);
2898  }
2899 
2905  {
2906  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
2907  }
2908 
2914  {
2915  return new FPSort(this, Native.mkFpaSort16(nCtx()));
2916  }
2917 
2923  {
2924  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
2925  }
2926 
2932  {
2933  return new FPSort(this, Native.mkFpaSort32(nCtx()));
2934  }
2935 
2941  {
2942  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
2943  }
2944 
2950  {
2951  return new FPSort(this, Native.mkFpaSort64(nCtx()));
2952  }
2953 
2959  {
2960  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
2961  }
2962 
2968  {
2969  return new FPSort(this, Native.mkFpaSort128(nCtx()));
2970  }
2971 
2972 
2979  {
2980  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
2981  }
2982 
2989  public FPNum mkFPInf(FPSort s, boolean negative)
2990  {
2991  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
2992  }
2993 
3000  public FPNum mkFPZero(FPSort s, boolean negative)
3001  {
3002  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3003  }
3004 
3011  public FPNum mkFPNumeral(float v, FPSort s)
3012  {
3013  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3014  }
3015 
3022  public FPNum mkFPNumeral(double v, FPSort s)
3023  {
3024  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3025  }
3026 
3033  public FPNum mkFPNumeral(int v, FPSort s)
3034  {
3035  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3036  }
3037 
3046  public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
3047  {
3048  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3049  }
3050 
3059  public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
3060  {
3061  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3062  }
3063 
3070  public FPNum mkFP(float v, FPSort s)
3071  {
3072  return mkFPNumeral(v, s);
3073  }
3074 
3081  public FPNum mkFP(double v, FPSort s)
3082  {
3083  return mkFPNumeral(v, s);
3084  }
3085 
3093  public FPNum mkFP(int v, FPSort s)
3094  {
3095  return mkFPNumeral(v, s);
3096  }
3097 
3106  public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
3107  {
3108  return mkFPNumeral(sgn, sig, exp, s);
3109  }
3110 
3119  public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
3120  {
3121  return mkFPNumeral(sgn, sig, exp, s);
3122  }
3123 
3124 
3130  public FPExpr mkFPAbs(FPExpr t)
3131  {
3132  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3133  }
3134 
3140  public FPExpr mkFPNeg(FPExpr t)
3141  {
3142  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3143  }
3144 
3152  public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
3153  {
3154  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3155  }
3156 
3164  public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
3165  {
3166  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3167  }
3168 
3176  public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
3177  {
3178  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3179  }
3180 
3188  public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
3189  {
3190  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3191  }
3192 
3203  public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
3204  {
3205  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3206  }
3207 
3215  {
3216  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3217  }
3218 
3225  public FPExpr mkFPRem(FPExpr t1, FPExpr t2)
3226  {
3227  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3228  }
3229 
3238  {
3239  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3240  }
3241 
3248  public FPExpr mkFPMin(FPExpr t1, FPExpr t2)
3249  {
3250  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3251  }
3252 
3259  public FPExpr mkFPMax(FPExpr t1, FPExpr t2)
3260  {
3261  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3262  }
3263 
3270  public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
3271  {
3272  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3273  }
3274 
3281  public BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
3282  {
3283  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3284  }
3285 
3292  public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
3293  {
3294  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3295  }
3296 
3303  public BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
3304  {
3305  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3306  }
3307 
3316  public BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
3317  {
3318  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3319  }
3320 
3327  {
3328  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3329  }
3330 
3337  {
3338  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3339  }
3340 
3347  {
3348  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3349  }
3350 
3357  {
3358  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3359  }
3360 
3367  {
3368  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3369  }
3370 
3377  {
3378  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3379  }
3380 
3387  {
3388  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3389  }
3390 
3405  {
3406  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3407  }
3408 
3421  {
3422  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3423  }
3424 
3437  {
3438  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3439  }
3440 
3453  {
3454  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3455  }
3456 
3470  public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
3471  {
3472  if (signed)
3473  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3474  else
3475  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3476  }
3477 
3489  {
3490  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3491  }
3492 
3505  public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
3506  {
3507  if (signed)
3508  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3509  else
3510  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3511  }
3512 
3523  {
3524  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3525  }
3526 
3538  {
3539  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3540  }
3541 
3556  {
3557  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3558  }
3559 
3560 
3571  public AST wrapAST(long nativeObject)
3572  {
3573  return AST.create(this, nativeObject);
3574  }
3575 
3588  public long unwrapAST(AST a)
3589  {
3590  return a.getNativeObject();
3591  }
3592 
3597  public String SimplifyHelp()
3598  {
3599  return Native.simplifyGetHelp(nCtx());
3600  }
3601 
3606  {
3607  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3608  }
3609 
3618  public void updateParamValue(String id, String value)
3619  {
3620  Native.updateParamValue(nCtx(), id, value);
3621  }
3622 
3623  long m_ctx = 0;
3624 
3625  long nCtx()
3626  {
3627  return m_ctx;
3628  }
3629 
3630  void initContext()
3631  {
3632  setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
3633  Native.setInternalErrorHandler(nCtx());
3634  }
3635 
3636  void checkContextMatch(Z3Object other)
3637  {
3638  if (this != other.getContext())
3639  throw new Z3Exception("Context mismatch");
3640  }
3641 
3642  void checkContextMatch(Z3Object[] arr)
3643  {
3644  if (arr != null)
3645  for (Z3Object a : arr)
3646  checkContextMatch(a);
3647  }
3648 
3649  private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
3650  private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(10);
3651  private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(10);
3652  private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(10);
3653  private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(10);
3654  private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(10);
3655  private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(10);
3656  private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(10);
3657  private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(10);
3658  private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(10);
3659  private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(10);
3660  private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(10);
3661  private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(10);
3662  private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10);
3663  private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10);
3664 
3666  {
3667  return m_AST_DRQ;
3668  }
3669 
3671  {
3672  return m_ASTMap_DRQ;
3673  }
3674 
3676  {
3677  return m_ASTVector_DRQ;
3678  }
3679 
3681  {
3682  return m_ApplyResult_DRQ;
3683  }
3684 
3686  {
3687  return m_FuncEntry_DRQ;
3688  }
3689 
3691  {
3692  return m_FuncInterp_DRQ;
3693  }
3694 
3696  {
3697  return m_Goal_DRQ;
3698  }
3699 
3701  {
3702  return m_Model_DRQ;
3703  }
3704 
3706  {
3707  return m_Params_DRQ;
3708  }
3709 
3711  {
3712  return m_ParamDescrs_DRQ;
3713  }
3714 
3716  {
3717  return m_Probe_DRQ;
3718  }
3719 
3721  {
3722  return m_Solver_DRQ;
3723  }
3724 
3726  {
3727  return m_Statistics_DRQ;
3728  }
3729 
3731  {
3732  return m_Tactic_DRQ;
3733  }
3734 
3736  {
3737  return m_Fixedpoint_DRQ;
3738  }
3739 
3740  protected long m_refCount = 0;
3741 
3745  protected void finalize()
3746  {
3747  dispose();
3748 
3749  if (m_refCount == 0)
3750  {
3751  try
3752  {
3753  Native.delContext(m_ctx);
3754  } catch (Z3Exception e)
3755  {
3756  // OK.
3757  }
3758  m_ctx = 0;
3759  }
3760  /*
3761  else
3762  CMW: re-queue the finalizer? */
3763  }
3764 
3768  public void dispose()
3769  {
3770  m_AST_DRQ.clear(this);
3771  m_ASTMap_DRQ.clear(this);
3772  m_ASTVector_DRQ.clear(this);
3773  m_ApplyResult_DRQ.clear(this);
3774  m_FuncEntry_DRQ.clear(this);
3775  m_FuncInterp_DRQ.clear(this);
3776  m_Goal_DRQ.clear(this);
3777  m_Model_DRQ.clear(this);
3778  m_Params_DRQ.clear(this);
3779  m_Probe_DRQ.clear(this);
3780  m_Solver_DRQ.clear(this);
3781  m_Statistics_DRQ.clear(this);
3782  m_Tactic_DRQ.clear(this);
3783  m_Fixedpoint_DRQ.clear(this);
3784 
3785  m_boolSort = null;
3786  m_intSort = null;
3787  m_realSort = null;
3788  }
3789 }
BoolExpr mkFPIsNegative(FPExpr t)
Definition: Context.java:3376
static long mkFpaFp(long a0, long a1, long a2, long a3)
Definition: Native.java:5521
IntExpr mkIntConst(Symbol name)
Definition: Context.java:545
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
Definition: Native.java:5818
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1557
static long tacticRepeat(long a0, long a1, int a2)
Definition: Native.java:3930
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
Definition: Context.java:661
static long mkBvule(long a0, long a1, long a2)
Definition: Native.java:1460
static long mkSolver(long a0)
Definition: Native.java:4216
def RealSort
Definition: z3py.py:2641
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
Definition: Native.java:5827
Tactic when(Probe p, Tactic t)
Definition: Context.java:2459
RatNum mkReal(String v)
Definition: Context.java:1901
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1000
static long mkExtract(long a0, int a1, int a2, long a3)
Definition: Native.java:1523
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
Definition: Context.java:315
static void interrupt(long a0)
Definition: Native.java:700
static long getSmtlibSort(long a0, int a1)
Definition: Native.java:3209
Probe and(Probe p1, Probe p2)
Definition: Context.java:2694
static long mkMod(long a0, long a1, long a2)
Definition: Native.java:1190
static long mkBvugt(long a0, long a1, long a2)
Definition: Native.java:1496
static void delConfig(long a0)
Definition: Native.java:645
ArrayExpr mkConstArray(Sort domain, Expr v)
Definition: Context.java:1656
static int getSmtlibNumSorts(long a0)
Definition: Native.java:3200
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:1298
RealExpr mkFPToReal(FPExpr t)
Definition: Context.java:3522
static long tacticOrElse(long a0, long a1, long a2)
Definition: Native.java:3876
Probe lt(Probe p1, Probe p2)
Definition: Context.java:2633
BoolExpr mkDistinct(Expr...args)
Definition: Context.java:638
static long mkFpaNeg(long a0, long a1)
Definition: Native.java:5584
FPNum mkFPNumeral(double v, FPSort s)
Definition: Context.java:3022
static int getNumProbes(long a0)
Definition: Native.java:4083
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1198
BoolExpr mkFPIsSubnormal(FPExpr t)
Definition: Context.java:3336
static void parseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3138
static long mkNumeral(long a0, String a1, long a2)
Definition: Native.java:1856
BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1330
def IntSort
Definition: z3py.py:2625
static long mkFpaDiv(long a0, long a1, long a2, long a3)
Definition: Native.java:5620
static void updateParamValue(long a0, String a1, String a2)
Definition: Native.java:692
def BoolSort
Definition: z3py.py:1336
BitVecExpr mkBVNeg(BitVecExpr t)
Definition: Context.java:1013
static long mkFreshConst(long a0, String a1, long a2)
Definition: Native.java:1037
ArithExpr mkSub(ArithExpr...t)
Definition: Context.java:746
static long mkConfig()
Definition: Native.java:639
FPNum mkFPInf(FPSort s, boolean negative)
Definition: Context.java:2989
Expr mkNumeral(int v, Sort ty)
Definition: Context.java:1855
BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1531
ListSort mkListSort(String name, Sort elemSort)
Definition: Context.java:237
FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t)
Definition: Context.java:3214
FPNum mkFPNumeral(int v, FPSort s)
Definition: Context.java:3033
Expr mkSetAdd(Expr set, Expr element)
Definition: Context.java:1731
static long mkFpaIsNegative(long a0, long a1)
Definition: Native.java:5773
StringSymbol mkSymbol(String name)
Definition: Context.java:80
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1640
FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Definition: Context.java:3436
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1024
static long mkFpaRne(long a0)
Definition: Native.java:5332
Probe eq(Probe p1, Probe p2)
Definition: Context.java:2683
def BitVecSort
Definition: z3py.py:3446
BitVecExpr mkZeroExt(int i, BitVecExpr t)
Definition: Context.java:1300
static long mkOr(long a0, int a1, long[] a2)
Definition: Native.java:1136
BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1407
Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2057
IDecRefQueue getModelDRQ()
Definition: Context.java:3700
String getProbeDescription(String name)
Definition: Context.java:2608
IntNum mkInt(String v)
Definition: Context.java:1938
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1065
BoolExpr mkAnd(BoolExpr...t)
Definition: Context.java:706
static long mkSub(long a0, int a1, long[] a2)
Definition: Native.java:1163
static long tacticFailIf(long a0, long a1)
Definition: Native.java:3957
IDecRefQueue getStatisticsDRQ()
Definition: Context.java:3725
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1369
static long mkExtRotateLeft(long a0, long a1, long a2)
Definition: Native.java:1604
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
Definition: Context.java:3281
FPRMNum mkFPRoundTowardNegative()
Definition: Context.java:2857
FPNum mkFP(float v, FPSort s)
Definition: Context.java:3070
static long mkFpaIsPositive(long a0, long a1)
Definition: Native.java:5782
static long mkFpaSort16(long a0)
Definition: Native.java:5431
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
Definition: Context.java:684
IDecRefQueue getFuncInterpDRQ()
Definition: Context.java:3690
static long mkFpaSqrt(long a0, long a1, long a2)
Definition: Native.java:5638
static long mkBvlshr(long a0, long a1, long a2)
Definition: Native.java:1568
BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2286
BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1572
BitVecExpr mkExtract(int high, int low, BitVecExpr t)
Definition: Context.java:1271
UninterpretedSort mkUninterpretedSort(String str)
Definition: Context.java:152
BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1133
static String probeGetDescr(long a0, String a1)
Definition: Native.java:4128
static long mkBvuge(long a0, long a1, long a2)
Definition: Native.java:1478
static long mkSolverForLogic(long a0, long a1)
Definition: Native.java:4234
static long getSmtlibDecl(long a0, int a1)
Definition: Native.java:3191
static long mkFpaAdd(long a0, long a1, long a2, long a3)
Definition: Native.java:5593
static long simplifyGetParamDescrs(long a0)
Definition: Native.java:2756
BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3316
FPNum mkFPNaN(FPSort s)
Definition: Context.java:2978
static long mkLe(long a0, long a1, long a2)
Definition: Native.java:1226
static long mkSetIntersect(long a0, int a1, long[] a2)
Definition: Native.java:1811
static long mkFpaRem(long a0, long a1, long a2)
Definition: Native.java:5647
static long mkConcat(long a0, long a1, long a2)
Definition: Native.java:1514
static long mkSelect(long a0, long a1, long a2)
Definition: Native.java:1712
static long mkBvnand(long a0, long a1, long a2)
Definition: Native.java:1334
static long mkFpaRoundTowardNegative(long a0)
Definition: Native.java:5377
static long mkFpaToReal(long a0, long a1)
Definition: Native.java:5854
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1422
BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2307
static long probeEq(long a0, long a1, long a2)
Definition: Native.java:4029
static long mkGe(long a0, long a1, long a2)
Definition: Native.java:1244
static long mkXor(long a0, long a1, long a2)
Definition: Native.java:1118
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:1838
BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1101
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Definition: Context.java:194
BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1050
static long mkBvslt(long a0, long a1, long a2)
Definition: Native.java:1451
FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
Definition: Context.java:392
static long mkFpaEq(long a0, long a1, long a2)
Definition: Native.java:5719
void setPrintMode(Z3_ast_print_mode value)
Definition: Context.java:2113
FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3188
static long mkAdd(long a0, int a1, long[] a2)
Definition: Native.java:1145
static int getSmtlibNumFormulas(long a0)
Definition: Native.java:3146
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
Definition: Native.java:5557
FuncDecl mkConstDecl(String name, Sort range)
Definition: Context.java:439
Expr mkSetDifference(Expr arg1, Expr arg2)
Definition: Context.java:1781
static long probeOr(long a0, long a1, long a2)
Definition: Native.java:4047
SetSort mkSetSort(Sort ty)
Definition: Context.java:1702
IDecRefQueue getApplyResultDRQ()
Definition: Context.java:3680
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:816
FPExpr mkFPNeg(FPExpr t)
Definition: Context.java:3140
IntExpr mkReal2Int(RealExpr t)
Definition: Context.java:880
Expr mkSetComplement(Expr arg)
Definition: Context.java:1794
IDecRefQueue getParamDescrsDRQ()
Definition: Context.java:3710
RatNum mkReal(int v)
Definition: Context.java:1914
static long probeNot(long a0, long a1)
Definition: Native.java:4056
static long mkSignExt(long a0, int a1, long a2)
Definition: Native.java:1532
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3046
FPRMExpr mkFPRoundNearestTiesToEven()
Definition: Context.java:2803
static long mkBvsmod(long a0, long a1, long a2)
Definition: Native.java:1433
AST wrapAST(long nativeObject)
Definition: Context.java:3571
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1649
static long mkSetComplement(long a0, long a1)
Definition: Native.java:1829
static long mkInt(long a0, int a1, long a2)
Definition: Native.java:1874
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
Definition: Context.java:379
static long probeConst(long a0, double a1)
Definition: Native.java:3984
static long mkSetAdd(long a0, long a1, long a2)
Definition: Native.java:1784
static long mkFpaNumeralInt(long a0, int a1, long a2)
Definition: Native.java:5548
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1694
static long mkBvneg(long a0, long a1)
Definition: Native.java:1361
static long mkInt64(long a0, long a1, long a2)
Definition: Native.java:1892
FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Definition: Context.java:3488
BoolExpr mkFPIsPositive(FPExpr t)
Definition: Context.java:3386
static long mkBvsdiv(long a0, long a1, long a2)
Definition: Native.java:1406
static long mkMap(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1739
FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
Definition: Context.java:3404
static int getNumTactics(long a0)
Definition: Native.java:4065
static long mkZeroExt(long a0, int a1, long a2)
Definition: Native.java:1541
static long mkBvnot(long a0, long a1)
Definition: Native.java:1280
static long mkFpaRna(long a0)
Definition: Native.java:5350
static long mkDistinct(long a0, int a1, long[] a2)
Definition: Native.java:1073
BoolExpr mkIsInteger(RealExpr t)
Definition: Context.java:889
static long mkUnaryMinus(long a0, long a1)
Definition: Native.java:1172
BoolExpr mkBVNegNoOverflow(BitVecExpr t)
Definition: Context.java:1545
static long mkSetDifference(long a0, long a1, long a2)
Definition: Native.java:1820
static long mkBvsgt(long a0, long a1, long a2)
Definition: Native.java:1505
static long mkSetDel(long a0, long a1, long a2)
Definition: Native.java:1793
static long mkRotateRight(long a0, int a1, long a2)
Definition: Native.java:1595
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1667
static long mkStore(long a0, long a1, long a2, long a3)
Definition: Native.java:1721
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2069
FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
Definition: Context.java:3470
Probe gt(Probe p1, Probe p2)
Definition: Context.java:2645
BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3270
static long mkSolverFromTactic(long a0, long a1)
Definition: Native.java:4243
BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1185
static long mkBvadd(long a0, long a1, long a2)
Definition: Native.java:1370
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1488
static void delContext(long a0)
Definition: Native.java:671
BoolExpr mkFPIsInfinite(FPExpr t)
Definition: Context.java:3356
static long mkBvsle(long a0, long a1, long a2)
Definition: Native.java:1469
BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:948
BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:961
BitVecExpr mkBVNot(BitVecExpr t)
Definition: Context.java:900
static long mkFpaGeq(long a0, long a1, long a2)
Definition: Native.java:5701
static long mkFpaGt(long a0, long a1, long a2)
Definition: Native.java:5710
BitVecExpr mkBVRedOR(BitVecExpr t)
Definition: Context.java:923
static long mkFpaToFpBv(long a0, long a1, long a2)
Definition: Native.java:5791
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2532
BitVecExpr mkBVConst(String name, int size)
Definition: Context.java:585
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:827
static void setAstPrintMode(long a0, int a1)
Definition: Native.java:3050
BoolExpr mkFPIsNaN(FPExpr t)
Definition: Context.java:3366
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1086
IDecRefQueue getTacticDRQ()
Definition: Context.java:3730
static long mkDiv(long a0, long a1, long a2)
Definition: Native.java:1181
static long mkIte(long a0, long a1, long a2, long a3)
Definition: Native.java:1091
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
Definition: Native.java:5845
FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3152
static String tacticGetDescr(long a0, String a1)
Definition: Native.java:4119
static long tacticFailIfNotDecided(long a0)
Definition: Native.java:3966
ArrayExpr mkMap(FuncDecl f, ArrayExpr...args)
Definition: Context.java:1677
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1237
static long mkSimpleSolver(long a0)
Definition: Native.java:4225
static long mkSetMember(long a0, long a1, long a2)
Definition: Native.java:1838
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2032
static long mkFpaSortDouble(long a0)
Definition: Native.java:5458
static long mkFpaSort64(long a0)
Definition: Native.java:5467
FPRMNum mkFPRoundNearestTiesToAway()
Definition: Context.java:2821
BoolExpr mkBoolConst(String name)
Definition: Context.java:537
FPNum mkFPZero(FPSort s, boolean negative)
Definition: Context.java:3000
BitVecExpr mkRepeat(int i, BitVecExpr t)
Definition: Context.java:1312
FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Definition: Context.java:3203
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:974
void updateParamValue(String id, String value)
Definition: Context.java:3618
Probe mkProbe(String name)
Definition: Context.java:2616
BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
Definition: Context.java:695
BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1349
static long tacticParOr(long a0, int a1, long[] a2)
Definition: Native.java:3885
static long tacticSkip(long a0)
Definition: Native.java:3939
static int getSmtlibNumDecls(long a0)
Definition: Native.java:3182
static long mkBvurem(long a0, long a1, long a2)
Definition: Native.java:1415
Tactic repeat(Tactic t, int max)
Definition: Context.java:2485
static long mkSetSubset(long a0, long a1, long a2)
Definition: Native.java:1847
static long mkImplies(long a0, long a1, long a2)
Definition: Native.java:1109
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
Definition: Context.java:2131
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:327
Tactic then(Tactic t1, Tactic t2, Tactic...ts)
Definition: Context.java:2422
FPNum mkFP(int v, FPSort s)
Definition: Context.java:3093
Tactic tryFor(Tactic t, int ms)
Definition: Context.java:2446
static long probeGt(long a0, long a1, long a2)
Definition: Native.java:4002
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
Definition: z3_api.h:1256
static long mkFpaAbs(long a0, long a1)
Definition: Native.java:5575
static long mkFpaIsNan(long a0, long a1)
Definition: Native.java:5764
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
Definition: Context.java:673
void parseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2169
static long getSmtlibAssumption(long a0, int a1)
Definition: Native.java:3173
IntExpr mkIntConst(String name)
Definition: Context.java:553
Expr mkSetUnion(Expr...args)
Definition: Context.java:1757
IDecRefQueue getASTVectorDRQ()
Definition: Context.java:3675
static long mkFpaSortSingle(long a0)
Definition: Native.java:5440
static long mkEq(long a0, long a1, long a2)
Definition: Native.java:1064
static long mkRem(long a0, long a1, long a2)
Definition: Native.java:1199
IDecRefQueue getASTMapDRQ()
Definition: Context.java:3670
Probe not(Probe p)
Definition: Context.java:2716
static long mkExtRotateRight(long a0, long a1, long a2)
Definition: Native.java:1613
static long mkFpaMul(long a0, long a1, long a2, long a3)
Definition: Native.java:5611
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1172
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3106
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1211
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:987
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
Definition: Context.java:367
IntNum mkInt(long v)
Definition: Context.java:1964
Solver mkSolver(String logic)
Definition: Context.java:2755
static long mkInt2bv(long a0, int a1, long a2)
Definition: Native.java:1622
BitVecExpr mkBVRedAND(BitVecExpr t)
Definition: Context.java:911
ArithExpr mkAdd(ArithExpr...t)
Definition: Context.java:726
IntExpr mkRem(IntExpr t1, IntExpr t2)
Definition: Context.java:792
FiniteDomainSort mkFiniteDomainSort(String name, long size)
Definition: Context.java:256
static long mkFpaRtz(long a0)
Definition: Native.java:5404
static long mkBvand(long a0, long a1, long a2)
Definition: Native.java:1307
FuncDecl mkConstDecl(Symbol name, Sort range)
Definition: Context.java:429
Expr mkSetMembership(Expr elem, Expr set)
Definition: Context.java:1804
static long mkRepeat(long a0, int a1, long a2)
Definition: Native.java:1550
FPRMNum mkFPRoundTowardPositive()
Definition: Context.java:2839
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1516
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
Definition: Native.java:985
IDecRefQueue getParamsDRQ()
Definition: Context.java:3705
static long mkPattern(long a0, int a1, long[] a2)
Definition: Native.java:1910
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
Definition: Native.java:5656
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:143
void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2150
static String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
Definition: Native.java:3103
static long mkFpaNumeralFloat(long a0, float a1, long a2)
Definition: Native.java:5530
static long mkBvult(long a0, long a1, long a2)
Definition: Native.java:1442
def EnumSort
Definition: z3py.py:4421
FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3176
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:650
static void parseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3130
static int getSmtlibNumAssumptions(long a0)
Definition: Native.java:3164
Expr mkFreshConst(String prefix, Sort range)
Definition: Context.java:510
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Definition: Context.java:3237
static long mkAnd(long a0, int a1, long[] a2)
Definition: Native.java:1127
Tactic failIf(Probe p)
Definition: Context.java:2512
static long mkLt(long a0, long a1, long a2)
Definition: Native.java:1217
Expr mkFullSet(Sort domain)
Definition: Context.java:1721
static long mkContextRc(long a0)
Definition: Native.java:663
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
Definition: Context.java:3225
BoolExpr mkOr(BoolExpr...t)
Definition: Context.java:716
static long mkFpaRtp(long a0)
Definition: Native.java:5368
FPNum mkFP(double v, FPSort s)
Definition: Context.java:3081
static long mkFpaRoundTowardPositive(long a0)
Definition: Native.java:5359
Expr mkSetIntersection(Expr...args)
Definition: Context.java:1769
static long mkFpaIsSubnormal(long a0, long a1)
Definition: Native.java:5737
Expr mkTermArray(ArrayExpr array)
Definition: Context.java:1692
static long mkBvsub(long a0, long a1, long a2)
Definition: Native.java:1379
static long mkFpaToIeeeBv(long a0, long a1)
Definition: Native.java:5917
static long mkConstArray(long a0, long a1, long a2)
Definition: Native.java:1730
static long mkInt2real(long a0, long a1)
Definition: Native.java:1253
FPExpr mkFPMin(FPExpr t1, FPExpr t2)
Definition: Context.java:3248
BoolExpr mkBool(boolean value)
Definition: Context.java:619
static long mkConst(long a0, long a1, long a2)
Definition: Native.java:1019
static long mkFpaInf(long a0, long a1, boolean a2)
Definition: Native.java:5503
static long mkBvsge(long a0, long a1, long a2)
Definition: Native.java:1487
def ArraySort(d, r)
Definition: z3py.py:3978
Probe or(Probe p1, Probe p2)
Definition: Context.java:2705
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
Definition: Native.java:5800
BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
Definition: Context.java:3555
static long mkFpaRoundNearestTiesToAway(long a0)
Definition: Native.java:5341
static long tacticParAndThen(long a0, long a1, long a2)
Definition: Native.java:3894
static String getProbeName(long a0, int a1)
Definition: Native.java:4092
FPExpr mkFPAbs(FPExpr t)
Definition: Context.java:3130
FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3164
Tactic with(Tactic t, Params p)
Definition: Context.java:2546
IntExpr mkMod(IntExpr t1, IntExpr t2)
Definition: Context.java:779
BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
Definition: Context.java:3505
Probe ge(Probe p1, Probe p2)
Definition: Context.java:2671
static long mkBvashr(long a0, long a1, long a2)
Definition: Native.java:1577
static long mkGt(long a0, long a1, long a2)
Definition: Native.java:1235
IDecRefQueue getGoalDRQ()
Definition: Context.java:3695
ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
Definition: Context.java:1584
static long mkFullSet(long a0, long a1)
Definition: Native.java:1775
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
Definition: Context.java:246
BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1159
BitVecExpr mkInt2BV(int n, IntExpr t)
Definition: Context.java:1440
BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
Definition: Context.java:1394
ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
Definition: Context.java:803
static long probeLe(long a0, long a1, long a2)
Definition: Native.java:4011
Context(Map< String, String > settings)
Definition: Context.java:56
BoolExpr mkBoolConst(Symbol name)
Definition: Context.java:529
static long mkFpaIsInfinite(long a0, long a1)
Definition: Native.java:5755
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
Definition: Context.java:3259
IntSymbol mkSymbol(int i)
Definition: Context.java:72
Expr mkApp(FuncDecl f, Expr...args)
Definition: Context.java:593
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2045
BoolExpr[] getSMTLIBAssumptions()
Definition: Context.java:2222
Expr mkConst(String name, Sort range)
Definition: Context.java:501
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3112
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
Definition: Context.java:304
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1703
static long mkRotateLeft(long a0, int a1, long a2)
Definition: Native.java:1586
static String simplifyGetHelp(long a0)
Definition: Native.java:2747
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
Definition: Native.java:5566
Tactic parAndThen(Tactic t1, Tactic t2)
Definition: Context.java:2565
static long mkFpaMin(long a0, long a1, long a2)
Definition: Native.java:5665
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
Definition: Context.java:1382
static long mkBvredand(long a0, long a1)
Definition: Native.java:1289
static long tacticFail(long a0)
Definition: Native.java:3948
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:1325
EnumSort mkEnumSort(String name, String...enumNames)
Definition: Context.java:218
static long tacticUsingParams(long a0, long a1, long a2)
Definition: Native.java:3975
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1146
Probe constProbe(double val)
Definition: Context.java:2624
static long probeLt(long a0, long a1, long a2)
Definition: Native.java:3993
static long mkFpaIsNormal(long a0, long a1)
Definition: Native.java:5728
static long mkBvudiv(long a0, long a1, long a2)
Definition: Native.java:1397
static long mkFpaNan(long a0, long a1)
Definition: Native.java:5494
static long probeGe(long a0, long a1, long a2)
Definition: Native.java:4020
static long mkBvshl(long a0, long a1, long a2)
Definition: Native.java:1559
Expr mkSetDel(Expr set, Expr element)
Definition: Context.java:1744
static long mkFalse(long a0)
Definition: Native.java:1055
static long mkFpaRtn(long a0)
Definition: Native.java:5386
static long mkBvsrem(long a0, long a1, long a2)
Definition: Native.java:1424
BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:935
BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1502
BitVecExpr mkFPToIEEEBV(FPExpr t)
Definition: Context.java:3537
static long mkEmptySet(long a0, long a1)
Definition: Native.java:1766
static long mkFpaRoundNearestTiesToEven(long a0)
Definition: Native.java:5323
Expr mkBound(int index, Sort ty)
Definition: Context.java:463
IDecRefQueue getSolverDRQ()
Definition: Context.java:3720
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1676
RatNum mkReal(long v)
Definition: Context.java:1927
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3011
static String getTacticName(long a0, int a1)
Definition: Native.java:4074
BitVecExpr mkBVConst(Symbol name, int size)
Definition: Context.java:577
static long tacticTryFor(long a0, long a1, int a2)
Definition: Native.java:3903
static long mkArrayDefault(long a0, long a1)
Definition: Native.java:1748
static long mkBvnegNoOverflow(long a0, long a1)
Definition: Native.java:1685
IDecRefQueue getASTDRQ()
Definition: Context.java:3665
static long mkBound(long a0, int a1, long a2)
Definition: Native.java:1919
static long mkTrue(long a0)
Definition: Native.java:1046
Tactic mkTactic(String name)
Definition: Context.java:2382
static long mkFpaSort128(long a0)
Definition: Native.java:5485
static long mkMul(long a0, int a1, long[] a2)
Definition: Native.java:1154
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
Definition: Native.java:5809
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3059
static long mkReal(long a0, int a1, int a2)
Definition: Native.java:1865
FPSort mkFPSort(int ebits, int sbits)
Definition: Context.java:2895
static long tacticAndThen(long a0, long a1, long a2)
Definition: Native.java:3867
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
Definition: Context.java:1638
BitVecSort mkBitVecSort(int size)
Definition: Context.java:176
static long mkFpaLt(long a0, long a1, long a2)
Definition: Native.java:5692
ParamDescrs getSimplifyParameterDescriptions()
Definition: Context.java:3605
Fixedpoint mkFixedpoint()
Definition: Context.java:2784
static long mkBvxnor(long a0, long a1, long a2)
Definition: Native.java:1352
BoolExpr[] getSMTLIBFormulas()
Definition: Context.java:2198
Tactic parOr(Tactic...t)
Definition: Context.java:2554
static long mkFpaMax(long a0, long a1, long a2)
Definition: Native.java:5674
static long mkFpaSub(long a0, long a1, long a2, long a3)
Definition: Native.java:5602
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3119
BoolExpr mkFPIsNormal(FPExpr t)
Definition: Context.java:3326
static long mkSetUnion(long a0, int a1, long[] a2)
Definition: Native.java:1802
Tactic cond(Probe p, Tactic t1, Tactic t2)
Definition: Context.java:2472
static long mkPower(long a0, long a1, long a2)
Definition: Native.java:1208
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1119
static long mkFpaIsZero(long a0, long a1)
Definition: Native.java:5746
Solver mkSolver(Symbol logic)
Definition: Context.java:2741
def Map(f, args)
Definition: z3py.py:4063
FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
Definition: Context.java:3420
FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
Definition: Context.java:403
ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
Definition: Context.java:1593
static long mkBvor(long a0, long a1, long a2)
Definition: Native.java:1316
BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3292
static long getSmtlibFormula(long a0, int a1)
Definition: Native.java:3155
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:184
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:486
BitVecNum mkBV(int v, int size)
Definition: Context.java:1986
static long mkBv2int(long a0, long a1, boolean a2)
Definition: Native.java:1631
BoolExpr mkNot(BoolExpr a)
Definition: Context.java:648
Expr mkNumeral(long v, Sort ty)
Definition: Context.java:1871
DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
Definition: Context.java:358
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:838
FPRMSort mkFPRoundingModeSort()
Definition: Context.java:2794
ListSort mkListSort(Symbol name, Sort elemSort)
Definition: Context.java:227
static long mkFpaRoundTowardZero(long a0)
Definition: Native.java:5395
Tactic orElse(Tactic t1, Tactic t2)
Definition: Context.java:2432
Expr mkConst(FuncDecl f)
Definition: Context.java:521
Probe le(Probe p1, Probe p2)
Definition: Context.java:2658
ArithExpr mkUnaryMinus(ArithExpr t)
Definition: Context.java:756
EnumSort mkEnumSort(Symbol name, Symbol...enumNames)
Definition: Context.java:207
static long probeAnd(long a0, long a1, long a2)
Definition: Native.java:4038
RealExpr mkInt2Real(IntExpr t)
Definition: Context.java:867
RealExpr mkRealConst(Symbol name)
Definition: Context.java:561
static long mkBvmul(long a0, long a1, long a2)
Definition: Native.java:1388
static long mkFpaSortQuadruple(long a0)
Definition: Native.java:5476
def FPSort
Definition: z3py.py:7920
Expr mkSetSubset(Expr arg1, Expr arg2)
Definition: Context.java:1817
FuncDecl mkFreshConstDecl(String prefix, Sort range)
Definition: Context.java:451
Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2086
static long mkFpaNumeralDouble(long a0, double a1, long a2)
Definition: Native.java:5539
BitVecNum mkBV(String v, int size)
Definition: Context.java:1976
Solver mkSolver(Tactic t)
Definition: Context.java:2774
ArithExpr mkMul(ArithExpr...t)
Definition: Context.java:736
String getTacticDescription(String name)
Definition: Context.java:2374
Expr mkSelect(ArrayExpr a, Expr i)
Definition: Context.java:1612
static long mkFpaFma(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:5629
static long mkReal2int(long a0, long a1)
Definition: Native.java:1262
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
Definition: Context.java:418
static long mkFpaSortHalf(long a0)
Definition: Native.java:5422
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
Definition: Native.java:5836
BitVecNum mkBV(long v, int size)
Definition: Context.java:1996
BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1037
static long tacticWhen(long a0, long a1, long a2)
Definition: Native.java:3912
ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
Definition: Context.java:766
RealExpr mkRealConst(String name)
Definition: Context.java:569
static long mkNot(long a0, long a1)
Definition: Native.java:1082
static long mkBvSort(long a0, int a1)
Definition: Native.java:888
FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Definition: Context.java:3452
static long mkFpaSort32(long a0)
Definition: Native.java:5449
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1255
RatNum mkReal(int num, int den)
Definition: Context.java:1887
BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
Definition: Context.java:3303
BitVecExpr mkSignExt(int i, BitVecExpr t)
Definition: Context.java:1286
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1224
Expr mkEmptySet(Sort domain)
Definition: Context.java:1711
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
Definition: Context.java:1461
static long mkIsInt(long a0, long a1)
Definition: Native.java:1271
FPRMNum mkFPRoundTowardZero()
Definition: Context.java:2875
Pattern mkPattern(Expr...terms)
Definition: Context.java:472
static long mkFpaLeq(long a0, long a1, long a2)
Definition: Native.java:5683
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3121
BoolExpr mkEq(Expr x, Expr y)
Definition: Context.java:627
static long mkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:5926
static long mkBvsubNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1658
static long mkIff(long a0, long a1, long a2)
Definition: Native.java:1100
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:849
BoolExpr mkFPIsZero(FPExpr t)
Definition: Context.java:3346
FuncDecl[] getSMTLIBDecls()
Definition: Context.java:2246
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2020
IDecRefQueue getProbeDRQ()
Definition: Context.java:3715
Tactic andThen(Tactic t1, Tactic t2, Tactic...ts)
Definition: Context.java:2391
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
Definition: Context.java:2335
IDecRefQueue getFixedpointDRQ()
Definition: Context.java:3735
static long tacticCond(long a0, long a1, long a2, long a3)
Definition: Native.java:3921
IDecRefQueue getFuncEntryDRQ()
Definition: Context.java:3685
static long mkFpaZero(long a0, long a1, boolean a2)
Definition: Native.java:5512
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1473
static long mkBvnor(long a0, long a1, long a2)
Definition: Native.java:1343