mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Java API: Removed auto-generated files.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
11ffbab0bd
commit
c1bd6cb2fa
|
|
@ -1,498 +0,0 @@
|
|||
// Automatically generated file
|
||||
package com.Microsoft.Z3;
|
||||
public final class Native {
|
||||
public static class IntPtr { public int value; }
|
||||
public static class LongPtr { public long value; }
|
||||
public static class StringPtr { public String value; }
|
||||
public static class errorHandler { public long ptr; }
|
||||
static { System.loadLibrary("<mk_util.JavaDLLComponent instance at 0x026CDA08>"); }
|
||||
public static native long mkConfig();
|
||||
public static native void delConfig(long a0);
|
||||
public static native void setParamValue(long a0, String a1, String a2);
|
||||
public static native long mkContext(long a0);
|
||||
public static native long mkContextRc(long a0);
|
||||
public static native void delContext(long a0);
|
||||
public static native void incRef(long a0, long a1);
|
||||
public static native void decRef(long a0, long a1);
|
||||
public static native void updateParamValue(long a0, String a1, String a2);
|
||||
public static native boolean getParamValue(long a0, String a1, StringPtr a2);
|
||||
public static native void interrupt(long a0);
|
||||
public static native long mkParams(long a0);
|
||||
public static native void paramsIncRef(long a0, long a1);
|
||||
public static native void paramsDecRef(long a0, long a1);
|
||||
public static native void paramsSetBool(long a0, long a1, long a2, boolean a3);
|
||||
public static native void paramsSetUint(long a0, long a1, long a2, int a3);
|
||||
public static native void paramsSetDouble(long a0, long a1, long a2, double a3);
|
||||
public static native void paramsSetSymbol(long a0, long a1, long a2, long a3);
|
||||
public static native String paramsToString(long a0, long a1);
|
||||
public static native void paramsValidate(long a0, long a1, long a2);
|
||||
public static native void paramDescrsIncRef(long a0, long a1);
|
||||
public static native void paramDescrsDecRef(long a0, long a1);
|
||||
public static native int paramDescrsGetKind(long a0, long a1, long a2);
|
||||
public static native int paramDescrsSize(long a0, long a1);
|
||||
public static native long paramDescrsGetName(long a0, long a1, int a2);
|
||||
public static native String paramDescrsToString(long a0, long a1);
|
||||
public static native long mkIntSymbol(long a0, int a1);
|
||||
public static native long mkStringSymbol(long a0, String a1);
|
||||
public static native long mkUninterpretedSort(long a0, long a1);
|
||||
public static native long mkBoolSort(long a0);
|
||||
public static native long mkIntSort(long a0);
|
||||
public static native long mkRealSort(long a0);
|
||||
public static native long mkBvSort(long a0, int a1);
|
||||
public static native long mkFiniteDomainSort(long a0, long a1, long a2);
|
||||
public static native long mkArraySort(long a0, long a1, long a2);
|
||||
public static native long mkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6);
|
||||
public static native long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5);
|
||||
public static native long mkListSort(long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8);
|
||||
public static native long mkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6);
|
||||
public static native void delConstructor(long a0, long a1);
|
||||
public static native long mkDatatype(long a0, long a1, int a2, long[] a3);
|
||||
public static native long mkConstructorList(long a0, int a1, long[] a2);
|
||||
public static native void delConstructorList(long a0, long a1);
|
||||
public static native void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4);
|
||||
public static native void queryConstructor(long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5);
|
||||
public static native long mkFuncDecl(long a0, long a1, int a2, long[] a3, long a4);
|
||||
public static native long mkApp(long a0, long a1, int a2, long[] a3);
|
||||
public static native long mkConst(long a0, long a1, long a2);
|
||||
public static native long mkFreshFuncDecl(long a0, String a1, int a2, long[] a3, long a4);
|
||||
public static native long mkFreshConst(long a0, String a1, long a2);
|
||||
public static native long mkTrue(long a0);
|
||||
public static native long mkFalse(long a0);
|
||||
public static native long mkEq(long a0, long a1, long a2);
|
||||
public static native long mkDistinct(long a0, int a1, long[] a2);
|
||||
public static native long mkNot(long a0, long a1);
|
||||
public static native long mkIte(long a0, long a1, long a2, long a3);
|
||||
public static native long mkIff(long a0, long a1, long a2);
|
||||
public static native long mkImplies(long a0, long a1, long a2);
|
||||
public static native long mkXor(long a0, long a1, long a2);
|
||||
public static native long mkAnd(long a0, int a1, long[] a2);
|
||||
public static native long mkOr(long a0, int a1, long[] a2);
|
||||
public static native long mkAdd(long a0, int a1, long[] a2);
|
||||
public static native long mkMul(long a0, int a1, long[] a2);
|
||||
public static native long mkSub(long a0, int a1, long[] a2);
|
||||
public static native long mkUnaryMinus(long a0, long a1);
|
||||
public static native long mkDiv(long a0, long a1, long a2);
|
||||
public static native long mkMod(long a0, long a1, long a2);
|
||||
public static native long mkRem(long a0, long a1, long a2);
|
||||
public static native long mkPower(long a0, long a1, long a2);
|
||||
public static native long mkLt(long a0, long a1, long a2);
|
||||
public static native long mkLe(long a0, long a1, long a2);
|
||||
public static native long mkGt(long a0, long a1, long a2);
|
||||
public static native long mkGe(long a0, long a1, long a2);
|
||||
public static native long mkInt2real(long a0, long a1);
|
||||
public static native long mkReal2int(long a0, long a1);
|
||||
public static native long mkIsInt(long a0, long a1);
|
||||
public static native long mkBvnot(long a0, long a1);
|
||||
public static native long mkBvredand(long a0, long a1);
|
||||
public static native long mkBvredor(long a0, long a1);
|
||||
public static native long mkBvand(long a0, long a1, long a2);
|
||||
public static native long mkBvor(long a0, long a1, long a2);
|
||||
public static native long mkBvxor(long a0, long a1, long a2);
|
||||
public static native long mkBvnand(long a0, long a1, long a2);
|
||||
public static native long mkBvnor(long a0, long a1, long a2);
|
||||
public static native long mkBvxnor(long a0, long a1, long a2);
|
||||
public static native long mkBvneg(long a0, long a1);
|
||||
public static native long mkBvadd(long a0, long a1, long a2);
|
||||
public static native long mkBvsub(long a0, long a1, long a2);
|
||||
public static native long mkBvmul(long a0, long a1, long a2);
|
||||
public static native long mkBvudiv(long a0, long a1, long a2);
|
||||
public static native long mkBvsdiv(long a0, long a1, long a2);
|
||||
public static native long mkBvurem(long a0, long a1, long a2);
|
||||
public static native long mkBvsrem(long a0, long a1, long a2);
|
||||
public static native long mkBvsmod(long a0, long a1, long a2);
|
||||
public static native long mkBvult(long a0, long a1, long a2);
|
||||
public static native long mkBvslt(long a0, long a1, long a2);
|
||||
public static native long mkBvule(long a0, long a1, long a2);
|
||||
public static native long mkBvsle(long a0, long a1, long a2);
|
||||
public static native long mkBvuge(long a0, long a1, long a2);
|
||||
public static native long mkBvsge(long a0, long a1, long a2);
|
||||
public static native long mkBvugt(long a0, long a1, long a2);
|
||||
public static native long mkBvsgt(long a0, long a1, long a2);
|
||||
public static native long mkConcat(long a0, long a1, long a2);
|
||||
public static native long mkExtract(long a0, int a1, int a2, long a3);
|
||||
public static native long mkSignExt(long a0, int a1, long a2);
|
||||
public static native long mkZeroExt(long a0, int a1, long a2);
|
||||
public static native long mkRepeat(long a0, int a1, long a2);
|
||||
public static native long mkBvshl(long a0, long a1, long a2);
|
||||
public static native long mkBvlshr(long a0, long a1, long a2);
|
||||
public static native long mkBvashr(long a0, long a1, long a2);
|
||||
public static native long mkRotateLeft(long a0, int a1, long a2);
|
||||
public static native long mkRotateRight(long a0, int a1, long a2);
|
||||
public static native long mkExtRotateLeft(long a0, long a1, long a2);
|
||||
public static native long mkExtRotateRight(long a0, long a1, long a2);
|
||||
public static native long mkInt2bv(long a0, int a1, long a2);
|
||||
public static native long mkBv2int(long a0, long a1, boolean a2);
|
||||
public static native long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3);
|
||||
public static native long mkBvaddNoUnderflow(long a0, long a1, long a2);
|
||||
public static native long mkBvsubNoOverflow(long a0, long a1, long a2);
|
||||
public static native long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3);
|
||||
public static native long mkBvsdivNoOverflow(long a0, long a1, long a2);
|
||||
public static native long mkBvnegNoOverflow(long a0, long a1);
|
||||
public static native long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3);
|
||||
public static native long mkBvmulNoUnderflow(long a0, long a1, long a2);
|
||||
public static native long mkSelect(long a0, long a1, long a2);
|
||||
public static native long mkStore(long a0, long a1, long a2, long a3);
|
||||
public static native long mkConstArray(long a0, long a1, long a2);
|
||||
public static native long mkMap(long a0, long a1, int a2, long[] a3);
|
||||
public static native long mkArrayDefault(long a0, long a1);
|
||||
public static native long mkSetSort(long a0, long a1);
|
||||
public static native long mkEmptySet(long a0, long a1);
|
||||
public static native long mkFullSet(long a0, long a1);
|
||||
public static native long mkSetAdd(long a0, long a1, long a2);
|
||||
public static native long mkSetDel(long a0, long a1, long a2);
|
||||
public static native long mkSetUnion(long a0, int a1, long[] a2);
|
||||
public static native long mkSetIntersect(long a0, int a1, long[] a2);
|
||||
public static native long mkSetDifference(long a0, long a1, long a2);
|
||||
public static native long mkSetComplement(long a0, long a1);
|
||||
public static native long mkSetMember(long a0, long a1, long a2);
|
||||
public static native long mkSetSubset(long a0, long a1, long a2);
|
||||
public static native long mkNumeral(long a0, String a1, long a2);
|
||||
public static native long mkReal(long a0, int a1, int a2);
|
||||
public static native long mkInt(long a0, int a1, long a2);
|
||||
public static native long mkUnsignedInt(long a0, int a1, long a2);
|
||||
public static native long mkInt64(long a0, long a1, long a2);
|
||||
public static native long mkUnsignedInt64(long a0, long a1, long a2);
|
||||
public static native long mkPattern(long a0, int a1, long[] a2);
|
||||
public static native long mkBound(long a0, int a1, long a2);
|
||||
public static native long mkForall(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7);
|
||||
public static native long mkExists(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7);
|
||||
public static native long mkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8);
|
||||
public static native long mkQuantifierEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long[] a11, long a12);
|
||||
public static native long mkForallConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6);
|
||||
public static native long mkExistsConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6);
|
||||
public static native long mkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7);
|
||||
public static native long mkQuantifierConstEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long a11);
|
||||
public static native int getSymbolKind(long a0, long a1);
|
||||
public static native int getSymbolInt(long a0, long a1);
|
||||
public static native String getSymbolString(long a0, long a1);
|
||||
public static native long getSortName(long a0, long a1);
|
||||
public static native int getSortId(long a0, long a1);
|
||||
public static native long sortToAst(long a0, long a1);
|
||||
public static native boolean isEqSort(long a0, long a1, long a2);
|
||||
public static native int getSortKind(long a0, long a1);
|
||||
public static native int getBvSortSize(long a0, long a1);
|
||||
public static native boolean getFiniteDomainSortSize(long a0, long a1, LongPtr a2);
|
||||
public static native long getArraySortDomain(long a0, long a1);
|
||||
public static native long getArraySortRange(long a0, long a1);
|
||||
public static native long getTupleSortMkDecl(long a0, long a1);
|
||||
public static native int getTupleSortNumFields(long a0, long a1);
|
||||
public static native long getTupleSortFieldDecl(long a0, long a1, int a2);
|
||||
public static native int getDatatypeSortNumConstructors(long a0, long a1);
|
||||
public static native long getDatatypeSortConstructor(long a0, long a1, int a2);
|
||||
public static native long getDatatypeSortRecognizer(long a0, long a1, int a2);
|
||||
public static native long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3);
|
||||
public static native int getRelationArity(long a0, long a1);
|
||||
public static native long getRelationColumn(long a0, long a1, int a2);
|
||||
public static native long funcDeclToAst(long a0, long a1);
|
||||
public static native boolean isEqFuncDecl(long a0, long a1, long a2);
|
||||
public static native int getFuncDeclId(long a0, long a1);
|
||||
public static native long getDeclName(long a0, long a1);
|
||||
public static native int getDeclKind(long a0, long a1);
|
||||
public static native int getDomainSize(long a0, long a1);
|
||||
public static native int getArity(long a0, long a1);
|
||||
public static native long getDomain(long a0, long a1, int a2);
|
||||
public static native long getRange(long a0, long a1);
|
||||
public static native int getDeclNumParameters(long a0, long a1);
|
||||
public static native int getDeclParameterKind(long a0, long a1, int a2);
|
||||
public static native int getDeclIntParameter(long a0, long a1, int a2);
|
||||
public static native double getDeclDoubleParameter(long a0, long a1, int a2);
|
||||
public static native long getDeclSymbolParameter(long a0, long a1, int a2);
|
||||
public static native long getDeclSortParameter(long a0, long a1, int a2);
|
||||
public static native long getDeclAstParameter(long a0, long a1, int a2);
|
||||
public static native long getDeclFuncDeclParameter(long a0, long a1, int a2);
|
||||
public static native String getDeclRationalParameter(long a0, long a1, int a2);
|
||||
public static native long appToAst(long a0, long a1);
|
||||
public static native long getAppDecl(long a0, long a1);
|
||||
public static native int getAppNumArgs(long a0, long a1);
|
||||
public static native long getAppArg(long a0, long a1, int a2);
|
||||
public static native boolean isEqAst(long a0, long a1, long a2);
|
||||
public static native int getAstId(long a0, long a1);
|
||||
public static native int getAstHash(long a0, long a1);
|
||||
public static native long getSort(long a0, long a1);
|
||||
public static native boolean isWellSorted(long a0, long a1);
|
||||
public static native int getBoolValue(long a0, long a1);
|
||||
public static native int getAstKind(long a0, long a1);
|
||||
public static native boolean isApp(long a0, long a1);
|
||||
public static native boolean isNumeralAst(long a0, long a1);
|
||||
public static native boolean isAlgebraicNumber(long a0, long a1);
|
||||
public static native long toApp(long a0, long a1);
|
||||
public static native long toFuncDecl(long a0, long a1);
|
||||
public static native String getNumeralString(long a0, long a1);
|
||||
public static native String getNumeralDecimalString(long a0, long a1, int a2);
|
||||
public static native long getNumerator(long a0, long a1);
|
||||
public static native long getDenominator(long a0, long a1);
|
||||
public static native boolean getNumeralSmall(long a0, long a1, LongPtr a2, LongPtr a3);
|
||||
public static native boolean getNumeralInt(long a0, long a1, IntPtr a2);
|
||||
public static native boolean getNumeralUint(long a0, long a1, IntPtr a2);
|
||||
public static native boolean getNumeralUint64(long a0, long a1, LongPtr a2);
|
||||
public static native boolean getNumeralInt64(long a0, long a1, LongPtr a2);
|
||||
public static native boolean getNumeralRationalInt64(long a0, long a1, LongPtr a2, LongPtr a3);
|
||||
public static native long getAlgebraicNumberLower(long a0, long a1, int a2);
|
||||
public static native long getAlgebraicNumberUpper(long a0, long a1, int a2);
|
||||
public static native long patternToAst(long a0, long a1);
|
||||
public static native int getPatternNumTerms(long a0, long a1);
|
||||
public static native long getPattern(long a0, long a1, int a2);
|
||||
public static native int getIndexValue(long a0, long a1);
|
||||
public static native boolean isQuantifierForall(long a0, long a1);
|
||||
public static native int getQuantifierWeight(long a0, long a1);
|
||||
public static native int getQuantifierNumPatterns(long a0, long a1);
|
||||
public static native long getQuantifierPatternAst(long a0, long a1, int a2);
|
||||
public static native int getQuantifierNumNoPatterns(long a0, long a1);
|
||||
public static native long getQuantifierNoPatternAst(long a0, long a1, int a2);
|
||||
public static native int getQuantifierNumBound(long a0, long a1);
|
||||
public static native long getQuantifierBoundName(long a0, long a1, int a2);
|
||||
public static native long getQuantifierBoundSort(long a0, long a1, int a2);
|
||||
public static native long getQuantifierBody(long a0, long a1);
|
||||
public static native long simplify(long a0, long a1);
|
||||
public static native long simplifyEx(long a0, long a1, long a2);
|
||||
public static native String simplifyGetHelp(long a0);
|
||||
public static native long simplifyGetParamDescrs(long a0);
|
||||
public static native long updateTerm(long a0, long a1, int a2, long[] a3);
|
||||
public static native long substitute(long a0, long a1, int a2, long[] a3, long[] a4);
|
||||
public static native long substituteVars(long a0, long a1, int a2, long[] a3);
|
||||
public static native long translate(long a0, long a1, long a2);
|
||||
public static native void modelIncRef(long a0, long a1);
|
||||
public static native void modelDecRef(long a0, long a1);
|
||||
public static native boolean modelEval(long a0, long a1, long a2, boolean a3, LongPtr a4);
|
||||
public static native long modelGetConstInterp(long a0, long a1, long a2);
|
||||
public static native long modelGetFuncInterp(long a0, long a1, long a2);
|
||||
public static native int modelGetNumConsts(long a0, long a1);
|
||||
public static native long modelGetConstDecl(long a0, long a1, int a2);
|
||||
public static native int modelGetNumFuncs(long a0, long a1);
|
||||
public static native long modelGetFuncDecl(long a0, long a1, int a2);
|
||||
public static native int modelGetNumSorts(long a0, long a1);
|
||||
public static native long modelGetSort(long a0, long a1, int a2);
|
||||
public static native long modelGetSortUniverse(long a0, long a1, long a2);
|
||||
public static native boolean isAsArray(long a0, long a1);
|
||||
public static native long getAsArrayFuncDecl(long a0, long a1);
|
||||
public static native void funcInterpIncRef(long a0, long a1);
|
||||
public static native void funcInterpDecRef(long a0, long a1);
|
||||
public static native int funcInterpGetNumEntries(long a0, long a1);
|
||||
public static native long funcInterpGetEntry(long a0, long a1, int a2);
|
||||
public static native long funcInterpGetElse(long a0, long a1);
|
||||
public static native int funcInterpGetArity(long a0, long a1);
|
||||
public static native void funcEntryIncRef(long a0, long a1);
|
||||
public static native void funcEntryDecRef(long a0, long a1);
|
||||
public static native long funcEntryGetValue(long a0, long a1);
|
||||
public static native int funcEntryGetNumArgs(long a0, long a1);
|
||||
public static native long funcEntryGetArg(long a0, long a1, int a2);
|
||||
public static native int openLog(String a0);
|
||||
public static native void appendLog(String a0);
|
||||
public static native void closeLog();
|
||||
public static native void toggleWarningMessages(boolean a0);
|
||||
public static native void setAstPrintMode(long a0, int a1);
|
||||
public static native String astToString(long a0, long a1);
|
||||
public static native String patternToString(long a0, long a1);
|
||||
public static native String sortToString(long a0, long a1);
|
||||
public static native String funcDeclToString(long a0, long a1);
|
||||
public static native String modelToString(long a0, long a1);
|
||||
public static native String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7);
|
||||
public static native long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
|
||||
public static native long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
|
||||
public static native void parseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
|
||||
public static native void parseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7);
|
||||
public static native int getSmtlibNumFormulas(long a0);
|
||||
public static native long getSmtlibFormula(long a0, int a1);
|
||||
public static native int getSmtlibNumAssumptions(long a0);
|
||||
public static native long getSmtlibAssumption(long a0, int a1);
|
||||
public static native int getSmtlibNumDecls(long a0);
|
||||
public static native long getSmtlibDecl(long a0, int a1);
|
||||
public static native int getSmtlibNumSorts(long a0);
|
||||
public static native long getSmtlibSort(long a0, int a1);
|
||||
public static native String getSmtlibError(long a0);
|
||||
public static native int getErrorCode(long a0);
|
||||
public static native void setError(long a0, int a1);
|
||||
public static native String getErrorMsg(int a0);
|
||||
public static native String getErrorMsgEx(long a0, int a1);
|
||||
public static native void getVersion(IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3);
|
||||
public static native void enableTrace(String a0);
|
||||
public static native void disableTrace(String a0);
|
||||
public static native void resetMemory();
|
||||
public static native long mkFixedpoint(long a0);
|
||||
public static native void fixedpointIncRef(long a0, long a1);
|
||||
public static native void fixedpointDecRef(long a0, long a1);
|
||||
public static native void fixedpointAddRule(long a0, long a1, long a2, long a3);
|
||||
public static native void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4);
|
||||
public static native void fixedpointAssert(long a0, long a1, long a2);
|
||||
public static native int fixedpointQuery(long a0, long a1, long a2);
|
||||
public static native int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3);
|
||||
public static native long fixedpointGetAnswer(long a0, long a1);
|
||||
public static native String fixedpointGetReasonUnknown(long a0, long a1);
|
||||
public static native void fixedpointUpdateRule(long a0, long a1, long a2, long a3);
|
||||
public static native int fixedpointGetNumLevels(long a0, long a1, long a2);
|
||||
public static native long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3);
|
||||
public static native void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4);
|
||||
public static native long fixedpointGetStatistics(long a0, long a1);
|
||||
public static native void fixedpointRegisterRelation(long a0, long a1, long a2);
|
||||
public static native void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4);
|
||||
public static native long fixedpointGetRules(long a0, long a1);
|
||||
public static native long fixedpointGetAssertions(long a0, long a1);
|
||||
public static native void fixedpointSetParams(long a0, long a1, long a2);
|
||||
public static native String fixedpointGetHelp(long a0, long a1);
|
||||
public static native long fixedpointGetParamDescrs(long a0, long a1);
|
||||
public static native String fixedpointToString(long a0, long a1, int a2, long[] a3);
|
||||
public static native long fixedpointFromString(long a0, long a1, String a2);
|
||||
public static native long fixedpointFromFile(long a0, long a1, String a2);
|
||||
public static native void fixedpointPush(long a0, long a1);
|
||||
public static native void fixedpointPop(long a0, long a1);
|
||||
public static native long mkAstVector(long a0);
|
||||
public static native void astVectorIncRef(long a0, long a1);
|
||||
public static native void astVectorDecRef(long a0, long a1);
|
||||
public static native int astVectorSize(long a0, long a1);
|
||||
public static native long astVectorGet(long a0, long a1, int a2);
|
||||
public static native void astVectorSet(long a0, long a1, int a2, long a3);
|
||||
public static native void astVectorResize(long a0, long a1, int a2);
|
||||
public static native void astVectorPush(long a0, long a1, long a2);
|
||||
public static native long astVectorTranslate(long a0, long a1, long a2);
|
||||
public static native String astVectorToString(long a0, long a1);
|
||||
public static native long mkAstMap(long a0);
|
||||
public static native void astMapIncRef(long a0, long a1);
|
||||
public static native void astMapDecRef(long a0, long a1);
|
||||
public static native boolean astMapContains(long a0, long a1, long a2);
|
||||
public static native long astMapFind(long a0, long a1, long a2);
|
||||
public static native void astMapInsert(long a0, long a1, long a2, long a3);
|
||||
public static native void astMapErase(long a0, long a1, long a2);
|
||||
public static native void astMapReset(long a0, long a1);
|
||||
public static native int astMapSize(long a0, long a1);
|
||||
public static native long astMapKeys(long a0, long a1);
|
||||
public static native String astMapToString(long a0, long a1);
|
||||
public static native long mkGoal(long a0, boolean a1, boolean a2, boolean a3);
|
||||
public static native void goalIncRef(long a0, long a1);
|
||||
public static native void goalDecRef(long a0, long a1);
|
||||
public static native int goalPrecision(long a0, long a1);
|
||||
public static native void goalAssert(long a0, long a1, long a2);
|
||||
public static native boolean goalInconsistent(long a0, long a1);
|
||||
public static native int goalDepth(long a0, long a1);
|
||||
public static native void goalReset(long a0, long a1);
|
||||
public static native int goalSize(long a0, long a1);
|
||||
public static native long goalFormula(long a0, long a1, int a2);
|
||||
public static native int goalNumExprs(long a0, long a1);
|
||||
public static native boolean goalIsDecidedSat(long a0, long a1);
|
||||
public static native boolean goalIsDecidedUnsat(long a0, long a1);
|
||||
public static native long goalTranslate(long a0, long a1, long a2);
|
||||
public static native String goalToString(long a0, long a1);
|
||||
public static native long mkTactic(long a0, String a1);
|
||||
public static native void tacticIncRef(long a0, long a1);
|
||||
public static native void tacticDecRef(long a0, long a1);
|
||||
public static native long mkProbe(long a0, String a1);
|
||||
public static native void probeIncRef(long a0, long a1);
|
||||
public static native void probeDecRef(long a0, long a1);
|
||||
public static native long tacticAndThen(long a0, long a1, long a2);
|
||||
public static native long tacticOrElse(long a0, long a1, long a2);
|
||||
public static native long tacticParOr(long a0, int a1, long[] a2);
|
||||
public static native long tacticParAndThen(long a0, long a1, long a2);
|
||||
public static native long tacticTryFor(long a0, long a1, int a2);
|
||||
public static native long tacticWhen(long a0, long a1, long a2);
|
||||
public static native long tacticCond(long a0, long a1, long a2, long a3);
|
||||
public static native long tacticRepeat(long a0, long a1, int a2);
|
||||
public static native long tacticSkip(long a0);
|
||||
public static native long tacticFail(long a0);
|
||||
public static native long tacticFailIf(long a0, long a1);
|
||||
public static native long tacticFailIfNotDecided(long a0);
|
||||
public static native long tacticUsingParams(long a0, long a1, long a2);
|
||||
public static native long probeConst(long a0, double a1);
|
||||
public static native long probeLt(long a0, long a1, long a2);
|
||||
public static native long probeGt(long a0, long a1, long a2);
|
||||
public static native long probeLe(long a0, long a1, long a2);
|
||||
public static native long probeGe(long a0, long a1, long a2);
|
||||
public static native long probeEq(long a0, long a1, long a2);
|
||||
public static native long probeAnd(long a0, long a1, long a2);
|
||||
public static native long probeOr(long a0, long a1, long a2);
|
||||
public static native long probeNot(long a0, long a1);
|
||||
public static native int getNumTactics(long a0);
|
||||
public static native String getTacticName(long a0, int a1);
|
||||
public static native int getNumProbes(long a0);
|
||||
public static native String getProbeName(long a0, int a1);
|
||||
public static native String tacticGetHelp(long a0, long a1);
|
||||
public static native long tacticGetParamDescrs(long a0, long a1);
|
||||
public static native String tacticGetDescr(long a0, String a1);
|
||||
public static native String probeGetDescr(long a0, String a1);
|
||||
public static native double probeApply(long a0, long a1, long a2);
|
||||
public static native long tacticApply(long a0, long a1, long a2);
|
||||
public static native long tacticApplyEx(long a0, long a1, long a2, long a3);
|
||||
public static native void applyResultIncRef(long a0, long a1);
|
||||
public static native void applyResultDecRef(long a0, long a1);
|
||||
public static native String applyResultToString(long a0, long a1);
|
||||
public static native int applyResultGetNumSubgoals(long a0, long a1);
|
||||
public static native long applyResultGetSubgoal(long a0, long a1, int a2);
|
||||
public static native long applyResultConvertModel(long a0, long a1, int a2, long a3);
|
||||
public static native long mkSolver(long a0);
|
||||
public static native long mkSimpleSolver(long a0);
|
||||
public static native long mkSolverForLogic(long a0, long a1);
|
||||
public static native long mkSolverFromTactic(long a0, long a1);
|
||||
public static native String solverGetHelp(long a0, long a1);
|
||||
public static native long solverGetParamDescrs(long a0, long a1);
|
||||
public static native void solverSetParams(long a0, long a1, long a2);
|
||||
public static native void solverIncRef(long a0, long a1);
|
||||
public static native void solverDecRef(long a0, long a1);
|
||||
public static native void solverPush(long a0, long a1);
|
||||
public static native void solverPop(long a0, long a1, int a2);
|
||||
public static native void solverReset(long a0, long a1);
|
||||
public static native int solverGetNumScopes(long a0, long a1);
|
||||
public static native void solverAssert(long a0, long a1, long a2);
|
||||
public static native void solverAssertAndTrack(long a0, long a1, long a2, long a3);
|
||||
public static native long solverGetAssertions(long a0, long a1);
|
||||
public static native int solverCheck(long a0, long a1);
|
||||
public static native int solverCheckAssumptions(long a0, long a1, int a2, long[] a3);
|
||||
public static native long solverGetModel(long a0, long a1);
|
||||
public static native long solverGetProof(long a0, long a1);
|
||||
public static native long solverGetUnsatCore(long a0, long a1);
|
||||
public static native String solverGetReasonUnknown(long a0, long a1);
|
||||
public static native long solverGetStatistics(long a0, long a1);
|
||||
public static native String solverToString(long a0, long a1);
|
||||
public static native String statsToString(long a0, long a1);
|
||||
public static native void statsIncRef(long a0, long a1);
|
||||
public static native void statsDecRef(long a0, long a1);
|
||||
public static native int statsSize(long a0, long a1);
|
||||
public static native String statsGetKey(long a0, long a1, int a2);
|
||||
public static native boolean statsIsUint(long a0, long a1, int a2);
|
||||
public static native boolean statsIsDouble(long a0, long a1, int a2);
|
||||
public static native int statsGetUintValue(long a0, long a1, int a2);
|
||||
public static native double statsGetDoubleValue(long a0, long a1, int a2);
|
||||
public static native long mkInjectiveFunction(long a0, long a1, int a2, long[] a3, long a4);
|
||||
public static native void setLogic(long a0, String a1);
|
||||
public static native void push(long a0);
|
||||
public static native void pop(long a0, int a1);
|
||||
public static native int getNumScopes(long a0);
|
||||
public static native void persistAst(long a0, long a1, int a2);
|
||||
public static native void assertCnstr(long a0, long a1);
|
||||
public static native int checkAndGetModel(long a0, LongPtr a1);
|
||||
public static native int check(long a0);
|
||||
public static native int checkAssumptions(long a0, int a1, long[] a2, LongPtr a3, LongPtr a4, IntPtr a5, long[] a6);
|
||||
public static native int getImpliedEqualities(long a0, int a1, long[] a2, int[] a3);
|
||||
public static native void delModel(long a0, long a1);
|
||||
public static native void softCheckCancel(long a0);
|
||||
public static native int getSearchFailure(long a0);
|
||||
public static native long mkLabel(long a0, long a1, boolean a2, long a3);
|
||||
public static native long getRelevantLabels(long a0);
|
||||
public static native long getRelevantLiterals(long a0);
|
||||
public static native long getGuessedLiterals(long a0);
|
||||
public static native void delLiterals(long a0, long a1);
|
||||
public static native int getNumLiterals(long a0, long a1);
|
||||
public static native long getLabelSymbol(long a0, long a1, int a2);
|
||||
public static native long getLiteral(long a0, long a1, int a2);
|
||||
public static native void disableLiteral(long a0, long a1, int a2);
|
||||
public static native void blockLiterals(long a0, long a1);
|
||||
public static native int getModelNumConstants(long a0, long a1);
|
||||
public static native long getModelConstant(long a0, long a1, int a2);
|
||||
public static native int getModelNumFuncs(long a0, long a1);
|
||||
public static native long getModelFuncDecl(long a0, long a1, int a2);
|
||||
public static native boolean evalFuncDecl(long a0, long a1, long a2, LongPtr a3);
|
||||
public static native boolean isArrayValue(long a0, long a1, long a2, IntPtr a3);
|
||||
public static native void getArrayValue(long a0, long a1, long a2, int a3, long[] a4, long[] a5, LongPtr a6);
|
||||
public static native long getModelFuncElse(long a0, long a1, int a2);
|
||||
public static native int getModelFuncNumEntries(long a0, long a1, int a2);
|
||||
public static native int getModelFuncEntryNumArgs(long a0, long a1, int a2, int a3);
|
||||
public static native long getModelFuncEntryArg(long a0, long a1, int a2, int a3, int a4);
|
||||
public static native long getModelFuncEntryValue(long a0, long a1, int a2, int a3);
|
||||
public static native boolean eval(long a0, long a1, long a2, LongPtr a3);
|
||||
public static native boolean evalDecl(long a0, long a1, long a2, int a3, long[] a4, LongPtr a5);
|
||||
public static native String contextToString(long a0);
|
||||
public static native String statisticsToString(long a0);
|
||||
public static native long getContextAssignment(long a0);
|
||||
public static void main(String[] args) {
|
||||
IntPtr major = new IntPtr(), minor = new IntPtr(), build = new IntPtr(), revision = new IntPtr();
|
||||
getVersion(major, minor, build, revision);
|
||||
System.out.format("Z3 (for Java) %d.%d.%d%n", major.value, minor.value, build.value);
|
||||
}
|
||||
}
|
||||
Loading…
Reference in a new issue