| 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