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

Re: parameters in new strategies


> I am trying to work out how to write new strategies.
> I would like to give as a parameter to this strategy the parameter 
> to be used in the theories. Eg:
> (defstep simple-cts2 (&optional fctdomain)
>       :THEORIES ("lambda_abstractions[fctdomain]" 
>                  "continuous_functions[fctdomain]")
>       :EXCLUDE  ("continuous[fctdomain]" 
>                  "continuity_def[fctdomain]"))
>    "cts for fcts with domain fctdomain"
>    "By theorems in continuous_functions")
> But this does not work at all:
> test2 :
>   |-------
> {1}   FORALL (a, y: real): continuous(LAMBDA x: a + x, y)
> Rule? (simple-cts2 :fctdomain "real")
> Actual does not resolve

This message is because the value for GRIND's :THEORY key is 
("lambda_abstractions[fctdomain]" "continuous_functions[fctdomain]"),
i.e. the parameter of your strategy is not evaluated within the
string. In order to do that, you could use something like this (ask
your local lisp hacker for improvements...)

(defstep simple-cts2 (&optional (fctdomain "real"))
  (let ((rewrite-theories  
	 (list (format nil "lambda_abstractions[~a]" fctdomain)
	       (format nil "continuous_functions[~a]" fctdomain)))
	 (list (format nil "continuous[~a]" fctdomain)
	       (format nil "continuity_def[~a]" fctdomain))))
	    :THEORIES rewrite-theories
	    :EXCLUDE exclude-theories))
  "cts for fcts with domain fctdomain"
  "By theorems in continuous_functions")

> And I don't really want it as an optional parameter, but a required 
> one anyway.

You can either provide a default value for the parameter (as above) or
you can simply use

(defstep simple-cts2 (fctdomain) ...)

to define a required parameter.

> Or is it that I should not expect PVS to handle theory-parameters as
> arguments to strategies?

Let's say you have to help PVS a little bit ;-)

Hope this helps,

	- Holger

Holger Pfeifer                              Tel.: (+49) 731 / 502-4124
Universitaet Ulm                             Fax: (+49) 731 / 502-4119
Abt. Kuenstliche Intelligenz          pfeifer@ki.informatik.uni-ulm.de
D-89069 Ulm