Currently, MARVLus handles refinement and base variables differently. Base variables are simply added to the environment while typing rules are applied to refinement variables to verify their satisfiability.
This process can be generalized by treating base variables as trivially true refinement variables.
An implementation idea is to create a function a vc_gen_refinement_variable function that:
has inputs variable_name, base_type, refinement_expression and rhs_expression
applies the typing rule for refinement variables (current MARVLus implementation)
For base variables a "True" expression is passed as the refinement_expression variable
Currently, MARVLus handles refinement and base variables differently. Base variables are simply added to the environment while typing rules are applied to refinement variables to verify their satisfiability.
This process can be generalized by treating base variables as trivially true refinement variables.
An implementation idea is to create a function a
vc_gen_refinement_variablefunction that:For base variables a "True" expression is passed as the refinement_expression variable