18 package com.microsoft.z3;
56 public Context(Map<String, String> settings)
60 for (
Map.Entry<String, String> kv : settings.entrySet())
88 Symbol[] mkSymbols(String[] names)
93 for (
int i = 0; i < names.length; ++i)
99 private IntSort m_intSort = null;
107 if (m_boolSort == null)
117 if (m_intSort == null)
127 if (m_realSort == null)
145 checkContextMatch(s);
186 checkContextMatch(domain);
187 checkContextMatch(range);
188 return new ArraySort(
this, domain, range);
197 checkContextMatch(name);
198 checkContextMatch(fieldNames);
199 checkContextMatch(fieldSorts);
200 return new TupleSort(
this, name, (
int) fieldNames.length, fieldNames,
210 checkContextMatch(name);
211 checkContextMatch(enumNames);
212 return new EnumSort(
this, name, enumNames);
229 checkContextMatch(name);
230 checkContextMatch(elemSort);
231 return new ListSort(
this, name, elemSort);
239 checkContextMatch(elemSort);
249 checkContextMatch(name);
274 Symbol[] fieldNames,
Sort[] sorts,
int[] sortRefs)
278 return new Constructor(
this, name, recognizer, fieldNames, sorts,
293 String[] fieldNames,
Sort[] sorts,
int[] sortRefs)
298 mkSymbols(fieldNames), sorts, sortRefs);
307 checkContextMatch(name);
308 checkContextMatch(constructors);
318 checkContextMatch(constructors);
330 checkContextMatch(names);
331 int n = (int) names.length;
333 long[] n_constr =
new long[n];
334 for (
int i = 0; i < n; i++)
338 checkContextMatch(constructor);
340 n_constr[i] = cla[i].getNativeObject();
342 long[] n_res =
new long[n];
346 for (
int i = 0; i < n; i++)
370 checkContextMatch(name);
371 checkContextMatch(domain);
372 checkContextMatch(range);
373 return new FuncDecl(
this, name, domain, range);
382 checkContextMatch(name);
383 checkContextMatch(domain);
384 checkContextMatch(range);
386 return new FuncDecl(
this, name, q, range);
395 checkContextMatch(domain);
396 checkContextMatch(range);
406 checkContextMatch(domain);
407 checkContextMatch(range);
421 checkContextMatch(domain);
422 checkContextMatch(range);
423 return new FuncDecl(
this, prefix, domain, range);
431 checkContextMatch(name);
432 checkContextMatch(range);
433 return new FuncDecl(
this, name, null, range);
441 checkContextMatch(range);
454 checkContextMatch(range);
455 return new FuncDecl(
this, prefix, null, range);
465 return Expr.create(
this,
474 if (terms.length == 0)
475 throw new Z3Exception(
"Cannot create a pattern from zero terms");
477 long[] termsNative =
AST.arrayToNative(terms);
488 checkContextMatch(name);
489 checkContextMatch(range);
494 range.getNativeObject()));
512 checkContextMatch(range);
513 return Expr.create(
this,
595 checkContextMatch(f);
596 checkContextMatch(args);
597 return Expr.create(
this, f, args);
629 checkContextMatch(x);
630 checkContextMatch(y);
632 y.getNativeObject()));
640 checkContextMatch(args);
642 AST.arrayToNative(args)));
650 checkContextMatch(a);
663 checkContextMatch(t1);
664 checkContextMatch(t2);
665 checkContextMatch(t3);
667 t2.getNativeObject(), t3.getNativeObject()));
675 checkContextMatch(t1);
676 checkContextMatch(t2);
678 t2.getNativeObject()));
686 checkContextMatch(t1);
687 checkContextMatch(t2);
689 t1.getNativeObject(), t2.getNativeObject()));
697 checkContextMatch(t1);
698 checkContextMatch(t2);
700 t2.getNativeObject()));
708 checkContextMatch(t);
710 AST.arrayToNative(t)));
718 checkContextMatch(t);
720 AST.arrayToNative(t)));
728 checkContextMatch(t);
738 checkContextMatch(t);
748 checkContextMatch(t);
758 checkContextMatch(t);
768 checkContextMatch(t1);
769 checkContextMatch(t2);
771 t1.getNativeObject(), t2.getNativeObject()));
781 checkContextMatch(t1);
782 checkContextMatch(t2);
784 t2.getNativeObject()));
794 checkContextMatch(t1);
795 checkContextMatch(t2);
797 t2.getNativeObject()));
805 checkContextMatch(t1);
806 checkContextMatch(t2);
810 t2.getNativeObject()));
818 checkContextMatch(t1);
819 checkContextMatch(t2);
821 t2.getNativeObject()));
829 checkContextMatch(t1);
830 checkContextMatch(t2);
832 t2.getNativeObject()));
840 checkContextMatch(t1);
841 checkContextMatch(t2);
843 t2.getNativeObject()));
851 checkContextMatch(t1);
852 checkContextMatch(t2);
854 t2.getNativeObject()));
869 checkContextMatch(t);
882 checkContextMatch(t);
891 checkContextMatch(t);
902 checkContextMatch(t);
913 checkContextMatch(t);
915 t.getNativeObject()));
925 checkContextMatch(t);
927 t.getNativeObject()));
937 checkContextMatch(t1);
938 checkContextMatch(t2);
940 t1.getNativeObject(), t2.getNativeObject()));
950 checkContextMatch(t1);
951 checkContextMatch(t2);
953 t2.getNativeObject()));
963 checkContextMatch(t1);
964 checkContextMatch(t2);
966 t1.getNativeObject(), t2.getNativeObject()));
976 checkContextMatch(t1);
977 checkContextMatch(t2);
979 t1.getNativeObject(), t2.getNativeObject()));
989 checkContextMatch(t1);
990 checkContextMatch(t2);
992 t1.getNativeObject(), t2.getNativeObject()));
1002 checkContextMatch(t1);
1003 checkContextMatch(t2);
1005 t1.getNativeObject(), t2.getNativeObject()));
1015 checkContextMatch(t);
1026 checkContextMatch(t1);
1027 checkContextMatch(t2);
1029 t1.getNativeObject(), t2.getNativeObject()));
1039 checkContextMatch(t1);
1040 checkContextMatch(t2);
1042 t1.getNativeObject(), t2.getNativeObject()));
1052 checkContextMatch(t1);
1053 checkContextMatch(t2);
1055 t1.getNativeObject(), t2.getNativeObject()));
1067 checkContextMatch(t1);
1068 checkContextMatch(t2);
1070 t1.getNativeObject(), t2.getNativeObject()));
1088 checkContextMatch(t1);
1089 checkContextMatch(t2);
1091 t1.getNativeObject(), t2.getNativeObject()));
1103 checkContextMatch(t1);
1104 checkContextMatch(t2);
1106 t1.getNativeObject(), t2.getNativeObject()));
1121 checkContextMatch(t1);
1122 checkContextMatch(t2);
1124 t1.getNativeObject(), t2.getNativeObject()));
1135 checkContextMatch(t1);
1136 checkContextMatch(t2);
1138 t1.getNativeObject(), t2.getNativeObject()));
1148 checkContextMatch(t1);
1149 checkContextMatch(t2);
1151 t2.getNativeObject()));
1161 checkContextMatch(t1);
1162 checkContextMatch(t2);
1164 t2.getNativeObject()));
1174 checkContextMatch(t1);
1175 checkContextMatch(t2);
1177 t2.getNativeObject()));
1187 checkContextMatch(t1);
1188 checkContextMatch(t2);
1190 t2.getNativeObject()));
1200 checkContextMatch(t1);
1201 checkContextMatch(t2);
1203 t2.getNativeObject()));
1213 checkContextMatch(t1);
1214 checkContextMatch(t2);
1216 t2.getNativeObject()));
1226 checkContextMatch(t1);
1227 checkContextMatch(t2);
1229 t2.getNativeObject()));
1239 checkContextMatch(t1);
1240 checkContextMatch(t2);
1242 t2.getNativeObject()));
1257 checkContextMatch(t1);
1258 checkContextMatch(t2);
1260 t1.getNativeObject(), t2.getNativeObject()));
1274 checkContextMatch(t);
1276 t.getNativeObject()));
1288 checkContextMatch(t);
1290 t.getNativeObject()));
1302 checkContextMatch(t);
1304 t.getNativeObject()));
1314 checkContextMatch(t);
1316 t.getNativeObject()));
1332 checkContextMatch(t1);
1333 checkContextMatch(t2);
1335 t1.getNativeObject(), t2.getNativeObject()));
1351 checkContextMatch(t1);
1352 checkContextMatch(t2);
1354 t1.getNativeObject(), t2.getNativeObject()));
1371 checkContextMatch(t1);
1372 checkContextMatch(t2);
1374 t1.getNativeObject(), t2.getNativeObject()));
1384 checkContextMatch(t);
1386 t.getNativeObject()));
1396 checkContextMatch(t);
1398 t.getNativeObject()));
1410 checkContextMatch(t1);
1411 checkContextMatch(t2);
1413 t1.getNativeObject(), t2.getNativeObject()));
1425 checkContextMatch(t1);
1426 checkContextMatch(t2);
1428 t1.getNativeObject(), t2.getNativeObject()));
1442 checkContextMatch(t);
1444 t.getNativeObject()));
1463 checkContextMatch(t);
1465 (signed) ?
true :
false));
1476 checkContextMatch(t1);
1477 checkContextMatch(t2);
1479 .getNativeObject(), t2.getNativeObject(), (isSigned) ?
true
1491 checkContextMatch(t1);
1492 checkContextMatch(t2);
1494 t1.getNativeObject(), t2.getNativeObject()));
1505 checkContextMatch(t1);
1506 checkContextMatch(t2);
1508 t1.getNativeObject(), t2.getNativeObject()));
1519 checkContextMatch(t1);
1520 checkContextMatch(t2);
1522 .getNativeObject(), t2.getNativeObject(), (isSigned) ?
true
1534 checkContextMatch(t1);
1535 checkContextMatch(t2);
1537 t1.getNativeObject(), t2.getNativeObject()));
1547 checkContextMatch(t);
1549 t.getNativeObject()));
1560 checkContextMatch(t1);
1561 checkContextMatch(t2);
1563 .getNativeObject(), t2.getNativeObject(), (isSigned) ?
true
1575 checkContextMatch(t1);
1576 checkContextMatch(t2);
1578 t1.getNativeObject(), t2.getNativeObject()));
1614 checkContextMatch(a);
1615 checkContextMatch(i);
1619 i.getNativeObject()));
1640 checkContextMatch(a);
1641 checkContextMatch(i);
1642 checkContextMatch(v);
1644 i.getNativeObject(), v.getNativeObject()));
1658 checkContextMatch(domain);
1659 checkContextMatch(v);
1661 domain.getNativeObject(), v.getNativeObject()));
1679 checkContextMatch(f);
1680 checkContextMatch(args);
1682 f.getNativeObject(),
AST.arrayLength(args),
1683 AST.arrayToNative(args)));
1694 checkContextMatch(array);
1695 return Expr.create(
this,
1704 checkContextMatch(ty);
1713 checkContextMatch(domain);
1714 return Expr.create(
this,
1723 checkContextMatch(domain);
1724 return Expr.create(
this,
1733 checkContextMatch(set);
1734 checkContextMatch(element);
1738 element.getNativeObject()));
1746 checkContextMatch(set);
1747 checkContextMatch(element);
1751 element.getNativeObject()));
1759 checkContextMatch(args);
1763 AST.arrayToNative(args)));
1771 checkContextMatch(args);
1775 AST.arrayToNative(args)));
1783 checkContextMatch(arg1);
1784 checkContextMatch(arg2);
1788 arg2.getNativeObject()));
1796 checkContextMatch(arg);
1797 return Expr.create(
this,
1806 checkContextMatch(elem);
1807 checkContextMatch(set);
1811 set.getNativeObject()));
1819 checkContextMatch(arg1);
1820 checkContextMatch(arg2);
1824 arg2.getNativeObject()));
1840 checkContextMatch(ty);
1841 return Expr.create(
this,
1857 checkContextMatch(ty);
1858 return Expr.create(
this,
Native.
mkInt(nCtx(), v, ty.getNativeObject()));
1873 checkContextMatch(ty);
1874 return Expr.create(
this,
1905 .getNativeObject()));
1918 .getNativeObject()));
1931 .getNativeObject()));
1942 .getNativeObject()));
1955 .getNativeObject()));
1968 .getNativeObject()));
2021 int weight,
Pattern[] patterns,
Expr[] noPatterns,
2025 return new Quantifier(
this,
true, sorts, names, body, weight, patterns,
2026 noPatterns, quantifierID, skolemID);
2037 return new Quantifier(
this,
true, boundConstants, body, weight,
2038 patterns, noPatterns, quantifierID, skolemID);
2046 int weight,
Pattern[] patterns,
Expr[] noPatterns,
2050 return new Quantifier(
this,
false, sorts, names, body, weight,
2051 patterns, noPatterns, quantifierID, skolemID);
2062 return new Quantifier(
this,
false, boundConstants, body, weight,
2063 patterns, noPatterns, quantifierID, skolemID);
2076 return mkForall(sorts, names, body, weight, patterns, noPatterns,
2077 quantifierID, skolemID);
2079 return mkExists(sorts, names, body, weight, patterns, noPatterns,
2080 quantifierID, skolemID);
2092 return mkForall(boundConstants, body, weight, patterns, noPatterns,
2093 quantifierID, skolemID);
2095 return mkExists(boundConstants, body, weight, patterns, noPatterns,
2096 quantifierID, skolemID);
2132 String status, String attributes,
BoolExpr[] assumptions,
2137 attributes, (
int) assumptions.length,
2138 AST.arrayToNative(assumptions), formula.getNativeObject());
2153 int csn =
Symbol.arrayLength(sortNames);
2154 int cs =
Sort.arrayLength(sorts);
2155 int cdn =
Symbol.arrayLength(declNames);
2156 int cd =
AST.arrayLength(decls);
2157 if (csn != cs || cdn != cd)
2160 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2161 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2162 AST.arrayToNative(decls));
2173 int csn =
Symbol.arrayLength(sortNames);
2174 int cs =
Sort.arrayLength(sorts);
2175 int cdn =
Symbol.arrayLength(declNames);
2176 int cd =
AST.arrayLength(decls);
2177 if (csn != cs || cdn != cd)
2180 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2181 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2182 AST.arrayToNative(decls));
2203 for (
int i = 0; i < n; i++)
2227 for (
int i = 0; i < n; i++)
2251 for (
int i = 0; i < n; i++)
2274 for (
int i = 0; i < n; i++)
2291 int csn =
Symbol.arrayLength(sortNames);
2292 int cs =
Sort.arrayLength(sorts);
2293 int cdn =
Symbol.arrayLength(declNames);
2294 int cd =
AST.arrayLength(decls);
2295 if (csn != cs || cdn != cd)
2298 str,
AST.arrayLength(sorts),
Symbol.arrayToNative(sortNames),
2299 AST.arrayToNative(sorts),
AST.arrayLength(decls),
2300 Symbol.arrayToNative(declNames),
AST.arrayToNative(decls)));
2312 int csn =
Symbol.arrayLength(sortNames);
2313 int cs =
Sort.arrayLength(sorts);
2314 int cdn =
Symbol.arrayLength(declNames);
2315 int cd =
AST.arrayLength(decls);
2316 if (csn != cs || cdn != cd)
2319 fileName,
AST.arrayLength(sorts),
2320 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2321 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2322 AST.arrayToNative(decls)));
2335 public Goal mkGoal(
boolean models,
boolean unsatCores,
boolean proofs)
2338 return new Goal(
this, models, unsatCores, proofs);
2364 String[] res =
new String[n];
2365 for (
int i = 0; i < n; i++)
2384 return new Tactic(
this, name);
2394 checkContextMatch(t1);
2395 checkContextMatch(t2);
2396 checkContextMatch(ts);
2399 if (ts != null && ts.length > 0)
2401 last = ts[ts.length - 1].getNativeObject();
2402 for (
int i = ts.length - 2; i >= 0; i--)
2410 t1.getNativeObject(), last));
2413 t1.getNativeObject(), t2.getNativeObject()));
2434 checkContextMatch(t1);
2435 checkContextMatch(t2);
2437 t1.getNativeObject(), t2.getNativeObject()));
2448 checkContextMatch(t);
2450 t.getNativeObject(), ms));
2461 checkContextMatch(t);
2462 checkContextMatch(p);
2464 t.getNativeObject()));
2474 checkContextMatch(p);
2475 checkContextMatch(t1);
2476 checkContextMatch(t2);
2478 t1.getNativeObject(), t2.getNativeObject()));
2487 checkContextMatch(t);
2489 t.getNativeObject(), max));
2514 checkContextMatch(p);
2534 checkContextMatch(t);
2535 checkContextMatch(p);
2537 t.getNativeObject(), p.getNativeObject()));
2556 checkContextMatch(t);
2567 checkContextMatch(t1);
2568 checkContextMatch(t2);
2570 t1.getNativeObject(), t2.getNativeObject()));
2598 String[] res =
new String[n];
2599 for (
int i = 0; i < n; i++)
2618 return new Probe(
this, name);
2635 checkContextMatch(p1);
2636 checkContextMatch(p2);
2638 p2.getNativeObject()));
2647 checkContextMatch(p1);
2648 checkContextMatch(p2);
2650 p2.getNativeObject()));
2660 checkContextMatch(p1);
2661 checkContextMatch(p2);
2663 p2.getNativeObject()));
2673 checkContextMatch(p1);
2674 checkContextMatch(p2);
2676 p2.getNativeObject()));
2685 checkContextMatch(p1);
2686 checkContextMatch(p2);
2688 p2.getNativeObject()));
2696 checkContextMatch(p1);
2697 checkContextMatch(p2);
2699 p2.getNativeObject()));
2707 checkContextMatch(p1);
2708 checkContextMatch(p2);
2710 p2.getNativeObject()));
2718 checkContextMatch(p);
2748 logic.getNativeObject()));
2778 t.getNativeObject()));
2897 return new FPSort(
this, ebits, sbits);
3154 return new FPExpr(
this,
Native.
mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3166 return new FPExpr(
this,
Native.
mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3178 return new FPExpr(
this,
Native.
mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3190 return new FPExpr(
this,
Native.
mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3205 return new FPExpr(
this,
Native.
mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3406 return new FPExpr(
this,
Native.
mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3573 return AST.create(
this, nativeObject);
3590 return a.getNativeObject();
3633 Native.setInternalErrorHandler(nCtx());
3636 void checkContextMatch(Z3Object other)
3638 if (
this != other.getContext())
3639 throw new Z3Exception(
"Context mismatch");
3642 void checkContextMatch(Z3Object[] arr)
3645 for (Z3Object a : arr)
3646 checkContextMatch(a);
3649 private ASTDecRefQueue m_AST_DRQ =
new ASTDecRefQueue();
3650 private ASTMapDecRefQueue m_ASTMap_DRQ =
new ASTMapDecRefQueue(10);
3651 private ASTVectorDecRefQueue m_ASTVector_DRQ =
new ASTVectorDecRefQueue(10);
3652 private ApplyResultDecRefQueue m_ApplyResult_DRQ =
new ApplyResultDecRefQueue(10);
3653 private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ =
new FuncInterpEntryDecRefQueue(10);
3654 private FuncInterpDecRefQueue m_FuncInterp_DRQ =
new FuncInterpDecRefQueue(10);
3655 private GoalDecRefQueue m_Goal_DRQ =
new GoalDecRefQueue(10);
3656 private ModelDecRefQueue m_Model_DRQ =
new ModelDecRefQueue(10);
3657 private ParamsDecRefQueue m_Params_DRQ =
new ParamsDecRefQueue(10);
3658 private ParamDescrsDecRefQueue m_ParamDescrs_DRQ =
new ParamDescrsDecRefQueue(10);
3659 private ProbeDecRefQueue m_Probe_DRQ =
new ProbeDecRefQueue(10);
3660 private SolverDecRefQueue m_Solver_DRQ =
new SolverDecRefQueue(10);
3661 private StatisticsDecRefQueue m_Statistics_DRQ =
new StatisticsDecRefQueue(10);
3662 private TacticDecRefQueue m_Tactic_DRQ =
new TacticDecRefQueue(10);
3663 private FixedpointDecRefQueue m_Fixedpoint_DRQ =
new FixedpointDecRefQueue(10);
3672 return m_ASTMap_DRQ;
3677 return m_ASTVector_DRQ;
3682 return m_ApplyResult_DRQ;
3687 return m_FuncEntry_DRQ;
3692 return m_FuncInterp_DRQ;
3707 return m_Params_DRQ;
3712 return m_ParamDescrs_DRQ;
3722 return m_Solver_DRQ;
3727 return m_Statistics_DRQ;
3732 return m_Tactic_DRQ;
3737 return m_Fixedpoint_DRQ;
3749 if (m_refCount == 0)
3770 m_AST_DRQ.clear(
this);
3771 m_ASTMap_DRQ.clear(
this);
3772 m_ASTVector_DRQ.clear(
this);
3773 m_ApplyResult_DRQ.clear(
this);
3774 m_FuncEntry_DRQ.clear(
this);
3775 m_FuncInterp_DRQ.clear(
this);
3776 m_Goal_DRQ.clear(
this);
3777 m_Model_DRQ.clear(
this);
3778 m_Params_DRQ.clear(
this);
3779 m_Probe_DRQ.clear(
this);
3780 m_Solver_DRQ.clear(
this);
3781 m_Statistics_DRQ.clear(
this);
3782 m_Tactic_DRQ.clear(
this);
3783 m_Fixedpoint_DRQ.clear(
this);
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)
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)
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)
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)
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 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)
BoolExpr mkDistinct(Expr...args)
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)
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)
BitVecExpr mkBVNeg(BitVecExpr t)
static long mkFreshConst(long a0, String a1, long a2)
ArithExpr mkSub(ArithExpr...t)
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)
Expr mkSetAdd(Expr set, Expr element)
static long mkFpaIsNegative(long a0, long a1)
StringSymbol mkSymbol(String name)
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)
IDecRefQueue getModelDRQ()
String getProbeDescription(String name)
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkAnd(BoolExpr...t)
static long mkSub(long a0, int a1, long[] a2)
static long tacticFailIf(long a0, long a1)
IDecRefQueue getStatisticsDRQ()
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Tactic failIfNotDecided()
static long mkExtRotateLeft(long a0, long a1, long a2)
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
FPRMNum mkFPRoundTowardNegative()
FPNum mkFP(float v, FPSort s)
static long mkFpaIsPositive(long a0, long a1)
static long mkFpaSort16(long a0)
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
IDecRefQueue getFuncInterpDRQ()
static long mkFpaSqrt(long a0, long a1, long a2)
static long mkBvlshr(long a0, long a1, long a2)
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)
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)
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)
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)
static long mkGe(long a0, long a1, long a2)
static long mkXor(long a0, long a1, long a2)
Expr mkNumeral(String v, Sort ty)
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 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)
FuncDecl mkConstDecl(String name, Sort range)
Expr mkSetDifference(Expr arg1, Expr arg2)
static long probeOr(long a0, long a1, long a2)
SetSort mkSetSort(Sort ty)
IDecRefQueue getApplyResultDRQ()
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
IntExpr mkReal2Int(RealExpr t)
Expr mkSetComplement(Expr arg)
IDecRefQueue getParamDescrsDRQ()
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)
static long mkSetComplement(long a0, long a1)
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)
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 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)
BitVecExpr mkBVNot(BitVecExpr t)
static long mkFpaGeq(long a0, long a1, long a2)
static long mkFpaGt(long a0, long a1, long a2)
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)
IDecRefQueue getTacticDRQ()
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)
ArrayExpr mkMap(FuncDecl f, ArrayExpr...args)
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)
static long tacticParOr(long a0, int a1, long[] a2)
static long tacticSkip(long a0)
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)
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)
Tactic then(Tactic t1, Tactic t2, Tactic...ts)
FPNum mkFP(int v, FPSort s)
Tactic tryFor(Tactic t, int ms)
static long probeGt(long a0, long a1, long a2)
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
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)
Expr mkSetUnion(Expr...args)
IDecRefQueue getASTVectorDRQ()
static long mkFpaSortSingle(long a0)
static long mkEq(long a0, long a1, long a2)
static long mkRem(long a0, long a1, long a2)
IDecRefQueue getASTMapDRQ()
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)
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)
ArithExpr mkAdd(ArithExpr...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)
Expr mkSetMembership(Expr elem, Expr set)
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)
IDecRefQueue getParamsDRQ()
static long mkPattern(long a0, int a1, long[] a2)
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
UninterpretedSort mkUninterpretedSort(Symbol s)
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)
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)
Expr mkFreshConst(String prefix, Sort range)
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
static long mkAnd(long a0, int a1, long[] a2)
static long mkLt(long a0, long a1, long a2)
Expr mkFullSet(Sort domain)
static long mkContextRc(long a0)
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
BoolExpr mkOr(BoolExpr...t)
static long mkFpaRtp(long a0)
FPNum mkFP(double v, FPSort s)
static long mkFpaRoundTowardPositive(long a0)
Expr mkSetIntersection(Expr...args)
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)
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)
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)
static long mkBvashr(long a0, long a1, long a2)
static long mkGt(long a0, long a1, long a2)
IDecRefQueue getGoalDRQ()
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)
static long probeLe(long a0, long a1, long a2)
Context(Map< String, String > settings)
BoolExpr mkBoolConst(Symbol name)
static long mkFpaIsInfinite(long a0, long a1)
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
IntSymbol mkSymbol(int i)
Expr mkApp(FuncDecl f, Expr...args)
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
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)
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)
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)
Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
static long mkBvxor(long a0, long a1, long a2)
EnumSort mkEnumSort(String name, String...enumNames)
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)
Expr mkSetDel(Expr set, Expr element)
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)
static long mkEmptySet(long a0, long a1)
static long mkFpaRoundNearestTiesToEven(long a0)
Expr mkBound(int index, Sort ty)
IDecRefQueue getSolverDRQ()
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
FPNum mkFPNumeral(float v, FPSort s)
static String getTacticName(long a0, int 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 mkBound(long a0, int a1, long a2)
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)
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)
static long mkFpaLt(long a0, long a1, long a2)
ParamDescrs getSimplifyParameterDescriptions()
Fixedpoint mkFixedpoint()
static long mkBvxnor(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)
BitVecNum mkBV(int v, int size)
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)
EnumSort mkEnumSort(Symbol name, Symbol...enumNames)
static long probeAnd(long a0, long a1, long a2)
RealExpr mkInt2Real(IntExpr t)
RealExpr mkRealConst(Symbol name)
static long mkBvmul(long a0, long a1, long a2)
static long mkFpaSortQuadruple(long a0)
Expr mkSetSubset(Expr arg1, Expr arg2)
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)
ArithExpr mkMul(ArithExpr...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)
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)
Expr mkEmptySet(Sort domain)
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
static long mkIsInt(long a0, long a1)
FPRMNum mkFPRoundTowardZero()
Pattern mkPattern(Expr...terms)
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)
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)
FuncDecl[] getSMTLIBDecls()
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
IDecRefQueue getProbeDRQ()
Tactic andThen(Tactic t1, Tactic t2, Tactic...ts)
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
IDecRefQueue getFixedpointDRQ()
static long tacticCond(long a0, long a1, long a2, long a3)
IDecRefQueue getFuncEntryDRQ()
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)