InterpolationContext.ComputeInterpolantResult Class Reference

Data Fields
Z3_lbool	status = Z3_lbool.Z3_L_UNDEF
BoolExpr []	interp = null
Model	model = null

Detailed Description

Definition at line 95 of file InterpolationContext.java.

Field Documentation

interp

BoolExpr [] interp = null

Definition at line 98 of file InterpolationContext.java.

Referenced by InterpolationContext.ComputeInterpolant().

model

Model model = null

Definition at line 99 of file InterpolationContext.java.

Referenced by ModelRef.__del__(), ModelRef.__getitem__(), ModelRef.__len__(), InterpolationContext.ComputeInterpolant(), ModelRef.decls(), ModelRef.eval(), ModelRef.get_interp(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sexpr().

status

Z3_lbool status = Z3_lbool.Z3_L_UNDEF

Definition at line 97 of file InterpolationContext.java.

Referenced by InterpolationContext.ComputeInterpolant().