18package com.microsoft.z3;
20import static com.microsoft.z3.Constructor.of;
22import com.microsoft.z3.enumerations.Z3_ast_print_mode;
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);
233 checkContextMatch(domains);
234 checkContextMatch(
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);
456 checkContextMatch(name);
457 checkContextMatch(domain);
458 checkContextMatch(
range);
469 checkContextMatch(domain);
470 checkContextMatch(
range);
480 checkContextMatch(domain);
481 checkContextMatch(
range);
495 checkContextMatch(domain);
496 checkContextMatch(
range);
505 checkContextMatch(name);
506 checkContextMatch(
range);
515 checkContextMatch(
range);
528 checkContextMatch(
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,
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) {
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)
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();
3974 void checkContextMatch(Z3Object other)
3976 if (
this != other.getContext())
3977 throw new Z3Exception(
"Context mismatch");
3980 void checkContextMatch(Z3Object other1, Z3Object other2)
3982 checkContextMatch(other1);
3983 checkContextMatch(other2);
3986 void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
3988 checkContextMatch(other1);
3989 checkContextMatch(other2);
3990 checkContextMatch(other3);
3993 void checkContextMatch(Z3Object[] arr)
3996 for (Z3Object a : arr)
3997 checkContextMatch(a);
4000 private ASTDecRefQueue m_AST_DRQ =
new ASTDecRefQueue();
4001 private ASTMapDecRefQueue m_ASTMap_DRQ =
new ASTMapDecRefQueue();
4002 private ASTVectorDecRefQueue m_ASTVector_DRQ =
new ASTVectorDecRefQueue();
4003 private ApplyResultDecRefQueue m_ApplyResult_DRQ =
new ApplyResultDecRefQueue();
4004 private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ =
new FuncInterpEntryDecRefQueue();
4005 private FuncInterpDecRefQueue m_FuncInterp_DRQ =
new FuncInterpDecRefQueue();
4006 private GoalDecRefQueue m_Goal_DRQ =
new GoalDecRefQueue();
4007 private ModelDecRefQueue m_Model_DRQ =
new ModelDecRefQueue();
4008 private ParamsDecRefQueue m_Params_DRQ =
new ParamsDecRefQueue();
4009 private ParamDescrsDecRefQueue m_ParamDescrs_DRQ =
new ParamDescrsDecRefQueue();
4010 private ProbeDecRefQueue m_Probe_DRQ =
new ProbeDecRefQueue();
4011 private SolverDecRefQueue m_Solver_DRQ =
new SolverDecRefQueue();
4012 private StatisticsDecRefQueue m_Statistics_DRQ =
new StatisticsDecRefQueue();
4013 private TacticDecRefQueue m_Tactic_DRQ =
new TacticDecRefQueue();
4014 private FixedpointDecRefQueue m_Fixedpoint_DRQ =
new FixedpointDecRefQueue();
4015 private OptimizeDecRefQueue m_Optimize_DRQ =
new OptimizeDecRefQueue();
4016 private ConstructorDecRefQueue m_Constructor_DRQ =
new ConstructorDecRefQueue();
4017 private ConstructorListDecRefQueue m_ConstructorList_DRQ =
4018 new ConstructorListDecRefQueue();
4021 return m_Constructor_DRQ;
4025 return m_ConstructorList_DRQ;
4035 return m_ASTMap_DRQ;
4040 return m_ASTVector_DRQ;
4045 return m_ApplyResult_DRQ;
4050 return m_FuncEntry_DRQ;
4055 return m_FuncInterp_DRQ;
4070 return m_Params_DRQ;
4075 return m_ParamDescrs_DRQ;
4085 return m_Solver_DRQ;
4090 return m_Statistics_DRQ;
4095 return m_Tactic_DRQ;
4100 return m_Fixedpoint_DRQ;
4105 return m_Optimize_DRQ;
4114 m_AST_DRQ.forceClear(
this);
4115 m_ASTMap_DRQ.forceClear(
this);
4116 m_ASTVector_DRQ.forceClear(
this);
4117 m_ApplyResult_DRQ.forceClear(
this);
4118 m_FuncEntry_DRQ.forceClear(
this);
4119 m_FuncInterp_DRQ.forceClear(
this);
4120 m_Goal_DRQ.forceClear(
this);
4121 m_Model_DRQ.forceClear(
this);
4122 m_Params_DRQ.forceClear(
this);
4123 m_Probe_DRQ.forceClear(
this);
4124 m_Solver_DRQ.forceClear(
this);
4125 m_Optimize_DRQ.forceClear(
this);
4126 m_Statistics_DRQ.forceClear(
this);
4127 m_Tactic_DRQ.forceClear(
this);
4128 m_Fixedpoint_DRQ.forceClear(
this);
4133 m_stringSort =
null;
4135 synchronized (creation_lock) {
BoolExpr[] ToBoolExprArray()
BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
Expr mkConst(String name, Sort range)
Probe ge(Probe p1, Probe p2)
FuncDecl mkConstDecl(String name, Sort range)
RealExpr mkInt2Real(IntExpr t)
BoolExpr mkEq(Expr x, Expr y)
Solver mkSolver(String logic)
BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
Tactic repeat(Tactic t, int max)
Pattern mkPattern(Expr... terms)
ArraySort mkArraySort(Sort[] domains, Sort range)
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
String getProbeDescription(String name)
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
BoolExpr mkBVNegNoOverflow(BitVecExpr t)
FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t)
BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
FPRMExpr mkFPRoundNearestTiesToEven()
Expr mkTermArray(ArrayExpr array)
BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
Fixedpoint mkFixedpoint()
Tactic usingParams(Tactic t, Params p)
Tactic parOr(Tactic... t)
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
FiniteDomainSort mkFiniteDomainSort(String name, long size)
FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
Tactic then(Tactic t1, Tactic t2, Tactic... ts)
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
BoolExpr mkFPIsSubnormal(FPExpr t)
FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
FPSort mkFPSort(int ebits, int sbits)
Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
ArrayExpr mkSetIntersection(ArrayExpr... args)
Probe le(Probe p1, Probe p2)
SetSort mkSetSort(Sort ty)
Expr mkSelect(ArrayExpr a, Expr[] args)
RealExpr mkFPToReal(FPExpr t)
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkZeroExt(int i, BitVecExpr t)
AST wrapAST(long nativeObject)
UninterpretedSort mkUninterpretedSort(Symbol s)
SeqExpr mkString(String s)
IDecRefQueue< FuncInterp > getFuncInterpDRQ()
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
ArithExpr mkMul(ArithExpr... t)
ArithExpr mkSub(ArithExpr... t)
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
FPNum mkFP(double v, FPSort s)
SeqExpr mkEmptySeq(Sort s)
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
SeqExpr mkUnit(Expr elem)
BoolExpr mkFPIsZero(FPExpr t)
FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
BoolExpr mkNot(BoolExpr a)
FPNum mkFPInf(FPSort s, boolean negative)
ArithExpr mkUnaryMinus(ArithExpr t)
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
Expr mkNumeral(int v, Sort ty)
Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkBVConst(Symbol name, int size)
FPRMNum mkFPRoundTowardZero()
ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
Probe or(Probe p1, Probe p2)
IDecRefQueue< ASTMap > getASTMapDRQ()
Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Tactic cond(Probe p, Tactic t1, Tactic t2)
IDecRefQueue< Statistics > getStatisticsDRQ()
IDecRefQueue< Model > getModelDRQ()
BitVecExpr mkBVConst(String name, int size)
SeqExpr mkConcat(SeqExpr... t)
IDecRefQueue< Optimize > getOptimizeDRQ()
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body)
IDecRefQueue< AST > getASTDRQ()
EnumSort mkEnumSort(String name, String... enumNames)
FPNum mkFPNumeral(int v, FPSort s)
ReExpr mkComplement(ReExpr re)
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
FuncDecl mkFreshConstDecl(String prefix, Sort range)
IntExpr mkReal2Int(RealExpr t)
IDecRefQueue< ApplyResult > getApplyResultDRQ()
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
void updateParamValue(String id, String value)
IntExpr stringToInt(Expr e)
ReExpr mkLoop(ReExpr re, int lo, int hi)
BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
ArraySort mkArraySort(Sort domain, Sort range)
BitVecNum mkBV(long v, int size)
FPNum mkFPNumeral(float v, FPSort s)
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
Tactic when(Probe p, Tactic t)
ArrayExpr mkSetDel(ArrayExpr set, Expr element)
BitVecExpr mkRepeat(int i, BitVecExpr t)
BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
IDecRefQueue< Goal > getGoalDRQ()
Probe mkProbe(String name)
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
RealExpr mkRealConst(String name)
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
Tactic failIfNotDecided()
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
ParamDescrs getSimplifyParameterDescriptions()
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
Probe gt(Probe p1, Probe p2)
SeqExpr intToString(Expr e)
Expr mkNumeral(String v, Sort ty)
ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
Tactic with(Tactic t, Params p)
ReExpr mkRange(SeqExpr lo, SeqExpr hi)
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
BoolExpr mkFPIsNormal(FPExpr t)
FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
String[] getTacticNames()
Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
ReExpr mkLoop(ReExpr re, int lo)
SeqExpr mkAt(SeqExpr s, IntExpr index)
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
FPRMNum mkFPRoundNearestTiesToAway()
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkBool(boolean value)
BoolExpr mkAnd(BoolExpr... t)
IntExpr mkMod(IntExpr t1, IntExpr t2)
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
FPExpr mkFPMin(FPExpr t1, FPExpr t2)
BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkFPIsInfinite(FPExpr t)
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
ReExpr mkOption(ReExpr re)
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
FPRMNum mkFPRoundTowardNegative()
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
IDecRefQueue< Params > getParamsDRQ()
Probe eq(Probe p1, Probe p2)
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
ArrayExpr mkSetUnion(ArrayExpr... args)
IDecRefQueue< Solver > getSolverDRQ()
BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
BoolExpr mkAtMost(BoolExpr[] args, int k)
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
IntExpr mkIntConst(String name)
Solver mkSolver(Tactic t)
Expr mkUpdateField(FuncDecl field, Expr t, Expr v)
BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
Expr mkBound(int index, Sort ty)
IDecRefQueue< Constructor > getConstructorDRQ()
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
ArrayExpr mkFullSet(Sort domain)
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
IntExpr mkIntConst(Symbol name)
Expr mkNumeral(long v, Sort ty)
BoolExpr mkFPIsNaN(FPExpr t)
Tactic mkTactic(String name)
BitVecExpr mkBVNot(BitVecExpr t)
FPNum mkFPNumeral(double v, FPSort s)
Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
FuncDecl mkConstDecl(Symbol name, Sort range)
BoolExpr mkIsInteger(RealExpr t)
FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
BitVecExpr mkInt2BV(int n, IntExpr t)
Tactic parAndThen(Tactic t1, Tactic t2)
BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
BitVecNum mkBV(int v, int size)
Context(Map< String, String > settings)
FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
FPRMSort mkFPRoundingModeSort()
RealExpr mkRealConst(Symbol name)
String getTacticDescription(String name)
IDecRefQueue< Probe > getProbeDRQ()
Solver mkSolver(Symbol logic)
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
RatNum mkReal(int num, int den)
BitVecSort mkBitVecSort(int size)
BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
SeqSort mkSeqSort(Sort s)
IntExpr mkLength(SeqExpr s)
ArrayExpr mkSetComplement(ArrayExpr arg)
Probe constProbe(double val)
BoolExpr mkAtLeast(BoolExpr[] args, int k)
BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
BoolExpr mkBoolConst(String name)
BoolExpr mkDistinct(Expr... args)
ArrayExpr mkEmptySet(Sort domain)
BoolExpr mkFPIsPositive(FPExpr t)
BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkExtract(int high, int low, BitVecExpr t)
BitVecExpr mkBVNeg(BitVecExpr t)
IDecRefQueue< Tactic > getTacticDRQ()
BoolExpr mkOr(BoolExpr... t)
FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
Lambda mkLambda(Expr[] boundConstants, Expr body)
FPSort mkFPSortQuadruple()
FPRMNum mkFPRoundTowardPositive()
FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
ListSort mkListSort(Symbol name, Sort elemSort)
BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
BitVecExpr mkSignExt(int i, BitVecExpr t)
ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
BoolExpr mkFPIsNegative(FPExpr t)
ListSort mkListSort(String name, Sort elemSort)
BitVecExpr mkBVRedAND(BitVecExpr t)
Probe and(Probe p1, Probe p2)
BitVecExpr mkFPToIEEEBV(FPExpr t)
Tactic tryFor(Tactic t, int ms)
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
UninterpretedSort mkUninterpretedSort(String str)
void setPrintMode(Z3_ast_print_mode value)
Expr mkSelect(ArrayExpr a, Expr i)
BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
ArithExpr mkAdd(ArithExpr... t)
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
BitVecNum mkBV(String v, int size)
Probe lt(Probe p1, Probe p2)
BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
BitVecExpr mkBVRedOR(BitVecExpr t)
ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
ReExpr mkIntersect(ReExpr... t)
BoolExpr mkInRe(SeqExpr s, ReExpr re)
IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
FPNum mkFP(float v, FPSort s)
Expr mkConst(Symbol name, Sort range)
FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
IntExpr mkRem(IntExpr t1, IntExpr t2)
ReExpr mkConcat(ReExpr... t)
FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
ReExpr mkUnion(ReExpr... t)
Tactic orElse(Tactic t1, Tactic t2)
ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
FPNum mkFP(int v, FPSort s)
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
ArrayExpr mkConstArray(Sort domain, Expr v)
IDecRefQueue< ConstructorList > getConstructorListDRQ()
Expr mkApp(FuncDecl f, Expr... args)
Expr mkFreshConst(String prefix, Sort range)
IntSymbol mkSymbol(int i)
StringSymbol mkSymbol(String name)
BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
FPNum mkFPZero(FPSort s, boolean negative)
BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
BoolExpr mkBoolConst(Symbol name)
BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
IDecRefQueue< ASTVector > getASTVectorDRQ()
ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
static long mkSetAdd(long a0, long a1, long a2)
static long mkBvsmod(long a0, long a1, long a2)
static long mkSimpleSolver(long a0)
static long tacticParOr(long a0, int a1, long[] a2)
static long mkXor(long a0, long a1, long a2)
static long mkSeqSuffix(long a0, long a1, long a2)
static long mkStringSort(long a0)
static long mkFpaSortQuadruple(long a0)
static long mkInt64(long a0, long a1, long a2)
static long mkSelect(long a0, long a1, long a2)
static long mkFpaNeg(long a0, long a1)
static long mkBvsub(long a0, long a1, long a2)
static long mkBvredor(long a0, long a1)
static long mkExtRotateLeft(long a0, long a1, long a2)
static native void setInternalErrorHandler(long ctx)
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
static long mkFpaSqrt(long a0, long a1, long a2)
static long mkFpaToReal(long a0, long a1)
static long mkFalse(long a0)
static long tacticUsingParams(long a0, long a1, long a2)
static long tacticRepeat(long a0, long a1, int a2)
static long mkFpaRoundNearestTiesToEven(long a0)
static void delContext(long a0)
static long mkFpaFma(long a0, long a1, long a2, long a3, long a4)
static long mkSetComplement(long a0, long a1)
static long mkFpaSortHalf(long a0)
static long mkFpaIsSubnormal(long a0, long a1)
static long mkStrToInt(long a0, long a1)
static long mkAdd(long a0, int a1, long[] a2)
static long mkFpaRem(long a0, long a1, long a2)
static long mkBvSort(long a0, int a1)
static long mkFpaNumeralFloat(long a0, float a1, long a2)
static long mkBvult(long a0, long a1, long a2)
static long mkFpaIsNormal(long a0, long a1)
static long mkBvnegNoOverflow(long a0, long a1)
static long probeAnd(long a0, long a1, long a2)
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
static long mkBvsle(long a0, long a1, long a2)
static long mkFpaMin(long a0, long a1, long a2)
static String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
static long mkGt(long a0, long a1, long a2)
static long mkFpaNumeralDouble(long a0, double a1, long a2)
static long mkGe(long a0, long a1, long a2)
static void updateParamValue(long a0, String a1, String a2)
static long tacticFailIf(long a0, long a1)
static long mkFpaMul(long a0, long a1, long a2, long a3)
static long mkFpaSort64(long a0)
static String getTacticName(long a0, int a1)
static long mkRotateRight(long a0, int a1, long a2)
static long mkReStar(long a0, long a1)
static long mkConstArray(long a0, long a1, long a2)
static long mkSeqAt(long a0, long a1, long a2)
static long probeNot(long a0, long a1)
static long mkDistinct(long a0, int a1, long[] a2)
static long mkInt2bv(long a0, int a1, long a2)
static long mkFpaToIeeeBv(long a0, long a1)
static long mkFpaRna(long a0)
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
static long mkFullSet(long a0, long a1)
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
static long mkSelectN(long a0, long a1, int a2, long[] a3)
static long mkSolverForLogic(long a0, long a1)
static long probeGt(long a0, long a1, long a2)
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static long mkDiv(long a0, long a1, long a2)
static long mkBvnot(long a0, long a1)
static long mkFpaNumeralInt(long a0, int a1, long a2)
static long mkSetDifference(long a0, long a1, long a2)
static long datatypeUpdateField(long a0, long a1, long a2, long a3)
static long mkFpaRoundNearestTiesToAway(long a0)
static long mkReConcat(long a0, int a1, long[] a2)
static long mkSeqToRe(long a0, long a1)
static long probeOr(long a0, long a1, long a2)
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
static long mkBvsgt(long a0, long a1, long a2)
static long mkFpaNan(long a0, long a1)
static long mkBv2int(long a0, long a1, boolean a2)
static long probeGe(long a0, long a1, long a2)
static long mkIntToStr(long a0, long a1)
static long mkReSort(long a0, long a1)
static String getProbeName(long a0, int a1)
static long tacticOrElse(long a0, long a1, long a2)
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
static long mkIte(long a0, long a1, long a2, long a3)
static long probeLe(long a0, long a1, long a2)
static long mkString(long a0, String a1)
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
static long mkFpaSort16(long a0)
static long mkBvule(long a0, long a1, long a2)
static long mkFpaRtz(long a0)
static long mkSetDel(long a0, long a1, long a2)
static long mkSolver(long a0)
static long mkIsInt(long a0, long a1)
static long mkPble(long a0, int a1, long[] a2, int[] a3, int a4)
static long mkFpaSort128(long a0)
static long mkSignExt(long a0, int a1, long a2)
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
static long mkExtRotateRight(long a0, long a1, long a2)
static long mkBvashr(long a0, long a1, long a2)
static long mkFpaInf(long a0, long a1, boolean a2)
static long mkTrue(long a0)
static long mkRotateLeft(long a0, int a1, long a2)
static long mkArrayExt(long a0, long a1, long a2)
static void setAstPrintMode(long a0, int a1)
static long mkAtmost(long a0, int a1, long[] a2, int a3)
static long mkBvshl(long a0, long a1, long a2)
static long mkReRange(long a0, long a1, long a2)
static long mkFpaFp(long a0, long a1, long a2, long a3)
static long mkPbeq(long a0, int a1, long[] a2, int[] a3, int a4)
static long mkSeqReplace(long a0, long a1, long a2, long a3)
static long mkBvsdiv(long a0, long a1, long a2)
static long mkBvmul(long a0, long a1, long a2)
static long mkFpaToFpBv(long a0, long a1, long a2)
static long mkFpaZero(long a0, long a1, boolean a2)
static long mkSeqUnit(long a0, long a1)
static long tacticCond(long a0, long a1, long a2, long a3)
static long mkImplies(long a0, long a1, long a2)
static long mkReal2int(long a0, long a1)
static long mkArrayDefault(long a0, long a1)
static long mkZeroExt(long a0, int a1, long a2)
static long mkBound(long a0, int a1, long a2)
static long mkNot(long a0, long a1)
static long mkFpaSortDouble(long a0)
static long mkBvugt(long a0, long a1, long a2)
static long mkReOption(long a0, long a1)
static long mkBvxnor(long a0, long a1, long a2)
static long mkFpaSortSingle(long a0)
static long mkReComplement(long a0, long a1)
static long mkStore(long a0, long a1, long a2, long a3)
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
static long mkSub(long a0, int a1, long[] a2)
static long mkBvsubNoOverflow(long a0, long a1, long a2)
static long mkBvand(long a0, long a1, long a2)
static long mkFpaGt(long a0, long a1, long a2)
static long mkReFull(long a0, long a1)
static long mkStoreN(long a0, long a1, int a2, long[] a3, long a4)
static long probeEq(long a0, long a1, long a2)
static long mkBvudiv(long a0, long a1, long a2)
static long tacticParAndThen(long a0, long a1, long a2)
static long mkSeqConcat(long a0, int a1, long[] a2)
static long mkEmptySet(long a0, long a1)
static long mkAtleast(long a0, int a1, long[] a2, int a3)
static long mkMul(long a0, int a1, long[] a2)
static long mkLt(long a0, long a1, long a2)
static long mkFreshConst(long a0, String a1, long a2)
static long mkBvsrem(long a0, long a1, long a2)
static long mkSetMember(long a0, long a1, long a2)
static long mkSeqEmpty(long a0, long a1)
static long mkSolverFromTactic(long a0, long a1)
static long mkFpaAbs(long a0, long a1)
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
static long mkConst(long a0, long a1, long a2)
static long tacticSkip(long a0)
static void interrupt(long a0)
static long mkOr(long a0, int a1, long[] a2)
static long mkBvadd(long a0, long a1, long a2)
static long mkFpaIsNan(long a0, long a1)
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
static long mkNumeral(long a0, String a1, long a2)
static long mkBvnor(long a0, long a1, long a2)
static long mkFpaLeq(long a0, long a1, long a2)
static int getNumTactics(long a0)
static long mkLe(long a0, long a1, long a2)
static long tacticFail(long a0)
static long mkBvsge(long a0, long a1, long a2)
static long mkBvxor(long a0, long a1, long a2)
static long tacticTryFor(long a0, long a1, int a2)
static void setParamValue(long a0, String a1, String a2)
static long mkMod(long a0, long a1, long a2)
static long mkReEmpty(long a0, long a1)
static long mkFpaSort32(long a0)
static int getNumProbes(long a0)
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
static long mkInt(long a0, int a1, long a2)
static long mkConcat(long a0, long a1, long a2)
static long mkReLoop(long a0, long a1, int a2, int a3)
static long mkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static long mkSetSubset(long a0, long a1, long a2)
static long mkUnaryMinus(long a0, long a1)
static long mkBvuge(long a0, long a1, long a2)
static long mkFpaRoundTowardZero(long a0)
static long mkInt2real(long a0, long a1)
static long mkFpaLt(long a0, long a1, long a2)
static long mkSeqContains(long a0, long a1, long a2)
static long mkFpaIsPositive(long a0, long a1)
static long mkContextRc(long a0)
static long mkFpaAdd(long a0, long a1, long a2, long a3)
static long mkPattern(long a0, int a1, long[] a2)
static long simplifyGetParamDescrs(long a0)
static long tacticFailIfNotDecided(long a0)
static long mkReIntersect(long a0, int a1, long[] a2)
static long mkBvor(long a0, long a1, long a2)
static long mkAnd(long a0, int a1, long[] a2)
static long mkSeqPrefix(long a0, long a1, long a2)
static long mkBvslt(long a0, long a1, long a2)
static long mkFpaGeq(long a0, long a1, long a2)
static long mkBvnand(long a0, long a1, long a2)
static String simplifyGetHelp(long a0)
static long mkSeqInRe(long a0, long a1, long a2)
static long mkIff(long a0, long a1, long a2)
static long mkFpaRne(long a0)
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
static long mkFpaIsNegative(long a0, long a1)
static long mkFpaRtp(long a0)
static long mkRepeat(long a0, int a1, long a2)
static long mkEq(long a0, long a1, long a2)
static long mkSeqExtract(long a0, long a1, long a2, long a3)
static long mkPbge(long a0, int a1, long[] a2, int[] a3, int a4)
static long mkFpaSub(long a0, long a1, long a2, long a3)
static long mkFpaRoundTowardPositive(long a0)
static long mkReUnion(long a0, int a1, long[] a2)
static long mkBvredand(long a0, long a1)
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
static long mkFpaIsInfinite(long a0, long a1)
static String tacticGetDescr(long a0, String a1)
static long mkRem(long a0, long a1, long a2)
static long mkSetUnion(long a0, int a1, long[] a2)
static long probeLt(long a0, long a1, long a2)
static void delConfig(long a0)
static long mkBvneg(long a0, long a1)
static long mkBvurem(long a0, long a1, long a2)
static long mkPower(long a0, long a1, long a2)
static long mkFpaRoundTowardNegative(long a0)
static long mkSeqIndex(long a0, long a1, long a2, long a3)
static String probeGetDescr(long a0, String a1)
static long mkSetIntersect(long a0, int a1, long[] a2)
static long tacticWhen(long a0, long a1, long a2)
static long mkReal(long a0, int a1, int a2)
static long mkFpaRtn(long a0)
static long mkSeqLength(long a0, long a1)
static long probeConst(long a0, double a1)
static long mkFpaDiv(long a0, long a1, long a2, long a3)
static long mkBvlshr(long a0, long a1, long a2)
static long mkExtract(long a0, int a1, int a2, long a3)
static long mkFpaMax(long a0, long a1, long a2)
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
static long mkFpaEq(long a0, long a1, long a2)
static long mkMap(long a0, long a1, int a2, long[] a3)
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
static long mkRePlus(long a0, long a1)
static long mkSeqSort(long a0, long a1)
static long tacticAndThen(long a0, long a1, long a2)
static long mkFpaIsZero(long a0, long a1)
static Quantifier of(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Z3_PRINT_SMTLIB2_COMPLIANT
expr range(expr const &lo, expr const &hi)
expr max(expr const &a, expr const &b)
def EnumSort(name, values, ctx=None)
def String(name, ctx=None)
def FiniteDomainSort(name, sz, ctx=None)
def FPSort(ebits, sbits, ctx=None)
def TupleSort(name, sorts, ctx=None)
def BitVecSort(sz, ctx=None)