public class SMTTermCall extends SMTTerm
SMTTerm.False, SMTTerm.True
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
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()
Copyright © 2003-2019 The KeY-Project.