public class SMTTermCall extends SMTTerm
SMTTerm.False, SMTTerm.True
Modifier and Type | Field and Description |
---|---|
(package private) java.util.List<SMTTerm> |
args |
(package private) SMTFunction |
func |
Constructor and Description |
---|
SMTTermCall(SMTFunction func,
java.util.List<SMTTerm> args) |
SMTTermCall(SMTFunction func,
SMTTerm arg) |
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) |
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
SMTFunction func
java.util.List<SMTTerm> args
public SMTTermCall(SMTFunction func, java.util.List<SMTTerm> args)
public SMTTermCall(SMTFunction func, SMTTerm arg)
public SMTFunction getFunc()
public void setFunc(SMTFunction func)
public java.util.List<SMTTerm> getArgs()
public void setArgs(java.util.List<SMTTerm> args)
public java.util.List<SMTTermVariable> getQuantVars()
getQuantVars
in class SMTTerm
public java.util.List<SMTTermVariable> getUQVars()
public java.util.List<SMTTermVariable> getEQVars()
public java.util.List<SMTTermVariable> getVars()
public boolean occurs(SMTTermVariable a)
public SMTTerm substitute(SMTTermVariable a, SMTTerm b)
substitute
in class SMTTerm
public SMTTerm substitute(SMTTerm a, SMTTerm b)
substitute
in class SMTTerm
public SMTTerm replace(SMTTermCall a, SMTTerm b)
public SMTTerm instantiate(SMTTermVariable a, SMTTerm b)
instantiate
in class SMTTerm
public SMTTermCall copy()
public boolean equals(java.lang.Object term)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toSting()