Support for fixed width integers

[adsharma]

I'm trying to implement the following:

def foo(x, y):
    i: i8 = 200  # should not be satisfiable due to width
    j = 200 # ok

using

https://github.com/adsharma/Typpete/commit/53feec072a60675436748d024a988902ae489f33

But I'm running into an error on this line:

https://github.com/adsharma/Typpete/blob/53feec072a60675436748d024a988902ae489f33/typpete/src/z3_types.py#L566

TypeError: '<' not supported between instances of 'DatatypeRef' and 'int'

If t was an Int it would have been a valid expression. But it seems to be a DatatypeRef. Any suggestions on how to specify this constraint? Looks like I have to ast-fy the limit to be able to build an expression. Pointers to existing code would be great. I looked at z3_axioms.py but couldn't find one.

[adsharma]

This code is working better for me:

        # unsigned
        for w in (64, 32, 16, 8):
            T = getattr(self, f"u{w}")
            t = self.new_z3_const("t")
            a = ForAll(t, And(self.subtype(t, T), t < (1 << w), t >= 0))
            axioms.append(a)

But one problem remains: only Constants from ArithSort seem to be comparable to integer constants. For example:

t = Int('t')
axioms.append(t >=0)

works. But if t is from z3_types.type_sort, comparison to constants isn't possible. Looking for ways to make z3_types.u8 behave the same way as z3.Int.

[adsharma]

I made some more progress in:

https://github.com/adsharma/Typpete/commit/618d449a654df379d5c49775c046c6859a7a051e

But now I see a different problem in _infer_annotated_assign().

https://paste.ubuntu.com/p/ShWffRkfjY/

Any hints on how to convince z3 that Int is compatible with i8 as long as it's within the bounds?

[adsharma]

Also discussed here: https://github.com/Z3Prover/z3/discussions/5428

[adsharma]

The discussion moved to https://github.com/dafny-lang/dafny/issues/1323. I'm able to get things working with dafny. Now trying to generate similar results using typpete.

[adsharma]

https://github.com/adsharma/Typpete/commit/38068caab098616dd5956affe07a491f181180e6 works for me.