[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: problems with writing strategies for PVS*From*: Joachim van den Berg <joachim@cicero.cs.kun.nl>*Date*: Fri, 5 Jan 2001 02:33:53 +0100 (CET)*cc*: joachim@cs.kun.nl

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/

- Prev by Date:
**Re: show-tccs doesn't work** - Next by Date:
**infix-problem** - Prev by thread:
**Re: infix-problem** - Next by thread:
**show-tccs doesn't work** - Index(es):