public final class Junctor extends AbstractSortedOperator
Modifier and Type | Field and Description |
---|---|
static Junctor |
AND
the usual 'and' operator '/\' (be A, B formulae then 'A /\ B'
is true if and only if A is true and B is true
|
static Junctor |
FALSE
the false constant
|
static Junctor |
IMP
the usual 'implication' operator '->' (be A, B formulae then
'A -> B' is true if and only if A is false or B is true
|
static Junctor |
NOT
the usual 'negation' operator '-'
|
static Junctor |
OR
the usual 'or' operator '\/' (be A, B formulae then 'A \/ B'
is true if and only if A is true or B is true
|
static Junctor |
TRUE
the true constant
|
Modifier and Type | Method and Description |
---|---|
int |
arity()
the arity of this operator
|
boolean |
bindVarsAt(int n)
Tells whether the operator binds variables at the n-th subterm.
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
Name |
name()
returns the name of this element
|
java.lang.String |
toString() |
void |
validTopLevelException(Term term)
Checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator.
|
protected ImmutableArray<java.lang.Boolean> |
whereToBind() |
additionalValidTopLevel, argSort, argSorts, sort, sort
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
arity, bindVarsAt, isRigid, validTopLevel, validTopLevelException
public static final Junctor TRUE
public static final Junctor FALSE
public static final Junctor AND
public static final Junctor OR
public static final Junctor NOT
public static final Junctor IMP
protected final ImmutableArray<java.lang.Boolean> whereToBind()
public final Name name()
Named
public final int arity()
Operator
public final boolean bindVarsAt(int n)
Operator
bindVarsAt
in interface Operator
public final boolean isRigid()
Operator
public void validTopLevelException(Term term) throws TermCreationException
Operator
validTopLevelException
in interface Operator
TermCreationException
- if a construction error was recognisepublic java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.