Reasoner for restricted cardinality constraints over ALC concept descriptions. Implemented on top of the Z3 solver.
