Prover9 Manual Version 2009-02A

Actions

Prover9's actions allow the user to change the search strategy during the search. For example, after a certain number of given clauses have been used, the max_weight can be changed.

Actions can be triggered in two ways:

Accepted Actions

The currently accepted actions are exit (which terminates the search) and a subset of the ordinary flags and parameters.

Actions Triggered by Counters

Counter actions are given as a list of rules trigger -> action in the input file. Here are the currently recognized triggers for counter actions. The list must start with list(actions). and end with end_of_list.

Here is an example list of counter actions.

list(actions).

  given=10        -> set(print_kept).
  kept=1000       -> assign(max_weight, 30).
  generated=5000  -> assign(pick_given_ratio, 4).
  level=3         -> exit.

end_of_list.

Actions Triggered by Clauses

Clause actions occur as attributes on clauses, for example,
A * B != B * A  # action(in_proof -> assign(max_weight, 30)).
In this example (which only makes sense if max_proofs > 1), if the clause occurs in a proof, the action is applied.

The only trigger currently recognized for clause actions is in_proof. Others will likely be added.


Next Section: Goals and Denials