de.uka.ilkd.key.smt.lang

Class SMTTermCall

java.lang.Object

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

de.uka.ilkd.key.smt.lang.SMTTermCall

public class SMTTermCall
extends SMTTerm

SMTLib supports functions as well as predicates. We only use functions and represent predicates as boolean valued functions. As consequence a function application can build a term as well as a formula.

Author:

Aboubakr Achraf El Ghazi

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) java.util.List<SMTTerm>	args
(package private) SMTFunction	func

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

comment, FALSE, TRUE, upp

Constructor Summary

Constructors

Constructor and Description
SMTTermCall(SMTFunction func, java.util.List<SMTTerm> args)
SMTTermCall(SMTFunction func, SMTTerm arg)

Method Summary

Modifier and Type	Method and Description
SMTTermCall	copy()
boolean	equals(java.lang.Object term)
java.util.List<SMTTerm>	getArgs()
java.util.List<SMTTermVariable>	getEQVars()
SMTFunction	getFunc()
java.util.List<SMTTermVariable>	getQuantVars()
java.util.List<SMTTermVariable>	getUQVars()
java.util.List<SMTTermVariable>	getVars()
int	hashCode()
SMTTerm	instantiate(SMTTermVariable a, SMTTerm b)
boolean	occurs(SMTTermVariable a)
boolean	occurs(java.lang.String id)
SMTTerm	replace(SMTTermCall a, SMTTerm b)
void	setArgs(java.util.List<SMTTerm> args)
void	setFunc(SMTFunction func)
SMTSort	sort()
SMTTerm	substitute(SMTTerm a, SMTTerm b)
SMTTerm	substitute(SMTTermVariable a, SMTTerm b)
java.lang.String	toSting()
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, getSubs, 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, toString, unaryOp

Methods inherited from class java.lang.Object

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

Field Detail

func

SMTFunction func

args

java.util.List<SMTTerm> args

Constructor Detail

SMTTermCall

public SMTTermCall(SMTFunction func,
                   java.util.List<SMTTerm> args)

SMTTermCall

public SMTTermCall(SMTFunction func,
                   SMTTerm arg)

Method Detail

getFunc

public SMTFunction getFunc()

setFunc

public void setFunc(SMTFunction func)

getArgs

public java.util.List<SMTTerm> getArgs()

setArgs

public void setArgs(java.util.List<SMTTerm> args)

getQuantVars

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

Overrides:

getQuantVars in class SMTTerm

getUQVars

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

Overrides:

getUQVars in class SMTTerm

getEQVars

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

Overrides:

getEQVars in class SMTTerm

getVars

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

Overrides:

getVars in class SMTTerm

sort

public SMTSort sort()

Specified by:

sort in class SMTTerm

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

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 SMTTermCall copy()

Specified by:

copy in class SMTTerm

equals

public boolean equals(java.lang.Object term)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toSting

public java.lang.String toSting()

toString

public java.lang.String toString(int nestPos)

Overrides:

toString in class SMTTerm