All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
private List<String> |
checkChainable(int nestPos,
List<SMTTerm> args) |
SMTTermBinOp |
copy() |
boolean |
equals(Object term) |
boolean |
equals(SMTTermBinOp bt) |
private void |
extractArgs(SMTTermBinOp binop,
List<SMTTerm> args) |
private void |
extractArgsLeft(SMTTermBinOp binop,
List<SMTTerm> args) |
private void |
extractArgsRight(SMTTermBinOp binop,
List<SMTTerm> args) |
private List<SMTTerm> |
extractChain(int start,
List<SMTTerm> args,
List<SMTTermBinOp.Op> ops,
List<SMTTerm> chainables) |
List<SMTTermVariable> |
getEQVars() |
SMTTerm |
getLeft() |
SMTTermBinOp.Op |
getOperator() |
static SMTTermBinOp.OpProperty |
getProperty(SMTTermBinOp.Op op) |
List<SMTTermVariable> |
getQuantVars() |
SMTTerm |
getRight() |
private String |
getSymbol(SMTTermBinOp.Op operator,
SMTTerm first) |
List<SMTTermVariable> |
getUQVars() |
List<SMTTermVariable> |
getVars() |
int |
hashCode() |
private static void |
initMaps() |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
boolean |
isChainableBinOp(SMTTerm t) |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(String id) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
private List<List<SMTTerm>> |
searchChains(List<SMTTerm> args,
List<SMTTermBinOp.Op> ops) |
void |
setLeft(SMTTerm left) |
void |
setOperator(SMTTermBinOp.Op operator) |
void |
setRight(SMTTerm right) |
SMTSort |
sort() |
SMTTerm |
substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
substitute(SMTTermVariable a,
SMTTerm b) |
String |
toSting() |
String |
toString(int nestPos) |