Package apron

Class Pplite

java.lang.Object

apron.Manager

apron.Pplite

public class Pplite
extends Manager

Manager factory for the PPLite domains.

Field Summary

Fields inherited from class apron.Manager

FUNID_ADD_DIMENSIONS, FUNID_ADD_RAY_ARRAY, FUNID_APPROXIMATE, FUNID_ASSIGN_LINEXPR_ARRAY, FUNID_ASSIGN_TEXPR_ARRAY, FUNID_BOTTOM, FUNID_BOUND_DIMENSION, FUNID_BOUND_LINEXPR, FUNID_BOUND_TEXPR, FUNID_CANONICALIZE, FUNID_CLOSURE, FUNID_COPY, FUNID_DESERIALIZE_RAW, FUNID_DIMENSION, FUNID_EXPAND, FUNID_FDUMP, FUNID_FOLD, FUNID_FORGET_ARRAY, FUNID_FPRINT, FUNID_FPRINTDIFF, FUNID_FREE, FUNID_HASH, FUNID_IS_BOTTOM, FUNID_IS_DIMENSION_UNCONSTRAINED, FUNID_IS_EQ, FUNID_IS_LEQ, FUNID_IS_TOP, FUNID_JOIN, FUNID_JOIN_ARRAY, FUNID_MEET, FUNID_MEET_ARRAY, FUNID_MEET_LINCONS_ARRAY, FUNID_MEET_TCONS_ARRAY, FUNID_MINIMIZE, FUNID_OF_BOX, FUNID_PERMUTE_DIMENSIONS, FUNID_REMOVE_DIMENSIONS, FUNID_SAT_INTERVAL, FUNID_SAT_LINCONS, FUNID_SAT_TCONS, FUNID_SERIALIZE_RAW, FUNID_SIZE, FUNID_SUBSTITUTE_LINEXPR_ARRAY, FUNID_SUBSTITUTE_TEXPR_ARRAY, FUNID_TO_BOX, FUNID_TO_GENERATOR_ARRAY, FUNID_TO_LINCONS_ARRAY, FUNID_TO_TCONS_ARRAY, FUNID_TOP, FUNID_WIDENING, SCALAR_DOUBLE, SCALAR_MPFR, SCALAR_MPQ

Constructor Summary

Constructors

Constructor	Description
Pplite(boolean strict)	Creates a new manager to create and manipulate convex polyhedra.

Method Summary

Modifier and Type	Method	Description
void	collapse(Abstract0 a, int n)	Modifies a to have at most n disjuncts.
String	getKind()
int	getNumDisjuncts(Abstract0 a)	Returns the number of disjuncts in a
String	getWidenSpec()
boolean	isDisjunctive(Abstract0 a)	Returns true if a is a disjunctive abstract element
boolean	isGeomSubsetEq(Abstract0 a1, Abstract0 a2)	Geometric inclusion test
void	setKind(String name)	Sets specific implementation of polyhedra domain; this should be called before creating objects, since the different implementations are incompatible.
void	setWidenSpec(String name)	Sets the widening specification used by domains; legal values are: - "safe": the Cousot and Cousot POPL77 specification, which does not assume the inclusion between arguments; - "risky": the Cousot and Cousot PLILP92 footnote 6 alternative specification, assuming the inclusion between arguments.
Abstract0	split(Abstract0 a, Lincons0 c, boolean integral, boolean strict)	Splits element a using (non-interval) linear inequality constraint c.
Lincons0[]	toDisjunctLincons(Abstract0 a, int n)	Returns a set of linear constraints for the n-tn disjunct of a
Tcons0[]	toDisjunctTcons(Abstract0 a, int n)	Returns a set of constraints for the n-tn disjunct of a

Methods inherited from class apron.Manager

finalize, getAlgorithm, getFlagBestWanted, getFlagExactWanted, getLibrary, getMaxObjectSize, getPreferedScalarType, getTimeout, getVersion, setAlgorithm, setFlagBestWanted, setFlagExactWanted, setMaxObjectSize, setPreferedScalarType, setTimeout, wasBest, wasExact

Methods inherited from class java.lang.Object

clone, equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

Pplite

public Pplite(boolean strict)

Creates a new manager to create and manipulate convex polyhedra. using the PPLite library.

If strict is true, then the domain can express strict inequalities, i.e., non-closed convex polyhedra. Otherwise, the domain expresses closed convex polyhedra.

Method Details

setKind

public void setKind(String name)

Sets specific implementation of polyhedra domain; this should be called before creating objects, since the different implementations are incompatible.

Accepted values: "Poly" (default), "F_Poly", "U_Poly", "UF_Poly", "P_Set", "FP_Set".

getKind

public String getKind()

setWidenSpec

public void setWidenSpec(String name)

Sets the widening specification used by domains; legal values are: - "safe": the Cousot and Cousot POPL77 specification, which does not assume the inclusion between arguments; - "risky": the Cousot and Cousot PLILP92 footnote 6 alternative specification, assuming the inclusion between arguments.

getWidenSpec

public String getWidenSpec()

split

public Abstract0 split(Abstract0 a,
 Lincons0 c,
 boolean integral,
 boolean strict)

Splits element a using (non-interval) linear inequality constraint c. The return value is computed by adding the complement of c to element a, whereas a itself is updated by adding constraint c. If parameter integral is true, then the constraint c is assumed to evaluate to an integral value and refined accordingly; e.g., (x < 5) is refined into (x ≤ 4) and its complement is computed as (x ≥ 5). If parameter integral is false, a rational split is computed; in this case, if strict is false then the complement of a lose constraint is still lose; strict splits require a strict manager.

isDisjunctive

public boolean isDisjunctive(Abstract0 a)

Returns true if a is a disjunctive abstract element

getNumDisjuncts

public int getNumDisjuncts(Abstract0 a)

Returns the number of disjuncts in a

toDisjunctLincons

public Lincons0[] toDisjunctLincons(Abstract0 a,
 int n)
                             throws ApronException

Returns a set of linear constraints for the n-tn disjunct of a

Throws:

ApronException

toDisjunctTcons

public Tcons0[] toDisjunctTcons(Abstract0 a,
 int n)
                         throws ApronException

Returns a set of constraints for the n-tn disjunct of a

Throws:

ApronException

collapse

public void collapse(Abstract0 a,
 int n)
              throws ApronException

Modifies a to have at most n disjuncts.

Throws:

ApronException

isGeomSubsetEq

public boolean isGeomSubsetEq(Abstract0 a1,
 Abstract0 a2)
                       throws ApronException

Geometric inclusion test

Throws:

ApronException