Z3
Context.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
20 import static com.microsoft.z3.Constructor.of;
21 
23 
24 import java.util.Map;
25 
29 public class Context implements AutoCloseable {
30  private final long m_ctx;
31  static final Object creation_lock = new Object();
32 
33  public Context () {
34  m_ctx = Native.mkContextRc(0);
35  init();
36  }
37 
38  protected Context (long m_ctx) {
39  this.m_ctx = m_ctx;
40  init();
41  }
42 
43 
61  public Context(Map<String, String> settings) {
62  long cfg = Native.mkConfig();
63  for (Map.Entry<String, String> kv : settings.entrySet()) {
64  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
65  }
66  m_ctx = Native.mkContextRc(cfg);
67  Native.delConfig(cfg);
68  init();
69  }
70 
71  private void init() {
74  }
75 
81  public IntSymbol mkSymbol(int i)
82  {
83  return new IntSymbol(this, i);
84  }
85 
90  {
91  return new StringSymbol(this, name);
92  }
93 
97  Symbol[] mkSymbols(String[] names)
98  {
99  if (names == null)
100  return null;
101  Symbol[] result = new Symbol[names.length];
102  for (int i = 0; i < names.length; ++i)
103  result[i] = mkSymbol(names[i]);
104  return result;
105  }
106 
107  private BoolSort m_boolSort = null;
108  private IntSort m_intSort = null;
109  private RealSort m_realSort = null;
110  private SeqSort m_stringSort = null;
111 
116  {
117  if (m_boolSort == null) {
118  m_boolSort = new BoolSort(this);
119  }
120  return m_boolSort;
121  }
122 
127  {
128  if (m_intSort == null) {
129  m_intSort = new IntSort(this);
130  }
131  return m_intSort;
132  }
133 
138  {
139  if (m_realSort == null) {
140  m_realSort = new RealSort(this);
141  }
142  return m_realSort;
143  }
144 
149  {
150  return new BoolSort(this);
151  }
152 
157  {
158  if (m_stringSort == null) {
159  m_stringSort = mkStringSort();
160  }
161  return m_stringSort;
162  }
163 
168  {
169  checkContextMatch(s);
170  return new UninterpretedSort(this, s);
171  }
172 
177  {
178  return mkUninterpretedSort(mkSymbol(str));
179  }
180 
185  {
186  return new IntSort(this);
187  }
188 
193  {
194  return new RealSort(this);
195  }
196 
200  public BitVecSort mkBitVecSort(int size)
201  {
202  return new BitVecSort(this, Native.mkBvSort(nCtx(), size));
203  }
204 
208  public ArraySort mkArraySort(Sort domain, Sort range)
209  {
210  checkContextMatch(domain);
211  checkContextMatch(range);
212  return new ArraySort(this, domain, range);
213  }
214 
219  {
220  return new SeqSort(this, Native.mkStringSort(nCtx()));
221  }
222 
227  {
228  return new SeqSort(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
229  }
230 
234  public ReSort mkReSort(Sort s)
235  {
236  return new ReSort(this, Native.mkReSort(nCtx(), s.getNativeObject()));
237  }
238 
239 
243  public TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames,
244  Sort[] fieldSorts)
245  {
246  checkContextMatch(name);
247  checkContextMatch(fieldNames);
248  checkContextMatch(fieldSorts);
249  return new TupleSort(this, name, fieldNames.length, fieldNames,
250  fieldSorts);
251  }
252 
256  public EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
257 
258  {
259  checkContextMatch(name);
260  checkContextMatch(enumNames);
261  return new EnumSort(this, name, enumNames);
262  }
263 
267  public EnumSort mkEnumSort(String name, String... enumNames)
268 
269  {
270  return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
271  }
272 
276  public ListSort mkListSort(Symbol name, Sort elemSort)
277  {
278  checkContextMatch(name);
279  checkContextMatch(elemSort);
280  return new ListSort(this, name, elemSort);
281  }
282 
286  public ListSort mkListSort(String name, Sort elemSort)
287  {
288  checkContextMatch(elemSort);
289  return new ListSort(this, mkSymbol(name), elemSort);
290  }
291 
296 
297  {
298  checkContextMatch(name);
299  return new FiniteDomainSort(this, name, size);
300  }
301 
306 
307  {
308  return new FiniteDomainSort(this, mkSymbol(name), size);
309  }
310 
322  public Constructor mkConstructor(Symbol name, Symbol recognizer,
323  Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
324 
325  {
326  return of(this, name, recognizer, fieldNames, sorts,
327  sortRefs);
328  }
329 
333  public Constructor mkConstructor(String name, String recognizer,
334  String[] fieldNames, Sort[] sorts, int[] sortRefs)
335  {
336  return of(this, mkSymbol(name), mkSymbol(recognizer),
337  mkSymbols(fieldNames), sorts, sortRefs);
338  }
339 
343  public DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
344 
345  {
346  checkContextMatch(name);
347  checkContextMatch(constructors);
348  return new DatatypeSort(this, name, constructors);
349  }
350 
354  public DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
355 
356  {
357  checkContextMatch(constructors);
358  return new DatatypeSort(this, mkSymbol(name), constructors);
359  }
360 
367 
368  {
369  checkContextMatch(names);
370  int n = names.length;
371  ConstructorList[] cla = new ConstructorList[n];
372  long[] n_constr = new long[n];
373  for (int i = 0; i < n; i++)
374  {
375  Constructor[] constructor = c[i];
376 
377  checkContextMatch(constructor);
378  cla[i] = new ConstructorList(this, constructor);
379  n_constr[i] = cla[i].getNativeObject();
380  }
381  long[] n_res = new long[n];
382  Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res,
383  n_constr);
384  DatatypeSort[] res = new DatatypeSort[n];
385  for (int i = 0; i < n; i++)
386  res[i] = new DatatypeSort(this, n_res[i]);
387  return res;
388  }
389 
394 
395  {
396  return mkDatatypeSorts(mkSymbols(names), c);
397  }
398 
405  public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
406  throws Z3Exception
407  {
408  return Expr.create (this,
410  (nCtx(), field.getNativeObject(),
411  t.getNativeObject(), v.getNativeObject()));
412  }
413 
414 
418  public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
419 
420  {
421  checkContextMatch(name);
422  checkContextMatch(domain);
423  checkContextMatch(range);
424  return new FuncDecl(this, name, domain, range);
425  }
426 
430  public FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
431 
432  {
433  checkContextMatch(name);
434  checkContextMatch(domain);
435  checkContextMatch(range);
436  Sort[] q = new Sort[] { domain };
437  return new FuncDecl(this, name, q, range);
438  }
439 
443  public FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
444 
445  {
446  checkContextMatch(domain);
447  checkContextMatch(range);
448  return new FuncDecl(this, mkSymbol(name), domain, range);
449  }
450 
454  public FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
455 
456  {
457  checkContextMatch(domain);
458  checkContextMatch(range);
459  Sort[] q = new Sort[] { domain };
460  return new FuncDecl(this, mkSymbol(name), q, range);
461  }
462 
469  public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
470 
471  {
472  checkContextMatch(domain);
473  checkContextMatch(range);
474  return new FuncDecl(this, prefix, domain, range);
475  }
476 
480  public FuncDecl mkConstDecl(Symbol name, Sort range)
481  {
482  checkContextMatch(name);
483  checkContextMatch(range);
484  return new FuncDecl(this, name, null, range);
485  }
486 
490  public FuncDecl mkConstDecl(String name, Sort range)
491  {
492  checkContextMatch(range);
493  return new FuncDecl(this, mkSymbol(name), null, range);
494  }
495 
502  public FuncDecl mkFreshConstDecl(String prefix, Sort range)
503 
504  {
505  checkContextMatch(range);
506  return new FuncDecl(this, prefix, null, range);
507  }
508 
514  public Expr mkBound(int index, Sort ty)
515  {
516  return Expr.create(this,
517  Native.mkBound(nCtx(), index, ty.getNativeObject()));
518  }
519 
523  public Pattern mkPattern(Expr... terms)
524  {
525  if (terms.length == 0)
526  throw new Z3Exception("Cannot create a pattern from zero terms");
527 
528  long[] termsNative = AST.arrayToNative(terms);
529  return new Pattern(this, Native.mkPattern(nCtx(), terms.length,
530  termsNative));
531  }
532 
537  public Expr mkConst(Symbol name, Sort range)
538  {
539  checkContextMatch(name);
540  checkContextMatch(range);
541 
542  return Expr.create(
543  this,
544  Native.mkConst(nCtx(), name.getNativeObject(),
545  range.getNativeObject()));
546  }
547 
552  public Expr mkConst(String name, Sort range)
553  {
554  return mkConst(mkSymbol(name), range);
555  }
556 
561  public Expr mkFreshConst(String prefix, Sort range)
562  {
563  checkContextMatch(range);
564  return Expr.create(this,
565  Native.mkFreshConst(nCtx(), prefix, range.getNativeObject()));
566  }
567 
573  {
574  return mkApp(f, (Expr[]) null);
575  }
576 
581  {
582  return (BoolExpr) mkConst(name, getBoolSort());
583  }
584 
589  {
590  return (BoolExpr) mkConst(mkSymbol(name), getBoolSort());
591  }
592 
596  public IntExpr mkIntConst(Symbol name)
597  {
598  return (IntExpr) mkConst(name, getIntSort());
599  }
600 
604  public IntExpr mkIntConst(String name)
605  {
606  return (IntExpr) mkConst(name, getIntSort());
607  }
608 
613  {
614  return (RealExpr) mkConst(name, getRealSort());
615  }
616 
621  {
622  return (RealExpr) mkConst(name, getRealSort());
623  }
624 
628  public BitVecExpr mkBVConst(Symbol name, int size)
629  {
630  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
631  }
632 
636  public BitVecExpr mkBVConst(String name, int size)
637  {
638  return (BitVecExpr) mkConst(name, mkBitVecSort(size));
639  }
640 
644  public Expr mkApp(FuncDecl f, Expr... args)
645  {
646  checkContextMatch(f);
647  checkContextMatch(args);
648  return Expr.create(this, f, args);
649  }
650 
654  public BoolExpr mkTrue()
655  {
656  return new BoolExpr(this, Native.mkTrue(nCtx()));
657  }
658 
662  public BoolExpr mkFalse()
663  {
664  return new BoolExpr(this, Native.mkFalse(nCtx()));
665  }
666 
670  public BoolExpr mkBool(boolean value)
671  {
672  return value ? mkTrue() : mkFalse();
673  }
674 
678  public BoolExpr mkEq(Expr x, Expr y)
679  {
680  checkContextMatch(x);
681  checkContextMatch(y);
682  return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(),
683  y.getNativeObject()));
684  }
685 
689  public BoolExpr mkDistinct(Expr... args)
690  {
691  checkContextMatch(args);
692  return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length,
693  AST.arrayToNative(args)));
694  }
695 
700  {
701  checkContextMatch(a);
702  return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject()));
703  }
704 
712  public Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
713  {
714  checkContextMatch(t1);
715  checkContextMatch(t2);
716  checkContextMatch(t3);
717  return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
718  t2.getNativeObject(), t3.getNativeObject()));
719  }
720 
725  {
726  checkContextMatch(t1);
727  checkContextMatch(t2);
728  return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(),
729  t2.getNativeObject()));
730  }
731 
736  {
737  checkContextMatch(t1);
738  checkContextMatch(t2);
739  return new BoolExpr(this, Native.mkImplies(nCtx(),
740  t1.getNativeObject(), t2.getNativeObject()));
741  }
742 
747  {
748  checkContextMatch(t1);
749  checkContextMatch(t2);
750  return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(),
751  t2.getNativeObject()));
752  }
753 
757  public BoolExpr mkAnd(BoolExpr... t)
758  {
759  checkContextMatch(t);
760  return new BoolExpr(this, Native.mkAnd(nCtx(), t.length,
761  AST.arrayToNative(t)));
762  }
763 
767  public BoolExpr mkOr(BoolExpr... t)
768  {
769  checkContextMatch(t);
770  return new BoolExpr(this, Native.mkOr(nCtx(), t.length,
771  AST.arrayToNative(t)));
772  }
773 
777  public ArithExpr mkAdd(ArithExpr... t)
778  {
779  checkContextMatch(t);
780  return (ArithExpr) Expr.create(this,
781  Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t)));
782  }
783 
787  public ArithExpr mkMul(ArithExpr... t)
788  {
789  checkContextMatch(t);
790  return (ArithExpr) Expr.create(this,
791  Native.mkMul(nCtx(), t.length, AST.arrayToNative(t)));
792  }
793 
797  public ArithExpr mkSub(ArithExpr... t)
798  {
799  checkContextMatch(t);
800  return (ArithExpr) Expr.create(this,
801  Native.mkSub(nCtx(), t.length, AST.arrayToNative(t)));
802  }
803 
808  {
809  checkContextMatch(t);
810  return (ArithExpr) Expr.create(this,
811  Native.mkUnaryMinus(nCtx(), t.getNativeObject()));
812  }
813 
818  {
819  checkContextMatch(t1);
820  checkContextMatch(t2);
821  return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(),
822  t1.getNativeObject(), t2.getNativeObject()));
823  }
824 
830  public IntExpr mkMod(IntExpr t1, IntExpr t2)
831  {
832  checkContextMatch(t1);
833  checkContextMatch(t2);
834  return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(),
835  t2.getNativeObject()));
836  }
837 
843  public IntExpr mkRem(IntExpr t1, IntExpr t2)
844  {
845  checkContextMatch(t1);
846  checkContextMatch(t2);
847  return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(),
848  t2.getNativeObject()));
849  }
850 
855  {
856  checkContextMatch(t1);
857  checkContextMatch(t2);
858  return (ArithExpr) Expr.create(
859  this,
860  Native.mkPower(nCtx(), t1.getNativeObject(),
861  t2.getNativeObject()));
862  }
863 
868  {
869  checkContextMatch(t1);
870  checkContextMatch(t2);
871  return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(),
872  t2.getNativeObject()));
873  }
874 
879  {
880  checkContextMatch(t1);
881  checkContextMatch(t2);
882  return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(),
883  t2.getNativeObject()));
884  }
885 
890  {
891  checkContextMatch(t1);
892  checkContextMatch(t2);
893  return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(),
894  t2.getNativeObject()));
895  }
896 
901  {
902  checkContextMatch(t1);
903  checkContextMatch(t2);
904  return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(),
905  t2.getNativeObject()));
906  }
907 
919  {
920  checkContextMatch(t);
921  return new RealExpr(this,
922  Native.mkInt2real(nCtx(), t.getNativeObject()));
923  }
924 
932  {
933  checkContextMatch(t);
934  return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject()));
935  }
936 
941  {
942  checkContextMatch(t);
943  return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
944  }
945 
952  {
953  checkContextMatch(t);
954  return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject()));
955  }
956 
963  {
964  checkContextMatch(t);
965  return new BitVecExpr(this, Native.mkBvredand(nCtx(),
966  t.getNativeObject()));
967  }
968 
975  {
976  checkContextMatch(t);
977  return new BitVecExpr(this, Native.mkBvredor(nCtx(),
978  t.getNativeObject()));
979  }
980 
987  {
988  checkContextMatch(t1);
989  checkContextMatch(t2);
990  return new BitVecExpr(this, Native.mkBvand(nCtx(),
991  t1.getNativeObject(), t2.getNativeObject()));
992  }
993 
1000  {
1001  checkContextMatch(t1);
1002  checkContextMatch(t2);
1003  return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(),
1004  t2.getNativeObject()));
1005  }
1006 
1013  {
1014  checkContextMatch(t1);
1015  checkContextMatch(t2);
1016  return new BitVecExpr(this, Native.mkBvxor(nCtx(),
1017  t1.getNativeObject(), t2.getNativeObject()));
1018  }
1019 
1026  {
1027  checkContextMatch(t1);
1028  checkContextMatch(t2);
1029  return new BitVecExpr(this, Native.mkBvnand(nCtx(),
1030  t1.getNativeObject(), t2.getNativeObject()));
1031  }
1032 
1039  {
1040  checkContextMatch(t1);
1041  checkContextMatch(t2);
1042  return new BitVecExpr(this, Native.mkBvnor(nCtx(),
1043  t1.getNativeObject(), t2.getNativeObject()));
1044  }
1045 
1052  {
1053  checkContextMatch(t1);
1054  checkContextMatch(t2);
1055  return new BitVecExpr(this, Native.mkBvxnor(nCtx(),
1056  t1.getNativeObject(), t2.getNativeObject()));
1057  }
1058 
1065  {
1066  checkContextMatch(t);
1067  return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject()));
1068  }
1069 
1076  {
1077  checkContextMatch(t1);
1078  checkContextMatch(t2);
1079  return new BitVecExpr(this, Native.mkBvadd(nCtx(),
1080  t1.getNativeObject(), t2.getNativeObject()));
1081  }
1082 
1089  {
1090  checkContextMatch(t1);
1091  checkContextMatch(t2);
1092  return new BitVecExpr(this, Native.mkBvsub(nCtx(),
1093  t1.getNativeObject(), t2.getNativeObject()));
1094  }
1095 
1102  {
1103  checkContextMatch(t1);
1104  checkContextMatch(t2);
1105  return new BitVecExpr(this, Native.mkBvmul(nCtx(),
1106  t1.getNativeObject(), t2.getNativeObject()));
1107  }
1108 
1117  {
1118  checkContextMatch(t1);
1119  checkContextMatch(t2);
1120  return new BitVecExpr(this, Native.mkBvudiv(nCtx(),
1121  t1.getNativeObject(), t2.getNativeObject()));
1122  }
1123 
1138  {
1139  checkContextMatch(t1);
1140  checkContextMatch(t2);
1141  return new BitVecExpr(this, Native.mkBvsdiv(nCtx(),
1142  t1.getNativeObject(), t2.getNativeObject()));
1143  }
1144 
1153  {
1154  checkContextMatch(t1);
1155  checkContextMatch(t2);
1156  return new BitVecExpr(this, Native.mkBvurem(nCtx(),
1157  t1.getNativeObject(), t2.getNativeObject()));
1158  }
1159 
1171  {
1172  checkContextMatch(t1);
1173  checkContextMatch(t2);
1174  return new BitVecExpr(this, Native.mkBvsrem(nCtx(),
1175  t1.getNativeObject(), t2.getNativeObject()));
1176  }
1177 
1185  {
1186  checkContextMatch(t1);
1187  checkContextMatch(t2);
1188  return new BitVecExpr(this, Native.mkBvsmod(nCtx(),
1189  t1.getNativeObject(), t2.getNativeObject()));
1190  }
1191 
1198  {
1199  checkContextMatch(t1);
1200  checkContextMatch(t2);
1201  return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(),
1202  t2.getNativeObject()));
1203  }
1204 
1211  {
1212  checkContextMatch(t1);
1213  checkContextMatch(t2);
1214  return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(),
1215  t2.getNativeObject()));
1216  }
1217 
1224  {
1225  checkContextMatch(t1);
1226  checkContextMatch(t2);
1227  return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(),
1228  t2.getNativeObject()));
1229  }
1230 
1237  {
1238  checkContextMatch(t1);
1239  checkContextMatch(t2);
1240  return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(),
1241  t2.getNativeObject()));
1242  }
1243 
1250  {
1251  checkContextMatch(t1);
1252  checkContextMatch(t2);
1253  return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(),
1254  t2.getNativeObject()));
1255  }
1256 
1263  {
1264  checkContextMatch(t1);
1265  checkContextMatch(t2);
1266  return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(),
1267  t2.getNativeObject()));
1268  }
1269 
1276  {
1277  checkContextMatch(t1);
1278  checkContextMatch(t2);
1279  return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(),
1280  t2.getNativeObject()));
1281  }
1282 
1289  {
1290  checkContextMatch(t1);
1291  checkContextMatch(t2);
1292  return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(),
1293  t2.getNativeObject()));
1294  }
1295 
1307  {
1308  checkContextMatch(t1);
1309  checkContextMatch(t2);
1310  return new BitVecExpr(this, Native.mkConcat(nCtx(),
1311  t1.getNativeObject(), t2.getNativeObject()));
1312  }
1313 
1322  public BitVecExpr mkExtract(int high, int low, BitVecExpr t)
1323 
1324  {
1325  checkContextMatch(t);
1326  return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low,
1327  t.getNativeObject()));
1328  }
1329 
1338  {
1339  checkContextMatch(t);
1340  return new BitVecExpr(this, Native.mkSignExt(nCtx(), i,
1341  t.getNativeObject()));
1342  }
1343 
1352  {
1353  checkContextMatch(t);
1354  return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i,
1355  t.getNativeObject()));
1356  }
1357 
1363  public BitVecExpr mkRepeat(int i, BitVecExpr t)
1364  {
1365  checkContextMatch(t);
1366  return new BitVecExpr(this, Native.mkRepeat(nCtx(), i,
1367  t.getNativeObject()));
1368  }
1369 
1382  {
1383  checkContextMatch(t1);
1384  checkContextMatch(t2);
1385  return new BitVecExpr(this, Native.mkBvshl(nCtx(),
1386  t1.getNativeObject(), t2.getNativeObject()));
1387  }
1388 
1401  {
1402  checkContextMatch(t1);
1403  checkContextMatch(t2);
1404  return new BitVecExpr(this, Native.mkBvlshr(nCtx(),
1405  t1.getNativeObject(), t2.getNativeObject()));
1406  }
1407 
1421  {
1422  checkContextMatch(t1);
1423  checkContextMatch(t2);
1424  return new BitVecExpr(this, Native.mkBvashr(nCtx(),
1425  t1.getNativeObject(), t2.getNativeObject()));
1426  }
1427 
1434  {
1435  checkContextMatch(t);
1436  return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i,
1437  t.getNativeObject()));
1438  }
1439 
1446  {
1447  checkContextMatch(t);
1448  return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i,
1449  t.getNativeObject()));
1450  }
1451 
1459 
1460  {
1461  checkContextMatch(t1);
1462  checkContextMatch(t2);
1463  return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(),
1464  t1.getNativeObject(), t2.getNativeObject()));
1465  }
1466 
1474 
1475  {
1476  checkContextMatch(t1);
1477  checkContextMatch(t2);
1478  return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(),
1479  t1.getNativeObject(), t2.getNativeObject()));
1480  }
1481 
1491  public BitVecExpr mkInt2BV(int n, IntExpr t)
1492  {
1493  checkContextMatch(t);
1494  return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n,
1495  t.getNativeObject()));
1496  }
1497 
1512  public IntExpr mkBV2Int(BitVecExpr t, boolean signed)
1513  {
1514  checkContextMatch(t);
1515  return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
1516  (signed)));
1517  }
1518 
1525  boolean isSigned)
1526  {
1527  checkContextMatch(t1);
1528  checkContextMatch(t2);
1529  return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
1530  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1531  }
1532 
1539 
1540  {
1541  checkContextMatch(t1);
1542  checkContextMatch(t2);
1543  return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(),
1544  t1.getNativeObject(), t2.getNativeObject()));
1545  }
1546 
1553 
1554  {
1555  checkContextMatch(t1);
1556  checkContextMatch(t2);
1557  return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(),
1558  t1.getNativeObject(), t2.getNativeObject()));
1559  }
1560 
1567  boolean isSigned)
1568  {
1569  checkContextMatch(t1);
1570  checkContextMatch(t2);
1571  return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
1572  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1573  }
1574 
1581 
1582  {
1583  checkContextMatch(t1);
1584  checkContextMatch(t2);
1585  return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(),
1586  t1.getNativeObject(), t2.getNativeObject()));
1587  }
1588 
1595  {
1596  checkContextMatch(t);
1597  return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(),
1598  t.getNativeObject()));
1599  }
1600 
1607  boolean isSigned)
1608  {
1609  checkContextMatch(t1);
1610  checkContextMatch(t2);
1611  return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
1612  .getNativeObject(), t2.getNativeObject(), (isSigned)));
1613  }
1614 
1621 
1622  {
1623  checkContextMatch(t1);
1624  checkContextMatch(t2);
1625  return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(),
1626  t1.getNativeObject(), t2.getNativeObject()));
1627  }
1628 
1632  public ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
1633 
1634  {
1635  return (ArrayExpr) mkConst(name, mkArraySort(domain, range));
1636  }
1637 
1641  public ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
1642 
1643  {
1644  return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range));
1645  }
1646 
1661  {
1662  checkContextMatch(a);
1663  checkContextMatch(i);
1664  return Expr.create(
1665  this,
1666  Native.mkSelect(nCtx(), a.getNativeObject(),
1667  i.getNativeObject()));
1668  }
1669 
1687  {
1688  checkContextMatch(a);
1689  checkContextMatch(i);
1690  checkContextMatch(v);
1691  return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(),
1692  i.getNativeObject(), v.getNativeObject()));
1693  }
1694 
1704  public ArrayExpr mkConstArray(Sort domain, Expr v)
1705  {
1706  checkContextMatch(domain);
1707  checkContextMatch(v);
1708  return new ArrayExpr(this, Native.mkConstArray(nCtx(),
1709  domain.getNativeObject(), v.getNativeObject()));
1710  }
1711 
1725  public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
1726  {
1727  checkContextMatch(f);
1728  checkContextMatch(args);
1729  return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(),
1730  f.getNativeObject(), AST.arrayLength(args),
1731  AST.arrayToNative(args)));
1732  }
1733 
1741  {
1742  checkContextMatch(array);
1743  return Expr.create(this,
1744  Native.mkArrayDefault(nCtx(), array.getNativeObject()));
1745  }
1746 
1750  public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
1751  {
1752  checkContextMatch(arg1);
1753  checkContextMatch(arg2);
1754  return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
1755  }
1756 
1757 
1762  {
1763  checkContextMatch(ty);
1764  return new SetSort(this, ty);
1765  }
1766 
1770  public ArrayExpr mkEmptySet(Sort domain)
1771  {
1772  checkContextMatch(domain);
1773  return (ArrayExpr)Expr.create(this,
1774  Native.mkEmptySet(nCtx(), domain.getNativeObject()));
1775  }
1776 
1780  public ArrayExpr mkFullSet(Sort domain)
1781  {
1782  checkContextMatch(domain);
1783  return (ArrayExpr)Expr.create(this,
1784  Native.mkFullSet(nCtx(), domain.getNativeObject()));
1785  }
1786 
1790  public ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
1791  {
1792  checkContextMatch(set);
1793  checkContextMatch(element);
1794  return (ArrayExpr)Expr.create(this,
1795  Native.mkSetAdd(nCtx(), set.getNativeObject(),
1796  element.getNativeObject()));
1797  }
1798 
1802  public ArrayExpr mkSetDel(ArrayExpr set, Expr element)
1803  {
1804  checkContextMatch(set);
1805  checkContextMatch(element);
1806  return (ArrayExpr)Expr.create(this,
1807  Native.mkSetDel(nCtx(), set.getNativeObject(),
1808  element.getNativeObject()));
1809  }
1810 
1815  {
1816  checkContextMatch(args);
1817  return (ArrayExpr)Expr.create(this,
1818  Native.mkSetUnion(nCtx(), args.length,
1819  AST.arrayToNative(args)));
1820  }
1821 
1826  {
1827  checkContextMatch(args);
1828  return (ArrayExpr)Expr.create(this,
1829  Native.mkSetIntersect(nCtx(), args.length,
1830  AST.arrayToNative(args)));
1831  }
1832 
1837  {
1838  checkContextMatch(arg1);
1839  checkContextMatch(arg2);
1840  return (ArrayExpr)Expr.create(this,
1841  Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
1842  arg2.getNativeObject()));
1843  }
1844 
1849  {
1850  checkContextMatch(arg);
1851  return (ArrayExpr)Expr.create(this,
1852  Native.mkSetComplement(nCtx(), arg.getNativeObject()));
1853  }
1854 
1859  {
1860  checkContextMatch(elem);
1861  checkContextMatch(set);
1862  return (BoolExpr) Expr.create(this,
1863  Native.mkSetMember(nCtx(), elem.getNativeObject(),
1864  set.getNativeObject()));
1865  }
1866 
1871  {
1872  checkContextMatch(arg1);
1873  checkContextMatch(arg2);
1874  return (BoolExpr) Expr.create(this,
1875  Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
1876  arg2.getNativeObject()));
1877  }
1878 
1879 
1888  {
1889  checkContextMatch(s);
1890  return new SeqExpr(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
1891  }
1892 
1896  public SeqExpr MkUnit(Expr elem)
1897  {
1898  checkContextMatch(elem);
1899  return new SeqExpr(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
1900  }
1901 
1906  {
1907  return new SeqExpr(this, Native.mkString(nCtx(), s));
1908  }
1909 
1913  public SeqExpr MkConcat(SeqExpr... t)
1914  {
1915  checkContextMatch(t);
1916  return new SeqExpr(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
1917  }
1918 
1919 
1924  {
1925  checkContextMatch(s);
1926  return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
1927  }
1928 
1933  {
1934  checkContextMatch(s1, s2);
1935  return new BoolExpr(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
1936  }
1937 
1942  {
1943  checkContextMatch(s1, s2);
1944  return new BoolExpr(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
1945  }
1946 
1951  {
1952  checkContextMatch(s1, s2);
1953  return new BoolExpr(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
1954  }
1955 
1959  public SeqExpr MkAt(SeqExpr s, IntExpr index)
1960  {
1961  checkContextMatch(s, index);
1962  return new SeqExpr(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
1963  }
1964 
1968  public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
1969  {
1970  checkContextMatch(s, offset, length);
1971  return new SeqExpr(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
1972  }
1973 
1977  public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
1978  {
1979  checkContextMatch(s, substr, offset);
1980  return new IntExpr(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
1981  }
1982 
1987  {
1988  checkContextMatch(s, src, dst);
1989  return new SeqExpr(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
1990  }
1991 
1995  public ReExpr MkToRe(SeqExpr s)
1996  {
1997  checkContextMatch(s);
1998  return new ReExpr(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
1999  }
2000 
2001 
2006  {
2007  checkContextMatch(s, re);
2008  return new BoolExpr(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
2009  }
2010 
2014  public ReExpr MkStar(ReExpr re)
2015  {
2016  checkContextMatch(re);
2017  return new ReExpr(this, Native.mkReStar(nCtx(), re.getNativeObject()));
2018  }
2019 
2023  public ReExpr MPlus(ReExpr re)
2024  {
2025  checkContextMatch(re);
2026  return new ReExpr(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
2027  }
2028 
2032  public ReExpr MOption(ReExpr re)
2033  {
2034  checkContextMatch(re);
2035  return new ReExpr(this, Native.mkReOption(nCtx(), re.getNativeObject()));
2036  }
2037 
2041  public ReExpr MkConcat(ReExpr... t)
2042  {
2043  checkContextMatch(t);
2044  return new ReExpr(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
2045  }
2046 
2050  public ReExpr MkUnion(ReExpr... t)
2051  {
2052  checkContextMatch(t);
2053  return new ReExpr(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
2054  }
2055 
2056 
2068  public Expr mkNumeral(String v, Sort ty)
2069  {
2070  checkContextMatch(ty);
2071  return Expr.create(this,
2072  Native.mkNumeral(nCtx(), v, ty.getNativeObject()));
2073  }
2074 
2085  public Expr mkNumeral(int v, Sort ty)
2086  {
2087  checkContextMatch(ty);
2088  return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject()));
2089  }
2090 
2101  public Expr mkNumeral(long v, Sort ty)
2102  {
2103  checkContextMatch(ty);
2104  return Expr.create(this,
2105  Native.mkInt64(nCtx(), v, ty.getNativeObject()));
2106  }
2107 
2117  public RatNum mkReal(int num, int den)
2118  {
2119  if (den == 0) {
2120  throw new Z3Exception("Denominator is zero");
2121  }
2122 
2123  return new RatNum(this, Native.mkReal(nCtx(), num, den));
2124  }
2125 
2133  {
2134 
2135  return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort()
2136  .getNativeObject()));
2137  }
2138 
2145  public RatNum mkReal(int v)
2146  {
2147 
2148  return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort()
2149  .getNativeObject()));
2150  }
2151 
2158  public RatNum mkReal(long v)
2159  {
2160 
2161  return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort()
2162  .getNativeObject()));
2163  }
2164 
2169  public IntNum mkInt(String v)
2170  {
2171 
2172  return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort()
2173  .getNativeObject()));
2174  }
2175 
2182  public IntNum mkInt(int v)
2183  {
2184 
2185  return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort()
2186  .getNativeObject()));
2187  }
2188 
2195  public IntNum mkInt(long v)
2196  {
2197 
2198  return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort()
2199  .getNativeObject()));
2200  }
2201 
2207  public BitVecNum mkBV(String v, int size)
2208  {
2209  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2210  }
2211 
2217  public BitVecNum mkBV(int v, int size)
2218  {
2219  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2220  }
2221 
2227  public BitVecNum mkBV(long v, int size)
2228  {
2229  return (BitVecNum) mkNumeral(v, mkBitVecSort(size));
2230  }
2231 
2257  public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
2258  int weight, Pattern[] patterns, Expr[] noPatterns,
2259  Symbol quantifierID, Symbol skolemID)
2260  {
2261 
2262  return Quantifier.of(this, true, sorts, names, body, weight, patterns,
2263  noPatterns, quantifierID, skolemID);
2264  }
2265 
2270  public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
2271  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2272  Symbol skolemID)
2273  {
2274 
2275  return Quantifier.of(this, true, boundConstants, body, weight,
2276  patterns, noPatterns, quantifierID, skolemID);
2277  }
2278 
2283  public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
2284  int weight, Pattern[] patterns, Expr[] noPatterns,
2285  Symbol quantifierID, Symbol skolemID)
2286  {
2287 
2288  return Quantifier.of(this, false, sorts, names, body, weight,
2289  patterns, noPatterns, quantifierID, skolemID);
2290  }
2291 
2296  public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
2297  Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
2298  Symbol skolemID)
2299  {
2300 
2301  return Quantifier.of(this, false, boundConstants, body, weight,
2302  patterns, noPatterns, quantifierID, skolemID);
2303  }
2304 
2309  public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
2310  Symbol[] names, Expr body, int weight, Pattern[] patterns,
2311  Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
2312 
2313  {
2314 
2315  if (universal)
2316  return mkForall(sorts, names, body, weight, patterns, noPatterns,
2317  quantifierID, skolemID);
2318  else
2319  return mkExists(sorts, names, body, weight, patterns, noPatterns,
2320  quantifierID, skolemID);
2321  }
2322 
2327  public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
2328  Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
2329  Symbol quantifierID, Symbol skolemID)
2330  {
2331 
2332  if (universal)
2333  return mkForall(boundConstants, body, weight, patterns, noPatterns,
2334  quantifierID, skolemID);
2335  else
2336  return mkExists(boundConstants, body, weight, patterns, noPatterns,
2337  quantifierID, skolemID);
2338  }
2339 
2354  public void setPrintMode(Z3_ast_print_mode value)
2355  {
2356  Native.setAstPrintMode(nCtx(), value.toInt());
2357  }
2358 
2373  String status, String attributes, BoolExpr[] assumptions,
2374  BoolExpr formula)
2375  {
2376 
2377  return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
2378  attributes, assumptions.length,
2379  AST.arrayToNative(assumptions), formula.getNativeObject());
2380  }
2381 
2391  public void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts,
2392  Symbol[] declNames, FuncDecl[] decls)
2393  {
2394  int csn = Symbol.arrayLength(sortNames);
2395  int cs = Sort.arrayLength(sorts);
2396  int cdn = Symbol.arrayLength(declNames);
2397  int cd = AST.arrayLength(decls);
2398  if (csn != cs || cdn != cd)
2399  throw new Z3Exception("Argument size mismatch");
2400  Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts),
2401  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2402  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2403  AST.arrayToNative(decls));
2404  }
2405 
2410  public void parseSMTLIBFile(String fileName, Symbol[] sortNames,
2411  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2412 
2413  {
2414  int csn = Symbol.arrayLength(sortNames);
2415  int cs = Sort.arrayLength(sorts);
2416  int cdn = Symbol.arrayLength(declNames);
2417  int cd = AST.arrayLength(decls);
2418  if (csn != cs || cdn != cd)
2419  throw new Z3Exception("Argument size mismatch");
2420  Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts),
2421  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2422  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2423  AST.arrayToNative(decls));
2424  }
2425 
2431  {
2432  return Native.getSmtlibNumFormulas(nCtx());
2433  }
2434 
2440  {
2441 
2442  int n = getNumSMTLIBFormulas();
2443  BoolExpr[] res = new BoolExpr[n];
2444  for (int i = 0; i < n; i++)
2445  res[i] = (BoolExpr) Expr.create(this,
2446  Native.getSmtlibFormula(nCtx(), i));
2447  return res;
2448  }
2449 
2455  {
2456  return Native.getSmtlibNumAssumptions(nCtx());
2457  }
2458 
2464  {
2465 
2466  int n = getNumSMTLIBAssumptions();
2467  BoolExpr[] res = new BoolExpr[n];
2468  for (int i = 0; i < n; i++)
2469  res[i] = (BoolExpr) Expr.create(this,
2470  Native.getSmtlibAssumption(nCtx(), i));
2471  return res;
2472  }
2473 
2478  public int getNumSMTLIBDecls()
2479  {
2480  return Native.getSmtlibNumDecls(nCtx());
2481  }
2482 
2488  {
2489 
2490  int n = getNumSMTLIBDecls();
2491  FuncDecl[] res = new FuncDecl[n];
2492  for (int i = 0; i < n; i++)
2493  res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i));
2494  return res;
2495  }
2496 
2501  public int getNumSMTLIBSorts()
2502  {
2503  return Native.getSmtlibNumSorts(nCtx());
2504  }
2505 
2511  {
2512 
2513  int n = getNumSMTLIBSorts();
2514  Sort[] res = new Sort[n];
2515  for (int i = 0; i < n; i++)
2516  res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i));
2517  return res;
2518  }
2519 
2527  public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
2528  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2529 
2530  {
2531 
2532  int csn = Symbol.arrayLength(sortNames);
2533  int cs = Sort.arrayLength(sorts);
2534  int cdn = Symbol.arrayLength(declNames);
2535  int cd = AST.arrayLength(decls);
2536  if (csn != cs || cdn != cd) {
2537  throw new Z3Exception("Argument size mismatch");
2538  }
2539  return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
2540  str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
2541  AST.arrayToNative(sorts), AST.arrayLength(decls),
2542  Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
2543  }
2544 
2549  public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
2550  Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
2551 
2552  {
2553  int csn = Symbol.arrayLength(sortNames);
2554  int cs = Sort.arrayLength(sorts);
2555  int cdn = Symbol.arrayLength(declNames);
2556  int cd = AST.arrayLength(decls);
2557  if (csn != cs || cdn != cd)
2558  throw new Z3Exception("Argument size mismatch");
2559  return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
2560  fileName, AST.arrayLength(sorts),
2561  Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
2562  AST.arrayLength(decls), Symbol.arrayToNative(declNames),
2563  AST.arrayToNative(decls)));
2564  }
2565 
2576  public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
2577 
2578  {
2579  return new Goal(this, models, unsatCores, proofs);
2580  }
2581 
2585  public Params mkParams()
2586  {
2587  return new Params(this);
2588  }
2589 
2593  public int getNumTactics()
2594  {
2595  return Native.getNumTactics(nCtx());
2596  }
2597 
2602  {
2603 
2604  int n = getNumTactics();
2605  String[] res = new String[n];
2606  for (int i = 0; i < n; i++)
2607  res[i] = Native.getTacticName(nCtx(), i);
2608  return res;
2609  }
2610 
2616  {
2617  return Native.tacticGetDescr(nCtx(), name);
2618  }
2619 
2623  public Tactic mkTactic(String name)
2624  {
2625  return new Tactic(this, name);
2626  }
2627 
2632  public Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
2633 
2634  {
2635  checkContextMatch(t1);
2636  checkContextMatch(t2);
2637  checkContextMatch(ts);
2638 
2639  long last = 0;
2640  if (ts != null && ts.length > 0)
2641  {
2642  last = ts[ts.length - 1].getNativeObject();
2643  for (int i = ts.length - 2; i >= 0; i--) {
2644  last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
2645  last);
2646  }
2647  }
2648  if (last != 0)
2649  {
2650  last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last);
2651  return new Tactic(this, Native.tacticAndThen(nCtx(),
2652  t1.getNativeObject(), last));
2653  } else
2654  return new Tactic(this, Native.tacticAndThen(nCtx(),
2655  t1.getNativeObject(), t2.getNativeObject()));
2656  }
2657 
2664  public Tactic then(Tactic t1, Tactic t2, Tactic... ts)
2665  {
2666  return andThen(t1, t2, ts);
2667  }
2668 
2674  public Tactic orElse(Tactic t1, Tactic t2)
2675  {
2676  checkContextMatch(t1);
2677  checkContextMatch(t2);
2678  return new Tactic(this, Native.tacticOrElse(nCtx(),
2679  t1.getNativeObject(), t2.getNativeObject()));
2680  }
2681 
2688  public Tactic tryFor(Tactic t, int ms)
2689  {
2690  checkContextMatch(t);
2691  return new Tactic(this, Native.tacticTryFor(nCtx(),
2692  t.getNativeObject(), ms));
2693  }
2694 
2701  public Tactic when(Probe p, Tactic t)
2702  {
2703  checkContextMatch(t);
2704  checkContextMatch(p);
2705  return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(),
2706  t.getNativeObject()));
2707  }
2708 
2714  public Tactic cond(Probe p, Tactic t1, Tactic t2)
2715  {
2716  checkContextMatch(p);
2717  checkContextMatch(t1);
2718  checkContextMatch(t2);
2719  return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(),
2720  t1.getNativeObject(), t2.getNativeObject()));
2721  }
2722 
2727  public Tactic repeat(Tactic t, int max)
2728  {
2729  checkContextMatch(t);
2730  return new Tactic(this, Native.tacticRepeat(nCtx(),
2731  t.getNativeObject(), max));
2732  }
2733 
2737  public Tactic skip()
2738  {
2739  return new Tactic(this, Native.tacticSkip(nCtx()));
2740  }
2741 
2745  public Tactic fail()
2746  {
2747  return new Tactic(this, Native.tacticFail(nCtx()));
2748  }
2749 
2754  public Tactic failIf(Probe p)
2755  {
2756  checkContextMatch(p);
2757  return new Tactic(this,
2758  Native.tacticFailIf(nCtx(), p.getNativeObject()));
2759  }
2760 
2766  {
2767  return new Tactic(this, Native.tacticFailIfNotDecided(nCtx()));
2768  }
2769 
2775  {
2776  checkContextMatch(t);
2777  checkContextMatch(p);
2778  return new Tactic(this, Native.tacticUsingParams(nCtx(),
2779  t.getNativeObject(), p.getNativeObject()));
2780  }
2781 
2788  public Tactic with(Tactic t, Params p)
2789  {
2790  return usingParams(t, p);
2791  }
2792 
2796  public Tactic parOr(Tactic... t)
2797  {
2798  checkContextMatch(t);
2799  return new Tactic(this, Native.tacticParOr(nCtx(),
2800  Tactic.arrayLength(t), Tactic.arrayToNative(t)));
2801  }
2802 
2808  {
2809  checkContextMatch(t1);
2810  checkContextMatch(t2);
2811  return new Tactic(this, Native.tacticParAndThen(nCtx(),
2812  t1.getNativeObject(), t2.getNativeObject()));
2813  }
2814 
2820  public void interrupt()
2821  {
2822  Native.interrupt(nCtx());
2823  }
2824 
2828  public int getNumProbes()
2829  {
2830  return Native.getNumProbes(nCtx());
2831  }
2832 
2837  {
2838 
2839  int n = getNumProbes();
2840  String[] res = new String[n];
2841  for (int i = 0; i < n; i++)
2842  res[i] = Native.getProbeName(nCtx(), i);
2843  return res;
2844  }
2845 
2851  {
2852  return Native.probeGetDescr(nCtx(), name);
2853  }
2854 
2858  public Probe mkProbe(String name)
2859  {
2860  return new Probe(this, name);
2861  }
2862 
2866  public Probe constProbe(double val)
2867  {
2868  return new Probe(this, Native.probeConst(nCtx(), val));
2869  }
2870 
2875  public Probe lt(Probe p1, Probe p2)
2876  {
2877  checkContextMatch(p1);
2878  checkContextMatch(p2);
2879  return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(),
2880  p2.getNativeObject()));
2881  }
2882 
2887  public Probe gt(Probe p1, Probe p2)
2888  {
2889  checkContextMatch(p1);
2890  checkContextMatch(p2);
2891  return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(),
2892  p2.getNativeObject()));
2893  }
2894 
2900  public Probe le(Probe p1, Probe p2)
2901  {
2902  checkContextMatch(p1);
2903  checkContextMatch(p2);
2904  return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(),
2905  p2.getNativeObject()));
2906  }
2907 
2913  public Probe ge(Probe p1, Probe p2)
2914  {
2915  checkContextMatch(p1);
2916  checkContextMatch(p2);
2917  return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(),
2918  p2.getNativeObject()));
2919  }
2920 
2925  public Probe eq(Probe p1, Probe p2)
2926  {
2927  checkContextMatch(p1);
2928  checkContextMatch(p2);
2929  return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(),
2930  p2.getNativeObject()));
2931  }
2932 
2936  public Probe and(Probe p1, Probe p2)
2937  {
2938  checkContextMatch(p1);
2939  checkContextMatch(p2);
2940  return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(),
2941  p2.getNativeObject()));
2942  }
2943 
2947  public Probe or(Probe p1, Probe p2)
2948  {
2949  checkContextMatch(p1);
2950  checkContextMatch(p2);
2951  return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(),
2952  p2.getNativeObject()));
2953  }
2954 
2958  public Probe not(Probe p)
2959  {
2960  checkContextMatch(p);
2961  return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject()));
2962  }
2963 
2971  public Solver mkSolver()
2972  {
2973  return mkSolver((Symbol) null);
2974  }
2975 
2983  public Solver mkSolver(Symbol logic)
2984  {
2985 
2986  if (logic == null)
2987  return new Solver(this, Native.mkSolver(nCtx()));
2988  else
2989  return new Solver(this, Native.mkSolverForLogic(nCtx(),
2990  logic.getNativeObject()));
2991  }
2992 
2997  public Solver mkSolver(String logic)
2998  {
2999  return mkSolver(mkSymbol(logic));
3000  }
3001 
3006  {
3007  return new Solver(this, Native.mkSimpleSolver(nCtx()));
3008  }
3009 
3017  {
3018 
3019  return new Solver(this, Native.mkSolverFromTactic(nCtx(),
3020  t.getNativeObject()));
3021  }
3022 
3027  {
3028  return new Fixedpoint(this);
3029  }
3030 
3035  {
3036  return new Optimize(this);
3037  }
3038 
3039 
3045  {
3046  return new FPRMSort(this);
3047  }
3048 
3054  {
3055  return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
3056  }
3057 
3062  public FPRMNum mkFPRNE()
3063  {
3064  return new FPRMNum(this, Native.mkFpaRne(nCtx()));
3065  }
3066 
3072  {
3073  return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
3074  }
3075 
3080  public FPRMNum mkFPRNA()
3081  {
3082  return new FPRMNum(this, Native.mkFpaRna(nCtx()));
3083  }
3084 
3090  {
3091  return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
3092  }
3093 
3098  public FPRMNum mkFPRTP()
3099  {
3100  return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
3101  }
3102 
3108  {
3109  return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
3110  }
3111 
3116  public FPRMNum mkFPRTN()
3117  {
3118  return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
3119  }
3120 
3126  {
3127  return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
3128  }
3129 
3134  public FPRMNum mkFPRTZ()
3135  {
3136  return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
3137  }
3138 
3145  public FPSort mkFPSort(int ebits, int sbits)
3146  {
3147  return new FPSort(this, ebits, sbits);
3148  }
3149 
3155  {
3156  return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
3157  }
3158 
3164  {
3165  return new FPSort(this, Native.mkFpaSort16(nCtx()));
3166  }
3167 
3173  {
3174  return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
3175  }
3176 
3182  {
3183  return new FPSort(this, Native.mkFpaSort32(nCtx()));
3184  }
3185 
3191  {
3192  return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
3193  }
3194 
3200  {
3201  return new FPSort(this, Native.mkFpaSort64(nCtx()));
3202  }
3203 
3209  {
3210  return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
3211  }
3212 
3218  {
3219  return new FPSort(this, Native.mkFpaSort128(nCtx()));
3220  }
3221 
3222 
3229  {
3230  return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
3231  }
3232 
3239  public FPNum mkFPInf(FPSort s, boolean negative)
3240  {
3241  return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
3242  }
3243 
3250  public FPNum mkFPZero(FPSort s, boolean negative)
3251  {
3252  return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
3253  }
3254 
3261  public FPNum mkFPNumeral(float v, FPSort s)
3262  {
3263  return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
3264  }
3265 
3272  public FPNum mkFPNumeral(double v, FPSort s)
3273  {
3274  return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
3275  }
3276 
3283  public FPNum mkFPNumeral(int v, FPSort s)
3284  {
3285  return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
3286  }
3287 
3296  public FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
3297  {
3298  return new FPNum(this, Native.mkFpaNumeralIntUint(nCtx(), sgn, exp, sig, s.getNativeObject()));
3299  }
3300 
3309  public FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
3310  {
3311  return new FPNum(this, Native.mkFpaNumeralInt64Uint64(nCtx(), sgn, exp, sig, s.getNativeObject()));
3312  }
3313 
3320  public FPNum mkFP(float v, FPSort s)
3321  {
3322  return mkFPNumeral(v, s);
3323  }
3324 
3331  public FPNum mkFP(double v, FPSort s)
3332  {
3333  return mkFPNumeral(v, s);
3334  }
3335 
3343  public FPNum mkFP(int v, FPSort s)
3344  {
3345  return mkFPNumeral(v, s);
3346  }
3347 
3356  public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
3357  {
3358  return mkFPNumeral(sgn, sig, exp, s);
3359  }
3360 
3369  public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
3370  {
3371  return mkFPNumeral(sgn, sig, exp, s);
3372  }
3373 
3374 
3380  public FPExpr mkFPAbs(FPExpr t)
3381  {
3382  return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
3383  }
3384 
3390  public FPExpr mkFPNeg(FPExpr t)
3391  {
3392  return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
3393  }
3394 
3402  public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
3403  {
3404  return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3405  }
3406 
3414  public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
3415  {
3416  return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3417  }
3418 
3426  public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
3427  {
3428  return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3429  }
3430 
3438  public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
3439  {
3440  return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3441  }
3442 
3453  public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
3454  {
3455  return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3456  }
3457 
3465  {
3466  return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3467  }
3468 
3475  public FPExpr mkFPRem(FPExpr t1, FPExpr t2)
3476  {
3477  return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3478  }
3479 
3488  {
3489  return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
3490  }
3491 
3498  public FPExpr mkFPMin(FPExpr t1, FPExpr t2)
3499  {
3500  return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3501  }
3502 
3509  public FPExpr mkFPMax(FPExpr t1, FPExpr t2)
3510  {
3511  return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3512  }
3513 
3520  public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
3521  {
3522  return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3523  }
3524 
3531  public BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
3532  {
3533  return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3534  }
3535 
3542  public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
3543  {
3544  return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3545  }
3546 
3553  public BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
3554  {
3555  return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3556  }
3557 
3566  public BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
3567  {
3568  return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
3569  }
3570 
3577  {
3578  return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
3579  }
3580 
3587  {
3588  return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
3589  }
3590 
3597  {
3598  return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
3599  }
3600 
3607  {
3608  return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
3609  }
3610 
3617  {
3618  return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
3619  }
3620 
3627  {
3628  return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
3629  }
3630 
3637  {
3638  return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
3639  }
3640 
3655  {
3656  return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3657  }
3658 
3671  {
3672  return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
3673  }
3674 
3687  {
3688  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3689  }
3690 
3703  {
3704  return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3705  }
3706 
3720  public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
3721  {
3722  if (signed)
3723  return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3724  else
3725  return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
3726  }
3727 
3739  {
3740  return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
3741  }
3742 
3755  public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
3756  {
3757  if (signed)
3758  return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3759  else
3760  return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
3761  }
3762 
3773  {
3774  return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
3775  }
3776 
3788  {
3789  return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
3790  }
3791 
3806  {
3807  return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
3808  }
3809 
3810 
3821  public AST wrapAST(long nativeObject)
3822  {
3823  return AST.create(this, nativeObject);
3824  }
3825 
3838  public long unwrapAST(AST a)
3839  {
3840  return a.getNativeObject();
3841  }
3842 
3848  {
3849  return Native.simplifyGetHelp(nCtx());
3850  }
3851 
3856  {
3857  return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx()));
3858  }
3859 
3868  public void updateParamValue(String id, String value)
3869  {
3870  Native.updateParamValue(nCtx(), id, value);
3871  }
3872 
3873 
3874  long nCtx()
3875  {
3876  return m_ctx;
3877  }
3878 
3879 
3880  void checkContextMatch(Z3Object other)
3881  {
3882  if (this != other.getContext())
3883  throw new Z3Exception("Context mismatch");
3884  }
3885 
3886  void checkContextMatch(Z3Object other1, Z3Object other2)
3887  {
3888  checkContextMatch(other1);
3889  checkContextMatch(other2);
3890  }
3891 
3892  void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
3893  {
3894  checkContextMatch(other1);
3895  checkContextMatch(other2);
3896  checkContextMatch(other3);
3897  }
3898 
3899  void checkContextMatch(Z3Object[] arr)
3900  {
3901  if (arr != null)
3902  for (Z3Object a : arr)
3903  checkContextMatch(a);
3904  }
3905 
3906  private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
3907  private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
3908  private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
3909  private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
3910  private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
3911  private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
3912  private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
3913  private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
3914  private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
3915  private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
3916  private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
3917  private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
3918  private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
3919  private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
3920  private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
3921  private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
3922  private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
3923  private ConstructorListDecRefQueue m_ConstructorList_DRQ =
3925 
3927  return m_Constructor_DRQ;
3928  }
3929 
3931  return m_ConstructorList_DRQ;
3932  }
3933 
3935  {
3936  return m_AST_DRQ;
3937  }
3938 
3940  {
3941  return m_ASTMap_DRQ;
3942  }
3943 
3945  {
3946  return m_ASTVector_DRQ;
3947  }
3948 
3950  {
3951  return m_ApplyResult_DRQ;
3952  }
3953 
3955  {
3956  return m_FuncEntry_DRQ;
3957  }
3958 
3960  {
3961  return m_FuncInterp_DRQ;
3962  }
3963 
3965  {
3966  return m_Goal_DRQ;
3967  }
3968 
3970  {
3971  return m_Model_DRQ;
3972  }
3973 
3975  {
3976  return m_Params_DRQ;
3977  }
3978 
3980  {
3981  return m_ParamDescrs_DRQ;
3982  }
3983 
3985  {
3986  return m_Probe_DRQ;
3987  }
3988 
3990  {
3991  return m_Solver_DRQ;
3992  }
3993 
3995  {
3996  return m_Statistics_DRQ;
3997  }
3998 
4000  {
4001  return m_Tactic_DRQ;
4002  }
4003 
4005  {
4006  return m_Fixedpoint_DRQ;
4007  }
4008 
4010  {
4011  return m_Optimize_DRQ;
4012  }
4013 
4017  @Override
4018  public void close()
4019  {
4020  m_AST_DRQ.forceClear(this);
4021  m_ASTMap_DRQ.forceClear(this);
4022  m_ASTVector_DRQ.forceClear(this);
4023  m_ApplyResult_DRQ.forceClear(this);
4024  m_FuncEntry_DRQ.forceClear(this);
4025  m_FuncInterp_DRQ.forceClear(this);
4026  m_Goal_DRQ.forceClear(this);
4027  m_Model_DRQ.forceClear(this);
4028  m_Params_DRQ.forceClear(this);
4029  m_Probe_DRQ.forceClear(this);
4030  m_Solver_DRQ.forceClear(this);
4031  m_Optimize_DRQ.forceClear(this);
4032  m_Statistics_DRQ.forceClear(this);
4033  m_Tactic_DRQ.forceClear(this);
4034  m_Fixedpoint_DRQ.forceClear(this);
4035 
4036  m_boolSort = null;
4037  m_intSort = null;
4038  m_realSort = null;
4039  m_stringSort = null;
4040 
4041  Native.delContext(m_ctx);
4042  }
4043 }
BoolExpr mkFPIsNegative(FPExpr t)
Definition: Context.java:3626
static long mkFpaFp(long a0, long a1, long a2, long a3)
Definition: Native.java:5723
IntExpr mkIntConst(Symbol name)
Definition: Context.java:596
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6020
ReExpr MkUnion(ReExpr... t)
Definition: Context.java:2050
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1606
static long tacticRepeat(long a0, long a1, int a2)
Definition: Native.java:3846
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
Definition: Context.java:712
IDecRefQueue< Probe > getProbeDRQ()
Definition: Context.java:3984
static long mkBvule(long a0, long a1, long a2)
Definition: Native.java:1493
static long mkSolver(long a0)
Definition: Native.java:4132
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
Definition: Native.java:6029
Tactic when(Probe p, Tactic t)
Definition: Context.java:2701
RatNum mkReal(String v)
Definition: Context.java:2132
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1051
IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
Definition: Context.java:1977
static long mkExtract(long a0, int a1, int a2, long a3)
Definition: Native.java:1556
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
Definition: Context.java:354
static void interrupt(long a0)
Definition: Native.java:724
static long getSmtlibSort(long a0, int a1)
Definition: Native.java:3530
Pattern mkPattern(Expr... terms)
Definition: Context.java:523
def SeqSort(s)
Definition: z3py.py:9357
Probe and(Probe p1, Probe p2)
Definition: Context.java:2936
static long mkMod(long a0, long a1, long a2)
Definition: Native.java:1223
static long mkBvugt(long a0, long a1, long a2)
Definition: Native.java:1529
static long mkSeqContains(long a0, long a1, long a2)
Definition: Native.java:2078
static void delConfig(long a0)
Definition: Native.java:669
ArrayExpr mkConstArray(Sort domain, Expr v)
Definition: Context.java:1704
static int getSmtlibNumSorts(long a0)
Definition: Native.java:3521
Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
Definition: Context.java:322
static long mkBvredor(long a0, long a1)
Definition: Native.java:1331
RealExpr mkFPToReal(FPExpr t)
Definition: Context.java:3772
static long tacticOrElse(long a0, long a1, long a2)
Definition: Native.java:3792
Probe lt(Probe p1, Probe p2)
Definition: Context.java:2875
static long mkFpaNeg(long a0, long a1)
Definition: Native.java:5786
FPNum mkFPNumeral(double v, FPSort s)
Definition: Context.java:3272
static int getNumProbes(long a0)
Definition: Native.java:3999
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1249
BoolExpr mkFPIsSubnormal(FPExpr t)
Definition: Context.java:3586
static void parseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3459
static long mkNumeral(long a0, String a1, long a2)
Definition: Native.java:1898
ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1836
BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1381
static long mkFpaDiv(long a0, long a1, long a2, long a3)
Definition: Native.java:5822
static void updateParamValue(long a0, String a1, String a2)
Definition: Native.java:716
ArrayExpr mkSetComplement(ArrayExpr arg)
Definition: Context.java:1848
BitVecExpr mkBVNeg(BitVecExpr t)
Definition: Context.java:1064
static long mkFreshConst(long a0, String a1, long a2)
Definition: Native.java:1070
static long mkConfig()
Definition: Native.java:663
def ReSort(s)
Definition: z3py.py:9584
def RealSort(ctx=None)
Definition: z3py.py:2721
FPNum mkFPInf(FPSort s, boolean negative)
Definition: Context.java:3239
Expr mkNumeral(int v, Sort ty)
Definition: Context.java:2085
BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1580
ListSort mkListSort(String name, Sort elemSort)
Definition: Context.java:286
FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t)
Definition: Context.java:3464
FPNum mkFPNumeral(int v, FPSort s)
Definition: Context.java:3283
static long mkFpaIsNegative(long a0, long a1)
Definition: Native.java:5975
StringSymbol mkSymbol(String name)
Definition: Context.java:89
static long mkSeqToRe(long a0, long a1)
Definition: Native.java:2132
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1673
FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
Definition: Context.java:3686
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1075
static long mkFpaRne(long a0)
Definition: Native.java:5534
String [] getTacticNames()
Definition: Context.java:2601
Probe eq(Probe p1, Probe p2)
Definition: Context.java:2925
BitVecExpr mkZeroExt(int i, BitVecExpr t)
Definition: Context.java:1351
static long mkOr(long a0, int a1, long[] a2)
Definition: Native.java:1169
BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1458
Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2296
BoolExpr mkDistinct(Expr... args)
Definition: Context.java:689
String getProbeDescription(String name)
Definition: Context.java:2850
IntNum mkInt(String v)
Definition: Context.java:2169
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1116
Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1750
BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
Definition: Context.java:1932
static long mkSub(long a0, int a1, long[] a2)
Definition: Native.java:1196
static long tacticFailIf(long a0, long a1)
Definition: Native.java:3873
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1420
static long mkExtRotateLeft(long a0, long a1, long a2)
Definition: Native.java:1637
static long mkSeqReplace(long a0, long a1, long a2, long a3)
Definition: Native.java:2096
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
Definition: Context.java:3531
FPRMNum mkFPRoundTowardNegative()
Definition: Context.java:3107
FPNum mkFP(float v, FPSort s)
Definition: Context.java:3320
static long mkFpaIsPositive(long a0, long a1)
Definition: Native.java:5984
SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
Definition: Context.java:1968
static long mkFpaSort16(long a0)
Definition: Native.java:5633
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
Definition: Context.java:735
static long mkReStar(long a0, long a1)
Definition: Native.java:2159
ReExpr MOption(ReExpr re)
Definition: Context.java:2032
static long mkFpaSqrt(long a0, long a1, long a2)
Definition: Native.java:5840
static long mkBvlshr(long a0, long a1, long a2)
Definition: Native.java:1601
SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
Definition: Context.java:1986
BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2527
BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1620
BitVecExpr mkExtract(int high, int low, BitVecExpr t)
Definition: Context.java:1322
UninterpretedSort mkUninterpretedSort(String str)
Definition: Context.java:176
BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1184
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
Definition: Context.java:4004
static String probeGetDescr(long a0, String a1)
Definition: Native.java:4044
static long mkBvuge(long a0, long a1, long a2)
Definition: Native.java:1511
static long mkSolverForLogic(long a0, long a1)
Definition: Native.java:4150
static long getSmtlibDecl(long a0, int a1)
Definition: Native.java:3512
static long mkFpaAdd(long a0, long a1, long a2, long a3)
Definition: Native.java:5795
static long simplifyGetParamDescrs(long a0)
Definition: Native.java:3077
String [] getProbeNames()
Definition: Context.java:2836
BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3566
FPNum mkFPNaN(FPSort s)
Definition: Context.java:3228
static long mkLe(long a0, long a1, long a2)
Definition: Native.java:1259
static long mkSetIntersect(long a0, int a1, long[] a2)
Definition: Native.java:1844
static long mkFpaRem(long a0, long a1, long a2)
Definition: Native.java:5849
static long mkConcat(long a0, long a1, long a2)
Definition: Native.java:1547
static long mkSelect(long a0, long a1, long a2)
Definition: Native.java:1745
static long mkBvnand(long a0, long a1, long a2)
Definition: Native.java:1367
static long mkFpaRoundTowardNegative(long a0)
Definition: Native.java:5579
static long mkFpaToReal(long a0, long a1)
Definition: Native.java:6056
Tactic then(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2664
IDecRefQueue< Statistics > getStatisticsDRQ()
Definition: Context.java:3994
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1473
BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2549
static long probeEq(long a0, long a1, long a2)
Definition: Native.java:3945
IDecRefQueue< AST > getASTDRQ()
Definition: Context.java:3934
static long mkGe(long a0, long a1, long a2)
Definition: Native.java:1277
static long mkXor(long a0, long a1, long a2)
Definition: Native.java:1151
Expr mkNumeral(String v, Sort ty)
Definition: Context.java:2068
static long mkSeqInRe(long a0, long a1, long a2)
Definition: Native.java:2141
BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1152
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
Definition: Context.java:243
BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1101
static long mkBvslt(long a0, long a1, long a2)
Definition: Native.java:1484
FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
Definition: Context.java:443
Definition: FuncInterp.java:31
static long mkFpaEq(long a0, long a1, long a2)
Definition: Native.java:5921
void setPrintMode(Z3_ast_print_mode value)
Definition: Context.java:2354
FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3438
static long mkReUnion(long a0, int a1, long[] a2)
Definition: Native.java:2177
static long mkAdd(long a0, int a1, long[] a2)
Definition: Native.java:1178
static int getSmtlibNumFormulas(long a0)
Definition: Native.java:3467
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
Definition: Native.java:5759
static long mkReConcat(long a0, int a1, long[] a2)
Definition: Native.java:2186
SeqExpr MkString(String s)
Definition: Context.java:1905
FuncDecl mkConstDecl(String name, Sort range)
Definition: Context.java:490
static long probeOr(long a0, long a1, long a2)
Definition: Native.java:3963
SetSort mkSetSort(Sort ty)
Definition: Context.java:1761
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:867
static long mkSeqIndex(long a0, long a1, long a2, long a3)
Definition: Native.java:2123
static long mkSeqSuffix(long a0, long a1, long a2)
Definition: Native.java:2069
static long mkSeqExtract(long a0, long a1, long a2, long a3)
Definition: Native.java:2087
FPExpr mkFPNeg(FPExpr t)
Definition: Context.java:3390
IntExpr mkReal2Int(RealExpr t)
Definition: Context.java:931
RatNum mkReal(int v)
Definition: Context.java:2145
IDecRefQueue< ASTMap > getASTMapDRQ()
Definition: Context.java:3939
BoolExpr MkInRe(SeqExpr s, ReExpr re)
Definition: Context.java:2005
static long probeNot(long a0, long a1)
Definition: Native.java:3972
static long mkSignExt(long a0, int a1, long a2)
Definition: Native.java:1565
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3296
FPRMExpr mkFPRoundNearestTiesToEven()
Definition: Context.java:3053
static long mkBvsmod(long a0, long a1, long a2)
Definition: Native.java:1466
AST wrapAST(long nativeObject)
Definition: Context.java:3821
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1682
BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
Definition: Context.java:1870
ArithExpr mkAdd(ArithExpr... t)
Definition: Context.java:777
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long mkSetComplement(long a0, long a1)
Definition: Native.java:1862
IDecRefQueue< Tactic > getTacticDRQ()
Definition: Context.java:3999
static long mkInt(long a0, int a1, long a2)
Definition: Native.java:1916
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
Definition: Context.java:430
static long probeConst(long a0, double a1)
Definition: Native.java:3900
static long mkSetAdd(long a0, long a1, long a2)
Definition: Native.java:1817
static long mkFpaNumeralInt(long a0, int a1, long a2)
Definition: Native.java:5750
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1727
static long mkBvneg(long a0, long a1)
Definition: Native.java:1394
static long mkInt64(long a0, long a1, long a2)
Definition: Native.java:1934
FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
Definition: Context.java:3738
BoolExpr mkFPIsPositive(FPExpr t)
Definition: Context.java:3636
static long mkBvsdiv(long a0, long a1, long a2)
Definition: Native.java:1439
static long mkMap(long a0, long a1, int a2, long[] a3)
Definition: Native.java:1772
FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
Definition: Context.java:3654
static int getNumTactics(long a0)
Definition: Native.java:3981
ArrayExpr mkSetDel(ArrayExpr set, Expr element)
Definition: Context.java:1802
static long mkZeroExt(long a0, int a1, long a2)
Definition: Native.java:1574
static long mkBvnot(long a0, long a1)
Definition: Native.java:1313
static long mkFpaRna(long a0)
Definition: Native.java:5552
static long mkDistinct(long a0, int a1, long[] a2)
Definition: Native.java:1106
BoolExpr mkIsInteger(RealExpr t)
Definition: Context.java:940
static long mkUnaryMinus(long a0, long a1)
Definition: Native.java:1205
BoolExpr mkBVNegNoOverflow(BitVecExpr t)
Definition: Context.java:1594
static long mkSetDifference(long a0, long a1, long a2)
Definition: Native.java:1853
static long mkBvsgt(long a0, long a1, long a2)
Definition: Native.java:1538
static long mkSetDel(long a0, long a1, long a2)
Definition: Native.java:1826
static long mkRotateRight(long a0, int a1, long a2)
Definition: Native.java:1628
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
Definition: Native.java:1700
static long mkStore(long a0, long a1, long a2, long a3)
Definition: Native.java:1754
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2309
FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
Definition: Context.java:3720
Probe gt(Probe p1, Probe p2)
Definition: Context.java:2887
BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
Definition: Context.java:1941
BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3520
static long mkSolverFromTactic(long a0, long a1)
Definition: Native.java:4159
BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1236
static long mkBvadd(long a0, long a1, long a2)
Definition: Native.java:1403
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1538
static void delContext(long a0)
Definition: Native.java:695
BoolExpr mkFPIsInfinite(FPExpr t)
Definition: Context.java:3606
static long mkBvsle(long a0, long a1, long a2)
Definition: Native.java:1502
BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:999
BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1012
IDecRefQueue< Model > getModelDRQ()
Definition: Context.java:3969
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
Definition: Context.java:3954
ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
Definition: Context.java:1790
BitVecExpr mkBVNot(BitVecExpr t)
Definition: Context.java:951
def FiniteDomainSort(name, sz, ctx=None)
Definition: z3py.py:6563
static long mkFpaGeq(long a0, long a1, long a2)
Definition: Native.java:5903
static long mkFpaGt(long a0, long a1, long a2)
Definition: Native.java:5912
EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
Definition: Context.java:256
BitVecExpr mkBVRedOR(BitVecExpr t)
Definition: Context.java:974
static long mkFpaToFpBv(long a0, long a1, long a2)
Definition: Native.java:5993
Tactic usingParams(Tactic t, Params p)
Definition: Context.java:2774
BitVecExpr mkBVConst(String name, int size)
Definition: Context.java:636
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:878
static void setAstPrintMode(long a0, int a1)
Definition: Native.java:3371
BoolExpr mkFPIsNaN(FPExpr t)
Definition: Context.java:3616
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1137
static long mkDiv(long a0, long a1, long a2)
Definition: Native.java:1214
static long mkIte(long a0, long a1, long a2, long a3)
Definition: Native.java:1124
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6047
FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3402
static String tacticGetDescr(long a0, String a1)
Definition: Native.java:4035
static long tacticFailIfNotDecided(long a0)
Definition: Native.java:3882
static long mkSeqConcat(long a0, int a1, long[] a2)
Definition: Native.java:2051
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1288
static long mkSimpleSolver(long a0)
Definition: Native.java:4141
static long mkSetMember(long a0, long a1, long a2)
Definition: Native.java:1871
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2270
static long mkFpaSortDouble(long a0)
Definition: Native.java:5660
static long mkFpaSort64(long a0)
Definition: Native.java:5669
FPRMNum mkFPRoundNearestTiesToAway()
Definition: Context.java:3071
BoolExpr mkBoolConst(String name)
Definition: Context.java:588
FPNum mkFPZero(FPSort s, boolean negative)
Definition: Context.java:3250
BitVecExpr mkRepeat(int i, BitVecExpr t)
Definition: Context.java:1363
FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Definition: Context.java:3453
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1025
void updateParamValue(String id, String value)
Definition: Context.java:3868
Probe mkProbe(String name)
Definition: Context.java:2858
BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
Definition: Context.java:746
BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1400
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:3949
static long tacticParOr(long a0, int a1, long[] a2)
Definition: Native.java:3801
static long tacticSkip(long a0)
Definition: Native.java:3855
static long mkString(long a0, String a1)
Definition: Native.java:2006
static int getSmtlibNumDecls(long a0)
Definition: Native.java:3503
static long mkBvurem(long a0, long a1, long a2)
Definition: Native.java:1448
Tactic repeat(Tactic t, int max)
Definition: Context.java:2727
static long mkSetSubset(long a0, long a1, long a2)
Definition: Native.java:1880
IDecRefQueue< Optimize > getOptimizeDRQ()
Definition: Context.java:4009
static long mkImplies(long a0, long a1, long a2)
Definition: Native.java:1142
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
Definition: Context.java:2372
DatatypeSort [] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Definition: Context.java:366
FPNum mkFP(int v, FPSort s)
Definition: Context.java:3343
Tactic tryFor(Tactic t, int ms)
Definition: Context.java:2688
static long probeGt(long a0, long a1, long a2)
Definition: Native.java:3918
static long mkFpaAbs(long a0, long a1)
Definition: Native.java:5777
static long mkFpaIsNan(long a0, long a1)
Definition: Native.java:5966
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
Definition: Context.java:724
void parseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2410
static long getSmtlibAssumption(long a0, int a1)
Definition: Native.java:3494
IntExpr mkIntConst(String name)
Definition: Context.java:604
BoolExpr mkOr(BoolExpr... t)
Definition: Context.java:767
static long mkFpaSortSingle(long a0)
Definition: Native.java:5642
static long mkEq(long a0, long a1, long a2)
Definition: Native.java:1097
static long mkRem(long a0, long a1, long a2)
Definition: Native.java:1232
def FPSort(ebits, sbits, ctx=None)
Definition: z3py.py:8556
Probe not(Probe p)
Definition: Context.java:2958
static long mkExtRotateRight(long a0, long a1, long a2)
Definition: Native.java:1646
static long mkFpaMul(long a0, long a1, long a2, long a3)
Definition: Native.java:5813
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1223
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
Definition: Context.java:3356
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1262
ReExpr MkStar(ReExpr re)
Definition: Context.java:2014
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1038
IDecRefQueue< ASTVector > getASTVectorDRQ()
Definition: Context.java:3944
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
Definition: Context.java:418
IntNum mkInt(long v)
Definition: Context.java:2195
Solver mkSolver(String logic)
Definition: Context.java:2997
static long mkInt2bv(long a0, int a1, long a2)
Definition: Native.java:1655
BitVecExpr mkBVRedAND(BitVecExpr t)
Definition: Context.java:962
IntExpr mkRem(IntExpr t1, IntExpr t2)
Definition: Context.java:843
FiniteDomainSort mkFiniteDomainSort(String name, long size)
Definition: Context.java:305
static long mkFpaRtz(long a0)
Definition: Native.java:5606
static long mkBvand(long a0, long a1, long a2)
Definition: Native.java:1340
FuncDecl mkConstDecl(Symbol name, Sort range)
Definition: Context.java:480
static long mkRepeat(long a0, int a1, long a2)
Definition: Native.java:1583
FPRMNum mkFPRoundTowardPositive()
Definition: Context.java:3089
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1566
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
Definition: Native.java:1018
static long mkReOption(long a0, long a1)
Definition: Native.java:2168
static long mkPattern(long a0, int a1, long[] a2)
Definition: Native.java:2195
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
Definition: Native.java:5858
UninterpretedSort mkUninterpretedSort(Symbol s)
Definition: Context.java:167
ArithExpr mkMul(ArithExpr... t)
Definition: Context.java:787
void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Definition: Context.java:2391
static String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
Definition: Native.java:3424
IntExpr MkLength(SeqExpr s)
Definition: Context.java:1923
static native void setInternalErrorHandler(long ctx)
static long mkFpaNumeralFloat(long a0, float a1, long a2)
Definition: Native.java:5732
static long mkBvult(long a0, long a1, long a2)
Definition: Native.java:1475
FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3426
static void setParamValue(long a0, String a1, String a2)
Definition: Native.java:674
static void parseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3451
static int getSmtlibNumAssumptions(long a0)
Definition: Native.java:3485
BoolExpr mkAnd(BoolExpr... t)
Definition: Context.java:757
Expr mkFreshConst(String prefix, Sort range)
Definition: Context.java:561
static long mkSeqAt(long a0, long a1, long a2)
Definition: Native.java:2105
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
Definition: Context.java:3487
static long mkAnd(long a0, int a1, long[] a2)
Definition: Native.java:1160
Tactic failIf(Probe p)
Definition: Context.java:2754
static long mkSeqUnit(long a0, long a1)
Definition: Native.java:2042
static long mkLt(long a0, long a1, long a2)
Definition: Native.java:1250
static long mkContextRc(long a0)
Definition: Native.java:687
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
Definition: Context.java:3475
IDecRefQueue< ConstructorList > getConstructorListDRQ()
Definition: Context.java:3930
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:3989
static long mkFpaRtp(long a0)
Definition: Native.java:5570
FPNum mkFP(double v, FPSort s)
Definition: Context.java:3331
ArrayExpr mkEmptySet(Sort domain)
Definition: Context.java:1770
static long mkFpaRoundTowardPositive(long a0)
Definition: Native.java:5561
static long mkFpaIsSubnormal(long a0, long a1)
Definition: Native.java:5939
Expr mkTermArray(ArrayExpr array)
Definition: Context.java:1740
static long mkBvsub(long a0, long a1, long a2)
Definition: Native.java:1412
static long mkFpaToIeeeBv(long a0, long a1)
Definition: Native.java:6128
static long mkConstArray(long a0, long a1, long a2)
Definition: Native.java:1763
EnumSort mkEnumSort(String name, String... enumNames)
Definition: Context.java:267
static long mkSeqSort(long a0, long a1)
Definition: Native.java:1952
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Definition: Context.java:3979
static long mkInt2real(long a0, long a1)
Definition: Native.java:1286
FPExpr mkFPMin(FPExpr t1, FPExpr t2)
Definition: Context.java:3498
BoolExpr mkBool(boolean value)
Definition: Context.java:670
static long mkConst(long a0, long a1, long a2)
Definition: Native.java:1052
static long mkFpaInf(long a0, long a1, boolean a2)
Definition: Native.java:5705
static long mkBvsge(long a0, long a1, long a2)
Definition: Native.java:1520
SeqSort mkSeqSort(Sort s)
Definition: Context.java:226
def ArraySort(d, r)
Definition: z3py.py:4110
static long mkReSort(long a0, long a1)
Definition: Native.java:1970
Probe or(Probe p1, Probe p2)
Definition: Context.java:2947
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
Definition: Native.java:6002
BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
Definition: Context.java:3805
static long mkFpaRoundNearestTiesToAway(long a0)
Definition: Native.java:5543
static long tacticParAndThen(long a0, long a1, long a2)
Definition: Native.java:3810
static String getProbeName(long a0, int a1)
Definition: Native.java:4008
FPExpr mkFPAbs(FPExpr t)
Definition: Context.java:3380
def IntSort(ctx=None)
Definition: z3py.py:2705
FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Definition: Context.java:3414
Tactic with(Tactic t, Params p)
Definition: Context.java:2788
IntExpr mkMod(IntExpr t1, IntExpr t2)
Definition: Context.java:830
BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
Definition: Context.java:3755
Probe ge(Probe p1, Probe p2)
Definition: Context.java:2913
def EnumSort(name, values, ctx=None)
Definition: z3py.py:4574
static long mkBvashr(long a0, long a1, long a2)
Definition: Native.java:1610
static long mkGt(long a0, long a1, long a2)
Definition: Native.java:1268
Expr mkApp(FuncDecl f, Expr... args)
Definition: Context.java:644
ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
Definition: Context.java:1632
static long mkFullSet(long a0, long a1)
Definition: Native.java:1808
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
Definition: Context.java:295
BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1210
BitVecExpr mkInt2BV(int n, IntExpr t)
Definition: Context.java:1491
BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
Definition: Context.java:1445
ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
Definition: Context.java:854
IDecRefQueue< Constructor > getConstructorDRQ()
Definition: Context.java:3926
static long probeLe(long a0, long a1, long a2)
Definition: Native.java:3927
ReExpr MPlus(ReExpr re)
Definition: Context.java:2023
Context(Map< String, String > settings)
Definition: Context.java:61
ArrayExpr mkSetUnion(ArrayExpr... args)
Definition: Context.java:1814
BoolExpr mkBoolConst(Symbol name)
Definition: Context.java:580
static long mkFpaIsInfinite(long a0, long a1)
Definition: Native.java:5957
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
Definition: Context.java:3509
ArrayExpr mkFullSet(Sort domain)
Definition: Context.java:1780
IntSymbol mkSymbol(int i)
Definition: Context.java:81
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2283
SeqExpr MkUnit(Expr elem)
Definition: Context.java:1896
BoolExpr [] getSMTLIBAssumptions()
Definition: Context.java:2463
Expr mkConst(String name, Sort range)
Definition: Context.java:552
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3433
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
Definition: Context.java:343
SeqExpr MkEmptySeq(Sort s)
Definition: Context.java:1887
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
Definition: Native.java:1736
static long mkRotateLeft(long a0, int a1, long a2)
Definition: Native.java:1619
static String simplifyGetHelp(long a0)
Definition: Native.java:3068
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
Definition: Native.java:5768
Tactic parAndThen(Tactic t1, Tactic t2)
Definition: Context.java:2807
ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
Definition: Context.java:1725
static long mkFpaMin(long a0, long a1, long a2)
Definition: Native.java:5867
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
Definition: Context.java:1433
static long mkBvredand(long a0, long a1)
Definition: Native.java:1322
static long tacticFail(long a0)
Definition: Native.java:3864
static long mkSeqLength(long a0, long a1)
Definition: Native.java:2114
Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
Definition: Context.java:333
static long mkBvxor(long a0, long a1, long a2)
Definition: Native.java:1358
static long tacticUsingParams(long a0, long a1, long a2)
Definition: Native.java:3891
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1197
Probe constProbe(double val)
Definition: Context.java:2866
static long probeLt(long a0, long a1, long a2)
Definition: Native.java:3909
static long mkFpaIsNormal(long a0, long a1)
Definition: Native.java:5930
static long mkBvudiv(long a0, long a1, long a2)
Definition: Native.java:1430
static long mkFpaNan(long a0, long a1)
Definition: Native.java:5696
static long probeGe(long a0, long a1, long a2)
Definition: Native.java:3936
static long mkBvshl(long a0, long a1, long a2)
Definition: Native.java:1592
static long mkFalse(long a0)
Definition: Native.java:1088
static long mkFpaRtn(long a0)
Definition: Native.java:5588
static long mkBvsrem(long a0, long a1, long a2)
Definition: Native.java:1457
BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:986
BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1552
BitVecExpr mkFPToIEEEBV(FPExpr t)
Definition: Context.java:3787
def BitVecSort(sz, ctx=None)
Definition: z3py.py:3530
static long mkEmptySet(long a0, long a1)
Definition: Native.java:1799
static long mkFpaRoundNearestTiesToEven(long a0)
Definition: Native.java:5525
Expr mkBound(int index, Sort ty)
Definition: Context.java:514
BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
Definition: Context.java:1950
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1709
RatNum mkReal(long v)
Definition: Context.java:2158
FPNum mkFPNumeral(float v, FPSort s)
Definition: Context.java:3261
static String getTacticName(long a0, int a1)
Definition: Native.java:3990
static long mkRePlus(long a0, long a1)
Definition: Native.java:2150
BitVecExpr mkBVConst(Symbol name, int size)
Definition: Context.java:628
static long tacticTryFor(long a0, long a1, int a2)
Definition: Native.java:3819
static long mkArrayDefault(long a0, long a1)
Definition: Native.java:1781
static long mkBvnegNoOverflow(long a0, long a1)
Definition: Native.java:1718
static long mkArrayExt(long a0, long a1, long a2)
Definition: Native.java:1889
static long mkStringSort(long a0)
Definition: Native.java:1988
static long mkBound(long a0, int a1, long a2)
Definition: Native.java:2204
static long mkTrue(long a0)
Definition: Native.java:1079
Tactic mkTactic(String name)
Definition: Context.java:2623
static long mkFpaSort128(long a0)
Definition: Native.java:5687
static long mkMul(long a0, int a1, long[] a2)
Definition: Native.java:1187
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
Definition: Native.java:6011
static long mkSeqEmpty(long a0, long a1)
Definition: Native.java:2033
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3309
static long mkReal(long a0, int a1, int a2)
Definition: Native.java:1907
FPSort mkFPSort(int ebits, int sbits)
Definition: Context.java:3145
static long tacticAndThen(long a0, long a1, long a2)
Definition: Native.java:3783
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
Definition: Context.java:1686
BitVecSort mkBitVecSort(int size)
Definition: Context.java:200
ReExpr MkConcat(ReExpr... t)
Definition: Context.java:2041
static long mkFpaLt(long a0, long a1, long a2)
Definition: Native.java:5894
ParamDescrs getSimplifyParameterDescriptions()
Definition: Context.java:3855
IDecRefQueue< Params > getParamsDRQ()
Definition: Context.java:3974
Fixedpoint mkFixedpoint()
Definition: Context.java:3026
static long mkBvxnor(long a0, long a1, long a2)
Definition: Native.java:1385
static long mkSeqPrefix(long a0, long a1, long a2)
Definition: Native.java:2060
BoolExpr [] getSMTLIBFormulas()
Definition: Context.java:2439
static long mkFpaMax(long a0, long a1, long a2)
Definition: Native.java:5876
static long mkFpaSub(long a0, long a1, long a2, long a3)
Definition: Native.java:5804
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
Definition: Context.java:3369
BoolExpr mkFPIsNormal(FPExpr t)
Definition: Context.java:3576
static long mkSetUnion(long a0, int a1, long[] a2)
Definition: Native.java:1835
Tactic cond(Probe p, Tactic t1, Tactic t2)
Definition: Context.java:2714
static long mkPower(long a0, long a1, long a2)
Definition: Native.java:1241
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1170
static long mkFpaIsZero(long a0, long a1)
Definition: Native.java:5948
Solver mkSolver(Symbol logic)
Definition: Context.java:2983
def Map(f, args)
Definition: z3py.py:4207
FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
Definition: Context.java:3670
FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
Definition: Context.java:454
ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
Definition: Context.java:1641
static long mkBvor(long a0, long a1, long a2)
Definition: Native.java:1349
BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
Definition: Context.java:3542
static long getSmtlibFormula(long a0, int a1)
Definition: Native.java:3476
ArraySort mkArraySort(Sort domain, Sort range)
Definition: Context.java:208
Expr mkConst(Symbol name, Sort range)
Definition: Context.java:537
Tactic parOr(Tactic... t)
Definition: Context.java:2796
BitVecNum mkBV(int v, int size)
Definition: Context.java:2217
SeqExpr MkAt(SeqExpr s, IntExpr index)
Definition: Context.java:1959
static long mkBv2int(long a0, long a1, boolean a2)
Definition: Native.java:1664
BoolExpr mkNot(BoolExpr a)
Definition: Context.java:699
Expr mkNumeral(long v, Sort ty)
Definition: Context.java:2101
DatatypeSort [] mkDatatypeSorts(String[] names, Constructor[][] c)
Definition: Context.java:393
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
Definition: Context.java:889
FPRMSort mkFPRoundingModeSort()
Definition: Context.java:3044
ListSort mkListSort(Symbol name, Sort elemSort)
Definition: Context.java:276
static long mkFpaRoundTowardZero(long a0)
Definition: Native.java:5597
Tactic orElse(Tactic t1, Tactic t2)
Definition: Context.java:2674
ReSort mkReSort(Sort s)
Definition: Context.java:234
Expr mkConst(FuncDecl f)
Definition: Context.java:572
Probe le(Probe p1, Probe p2)
Definition: Context.java:2900
ArithExpr mkUnaryMinus(ArithExpr t)
Definition: Context.java:807
static long probeAnd(long a0, long a1, long a2)
Definition: Native.java:3954
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
Definition: Context.java:2632
RealExpr mkInt2Real(IntExpr t)
Definition: Context.java:918
RealExpr mkRealConst(Symbol name)
Definition: Context.java:612
static long mkBvmul(long a0, long a1, long a2)
Definition: Native.java:1421
static long mkFpaSortQuadruple(long a0)
Definition: Native.java:5678
static long datatypeUpdateField(long a0, long a1, long a2, long a3)
Definition: Native.java:2456
FuncDecl mkFreshConstDecl(String prefix, Sort range)
Definition: Context.java:502
Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2327
static long mkFpaNumeralDouble(long a0, double a1, long a2)
Definition: Native.java:5741
BitVecNum mkBV(String v, int size)
Definition: Context.java:2207
Solver mkSolver(Tactic t)
Definition: Context.java:3016
String getTacticDescription(String name)
Definition: Context.java:2615
Expr mkSelect(ArrayExpr a, Expr i)
Definition: Context.java:1660
static long mkFpaFma(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:5831
ReExpr MkToRe(SeqExpr s)
Definition: Context.java:1995
static long mkReal2int(long a0, long a1)
Definition: Native.java:1295
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
Definition: Context.java:469
static long mkFpaSortHalf(long a0)
Definition: Native.java:5624
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
Definition: Native.java:6038
BitVecNum mkBV(long v, int size)
Definition: Context.java:2227
BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1088
static long tacticWhen(long a0, long a1, long a2)
Definition: Native.java:3828
ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
Definition: Context.java:817
RealExpr mkRealConst(String name)
Definition: Context.java:620
static long mkNot(long a0, long a1)
Definition: Native.java:1115
ArrayExpr mkSetIntersection(ArrayExpr... args)
Definition: Context.java:1825
Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
Definition: Context.java:405
static long mkBvSort(long a0, int a1)
Definition: Native.java:921
FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
Definition: Context.java:3702
static long mkFpaSort32(long a0)
Definition: Native.java:5651
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1306
RatNum mkReal(int num, int den)
Definition: Context.java:2117
BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
Definition: Context.java:3553
BitVecExpr mkSignExt(int i, BitVecExpr t)
Definition: Context.java:1337
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
Definition: Context.java:1275
BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
Definition: Context.java:1858
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
Definition: Context.java:1512
IDecRefQueue< FuncInterp > getFuncInterpDRQ()
Definition: Context.java:3959
static long mkIsInt(long a0, long a1)
Definition: Native.java:1304
FPRMNum mkFPRoundTowardZero()
Definition: Context.java:3125
static long mkFpaLeq(long a0, long a1, long a2)
Definition: Native.java:5885
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
Definition: Native.java:3442
SeqExpr MkConcat(SeqExpr... t)
Definition: Context.java:1913
BoolExpr mkEq(Expr x, Expr y)
Definition: Context.java:678
static long mkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:6137
def BoolSort(ctx=None)
Definition: z3py.py:1407
static long mkBvsubNoOverflow(long a0, long a1, long a2)
Definition: Native.java:1691
static long mkIff(long a0, long a1, long a2)
Definition: Native.java:1133
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
Definition: Context.java:900
BoolExpr mkFPIsZero(FPExpr t)
Definition: Context.java:3596
def String(name, ctx=None)
Definition: z3py.py:9443
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:3964
FuncDecl [] getSMTLIBDecls()
Definition: Context.java:2487
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Definition: Context.java:2257
ArithExpr mkSub(ArithExpr... t)
Definition: Context.java:797
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
Definition: Context.java:2576
static long tacticCond(long a0, long a1, long a2, long a3)
Definition: Native.java:3837
static long mkFpaZero(long a0, long a1, boolean a2)
Definition: Native.java:5714
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Definition: Context.java:1524
static long mkBvnor(long a0, long a1, long a2)
Definition: Native.java:1376