cprover
|
Back to Code Contracts User Documentation
While quantified expressions with arbitrary Boolean expressions are supported with an SMT backend, the SAT backend only supports bounded quantification under constant lower & upper bounds. This is because the SAT backend currently expands a universal quantifier (__CPROVER_forall) to a conjunction and an existential quantifier (__CPROVER_exists) to a disjunction on each value within the specified bound.
Concretely, with the SAT backend, the following syntax must be used for quantifiers:
where *range* is an expression of the form
where *lower bound*and *upper bound* are constants. The bound predicates could be strict (e.g., *lower bound* < *id*), or non-strict (e.g., *upper bound* <= *id*), but both the bounds must be constants.
For __CPROVER_forall all *type* values for *identifier* must satisfy *boolean expression*.
For __CPROVER_exists some (at least one) *type* value for *identifier* must satisfy *boolean expression*.
The examples above only work with the SMT backend, since len is not constant. However, if a constant maximum upper bound, say MAX_LEN, is known, then the following workaround may be used with the SAT backend: