share/strategies.conf

   1 [strategy]
   2 name = "Split"
   3 desc = "Split"
   4 shortcut = "s"
   5 code = "t split_goal_wp exit"
   6
   7 [strategy]
   8 name = "Inline"
   9 desc = "Inline"
  10 shortcut = "i"
  11 code = "t inline_goal exit"
  12
  13 [strategy]
  14 name = "Auto Level 0"
  15 desc = "Simple@ automatic@ run@ of@ main@ provers"
  16 shortcut = "b"
  17 code = "
  18 start:
  19   c Alt-Ergo,1.01, 1 1000
  20   c CVC4,1.4, 1 1000
  21   c Z3,4.4.1, 1 1000
  22   t split_goal_wp start
  23   c Alt-Ergo,1.01, 10 4000
  24   c CVC4,1.4, 10 4000
  25   c Z3,4.4.1, 10 4000"
  26
  27 [strategy]
  28 name = "Auto Level 1"
  29 desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations"
  30 code = "
  31 start:
  32    c Alt-Ergo,1.01, 1 1000
  33    c CVC4,1.4, 1 1000
  34    c Z3,4.4.1, 1 1000
  35 next:
  36    t split_goal_wp start
  37    c Alt-Ergo,1.01, 5 2000
  38    c CVC4,1.4, 5 2000
  39    c Z3,4.4.1, 5 2000
  40    t introduce_premises afterintro
  41    g inline
  42 afterintro:
  43    t split_goal_wp start
  44 inline:
  45    t inline_goal afterinline
  46    g longtime
  47 afterinline:
  48    t split_goal_wp start
  49 longtime:
  50    c Alt-Ergo,1.01, 30 4000
  51    c CVC4,1.4, 30 4000
  52    c Z3,4.4.1, 30 4000"