Improve behavior of mod, int2bv, bv2nat, etc. when called on non-constant terms

[bclement-ocp]

This is an alternative / improved approach to (some of) #736

The crux of the issue is that if we have a function that is interpreted only on constants (i.e. a function for which we can compute, but not reason about, such as mod or bv2nat and int2bv), once we fall back to its "term" version when the argument is not a constant, we will never evaluate the result.

Simple example:

$ cat int2bv1.smt2
(set-logic ALL)

(assert (distinct ((_ int2bv 2) 0) #b00))
(check-sat)
$ alt-ergo --frontend dolmen int2bv1.smt2 2>/dev/null

; File "int2bv1.smt2", line 4, characters 1-12: Valid (0.0064) (1 steps) (goal g_1)

unsat

$ cat int2bv2.smt2
(set-logic ALL)

(define-fun x () Int 0)
(assert (distinct ((_ int2bv 2) x) #b00))
(check-sat)
$ alt-ergo --frontend dolmen int2bv2.smt2

; File "int2bv2.smt2", line 5, characters 1-12: I don't know (0.0060) (4 steps) (goal g_1)

unknown

It is not clear to me at the time of writing what the proper fix for this is. Preprocessing unconstrained equalities into hard rewrites would make sense, but we are not really equipped to do it because there are term-indexed maps everywhere. Probably the better fix would be to have a way to indicate that certain functions should trigger a second call to X.make when (one of) their argument gets substituted. I am not sure if this should be a different type of semantic values (say, Lazy or Partial) or just a flag on Term semantic values, although the latter is probably more pragmatic.

[bclement-ocp]

Writing this so that I don't forget again: we can't make a second call to X.make because once the equality x = 2 is known, the value is (generally) a semantic value, not a term anymore.

[bclement-ocp]

So now I think that the best way to do this would be:

• Add a function val compute : Symbols.t -> r list -> r. Computable symbols are symbols that can be evaluated on constants.
• Add "computable" symbols as a separate constructor in Shostak (treated as a "builtin" theory like Ac), so that we can have the appropriate terms as leafs. This should also mean that the terms will get abstracted properly when they appear in equations.
• When the leafs of a computable symbol get updated, call the compute function from the appropriate theory (dispatched based on is_mine_symb).

Of course, if compute is not able to compute, it should return a new computable term that we will try to evaluate again later.

It feels kind of weird because it somewhat blurs the line between terms and representatives, but I don't see a better way.