Z3
Public Member Functions
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.

39  {
40  m_ctx = Native.mkInterpolationContext(0);
41  initContext();
42  }
InterpolationContext ( Map< String, String >  settings) throws Z3Exception
inline

Constructor.

See also
Context.Context(Dictionary<string, string>)

Definition at line 49 of file InterpolationContext.java.

50  {
51  long cfg = Native.mkConfig();
52  for (Map.Entry<String, String> kv : settings.entrySet())
53  Native.setParamValue(cfg, kv.getKey(), kv.getValue());
54  m_ctx = Native.mkInterpolationContext(cfg);
55  Native.delConfig(cfg);
56  initContext();
57  }
def Map(f, args)
Definition: z3py.py:4040

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.

128  {
129  Native.StringPtr n_err_str = new Native.StringPtr();
130  int r = Native.checkInterpolant(nCtx(),
131  cnsts.length,
132  Expr.arrayToNative(cnsts),
133  parents,
134  Expr.arrayToNative(interps),
135  n_err_str,
136  theory.length,
137  Expr.arrayToNative(theory));
138  error = n_err_str.value;
139  return r;
140  }
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.

117  {
118  return Native.interpolationProfile(nCtx());
119  }
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.

64  {
65  checkContextMatch(a);
66  return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject()));
67  }
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.

149  {
150  Native.IntPtr n_num = new Native.IntPtr();
151  Native.IntPtr n_num_theory = new Native.IntPtr();
152  Native.ObjArrayPtr n_cnsts = new Native.ObjArrayPtr();
153  Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
154  Native.ObjArrayPtr n_theory = new Native.ObjArrayPtr();
155  Native.StringPtr n_err_str = new Native.StringPtr();
156  int r = Native.readInterpolationProblem(nCtx(), n_num, n_cnsts, n_parents, filename, n_err_str, n_num_theory, n_theory);
157  int num = n_num.value;
158  int num_theory = n_num_theory.value;
159  error = n_err_str.value;
160  cnsts = new Expr[num];
161  parents = new int[num];
162  theory = new Expr[num_theory];
163  for (int i = 0; i < num; i++)
164  {
165  cnsts[i] = Expr.create(this, n_cnsts.value[i]);
166  parents[i] = n_parents.value[i];
167  }
168  for (int i = 0; i < num_theory; i++)
169  theory[i] = Expr.create(this, n_theory.value[i]);
170  return r;
171  }
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.

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