18 package com.microsoft.z3;
30 private final long m_ctx;
31 static final Object creation_lock =
new Object();
61 public Context(Map<String, String> settings) {
102 for (
int i = 0; i < names.length; ++i)
108 private IntSort m_intSort = null;
110 private SeqSort m_stringSort = null;
117 if (m_boolSort == null) {
128 if (m_intSort == null) {
139 if (m_realSort == null) {
158 if (m_stringSort == null) {
169 checkContextMatch(s);
210 checkContextMatch(domain);
211 checkContextMatch(range);
212 return new ArraySort(
this, domain, range);
246 checkContextMatch(name);
247 checkContextMatch(fieldNames);
248 checkContextMatch(fieldSorts);
249 return new TupleSort(
this, name, fieldNames.length, fieldNames,
259 checkContextMatch(name);
260 checkContextMatch(enumNames);
261 return new EnumSort(
this, name, enumNames);
278 checkContextMatch(name);
279 checkContextMatch(elemSort);
280 return new ListSort(
this, name, elemSort);
288 checkContextMatch(elemSort);
298 checkContextMatch(name);
323 Symbol[] fieldNames,
Sort[] sorts,
int[] sortRefs)
326 return of(
this, name, recognizer, fieldNames, sorts,
334 String[] fieldNames,
Sort[] sorts,
int[] sortRefs)
337 mkSymbols(fieldNames), sorts, sortRefs);
346 checkContextMatch(name);
347 checkContextMatch(constructors);
357 checkContextMatch(constructors);
369 checkContextMatch(names);
370 int n = names.length;
372 long[] n_constr =
new long[n];
373 for (
int i = 0; i < n; i++)
377 checkContextMatch(constructor);
379 n_constr[i] = cla[i].getNativeObject();
381 long[] n_res =
new long[n];
385 for (
int i = 0; i < n; i++)
408 return Expr.create (
this,
410 (nCtx(), field.getNativeObject(),
411 t.getNativeObject(), v.getNativeObject()));
421 checkContextMatch(name);
422 checkContextMatch(domain);
423 checkContextMatch(range);
424 return new FuncDecl(
this, name, domain, range);
433 checkContextMatch(name);
434 checkContextMatch(domain);
435 checkContextMatch(range);
437 return new FuncDecl(
this, name, q, range);
446 checkContextMatch(domain);
447 checkContextMatch(range);
457 checkContextMatch(domain);
458 checkContextMatch(range);
472 checkContextMatch(domain);
473 checkContextMatch(range);
474 return new FuncDecl(
this, prefix, domain, range);
482 checkContextMatch(name);
483 checkContextMatch(range);
484 return new FuncDecl(
this, name, null, range);
492 checkContextMatch(range);
505 checkContextMatch(range);
506 return new FuncDecl(
this, prefix, null, range);
516 return Expr.create(
this,
525 if (terms.length == 0)
526 throw new Z3Exception(
"Cannot create a pattern from zero terms");
528 long[] termsNative =
AST.arrayToNative(terms);
539 checkContextMatch(name);
540 checkContextMatch(range);
545 range.getNativeObject()));
563 checkContextMatch(range);
564 return Expr.create(
this,
646 checkContextMatch(f);
647 checkContextMatch(args);
648 return Expr.create(
this, f, args);
680 checkContextMatch(x);
681 checkContextMatch(y);
683 y.getNativeObject()));
691 checkContextMatch(args);
693 AST.arrayToNative(args)));
701 checkContextMatch(a);
714 checkContextMatch(t1);
715 checkContextMatch(t2);
716 checkContextMatch(t3);
718 t2.getNativeObject(), t3.getNativeObject()));
726 checkContextMatch(t1);
727 checkContextMatch(t2);
729 t2.getNativeObject()));
737 checkContextMatch(t1);
738 checkContextMatch(t2);
740 t1.getNativeObject(), t2.getNativeObject()));
748 checkContextMatch(t1);
749 checkContextMatch(t2);
751 t2.getNativeObject()));
759 checkContextMatch(t);
761 AST.arrayToNative(t)));
769 checkContextMatch(t);
771 AST.arrayToNative(t)));
779 checkContextMatch(t);
789 checkContextMatch(t);
799 checkContextMatch(t);
809 checkContextMatch(t);
819 checkContextMatch(t1);
820 checkContextMatch(t2);
822 t1.getNativeObject(), t2.getNativeObject()));
832 checkContextMatch(t1);
833 checkContextMatch(t2);
835 t2.getNativeObject()));
845 checkContextMatch(t1);
846 checkContextMatch(t2);
848 t2.getNativeObject()));
856 checkContextMatch(t1);
857 checkContextMatch(t2);
861 t2.getNativeObject()));
869 checkContextMatch(t1);
870 checkContextMatch(t2);
872 t2.getNativeObject()));
880 checkContextMatch(t1);
881 checkContextMatch(t2);
883 t2.getNativeObject()));
891 checkContextMatch(t1);
892 checkContextMatch(t2);
894 t2.getNativeObject()));
902 checkContextMatch(t1);
903 checkContextMatch(t2);
905 t2.getNativeObject()));
920 checkContextMatch(t);
933 checkContextMatch(t);
942 checkContextMatch(t);
953 checkContextMatch(t);
964 checkContextMatch(t);
966 t.getNativeObject()));
976 checkContextMatch(t);
978 t.getNativeObject()));
988 checkContextMatch(t1);
989 checkContextMatch(t2);
991 t1.getNativeObject(), t2.getNativeObject()));
1001 checkContextMatch(t1);
1002 checkContextMatch(t2);
1004 t2.getNativeObject()));
1014 checkContextMatch(t1);
1015 checkContextMatch(t2);
1017 t1.getNativeObject(), t2.getNativeObject()));
1027 checkContextMatch(t1);
1028 checkContextMatch(t2);
1030 t1.getNativeObject(), t2.getNativeObject()));
1040 checkContextMatch(t1);
1041 checkContextMatch(t2);
1043 t1.getNativeObject(), t2.getNativeObject()));
1053 checkContextMatch(t1);
1054 checkContextMatch(t2);
1056 t1.getNativeObject(), t2.getNativeObject()));
1066 checkContextMatch(t);
1077 checkContextMatch(t1);
1078 checkContextMatch(t2);
1080 t1.getNativeObject(), t2.getNativeObject()));
1090 checkContextMatch(t1);
1091 checkContextMatch(t2);
1093 t1.getNativeObject(), t2.getNativeObject()));
1103 checkContextMatch(t1);
1104 checkContextMatch(t2);
1106 t1.getNativeObject(), t2.getNativeObject()));
1118 checkContextMatch(t1);
1119 checkContextMatch(t2);
1121 t1.getNativeObject(), t2.getNativeObject()));
1139 checkContextMatch(t1);
1140 checkContextMatch(t2);
1142 t1.getNativeObject(), t2.getNativeObject()));
1154 checkContextMatch(t1);
1155 checkContextMatch(t2);
1157 t1.getNativeObject(), t2.getNativeObject()));
1172 checkContextMatch(t1);
1173 checkContextMatch(t2);
1175 t1.getNativeObject(), t2.getNativeObject()));
1186 checkContextMatch(t1);
1187 checkContextMatch(t2);
1189 t1.getNativeObject(), t2.getNativeObject()));
1199 checkContextMatch(t1);
1200 checkContextMatch(t2);
1202 t2.getNativeObject()));
1212 checkContextMatch(t1);
1213 checkContextMatch(t2);
1215 t2.getNativeObject()));
1225 checkContextMatch(t1);
1226 checkContextMatch(t2);
1228 t2.getNativeObject()));
1238 checkContextMatch(t1);
1239 checkContextMatch(t2);
1241 t2.getNativeObject()));
1251 checkContextMatch(t1);
1252 checkContextMatch(t2);
1254 t2.getNativeObject()));
1264 checkContextMatch(t1);
1265 checkContextMatch(t2);
1267 t2.getNativeObject()));
1277 checkContextMatch(t1);
1278 checkContextMatch(t2);
1280 t2.getNativeObject()));
1290 checkContextMatch(t1);
1291 checkContextMatch(t2);
1293 t2.getNativeObject()));
1308 checkContextMatch(t1);
1309 checkContextMatch(t2);
1311 t1.getNativeObject(), t2.getNativeObject()));
1325 checkContextMatch(t);
1327 t.getNativeObject()));
1339 checkContextMatch(t);
1341 t.getNativeObject()));
1353 checkContextMatch(t);
1355 t.getNativeObject()));
1365 checkContextMatch(t);
1367 t.getNativeObject()));
1383 checkContextMatch(t1);
1384 checkContextMatch(t2);
1386 t1.getNativeObject(), t2.getNativeObject()));
1402 checkContextMatch(t1);
1403 checkContextMatch(t2);
1405 t1.getNativeObject(), t2.getNativeObject()));
1422 checkContextMatch(t1);
1423 checkContextMatch(t2);
1425 t1.getNativeObject(), t2.getNativeObject()));
1435 checkContextMatch(t);
1437 t.getNativeObject()));
1447 checkContextMatch(t);
1449 t.getNativeObject()));
1461 checkContextMatch(t1);
1462 checkContextMatch(t2);
1464 t1.getNativeObject(), t2.getNativeObject()));
1476 checkContextMatch(t1);
1477 checkContextMatch(t2);
1479 t1.getNativeObject(), t2.getNativeObject()));
1493 checkContextMatch(t);
1495 t.getNativeObject()));
1514 checkContextMatch(t);
1527 checkContextMatch(t1);
1528 checkContextMatch(t2);
1530 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1541 checkContextMatch(t1);
1542 checkContextMatch(t2);
1544 t1.getNativeObject(), t2.getNativeObject()));
1555 checkContextMatch(t1);
1556 checkContextMatch(t2);
1558 t1.getNativeObject(), t2.getNativeObject()));
1569 checkContextMatch(t1);
1570 checkContextMatch(t2);
1572 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1583 checkContextMatch(t1);
1584 checkContextMatch(t2);
1586 t1.getNativeObject(), t2.getNativeObject()));
1596 checkContextMatch(t);
1598 t.getNativeObject()));
1609 checkContextMatch(t1);
1610 checkContextMatch(t2);
1612 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1623 checkContextMatch(t1);
1624 checkContextMatch(t2);
1626 t1.getNativeObject(), t2.getNativeObject()));
1662 checkContextMatch(a);
1663 checkContextMatch(i);
1667 i.getNativeObject()));
1688 checkContextMatch(a);
1689 checkContextMatch(i);
1690 checkContextMatch(v);
1692 i.getNativeObject(), v.getNativeObject()));
1706 checkContextMatch(domain);
1707 checkContextMatch(v);
1709 domain.getNativeObject(), v.getNativeObject()));
1727 checkContextMatch(f);
1728 checkContextMatch(args);
1730 f.getNativeObject(),
AST.arrayLength(args),
1731 AST.arrayToNative(args)));
1742 checkContextMatch(array);
1743 return Expr.create(
this,
1752 checkContextMatch(arg1);
1753 checkContextMatch(arg2);
1754 return Expr.create(
this,
Native.
mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
1763 checkContextMatch(ty);
1772 checkContextMatch(domain);
1782 checkContextMatch(domain);
1792 checkContextMatch(
set);
1793 checkContextMatch(element);
1796 element.getNativeObject()));
1804 checkContextMatch(
set);
1805 checkContextMatch(element);
1808 element.getNativeObject()));
1816 checkContextMatch(args);
1819 AST.arrayToNative(args)));
1827 checkContextMatch(args);
1830 AST.arrayToNative(args)));
1838 checkContextMatch(arg1);
1839 checkContextMatch(arg2);
1842 arg2.getNativeObject()));
1850 checkContextMatch(arg);
1860 checkContextMatch(elem);
1861 checkContextMatch(
set);
1864 set.getNativeObject()));
1872 checkContextMatch(arg1);
1873 checkContextMatch(arg2);
1876 arg2.getNativeObject()));
1889 checkContextMatch(s);
1898 checkContextMatch(elem);
1915 checkContextMatch(t);
1925 checkContextMatch(s);
1934 checkContextMatch(s1, s2);
1943 checkContextMatch(s1, s2);
1952 checkContextMatch(s1, s2);
1961 checkContextMatch(s, index);
1962 return new SeqExpr(
this,
Native.
mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
1970 checkContextMatch(s, offset, length);
1971 return new SeqExpr(
this,
Native.
mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
1979 checkContextMatch(s, substr, offset);
1980 return new IntExpr(
this,
Native.
mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
1988 checkContextMatch(s, src, dst);
1989 return new SeqExpr(
this,
Native.
mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
1997 checkContextMatch(s);
2007 checkContextMatch(s, re);
2016 checkContextMatch(re);
2025 checkContextMatch(re);
2034 checkContextMatch(re);
2043 checkContextMatch(t);
2052 checkContextMatch(t);
2070 checkContextMatch(ty);
2071 return Expr.create(
this,
2087 checkContextMatch(ty);
2088 return Expr.create(
this,
Native.
mkInt(nCtx(), v, ty.getNativeObject()));
2103 checkContextMatch(ty);
2104 return Expr.create(
this,
2136 .getNativeObject()));
2149 .getNativeObject()));
2162 .getNativeObject()));
2173 .getNativeObject()));
2186 .getNativeObject()));
2199 .getNativeObject()));
2258 int weight,
Pattern[] patterns,
Expr[] noPatterns,
2262 return Quantifier.
of(
this,
true, sorts, names, body, weight, patterns,
2263 noPatterns, quantifierID, skolemID);
2275 return Quantifier.
of(
this,
true, boundConstants, body, weight,
2276 patterns, noPatterns, quantifierID, skolemID);
2284 int weight,
Pattern[] patterns,
Expr[] noPatterns,
2288 return Quantifier.
of(
this,
false, sorts, names, body, weight,
2289 patterns, noPatterns, quantifierID, skolemID);
2301 return Quantifier.
of(
this,
false, boundConstants, body, weight,
2302 patterns, noPatterns, quantifierID, skolemID);
2316 return mkForall(sorts, names, body, weight, patterns, noPatterns,
2317 quantifierID, skolemID);
2319 return mkExists(sorts, names, body, weight, patterns, noPatterns,
2320 quantifierID, skolemID);
2333 return mkForall(boundConstants, body, weight, patterns, noPatterns,
2334 quantifierID, skolemID);
2336 return mkExists(boundConstants, body, weight, patterns, noPatterns,
2337 quantifierID, skolemID);
2378 attributes, assumptions.length,
2379 AST.arrayToNative(assumptions), formula.getNativeObject());
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)
2401 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2402 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2403 AST.arrayToNative(decls));
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)
2421 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2422 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2423 AST.arrayToNative(decls));
2444 for (
int i = 0; i < n; i++)
2468 for (
int i = 0; i < n; i++)
2492 for (
int i = 0; i < n; i++)
2515 for (
int i = 0; i < n; i++)
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) {
2540 str,
AST.arrayLength(sorts),
Symbol.arrayToNative(sortNames),
2541 AST.arrayToNative(sorts),
AST.arrayLength(decls),
2542 Symbol.arrayToNative(declNames),
AST.arrayToNative(decls)));
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)
2560 fileName,
AST.arrayLength(sorts),
2561 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2562 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2563 AST.arrayToNative(decls)));
2576 public Goal mkGoal(
boolean models,
boolean unsatCores,
boolean proofs)
2579 return new Goal(
this, models, unsatCores, proofs);
2606 for (
int i = 0; i < n; i++)
2625 return new Tactic(
this, name);
2635 checkContextMatch(t1);
2636 checkContextMatch(t2);
2637 checkContextMatch(ts);
2640 if (ts != null && ts.length > 0)
2642 last = ts[ts.length - 1].getNativeObject();
2643 for (
int i = ts.length - 2; i >= 0; i--) {
2652 t1.getNativeObject(), last));
2655 t1.getNativeObject(), t2.getNativeObject()));
2676 checkContextMatch(t1);
2677 checkContextMatch(t2);
2679 t1.getNativeObject(), t2.getNativeObject()));
2690 checkContextMatch(t);
2692 t.getNativeObject(), ms));
2703 checkContextMatch(t);
2704 checkContextMatch(p);
2706 t.getNativeObject()));
2716 checkContextMatch(p);
2717 checkContextMatch(t1);
2718 checkContextMatch(t2);
2720 t1.getNativeObject(), t2.getNativeObject()));
2729 checkContextMatch(t);
2731 t.getNativeObject(), max));
2756 checkContextMatch(p);
2776 checkContextMatch(t);
2777 checkContextMatch(p);
2779 t.getNativeObject(), p.getNativeObject()));
2798 checkContextMatch(t);
2809 checkContextMatch(t1);
2810 checkContextMatch(t2);
2812 t1.getNativeObject(), t2.getNativeObject()));
2841 for (
int i = 0; i < n; i++)
2860 return new Probe(
this, name);
2877 checkContextMatch(p1);
2878 checkContextMatch(p2);
2880 p2.getNativeObject()));
2889 checkContextMatch(p1);
2890 checkContextMatch(p2);
2892 p2.getNativeObject()));
2902 checkContextMatch(p1);
2903 checkContextMatch(p2);
2905 p2.getNativeObject()));
2915 checkContextMatch(p1);
2916 checkContextMatch(p2);
2918 p2.getNativeObject()));
2927 checkContextMatch(p1);
2928 checkContextMatch(p2);
2930 p2.getNativeObject()));
2938 checkContextMatch(p1);
2939 checkContextMatch(p2);
2941 p2.getNativeObject()));
2949 checkContextMatch(p1);
2950 checkContextMatch(p2);
2952 p2.getNativeObject()));
2960 checkContextMatch(p);
2990 logic.getNativeObject()));
3020 t.getNativeObject()));
3147 return new FPSort(
this, ebits, sbits);
3404 return new FPExpr(
this,
Native.
mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3416 return new FPExpr(
this,
Native.
mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3428 return new FPExpr(
this,
Native.
mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3440 return new FPExpr(
this,
Native.
mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3455 return new FPExpr(
this,
Native.
mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3656 return new FPExpr(
this,
Native.
mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3823 return AST.create(
this, nativeObject);
3840 return a.getNativeObject();
3880 void checkContextMatch(
Z3Object other)
3882 if (
this != other.getContext())
3888 checkContextMatch(other1);
3889 checkContextMatch(other2);
3894 checkContextMatch(other1);
3895 checkContextMatch(other2);
3896 checkContextMatch(other3);
3899 void checkContextMatch(
Z3Object[] arr)
3903 checkContextMatch(a);
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();
3927 return m_Constructor_DRQ;
3931 return m_ConstructorList_DRQ;
3941 return m_ASTMap_DRQ;
3946 return m_ASTVector_DRQ;
3951 return m_ApplyResult_DRQ;
3956 return m_FuncEntry_DRQ;
3961 return m_FuncInterp_DRQ;
3976 return m_Params_DRQ;
3981 return m_ParamDescrs_DRQ;
3991 return m_Solver_DRQ;
3996 return m_Statistics_DRQ;
4001 return m_Tactic_DRQ;
4006 return m_Fixedpoint_DRQ;
4011 return m_Optimize_DRQ;
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);
4039 m_stringSort = null;
BoolExpr mkFPIsNegative(FPExpr t)
static long mkFpaFp(long a0, long a1, long a2, long a3)
IntExpr mkIntConst(Symbol name)
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
ReExpr MkUnion(ReExpr... t)
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
static long tacticRepeat(long a0, long a1, int a2)
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
IDecRefQueue< Probe > getProbeDRQ()
static long mkBvule(long a0, long a1, long a2)
static long mkSolver(long a0)
int getNumSMTLIBAssumptions()
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
Tactic when(Probe p, Tactic t)
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
static long mkExtract(long a0, int a1, int a2, long a3)
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
static void interrupt(long a0)
static long getSmtlibSort(long a0, int a1)
Pattern mkPattern(Expr... terms)
Probe and(Probe p1, Probe p2)
static long mkMod(long a0, long a1, long a2)
static long mkBvugt(long a0, long a1, long a2)
static long mkSeqContains(long a0, long a1, long a2)
static void delConfig(long a0)
ArrayExpr mkConstArray(Sort domain, Expr v)
static int getSmtlibNumSorts(long a0)
Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
static long mkBvredor(long a0, long a1)
RealExpr mkFPToReal(FPExpr t)
int getNumSMTLIBFormulas()
static long tacticOrElse(long a0, long a1, long a2)
Probe lt(Probe p1, Probe p2)
static long mkFpaNeg(long a0, long a1)
FPNum mkFPNumeral(double v, FPSort s)
static int getNumProbes(long a0)
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkFPIsSubnormal(FPExpr t)
static void parseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static long mkNumeral(long a0, String a1, long a2)
ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
static long mkFpaDiv(long a0, long a1, long a2, long a3)
static void updateParamValue(long a0, String a1, String a2)
ArrayExpr mkSetComplement(ArrayExpr arg)
BitVecExpr mkBVNeg(BitVecExpr t)
static long mkFreshConst(long a0, String a1, long a2)
FPNum mkFPInf(FPSort s, boolean negative)
Expr mkNumeral(int v, Sort ty)
BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
ListSort mkListSort(String name, Sort elemSort)
FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t)
FPNum mkFPNumeral(int v, FPSort s)
static long mkFpaIsNegative(long a0, long a1)
StringSymbol mkSymbol(String name)
static long mkSeqToRe(long a0, long a1)
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
static long mkFpaRne(long a0)
String [] getTacticNames()
Probe eq(Probe p1, Probe p2)
BitVecExpr mkZeroExt(int i, BitVecExpr t)
static long mkOr(long a0, int a1, long[] a2)
BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
BoolExpr mkDistinct(Expr... args)
String getProbeDescription(String name)
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
static long mkSub(long a0, int a1, long[] a2)
static long tacticFailIf(long a0, long a1)
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Tactic failIfNotDecided()
static long mkExtRotateLeft(long a0, long a1, long a2)
static long mkSeqReplace(long a0, long a1, long a2, long a3)
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
FPRMNum mkFPRoundTowardNegative()
FPNum mkFP(float v, FPSort s)
static long mkFpaIsPositive(long a0, long a1)
SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
static long mkFpaSort16(long a0)
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
static long mkReStar(long a0, long a1)
ReExpr MOption(ReExpr re)
static long mkFpaSqrt(long a0, long a1, long a2)
static long mkBvlshr(long a0, long a1, long a2)
SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkExtract(int high, int low, BitVecExpr t)
UninterpretedSort mkUninterpretedSort(String str)
BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
static String probeGetDescr(long a0, String a1)
static long mkBvuge(long a0, long a1, long a2)
static long mkSolverForLogic(long a0, long a1)
static long getSmtlibDecl(long a0, int a1)
static long mkFpaAdd(long a0, long a1, long a2, long a3)
static long simplifyGetParamDescrs(long a0)
String [] getProbeNames()
BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
static long mkLe(long a0, long a1, long a2)
static long mkSetIntersect(long a0, int a1, long[] a2)
static long mkFpaRem(long a0, long a1, long a2)
static long mkConcat(long a0, long a1, long a2)
static long mkSelect(long a0, long a1, long a2)
static long mkBvnand(long a0, long a1, long a2)
static long mkFpaRoundTowardNegative(long a0)
static long mkFpaToReal(long a0, long a1)
Tactic then(Tactic t1, Tactic t2, Tactic... ts)
IDecRefQueue< Statistics > getStatisticsDRQ()
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
static long probeEq(long a0, long a1, long a2)
IDecRefQueue< AST > getASTDRQ()
static long mkGe(long a0, long a1, long a2)
static long mkXor(long a0, long a1, long a2)
Expr mkNumeral(String v, Sort ty)
static long mkSeqInRe(long a0, long a1, long a2)
BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
static long mkBvslt(long a0, long a1, long a2)
FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
static long mkFpaEq(long a0, long a1, long a2)
void setPrintMode(Z3_ast_print_mode value)
FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
static long mkReUnion(long a0, int a1, long[] a2)
static long mkAdd(long a0, int a1, long[] a2)
static int getSmtlibNumFormulas(long a0)
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
static long mkReConcat(long a0, int a1, long[] a2)
SeqExpr MkString(String s)
FuncDecl mkConstDecl(String name, Sort range)
static long probeOr(long a0, long a1, long a2)
SetSort mkSetSort(Sort ty)
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
static long mkSeqIndex(long a0, long a1, long a2, long a3)
static long mkSeqSuffix(long a0, long a1, long a2)
static long mkSeqExtract(long a0, long a1, long a2, long a3)
IntExpr mkReal2Int(RealExpr t)
IDecRefQueue< ASTMap > getASTMapDRQ()
BoolExpr MkInRe(SeqExpr s, ReExpr re)
static long probeNot(long a0, long a1)
static long mkSignExt(long a0, int a1, long a2)
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
FPRMExpr mkFPRoundNearestTiesToEven()
static long mkBvsmod(long a0, long a1, long a2)
AST wrapAST(long nativeObject)
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
ArithExpr mkAdd(ArithExpr... t)
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)
IDecRefQueue< Tactic > getTacticDRQ()
static long mkInt(long a0, int a1, long a2)
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
static long probeConst(long a0, double a1)
static long mkSetAdd(long a0, long a1, long a2)
static long mkFpaNumeralInt(long a0, int a1, long a2)
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
static long mkBvneg(long a0, long a1)
static long mkInt64(long a0, long a1, long a2)
FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
BoolExpr mkFPIsPositive(FPExpr t)
static long mkBvsdiv(long a0, long a1, long a2)
static long mkMap(long a0, long a1, int a2, long[] a3)
FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
static int getNumTactics(long a0)
ArrayExpr mkSetDel(ArrayExpr set, Expr element)
static long mkZeroExt(long a0, int a1, long a2)
static long mkBvnot(long a0, long a1)
static long mkFpaRna(long a0)
static long mkDistinct(long a0, int a1, long[] a2)
BoolExpr mkIsInteger(RealExpr t)
static long mkUnaryMinus(long a0, long a1)
BoolExpr mkBVNegNoOverflow(BitVecExpr t)
static long mkSetDifference(long a0, long a1, long a2)
static long mkBvsgt(long a0, long a1, long a2)
static long mkSetDel(long a0, long a1, long a2)
static long mkRotateRight(long a0, int a1, long a2)
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
static long mkStore(long a0, long a1, long a2, long a3)
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
Probe gt(Probe p1, Probe p2)
BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
static long mkSolverFromTactic(long a0, long a1)
BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
static long mkBvadd(long a0, long a1, long a2)
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
static void delContext(long a0)
BoolExpr mkFPIsInfinite(FPExpr t)
static long mkBvsle(long a0, long a1, long a2)
BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
IDecRefQueue< Model > getModelDRQ()
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
BitVecExpr mkBVNot(BitVecExpr t)
def FiniteDomainSort(name, sz, ctx=None)
static long mkFpaGeq(long a0, long a1, long a2)
static long mkFpaGt(long a0, long a1, long a2)
EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
BitVecExpr mkBVRedOR(BitVecExpr t)
static long mkFpaToFpBv(long a0, long a1, long a2)
Tactic usingParams(Tactic t, Params p)
BitVecExpr mkBVConst(String name, int size)
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
static void setAstPrintMode(long a0, int a1)
BoolExpr mkFPIsNaN(FPExpr t)
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
static long mkDiv(long a0, long a1, long a2)
static long mkIte(long a0, long a1, long a2, long a3)
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
static String tacticGetDescr(long a0, String a1)
static long tacticFailIfNotDecided(long a0)
static long mkSeqConcat(long a0, int a1, long[] a2)
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
static long mkSimpleSolver(long a0)
static long mkSetMember(long a0, long a1, long a2)
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long mkFpaSortDouble(long a0)
FPSort mkFPSortQuadruple()
static long mkFpaSort64(long a0)
FPRMNum mkFPRoundNearestTiesToAway()
BoolExpr mkBoolConst(String name)
FPNum mkFPZero(FPSort s, boolean negative)
BitVecExpr mkRepeat(int i, BitVecExpr t)
FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
void updateParamValue(String id, String value)
Probe mkProbe(String name)
BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
IDecRefQueue< ApplyResult > getApplyResultDRQ()
static long tacticParOr(long a0, int a1, long[] a2)
static long tacticSkip(long a0)
static long mkString(long a0, String a1)
static int getSmtlibNumDecls(long a0)
static long mkBvurem(long a0, long a1, long a2)
Tactic repeat(Tactic t, int max)
static long mkSetSubset(long a0, long a1, long a2)
IDecRefQueue< Optimize > getOptimizeDRQ()
static long mkImplies(long a0, long a1, long a2)
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
DatatypeSort [] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
FPNum mkFP(int v, FPSort s)
Tactic tryFor(Tactic t, int ms)
static long probeGt(long a0, long a1, long a2)
static long mkFpaAbs(long a0, long a1)
static long mkFpaIsNan(long a0, long a1)
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
void parseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
static long getSmtlibAssumption(long a0, int a1)
IntExpr mkIntConst(String name)
BoolExpr mkOr(BoolExpr... t)
static long mkFpaSortSingle(long a0)
static long mkEq(long a0, long a1, long a2)
static long mkRem(long a0, long a1, long a2)
def FPSort(ebits, sbits, ctx=None)
static long mkExtRotateRight(long a0, long a1, long a2)
static long mkFpaMul(long a0, long a1, long a2, long a3)
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
IDecRefQueue< ASTVector > getASTVectorDRQ()
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
Solver mkSolver(String logic)
static long mkInt2bv(long a0, int a1, long a2)
BitVecExpr mkBVRedAND(BitVecExpr t)
IntExpr mkRem(IntExpr t1, IntExpr t2)
FiniteDomainSort mkFiniteDomainSort(String name, long size)
static long mkFpaRtz(long a0)
static long mkBvand(long a0, long a1, long a2)
FuncDecl mkConstDecl(Symbol name, Sort range)
static long mkRepeat(long a0, int a1, long a2)
FPRMNum mkFPRoundTowardPositive()
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
static long mkReOption(long a0, long a1)
static long mkPattern(long a0, int a1, long[] a2)
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
UninterpretedSort mkUninterpretedSort(Symbol s)
ArithExpr mkMul(ArithExpr... t)
void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
static String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
IntExpr MkLength(SeqExpr s)
static native void setInternalErrorHandler(long ctx)
static long mkFpaNumeralFloat(long a0, float a1, long a2)
static long mkBvult(long a0, long a1, long a2)
FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
static void setParamValue(long a0, String a1, String a2)
static void parseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static int getSmtlibNumAssumptions(long a0)
BoolExpr mkAnd(BoolExpr... t)
Expr mkFreshConst(String prefix, Sort range)
static long mkSeqAt(long a0, long a1, long a2)
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
static long mkAnd(long a0, int a1, long[] a2)
static long mkSeqUnit(long a0, long a1)
static long mkLt(long a0, long a1, long a2)
static long mkContextRc(long a0)
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
IDecRefQueue< ConstructorList > getConstructorListDRQ()
IDecRefQueue< Solver > getSolverDRQ()
static long mkFpaRtp(long a0)
FPNum mkFP(double v, FPSort s)
ArrayExpr mkEmptySet(Sort domain)
static long mkFpaRoundTowardPositive(long a0)
static long mkFpaIsSubnormal(long a0, long a1)
Expr mkTermArray(ArrayExpr array)
static long mkBvsub(long a0, long a1, long a2)
static long mkFpaToIeeeBv(long a0, long a1)
static long mkConstArray(long a0, long a1, long a2)
EnumSort mkEnumSort(String name, String... enumNames)
static long mkSeqSort(long a0, long a1)
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
static long mkInt2real(long a0, long a1)
FPExpr mkFPMin(FPExpr t1, FPExpr t2)
BoolExpr mkBool(boolean value)
static long mkConst(long a0, long a1, long a2)
static long mkFpaInf(long a0, long a1, boolean a2)
static long mkBvsge(long a0, long a1, long a2)
SeqSort mkSeqSort(Sort s)
static long mkReSort(long a0, long a1)
Probe or(Probe p1, Probe p2)
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
static long mkFpaRoundNearestTiesToAway(long a0)
static long tacticParAndThen(long a0, long a1, long a2)
static String getProbeName(long a0, int a1)
FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
Tactic with(Tactic t, Params p)
IntExpr mkMod(IntExpr t1, IntExpr t2)
BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
Probe ge(Probe p1, Probe p2)
def EnumSort(name, values, ctx=None)
static long mkBvashr(long a0, long a1, long a2)
static long mkGt(long a0, long a1, long a2)
Expr mkApp(FuncDecl f, Expr... args)
ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
static long mkFullSet(long a0, long a1)
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkInt2BV(int n, IntExpr t)
BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
IDecRefQueue< Constructor > getConstructorDRQ()
static long probeLe(long a0, long a1, long a2)
Context(Map< String, String > settings)
ArrayExpr mkSetUnion(ArrayExpr... args)
BoolExpr mkBoolConst(Symbol name)
static long mkFpaIsInfinite(long a0, long a1)
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
ArrayExpr mkFullSet(Sort domain)
IntSymbol mkSymbol(int i)
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
SeqExpr MkUnit(Expr elem)
BoolExpr [] getSMTLIBAssumptions()
Expr mkConst(String name, Sort range)
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
SeqExpr MkEmptySeq(Sort s)
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
static long mkRotateLeft(long a0, int a1, long a2)
static String simplifyGetHelp(long a0)
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
Tactic parAndThen(Tactic t1, Tactic t2)
ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
static long mkFpaMin(long a0, long a1, long a2)
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
static long mkBvredand(long a0, long a1)
static long tacticFail(long a0)
static long mkSeqLength(long a0, long a1)
Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
static long mkBvxor(long a0, long a1, long a2)
static long tacticUsingParams(long a0, long a1, long a2)
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
Probe constProbe(double val)
static long probeLt(long a0, long a1, long a2)
static long mkFpaIsNormal(long a0, long a1)
static long mkBvudiv(long a0, long a1, long a2)
static long mkFpaNan(long a0, long a1)
static long probeGe(long a0, long a1, long a2)
static long mkBvshl(long a0, long a1, long a2)
static long mkFalse(long a0)
static long mkFpaRtn(long a0)
static long mkBvsrem(long a0, long a1, long a2)
BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkFPToIEEEBV(FPExpr t)
def BitVecSort(sz, ctx=None)
static long mkEmptySet(long a0, long a1)
static long mkFpaRoundNearestTiesToEven(long a0)
Expr mkBound(int index, Sort ty)
BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
FPNum mkFPNumeral(float v, FPSort s)
static String getTacticName(long a0, int a1)
static long mkRePlus(long a0, long a1)
BitVecExpr mkBVConst(Symbol name, int size)
static long tacticTryFor(long a0, long a1, int a2)
static long mkArrayDefault(long a0, long a1)
static long mkBvnegNoOverflow(long a0, long a1)
static long mkArrayExt(long a0, long a1, long a2)
static long mkStringSort(long a0)
static long mkBound(long a0, int a1, long a2)
Z3_PRINT_SMTLIB2_COMPLIANT
static long mkTrue(long a0)
Tactic mkTactic(String name)
static long mkFpaSort128(long a0)
static long mkMul(long a0, int a1, long[] a2)
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
static long mkSeqEmpty(long a0, long a1)
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
static long mkReal(long a0, int a1, int a2)
FPSort mkFPSort(int ebits, int sbits)
static long tacticAndThen(long a0, long a1, long a2)
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
BitVecSort mkBitVecSort(int size)
ReExpr MkConcat(ReExpr... t)
static long mkFpaLt(long a0, long a1, long a2)
ParamDescrs getSimplifyParameterDescriptions()
IDecRefQueue< Params > getParamsDRQ()
Fixedpoint mkFixedpoint()
static long mkBvxnor(long a0, long a1, long a2)
static long mkSeqPrefix(long a0, long a1, long a2)
BoolExpr [] getSMTLIBFormulas()
static long mkFpaMax(long a0, long a1, long a2)
static long mkFpaSub(long a0, long a1, long a2, long a3)
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
BoolExpr mkFPIsNormal(FPExpr t)
static long mkSetUnion(long a0, int a1, long[] a2)
Tactic cond(Probe p, Tactic t1, Tactic t2)
static long mkPower(long a0, long a1, long a2)
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
static long mkFpaIsZero(long a0, long a1)
Solver mkSolver(Symbol logic)
FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
static long mkBvor(long a0, long a1, long a2)
BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
static long getSmtlibFormula(long a0, int a1)
ArraySort mkArraySort(Sort domain, Sort range)
Expr mkConst(Symbol name, Sort range)
Tactic parOr(Tactic... t)
BitVecNum mkBV(int v, int size)
SeqExpr MkAt(SeqExpr s, IntExpr index)
static long mkBv2int(long a0, long a1, boolean a2)
BoolExpr mkNot(BoolExpr a)
Expr mkNumeral(long v, Sort ty)
DatatypeSort [] mkDatatypeSorts(String[] names, Constructor[][] c)
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
FPRMSort mkFPRoundingModeSort()
ListSort mkListSort(Symbol name, Sort elemSort)
static long mkFpaRoundTowardZero(long a0)
Tactic orElse(Tactic t1, Tactic t2)
Probe le(Probe p1, Probe p2)
ArithExpr mkUnaryMinus(ArithExpr t)
static long probeAnd(long a0, long a1, long a2)
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
RealExpr mkInt2Real(IntExpr t)
RealExpr mkRealConst(Symbol name)
static long mkBvmul(long a0, long a1, long a2)
static long mkFpaSortQuadruple(long a0)
static long datatypeUpdateField(long a0, long a1, long a2, long a3)
FuncDecl mkFreshConstDecl(String prefix, Sort range)
Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long mkFpaNumeralDouble(long a0, double a1, long a2)
BitVecNum mkBV(String v, int size)
Solver mkSolver(Tactic t)
String getTacticDescription(String name)
Expr mkSelect(ArrayExpr a, Expr i)
static long mkFpaFma(long a0, long a1, long a2, long a3, long a4)
static long mkReal2int(long a0, long a1)
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
static long mkFpaSortHalf(long a0)
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
BitVecNum mkBV(long v, int size)
BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
static long tacticWhen(long a0, long a1, long a2)
ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
RealExpr mkRealConst(String name)
static long mkNot(long a0, long a1)
ArrayExpr mkSetIntersection(ArrayExpr... args)
Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
static long mkBvSort(long a0, int a1)
FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
static long mkFpaSort32(long a0)
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
RatNum mkReal(int num, int den)
BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
BitVecExpr mkSignExt(int i, BitVecExpr t)
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
IDecRefQueue< FuncInterp > getFuncInterpDRQ()
static long mkIsInt(long a0, long a1)
FPRMNum mkFPRoundTowardZero()
static long mkFpaLeq(long a0, long a1, long a2)
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
SeqExpr MkConcat(SeqExpr... t)
BoolExpr mkEq(Expr x, Expr y)
static long mkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
static long mkBvsubNoOverflow(long a0, long a1, long a2)
static long mkIff(long a0, long a1, long a2)
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
BoolExpr mkFPIsZero(FPExpr t)
def String(name, ctx=None)
IDecRefQueue< Goal > getGoalDRQ()
FuncDecl [] getSMTLIBDecls()
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
ArithExpr mkSub(ArithExpr... t)
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
static long tacticCond(long a0, long a1, long a2, long a3)
static long mkFpaZero(long a0, long a1, boolean a2)
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
static long mkBvnor(long a0, long a1, long a2)