This file is indexed.

/usr/share/doc/prover9-doc/html/white-black.html is in prover9-doc 0.0.200902a-1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
  <title>Prover9 Manual: Keep and Delete Rules</title>
 <link rel="stylesheet" href="manual.css">
</head>

<body>


<hr>
<table width="100%">
<tr>
<colgroup>
<col width="33%">
<col width="34%">
<col width="33%">
</colgroup>
<td align="left"><i>Prover9 Manual</i>
<td align="center"><img src="prover9-5a-256t.gif">
<td align="right"><i>Version 2009-02A</i>
</table>
<hr>

<!-- Main content -->

<h1>Keep and Delete Rules (Advanced)</h1>

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
<a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a>,
<a href="process-inf.html#max_vars"><tt><b>max_vars</b></tt></a>,
<a href="process-inf.html#max_literals"><tt><b>max_literals</b></tt></a>,
and
<tt>max_depth</tt>.

<p>
The mechanism uses the <a href="clause-properties.html">
Clause Properties</a> language for specifying clauses that
are to be kept or deleted.

<p>
Two lists can be given in the input: a "<tt>keep</tt>" list
and a "<tt>delete</tt>" list.  Here are examples of each.
<pre class="my_file">
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.
</pre>

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

<pre class="my_code">
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;
</pre>
Note that if the clause satisfies rules in both lists, it is kept.

<p>
The ordinary parameters
<a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a>,
<a href="process-inf.html#max_vars"><tt><b>max_vars</b></tt></a>,
<a href="process-inf.html#max_literals"><tt><b>max_literals</b></tt></a>,
and
<tt>max_depth</tt>
are can be thought of as shorthand for simple rules in the
"<tt>delete</tt>" list.  For example the pair of commands
<pre class="my_file">
assign(max_literals, 3).
assign(max_vars, 0).
</pre>
are operationally equivalent to the "<tt>delete</tt>" list
<pre class="my_file">
list(delete).
    literals > 3.
    variables > 4.
end_of_list.
</pre>
In fact, the parameters
<a href="process-inf.html#max_weight"><tt><b>max_weight</b></tt></a>,
<a href="process-inf.html#max_vars"><tt><b>max_vars</b></tt></a>,
<a href="process-inf.html#max_literals"><tt><b>max_literals</b></tt></a>,
and
<tt>max_depth</tt>
are implemented in Prover9 by constructing an internal
"<tt>delete</tt>" list, and any "<tt>delete</tt>" list given
by the user is simply appended to the internal list.

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

<h2>

<!--
<hr>
Next Section:
<a href="goals.html">Goals and Denials</a>
-->

</body>
</html>