Add support for int.pow2

[hra687261]

Closes #1274

[bclement-ocp]

Suggested change

	| Sy.Op Sy.Int_pow2, [x] ->
	(* int.pow2 n = pow(2, n) *)
	mke coef p (E.mk_term (Sy.Op Sy.Pow) [E.Ints.of_int 2; x] ty) ctx
	| Sy.Op Sy.Int_pow2, [x] ->
	( mk_partial_interpretation_1 (fun x -> calc_power (Q.of_int 2) x ty) coef p ty t x, ctx)

avoids constructing the (pow 2 n) term

[hra687261]

Oh, it seems that the test that I added no longer works with this change, maybe we should not create the term when the argument is a literal, and create it when it isn't?

(set-logic ALL)
(declare-const n Int)
(assert (not (= (int.pow2 n) (ae.pow_int 2 n))))
(check-sat)

[bclement-ocp]

Hmmm this sounds very fishy, I don't think we should be able to deduce unsat from a delayed operation. I forgot about the equality (= (int.pow2 n) (pow 2 n)) when I first wrote my suggestion, I think if we want to have it your initial implementation is the right one.

In fact in that case we might even want to translate (int.pow2 n) into (pow 2 n) directly at the term level (i.e. in translate.ml, parse (int.pow2 n) directly as (pow 2 n) — I don't think there is any benefit in keeping the int.pow2 symbol if we introduce the equality anyways.

[hra687261]

I don't think we should be able to deduce unsat from a delayed operation.

We don't, I was using dune runtest instead of make runtest.

I was hoping there was a way to produce the same semantic values from both int.pow2 n and pow 2 n so that the symbolic reasoning would work when we don't know anything about n. But ok, creating the same term from the start should work indeed.

[bclement-ocp]

We don't have semantic values for pow; it's not part of the Shostak theory for (linear) arithmetic.

[bobot]

Just an advice add a test with a very large n to see what happens to alt-ergo. For colibri at first the result was an out-of-memory. ;)

[bclement-ocp]

Thanks for the tip! We already have a guard against such out-of-memory errors in calc_power for the generic pow function.