public class SMTTermQuant extends SMTTerm
Modifier and Type | Class and Description |
---|---|
static class |
SMTTermQuant.Quant |
SMTTerm.False, SMTTerm.True
Modifier and Type | Field and Description |
---|---|
(package private) java.util.List<SMTTermVariable> |
bindVars |
(package private) java.util.List<java.util.List<SMTTerm>> |
pats |
(package private) SMTTermQuant.Quant |
quant |
(package private) SMTTerm |
sub |
Constructor and Description |
---|
SMTTermQuant(SMTTermQuant.Quant quant,
java.util.List<SMTTermVariable> bindVars,
SMTTerm sub,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTermQuant(SMTTermQuant.Quant quant,
java.util.List<SMTTermVariable> bindVars,
SMTTerm sub,
SMTTerm pat) |
Modifier and Type | Method and Description |
---|---|
SMTTermQuant |
copy() |
boolean |
equals(java.lang.Object term) |
java.util.List<SMTTermVariable> |
getBindVars() |
java.util.List<SMTTermVariable> |
getEQVars() |
java.util.List<java.util.List<SMTTerm>> |
getPats() |
SMTTermQuant.Quant |
getQuant() |
java.util.List<SMTTermVariable> |
getQuantVars() |
SMTTerm |
getSub() |
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 |
setBindVars(java.util.List<SMTTermVariable> bindVars) |
void |
setPats(java.util.List<java.util.List<SMTTerm>> pats) |
void |
setQuant(SMTTermQuant.Quant quant) |
void |
setSub(SMTTerm sub) |
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
SMTTermQuant.Quant quant
java.util.List<SMTTermVariable> bindVars
SMTTerm sub
java.util.List<java.util.List<SMTTerm>> pats
public SMTTermQuant(SMTTermQuant.Quant quant, java.util.List<SMTTermVariable> bindVars, SMTTerm sub, java.util.List<java.util.List<SMTTerm>> pats)
public SMTTermQuant(SMTTermQuant.Quant quant, java.util.List<SMTTermVariable> bindVars, SMTTerm sub, SMTTerm pat)
public SMTTermQuant.Quant getQuant()
public void setQuant(SMTTermQuant.Quant quant)
public java.util.List<SMTTermVariable> getBindVars()
public void setBindVars(java.util.List<SMTTermVariable> bindVars)
public SMTTerm getSub()
public void setSub(SMTTerm sub)
public java.util.List<java.util.List<SMTTerm>> getPats()
public void setPats(java.util.List<java.util.List<SMTTerm>> pats)
pat
- the pat to setpublic 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 SMTTermQuant 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()