Treat some arguments to a special function call, e.g. in `So`, to be a request to SMT-solver

[buzden]

In a situation when we have some arguments a, b, c, ... given or already generated, some other arguments x, y, z, ... not yet generated and having a constructor argument So (f a b c ... x y z ...), if f contains, say, only particular type of arithmetic, we could ask SMT solver about x, y, z rather than generating them and after that checking for inhabitance of So ..., as we do now.

Something like

data X : Nat -> Nat -> Type where
  MkX : (a, b, x, y, z : Nat) -> So (x * a + y * b == z) -> X a b

genX : Fuel -> (a, b : Nat) -> Gen MaybeEmpty (X a b)
genX = deriveGen