de.uka.ilkd.key.smt.lang

Class SMTTermITE

java.lang.Object

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

de.uka.ilkd.key.smt.lang.SMTTermITE

public class SMTTermITE
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

Modifier and Type	Field and Description
(package private) SMTTerm	condition
(package private) SMTTerm	falseCase
private static java.lang.String	ITE_STRING
(package private) SMTTerm	trueCase

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

comment, FALSE, TRUE, upp

Constructor Summary

Constructors

Constructor and Description
SMTTermITE(SMTTerm condition, SMTTerm trueCase, SMTTerm falseCase)

Method Summary

Modifier and Type	Method and Description
SMTTerm	copy()
boolean	equals(java.lang.Object that)
SMTTerm	getCondition()
SMTTerm	getFalseCase()
java.util.List<SMTTermVariable>	getQuantVars()
SMTTerm	getTrueCase()
SMTTerm	instantiate(SMTTermVariable a, SMTTerm b)
boolean	occurs(SMTTermVariable a)
boolean	occurs(java.lang.String id)
SMTTerm	replace(SMTTermCall a, SMTTerm b)
void	setCondition(SMTTerm condition)
void	setFalseCase(SMTTerm falseCase)
void	setTrueCase(SMTTerm trueCase)
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, 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, forall, getComment, getEQVars, getSubs, getUQVars, getVars, gt, gte, iff, implies, implies, isCons, ite, lt, lte, minus, mul, multOp, not, not, number, number, or, or, plus, quant, quant, rem, setComment, sign, terms, terms, toList, toList, unaryOp

Methods inherited from class java.lang.Object

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

Field Detail

condition

SMTTerm condition

trueCase

SMTTerm trueCase

falseCase

SMTTerm falseCase

ITE_STRING

private static final java.lang.String ITE_STRING

See Also:

Constant Field Values

Constructor Detail

SMTTermITE

public SMTTermITE(SMTTerm condition,
                  SMTTerm trueCase,
                  SMTTerm falseCase)

Method Detail

occurs

public boolean occurs(SMTTermVariable a)

Specified by:

occurs in class SMTTerm

occurs

public boolean occurs(java.lang.String id)

Specified by:

occurs in class SMTTerm

sort

public SMTSort sort()

Specified by:

sort 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(int nestPos)

Overrides:

toString in class SMTTerm

toString

public java.lang.String toString()

Overrides:

toString in class SMTTerm

equals

public boolean equals(java.lang.Object that)

Overrides:

equals in class java.lang.Object

getCondition

public SMTTerm getCondition()

Returns:

the condition

getTrueCase

public SMTTerm getTrueCase()

Returns:

the trueCase

getFalseCase

public SMTTerm getFalseCase()

Returns:

the falseCase

setCondition

public void setCondition(SMTTerm condition)

Parameters:

condition - the condition to set

setTrueCase

public void setTrueCase(SMTTerm trueCase)

Parameters:

trueCase - the trueCase to set

setFalseCase

public void setFalseCase(SMTTerm falseCase)

Parameters:

falseCase - the falseCase to set

getQuantVars

public java.util.List<SMTTermVariable> getQuantVars()

Overrides:

getQuantVars in class SMTTerm