special casing for functions with only one instance

[polgreen]

Implement special casing for functions with only one instance (as in CVC4), do performance comparison

[cristina-david]

@pkesseli Here is the decidable fragment of Strong-Single Invocation (SSI) for Conditional Linear Integer Arithmetic (CLIA) from https://arxiv.org/abs/1802.04428. This should be easy to implement.

If the specification is \exists f. \forall x. \phi(f, x), then a formula is in SSI if:

1. f only occurs in \phi as f(t);
2. in each atomic formula, f(t) occurs at most once.

As SSI is single invocation, we have \exists f. \forall x. \phi(f, x) logically equivalent to \forall x.\exists z.\phi(z, x). Then, we assume \phi(z, x) is normalized such that every atomic formula is in the form of z>=t(x) or z<=t(x).

Let the set of terms involving x be T, then, for any x, the value of f(x) is always a term from T. Hence, we can build an implementation by enumerating every term t_i(x) in T as the value of f(x) and check if \phi(t_i(x), x) is satisfied:

f(x) = ite(\phi(t_1(x), x), t_1(x),
ite(\phi(t_2(x), x), t_2(x),
ite(...)))