Go to the documentation of this file.
18 package com.microsoft.z3;
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");
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);
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);
792 checkContextMatch(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);
1733 checkContextMatch(a);
1734 checkContextMatch(i);
1735 checkContextMatch(v);
1737 i.getNativeObject(), v.getNativeObject()));
1758 checkContextMatch(a);
1759 checkContextMatch(args);
1760 checkContextMatch(v);
1776 checkContextMatch(domain);
1777 checkContextMatch(v);
1779 domain.getNativeObject(), v.getNativeObject()));
1797 checkContextMatch(f);
1798 checkContextMatch(args);
1812 checkContextMatch(array);
1813 return Expr.create(
this,
1822 checkContextMatch(arg1);
1823 checkContextMatch(arg2);
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);
1897 checkContextMatch(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);
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);
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,
2626 if (csn != cs || cdn != cd) {
2648 if (csn != cs || cdn != cd)
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())
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) {
FPNum mkFP(double v, FPSort s)
static long datatypeUpdateField(long a0, long a1, long a2, long a3)
static long mkFpaSub(long a0, long a1, long a2, long a3)
static long mkFpaRoundTowardNegative(long a0)
static long mkDiv(long a0, long a1, long a2)
static long mkFpaSortQuadruple(long a0)
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
static long mkBvsle(long a0, long a1, long a2)
Probe gt(Probe p1, Probe p2)
BoolExpr mkBoolConst(String name)
static long mkSetMember(long a0, long a1, long a2)
static long tacticTryFor(long a0, long a1, int a2)
static long mkFpaIsSubnormal(long a0, long a1)
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ()
SeqSort mkSeqSort(Sort s)
static long mkBvSort(long a0, int a1)
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
void updateParamValue(String id, String value)
BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
static long mkFpaSort32(long a0)
BitVecExpr mkBVNot(BitVecExpr t)
BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
IDecRefQueue< Optimize > getOptimizeDRQ()
static long mkSub(long a0, int a1, long[] a2)
static long mkStoreN(long a0, long a1, int a2, long[] a3, long a4)
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
Tactic with(Tactic t, Params p)
BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed)
static long mkSetAdd(long a0, long a1, long a2)
static long mkBvshl(long a0, long a1, long a2)
FiniteDomainSort mkFiniteDomainSort(Symbol name, long size)
static long mkFpaDiv(long a0, long a1, long a2, long a3)
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
Expr mkFreshConst(String prefix, Sort range)
static long mkReEmpty(long a0, long a1)
def TupleSort(name, sorts, ctx=None)
BitVecExpr mkInt2BV(int n, IntExpr t)
ArrayExpr mkSetUnion(ArrayExpr... args)
static long mkSeqExtract(long a0, long a1, long a2, long a3)
static long mkDistinct(long a0, int a1, long[] a2)
static void interrupt(long a0)
IntExpr mkIntConst(String name)
static long mkRepeat(long a0, int a1, long a2)
ArrayExpr mkFullSet(Sort domain)
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
static long tacticFailIfNotDecided(long a0)
IDecRefQueue< Solver > getSolverDRQ()
FPExpr mkFPMax(FPExpr t1, FPExpr t2)
static long mkSolverForLogic(long a0, long a1)
static long mkFpaMax(long a0, long a1, long a2)
static long mkFpaSqrt(long a0, long a1, long a2)
static long mkReOption(long a0, long a1)
static long mkBvor(long a0, long a1, long a2)
ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
Expr mkConst(String name, Sort range)
static long mkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
Expr mkTermArray(ArrayExpr array)
FPNum mkFPZero(FPSort s, boolean negative)
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
IDecRefQueue< ASTVector > getASTVectorDRQ()
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
static long mkBvxnor(long a0, long a1, long a2)
static long mkSeqConcat(long a0, int a1, long[] a2)
static long mkOr(long a0, int a1, long[] a2)
Probe or(Probe p1, Probe p2)
BitVecExpr mkRepeat(int i, BitVecExpr t)
IntExpr mkRem(IntExpr t1, IntExpr t2)
static long mkBvsdiv(long a0, long a1, long a2)
static long mkReConcat(long a0, int a1, long[] a2)
static long mkIte(long a0, long a1, long a2, long a3)
static long mkZeroExt(long a0, int a1, long a2)
IDecRefQueue< ApplyResult > getApplyResultDRQ()
BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
static long mkSetSubset(long a0, long a1, long a2)
Tactic repeat(Tactic t, int max)
static long mkFpaNumeralDouble(long a0, double a1, long a2)
static long mkRotateLeft(long a0, int a1, long a2)
expr range(expr const &lo, expr const &hi)
FPNum mkFPNumeral(float v, FPSort s)
BitVecExpr mkBVConst(Symbol name, int size)
Expr mkApp(FuncDecl f, Expr... args)
Probe ge(Probe p1, Probe p2)
static long mkFpaRoundNearestTiesToAway(long a0)
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
ReExpr mkLoop(ReExpr re, int lo, int hi)
Tactic mkTactic(String name)
BoolExpr mkAnd(BoolExpr... t)
static long mkLt(long a0, long a1, long a2)
BoolExpr mkOr(BoolExpr... t)
Lambda mkLambda(Sort[] sorts, Symbol[] names, Expr body)
FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
static long probeConst(long a0, double a1)
IntSymbol mkSymbol(int i)
Fixedpoint mkFixedpoint()
static long mkBvneg(long a0, long a1)
static long mkBvxor(long a0, long a1, long a2)
static long mkIntToStr(long a0, long a1)
BitVecSort mkBitVecSort(int size)
FPSort mkFPSort(int ebits, int sbits)
static long probeNot(long a0, long a1)
static long mkSimpleSolver(long a0)
ArraySort mkArraySort(Sort[] domains, Sort range)
static long mkIff(long a0, long a1, long a2)
static long probeEq(long a0, long a1, long a2)
static long mkSelect(long a0, long a1, long a2)
ReExpr mkRange(SeqExpr lo, SeqExpr hi)
Solver mkSolver(String logic)
FuncDecl mkConstDecl(Symbol name, Sort range)
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
static long mkString(long a0, String a1)
SeqExpr mkConcat(SeqExpr... t)
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
BoolExpr mkFPGEq(FPExpr t1, FPExpr t2)
Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
FPExpr mkFPMin(FPExpr t1, FPExpr t2)
static String probeGetDescr(long a0, String a1)
static long mkFalse(long a0)
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Expr mkConst(Symbol name, Sort range)
static long mkBvnor(long a0, long a1, long a2)
static long mkFpaRoundTowardPositive(long a0)
Expr mkBound(int index, Sort ty)
FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2)
FPRMNum mkFPRoundTowardPositive()
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
static long mkFpaSort16(long a0)
static long mkIsInt(long a0, long a1)
static long mkSeqReplace(long a0, long a1, long a2, long a3)
FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2)
ArithExpr mkMul(ArithExpr... t)
static long mkFpaIsNan(long a0, long a1)
static long mkReComplement(long a0, long a1)
static long mkBvadd(long a0, long a1, long a2)
static long mkEq(long a0, long a1, long a2)
static long mkAtmost(long a0, int a1, long[] a2, int a3)
static long mkFpaRem(long a0, long a1, long a2)
static String getProbeName(long a0, int a1)
static long mkFpaNumeralFloat(long a0, float a1, long a2)
SeqExpr mkString(String s)
static long mkFpaToFpBv(long a0, long a1, long a2)
ArrayExpr mkArrayConst(Symbol name, Sort domain, Sort range)
ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
static long mkReUnion(long a0, int a1, long[] a2)
FPNum mkFPNumeral(boolean sgn, long exp, long sig, FPSort s)
static long tacticParOr(long a0, int a1, long[] a2)
static String simplifyGetHelp(long a0)
static long mkStrToInt(long a0, long a1)
IDecRefQueue< ConstructorList > getConstructorListDRQ()
static long mkReLoop(long a0, long a1, int a2, int a3)
def FiniteDomainSort(name, sz, ctx=None)
SeqExpr mkEmptySeq(Sort s)
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
static long mkRePlus(long a0, long a1)
BitVecExpr mkBVSub(BitVecExpr t1, BitVecExpr t2)
static long mkBvuge(long a0, long a1, long a2)
BoolExpr mkFPIsNormal(FPExpr t)
static long mkFpaNeg(long a0, long a1)
static long mkFpaSortSingle(long a0)
static long mkSeqAt(long a0, long a1, long a2)
FPExpr mkFPRem(FPExpr t1, FPExpr t2)
ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
ArithExpr mkDiv(ArithExpr t1, ArithExpr t2)
ArrayExpr mkArrayConst(String name, Sort domain, Sort range)
EnumSort mkEnumSort(String name, String... enumNames)
ArrayExpr mkEmptySet(Sort domain)
static long mkBvule(long a0, long a1, long a2)
static long mkSeqSuffix(long a0, long a1, long a2)
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
Solver mkSolver(Symbol logic)
Probe constProbe(double val)
ArraySort mkArraySort(Sort domain, Sort range)
static long mkRem(long a0, long a1, long a2)
static long mkFpaEq(long a0, long a1, long a2)
IDecRefQueue< FuncInterp > getFuncInterpDRQ()
BoolExpr mkBool(boolean value)
static long mkSeqEmpty(long a0, long a1)
static long tacticFailIf(long a0, long a1)
BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
IDecRefQueue< Goal > getGoalDRQ()
static long mkFpaLeq(long a0, long a1, long a2)
BitVecExpr mkFPToIEEEBV(FPExpr t)
static long mkSeqToRe(long a0, long a1)
IntExpr mkMod(IntExpr t1, IntExpr t2)
static long mkFpaRtz(long a0)
Tactic andThen(Tactic t1, Tactic t2, Tactic... ts)
static long mkPble(long a0, int a1, long[] a2, int[] a3, int a4)
BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
RealExpr mkInt2Real(IntExpr t)
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
static long mkAtleast(long a0, int a1, long[] a2, int a3)
static long mkSetDifference(long a0, long a1, long a2)
IDecRefQueue< Constructor > getConstructorDRQ()
BoolExpr mkBoolConst(Symbol name)
static long mkArrayDefault(long a0, long a1)
BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
static long mkBvugt(long a0, long a1, long a2)
Context(Map< String, String > settings)
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
static long mkReFull(long a0, long a1)
static int getNumTactics(long a0)
static long mkBvudiv(long a0, long a1, long a2)
Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long mkInt64(long a0, long a1, long a2)
ArrayExpr mkSetIntersection(ArrayExpr... args)
static long mkBvnand(long a0, long a1, long a2)
static long mkEmptySet(long a0, long a1)
FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
IDecRefQueue< Params > getParamsDRQ()
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long mkAnd(long a0, int a1, long[] a2)
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
static long mkExtract(long a0, int a1, int a2, long a3)
BitVecNum mkBV(long v, int size)
static long mkSelectN(long a0, long a1, int a2, long[] a3)
Tactic cond(Probe p, Tactic t1, Tactic t2)
static long mkAdd(long a0, int a1, long[] a2)
RealExpr mkRealConst(String name)
static long tacticAndThen(long a0, long a1, long a2)
static long mkConst(long a0, long a1, long a2)
static long mkFpaAdd(long a0, long a1, long a2, long a3)
Tactic parAndThen(Tactic t1, Tactic t2)
static long mkRotateRight(long a0, int a1, long a2)
FPRMNum mkFPRoundTowardZero()
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkFPGt(FPExpr t1, FPExpr t2)
BitVecExpr mkBVSRem(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
Tactic parOr(Tactic... t)
static long mkFpaRne(long a0)
Probe lt(Probe p1, Probe p2)
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
static long mkBvslt(long a0, long a1, long a2)
ArrayExpr mkConstArray(Sort domain, Expr v)
static long mkFpaIsZero(long a0, long a1)
BitVecNum mkBV(int v, int size)
static long mkReal2int(long a0, long a1)
ArithExpr mkSub(ArithExpr... t)
FPExpr mkFPToFP(BitVecExpr bv, FPSort s)
IntExpr stringToInt(Expr e)
static long mkFpaNan(long a0, long a1)
static long mkFpaSortHalf(long a0)
BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
static long mkBvsmod(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 mkImplies(long a0, long a1, long a2)
DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
Tactic orElse(Tactic t1, Tactic t2)
Probe le(Probe p1, Probe p2)
static long probeLt(long a0, long a1, long a2)
static long mkBvnegNoOverflow(long a0, long a1)
ArithExpr mkUnaryMinus(ArithExpr t)
static long mkSetDel(long a0, long a1, long a2)
static long tacticParAndThen(long a0, long a1, long a2)
IDecRefQueue< Probe > getProbeDRQ()
BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
BitVecNum mkBV(String v, int size)
BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
static long mkInt2real(long a0, long a1)
FuncDecl mkFreshConstDecl(String prefix, Sort range)
static long mkSolverFromTactic(long a0, long a1)
ParamDescrs getSimplifyParameterDescriptions()
SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
String getTacticDescription(String name)
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
static long mkBvsgt(long a0, long a1, long a2)
Pattern mkPattern(Expr... terms)
static long mkFpaMul(long a0, long a1, long a2, long a3)
static long mkFpaLt(long a0, long a1, long a2)
static long mkBvnot(long a0, long a1)
BitVecExpr mkSignExt(int i, BitVecExpr t)
RatNum mkReal(int num, int den)
static void delContext(long a0)
Expr mkSelect(ArrayExpr a, Expr[] args)
static long mkFpaZero(long a0, long a1, boolean a2)
static long simplifyGetParamDescrs(long a0)
FuncDecl mkFuncDecl(String name, Sort domain, Sort range)
BoolExpr mkEq(Expr x, Expr y)
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkAtMost(BoolExpr[] args, int k)
static void updateParamValue(long a0, String a1, String a2)
static long mkGe(long a0, long a1, long a2)
static long mkArrayExt(long a0, long a1, long a2)
BoolExpr mkFPIsZero(FPExpr t)
FPRMSort mkFPRoundingModeSort()
static long mkPower(long a0, long a1, long a2)
ListSort mkListSort(Symbol name, Sort elemSort)
FPNum mkFPNumeral(double v, FPSort s)
static long mkPbge(long a0, int a1, long[] a2, int[] a3, int a4)
static void setAstPrintMode(long a0, int a1)
Expr mkNumeral(long v, Sort ty)
static long mkReSort(long a0, long a1)
static long mkSeqLength(long a0, long a1)
BoolExpr mkNot(BoolExpr a)
BitVecExpr mkBVNeg(BitVecExpr t)
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static long mkExtRotateRight(long a0, long a1, long a2)
ReExpr mkOption(ReExpr re)
Expr mkNumeral(int v, Sort ty)
static long mkFpaSortDouble(long a0)
RealExpr mkRealConst(Symbol name)
static long mkFpaRoundTowardZero(long a0)
static long mkSetIntersect(long a0, int a1, long[] a2)
static long mkFpaMin(long a0, long a1, long a2)
static long tacticCond(long a0, long a1, long a2, long a3)
ListSort mkListSort(String name, Sort elemSort)
Solver mkSolver(Tactic t)
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
static long mkFpaRoundNearestTiesToEven(long a0)
StringSymbol mkSymbol(String name)
def FPSort(ebits, sbits, ctx=None)
BitVecExpr mkZeroExt(int i, BitVecExpr t)
static long mkConstArray(long a0, long a1, long a2)
static long mkPbeq(long a0, int a1, long[] a2, int[] a3, int a4)
static long mkSeqSort(long a0, long a1)
String[] getTacticNames()
Probe and(Probe p1, Probe p2)
static Lambda of(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
Expr mkSelect(ArrayExpr a, Expr i)
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
static long mkBvult(long a0, long a1, long a2)
IDecRefQueue< Statistics > getStatisticsDRQ()
FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
static long mkFpaAbs(long a0, long a1)
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
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 mkNot(long a0, long a1)
BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
static long mkLe(long a0, long a1, long a2)
Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
void setPrintMode(Z3_ast_print_mode value)
BoolExpr mkFPIsSubnormal(FPExpr t)
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Z3_PRINT_SMTLIB2_COMPLIANT
BoolExpr mkFPLt(FPExpr t1, FPExpr t2)
Goal mkGoal(boolean models, boolean unsatCores, boolean proofs)
ArrayExpr mkSetComplement(ArrayExpr arg)
ReExpr mkConcat(ReExpr... t)
static long mkGt(long a0, long a1, long a2)
IDecRefQueue< Fixedpoint > getFixedpointDRQ()
FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t)
UninterpretedSort mkUninterpretedSort(String str)
static long mkStringSort(long a0)
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
static int getNumProbes(long a0)
static long mkStore(long a0, long a1, long a2, long a3)
FPNum mkFPInf(FPSort s, boolean negative)
IntExpr mkIntConst(Symbol name)
static long mkBvashr(long a0, long a1, long a2)
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
static long mkNumeral(long a0, String a1, long a2)
BoolExpr mkFPIsNegative(FPExpr t)
expr max(expr const &a, expr const &b)
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
Tactic when(Probe p, Tactic t)
BoolExpr mkFPEq(FPExpr t1, FPExpr t2)
AST wrapAST(long nativeObject)
BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
static long mkFpaGt(long a0, long a1, long a2)
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
def BitVecSort(sz, ctx=None)
ArithExpr mkAdd(ArithExpr... t)
BoolExpr mkDistinct(Expr... args)
Tactic then(Tactic t1, Tactic t2, Tactic... ts)
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
static long mkSetComplement(long a0, long a1)
static long mkFpaSort128(long a0)
static long mkConcat(long a0, long a1, long a2)
static long mkBvmul(long a0, long a1, long a2)
Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long mkFpaRtn(long a0)
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
IDecRefQueue< AST > getASTDRQ()
FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
static long mkBvlshr(long a0, long a1, long a2)
Expr mkNumeral(String v, Sort ty)
static long tacticSkip(long a0)
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
SeqExpr mkUnit(Expr elem)
BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
RealExpr mkFPToReal(FPExpr t)
Tactic failIfNotDecided()
BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
static long mkFpaRtp(long a0)
BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
static long mkBvredor(long a0, long a1)
static long tacticUsingParams(long a0, long a1, long a2)
static long mkFpaToReal(long a0, long a1)
static long mkTrue(long a0)
def EnumSort(name, values, ctx=None)
SetSort mkSetSort(Sort ty)
ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
static long mkFpaInf(long a0, long a1, boolean a2)
static long mkBound(long a0, int a1, long a2)
BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
static long mkXor(long a0, long a1, long a2)
static long mkReStar(long a0, long a1)
BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
static long mkSignExt(long a0, int a1, long a2)
static long mkFpaIsNegative(long a0, long a1)
BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
FPNum mkFPNumeral(boolean sgn, int exp, int sig, FPSort s)
FPNum mkFPNumeral(int v, FPSort s)
static long tacticOrElse(long a0, long a1, long a2)
BoolExpr mkFPIsInfinite(FPExpr t)
IDecRefQueue< Model > getModelDRQ()
FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
Probe eq(Probe p1, Probe p2)
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
IDecRefQueue< Tactic > getTacticDRQ()
static String tacticGetDescr(long a0, String a1)
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
ReExpr mkLoop(ReExpr re, int lo)
static long mkFpaSort64(long a0)
static long mkFpaFma(long a0, long a1, long a2, long a3, long a4)
static long mkBv2int(long a0, long a1, boolean a2)
static long mkSeqContains(long a0, long a1, long a2)
static void delConfig(long a0)
static long mkUnaryMinus(long a0, long a1)
String getProbeDescription(String name)
BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
FPNum mkFP(float v, FPSort s)
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
FPRMNum mkFPRoundTowardNegative()
static long mkFpaToIeeeBv(long a0, long a1)
static int arrayLength(Z3Object[] a)
SeqExpr intToString(Expr e)
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
ReExpr mkComplement(ReExpr re)
static long mkFullSet(long a0, long a1)
BoolExpr mkInRe(SeqExpr s, ReExpr re)
static long mkBvredand(long a0, long a1)
BoolExpr mkFPLEq(FPExpr t1, FPExpr t2)
static long mkExtRotateLeft(long a0, long a1, long a2)
ReExpr mkIntersect(ReExpr... t)
BoolExpr mkAtLeast(BoolExpr[] args, int k)
FPSort mkFPSortQuadruple()
IntExpr mkReal2Int(RealExpr t)
BitVecExpr mkExtract(int high, int low, BitVecExpr t)
static long probeGe(long a0, long a1, long a2)
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
static long mkInt(long a0, int a1, long a2)
Lambda mkLambda(Expr[] boundConstants, Expr body)
static long mkMap(long a0, long a1, int a2, long[] a3)
static long tacticRepeat(long a0, long a1, int a2)
static long mkFpaNumeralInt(long a0, int a1, long a2)
static long mkSeqIndex(long a0, long a1, long a2, long a3)
Probe mkProbe(String name)
FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)
static String getTacticName(long a0, int a1)
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
static long mkReIntersect(long a0, int a1, long[] a2)
FPNum mkFP(int v, FPSort s)
BitVecExpr mkBVConst(String name, int size)
static long mkFpaRna(long a0)
Tactic tryFor(Tactic t, int ms)
BoolExpr mkFPIsPositive(FPExpr t)
static long mkContextRc(long a0)
static long mkBvsge(long a0, long a1, long a2)
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
static long probeLe(long a0, long a1, long a2)
static long mkFreshConst(long a0, String a1, long a2)
BoolExpr mkFPIsNaN(FPExpr t)
BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
static long[] arrayToNative(Z3Object[] a)
static long mkPattern(long a0, int a1, long[] a2)
static long mkSolver(long a0)
static long mkMul(long a0, int a1, long[] a2)
Expr mkUpdateField(FuncDecl field, Expr t, Expr v)
static long tacticFail(long a0)
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkBVNegNoOverflow(BitVecExpr t)
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
FuncDecl mkConstDecl(String name, Sort range)
FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2)
FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)
static long probeOr(long a0, long a1, long a2)
static native void setInternalErrorHandler(long ctx)
static long mkSetUnion(long a0, int a1, long[] a2)
static long probeGt(long a0, long a1, long a2)
static void setParamValue(long a0, String a1, String a2)
static long probeAnd(long a0, long a1, long a2)
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
static long mkFpaFp(long a0, long a1, long a2, long a3)
BoolExpr mkBVSLE(BitVecExpr t1, BitVecExpr t2)
static long mkFpaIsNormal(long a0, long a1)
FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
IntExpr mkLength(SeqExpr s)
static long mkFpaGeq(long a0, long a1, long a2)
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
static long mkSeqPrefix(long a0, long a1, long a2)
static long mkReal(long a0, int a1, int a2)
FiniteDomainSort mkFiniteDomainSort(String name, long size)
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
BitVecExpr mkBVRedAND(BitVecExpr t)
BoolExpr mkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
static long mkReRange(long a0, long a1, long a2)
static long mkInt2bv(long a0, int a1, long a2)
FPRMNum mkFPRoundNearestTiesToAway()
static long mkFpaIsInfinite(long a0, long a1)
static long mkBvurem(long a0, long a1, long a2)
static long mkBvsub(long a0, long a1, long a2)
UninterpretedSort mkUninterpretedSort(Symbol s)
static long mkFpaIsPositive(long a0, long a1)
EnumSort mkEnumSort(Symbol name, Symbol... enumNames)
IDecRefQueue< ASTMap > getASTMapDRQ()
ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
static long mkBvsrem(long a0, long a1, long a2)
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
static long mkSeqInRe(long a0, long a1, long a2)
BitVecExpr mkBVRedOR(BitVecExpr t)
static long mkBvsubNoOverflow(long a0, long a1, long a2)
ReExpr mkUnion(ReExpr... t)
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
FPRMExpr mkFPRoundNearestTiesToEven()
Tactic usingParams(Tactic t, Params p)
BoolExpr[] ToBoolExprArray()
FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
static long mkSeqUnit(long a0, long a1)
static long mkMod(long a0, long a1, long a2)
BoolExpr mkIsInteger(RealExpr t)
BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
static long mkBvand(long a0, long a1, long a2)
FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2)
ArrayExpr mkSetDel(ArrayExpr set, Expr element)
static long tacticWhen(long a0, long a1, long a2)
def String(name, ctx=None)
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
SeqExpr mkAt(SeqExpr s, IntExpr index)
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)