/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>
|