Z3
Data Structures | Public Member Functions | Static Public Member Functions
InterpolationContext Class Reference
+ 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< ConstructorgetConstructorDRQ ()
 
IDecRefQueue< ConstructorListgetConstructorListDRQ ()
 
IDecRefQueue< ASTgetASTDRQ ()
 
IDecRefQueue< ASTMap > getASTMapDRQ ()
 
IDecRefQueue< ASTVectorgetASTVectorDRQ ()
 
IDecRefQueue< ApplyResultgetApplyResultDRQ ()
 
IDecRefQueue< FuncInterp.Entry > getFuncEntryDRQ ()
 
IDecRefQueue< FuncInterpgetFuncInterpDRQ ()
 
IDecRefQueue< GoalgetGoalDRQ ()
 
IDecRefQueue< ModelgetModelDRQ ()
 
IDecRefQueue< ParamsgetParamsDRQ ()
 
IDecRefQueue< ParamDescrsgetParamDescrsDRQ ()
 
IDecRefQueue< ProbegetProbeDRQ ()
 
IDecRefQueue< SolvergetSolverDRQ ()
 
IDecRefQueue< StatisticsgetStatisticsDRQ ()
 
IDecRefQueue< TacticgetTacticDRQ ()
 
IDecRefQueue< FixedpointgetFixedpointDRQ ()
 
IDecRefQueue< OptimizegetOptimizeDRQ ()
 
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.

149  {
150  CheckInterpolantResult res = new CheckInterpolantResult();
151  Native.StringPtr n_err_str = new Native.StringPtr();
152  res.return_value = Native.checkInterpolant(nCtx(),
153  cnsts.length,
154  Expr.arrayToNative(cnsts),
155  parents,
156  Expr.arrayToNative(interps),
157  n_err_str,
158  theory.length,
159  Expr.arrayToNative(theory));
160  res.error = n_err_str.value;
161  return res;
162  }

§ 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.

110  {
111  checkContextMatch(pat);
112  checkContextMatch(p);
113 
114  ComputeInterpolantResult res = new ComputeInterpolantResult();
115  Native.LongPtr n_i = new Native.LongPtr();
116  Native.LongPtr n_m = new Native.LongPtr();
117  res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
118  if (res.status == Z3_lbool.Z3_L_FALSE)
119  res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
120  if (res.status == Z3_lbool.Z3_L_TRUE)
121  res.model = new Model(this, n_m.value);
122  return res;
123  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105

§ 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.

86  {
87  checkContextMatch(pf);
88  checkContextMatch(pat);
89  checkContextMatch(p);
90 
91  ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
92  return seq.ToBoolExprArray();
93  }

§ 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.

132  {
133  return Native.interpolationProfile(nCtx());
134  }

§ mkContext() [1/2]

static InterpolationContext mkContext ( )
inlinestatic

Constructor.

Definition at line 35 of file InterpolationContext.java.

36  {
37  long m_ctx;
38  synchronized(creation_lock) {
39  m_ctx = Native.mkInterpolationContext(0);
40  }
41  return new InterpolationContext(m_ctx);
42  }

§ 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.

52  {
53  long m_ctx;
54  synchronized(creation_lock) {
55  long cfg = Native.mkConfig();
56  for (Map.Entry<String, String> kv : settings.entrySet())
57  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
58  m_ctx = Native.mkInterpolationContext(cfg);
59  Native.delConfig(cfg);
60  }
61  return new InterpolationContext(m_ctx);
62  }
def Map(f, args)
Definition: z3py.py:4207
def String(name, ctx=None)
Definition: z3py.py:9443

§ 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.

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

§ 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.

180  {
181  ReadInterpolationProblemResult res = new ReadInterpolationProblemResult();
182 
183  Native.IntPtr n_num = new Native.IntPtr();
184  Native.IntPtr n_num_theory = new Native.IntPtr();
185  Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
186  Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
187  Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
188  Native.StringPtr n_err_str = new Native.StringPtr();
189  res.return_value = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
190  int num = n_num.value;
191  int num_theory = n_num_theory.value;
192  res.error = n_err_str.value;
193  res.cnsts = new Expr[num];
194  res.parents = new int[num];
195  theory = new Expr[num_theory];
196  for (int i = 0; i < num; i++)
197  {
198  res.cnsts[i] = Expr.create(this, n_cnsts.value[i]);
199  res.parents[i] = n_parents.value[i];
200  }
201  for (int i = 0; i < num_theory; i++)
202  res.theory[i] = Expr.create(this, n_theory.value[i]);
203  return res;
204  }

§ 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.

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