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++)
376 (nCtx(), field.getNativeObject(),
377 t.getNativeObject(), v.getNativeObject()));
387 checkContextMatch(name);
388 checkContextMatch(domain);
389 checkContextMatch(range);
390 return new FuncDecl(
this, name, domain, range);
399 checkContextMatch(name);
400 checkContextMatch(domain);
401 checkContextMatch(range);
403 return new FuncDecl(
this, name, q, range);
412 checkContextMatch(domain);
413 checkContextMatch(range);
423 checkContextMatch(domain);
424 checkContextMatch(range);
438 checkContextMatch(domain);
439 checkContextMatch(range);
440 return new FuncDecl(
this, prefix, domain, range);
448 checkContextMatch(name);
449 checkContextMatch(range);
450 return new FuncDecl(
this, name, null, range);
458 checkContextMatch(range);
471 checkContextMatch(range);
472 return new FuncDecl(
this, prefix, null, range);
482 return Expr.create(
this,
491 if (terms.length == 0)
492 throw new Z3Exception(
"Cannot create a pattern from zero terms");
494 long[] termsNative =
AST.arrayToNative(terms);
505 checkContextMatch(name);
506 checkContextMatch(range);
511 range.getNativeObject()));
529 checkContextMatch(range);
530 return Expr.create(
this,
612 checkContextMatch(f);
613 checkContextMatch(args);
614 return Expr.create(
this, f, args);
646 checkContextMatch(x);
647 checkContextMatch(y);
649 y.getNativeObject()));
657 checkContextMatch(args);
659 AST.arrayToNative(args)));
667 checkContextMatch(a);
680 checkContextMatch(t1);
681 checkContextMatch(t2);
682 checkContextMatch(t3);
684 t2.getNativeObject(), t3.getNativeObject()));
692 checkContextMatch(t1);
693 checkContextMatch(t2);
695 t2.getNativeObject()));
703 checkContextMatch(t1);
704 checkContextMatch(t2);
706 t1.getNativeObject(), t2.getNativeObject()));
714 checkContextMatch(t1);
715 checkContextMatch(t2);
717 t2.getNativeObject()));
725 checkContextMatch(t);
727 AST.arrayToNative(t)));
735 checkContextMatch(t);
737 AST.arrayToNative(t)));
745 checkContextMatch(t);
755 checkContextMatch(t);
765 checkContextMatch(t);
775 checkContextMatch(t);
785 checkContextMatch(t1);
786 checkContextMatch(t2);
788 t1.getNativeObject(), t2.getNativeObject()));
798 checkContextMatch(t1);
799 checkContextMatch(t2);
801 t2.getNativeObject()));
811 checkContextMatch(t1);
812 checkContextMatch(t2);
814 t2.getNativeObject()));
822 checkContextMatch(t1);
823 checkContextMatch(t2);
827 t2.getNativeObject()));
835 checkContextMatch(t1);
836 checkContextMatch(t2);
838 t2.getNativeObject()));
846 checkContextMatch(t1);
847 checkContextMatch(t2);
849 t2.getNativeObject()));
857 checkContextMatch(t1);
858 checkContextMatch(t2);
860 t2.getNativeObject()));
868 checkContextMatch(t1);
869 checkContextMatch(t2);
871 t2.getNativeObject()));
886 checkContextMatch(t);
899 checkContextMatch(t);
908 checkContextMatch(t);
919 checkContextMatch(t);
930 checkContextMatch(t);
932 t.getNativeObject()));
942 checkContextMatch(t);
944 t.getNativeObject()));
954 checkContextMatch(t1);
955 checkContextMatch(t2);
957 t1.getNativeObject(), t2.getNativeObject()));
967 checkContextMatch(t1);
968 checkContextMatch(t2);
970 t2.getNativeObject()));
980 checkContextMatch(t1);
981 checkContextMatch(t2);
983 t1.getNativeObject(), t2.getNativeObject()));
993 checkContextMatch(t1);
994 checkContextMatch(t2);
996 t1.getNativeObject(), t2.getNativeObject()));
1006 checkContextMatch(t1);
1007 checkContextMatch(t2);
1009 t1.getNativeObject(), t2.getNativeObject()));
1019 checkContextMatch(t1);
1020 checkContextMatch(t2);
1022 t1.getNativeObject(), t2.getNativeObject()));
1032 checkContextMatch(t);
1043 checkContextMatch(t1);
1044 checkContextMatch(t2);
1046 t1.getNativeObject(), t2.getNativeObject()));
1056 checkContextMatch(t1);
1057 checkContextMatch(t2);
1059 t1.getNativeObject(), t2.getNativeObject()));
1069 checkContextMatch(t1);
1070 checkContextMatch(t2);
1072 t1.getNativeObject(), t2.getNativeObject()));
1084 checkContextMatch(t1);
1085 checkContextMatch(t2);
1087 t1.getNativeObject(), t2.getNativeObject()));
1105 checkContextMatch(t1);
1106 checkContextMatch(t2);
1108 t1.getNativeObject(), t2.getNativeObject()));
1120 checkContextMatch(t1);
1121 checkContextMatch(t2);
1123 t1.getNativeObject(), t2.getNativeObject()));
1138 checkContextMatch(t1);
1139 checkContextMatch(t2);
1141 t1.getNativeObject(), t2.getNativeObject()));
1152 checkContextMatch(t1);
1153 checkContextMatch(t2);
1155 t1.getNativeObject(), t2.getNativeObject()));
1165 checkContextMatch(t1);
1166 checkContextMatch(t2);
1168 t2.getNativeObject()));
1178 checkContextMatch(t1);
1179 checkContextMatch(t2);
1181 t2.getNativeObject()));
1191 checkContextMatch(t1);
1192 checkContextMatch(t2);
1194 t2.getNativeObject()));
1204 checkContextMatch(t1);
1205 checkContextMatch(t2);
1207 t2.getNativeObject()));
1217 checkContextMatch(t1);
1218 checkContextMatch(t2);
1220 t2.getNativeObject()));
1230 checkContextMatch(t1);
1231 checkContextMatch(t2);
1233 t2.getNativeObject()));
1243 checkContextMatch(t1);
1244 checkContextMatch(t2);
1246 t2.getNativeObject()));
1256 checkContextMatch(t1);
1257 checkContextMatch(t2);
1259 t2.getNativeObject()));
1274 checkContextMatch(t1);
1275 checkContextMatch(t2);
1277 t1.getNativeObject(), t2.getNativeObject()));
1291 checkContextMatch(t);
1293 t.getNativeObject()));
1305 checkContextMatch(t);
1307 t.getNativeObject()));
1319 checkContextMatch(t);
1321 t.getNativeObject()));
1331 checkContextMatch(t);
1333 t.getNativeObject()));
1349 checkContextMatch(t1);
1350 checkContextMatch(t2);
1352 t1.getNativeObject(), t2.getNativeObject()));
1368 checkContextMatch(t1);
1369 checkContextMatch(t2);
1371 t1.getNativeObject(), t2.getNativeObject()));
1388 checkContextMatch(t1);
1389 checkContextMatch(t2);
1391 t1.getNativeObject(), t2.getNativeObject()));
1401 checkContextMatch(t);
1403 t.getNativeObject()));
1413 checkContextMatch(t);
1415 t.getNativeObject()));
1427 checkContextMatch(t1);
1428 checkContextMatch(t2);
1430 t1.getNativeObject(), t2.getNativeObject()));
1442 checkContextMatch(t1);
1443 checkContextMatch(t2);
1445 t1.getNativeObject(), t2.getNativeObject()));
1459 checkContextMatch(t);
1461 t.getNativeObject()));
1480 checkContextMatch(t);
1482 (signed) ?
true :
false));
1493 checkContextMatch(t1);
1494 checkContextMatch(t2);
1496 .getNativeObject(), t2.getNativeObject(), (isSigned) ?
true 1508 checkContextMatch(t1);
1509 checkContextMatch(t2);
1511 t1.getNativeObject(), t2.getNativeObject()));
1522 checkContextMatch(t1);
1523 checkContextMatch(t2);
1525 t1.getNativeObject(), t2.getNativeObject()));
1536 checkContextMatch(t1);
1537 checkContextMatch(t2);
1539 .getNativeObject(), t2.getNativeObject(), (isSigned) ?
true 1551 checkContextMatch(t1);
1552 checkContextMatch(t2);
1554 t1.getNativeObject(), t2.getNativeObject()));
1564 checkContextMatch(t);
1566 t.getNativeObject()));
1577 checkContextMatch(t1);
1578 checkContextMatch(t2);
1580 .getNativeObject(), t2.getNativeObject(), (isSigned) ?
true 1592 checkContextMatch(t1);
1593 checkContextMatch(t2);
1595 t1.getNativeObject(), t2.getNativeObject()));
1631 checkContextMatch(a);
1632 checkContextMatch(i);
1636 i.getNativeObject()));
1657 checkContextMatch(a);
1658 checkContextMatch(i);
1659 checkContextMatch(v);
1661 i.getNativeObject(), v.getNativeObject()));
1675 checkContextMatch(domain);
1676 checkContextMatch(v);
1678 domain.getNativeObject(), v.getNativeObject()));
1696 checkContextMatch(f);
1697 checkContextMatch(args);
1699 f.getNativeObject(),
AST.arrayLength(args),
1700 AST.arrayToNative(args)));
1711 checkContextMatch(array);
1712 return Expr.create(
this,
1721 checkContextMatch(ty);
1730 checkContextMatch(domain);
1740 checkContextMatch(domain);
1750 checkContextMatch(
set);
1751 checkContextMatch(element);
1754 element.getNativeObject()));
1762 checkContextMatch(
set);
1763 checkContextMatch(element);
1766 element.getNativeObject()));
1774 checkContextMatch(args);
1777 AST.arrayToNative(args)));
1785 checkContextMatch(args);
1788 AST.arrayToNative(args)));
1796 checkContextMatch(arg1);
1797 checkContextMatch(arg2);
1800 arg2.getNativeObject()));
1808 checkContextMatch(arg);
1818 checkContextMatch(elem);
1819 checkContextMatch(
set);
1822 set.getNativeObject()));
1830 checkContextMatch(arg1);
1831 checkContextMatch(arg2);
1834 arg2.getNativeObject()));
1850 checkContextMatch(ty);
1851 return Expr.create(
this,
1867 checkContextMatch(ty);
1868 return Expr.create(
this,
Native.
mkInt(nCtx(), v, ty.getNativeObject()));
1883 checkContextMatch(ty);
1884 return Expr.create(
this,
1915 .getNativeObject()));
1928 .getNativeObject()));
1941 .getNativeObject()));
1952 .getNativeObject()));
1965 .getNativeObject()));
1978 .getNativeObject()));
2031 int weight,
Pattern[] patterns,
Expr[] noPatterns,
2035 return new Quantifier(
this,
true, sorts, names, body, weight, patterns,
2036 noPatterns, quantifierID, skolemID);
2047 return new Quantifier(
this,
true, boundConstants, body, weight,
2048 patterns, noPatterns, quantifierID, skolemID);
2056 int weight,
Pattern[] patterns,
Expr[] noPatterns,
2060 return new Quantifier(
this,
false, sorts, names, body, weight,
2061 patterns, noPatterns, quantifierID, skolemID);
2072 return new Quantifier(
this,
false, boundConstants, body, weight,
2073 patterns, noPatterns, quantifierID, skolemID);
2086 return mkForall(sorts, names, body, weight, patterns, noPatterns,
2087 quantifierID, skolemID);
2089 return mkExists(sorts, names, body, weight, patterns, noPatterns,
2090 quantifierID, skolemID);
2102 return mkForall(boundConstants, body, weight, patterns, noPatterns,
2103 quantifierID, skolemID);
2105 return mkExists(boundConstants, body, weight, patterns, noPatterns,
2106 quantifierID, skolemID);
2142 String status, String attributes,
BoolExpr[] assumptions,
2147 attributes, (
int) assumptions.length,
2148 AST.arrayToNative(assumptions), formula.getNativeObject());
2163 int csn =
Symbol.arrayLength(sortNames);
2164 int cs =
Sort.arrayLength(sorts);
2165 int cdn =
Symbol.arrayLength(declNames);
2166 int cd =
AST.arrayLength(decls);
2167 if (csn != cs || cdn != cd)
2170 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2171 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2172 AST.arrayToNative(decls));
2183 int csn =
Symbol.arrayLength(sortNames);
2184 int cs =
Sort.arrayLength(sorts);
2185 int cdn =
Symbol.arrayLength(declNames);
2186 int cd =
AST.arrayLength(decls);
2187 if (csn != cs || cdn != cd)
2190 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2191 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2192 AST.arrayToNative(decls));
2213 for (
int i = 0; i < n; i++)
2237 for (
int i = 0; i < n; i++)
2261 for (
int i = 0; i < n; i++)
2284 for (
int i = 0; i < n; i++)
2301 int csn =
Symbol.arrayLength(sortNames);
2302 int cs =
Sort.arrayLength(sorts);
2303 int cdn =
Symbol.arrayLength(declNames);
2304 int cd =
AST.arrayLength(decls);
2305 if (csn != cs || cdn != cd)
2308 str,
AST.arrayLength(sorts),
Symbol.arrayToNative(sortNames),
2309 AST.arrayToNative(sorts),
AST.arrayLength(decls),
2310 Symbol.arrayToNative(declNames),
AST.arrayToNative(decls)));
2322 int csn =
Symbol.arrayLength(sortNames);
2323 int cs =
Sort.arrayLength(sorts);
2324 int cdn =
Symbol.arrayLength(declNames);
2325 int cd =
AST.arrayLength(decls);
2326 if (csn != cs || cdn != cd)
2329 fileName,
AST.arrayLength(sorts),
2330 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2331 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2332 AST.arrayToNative(decls)));
2345 public Goal mkGoal(
boolean models,
boolean unsatCores,
boolean proofs)
2348 return new Goal(
this, models, unsatCores, proofs);
2374 String[] res =
new String[n];
2375 for (
int i = 0; i < n; i++)
2394 return new Tactic(
this, name);
2404 checkContextMatch(t1);
2405 checkContextMatch(t2);
2406 checkContextMatch(ts);
2409 if (ts != null && ts.length > 0)
2411 last = ts[ts.length - 1].getNativeObject();
2412 for (
int i = ts.length - 2; i >= 0; i--)
2420 t1.getNativeObject(), last));
2423 t1.getNativeObject(), t2.getNativeObject()));
2444 checkContextMatch(t1);
2445 checkContextMatch(t2);
2447 t1.getNativeObject(), t2.getNativeObject()));
2458 checkContextMatch(t);
2460 t.getNativeObject(), ms));
2471 checkContextMatch(t);
2472 checkContextMatch(p);
2474 t.getNativeObject()));
2484 checkContextMatch(p);
2485 checkContextMatch(t1);
2486 checkContextMatch(t2);
2488 t1.getNativeObject(), t2.getNativeObject()));
2497 checkContextMatch(t);
2499 t.getNativeObject(), max));
2524 checkContextMatch(p);
2544 checkContextMatch(t);
2545 checkContextMatch(p);
2547 t.getNativeObject(), p.getNativeObject()));
2566 checkContextMatch(t);
2577 checkContextMatch(t1);
2578 checkContextMatch(t2);
2580 t1.getNativeObject(), t2.getNativeObject()));
2608 String[] res =
new String[n];
2609 for (
int i = 0; i < n; i++)
2628 return new Probe(
this, name);
2645 checkContextMatch(p1);
2646 checkContextMatch(p2);
2648 p2.getNativeObject()));
2657 checkContextMatch(p1);
2658 checkContextMatch(p2);
2660 p2.getNativeObject()));
2670 checkContextMatch(p1);
2671 checkContextMatch(p2);
2673 p2.getNativeObject()));
2683 checkContextMatch(p1);
2684 checkContextMatch(p2);
2686 p2.getNativeObject()));
2695 checkContextMatch(p1);
2696 checkContextMatch(p2);
2698 p2.getNativeObject()));
2706 checkContextMatch(p1);
2707 checkContextMatch(p2);
2709 p2.getNativeObject()));
2717 checkContextMatch(p1);
2718 checkContextMatch(p2);
2720 p2.getNativeObject()));
2728 checkContextMatch(p);
2758 logic.getNativeObject()));
2788 t.getNativeObject()));
2915 return new FPSort(
this, ebits, sbits);
3172 return new FPExpr(
this,
Native.
mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3184 return new FPExpr(
this,
Native.
mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3196 return new FPExpr(
this,
Native.
mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3208 return new FPExpr(
this,
Native.
mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3223 return new FPExpr(
this,
Native.
mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3424 return new FPExpr(
this,
Native.
mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3591 return AST.create(
this, nativeObject);
3608 return a.getNativeObject();
3654 void checkContextMatch(
Z3Object other)
3656 if (
this != other.getContext())
3660 void checkContextMatch(
Z3Object[] arr)
3664 checkContextMatch(a);
3667 private ASTDecRefQueue m_AST_DRQ =
new ASTDecRefQueue();
3668 private ASTMapDecRefQueue m_ASTMap_DRQ =
new ASTMapDecRefQueue(10);
3669 private ASTVectorDecRefQueue m_ASTVector_DRQ =
new ASTVectorDecRefQueue(10);
3670 private ApplyResultDecRefQueue m_ApplyResult_DRQ =
new ApplyResultDecRefQueue(10);
3671 private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ =
new FuncInterpEntryDecRefQueue(10);
3672 private FuncInterpDecRefQueue m_FuncInterp_DRQ =
new FuncInterpDecRefQueue(10);
3673 private GoalDecRefQueue m_Goal_DRQ =
new GoalDecRefQueue(10);
3674 private ModelDecRefQueue m_Model_DRQ =
new ModelDecRefQueue(10);
3675 private ParamsDecRefQueue m_Params_DRQ =
new ParamsDecRefQueue(10);
3676 private ParamDescrsDecRefQueue m_ParamDescrs_DRQ =
new ParamDescrsDecRefQueue(10);
3677 private ProbeDecRefQueue m_Probe_DRQ =
new ProbeDecRefQueue(10);
3678 private SolverDecRefQueue m_Solver_DRQ =
new SolverDecRefQueue(10);
3679 private StatisticsDecRefQueue m_Statistics_DRQ =
new StatisticsDecRefQueue(10);
3680 private TacticDecRefQueue m_Tactic_DRQ =
new TacticDecRefQueue(10);
3681 private FixedpointDecRefQueue m_Fixedpoint_DRQ =
new FixedpointDecRefQueue(10);
3682 private OptimizeDecRefQueue m_Optimize_DRQ =
new OptimizeDecRefQueue(10);
3691 return m_ASTMap_DRQ;
3696 return m_ASTVector_DRQ;
3701 return m_ApplyResult_DRQ;
3706 return m_FuncEntry_DRQ;
3711 return m_FuncInterp_DRQ;
3726 return m_Params_DRQ;
3731 return m_ParamDescrs_DRQ;
3741 return m_Solver_DRQ;
3746 return m_Statistics_DRQ;
3751 return m_Tactic_DRQ;
3756 return m_Fixedpoint_DRQ;
3761 return m_Optimize_DRQ;
3773 if (m_refCount == 0)
3794 m_AST_DRQ.clear(
this);
3795 m_ASTMap_DRQ.clear(
this);
3796 m_ASTVector_DRQ.clear(
this);
3797 m_ApplyResult_DRQ.clear(
this);
3798 m_FuncEntry_DRQ.clear(
this);
3799 m_FuncInterp_DRQ.clear(
this);
3800 m_Goal_DRQ.clear(
this);
3801 m_Model_DRQ.clear(
this);
3802 m_Params_DRQ.clear(
this);
3803 m_Probe_DRQ.clear(
this);
3804 m_Solver_DRQ.clear(
this);
3805 m_Statistics_DRQ.clear(
this);
3806 m_Tactic_DRQ.clear(
this);
3807 m_Fixedpoint_DRQ.clear(
this);
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)
IDecRefQueue getOptimizeDRQ()
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)
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)
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)
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)
ArrayExpr mkSetUnion(ArrayExpr...args)
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)
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)
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)
BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
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)
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 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)
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)
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)
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)
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()
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)
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)
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 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)
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)
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)
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)
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)
def EnumSort(name, values, ctx=None)
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)
ArrayExpr mkFullSet(Sort domain)
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)
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)
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)
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)
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)
ArrayExpr mkSetIntersection(ArrayExpr...args)
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)
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)
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)
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)