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:

- by some counter, for example, after 100 clauses have been retained, and
- when a clause containing an action attribute is used, for example, when it is used in a proof.

## Accepted Actions

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

- Changable flags: `reuse_denials`, `print_gen`, `print_kept`, `print_given`, `breadth_first`. `lightest_first`. `breadth_first_hints`.
- Changable parameters: `demod_step_limit`, `demod_increase_limit`, `new_constants`, `para_lit_limit`, `stats`, `max_given`, `max_weight`, `max_depth`, `max_vars`, `max_proofs`, `max_literals`, `constant_weight`, `variable_weight`, `not_weight`, `or_weight`, `prop_atom_weight`, `nest_penalty`, `depth_penalty`, `default_weight`, `pick_given_ratio`, `age_part`, `weight_part`, `hints_part`, `false_part`, `true_part`.

## 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.

- given: the number of given clauses that have been processed.
- generated: the number of clauses that have been inferred.
- kept: the number of clauses that have been inferred and retained.
- level: the search level (this applies to breadth-first searches).

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