[PyVCG] Refactor Record/union references and null

[hoe-jo]

records and unions are modeled as free integers with sentinel 0 meaning "null reference" and 1 meaning "self reference" — an ad-hoc encoding predating PyVCG's native recursive-record support.

PyVCG 1.0.9's self-recursive add_component + Record_Null_Check would let TRLC use real SMT record sorts with a proper null check instead of magic integers.

[florianschanda]

This is not actually what you want. The TRLC records and their references are references, they are not recursive datatypes in the SMT sense.

Specifically you need to model it as a "pointer", hence the integer which enumerates all possible records of a type. And then you have an uninterpreted function that turns the pointer into an instance.

A recursive structure in SMT / PyVCG is more like a LISP list.

[florianschanda]

I should also note that the branch in https://github.com/florianschanda/trlc/tree/vcg_rewrite deals with this more elegantly.