[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Declaring a list of expressions in a .pvs file
I have a strategy which at some point generates a number of
goals, each having a consequent of the form
EXISTS (e: SOME_DOMAIN):
(e = expr_1 OR
e = expr_2 OR
e = expr_3 OR ... )
When there is only one OR in the expression, then PVS manages to
discharge the goal automatically.
However, when there are 2 or more ORs, I instantiate the statement
manually (inst-cp for every expr_i).
The list of exprs that can occur is quite small, and I can pass it as a
parameter to the strategy as (``expr1'' ``expr2'' ``expr3'' ... ) and
then the instantiation can be automated too.
However, I'd like to go a step further and have the user declare a named
list of expressions (each written as a string) in the .pvs file.
The expressions are typically records, e.g. "(# a := 3, b := Z #)",
so I want to declare the list
mylist = ( "(# a := 3, b := Z #)" "(# a := 8, b := Y #)" "(# a := 5, b := Y #)")
The strategy would then use mylist. (In fact, the list can be generated
from other definitions in the .pvs file, and ideally this may be done by
Is there anyway to do this?