The InterpolationContext is suitable for generation of interpolants. More...
Public Member Functions | |
InterpolationContext () throws Z3Exception | |
InterpolationContext (Map< String, String > settings) throws Z3Exception | |
BoolExpr | MkInterpolant (BoolExpr a) throws Z3Exception |
String | InterpolationProfile () throws Z3Exception |
Return a string summarizing cumulative time used for interpolation. More... | |
int | CheckInterpolant (Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception |
Checks the correctness of an interpolant. More... | |
int | ReadInterpolationProblem (String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception |
Reads an interpolation problem from a file. More... | |
void | WriteInterpolationProblem (String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception |
Writes an interpolation problem to a file. More... | |
![]() | |
Context () throws Z3Exception | |
Context (Map< String, String > settings) throws Z3Exception | |
IntSymbol | mkSymbol (int i) throws Z3Exception |
StringSymbol | mkSymbol (String name) throws Z3Exception |
BoolSort | getBoolSort () throws Z3Exception |
IntSort | getIntSort () throws Z3Exception |
RealSort | getRealSort () throws Z3Exception |
BoolSort | mkBoolSort () throws Z3Exception |
UninterpretedSort | mkUninterpretedSort (Symbol s) throws Z3Exception |
UninterpretedSort | mkUninterpretedSort (String str) throws Z3Exception |
IntSort | mkIntSort () throws Z3Exception |
RealSort | mkRealSort () throws Z3Exception |
BitVecSort | mkBitVecSort (int size) throws Z3Exception |
ArraySort | mkArraySort (Sort domain, Sort range) throws Z3Exception |
TupleSort | mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts) throws Z3Exception |
EnumSort | mkEnumSort (Symbol name, Symbol...enumNames) throws Z3Exception |
EnumSort | mkEnumSort (String name, String...enumNames) throws Z3Exception |
ListSort | mkListSort (Symbol name, Sort elemSort) throws Z3Exception |
ListSort | mkListSort (String name, Sort elemSort) throws Z3Exception |
FiniteDomainSort | mkFiniteDomainSort (Symbol name, long size) throws Z3Exception |
FiniteDomainSort | mkFiniteDomainSort (String name, long size) throws Z3Exception |
Constructor | mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception |
Constructor | mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception |
DatatypeSort | mkDatatypeSort (Symbol name, Constructor[] constructors) throws Z3Exception |
DatatypeSort | mkDatatypeSort (String name, Constructor[] constructors) throws Z3Exception |
DatatypeSort[] | mkDatatypeSorts (Symbol[] names, Constructor[][] c) throws Z3Exception |
DatatypeSort[] | mkDatatypeSorts (String[] names, Constructor[][] c) throws Z3Exception |
FuncDecl | mkFuncDecl (Symbol name, Sort[] domain, Sort range) throws Z3Exception |
FuncDecl | mkFuncDecl (Symbol name, Sort domain, Sort range) throws Z3Exception |
FuncDecl | mkFuncDecl (String name, Sort[] domain, Sort range) throws Z3Exception |
FuncDecl | mkFuncDecl (String name, Sort domain, Sort range) throws Z3Exception |
FuncDecl | mkFreshFuncDecl (String prefix, Sort[] domain, Sort range) throws Z3Exception |
FuncDecl | mkConstDecl (Symbol name, Sort range) throws Z3Exception |
FuncDecl | mkConstDecl (String name, Sort range) throws Z3Exception |
FuncDecl | mkFreshConstDecl (String prefix, Sort range) throws Z3Exception |
Expr | mkBound (int index, Sort ty) throws Z3Exception |
Pattern | mkPattern (Expr...terms) throws Z3Exception |
Expr | mkConst (Symbol name, Sort range) throws Z3Exception |
Expr | mkConst (String name, Sort range) throws Z3Exception |
Expr | mkFreshConst (String prefix, Sort range) throws Z3Exception |
Expr | mkConst (FuncDecl f) throws Z3Exception |
BoolExpr | mkBoolConst (Symbol name) throws Z3Exception |
BoolExpr | mkBoolConst (String name) throws Z3Exception |
IntExpr | mkIntConst (Symbol name) throws Z3Exception |
IntExpr | mkIntConst (String name) throws Z3Exception |
RealExpr | mkRealConst (Symbol name) throws Z3Exception |
RealExpr | mkRealConst (String name) throws Z3Exception |
BitVecExpr | mkBVConst (Symbol name, int size) throws Z3Exception |
BitVecExpr | mkBVConst (String name, int size) throws Z3Exception |
Expr | mkApp (FuncDecl f, Expr...args) throws Z3Exception |
BoolExpr | mkTrue () throws Z3Exception |
BoolExpr | mkFalse () throws Z3Exception |
BoolExpr | mkBool (boolean value) throws Z3Exception |
BoolExpr | mkEq (Expr x, Expr y) throws Z3Exception |
BoolExpr | mkDistinct (Expr...args) throws Z3Exception |
BoolExpr | mkNot (BoolExpr a) throws Z3Exception |
Expr | mkITE (BoolExpr t1, Expr t2, Expr t3) throws Z3Exception |
BoolExpr | mkIff (BoolExpr t1, BoolExpr t2) throws Z3Exception |
BoolExpr | mkImplies (BoolExpr t1, BoolExpr t2) throws Z3Exception |
BoolExpr | mkXor (BoolExpr t1, BoolExpr t2) throws Z3Exception |
BoolExpr | mkAnd (BoolExpr...t) throws Z3Exception |
BoolExpr | mkOr (BoolExpr...t) throws Z3Exception |
ArithExpr | mkAdd (ArithExpr...t) throws Z3Exception |
ArithExpr | mkMul (ArithExpr...t) throws Z3Exception |
ArithExpr | mkSub (ArithExpr...t) throws Z3Exception |
ArithExpr | mkUnaryMinus (ArithExpr t) throws Z3Exception |
ArithExpr | mkDiv (ArithExpr t1, ArithExpr t2) throws Z3Exception |
IntExpr | mkMod (IntExpr t1, IntExpr t2) throws Z3Exception |
IntExpr | mkRem (IntExpr t1, IntExpr t2) throws Z3Exception |
ArithExpr | mkPower (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkLt (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkLe (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkGt (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkGe (ArithExpr t1, ArithExpr t2) throws Z3Exception |
RealExpr | mkInt2Real (IntExpr t) throws Z3Exception |
IntExpr | mkReal2Int (RealExpr t) throws Z3Exception |
BoolExpr | mkIsInteger (RealExpr t) throws Z3Exception |
BitVecExpr | mkBVNot (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRedAND (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRedOR (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVAND (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVXOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVNAND (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVNOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVXNOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVNeg (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVAdd (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSub (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVMul (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVUDiv (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSDiv (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVURem (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSRem (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSMod (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVULT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSLT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVULE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSLE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVUGE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSGE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVUGT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSGT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkConcat (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkExtract (int high, int low, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkSignExt (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkZeroExt (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkRepeat (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVSHL (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVLSHR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVASHR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVRotateLeft (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRotateRight (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVRotateRight (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkInt2BV (int n, IntExpr t) throws Z3Exception |
IntExpr | mkBV2Int (BitVecExpr t, boolean signed) throws Z3Exception |
BoolExpr | mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception |
BoolExpr | mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception |
BoolExpr | mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVNegNoOverflow (BitVecExpr t) throws Z3Exception |
BoolExpr | mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception |
BoolExpr | mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
ArrayExpr | mkArrayConst (Symbol name, Sort domain, Sort range) throws Z3Exception |
ArrayExpr | mkArrayConst (String name, Sort domain, Sort range) throws Z3Exception |
Expr | mkSelect (ArrayExpr a, Expr i) throws Z3Exception |
ArrayExpr | mkStore (ArrayExpr a, Expr i, Expr v) throws Z3Exception |
ArrayExpr | mkConstArray (Sort domain, Expr v) throws Z3Exception |
ArrayExpr | mkMap (FuncDecl f, ArrayExpr...args) throws Z3Exception |
Expr | mkTermArray (ArrayExpr array) throws Z3Exception |
SetSort | mkSetSort (Sort ty) throws Z3Exception |
Expr | mkEmptySet (Sort domain) throws Z3Exception |
Expr | mkFullSet (Sort domain) throws Z3Exception |
Expr | mkSetAdd (Expr set, Expr element) throws Z3Exception |
Expr | mkSetDel (Expr set, Expr element) throws Z3Exception |
Expr | mkSetUnion (Expr...args) throws Z3Exception |
Expr | mkSetIntersection (Expr...args) throws Z3Exception |
Expr | mkSetDifference (Expr arg1, Expr arg2) throws Z3Exception |
Expr | mkSetComplement (Expr arg) throws Z3Exception |
Expr | mkSetMembership (Expr elem, Expr set) throws Z3Exception |
Expr | mkSetSubset (Expr arg1, Expr arg2) throws Z3Exception |
Expr | mkNumeral (String v, Sort ty) throws Z3Exception |
Expr | mkNumeral (int v, Sort ty) throws Z3Exception |
Expr | mkNumeral (long v, Sort ty) throws Z3Exception |
RatNum | mkReal (int num, int den) throws Z3Exception |
RatNum | mkReal (String v) throws Z3Exception |
RatNum | mkReal (int v) throws Z3Exception |
RatNum | mkReal (long v) throws Z3Exception |
IntNum | mkInt (String v) throws Z3Exception |
IntNum | mkInt (int v) throws Z3Exception |
IntNum | mkInt (long v) throws Z3Exception |
BitVecNum | mkBV (String v, int size) throws Z3Exception |
BitVecNum | mkBV (int v, int size) throws Z3Exception |
BitVecNum | mkBV (long v, int size) throws Z3Exception |
Quantifier | mkForall (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkForall (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkExists (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkExists (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkQuantifier (boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
void | setPrintMode (Z3_ast_print_mode value) throws Z3Exception |
String | benchmarkToSMTString (String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula) throws Z3Exception |
void | parseSMTLIBString (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
void | parseSMTLIBFile (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
int | getNumSMTLIBFormulas () throws Z3Exception |
BoolExpr[] | getSMTLIBFormulas () throws Z3Exception |
int | getNumSMTLIBAssumptions () throws Z3Exception |
BoolExpr[] | getSMTLIBAssumptions () throws Z3Exception |
int | getNumSMTLIBDecls () throws Z3Exception |
FuncDecl[] | getSMTLIBDecls () throws Z3Exception |
int | getNumSMTLIBSorts () throws Z3Exception |
Sort[] | getSMTLIBSorts () throws Z3Exception |
BoolExpr | parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
BoolExpr | parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
Goal | mkGoal (boolean models, boolean unsatCores, boolean proofs) throws Z3Exception |
Params | mkParams () throws Z3Exception |
int | getNumTactics () throws Z3Exception |
String[] | getTacticNames () throws Z3Exception |
String | getTacticDescription (String name) throws Z3Exception |
Tactic | mkTactic (String name) throws Z3Exception |
Tactic | andThen (Tactic t1, Tactic t2, Tactic...ts) throws Z3Exception |
Tactic | then (Tactic t1, Tactic t2, Tactic...ts) throws Z3Exception |
Tactic | orElse (Tactic t1, Tactic t2) throws Z3Exception |
Tactic | tryFor (Tactic t, int ms) throws Z3Exception |
Tactic | when (Probe p, Tactic t) throws Z3Exception |
Tactic | cond (Probe p, Tactic t1, Tactic t2) throws Z3Exception |
Tactic | repeat (Tactic t, int max) throws Z3Exception |
Tactic | skip () throws Z3Exception |
Tactic | fail () throws Z3Exception |
Tactic | failIf (Probe p) throws Z3Exception |
Tactic | failIfNotDecided () throws Z3Exception |
Tactic | usingParams (Tactic t, Params p) throws Z3Exception |
Tactic | with (Tactic t, Params p) throws Z3Exception |
Tactic | parOr (Tactic...t) throws Z3Exception |
Tactic | parAndThen (Tactic t1, Tactic t2) throws Z3Exception |
void | interrupt () throws Z3Exception |
int | getNumProbes () throws Z3Exception |
String[] | getProbeNames () throws Z3Exception |
String | getProbeDescription (String name) throws Z3Exception |
Probe | mkProbe (String name) throws Z3Exception |
Probe | constProbe (double val) throws Z3Exception |
Probe | lt (Probe p1, Probe p2) throws Z3Exception |
Probe | gt (Probe p1, Probe p2) throws Z3Exception |
Probe | le (Probe p1, Probe p2) throws Z3Exception |
Probe | ge (Probe p1, Probe p2) throws Z3Exception |
Probe | eq (Probe p1, Probe p2) throws Z3Exception |
Probe | and (Probe p1, Probe p2) throws Z3Exception |
Probe | or (Probe p1, Probe p2) throws Z3Exception |
Probe | not (Probe p) throws Z3Exception |
Solver | mkSolver () throws Z3Exception |
Solver | mkSolver (Symbol logic) throws Z3Exception |
Solver | mkSolver (String logic) throws Z3Exception |
Solver | mkSimpleSolver () throws Z3Exception |
Solver | mkSolver (Tactic t) throws Z3Exception |
Fixedpoint | mkFixedpoint () throws Z3Exception |
AST | wrapAST (long nativeObject) throws Z3Exception |
long | unwrapAST (AST a) |
String | SimplifyHelp () throws Z3Exception |
ParamDescrs | getSimplifyParameterDescriptions () throws Z3Exception |
void | updateParamValue (String id, String value) throws Z3Exception |
void | dispose () |
![]() | |
void | dispose () throws Z3Exception |
Additional Inherited Members | |
![]() | |
static void | ToggleWarningMessages (boolean enabled) throws Z3Exception |
![]() | |
void | finalize () |
![]() | |
long | m_refCount = 0 |
The InterpolationContext is suitable for generation of interpolants.
For more information on interpolation please refer too the C/C++ API, which is well documented.
Definition at line 33 of file InterpolationContext.java.
|
inline |
Definition at line 38 of file InterpolationContext.java.
|
inline |
Definition at line 49 of file InterpolationContext.java.
|
inline |
Checks the correctness of an interpolant.
For more information on interpolation please refer too the function Z3_check_interpolant in the C/C++ API, which is well documented.
Definition at line 127 of file InterpolationContext.java.
|
inline |
Return a string summarizing cumulative time used for interpolation.
For more information on interpolation please refer too the function Z3_interpolation_profile in the C/C++ API, which is well documented.
Definition at line 116 of file InterpolationContext.java.
|
inline |
Create an expression that marks a formula position for interpolation.
Z3Exception |
Definition at line 63 of file InterpolationContext.java.
|
inline |
Reads an interpolation problem from a file.
For more information on interpolation please refer too the function Z3_read_interpolation_problem in the C/C++ API, which is well documented.
Definition at line 148 of file InterpolationContext.java.
|
inline |
Writes an interpolation problem to a file.
For more information on interpolation please refer too the function Z3_write_interpolation_problem in the C/C++ API, which is well documented.
Definition at line 179 of file InterpolationContext.java.