Class for removing irrelevant conjuncts from a conjunction (like equations that have been applied to all other formulas)
Class for representing (possibly quantified) conjunctions of arithmetic
literal (equations, inequalities), predicate literals and negated
A lazy version of conjunctions.
Class for representing a conjunction of negated
Interface for plugins that can be added to the
Factory to construct new reducer plugins.
Reducer plugin that sequentially applies a list of plugins.
Naive version of a subsumption test
Reducer plugin that always just returns unchanged formulas.