18 package com.microsoft.z3;
36 private final long m_ctx;
37 static final Object creation_lock =
new Object();
40 synchronized (creation_lock) {
47 synchronized (creation_lock) {
71 public Context(Map<String, String> settings) {
72 synchronized (creation_lock) {
114 for (
int i = 0; i < names.length; ++i)
120 private IntSort m_intSort = null;
122 private SeqSort m_stringSort = null;
129 if (m_boolSort == null) {
140 if (m_intSort == null) {
151 if (m_realSort == null) {
170 if (m_stringSort == null) {
181 checkContextMatch(s);
222 checkContextMatch(domain);
223 checkContextMatch(range);
224 return new ArraySort(
this, domain, range);
233 checkContextMatch(domains);
234 checkContextMatch(range);
235 return new ArraySort(
this, domains, range);
269 checkContextMatch(name);
270 checkContextMatch(fieldNames);
271 checkContextMatch(fieldSorts);
272 return new TupleSort(
this, name, fieldNames.length, fieldNames,
282 checkContextMatch(name);
283 checkContextMatch(enumNames);
284 return new EnumSort(
this, name, enumNames);
301 checkContextMatch(name);
302 checkContextMatch(elemSort);
303 return new ListSort(
this, name, elemSort);
311 checkContextMatch(elemSort);
321 checkContextMatch(name);
346 Symbol[] fieldNames,
Sort[] sorts,
int[] sortRefs)
349 return of(
this, name, recognizer, fieldNames, sorts,
357 String[] fieldNames,
Sort[] sorts,
int[] sortRefs)
360 mkSymbols(fieldNames), sorts, sortRefs);
369 checkContextMatch(name);
370 checkContextMatch(constructors);
380 checkContextMatch(constructors);
392 checkContextMatch(names);
393 int n = names.length;
395 long[] n_constr =
new long[n];
396 for (
int i = 0; i < n; i++)
400 checkContextMatch(constructor);
402 n_constr[i] = cla[i].getNativeObject();
404 long[] n_res =
new long[n];
408 for (
int i = 0; i < n; i++)
431 return Expr.create (
this,
433 (nCtx(), field.getNativeObject(),
434 t.getNativeObject(), v.getNativeObject()));
444 checkContextMatch(name);
445 checkContextMatch(domain);
446 checkContextMatch(range);
447 return new FuncDecl(
this, name, domain, range);
456 checkContextMatch(name);
457 checkContextMatch(domain);
458 checkContextMatch(range);
460 return new FuncDecl(
this, name, q, range);
469 checkContextMatch(domain);
470 checkContextMatch(range);
480 checkContextMatch(domain);
481 checkContextMatch(range);
495 checkContextMatch(domain);
496 checkContextMatch(range);
497 return new FuncDecl(
this, prefix, domain, range);
505 checkContextMatch(name);
506 checkContextMatch(range);
507 return new FuncDecl(
this, name, null, range);
515 checkContextMatch(range);
528 checkContextMatch(range);
529 return new FuncDecl(
this, prefix, null, range);
539 return Expr.create(
this,
548 if (terms.length == 0)
549 throw new Z3Exception(
"Cannot create a pattern from zero terms");
551 long[] termsNative =
AST.arrayToNative(terms);
562 checkContextMatch(name);
563 checkContextMatch(range);
568 range.getNativeObject()));
586 checkContextMatch(range);
587 return Expr.create(
this,
669 checkContextMatch(f);
670 checkContextMatch(args);
671 return Expr.create(
this, f, args);
703 checkContextMatch(x);
704 checkContextMatch(y);
706 y.getNativeObject()));
714 checkContextMatch(args);
716 AST.arrayToNative(args)));
724 checkContextMatch(a);
737 checkContextMatch(t1);
738 checkContextMatch(t2);
739 checkContextMatch(t3);
741 t2.getNativeObject(), t3.getNativeObject()));
749 checkContextMatch(t1);
750 checkContextMatch(t2);
752 t2.getNativeObject()));
760 checkContextMatch(t1);
761 checkContextMatch(t2);
763 t1.getNativeObject(), t2.getNativeObject()));
771 checkContextMatch(t1);
772 checkContextMatch(t2);
774 t2.getNativeObject()));
782 checkContextMatch(t);
784 AST.arrayToNative(t)));
792 checkContextMatch(t);
794 AST.arrayToNative(t)));
802 checkContextMatch(t);
812 checkContextMatch(t);
822 checkContextMatch(t);
832 checkContextMatch(t);
842 checkContextMatch(t1);
843 checkContextMatch(t2);
845 t1.getNativeObject(), t2.getNativeObject()));
855 checkContextMatch(t1);
856 checkContextMatch(t2);
858 t2.getNativeObject()));
868 checkContextMatch(t1);
869 checkContextMatch(t2);
871 t2.getNativeObject()));
879 checkContextMatch(t1);
880 checkContextMatch(t2);
884 t2.getNativeObject()));
892 checkContextMatch(t1);
893 checkContextMatch(t2);
895 t2.getNativeObject()));
903 checkContextMatch(t1);
904 checkContextMatch(t2);
906 t2.getNativeObject()));
914 checkContextMatch(t1);
915 checkContextMatch(t2);
917 t2.getNativeObject()));
925 checkContextMatch(t1);
926 checkContextMatch(t2);
928 t2.getNativeObject()));
943 checkContextMatch(t);
956 checkContextMatch(t);
965 checkContextMatch(t);
976 checkContextMatch(t);
987 checkContextMatch(t);
989 t.getNativeObject()));
999 checkContextMatch(t);
1001 t.getNativeObject()));
1011 checkContextMatch(t1);
1012 checkContextMatch(t2);
1014 t1.getNativeObject(), t2.getNativeObject()));
1024 checkContextMatch(t1);
1025 checkContextMatch(t2);
1027 t2.getNativeObject()));
1037 checkContextMatch(t1);
1038 checkContextMatch(t2);
1040 t1.getNativeObject(), t2.getNativeObject()));
1050 checkContextMatch(t1);
1051 checkContextMatch(t2);
1053 t1.getNativeObject(), t2.getNativeObject()));
1063 checkContextMatch(t1);
1064 checkContextMatch(t2);
1066 t1.getNativeObject(), t2.getNativeObject()));
1076 checkContextMatch(t1);
1077 checkContextMatch(t2);
1079 t1.getNativeObject(), t2.getNativeObject()));
1089 checkContextMatch(t);
1100 checkContextMatch(t1);
1101 checkContextMatch(t2);
1103 t1.getNativeObject(), t2.getNativeObject()));
1113 checkContextMatch(t1);
1114 checkContextMatch(t2);
1116 t1.getNativeObject(), t2.getNativeObject()));
1126 checkContextMatch(t1);
1127 checkContextMatch(t2);
1129 t1.getNativeObject(), t2.getNativeObject()));
1141 checkContextMatch(t1);
1142 checkContextMatch(t2);
1144 t1.getNativeObject(), t2.getNativeObject()));
1162 checkContextMatch(t1);
1163 checkContextMatch(t2);
1165 t1.getNativeObject(), t2.getNativeObject()));
1177 checkContextMatch(t1);
1178 checkContextMatch(t2);
1180 t1.getNativeObject(), t2.getNativeObject()));
1195 checkContextMatch(t1);
1196 checkContextMatch(t2);
1198 t1.getNativeObject(), t2.getNativeObject()));
1209 checkContextMatch(t1);
1210 checkContextMatch(t2);
1212 t1.getNativeObject(), t2.getNativeObject()));
1222 checkContextMatch(t1);
1223 checkContextMatch(t2);
1225 t2.getNativeObject()));
1235 checkContextMatch(t1);
1236 checkContextMatch(t2);
1238 t2.getNativeObject()));
1248 checkContextMatch(t1);
1249 checkContextMatch(t2);
1251 t2.getNativeObject()));
1261 checkContextMatch(t1);
1262 checkContextMatch(t2);
1264 t2.getNativeObject()));
1274 checkContextMatch(t1);
1275 checkContextMatch(t2);
1277 t2.getNativeObject()));
1287 checkContextMatch(t1);
1288 checkContextMatch(t2);
1290 t2.getNativeObject()));
1300 checkContextMatch(t1);
1301 checkContextMatch(t2);
1303 t2.getNativeObject()));
1313 checkContextMatch(t1);
1314 checkContextMatch(t2);
1316 t2.getNativeObject()));
1331 checkContextMatch(t1);
1332 checkContextMatch(t2);
1334 t1.getNativeObject(), t2.getNativeObject()));
1348 checkContextMatch(t);
1350 t.getNativeObject()));
1362 checkContextMatch(t);
1364 t.getNativeObject()));
1376 checkContextMatch(t);
1378 t.getNativeObject()));
1388 checkContextMatch(t);
1390 t.getNativeObject()));
1406 checkContextMatch(t1);
1407 checkContextMatch(t2);
1409 t1.getNativeObject(), t2.getNativeObject()));
1425 checkContextMatch(t1);
1426 checkContextMatch(t2);
1428 t1.getNativeObject(), t2.getNativeObject()));
1445 checkContextMatch(t1);
1446 checkContextMatch(t2);
1448 t1.getNativeObject(), t2.getNativeObject()));
1458 checkContextMatch(t);
1460 t.getNativeObject()));
1470 checkContextMatch(t);
1472 t.getNativeObject()));
1484 checkContextMatch(t1);
1485 checkContextMatch(t2);
1487 t1.getNativeObject(), t2.getNativeObject()));
1499 checkContextMatch(t1);
1500 checkContextMatch(t2);
1502 t1.getNativeObject(), t2.getNativeObject()));
1516 checkContextMatch(t);
1518 t.getNativeObject()));
1537 checkContextMatch(t);
1550 checkContextMatch(t1);
1551 checkContextMatch(t2);
1553 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1564 checkContextMatch(t1);
1565 checkContextMatch(t2);
1567 t1.getNativeObject(), t2.getNativeObject()));
1578 checkContextMatch(t1);
1579 checkContextMatch(t2);
1581 t1.getNativeObject(), t2.getNativeObject()));
1592 checkContextMatch(t1);
1593 checkContextMatch(t2);
1595 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1606 checkContextMatch(t1);
1607 checkContextMatch(t2);
1609 t1.getNativeObject(), t2.getNativeObject()));
1619 checkContextMatch(t);
1621 t.getNativeObject()));
1632 checkContextMatch(t1);
1633 checkContextMatch(t2);
1635 .getNativeObject(), t2.getNativeObject(), (isSigned)));
1646 checkContextMatch(t1);
1647 checkContextMatch(t2);
1649 t1.getNativeObject(), t2.getNativeObject()));
1685 checkContextMatch(a);
1686 checkContextMatch(i);
1690 i.getNativeObject()));
1708 checkContextMatch(a);
1709 checkContextMatch(args);
1712 Native.
mkSelectN(nCtx(), a.getNativeObject(), args.length,
AST.arrayToNative(args)));
1733 checkContextMatch(a);
1734 checkContextMatch(i);
1735 checkContextMatch(v);
1737 i.getNativeObject(), v.getNativeObject()));
1758 checkContextMatch(a);
1759 checkContextMatch(args);
1760 checkContextMatch(v);
1762 args.length,
AST.arrayToNative(args), v.getNativeObject()));
1776 checkContextMatch(domain);
1777 checkContextMatch(v);
1779 domain.getNativeObject(), v.getNativeObject()));
1797 checkContextMatch(f);
1798 checkContextMatch(args);
1800 f.getNativeObject(),
AST.arrayLength(args),
1801 AST.arrayToNative(args)));
1812 checkContextMatch(array);
1813 return Expr.create(
this,
1822 checkContextMatch(arg1);
1823 checkContextMatch(arg2);
1824 return Expr.create(
this,
Native.
mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
1833 checkContextMatch(ty);
1842 checkContextMatch(domain);
1852 checkContextMatch(domain);
1862 checkContextMatch(set);
1863 checkContextMatch(element);
1866 element.getNativeObject()));
1874 checkContextMatch(set);
1875 checkContextMatch(element);
1878 element.getNativeObject()));
1886 checkContextMatch(args);
1889 AST.arrayToNative(args)));
1897 checkContextMatch(args);
1900 AST.arrayToNative(args)));
1908 checkContextMatch(arg1);
1909 checkContextMatch(arg2);
1912 arg2.getNativeObject()));
1920 checkContextMatch(arg);
1930 checkContextMatch(elem);
1931 checkContextMatch(set);
1934 set.getNativeObject()));
1942 checkContextMatch(arg1);
1943 checkContextMatch(arg2);
1946 arg2.getNativeObject()));
1959 checkContextMatch(s);
1968 checkContextMatch(elem);
2001 checkContextMatch(t);
2011 checkContextMatch(s);
2020 checkContextMatch(s1, s2);
2029 checkContextMatch(s1, s2);
2038 checkContextMatch(s1, s2);
2047 checkContextMatch(s, index);
2056 checkContextMatch(s, offset, length);
2065 checkContextMatch(s, substr, offset);
2066 return (
IntExpr)
Expr.create(
this,
Native.
mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
2074 checkContextMatch(s, src, dst);
2083 checkContextMatch(s);
2093 checkContextMatch(s, re);
2102 checkContextMatch(re);
2128 checkContextMatch(re);
2137 checkContextMatch(re);
2147 checkContextMatch(re);
2156 checkContextMatch(t);
2165 checkContextMatch(t);
2174 checkContextMatch(t);
2199 checkContextMatch(lo, hi);
2209 checkContextMatch(args);
2218 checkContextMatch(args);
2227 checkContextMatch(args);
2236 checkContextMatch(args);
2245 checkContextMatch(args);
2263 checkContextMatch(ty);
2264 return Expr.create(
this,
2280 checkContextMatch(ty);
2281 return Expr.create(
this,
Native.
mkInt(nCtx(), v, ty.getNativeObject()));
2296 checkContextMatch(ty);
2297 return Expr.create(
this,
2313 throw new Z3Exception(
"Denominator is zero");
2329 .getNativeObject()));
2342 .getNativeObject()));
2355 .getNativeObject()));
2366 .getNativeObject()));
2379 .getNativeObject()));
2392 .getNativeObject()));
2451 int weight,
Pattern[] patterns,
Expr[] noPatterns,
2455 return Quantifier.
of(
this,
true, sorts, names, body, weight, patterns,
2456 noPatterns, quantifierID, skolemID);
2468 return Quantifier.
of(
this,
true, boundConstants, body, weight,
2469 patterns, noPatterns, quantifierID, skolemID);
2477 int weight,
Pattern[] patterns,
Expr[] noPatterns,
2481 return Quantifier.
of(
this,
false, sorts, names, body, weight,
2482 patterns, noPatterns, quantifierID, skolemID);
2494 return Quantifier.
of(
this,
false, boundConstants, body, weight,
2495 patterns, noPatterns, quantifierID, skolemID);
2509 return mkForall(sorts, names, body, weight, patterns, noPatterns,
2510 quantifierID, skolemID);
2512 return mkExists(sorts, names, body, weight, patterns, noPatterns,
2513 quantifierID, skolemID);
2526 return mkForall(boundConstants, body, weight, patterns, noPatterns,
2527 quantifierID, skolemID);
2529 return mkExists(boundConstants, body, weight, patterns, noPatterns,
2530 quantifierID, skolemID);
2552 return Lambda.
of(
this, sorts, names, body);
2563 return Lambda.
of(
this, boundConstants, body);
2605 attributes, assumptions.length,
2606 AST.arrayToNative(assumptions), formula.getNativeObject());
2622 int csn =
Symbol.arrayLength(sortNames);
2623 int cs =
Sort.arrayLength(sorts);
2624 int cdn =
Symbol.arrayLength(declNames);
2625 int cd =
AST.arrayLength(decls);
2626 if (csn != cs || cdn != cd) {
2627 throw new Z3Exception(
"Argument size mismatch");
2630 str,
AST.arrayLength(sorts),
Symbol.arrayToNative(sortNames),
2631 AST.arrayToNative(sorts),
AST.arrayLength(decls),
2632 Symbol.arrayToNative(declNames),
AST.arrayToNative(decls)));
2644 int csn =
Symbol.arrayLength(sortNames);
2645 int cs =
Sort.arrayLength(sorts);
2646 int cdn =
Symbol.arrayLength(declNames);
2647 int cd =
AST.arrayLength(decls);
2648 if (csn != cs || cdn != cd)
2649 throw new Z3Exception(
"Argument size mismatch");
2651 fileName,
AST.arrayLength(sorts),
2652 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2653 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2654 AST.arrayToNative(decls)));
2668 public Goal mkGoal(
boolean models,
boolean unsatCores,
boolean proofs)
2671 return new Goal(
this, models, unsatCores, proofs);
2698 for (
int i = 0; i < n; i++)
2717 return new Tactic(
this, name);
2727 checkContextMatch(t1);
2728 checkContextMatch(t2);
2729 checkContextMatch(ts);
2732 if (ts != null && ts.length > 0)
2734 last = ts[ts.length - 1].getNativeObject();
2735 for (
int i = ts.length - 2; i >= 0; i--) {
2744 t1.getNativeObject(), last));
2747 t1.getNativeObject(), t2.getNativeObject()));
2768 checkContextMatch(t1);
2769 checkContextMatch(t2);
2771 t1.getNativeObject(), t2.getNativeObject()));
2782 checkContextMatch(t);
2784 t.getNativeObject(), ms));
2795 checkContextMatch(t);
2796 checkContextMatch(p);
2798 t.getNativeObject()));
2808 checkContextMatch(p);
2809 checkContextMatch(t1);
2810 checkContextMatch(t2);
2812 t1.getNativeObject(), t2.getNativeObject()));
2821 checkContextMatch(t);
2823 t.getNativeObject(),
max));
2848 checkContextMatch(p);
2868 checkContextMatch(t);
2869 checkContextMatch(p);
2871 t.getNativeObject(), p.getNativeObject()));
2890 checkContextMatch(t);
2901 checkContextMatch(t1);
2902 checkContextMatch(t2);
2904 t1.getNativeObject(), t2.getNativeObject()));
2933 for (
int i = 0; i < n; i++)
2952 return new Probe(
this, name);
2969 checkContextMatch(p1);
2970 checkContextMatch(p2);
2972 p2.getNativeObject()));
2981 checkContextMatch(p1);
2982 checkContextMatch(p2);
2984 p2.getNativeObject()));
2994 checkContextMatch(p1);
2995 checkContextMatch(p2);
2997 p2.getNativeObject()));
3007 checkContextMatch(p1);
3008 checkContextMatch(p2);
3010 p2.getNativeObject()));
3019 checkContextMatch(p1);
3020 checkContextMatch(p2);
3022 p2.getNativeObject()));
3030 checkContextMatch(p1);
3031 checkContextMatch(p2);
3033 p2.getNativeObject()));
3041 checkContextMatch(p1);
3042 checkContextMatch(p2);
3044 p2.getNativeObject()));
3052 checkContextMatch(p);
3082 logic.getNativeObject()));
3112 t.getNativeObject()));
3239 return new FPSort(
this, ebits, sbits);
3496 return new FPExpr(
this,
Native.
mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3508 return new FPExpr(
this,
Native.
mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3520 return new FPExpr(
this,
Native.
mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3532 return new FPExpr(
this,
Native.
mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
3547 return new FPExpr(
this,
Native.
mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
3748 return new FPExpr(
this,
Native.
mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
3915 return AST.create(
this, nativeObject);
3932 return a.getNativeObject();
3972 void checkContextMatch(Z3Object other)
3974 if (
this != other.getContext())
3975 throw new Z3Exception(
"Context mismatch");
3978 void checkContextMatch(Z3Object other1, Z3Object other2)
3980 checkContextMatch(other1);
3981 checkContextMatch(other2);
3984 void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
3986 checkContextMatch(other1);
3987 checkContextMatch(other2);
3988 checkContextMatch(other3);
3991 void checkContextMatch(Z3Object[] arr)
3994 for (Z3Object a : arr)
3995 checkContextMatch(a);
3998 private ASTDecRefQueue m_AST_DRQ =
new ASTDecRefQueue();
3999 private ASTMapDecRefQueue m_ASTMap_DRQ =
new ASTMapDecRefQueue();
4000 private ASTVectorDecRefQueue m_ASTVector_DRQ =
new ASTVectorDecRefQueue();
4001 private ApplyResultDecRefQueue m_ApplyResult_DRQ =
new ApplyResultDecRefQueue();
4002 private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ =
new FuncInterpEntryDecRefQueue();
4003 private FuncInterpDecRefQueue m_FuncInterp_DRQ =
new FuncInterpDecRefQueue();
4004 private GoalDecRefQueue m_Goal_DRQ =
new GoalDecRefQueue();
4005 private ModelDecRefQueue m_Model_DRQ =
new ModelDecRefQueue();
4006 private ParamsDecRefQueue m_Params_DRQ =
new ParamsDecRefQueue();
4007 private ParamDescrsDecRefQueue m_ParamDescrs_DRQ =
new ParamDescrsDecRefQueue();
4008 private ProbeDecRefQueue m_Probe_DRQ =
new ProbeDecRefQueue();
4009 private SolverDecRefQueue m_Solver_DRQ =
new SolverDecRefQueue();
4010 private StatisticsDecRefQueue m_Statistics_DRQ =
new StatisticsDecRefQueue();
4011 private TacticDecRefQueue m_Tactic_DRQ =
new TacticDecRefQueue();
4012 private FixedpointDecRefQueue m_Fixedpoint_DRQ =
new FixedpointDecRefQueue();
4013 private OptimizeDecRefQueue m_Optimize_DRQ =
new OptimizeDecRefQueue();
4014 private ConstructorDecRefQueue m_Constructor_DRQ =
new ConstructorDecRefQueue();
4015 private ConstructorListDecRefQueue m_ConstructorList_DRQ =
4016 new ConstructorListDecRefQueue();
4019 return m_Constructor_DRQ;
4023 return m_ConstructorList_DRQ;
4033 return m_ASTMap_DRQ;
4038 return m_ASTVector_DRQ;
4043 return m_ApplyResult_DRQ;
4048 return m_FuncEntry_DRQ;
4053 return m_FuncInterp_DRQ;
4068 return m_Params_DRQ;
4073 return m_ParamDescrs_DRQ;
4083 return m_Solver_DRQ;
4088 return m_Statistics_DRQ;
4093 return m_Tactic_DRQ;
4098 return m_Fixedpoint_DRQ;
4103 return m_Optimize_DRQ;
4112 m_AST_DRQ.forceClear(
this);
4113 m_ASTMap_DRQ.forceClear(
this);
4114 m_ASTVector_DRQ.forceClear(
this);
4115 m_ApplyResult_DRQ.forceClear(
this);
4116 m_FuncEntry_DRQ.forceClear(
this);
4117 m_FuncInterp_DRQ.forceClear(
this);
4118 m_Goal_DRQ.forceClear(
this);
4119 m_Model_DRQ.forceClear(
this);
4120 m_Params_DRQ.forceClear(
this);
4121 m_Probe_DRQ.forceClear(
this);
4122 m_Solver_DRQ.forceClear(
this);
4123 m_Optimize_DRQ.forceClear(
this);
4124 m_Statistics_DRQ.forceClear(
this);
4125 m_Tactic_DRQ.forceClear(
this);
4126 m_Fixedpoint_DRQ.forceClear(
this);
4131 m_stringSort = null;
4133 synchronized (creation_lock) {
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)
BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
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)
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)
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)
Expr mkSelect(ArrayExpr a, Expr[] args)
static void delConfig(long a0)
ArrayExpr mkConstArray(Sort domain, Expr v)
Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
static long mkBvredor(long a0, long a1)
RealExpr mkFPToReal(FPExpr t)
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 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 range(expr const &lo, expr const &hi)
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)
ReExpr mkLoop(ReExpr re, int lo)
SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
static long mkReEmpty(long a0, long a1)
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)
String getProbeDescription(String name)
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkAnd(BoolExpr...t)
SeqExpr mkUnit(Expr elem)
Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
ArrayExpr mkSetUnion(ArrayExpr...args)
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()
BoolExpr mkInRe(SeqExpr s, ReExpr re)
SeqExpr intToString(Expr e)
FPNum mkFP(float v, FPSort s)
static long mkFpaIsPositive(long a0, long a1)
static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
static long mkFpaSort16(long a0)
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
SeqExpr mkConcat(SeqExpr...t)
static long mkReStar(long a0, long a1)
static long mkFpaSqrt(long a0, long a1, long a2)
static long mkBvlshr(long a0, long a1, long a2)
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 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 mkStrToInt(long a0, long a1)
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)
IDecRefQueue< Statistics > getStatisticsDRQ()
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
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)
BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
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 long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
static long mkReConcat(long a0, int a1, long[] a2)
FuncDecl mkConstDecl(String name, Sort range)
static long probeOr(long a0, long a1, long a2)
SetSort mkSetSort(Sort ty)
ReExpr mkIntersect(ReExpr...t)
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()
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 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 mkReIntersect(long a0, int a1, long[] a2)
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)
BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
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 mkAtmost(long a0, int a1, long[] a2, int a3)
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)
Expr mkUpdateField(FuncDecl field, Expr t, Expr v)
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)
ReExpr mkComplement(ReExpr re)
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)
BoolExpr[] ToBoolExprArray()
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)
IDecRefQueue< Model > getModelDRQ()
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
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[] parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
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)
SeqExpr mkAt(SeqExpr s, IntExpr index)
static long mkReFull(long a0, long a1)
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)
ArrayExpr mkMap(FuncDecl f, ArrayExpr...args)
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
static long mkSimpleSolver(long a0)
static long mkPbge(long a0, int a1, long[] a2, int[] a3, int a4)
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)
Lambda mkLambda(Expr[] boundConstants, Expr body)
FPNum mkFPZero(FPSort s, boolean negative)
BoolExpr mkAtLeast(BoolExpr[] args, int k)
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 mkStoreN(long a0, long a1, int a2, long[] a3, long a4)
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 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)
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)
BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
static long mkFpaIsNan(long a0, long a1)
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
IntExpr mkIntConst(String name)
static long mkIntToStr(long a0, long a1)
static long mkFpaSortSingle(long a0)
static long mkEq(long a0, long a1, long a2)
static long mkRem(long a0, long a1, long a2)
static long mkExtRotateRight(long a0, long a1, long a2)
static long mkFpaMul(long a0, long a1, long a2, long a3)
ReExpr mkRange(SeqExpr lo, SeqExpr hi)
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
static long mkAtleast(long a0, int a1, long[] a2, int a3)
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
IDecRefQueue< ASTVector > getASTVectorDRQ()
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
IntExpr mkLength(SeqExpr s)
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)
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)
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)
SeqExpr mkString(String s)
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)
Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body)
static long mkLt(long a0, long a1, long a2)
static long mkReLoop(long a0, long a1, int a2, int a3)
static long mkContextRc(long a0)
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
BoolExpr mkOr(BoolExpr...t)
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 mkPbeq(long a0, int a1, long[] a2, int[] a3, int a4)
ArraySort mkArraySort(Sort[] domains, Sort range)
ReExpr mkConcat(ReExpr...t)
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 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)
static long mkBvashr(long a0, long a1, long a2)
static long mkReRange(long a0, long a1, long a2)
static long mkGt(long a0, long a1, long a2)
ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
static long mkFullSet(long a0, long a1)
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
ReExpr mkLoop(ReExpr re, int lo, int hi)
static long mkPble(long a0, int a1, long[] a2, int[] a3, int a4)
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)
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)
ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
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)
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)
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)
IntExpr stringToInt(Expr e)
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)
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)
SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
BitVecSort mkBitVecSort(int size)
static long mkFpaLt(long a0, long a1, long a2)
ParamDescrs getSimplifyParameterDescriptions()
IDecRefQueue< Params > getParamsDRQ()
SeqExpr mkEmptySeq(Sort s)
Fixedpoint mkFixedpoint()
BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
static long mkBvxnor(long a0, long a1, long a2)
static long mkSeqPrefix(long a0, long a1, long a2)
static long mkSelectN(long a0, long a1, int a2, long[] a3)
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)
IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
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)
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)
expr max(expr const &a, expr const &b)
BoolExpr mkNot(BoolExpr a)
BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
Expr mkNumeral(long v, Sort ty)
DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
FPRMSort mkFPRoundingModeSort()
ReExpr mkOption(ReExpr re)
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)
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[] parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
IDecRefQueue< FuncInterp > getFuncInterpDRQ()
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 mkReComplement(long a0, long a1)
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)
IDecRefQueue< Goal > getGoalDRQ()
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
BoolExpr mkAtMost(BoolExpr[] args, int k)
ReExpr mkUnion(ReExpr...t)
Tactic andThen(Tactic t1, Tactic t2, Tactic...ts)
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)