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

*To*: pvs-help@csl.sri.com*Subject*: parameters in new strategies*From*: Hanne Gottliebsen <hago@dcs.st-and.ac.uk>*Date*: Tue, 16 Nov 1999 17:19:59 +0000 (GMT)*Delivery-Date*: Tue Nov 16 09:19:21 1999

I am trying to work out how to write new strategies. I have with me the prover-guide and the "less elementary introduction", are there anything that gives more examples/explanation of new strategies? I have the following strategy: (defstep simple-cts ( ) (GRIND :DEFS NIL :THEORIES ("lambda_abstractions[real]" "continuous_functions[real]") :EXCLUDE ("continuous[real]" "continuity_def[real]")) "cts for fcts with domain real" "By theorems in continuous_functions") which applied works fine. 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) (GRIND :DEFS NIL :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 Restoring the state. test2 : |------- {1} FORALL (a, y: real): continuous(LAMBDA x: a + x, y) And I don't really want it as an optional parameter, but a required one anyway. Or is it that I should not expect PVS to handle theory-parameters as arguments to strategies? Thanks, Hanne Gottliebsen --------------------------------------------------------- Hanne Gottliebsen Office P337 Dept. of Computer Science Ph: +44 1334 46 3265 University of St Andrews hago@dcs.st-and.ac.uk - Who moved the stone? ---------------------------------------------------------

- Prev by Date:
**PVS2.3 detection of theory parameters** - Next by Date:
**parameters in new strategies** - Prev by thread:
**inspecting goal in strategy** - Next by thread:
**parameters in new strategies** - Index(es):