.TH ISOFILTER 1 "January 20, 2007"
.SH NAME
isofilter - removes isomorphic structures from
.BR mace4 (1)
models
.SH SYNOPSIS
.B isofilter
.RI [ options ]
<
.I input-file
>
.I output-file
.br
.B isofilter0
.RI [ options ]
<
.I input-file
>
.I output-file
.br
.B isofilter2
.RI [ options ]
<
.I input-file
>
.I output-file
.SH DESCRIPTION
This manual page documents briefly the \fBisofilter\fP, \fBisofilter0\fP and \fBisofilter2\fP commands.
.PP
If
.BR mace4 (1)
produces more than one structure, some of them are very likely to be
isomorphic to others. The program \fBisofilter\fP can be used to remove isomorphic
structures.
.SH ALGORITHM
There are multiple \fBisofilter\fP variants providing alternative algorithms.
.TP
.B isofilter
Uses Occurrence Profiles algorithm.
.TP
.B isofilter2
Uses Canonical Forms algorithm.
.SH OPTIONS
A summary of options is included below.
.TP
.B ignore_constants
Ignore all constants during the isomorphism tests.
.TP
.B check \fI<operations>
Consider only the listed \fIoperations\fP in the isomorphism tests.
.TP
.B output \fI<operations>
Output only the listed \fIoperations\fP.
.TP
.B wrap
Enclose the resulting structures in \fBlist(interpretations). ... end_of_list.\fP
.SH SEE ALSO
.BR mace4 (1).
.br
Full documentation for \fBisofilter\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
\fBisofilter\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).