public class BoundUniquenessChecker
extends java.lang.Object
\assumes (==>\forall var; phi)
\find (\forall var; phi ==>)
would nearly never match, as var would be required to match
the same object.Modifier and Type | Field and Description |
---|---|
private java.util.HashSet<QuantifiableVariable> |
boundVars |
private ImmutableList<Term> |
terms |
Constructor and Description |
---|
BoundUniquenessChecker(Sequent seq) |
BoundUniquenessChecker(Term t,
Sequent seq) |
Modifier and Type | Method and Description |
---|---|
void |
addAll(Sequent seq)
adds all formulas in the sequent to the list of terms to
include in the uniqueness check
|
void |
addTerm(Term term)
adds term to the list of terms to include in
the uniqueness check
|
boolean |
correct()
returns true if any variable is bound at most once in the
given set of terms
|
private boolean |
correct(Term t) |
private java.util.HashSet<QuantifiableVariable> boundVars
private ImmutableList<Term> terms
public BoundUniquenessChecker(Sequent seq)
public void addTerm(Term term)
term
- a Termpublic void addAll(Sequent seq)
seq
- the Sequent with the formulas to addprivate boolean correct(Term t)
public boolean correct()