[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
problems with writing strategies for PVS
Dear PVS experts,
I ran into some trouble while writing strategies for PVS. I really appreciate
if someone can give me a solution to this problem.
I would like to have a strategy which filters all the conditional statements
from the sequent formulas. On these statements I would like to apply
a function.
Below, I have written the most crucial part of the strategy.
(let ((sforms (gather-seq (s-forms (current-goal *ps*))
'*
nil
PRED1))
(fnums (gather-fnums sforms
'*
nil
PRED2)))
(.....))
PRED1 should be read as
#'(lambda (sf) (or (branch? (formula sf))
(and (negation? (formula sf))
(branch? (args1 (formula sf)))))
(or something like that)
After having extracted the conditional statements, I would like to apply
a function on the THEN and ELSE part. I can extract the conditional
expression and the THEN part with (args1 (formula sf)) and
(args2 (formula sf)), respectively, but I didn't manage the extract the ELSE
part. I hope that one of you can help me!
My second question is: is it feasible (and if so, how?) to evaluate the
expressions which are written in the THEN and ELSE part? More specifically,
can I recognise the boolean values TRUE and FALSE (easily)? I have searched
for recognisers for them, but I couldn't find any. Any suggestion is very
welcome!
Yours sincerely,
Joachim van den Berg
--
________________________________________________________________________
Joachim van den Berg______________________________tel. +31 24 36 52710
Computer Science Institute____________________mailto:joachim@cs.kun.nl
University of Nijmegen_____________http://www.cs.kun.nl/~joachim/LOOP/