Map encoding and polymorphism
We are generating code that uses generic structures such as maps. Ideally we would like to select the appropriate SMT encoding as late as possible, ideally in the prover driver. For example for maps, one can select the SMTlib theory of arrays, or use an abstract type with get/set functions and axioms.
If we use the Why3 theory map.Map in the generated code, then we have two choices:
- we can encode it to SMT arrays as is done e.g. in
smtlibv2.gen
; this works well. - we can choose to not do that; in this case, we would get extra "noise" due to the encoding of polymorphism.
There is another option to not use map.Map, and instead define an abstract (non-polymorphic) map type with fixed index and component types, get/set functions and the axioms. Given the cloning mechanism of Why3, this is still entirely generic, as one can do something like this:
module Gen_Map
type map
type index_type
type component_type
function get (m : map) (i : index_type) : component_type
...
end
...
clone Gen_Map with type index_type = int, component_type = comp
This has the advantage of avoiding the polymorphism encoding. However, using this variant, we have given up (1) above, we can't map this type to SMTlib arrays.
This has the effect that we are essentially deciding at code generation time whether to use SMTlib array encoding or not.
Now my question: Is there a way to write why3 code in such a way that one can select (at the driver level) whether to use SMTlib arrays or whether to use an abstract type (without polymorphism encoding)? If this involves writing e.g. a transformation, that would be an option for us.