.TH INTERPFILTER 1 "January 20, 2007"
.SH NAME
interpfilter - filter models with formulas
.SH SYNOPSIS
.B interpfilter
.RI < formulas-file >
.RI < test >
<
.RI < interpretations-file >
>
.RI < passing-interpretations-file >
.SH DESCRIPTION
This manual page documents briefly the
.B interpfilter
command.
.PP
Given a set of \fIformulas\fP, a \fItest\fP to perform, and a
stream of \fIinterpretations\fP, \fBinterpfilter\fP outputs the interpretations
that pass the test.
.SH TESTS
The following tests are available.
.TP
.B all_true
All formulas true in given interpretation.
.TP
.B some_true
Some formula true in given interpretation.
.TP
.B all_false
All formulas false in given interpretation.
.TP
.B some_false
Some formula false in given interpretation.
.SH SEE ALSO
.BR prover9 (1),
.BR mace4 (1).
.br
Full documentation for \fBinterpfilter\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
.SH AUTHOR
\fBinterpfilter\fP was written by William McCune <mccune@cs.unm.edu>
.PP
This manual page was written by Peter Collingbourne <peter@pcc.me.uk>,
for the Debian project (but may be used by others).