The strategies used for Experiments 1 and 2 on

http://aprove.informatik.rwth-aachen.de/eval/Formative/

To invoke AProVE with a strategy file "foo.strategy"
for its configuration, use

java -ea -jar <<...>> aprove20140427-formative.jar <<...>> -s foo.strategy

(Here <<...>> stands for other stuff that one might like to write at
this point. As usual, there ought to be a suitable "minisat2core"
executable in "$PATH".)

An explanation for some of the strategy parameters of the
reduction pair processor that may be of interest for twiddling:

* Usable:
Orient only usable rules instead of full R?

* Active:
If usable rules are to be considered, also use the argument filtering \pi
induced by the reduction pair to compute (and orient) only the usable
rules wrt \pi?

* Formative:
Orient only formative rules instead of full R?

* FormativeActive:
If formative rules are to be considered, also use the argument filtering \pi
induced by the reduction pair to compute (and orient) only the formative
rules wrt \pi?

Note that in case both formative and usable rules are desired, the
most restrictive settings are considered (demand orientation for a few
rules as possible). The most extreme configurations:

-  FR(P,UR(P,R),pi) \cap UR(P,R,\pi)
-  SFR(P,UR(P,R),pi)

* MergeMutual:
Use cheaper (but less precise) computation of the "activation
condition" for mutually recursive rules in R? (If f calls g and
g calls f, then all their rules get the same activation condition
if this flag gets set to "True")


Order-specific parameters:

* POLO:

- "Range" can take any positive value n, then coefficients for the
  interpretation are sought from [0..n].
- "Degree" can take any positive value k or SIMPLE or SIMPLE_MIXED.
  (Heuristics may be used to mitigate the size explosion of the
  symbolic polynomials in case of non-linear polynomials.)

* RPO (here under the name "PPO" for "Parametrisable Path Order".
Most parameters are self-speaking, except perhaps:

- "Xgengrc": If true, then it is exploited that x >= c holds for
  variables x and constants c of minimal precedence (arity 0 of c may
  also be caused by a sneaky argument filtering!)


Things that are NOT done currently in AProVE (even though they may be
rather feasible -- then again, we still need some more contributions
for the journal version, and the conference version passed the bar
already without them):

* switch to innermost (and back)
* type inference in innermost mode
* if the argument filtering happens to linearise all left-hand sides
  (one can encode this happenstance to constraints), do not
  necessarily consider the whole of R formative
* combine UR /wrt AF/ and Split-Formative Rules wrt AF
  (currently not done because the computation does not track which
  "split rules" correspond to which original rules from R)
