de.uka.ilkd.key.smt.lang

Class SMTTerm.True

java.lang.Object

de.uka.ilkd.key.smt.lang.SMTTerm

de.uka.ilkd.key.smt.lang.SMTTerm.True

Enclosing class:

SMTTerm

public static final class SMTTerm.True
extends SMTTerm

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.smt.lang.SMTTerm

SMTTerm.False, SMTTerm.True

Field Summary

Fields inherited from class de.uka.ilkd.key.smt.lang.SMTTerm

comment, FALSE, TRUE, upp

Constructor Summary

Constructors

Constructor and Description
True()

Method Summary

Modifier and Type	Method and Description
SMTTerm	and(SMTTerm right)
SMTTerm	copy()
SMTTerm	forall(java.util.List<SMTTermVariable> bindVars, java.util.List<java.util.List<SMTTerm>> pats)
SMTTerm	iff(SMTTerm right)
SMTTerm	implies(SMTTerm right)
SMTTerm	instantiate(SMTTermVariable a, SMTTerm b)
boolean	occurs(SMTTermVariable a)
boolean	occurs(java.lang.String id)
SMTTerm	or(SMTTerm right)
SMTTerm	replace(SMTTermCall a, SMTTerm b)
SMTTerm	sign(boolean pol)
SMTSort	sort()
SMTTerm	substitute(SMTTerm a, SMTTerm b)
SMTTerm	substitute(SMTTermVariable a, SMTTerm b)
java.lang.String	toString()
java.lang.String	toString(int nestPos)

Methods inherited from class de.uka.ilkd.key.smt.lang.SMTTerm

and, binOp, c, call, call, call, call, call, call, call, call, concat, div, equal, equal, exists, exists, exists, exists, exists, exists, exists, exists, forall, forall, forall, forall, forall, forall, forall, forall, forall, forall, getComment, getEQVars, getQuantVars, getSubs, getUQVars, getVars, gt, gte, implies, isCons, ite, lt, lte, minus, mul, multOp, not, not, number, number, or, plus, quant, quant, rem, setComment, terms, terms, toList, toList, unaryOp

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

True

public True()

Method Detail

sort

public SMTSort sort()

Specified by:

sort in class SMTTerm

occurs

public boolean occurs(SMTTermVariable a)

Specified by:

occurs in class SMTTerm

sign

public SMTTerm sign(boolean pol)

Overrides:

sign in class SMTTerm

occurs

public boolean occurs(java.lang.String id)

Specified by:

occurs in class SMTTerm

substitute

public SMTTerm substitute(SMTTermVariable a,
                          SMTTerm b)

Specified by:

substitute in class SMTTerm

substitute

public SMTTerm substitute(SMTTerm a,
                          SMTTerm b)

Specified by:

substitute in class SMTTerm

replace

public SMTTerm replace(SMTTermCall a,
                       SMTTerm b)

Specified by:

replace in class SMTTerm

instantiate

public SMTTerm instantiate(SMTTermVariable a,
                           SMTTerm b)

Specified by:

instantiate in class SMTTerm

copy

public SMTTerm copy()

Specified by:

copy in class SMTTerm

toString

public java.lang.String toString()

Overrides:

toString in class SMTTerm

toString

public java.lang.String toString(int nestPos)

Overrides:

toString in class SMTTerm

or

public SMTTerm or(SMTTerm right)

Overrides:

or in class SMTTerm

and

public SMTTerm and(SMTTerm right)

Overrides:

and in class SMTTerm

implies

public SMTTerm implies(SMTTerm right)

Overrides:

implies in class SMTTerm

iff

public SMTTerm iff(SMTTerm right)

Overrides:

iff in class SMTTerm

forall

public SMTTerm forall(java.util.List<SMTTermVariable> bindVars,
                      java.util.List<java.util.List<SMTTerm>> pats)

Overrides:

forall in class SMTTerm