Closed frejknutarlewander closed 2 years ago
invariant/constraint initialisation has been split over three methods
registerVars
_counts
AllDifferent
Each invariant now computes bounds of the output variables (some do tight computations, others overapproximate).
Improved unit tests for InDomain and InSparseDomain
InDomain
InSparseDomain
Added PowDomain constraint to give violation when base is 0 and exponent is negative.
PowDomain
Added NotEqualConst constraint for IntDiv when denominator is 0.
NotEqualConst
IntDiv
invariant/constraint initialisation has been split over three methods
registerVars
- called after the invariant is created and register input and output variablesregisterVars
(when the invariant is created) and computes the bounds of the output variable(s)_counts
forAllDifferent
)Each invariant now computes bounds of the output variables (some do tight computations, others overapproximate).
Improved unit tests for
InDomain
andInSparseDomain
Added
PowDomain
constraint to give violation when base is 0 and exponent is negative.Added
NotEqualConst
constraint forIntDiv
when denominator is 0.