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