---
name: "interpfilter"
section: "1"
platform: "linux"
package: "ladr4-apps"
version: "0.0.200911a-2.1+b2"
release: "Debian 10 (Buster)"
platforms: ["linux"]
url: "https://new.carta.tech/interpfilter"
---

# interpfilter(1)

filter models with formulas

## NAME

interpfilter - filter models with formulas

## SYNOPSIS

**interpfilter** \<*formulas-file*\> \<*test*\> \< \<*interpretations-file*\> \> \<*passing-interpretations-file*\>

## DESCRIPTION

This manual page documents briefly the **interpfilter** command.

Given a set of *formulas*, a *test* to perform, and a stream of *interpretations*, **interpfilter** outputs the interpretations that pass the test.

## TESTS

The following tests are available.

- **all\_true**

  All formulas true in given interpretation.

- **some\_true**

  Some formula true in given interpretation.

- **all\_false**

  All formulas false in given interpretation.

- **some\_false**

  Some formula false in given interpretation.

## SEE ALSO

[**prover9**(1)](/prover9/1.md), [**mace4**(1)](/mace4/1.md).\
 Full documentation for **interpfilter** is found in the **prover9** manual, available on Debian systems in the *prover9-doc* package at */usr/share/doc/prover9-doc/manual/index.html*.

## AUTHOR

**interpfilter** was written by William McCune \<mccune@cs.unm.edu\>

This manual page was written by Peter Collingbourne \<peter@pcc.me.uk\>, for the Debian project (but may be used by others).