Prover9 Manual |  | Version 2009-02A

# Keep and Delete Rules (Advanced)

This page describes a mechanism that allows the user to have more control over which clauses are kept or deleted than by using the parameters `max_weight`, `max_vars`, `max_literals`, and `max_depth`.

The mechanism uses the Clause Properties language for specifying clauses that are to be kept or deleted.

Two lists can be given in the input: a "`keep`" list and a "`delete`" list. Here are examples of each.

    list(keep).
        -horn & literals=3 & variables=0 & level<4.
        horn & variables<3.
    end_of_list.

    list(delete).
        weight > 30.
        weight > 20 & (-horn | variables > 4).
    end_of_list.

Given a newly derived clause, the following procedure is applied.

    If the clause satisfies any rule in the "keep" list, then
        the clause is kept;
    else if the clause satisfies any rule in the "delete" list, then
        the clause is deleted;
    else
        the clause is kept;

Note that if the clause satisfies rules in both lists, it is kept.

The ordinary parameters `max_weight`, `max_vars`, `max_literals`, and `max_depth` are can be thought of as shorthand for simple rules in the "`delete`" list. For example the pair of commands

    assign(max_literals, 3).
    assign(max_vars, 0).

are operationally equivalent to the "`delete`" list

    list(delete).
        literals > 3.
        variables > 4.
    end_of_list.

In fact, the parameters `max_weight`, `max_vars`, `max_literals`, and `max_depth` are implemented in Prover9 by constructing an internal "`delete`" list, and any "`delete`" list given by the user is simply appended to the internal list.

The rules in the "`delete`" list are not applied to initial clauses; that is, clauses that are input or derived before the selection of the first given clause.

##