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 statistics, 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.
Author: list the subset here!
Actions Triggered by Statistics
Statistic actions are given as a list of rules trigger -> action
in the input file.
Here are the currently recognized triggers for statistic 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 terms(actions).
and end with end_of_list.
Here is an example list of statistic action rules.
terms(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.