public class SMTTermBinOp extends SMTTerm
Modifier and Type | Class and Description |
---|---|
static class |
SMTTermBinOp.Op |
static class |
SMTTermBinOp.OpProperty |
SMTTerm.False, SMTTerm.True
Constructor and Description |
---|
SMTTermBinOp(SMTTermBinOp.Op operator,
SMTTerm left,
SMTTerm right) |
Modifier and Type | Method and Description |
---|---|
SMTTermBinOp |
copy() |
boolean |
equals(java.lang.Object term) |
boolean |
equals(SMTTermBinOp bt) |
java.util.List<SMTTermVariable> |
getEQVars() |
SMTTerm |
getLeft() |
SMTTermBinOp.Op |
getOperator() |
static SMTTermBinOp.OpProperty |
getProperty(SMTTermBinOp.Op op) |
java.util.List<SMTTermVariable> |
getQuantVars() |
SMTTerm |
getRight() |
java.util.List<SMTTermVariable> |
getUQVars() |
java.util.List<SMTTermVariable> |
getVars() |
int |
hashCode() |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
boolean |
isChainableBinOp(SMTTerm t) |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(java.lang.String id) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
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) |
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 SMTTermBinOp(SMTTermBinOp.Op operator, SMTTerm left, SMTTerm right)
public static SMTTermBinOp.OpProperty getProperty(SMTTermBinOp.Op op)
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 SMTTermBinOp.Op getOperator()
public void setOperator(SMTTermBinOp.Op operator)
public SMTTerm getLeft()
public void setLeft(SMTTerm left)
public SMTTerm getRight()
public void setRight(SMTTerm right)
public SMTTermBinOp copy()
public boolean equals(java.lang.Object term)
equals
in class java.lang.Object
public boolean equals(SMTTermBinOp bt)
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toSting()
public boolean isChainableBinOp(SMTTerm t)
Copyright © 2003-2019 The KeY-Project.