[ ]library(COLIBRI_DOC)
Simple COLIBRI interface
Predicates
- Arithmetic operators
- Operators allowed in numerical expressions.
- use_3B
- Enable 3B filtering.
- no_3B
- Disable 3B filtering.
- use_delta
- Enable difference logics and simplex.
- no_delta
- Disable difference logics and simplex.
- solve_cstrs
- Asks to solve current constraints.
- no_solve
- Disable constraints solving.
- set_timeout(T)
- Define time limit.
- set_threshold(T)
- Change reduction threshold.
- get_threshold(T)
- Return current reduction threshold.
- int_vars(Type,Vars)
- Typing constraints for "integer" variables Vars.
- set_default_int_bounds(Low,High)
- Default range for int variables
- Vars #: Range
- Range definition for "integer" types: int, int(N) and uint(N) (where N is the size in bits).
- X #< Y
- X is strictly less than Y.
- X #= Y
- X is equal to Y.
- X #=< Y
- X is less or equal to Y.
- X #> Y
- X is strictly greater than Y.
- X #>= Y
- X is greater or equal to Y.
- X #\= Y
- X is not equal to Y.
- real_vars(+Type,Vars)
- Typing constraints for "real" vars.
- Vars $: +Range
- Range definition for "real" types: real, float and double.
- X $< Y
- X is stricly less than Y.
- X $= Y
- X is equal to Y.
- X $=< Y
- X is less or equal to Y.
- X $> Y
- X is strictly greater than Y.
- X $>= Y
- X is greater or equal to Y.
- X $\= Y
- X is not equal to Y.
- isFinite(X)
- Restriction to finite values.
- isInfinite(X)
- Restriction to infinite values.
- isNormal(X)
- Restriction to normal values.
- isSubnormal(X)
- Restriction to subnormal values.
- isPositive(X)
- Restriction to positive floating point values.
- isNegative(X)
- Restriction to negative floating point values.
- neg(X)
- The negation of X is true.
- X and Y
- X is true and Y is true.
- X or Y
- X is true or Y is true.
- X xor Y
- Eclusive or of X and Y.
- X => Y
- X implies Y.
- ite(Cond,Then,Else)
- if Cond then Then else Else.
Description
A simple solver using COLIBRI
Usage
colibri.(sh|bat) File
or
colibri.(sh|bat)
The sh and bat extentions corresponds to linux and
windows environments. In the first form the script colibri reads
query from file File. In the second form the input is
searched in a file colibri.in in the directory from where the script is called. Results are sent to stdout.
Constraint solving techniques are widely recognized as a powerful
tool for Validation and Verification activities such as test data
generation or counter-example generation from a formal model,
program source code or binary code. A constraint solver maintains a
list of posted constraints (constraint store) over a set of
variables and a set of allowed values (domain) for each variable,
and provides facilities for constraint propagation (filtering) and
for instantiation of variables (labeling) in order to find a
solution.
We present here a simple interface to the COLIBRI library
(COnstraint LIBrary for veRIfication) developed at CEA List and used
inside the GATeL tool for model based testing and verification from
Lustre/SCADE. The variety of types and constraints provided by
COLIBRI makes it possible to use it in other validation tools at CEA
LIST like PathCrawle for test data generation purposes and Osmose
for structural testing from binary code.
COLIBRI provides basic constraints for arithmetic operations and
comparisons of various numeric types (integers, reals and floats).
Cast constraints are available for cast operations between these
types. COLIBRI also provides basic procedures allowing to
instantiate variables in their domains making it possible to design
specific labelling procedures. Thus the three aforementioned testing
tools have designed their own labelling procedures on the basis of
COLIBRI primitives.
The domains of numerical variables are represented by unions of
disjoint intervals (no NaNs for floats): integer bounds for
integers, double float bounds for reals, and double/simple float
bounds for double/simple floating point formats. These unions of
intervals make it possible to accurately handle domain differences.
For each numeric type and each basic unary/binary operation or
comparison, COLIBRI provides the corresponding constraint.
Moreover, for each arithmetic operation, additional filtering rules
apply algebraic simplifications, which are very similar for integer
and real arithmetics, whereas floating arithmetics uses specific
rules. Here are a few examples of basic algebraic simplifications.
- Factorization of constraints. If the constraint store contains
A+B=C and a new constraint A+B=X is added (or derived) in the
store, then only one of these two constraints remains in the
store and the variables C and X are unified, that
is, they are identified and their domain is set to the
intersection of the domains of C and X.
- Special values (neutral elements, absorbing elements).The
constraint A+0=X leads to the unification of A and X.
- Identities between arguments. The constraint A+A=C is
transformed into 2*A=C which is more precisely handled by
interval arithmetics. The constraint A+X=A in integer and real
arithmetics leads to the unification of A and B (which is
not valid in floating point arithmetics).
Bounded and modular integer arithmetics
COLIBRI provides two kinds of arithmetics for integers: bounded
arithmetics for ideal finite integers and modular arithmetics for
signed/unsigned computer integers. Bounded arithmetics is
implemented with classical filtering rules for integer interval
arithmetics. These rules are managed in the projection functions of
each arithmetic constraint. Moreover, a congruence domain is
associated to each integer variable. Filtering rules handle these
congruences in order to compute new ones and maintain the
consistency of interval bounds with congruences. The congruences are
introduced by multiplications by a constant and propagated in the
projection functions of each arithmetic constraint.
Modular arithmetics constraints are implemented by a combination of
bounded arithmetics constraints with modulus constraints. Thus they
benefit from the mechanisms provided for bounded integer
arithmetics. Notice that using the unions of disjoint intervals for
the domain representation makes it possible to precisely represent
the domain of signed/unsigned integers. For example, consider the
constraint A + B = C over 3-bit unsigned integers where A in 2..4, B
in 4..7 and C in 0..7. This constraint is handled by the constraints
corresponding to the bounded arithmetic expression C = A + B - K * 8
where K in 0..1 represents the overflow status.
The filtering of these constraints converges to the interval C in
[0..3, 6..7] where the sub-interval 0..3 of C is reached when there
is an overflow (i.e. K = 1).
The domain representation by compact intervals in this case would be
less precise and result in a complete interval C in [0..7] without
any reduction.
Real and floating point arithmetics
Real arithmetics is implemented with classical filtering rules for
real interval arithmetics where interval bounds are double floats.
In real interval arithmetics each projection function is computed
using different rounding modes for the lower and the upper bounds of
the resulting intervals. The lower bound is computed by rounding
downward, towards -1.0Inf, while the upper bound is computed
by rounding upward, towards +1.0Inf. This enlarging ensures that the
resulting interval is the smallest interval of doubles including all
real solutions.
Floating point arithmetics is implemented with a specific interval.
Notice that properties like associativity or distributivity do not
hold in floating point calculus.
The projection functions in this arithmetics have to take into
account absorption and cancellation phenomena specific to floating
point computations. These phenomena are handled by specific
filtering rules allowing to further reduce the domains of
floating point variables. For example, the constraint A+X=A over
floating point numbers means that X is absorbed by A.
The minimal absolute value in the domain of X can be used to
eliminate all the values in the domain of A that do not absorb this
minimum. Thus, in double precision with the default rounding mode
(called nearest to even), for
X = 1.0 the domain of A is strongly reduced to the union of two
intervals of values that can absorb X:
[MinDouble .. -9007199254740996.0, 9007199254740992.0 ..
MaxDouble].
COLIBRI uses very general and powerful filtering rules for addition
and subtraction operations. For example, for the constraint A+B=1.0
in double precision with the nearest to even rounding mode, such
filtering rules converge to the same interval for A and B
[-9007199254740991.0 .. 9007199254740992.0].
Implementation details
COLIBRI is implemented in ECLiPSe Prolog. Its suspensions, generic
unification and meta-term mechanisms make it possible to easily
design new abstract domains and associated constraints. Incremental
constraint posting with on-the-fly filtering and automatic
backtracking to a previous constraint state provided by COLIBRI are
important benefits for search-based state exploration tools, and in
particular, for test generation tools.
About
- Status: evolving
- Copyright © CEA List
- Date: February 2016
Generated from COLIBRI_DOC.eci on Wed Mar 23 17:46:17 2016