[SMT-LIB] Another feature request: cardinality constraints

[Florian Schanda]

Hi all,

Cardinality constrains often feature in encodings, and quite often they are 
inefficient. There is a fair body of literature out there on how to do it 
efficiently, and I think some solvers (from memory lingeling, but I might be 
wrong) spend time to recognize silly cardinality constraints and rework them 
into sensible ones.

I think it would be nice if SMTLIB can express cardinality so that solver 
writers can just implement something cool and we don't have to worry about 
encoding.

Some ideas come to mind:

   ; obvious
   (exactly-one a b c ...)
   (at-most-one a b c ...)

   ; between 3 and 5 must be true
   ((_ cardinality 3 5) a b c d e f ...)

If you want to go crazy you can also think up a way to describe weights, like 
you can do in answer set programming. :)


No feature request should go without applications, so:

   In SPARK we have a construct "Contract_Cases" where exactly one
   case must be true as they are not allowed to overlap:

      Contract_Cases => (x in 1 .. 10 => P,
                         x = 3        => Q)  -- not OK!

   Currently we encode this in the obvious and painful way (add integers) and
   it would be nice to write this differently.

I think additions to the core theory are the most useful ones, but this could 
also be added to bitvectors. Proposed syntax:

   (bvupot x)  ;; bv unsigned power-of-two (exactly one)

I can't think of a good name for the at-most-one case.


Thoughts?

	Florian