Using inverse functions to encode predicate function injectivity

[marcoeilers]

Addressing issue #291.

With this PR, for predicate P(x: Ref, i: Int), we generate

function  P(x: Ref, i: int): Field PredicateType_P FrameType;
function  P#sm(x: Ref, i: int): Field PredicateType_P PMaskType;
function  P_inv_x(p_1: (Field PredicateType_P FrameType)): Ref;
function  P_inv_i(p_1: (Field PredicateType_P FrameType)): int;
function  P_pmask_inv_x(pm: (Field PredicateType_P PMaskType)): Ref;
function  P_pmask_inv_i(pm: (Field PredicateType_P PMaskType)): int;
axiom (forall x: Ref, i: int ::
  { P(x, i) }
  P_inv_x(P(x, i)) == x && P_inv_i(P(x, i)) == i
);
axiom (forall x: Ref, i: int ::
  { P#sm(x, i) }
  P_pmask_inv_x(P#sm(x, i)) == x && P_pmask_inv_i(P#sm(x, i)) == i
);

instead of the current

function  P(x: Ref, i: int): Field PredicateType_P FrameType;
function  P#sm(x: Ref, i: int): Field PredicateType_P PMaskType;
axiom (forall x: Ref, i: int, x2: Ref, i2: int ::
  { P(x, i), P(x2, i2) }
  P(x, i) == P(x2, i2) ==> x == x2 && i == i2
);
axiom (forall x: Ref, i: int, x2: Ref, i2: int ::
  { P#sm(x, i), P#sm(x2, i2) }
  P#sm(x, i) == P#sm(x2, i2) ==> x == x2 && i == i2
);

and thus avoid a quadratic number of quantifier instantiations.