Declaring/Defining functions

[bruderj15]

Following #109 one may often use the Sum-Types to only use a small subset of Sort Int for example.

Consider a scheduling problem where one knows that some entities always have exactly one of n heights. Surely one could do:

data Entity t = Entity { height :: Expr t, ... } deriving anyclass (Equatable, Variable)

isOneOf :: forall t f. (KnownSMTSort t, (Equatable (Expr t)) Foldable f) 
  => Expr t -> f (Expr t) -> Expr BoolSort
isOneOf x = exactly @t 1 . fmap (=== x) . toList

problem = do
  e <- variable @(Entity IntSort)
  assert $ height e `isOneOf` [1..10]

However this is significantly more expensive in problem-size and solver-performance than:

data Height = One | Two | ... | Ten
-- with #109 derive: Symbolic Height
data Entity t = Entity { height :: Symbolic Height, ... } 

One may then want to use arithmetics with that and other expressions, so we need to convert:

sconvert :: Symbolic Height -> Expr IntSort

This conversion is obviously symbolic, so we need to (define-fun ...) in SMTLib.

This is easy as in hgoes/smtlib2. However, the types there are ugly and not lightweight at all.

We can do better!