Inheritance diagram for InterpolationContext:

Data Structures
class	CheckInterpolantResult

class	ComputeInterpolantResult

class	ReadInterpolationProblemResult

Public Member Functions
BoolExpr	MkInterpolant (BoolExpr a)

BoolExpr []	GetInterpolant (Expr pf, Expr pat, Params p)

ComputeInterpolantResult	ComputeInterpolant (Expr pat, Params p)

String	InterpolationProfile ()

CheckInterpolantResult	CheckInterpolant (Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)

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

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

Public Member Functions inherited from Context
	Context ()

	Context (Map< String, String > settings)

IntSymbol	mkSymbol (int i)

StringSymbol	mkSymbol (String name)

BoolSort	getBoolSort ()

IntSort	getIntSort ()

RealSort	getRealSort ()

BoolSort	mkBoolSort ()

SeqSort	getStringSort ()

UninterpretedSort	mkUninterpretedSort (Symbol s)

UninterpretedSort	mkUninterpretedSort (String str)

IntSort	mkIntSort ()

RealSort	mkRealSort ()

BitVecSort	mkBitVecSort (int size)

ArraySort	mkArraySort (Sort domain, Sort range)

SeqSort	mkStringSort ()

SeqSort	mkSeqSort (Sort s)

ReSort	mkReSort (Sort s)

TupleSort	mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)

EnumSort	mkEnumSort (Symbol name, Symbol... enumNames)

EnumSort	mkEnumSort (String name, String... enumNames)

ListSort	mkListSort (Symbol name, Sort elemSort)

ListSort	mkListSort (String name, Sort elemSort)

FiniteDomainSort	mkFiniteDomainSort (Symbol name, long size)

FiniteDomainSort	mkFiniteDomainSort (String name, long size)

Constructor	mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)

Constructor	mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs)

DatatypeSort	mkDatatypeSort (Symbol name, Constructor[] constructors)

DatatypeSort	mkDatatypeSort (String name, Constructor[] constructors)

DatatypeSort []	mkDatatypeSorts (Symbol[] names, Constructor[][] c)

DatatypeSort []	mkDatatypeSorts (String[] names, Constructor[][] c)

Expr	MkUpdateField (FuncDecl field, Expr t, Expr v) throws Z3Exception

FuncDecl	mkFuncDecl (Symbol name, Sort[] domain, Sort range)

FuncDecl	mkFuncDecl (Symbol name, Sort domain, Sort range)

FuncDecl	mkFuncDecl (String name, Sort[] domain, Sort range)

FuncDecl	mkFuncDecl (String name, Sort domain, Sort range)

FuncDecl	mkFreshFuncDecl (String prefix, Sort[] domain, Sort range)

FuncDecl	mkConstDecl (Symbol name, Sort range)

FuncDecl	mkConstDecl (String name, Sort range)

FuncDecl	mkFreshConstDecl (String prefix, Sort range)

Expr	mkBound (int index, Sort ty)

Pattern	mkPattern (Expr... terms)

Expr	mkConst (Symbol name, Sort range)

Expr	mkConst (String name, Sort range)

Expr	mkFreshConst (String prefix, Sort range)

Expr	mkConst (FuncDecl f)

BoolExpr	mkBoolConst (Symbol name)

BoolExpr	mkBoolConst (String name)

IntExpr	mkIntConst (Symbol name)

IntExpr	mkIntConst (String name)

RealExpr	mkRealConst (Symbol name)

RealExpr	mkRealConst (String name)

BitVecExpr	mkBVConst (Symbol name, int size)

BitVecExpr	mkBVConst (String name, int size)

Expr	mkApp (FuncDecl f, Expr... args)

BoolExpr	mkTrue ()

BoolExpr	mkFalse ()

BoolExpr	mkBool (boolean value)

BoolExpr	mkEq (Expr x, Expr y)

BoolExpr	mkDistinct (Expr... args)

BoolExpr	mkNot (BoolExpr a)

Expr	mkITE (BoolExpr t1, Expr t2, Expr t3)

BoolExpr	mkIff (BoolExpr t1, BoolExpr t2)

BoolExpr	mkImplies (BoolExpr t1, BoolExpr t2)

BoolExpr	mkXor (BoolExpr t1, BoolExpr t2)

BoolExpr	mkAnd (BoolExpr... t)

BoolExpr	mkOr (BoolExpr... t)

ArithExpr	mkAdd (ArithExpr... t)

ArithExpr	mkMul (ArithExpr... t)

ArithExpr	mkSub (ArithExpr... t)

ArithExpr	mkUnaryMinus (ArithExpr t)

ArithExpr	mkDiv (ArithExpr t1, ArithExpr t2)

IntExpr	mkMod (IntExpr t1, IntExpr t2)

IntExpr	mkRem (IntExpr t1, IntExpr t2)

ArithExpr	mkPower (ArithExpr t1, ArithExpr t2)

BoolExpr	mkLt (ArithExpr t1, ArithExpr t2)

BoolExpr	mkLe (ArithExpr t1, ArithExpr t2)

BoolExpr	mkGt (ArithExpr t1, ArithExpr t2)

BoolExpr	mkGe (ArithExpr t1, ArithExpr t2)

RealExpr	mkInt2Real (IntExpr t)

IntExpr	mkReal2Int (RealExpr t)

BoolExpr	mkIsInteger (RealExpr t)

BitVecExpr	mkBVNot (BitVecExpr t)

BitVecExpr	mkBVRedAND (BitVecExpr t)

BitVecExpr	mkBVRedOR (BitVecExpr t)

BitVecExpr	mkBVAND (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVOR (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVXOR (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVNAND (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVNOR (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVXNOR (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVNeg (BitVecExpr t)

BitVecExpr	mkBVAdd (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVSub (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVMul (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVUDiv (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVSDiv (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVURem (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVSRem (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVSMod (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVULT (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVSLT (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVULE (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVSLE (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVUGE (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVSGE (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVUGT (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVSGT (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkConcat (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkExtract (int high, int low, BitVecExpr t)

BitVecExpr	mkSignExt (int i, BitVecExpr t)

BitVecExpr	mkZeroExt (int i, BitVecExpr t)

BitVecExpr	mkRepeat (int i, BitVecExpr t)

BitVecExpr	mkBVSHL (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVLSHR (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVASHR (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVRotateLeft (int i, BitVecExpr t)

BitVecExpr	mkBVRotateRight (int i, BitVecExpr t)

BitVecExpr	mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkBVRotateRight (BitVecExpr t1, BitVecExpr t2)

BitVecExpr	mkInt2BV (int n, IntExpr t)

IntExpr	mkBV2Int (BitVecExpr t, boolean signed)

BoolExpr	mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)

BoolExpr	mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)

BoolExpr	mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2)

BoolExpr	mkBVNegNoOverflow (BitVecExpr t)

BoolExpr	mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned)

BoolExpr	mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2)

ArrayExpr	mkArrayConst (Symbol name, Sort domain, Sort range)

ArrayExpr	mkArrayConst (String name, Sort domain, Sort range)

Expr	mkSelect (ArrayExpr a, Expr i)

ArrayExpr	mkStore (ArrayExpr a, Expr i, Expr v)

ArrayExpr	mkConstArray (Sort domain, Expr v)

ArrayExpr	mkMap (FuncDecl f, ArrayExpr... args)

Expr	mkTermArray (ArrayExpr array)

Expr	mkArrayExt (ArrayExpr arg1, ArrayExpr arg2)

SetSort	mkSetSort (Sort ty)

ArrayExpr	mkEmptySet (Sort domain)

ArrayExpr	mkFullSet (Sort domain)

ArrayExpr	mkSetAdd (ArrayExpr set, Expr element)

ArrayExpr	mkSetDel (ArrayExpr set, Expr element)

ArrayExpr	mkSetUnion (ArrayExpr... args)

ArrayExpr	mkSetIntersection (ArrayExpr... args)

ArrayExpr	mkSetDifference (ArrayExpr arg1, ArrayExpr arg2)

ArrayExpr	mkSetComplement (ArrayExpr arg)

BoolExpr	mkSetMembership (Expr elem, ArrayExpr set)

BoolExpr	mkSetSubset (ArrayExpr arg1, ArrayExpr arg2)

SeqExpr	MkEmptySeq (Sort s)

SeqExpr	MkUnit (Expr elem)

SeqExpr	MkString (String s)

SeqExpr	MkConcat (SeqExpr... t)

IntExpr	MkLength (SeqExpr s)

BoolExpr	MkPrefixOf (SeqExpr s1, SeqExpr s2)

BoolExpr	MkSuffixOf (SeqExpr s1, SeqExpr s2)

BoolExpr	MkContains (SeqExpr s1, SeqExpr s2)

SeqExpr	MkAt (SeqExpr s, IntExpr index)

SeqExpr	MkExtract (SeqExpr s, IntExpr offset, IntExpr length)

IntExpr	MkIndexOf (SeqExpr s, SeqExpr substr, ArithExpr offset)

SeqExpr	MkReplace (SeqExpr s, SeqExpr src, SeqExpr dst)

ReExpr	MkToRe (SeqExpr s)

BoolExpr	MkInRe (SeqExpr s, ReExpr re)

ReExpr	MkStar (ReExpr re)

ReExpr	MPlus (ReExpr re)

ReExpr	MOption (ReExpr re)

ReExpr	MkConcat (ReExpr... t)

ReExpr	MkUnion (ReExpr... t)

Expr	mkNumeral (String v, Sort ty)

Expr	mkNumeral (int v, Sort ty)

Expr	mkNumeral (long v, Sort ty)

RatNum	mkReal (int num, int den)

RatNum	mkReal (String v)

RatNum	mkReal (int v)

RatNum	mkReal (long v)

IntNum	mkInt (String v)

IntNum	mkInt (int v)

IntNum	mkInt (long v)

BitVecNum	mkBV (String v, int size)

BitVecNum	mkBV (int v, int size)

BitVecNum	mkBV (long v, int size)

Quantifier	mkForall (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)

Quantifier	mkForall (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)

Quantifier	mkExists (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)

Quantifier	mkExists (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)

Quantifier	mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)

Quantifier	mkQuantifier (boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)

void	setPrintMode (Z3_ast_print_mode value)

String	benchmarkToSMTString (String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula)

void	parseSMTLIBString (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)

void	parseSMTLIBFile (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)

int	getNumSMTLIBFormulas ()

BoolExpr []	getSMTLIBFormulas ()

int	getNumSMTLIBAssumptions ()

BoolExpr []	getSMTLIBAssumptions ()

int	getNumSMTLIBDecls ()

FuncDecl []	getSMTLIBDecls ()

int	getNumSMTLIBSorts ()

Sort []	getSMTLIBSorts ()

BoolExpr	parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)

BoolExpr	parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)

Goal	mkGoal (boolean models, boolean unsatCores, boolean proofs)

Params	mkParams ()

int	getNumTactics ()

String []	getTacticNames ()

String	getTacticDescription (String name)

Tactic	mkTactic (String name)

Tactic	andThen (Tactic t1, Tactic t2, Tactic... ts)

Tactic	then (Tactic t1, Tactic t2, Tactic... ts)

Tactic	orElse (Tactic t1, Tactic t2)

Tactic	tryFor (Tactic t, int ms)

Tactic	when (Probe p, Tactic t)

Tactic	cond (Probe p, Tactic t1, Tactic t2)

Tactic	repeat (Tactic t, int max)

Tactic	skip ()

Tactic	fail ()

Tactic	failIf (Probe p)

Tactic	failIfNotDecided ()

Tactic	usingParams (Tactic t, Params p)

Tactic	with (Tactic t, Params p)

Tactic	parOr (Tactic... t)

Tactic	parAndThen (Tactic t1, Tactic t2)

void	interrupt ()

int	getNumProbes ()

String []	getProbeNames ()

String	getProbeDescription (String name)

Probe	mkProbe (String name)

Probe	constProbe (double val)

Probe	lt (Probe p1, Probe p2)

Probe	gt (Probe p1, Probe p2)

Probe	le (Probe p1, Probe p2)

Probe	ge (Probe p1, Probe p2)

Probe	eq (Probe p1, Probe p2)

Probe	and (Probe p1, Probe p2)

Probe	or (Probe p1, Probe p2)

Probe	not (Probe p)

Solver	mkSolver ()

Solver	mkSolver (Symbol logic)

Solver	mkSolver (String logic)

Solver	mkSimpleSolver ()

Solver	mkSolver (Tactic t)

Fixedpoint	mkFixedpoint ()

Optimize	mkOptimize ()

FPRMSort	mkFPRoundingModeSort ()

FPRMExpr	mkFPRoundNearestTiesToEven ()

FPRMNum	mkFPRNE ()

FPRMNum	mkFPRoundNearestTiesToAway ()

FPRMNum	mkFPRNA ()

FPRMNum	mkFPRoundTowardPositive ()

FPRMNum	mkFPRTP ()

FPRMNum	mkFPRoundTowardNegative ()

FPRMNum	mkFPRTN ()

FPRMNum	mkFPRoundTowardZero ()

FPRMNum	mkFPRTZ ()

FPSort	mkFPSort (int ebits, int sbits)

FPSort	mkFPSortHalf ()

FPSort	mkFPSort16 ()

FPSort	mkFPSortSingle ()

FPSort	mkFPSort32 ()

FPSort	mkFPSortDouble ()

FPSort	mkFPSort64 ()

FPSort	mkFPSortQuadruple ()

FPSort	mkFPSort128 ()

FPNum	mkFPNaN (FPSort s)

FPNum	mkFPInf (FPSort s, boolean negative)

FPNum	mkFPZero (FPSort s, boolean negative)

FPNum	mkFPNumeral (float v, FPSort s)

FPNum	mkFPNumeral (double v, FPSort s)

FPNum	mkFPNumeral (int v, FPSort s)

FPNum	mkFPNumeral (boolean sgn, int exp, int sig, FPSort s)

FPNum	mkFPNumeral (boolean sgn, long exp, long sig, FPSort s)

FPNum	mkFP (float v, FPSort s)

FPNum	mkFP (double v, FPSort s)

FPNum	mkFP (int v, FPSort s)

FPNum	mkFP (boolean sgn, int exp, int sig, FPSort s)

FPNum	mkFP (boolean sgn, long exp, long sig, FPSort s)

FPExpr	mkFPAbs (FPExpr t)

FPExpr	mkFPNeg (FPExpr t)

FPExpr	mkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2)

FPExpr	mkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2)

FPExpr	mkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2)

FPExpr	mkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2)

FPExpr	mkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3)

FPExpr	mkFPSqrt (FPRMExpr rm, FPExpr t)

FPExpr	mkFPRem (FPExpr t1, FPExpr t2)

FPExpr	mkFPRoundToIntegral (FPRMExpr rm, FPExpr t)

FPExpr	mkFPMin (FPExpr t1, FPExpr t2)

FPExpr	mkFPMax (FPExpr t1, FPExpr t2)

BoolExpr	mkFPLEq (FPExpr t1, FPExpr t2)

BoolExpr	mkFPLt (FPExpr t1, FPExpr t2)

BoolExpr	mkFPGEq (FPExpr t1, FPExpr t2)

BoolExpr	mkFPGt (FPExpr t1, FPExpr t2)

BoolExpr	mkFPEq (FPExpr t1, FPExpr t2)

BoolExpr	mkFPIsNormal (FPExpr t)

BoolExpr	mkFPIsSubnormal (FPExpr t)

BoolExpr	mkFPIsZero (FPExpr t)

BoolExpr	mkFPIsInfinite (FPExpr t)

BoolExpr	mkFPIsNaN (FPExpr t)

BoolExpr	mkFPIsNegative (FPExpr t)

BoolExpr	mkFPIsPositive (FPExpr t)

FPExpr	mkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)

FPExpr	mkFPToFP (BitVecExpr bv, FPSort s)

FPExpr	mkFPToFP (FPRMExpr rm, FPExpr t, FPSort s)

FPExpr	mkFPToFP (FPRMExpr rm, RealExpr t, FPSort s)

FPExpr	mkFPToFP (FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed)

FPExpr	mkFPToFP (FPSort s, FPRMExpr rm, FPExpr t)

BitVecExpr	mkFPToBV (FPRMExpr rm, FPExpr t, int sz, boolean signed)

RealExpr	mkFPToReal (FPExpr t)

BitVecExpr	mkFPToIEEEBV (FPExpr t)

BitVecExpr	mkFPToFP (FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)

AST	wrapAST (long nativeObject)

long	unwrapAST (AST a)

String	SimplifyHelp ()

ParamDescrs	getSimplifyParameterDescriptions ()

void	updateParamValue (String id, String value)

IDecRefQueue< Constructor >	getConstructorDRQ ()

IDecRefQueue< ConstructorList >	getConstructorListDRQ ()

IDecRefQueue< AST >	getASTDRQ ()

IDecRefQueue< ASTMap >	getASTMapDRQ ()

IDecRefQueue< ASTVector >	getASTVectorDRQ ()

IDecRefQueue< ApplyResult >	getApplyResultDRQ ()

IDecRefQueue< FuncInterp.Entry >	getFuncEntryDRQ ()

IDecRefQueue< FuncInterp >	getFuncInterpDRQ ()

IDecRefQueue< Goal >	getGoalDRQ ()

IDecRefQueue< Model >	getModelDRQ ()

IDecRefQueue< Params >	getParamsDRQ ()

IDecRefQueue< ParamDescrs >	getParamDescrsDRQ ()

IDecRefQueue< Probe >	getProbeDRQ ()

IDecRefQueue< Solver >	getSolverDRQ ()

IDecRefQueue< Statistics >	getStatisticsDRQ ()

IDecRefQueue< Tactic >	getTacticDRQ ()

IDecRefQueue< Fixedpoint >	getFixedpointDRQ ()

IDecRefQueue< Optimize >	getOptimizeDRQ ()

void	close ()

Static Public Member Functions
static InterpolationContext	mkContext ()

static InterpolationContext	mkContext (Map< String, String > settings)

Additional Inherited Members
Protected Member Functions inherited from Context
	Context (long m_ctx)

Detailed Description

The InterpolationContext is suitable for generation of interpolants.

Remarks: For more information on interpolation please refer too the C/C++ API, which is well documented.

Definition at line 30 of file InterpolationContext.java.

Member Function Documentation

◆ CheckInterpolant()

CheckInterpolantResult CheckInterpolant	(	Expr []	cnsts,
		int []	parents,
		BoolExpr []	interps,
		String	error,
		Expr []	theory
	)

inline

Checks the correctness of an interpolant.

Remarks: 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 148 of file InterpolationContext.java.

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

◆ ComputeInterpolant()

ComputeInterpolantResult ComputeInterpolant	(	Expr	pat,
		Params	p
	)

inline

Computes an interpolant.

Remarks: For more information on interpolation please refer too the function Z3_compute_interpolant in the C/C++ API, which is well documented.

Exceptions

Z3Exception

Definition at line 109 of file InterpolationContext.java.

     {
         checkContextMatch(pat);
         checkContextMatch(p);
 
         ComputeInterpolantResult res = new ComputeInterpolantResult();
         Native.LongPtr n_i = new Native.LongPtr();
         Native.LongPtr n_m = new Native.LongPtr();
         res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
         if (res.status == Z3_lbool.Z3_L_FALSE)
             res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
         if (res.status == Z3_lbool.Z3_L_TRUE) 
             res.model = new Model(this, n_m.value);
         return res;
     }

◆ GetInterpolant()

BoolExpr [] GetInterpolant	(	Expr	pf,
		Expr	pat,
		Params	p
	)

inline

Computes an interpolant. Remarks: For more information on interpolation please refer too the function Z3_get_interpolant in the C/C++ API, which is well documented.

Exceptions

Z3Exception

Definition at line 85 of file InterpolationContext.java.

     {
         checkContextMatch(pf);
         checkContextMatch(pat);
         checkContextMatch(p);
 
         ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
         return seq.ToBoolExprArray();
     }

◆ InterpolationProfile()

String InterpolationProfile ( )

inline

Return a string summarizing cumulative time used for interpolation.

Remarks: 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 131 of file InterpolationContext.java.

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

◆ mkContext() [1/2]

static InterpolationContext mkContext ( )

inlinestatic

Constructor.

Definition at line 35 of file InterpolationContext.java.

     {
         long m_ctx;
         synchronized(creation_lock) {
             m_ctx = Native.mkInterpolationContext(0);
         }
         return new InterpolationContext(m_ctx);
     }

◆ mkContext() [2/2]

static InterpolationContext mkContext ( Map< String, String > settings )

inlinestatic

Constructor.

Remarks:

See also: Context::Context

Definition at line 51 of file InterpolationContext.java.

     { 
         long m_ctx;
         synchronized(creation_lock) {
             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);
         }
         return new InterpolationContext(m_ctx);
     }

◆ MkInterpolant()

BoolExpr MkInterpolant ( BoolExpr a )

inline

Create an expression that marks a formula position for interpolation.

Exceptions

Z3Exception

Definition at line 72 of file InterpolationContext.java.

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

◆ ReadInterpolationProblem()

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

inline

Reads an interpolation problem from a file.

Remarks: 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 179 of file InterpolationContext.java.

     {
         ReadInterpolationProblemResult res = new ReadInterpolationProblemResult();
         
         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();
         res.return_value = 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;
         res.error = n_err_str.value;
         res.cnsts = new Expr[num];
         res.parents = new int[num];
         theory = new Expr[num_theory];
         for (int i = 0; i < num; i++)
         {
             res.cnsts[i] = Expr.create(this, n_cnsts.value[i]);
             res.parents[i] = n_parents.value[i];
         }
         for (int i = 0; i < num_theory; i++)
             res.theory[i] = Expr.create(this, n_theory.value[i]);
         return res;
     }

◆ WriteInterpolationProblem()

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

inline

Writes an interpolation problem to a file.

Remarks: 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 212 of file InterpolationContext.java.

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

Data Structures

Public Member Functions

Static Public Member Functions

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ CheckInterpolant()

◆ ComputeInterpolant()

◆ GetInterpolant()

◆ InterpolationProfile()

◆ mkContext() [1/2]

◆ mkContext() [2/2]

◆ MkInterpolant()

◆ ReadInterpolationProblem()

◆ WriteInterpolationProblem()