18 package com.microsoft.z3;
61 for (
Map.Entry<String, String> kv : settings.entrySet())
94 for (
int i = 0; i < names.length; ++i)
100 private IntSort m_intSort = null;
108 if (m_boolSort == null)
118 if (m_intSort == null)
128 if (m_realSort == null)
148 checkContextMatch(s);
194 checkContextMatch(domain);
195 checkContextMatch(range);
196 return new ArraySort(
this, domain, range);
206 checkContextMatch(name);
207 checkContextMatch(fieldNames);
208 checkContextMatch(fieldSorts);
209 return new TupleSort(
this, name, (
int) fieldNames.length, fieldNames,
220 checkContextMatch(name);
221 checkContextMatch(enumNames);
222 return new EnumSort(
this, name, enumNames);
240 checkContextMatch(name);
241 checkContextMatch(elemSort);
242 return new ListSort(
this, name, elemSort);
251 checkContextMatch(elemSort);
262 checkContextMatch(name);
288 Symbol[] fieldNames,
Sort[] sorts,
int[] sortRefs)
292 return new Constructor(
this, name, recognizer, fieldNames, sorts,
304 String[] fieldNames,
Sort[] sorts,
int[] sortRefs)
309 MkSymbols(fieldNames), sorts, sortRefs);
319 checkContextMatch(name);
320 checkContextMatch(constructors);
331 checkContextMatch(constructors);
344 checkContextMatch(names);
345 int n = (int) names.length;
347 long[] n_constr =
new long[n];
348 for (
int i = 0; i < n; i++)
352 checkContextMatch(constructor);
354 n_constr[i] = cla[i].getNativeObject();
356 long[] n_res =
new long[n];
360 for (
int i = 0; i < n; i++)
385 checkContextMatch(name);
386 checkContextMatch(domain);
387 checkContextMatch(range);
388 return new FuncDecl(
this, name, domain, range);
398 checkContextMatch(name);
399 checkContextMatch(domain);
400 checkContextMatch(range);
402 return new FuncDecl(
this, name, q, range);
412 checkContextMatch(domain);
413 checkContextMatch(range);
424 checkContextMatch(domain);
425 checkContextMatch(range);
439 checkContextMatch(domain);
440 checkContextMatch(range);
441 return new FuncDecl(
this, prefix, domain, range);
450 checkContextMatch(name);
451 checkContextMatch(range);
452 return new FuncDecl(
this, name, null, range);
461 checkContextMatch(range);
474 checkContextMatch(range);
475 return new FuncDecl(
this, prefix, null, range);
484 return Expr.create(
this,
493 if (terms.length == 0)
494 throw new Z3Exception(
"Cannot create a pattern from zero terms");
496 long[] termsNative =
AST.arrayToNative(terms);
508 checkContextMatch(name);
509 checkContextMatch(range);
514 range.getNativeObject()));
534 checkContextMatch(range);
535 return Expr.create(
this,
626 checkContextMatch(f);
627 checkContextMatch(args);
628 return Expr.create(
this, f, args);
660 checkContextMatch(x);
661 checkContextMatch(y);
663 y.getNativeObject()));
671 checkContextMatch(args);
673 AST.arrayToNative(args)));
682 checkContextMatch(a);
695 checkContextMatch(t1);
696 checkContextMatch(t2);
697 checkContextMatch(t3);
699 t2.getNativeObject(), t3.getNativeObject()));
708 checkContextMatch(t1);
709 checkContextMatch(t2);
711 t2.getNativeObject()));
720 checkContextMatch(t1);
721 checkContextMatch(t2);
723 t1.getNativeObject(), t2.getNativeObject()));
732 checkContextMatch(t1);
733 checkContextMatch(t2);
735 t2.getNativeObject()));
744 checkContextMatch(t);
746 AST.arrayToNative(t)));
755 checkContextMatch(t);
757 AST.arrayToNative(t)));
766 checkContextMatch(t);
777 checkContextMatch(t);
788 checkContextMatch(t);
799 checkContextMatch(t);
810 checkContextMatch(t1);
811 checkContextMatch(t2);
813 t1.getNativeObject(), t2.getNativeObject()));
823 checkContextMatch(t1);
824 checkContextMatch(t2);
826 t2.getNativeObject()));
836 checkContextMatch(t1);
837 checkContextMatch(t2);
839 t2.getNativeObject()));
848 checkContextMatch(t1);
849 checkContextMatch(t2);
853 t2.getNativeObject()));
862 checkContextMatch(t1);
863 checkContextMatch(t2);
865 t2.getNativeObject()));
874 checkContextMatch(t1);
875 checkContextMatch(t2);
877 t2.getNativeObject()));
886 checkContextMatch(t1);
887 checkContextMatch(t2);
889 t2.getNativeObject()));
898 checkContextMatch(t1);
899 checkContextMatch(t2);
901 t2.getNativeObject()));
916 checkContextMatch(t);
929 checkContextMatch(t);
939 checkContextMatch(t);
950 checkContextMatch(t);
961 checkContextMatch(t);
963 t.getNativeObject()));
973 checkContextMatch(t);
975 t.getNativeObject()));
985 checkContextMatch(t1);
986 checkContextMatch(t2);
988 t1.getNativeObject(), t2.getNativeObject()));
998 checkContextMatch(t1);
999 checkContextMatch(t2);
1001 t2.getNativeObject()));
1011 checkContextMatch(t1);
1012 checkContextMatch(t2);
1014 t1.getNativeObject(), t2.getNativeObject()));
1024 checkContextMatch(t1);
1025 checkContextMatch(t2);
1027 t1.getNativeObject(), 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(t);
1074 checkContextMatch(t1);
1075 checkContextMatch(t2);
1077 t1.getNativeObject(), t2.getNativeObject()));
1087 checkContextMatch(t1);
1088 checkContextMatch(t2);
1090 t1.getNativeObject(), t2.getNativeObject()));
1100 checkContextMatch(t1);
1101 checkContextMatch(t2);
1103 t1.getNativeObject(), t2.getNativeObject()));
1115 checkContextMatch(t1);
1116 checkContextMatch(t2);
1118 t1.getNativeObject(), t2.getNativeObject()));
1136 checkContextMatch(t1);
1137 checkContextMatch(t2);
1139 t1.getNativeObject(), t2.getNativeObject()));
1151 checkContextMatch(t1);
1152 checkContextMatch(t2);
1154 t1.getNativeObject(), t2.getNativeObject()));
1169 checkContextMatch(t1);
1170 checkContextMatch(t2);
1172 t1.getNativeObject(), t2.getNativeObject()));
1183 checkContextMatch(t1);
1184 checkContextMatch(t2);
1186 t1.getNativeObject(), t2.getNativeObject()));
1196 checkContextMatch(t1);
1197 checkContextMatch(t2);
1199 t2.getNativeObject()));
1209 checkContextMatch(t1);
1210 checkContextMatch(t2);
1212 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()));
1305 checkContextMatch(t1);
1306 checkContextMatch(t2);
1308 t1.getNativeObject(), t2.getNativeObject()));
1322 checkContextMatch(t);
1324 t.getNativeObject()));
1336 checkContextMatch(t);
1338 t.getNativeObject()));
1350 checkContextMatch(t);
1352 t.getNativeObject()));
1362 checkContextMatch(t);
1364 t.getNativeObject()));
1380 checkContextMatch(t1);
1381 checkContextMatch(t2);
1383 t1.getNativeObject(), t2.getNativeObject()));
1399 checkContextMatch(t1);
1400 checkContextMatch(t2);
1402 t1.getNativeObject(), t2.getNativeObject()));
1419 checkContextMatch(t1);
1420 checkContextMatch(t2);
1422 t1.getNativeObject(), t2.getNativeObject()));
1432 checkContextMatch(t);
1434 t.getNativeObject()));
1444 checkContextMatch(t);
1446 t.getNativeObject()));
1458 checkContextMatch(t1);
1459 checkContextMatch(t2);
1461 t1.getNativeObject(), t2.getNativeObject()));
1473 checkContextMatch(t1);
1474 checkContextMatch(t2);
1476 t1.getNativeObject(), t2.getNativeObject()));
1490 checkContextMatch(t);
1492 t.getNativeObject()));
1512 checkContextMatch(t);
1514 (signed) ?
true :
false));
1525 checkContextMatch(t1);
1526 checkContextMatch(t2);
1528 .getNativeObject(), t2.getNativeObject(), (isSigned) ?
true
1540 checkContextMatch(t1);
1541 checkContextMatch(t2);
1543 t1.getNativeObject(), t2.getNativeObject()));
1554 checkContextMatch(t1);
1555 checkContextMatch(t2);
1557 t1.getNativeObject(), t2.getNativeObject()));
1568 checkContextMatch(t1);
1569 checkContextMatch(t2);
1571 .getNativeObject(), t2.getNativeObject(), (isSigned) ?
true
1583 checkContextMatch(t1);
1584 checkContextMatch(t2);
1586 t1.getNativeObject(), t2.getNativeObject()));
1596 checkContextMatch(t);
1598 t.getNativeObject()));
1609 checkContextMatch(t1);
1610 checkContextMatch(t2);
1612 .getNativeObject(), t2.getNativeObject(), (isSigned) ?
true
1624 checkContextMatch(t1);
1625 checkContextMatch(t2);
1627 t1.getNativeObject(), t2.getNativeObject()));
1662 checkContextMatch(a);
1663 checkContextMatch(i);
1667 i.getNativeObject()));
1686 checkContextMatch(a);
1687 checkContextMatch(i);
1688 checkContextMatch(v);
1690 i.getNativeObject(), v.getNativeObject()));
1702 checkContextMatch(domain);
1703 checkContextMatch(v);
1705 domain.getNativeObject(), v.getNativeObject()));
1720 checkContextMatch(f);
1721 checkContextMatch(args);
1723 f.getNativeObject(),
AST.arrayLength(args),
1724 AST.arrayToNative(args)));
1735 checkContextMatch(array);
1736 return Expr.create(
this,
1746 checkContextMatch(ty);
1756 checkContextMatch(domain);
1757 return Expr.create(
this,
1767 checkContextMatch(domain);
1768 return Expr.create(
this,
1778 checkContextMatch(set);
1779 checkContextMatch(element);
1783 element.getNativeObject()));
1792 checkContextMatch(set);
1793 checkContextMatch(element);
1797 element.getNativeObject()));
1806 checkContextMatch(args);
1810 AST.arrayToNative(args)));
1819 checkContextMatch(args);
1823 AST.arrayToNative(args)));
1832 checkContextMatch(arg1);
1833 checkContextMatch(arg2);
1837 arg2.getNativeObject()));
1846 checkContextMatch(arg);
1847 return Expr.create(
this,
1857 checkContextMatch(elem);
1858 checkContextMatch(set);
1862 set.getNativeObject()));
1871 checkContextMatch(arg1);
1872 checkContextMatch(arg2);
1876 arg2.getNativeObject()));
1893 checkContextMatch(ty);
1894 return Expr.create(
this,
1911 checkContextMatch(ty);
1912 return Expr.create(
this,
Native.
mkInt(nCtx(), v, ty.getNativeObject()));
1928 checkContextMatch(ty);
1929 return Expr.create(
this,
1958 .getNativeObject()));
1970 .getNativeObject()));
1982 .getNativeObject()));
1993 .getNativeObject()));
2005 .getNativeObject()));
2017 .getNativeObject()));
2071 int weight,
Pattern[] patterns,
Expr[] noPatterns,
2075 return new Quantifier(
this,
true, sorts, names, body, weight, patterns,
2076 noPatterns, quantifierID, skolemID);
2087 return new Quantifier(
this,
true, boundConstants, body, weight,
2088 patterns, noPatterns, quantifierID, skolemID);
2096 int weight,
Pattern[] patterns,
Expr[] noPatterns,
2100 return new Quantifier(
this,
false, sorts, names, body, weight,
2101 patterns, noPatterns, quantifierID, skolemID);
2112 return new Quantifier(
this,
false, boundConstants, body, weight,
2113 patterns, noPatterns, quantifierID, skolemID);
2126 return mkForall(sorts, names, body, weight, patterns, noPatterns,
2127 quantifierID, skolemID);
2129 return mkExists(sorts, names, body, weight, patterns, noPatterns,
2130 quantifierID, skolemID);
2142 return mkForall(boundConstants, body, weight, patterns, noPatterns,
2143 quantifierID, skolemID);
2145 return mkExists(boundConstants, body, weight, patterns, noPatterns,
2146 quantifierID, skolemID);
2178 String status, String attributes,
BoolExpr[] assumptions,
2183 attributes, (
int) assumptions.length,
2184 AST.arrayToNative(assumptions), formula.getNativeObject());
2199 int csn =
Symbol.arrayLength(sortNames);
2200 int cs =
Sort.arrayLength(sorts);
2201 int cdn =
Symbol.arrayLength(declNames);
2202 int cd =
AST.arrayLength(decls);
2203 if (csn != cs || cdn != cd)
2206 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2207 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2208 AST.arrayToNative(decls));
2219 int csn =
Symbol.arrayLength(sortNames);
2220 int cs =
Sort.arrayLength(sorts);
2221 int cdn =
Symbol.arrayLength(declNames);
2222 int cd =
AST.arrayLength(decls);
2223 if (csn != cs || cdn != cd)
2226 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2227 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2228 AST.arrayToNative(decls));
2249 for (
int i = 0; i < n; i++)
2273 for (
int i = 0; i < n; i++)
2297 for (
int i = 0; i < n; i++)
2320 for (
int i = 0; i < n; i++)
2337 int csn =
Symbol.arrayLength(sortNames);
2338 int cs =
Sort.arrayLength(sorts);
2339 int cdn =
Symbol.arrayLength(declNames);
2340 int cd =
AST.arrayLength(decls);
2341 if (csn != cs || cdn != cd)
2344 str,
AST.arrayLength(sorts),
Symbol.arrayToNative(sortNames),
2345 AST.arrayToNative(sorts),
AST.arrayLength(decls),
2346 Symbol.arrayToNative(declNames),
AST.arrayToNative(decls)));
2358 int csn =
Symbol.arrayLength(sortNames);
2359 int cs =
Sort.arrayLength(sorts);
2360 int cdn =
Symbol.arrayLength(declNames);
2361 int cd =
AST.arrayLength(decls);
2362 if (csn != cs || cdn != cd)
2365 fileName,
AST.arrayLength(sorts),
2366 Symbol.arrayToNative(sortNames),
AST.arrayToNative(sorts),
2367 AST.arrayLength(decls),
Symbol.arrayToNative(declNames),
2368 AST.arrayToNative(decls)));
2380 public Goal mkGoal(
boolean models,
boolean unsatCores,
boolean proofs)
2384 return new Goal(
this, models, unsatCores, proofs);
2411 String[] res =
new String[n];
2412 for (
int i = 0; i < n; i++)
2433 return new Tactic(
this, name);
2443 checkContextMatch(t1);
2444 checkContextMatch(t2);
2445 checkContextMatch(ts);
2448 if (ts != null && ts.length > 0)
2450 last = ts[ts.length - 1].getNativeObject();
2451 for (
int i = ts.length - 2; i >= 0; i--)
2459 t1.getNativeObject(), last));
2462 t1.getNativeObject(), t2.getNativeObject()));
2483 checkContextMatch(t1);
2484 checkContextMatch(t2);
2486 t1.getNativeObject(), t2.getNativeObject()));
2498 checkContextMatch(t);
2500 t.getNativeObject(), ms));
2512 checkContextMatch(t);
2513 checkContextMatch(p);
2515 t.getNativeObject()));
2526 checkContextMatch(p);
2527 checkContextMatch(t1);
2528 checkContextMatch(t2);
2530 t1.getNativeObject(), t2.getNativeObject()));
2541 checkContextMatch(t);
2543 t.getNativeObject(), max));
2571 checkContextMatch(p);
2591 checkContextMatch(t);
2592 checkContextMatch(p);
2594 t.getNativeObject(), p.getNativeObject()));
2612 checkContextMatch(t);
2625 checkContextMatch(t1);
2626 checkContextMatch(t2);
2628 t1.getNativeObject(), t2.getNativeObject()));
2655 String[] res =
new String[n];
2656 for (
int i = 0; i < n; i++)
2675 return new Probe(
this, name);
2694 checkContextMatch(p1);
2695 checkContextMatch(p2);
2697 p2.getNativeObject()));
2708 checkContextMatch(p1);
2709 checkContextMatch(p2);
2711 p2.getNativeObject()));
2722 checkContextMatch(p1);
2723 checkContextMatch(p2);
2725 p2.getNativeObject()));
2735 checkContextMatch(p1);
2736 checkContextMatch(p2);
2738 p2.getNativeObject()));
2748 checkContextMatch(p1);
2749 checkContextMatch(p2);
2751 p2.getNativeObject()));
2760 checkContextMatch(p1);
2761 checkContextMatch(p2);
2763 p2.getNativeObject()));
2772 checkContextMatch(p1);
2773 checkContextMatch(p2);
2775 p2.getNativeObject()));
2785 checkContextMatch(p);
2813 logic.getNativeObject()));
2843 t.getNativeObject()));
2867 return AST.create(
this, nativeObject);
2881 return a.getNativeObject();
2932 void initContext() throws Z3Exception
2935 Native.setInternalErrorHandler(nCtx());
2938 void checkContextMatch(Z3Object other)
throws Z3Exception
2940 if (
this != other.getContext())
2941 throw new Z3Exception(
"Context mismatch");
2944 void checkContextMatch(Z3Object[] arr)
throws Z3Exception
2947 for (Z3Object a : arr)
2948 checkContextMatch(a);
2951 private ASTDecRefQueue m_AST_DRQ =
new ASTDecRefQueue();
2952 private ASTMapDecRefQueue m_ASTMap_DRQ =
new ASTMapDecRefQueue();
2953 private ASTVectorDecRefQueue m_ASTVector_DRQ =
new ASTVectorDecRefQueue();
2954 private ApplyResultDecRefQueue m_ApplyResult_DRQ =
new ApplyResultDecRefQueue();
2955 private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ =
new FuncInterpEntryDecRefQueue();
2956 private FuncInterpDecRefQueue m_FuncInterp_DRQ =
new FuncInterpDecRefQueue();
2957 private GoalDecRefQueue m_Goal_DRQ =
new GoalDecRefQueue();
2958 private ModelDecRefQueue m_Model_DRQ =
new ModelDecRefQueue();
2959 private ParamsDecRefQueue m_Params_DRQ =
new ParamsDecRefQueue();
2960 private ParamDescrsDecRefQueue m_ParamDescrs_DRQ =
new ParamDescrsDecRefQueue();
2961 private ProbeDecRefQueue m_Probe_DRQ =
new ProbeDecRefQueue();
2962 private SolverDecRefQueue m_Solver_DRQ =
new SolverDecRefQueue();
2963 private StatisticsDecRefQueue m_Statistics_DRQ =
new StatisticsDecRefQueue();
2964 private TacticDecRefQueue m_Tactic_DRQ =
new TacticDecRefQueue();
2965 private FixedpointDecRefQueue m_Fixedpoint_DRQ =
new FixedpointDecRefQueue();
2967 ASTDecRefQueue ast_DRQ()
2972 ASTMapDecRefQueue astmap_DRQ()
2974 return m_ASTMap_DRQ;
2977 ASTVectorDecRefQueue astvector_DRQ()
2979 return m_ASTVector_DRQ;
2982 ApplyResultDecRefQueue applyResult_DRQ()
2984 return m_ApplyResult_DRQ;
2987 FuncInterpEntryDecRefQueue funcEntry_DRQ()
2989 return m_FuncEntry_DRQ;
2992 FuncInterpDecRefQueue funcInterp_DRQ()
2994 return m_FuncInterp_DRQ;
2997 GoalDecRefQueue goal_DRQ()
3002 ModelDecRefQueue model_DRQ()
3007 ParamsDecRefQueue params_DRQ()
3009 return m_Params_DRQ;
3012 ParamDescrsDecRefQueue paramDescrs_DRQ()
3014 return m_ParamDescrs_DRQ;
3017 ProbeDecRefQueue probe_DRQ()
3022 SolverDecRefQueue solver_DRQ()
3024 return m_Solver_DRQ;
3027 StatisticsDecRefQueue statistics_DRQ()
3029 return m_Statistics_DRQ;
3032 TacticDecRefQueue tactic_DRQ()
3034 return m_Tactic_DRQ;
3037 FixedpointDecRefQueue fixedpoint_DRQ()
3039 return m_Fixedpoint_DRQ;
3051 if (m_refCount == 0)
3056 }
catch (Z3Exception e)
3072 m_AST_DRQ.clear(
this);
3073 m_ASTMap_DRQ.clear(
this);
3074 m_ASTVector_DRQ.clear(
this);
3075 m_ApplyResult_DRQ.clear(
this);
3076 m_FuncEntry_DRQ.clear(
this);
3077 m_FuncInterp_DRQ.clear(
this);
3078 m_Goal_DRQ.clear(
this);
3079 m_Model_DRQ.clear(
this);
3080 m_Params_DRQ.clear(
this);
3081 m_Probe_DRQ.clear(
this);
3082 m_Solver_DRQ.clear(
this);
3083 m_Statistics_DRQ.clear(
this);
3084 m_Tactic_DRQ.clear(
this);
3085 m_Fixedpoint_DRQ.clear(
this);
IntExpr mkIntConst(Symbol name)
BoolExpr mkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
static long tacticRepeat(long a0, long a1, int a2)
Expr mkITE(BoolExpr t1, Expr t2, Expr t3)
static long mkBvule(long a0, long a1, long a2)
static long mkSolver(long a0)
int getNumSMTLIBAssumptions()
Tactic when(Probe p, Tactic t)
BitVecExpr mkBVXNOR(BitVecExpr t1, BitVecExpr t2)
static long mkExtract(long a0, int a1, int a2, long a3)
DatatypeSort mkDatatypeSort(String name, Constructor[] constructors)
static void interrupt(long a0)
static long getSmtlibSort(long a0, int a1)
Probe and(Probe p1, Probe p2)
static long mkMod(long a0, long a1, long a2)
static long mkBvugt(long a0, long a1, long a2)
static void delConfig(long a0)
ArrayExpr mkConstArray(Sort domain, Expr v)
static int getSmtlibNumSorts(long a0)
Constructor mkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
static long mkBvredor(long a0, long a1)
int getNumSMTLIBFormulas()
static long tacticOrElse(long a0, long a1, long a2)
Probe lt(Probe p1, Probe p2)
BoolExpr mkDistinct(Expr...args)
static int getNumProbes(long a0)
BoolExpr mkBVUGE(BitVecExpr t1, BitVecExpr t2)
static void parseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static long mkNumeral(long a0, String a1, long a2)
BitVecExpr mkBVSHL(BitVecExpr t1, BitVecExpr t2)
static void updateParamValue(long a0, String a1, String a2)
static void toggleWarningMessages(boolean a0)
BitVecExpr mkBVNeg(BitVecExpr t)
static long mkFreshConst(long a0, String a1, long a2)
ArithExpr mkSub(ArithExpr...t)
Expr mkNumeral(int v, Sort ty)
BoolExpr mkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
ListSort mkListSort(String name, Sort elemSort)
Expr mkSetAdd(Expr set, Expr element)
StringSymbol mkSymbol(String name)
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
BitVecExpr mkBVAdd(BitVecExpr t1, BitVecExpr t2)
String[] getTacticNames()
Probe eq(Probe p1, Probe p2)
BitVecExpr mkZeroExt(int i, BitVecExpr t)
static long mkOr(long a0, int a1, long[] a2)
BitVecExpr mkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
Quantifier mkExists(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
String getProbeDescription(String name)
BitVecExpr mkBVUDiv(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkAnd(BoolExpr...t)
static long mkSub(long a0, int a1, long[] a2)
static long tacticFailIf(long a0, long a1)
BitVecExpr mkBVASHR(BitVecExpr t1, BitVecExpr t2)
Tactic failIfNotDecided()
static long mkExtRotateLeft(long a0, long a1, long a2)
BoolExpr mkImplies(BoolExpr t1, BoolExpr t2)
static long mkBvlshr(long a0, long a1, long a2)
BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
BoolExpr mkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkExtract(int high, int low, BitVecExpr t)
UninterpretedSort mkUninterpretedSort(String str)
BitVecExpr mkBVSMod(BitVecExpr t1, BitVecExpr t2)
static String probeGetDescr(long a0, String a1)
static long mkBvuge(long a0, long a1, long a2)
static long mkSolverForLogic(long a0, long a1)
static long getSmtlibDecl(long a0, int a1)
static long simplifyGetParamDescrs(long a0)
static long mkLe(long a0, long a1, long a2)
static long mkSetIntersect(long a0, int a1, long[] a2)
static long mkConcat(long a0, long a1, long a2)
static long mkSelect(long a0, long a1, long a2)
static long mkBvnand(long a0, long a1, long a2)
BitVecExpr mkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
static long probeEq(long a0, long a1, long a2)
static long mkGe(long a0, long a1, long a2)
static long mkXor(long a0, long a1, long a2)
Expr mkNumeral(String v, Sort ty)
BitVecExpr mkBVURem(BitVecExpr t1, BitVecExpr t2)
TupleSort mkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
BitVecExpr mkBVMul(BitVecExpr t1, BitVecExpr t2)
static long mkBvslt(long a0, long a1, long a2)
FuncDecl mkFuncDecl(String name, Sort[] domain, Sort range)
void setPrintMode(Z3_ast_print_mode value)
static long mkAdd(long a0, int a1, long[] a2)
static int getSmtlibNumFormulas(long a0)
FuncDecl mkConstDecl(String name, Sort range)
Expr mkSetDifference(Expr arg1, Expr arg2)
static long probeOr(long a0, long a1, long a2)
SetSort mkSetSort(Sort ty)
BoolExpr mkLt(ArithExpr t1, ArithExpr t2)
IntExpr mkReal2Int(RealExpr t)
Expr mkSetComplement(Expr arg)
static long probeNot(long a0, long a1)
static long mkSignExt(long a0, int a1, long a2)
static long mkBvsmod(long a0, long a1, long a2)
AST wrapAST(long nativeObject)
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
static long mkSetComplement(long a0, long a1)
static long mkInt(long a0, int a1, long a2)
FuncDecl mkFuncDecl(Symbol name, Sort domain, Sort range)
static long probeConst(long a0, double a1)
static long mkSetAdd(long a0, long a1, long a2)
static long 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)
static long mkBvsdiv(long a0, long a1, long a2)
static long mkMap(long a0, long a1, int a2, long[] a3)
static int getNumTactics(long a0)
static long mkZeroExt(long a0, int a1, long a2)
static long mkBvnot(long a0, long a1)
static long mkDistinct(long a0, int a1, long[] a2)
BoolExpr mkIsInteger(RealExpr t)
static long mkUnaryMinus(long a0, long a1)
BoolExpr mkBVNegNoOverflow(BitVecExpr t)
static long mkSetDifference(long a0, long a1, long a2)
static long mkBvsgt(long a0, long a1, long a2)
static long mkSetDel(long a0, long a1, long a2)
static long mkRotateRight(long a0, int a1, long a2)
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
static long mkStore(long a0, long a1, long a2, long a3)
Quantifier mkQuantifier(boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
Probe gt(Probe p1, Probe p2)
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)
static long mkBvsle(long a0, long a1, long a2)
BitVecExpr mkBVOR(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkBVXOR(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkBVNot(BitVecExpr t)
BitVecExpr mkBVRedOR(BitVecExpr t)
Tactic usingParams(Tactic t, Params p)
BitVecExpr mkBVConst(String name, int size)
BoolExpr mkLe(ArithExpr t1, ArithExpr t2)
static void setAstPrintMode(long a0, int a1)
BitVecExpr mkBVSDiv(BitVecExpr t1, BitVecExpr t2)
static long mkDiv(long a0, long a1, long a2)
static long mkIte(long a0, long a1, long a2, long a3)
static String tacticGetDescr(long a0, String a1)
static long tacticFailIfNotDecided(long a0)
ArrayExpr mkMap(FuncDecl f, ArrayExpr...args)
BoolExpr mkBVSGT(BitVecExpr t1, BitVecExpr t2)
static long mkSimpleSolver(long a0)
static long mkSetMember(long a0, long a1, long a2)
Quantifier mkForall(Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
BoolExpr mkBoolConst(String name)
BitVecExpr mkRepeat(int i, BitVecExpr t)
BitVecExpr mkBVNAND(BitVecExpr t1, BitVecExpr t2)
void updateParamValue(String id, String value)
Probe mkProbe(String name)
BoolExpr mkXor(BoolExpr t1, BoolExpr t2)
BitVecExpr mkBVLSHR(BitVecExpr t1, BitVecExpr t2)
static long tacticParOr(long a0, int a1, long[] a2)
static long tacticSkip(long a0)
static int getSmtlibNumDecls(long a0)
static long mkBvurem(long a0, long a1, long a2)
Tactic repeat(Tactic t, int max)
static long mkSetSubset(long a0, long a1, long a2)
static long mkImplies(long a0, long a1, long a2)
String benchmarkToSMTString(String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)
DatatypeSort[] mkDatatypeSorts(Symbol[] names, Constructor[][] c)
Tactic then(Tactic t1, Tactic t2, Tactic...ts)
Tactic tryFor(Tactic t, int ms)
static long probeGt(long a0, long a1, long a2)
Z3_ast_print_mode
Z3 pretty printing modes (See Z3_set_ast_print_mode).
BoolExpr mkIff(BoolExpr t1, BoolExpr t2)
void parseSMTLIBFile(String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
static long getSmtlibAssumption(long a0, int a1)
IntExpr mkIntConst(String name)
Expr mkSetUnion(Expr...args)
static void ToggleWarningMessages(boolean enabled)
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)
BoolExpr mkBVULE(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkBVSGE(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkBVNOR(BitVecExpr t1, BitVecExpr t2)
FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range)
Solver mkSolver(String logic)
static long mkInt2bv(long a0, int a1, long a2)
BitVecExpr mkBVRedAND(BitVecExpr t)
ArithExpr mkAdd(ArithExpr...t)
IntExpr mkRem(IntExpr t1, IntExpr t2)
FiniteDomainSort mkFiniteDomainSort(String name, long size)
static long mkBvand(long a0, long a1, long a2)
FuncDecl mkConstDecl(Symbol name, Sort range)
Expr mkSetMembership(Expr elem, Expr set)
static long mkRepeat(long a0, int a1, long a2)
BoolExpr mkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
static long mkPattern(long a0, int a1, long[] a2)
UninterpretedSort mkUninterpretedSort(Symbol s)
void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
static String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
static long mkBvult(long a0, long a1, long a2)
static void setParamValue(long a0, String a1, String a2)
static void parseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static int getSmtlibNumAssumptions(long a0)
Expr mkFreshConst(String prefix, Sort range)
static long mkAnd(long a0, int a1, long[] a2)
static long mkLt(long a0, long a1, long a2)
Expr mkFullSet(Sort domain)
static long mkContextRc(long a0)
BoolExpr mkOr(BoolExpr...t)
Expr mkSetIntersection(Expr...args)
Expr mkTermArray(ArrayExpr array)
static long mkBvsub(long a0, long a1, long a2)
static long mkConstArray(long a0, long a1, long a2)
static long mkInt2real(long a0, long a1)
BoolExpr mkBool(boolean value)
static long mkConst(long a0, long a1, long a2)
static long mkBvsge(long a0, long a1, long a2)
Probe or(Probe p1, Probe p2)
static long tacticParAndThen(long a0, long a1, long a2)
static String getProbeName(long a0, int a1)
Tactic with(Tactic t, Params p)
IntExpr mkMod(IntExpr t1, IntExpr t2)
Probe ge(Probe p1, Probe p2)
static long mkBvashr(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)
BoolExpr mkBVSLT(BitVecExpr t1, BitVecExpr t2)
BitVecExpr mkInt2BV(int n, IntExpr t)
BitVecExpr mkBVRotateRight(int i, BitVecExpr t)
ArithExpr mkPower(ArithExpr t1, ArithExpr t2)
static long probeLe(long a0, long a1, long a2)
Context(Map< String, String > settings)
BoolExpr mkBoolConst(Symbol name)
IntSymbol mkSymbol(int i)
Expr mkApp(FuncDecl f, Expr...args)
Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
BoolExpr[] getSMTLIBAssumptions()
Expr mkConst(String name, Sort range)
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
DatatypeSort mkDatatypeSort(Symbol name, Constructor[] constructors)
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
static long mkRotateLeft(long a0, int a1, long a2)
static String simplifyGetHelp(long a0)
Tactic parAndThen(Tactic t1, Tactic t2)
BitVecExpr mkBVRotateLeft(int i, BitVecExpr t)
static long mkBvredand(long a0, long a1)
static long tacticFail(long a0)
Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)
static long mkBvxor(long a0, long a1, long a2)
EnumSort mkEnumSort(String name, String...enumNames)
static long tacticUsingParams(long a0, long a1, long a2)
BoolExpr mkBVULT(BitVecExpr t1, BitVecExpr t2)
Probe constProbe(double val)
static long probeLt(long a0, long a1, long a2)
static long mkBvudiv(long a0, long a1, long a2)
static long probeGe(long a0, long a1, long a2)
static long mkBvshl(long a0, long a1, long a2)
Expr mkSetDel(Expr set, Expr element)
static long mkFalse(long a0)
static long mkBvsrem(long a0, long a1, long a2)
BitVecExpr mkBVAND(BitVecExpr t1, BitVecExpr t2)
BoolExpr mkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
static long mkEmptySet(long a0, long a1)
Expr mkBound(int index, Sort ty)
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
static String getTacticName(long a0, int a1)
BitVecExpr mkBVConst(Symbol name, int size)
static long tacticTryFor(long a0, long a1, int a2)
static long mkArrayDefault(long a0, long a1)
static long mkBvnegNoOverflow(long a0, long a1)
static long mkBound(long a0, int a1, long a2)
static long mkTrue(long a0)
Tactic mkTactic(String name)
static long mkMul(long a0, int a1, long[] a2)
static long mkReal(long a0, int a1, int a2)
static long tacticAndThen(long a0, long a1, long a2)
ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
BitVecSort mkBitVecSort(int size)
ParamDescrs getSimplifyParameterDescriptions()
Fixedpoint mkFixedpoint()
static long mkBvxnor(long a0, long a1, long a2)
BoolExpr[] getSMTLIBFormulas()
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)
Solver mkSolver(Symbol logic)
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)
static long getSmtlibFormula(long a0, int a1)
ArraySort mkArraySort(Sort domain, Sort range)
Expr mkConst(Symbol name, Sort range)
BitVecNum mkBV(int v, int size)
static long mkBv2int(long a0, long a1, boolean a2)
BoolExpr mkNot(BoolExpr a)
Expr mkNumeral(long v, Sort ty)
DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
BoolExpr mkGt(ArithExpr t1, ArithExpr t2)
ListSort mkListSort(Symbol name, Sort elemSort)
Tactic orElse(Tactic t1, Tactic t2)
Probe le(Probe p1, Probe p2)
ArithExpr mkUnaryMinus(ArithExpr t)
EnumSort mkEnumSort(Symbol name, Symbol...enumNames)
static long probeAnd(long a0, long a1, long a2)
RealExpr mkInt2Real(IntExpr t)
RealExpr mkRealConst(Symbol name)
static long mkBvmul(long a0, long a1, long a2)
Expr mkSetSubset(Expr arg1, Expr arg2)
FuncDecl mkFreshConstDecl(String prefix, Sort range)
Quantifier mkQuantifier(boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
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 mkReal2int(long a0, long a1)
FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
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)
BitVecExpr mkConcat(BitVecExpr t1, BitVecExpr t2)
RatNum mkReal(int num, int den)
BitVecExpr mkSignExt(int i, BitVecExpr t)
BoolExpr mkBVUGT(BitVecExpr t1, BitVecExpr t2)
Expr mkEmptySet(Sort domain)
IntExpr mkBV2Int(BitVecExpr t, boolean signed)
static long mkIsInt(long a0, long a1)
Pattern mkPattern(Expr...terms)
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 mkBvsubNoOverflow(long a0, long a1, long a2)
static long mkIff(long a0, long a1, long a2)
BoolExpr mkGe(ArithExpr t1, ArithExpr t2)
FuncDecl[] getSMTLIBDecls()
Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
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)
BoolExpr mkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, boolean isSigned)
static long mkBvnor(long a0, long a1, long a2)