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

Re: [PVS-Help] Changing a goal formula


You should not directly modify the state of the proof context because
you can introduce inconsistencies or break the theorem prover. The
proper way to modify the proof context is via logical steps performed by
basic strategies. 

If you have a goal f1 that you want to replace by f2 and you know that
f1 => f2, then try 

(branch (case f2)
        ((skip) ;; This is your new goal
         (the proof of f1 => f2)))


On Tue, 2005-06-28 at 00:19, Erika Rice wrote:
> 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
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way                 http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988