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) List<SMTTermVariable> |
bindVars |
(package private) List<List<SMTTerm>> |
pats |
(package private) SMTTermQuant.Quant |
quant |
(package private) SMTTerm |
sub |
Constructor and Description |
---|
SMTTermQuant(SMTTermQuant.Quant quant,
List<SMTTermVariable> bindVars,
SMTTerm sub,
List<List<SMTTerm>> pats) |
SMTTermQuant(SMTTermQuant.Quant quant,
List<SMTTermVariable> bindVars,
SMTTerm sub,
SMTTerm pat) |
Modifier and Type | Method and Description |
---|---|
SMTTermQuant |
copy() |
boolean |
equals(Object term) |
List<SMTTermVariable> |
getBindVars() |
List<SMTTermVariable> |
getEQVars() |
List<List<SMTTerm>> |
getPats() |
SMTTermQuant.Quant |
getQuant() |
List<SMTTermVariable> |
getQuantVars() |
SMTTerm |
getSub() |
List<SMTTermVariable> |
getUQVars() |
List<SMTTermVariable> |
getVars() |
int |
hashCode() |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(String id) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
void |
setBindVars(List<SMTTermVariable> bindVars) |
void |
setPats(List<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) |
String |
toSting() |
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
List<SMTTermVariable> bindVars
SMTTerm sub
public SMTTermQuant(SMTTermQuant.Quant quant, List<SMTTermVariable> bindVars, SMTTerm sub, List<List<SMTTerm>> pats)
public SMTTermQuant(SMTTermQuant.Quant quant, List<SMTTermVariable> bindVars, SMTTerm sub, SMTTerm pat)
public SMTTermQuant.Quant getQuant()
public void setQuant(SMTTermQuant.Quant quant)
public List<SMTTermVariable> getBindVars()
public void setBindVars(List<SMTTermVariable> bindVars)
public SMTTerm getSub()
public void setSub(SMTTerm sub)
public List<SMTTermVariable> getQuantVars()
getQuantVars
in class SMTTerm
public List<SMTTermVariable> getUQVars()
public List<SMTTermVariable> getEQVars()
public 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 String toSting()