[SMT-LIB] Translation of JML predicate into SMT language

[Daniela da Cruz]

Hello.

I am trying to translate the *\sum* predicate from JML into SMT language,
but I had no sure that I am going in the right way
and probably here someone can help me.

One example of this predicate, would be:

\sum int i; 0 <= i && i < n; a[i])

My first try to translate it into SMT (just for arrays, for now) resulted in
something like this:

:extrafuns ((sum_predicate Int Int Array Int))
:assumption (forall (?i Int) (= (sum_predicate ?i ?i ?a) (select ?a ?i)))
:assumption (forall (?i Int) (?j Int) (?a Array) (= (sum_predicate ?i ?j ?a)
(+ (select ?a ?i) (sum_predicate (+ ?i 1) ?j ?a))))

However, I think that is very slow. Also, how I would write this in version
2.0?

Thanks in advance,
Best Regards
Daniela da Cruz