Separation logic specification

Only the three kinds that mention no heap sort are specified here, and they are all Bool: sep.emp, and the two connectives. cvc5 marks the whole family experimental.

SEP_PTO and SEP_NIL are deliberately absent. Both are only meaningful against the heap that Solver.declareSepHeap declares — a pto whose operands are not the heap's location and data sorts is accepted by cvc5 at construction and rejected at check-sat, with an error naming set.union rather than pto. So they hang off the handle declareSepHeap answers instead, in Cvc.{Untyped,Typed}.Theory.Sep, where the sorts are known and can be checked.