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

[PVS-Help] Changing a goal formula

As part of a strategy, I want to replace a formula in the goal goal
with another formula.  Currently, I am using 
    (setf (formula (car (select-seq (s-forms *goal*) fnum))) new-formula)
However, this has the disadvantages that 
    1. My strategy acts like a skip (which makes using try/else
      impossible) 
    2. I cannot use undo after applying the strategy

Is there a proper way of manipulating a goal formula?  If not, is
there some way I can get around the problems above (esp. #1)?

Thank you, 

    Erika