InterpolationContext Class Reference

The InterpolationContext is suitable for generation of interpolants. More...

Inheritance diagram for InterpolationContext:

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...
Public Member Functions inherited from Context
	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 ()
Public Member Functions inherited from IDisposable
void	dispose () throws Z3Exception

Additional Inherited Members
Static Public Member Functions inherited from Context
static void	ToggleWarningMessages (boolean enabled) throws Z3Exception
Protected Member Functions inherited from Context
void	finalize ()
Protected Attributes inherited from Context
long	m_refCount = 0

Detailed Description

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.

Constructor & Destructor Documentation

InterpolationContext ( ) throws Z3Exception

inline

Constructor.

Definition at line 38 of file InterpolationContext.java.

    {
        m_ctx = Native.mkInterpolationContext(0);
        initContext(); 
    }

InterpolationContext ( Map< String, String >  settings ) throws Z3Exception

inline

Constructor.

See also

Context.Context(Dictionary<string, string>)

Definition at line 49 of file InterpolationContext.java.

    { 
        long cfg = Native.mkConfig();
        for (Map.Entry<String, String> kv : settings.entrySet())
            Native.setParamValue(cfg, kv.getKey(), kv.getValue());
        m_ctx = Native.mkInterpolationContext(cfg);
        Native.delConfig(cfg);
        initContext();
    }

Member Function Documentation

int CheckInterpolant ( Expr[]  cnsts, int[]  parents, Expr[]  interps, String  error, Expr[]  theory  ) throws Z3Exception

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.

    {
        Native.StringPtr n_err_str = new Native.StringPtr();
        int r = Native.checkInterpolant(nCtx(),
                                        cnsts.length,
                                        Expr.arrayToNative(cnsts),
                                        parents,
                                        Expr.arrayToNative(interps),
                                        n_err_str,
                                        theory.length,
                                        Expr.arrayToNative(theory));
        error = n_err_str.value;
        return r;
    }

String InterpolationProfile ( ) throws Z3Exception

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.

    {
        return Native.interpolationProfile(nCtx());
    }

BoolExpr MkInterpolant ( BoolExpr  a ) throws Z3Exception

inline

Create an expression that marks a formula position for interpolation.

Exceptions

Z3Exception

Definition at line 63 of file InterpolationContext.java.

    {
        checkContextMatch(a);        
        return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject()));
    }

int ReadInterpolationProblem ( String  filename, Expr[]  cnsts, int[]  parents, String  error, Expr[]  theory  ) throws Z3Exception

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.

    {
        Native.IntPtr n_num = new Native.IntPtr();
        Native.IntPtr n_num_theory = new Native.IntPtr();
        Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
        Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
        Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
        Native.StringPtr n_err_str = new Native.StringPtr();
        int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
        int num = n_num.value;
        int num_theory = n_num_theory.value;
        error = n_err_str.value;
        cnsts = new Expr[num];
        parents = new int[num];
        theory = new Expr[num_theory];
        for (int i = 0; i < num; i++)
        {
            cnsts[i] = Expr.create(this, n_cnsts.value[i]);
            parents[i] = n_parents.value[i];
        }
        for (int i = 0; i < num_theory; i++)
            theory[i] = Expr.create(this, n_theory.value[i]);
        return r;
    }

void WriteInterpolationProblem ( String  filename, Expr[]  cnsts, int[]  parents, String  error, Expr[]  theory  ) throws Z3Exception

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.

    {
        Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));     
    }