public class SMTTermBinOp extends SMTTerm
Modifier and Type | Class and Description |
---|---|
static class |
SMTTermBinOp.Op |
static class |
SMTTermBinOp.OpProperty |
SMTTerm.False, SMTTerm.True
Modifier and Type | Field and Description |
---|---|
private static java.util.HashMap<SMTTermBinOp.Op,java.lang.String> |
bvSymbols |
private static java.util.HashMap<SMTTermBinOp.Op,java.lang.String> |
intSymbols |
private SMTTerm |
left |
private SMTTermBinOp.Op |
operator |
private SMTTerm |
right |
Constructor and Description |
---|
SMTTermBinOp(SMTTermBinOp.Op operator,
SMTTerm left,
SMTTerm right) |
Modifier and Type | Method and Description |
---|---|
private java.util.List<java.lang.String> |
checkChainable(int nestPos,
java.util.List<SMTTerm> args) |
SMTTermBinOp |
copy() |
boolean |
equals(java.lang.Object term) |
boolean |
equals(SMTTermBinOp bt) |
private void |
extractArgs(SMTTermBinOp binop,
java.util.List<SMTTerm> args) |
private void |
extractArgsLeft(SMTTermBinOp binop,
java.util.List<SMTTerm> args) |
private void |
extractArgsRight(SMTTermBinOp binop,
java.util.List<SMTTerm> args) |
private java.util.List<SMTTerm> |
extractChain(int start,
java.util.List<SMTTerm> args,
java.util.List<SMTTermBinOp.Op> ops,
java.util.List<SMTTerm> chainables) |
java.util.List<SMTTermVariable> |
getEQVars() |
SMTTerm |
getLeft() |
SMTTermBinOp.Op |
getOperator() |
static SMTTermBinOp.OpProperty |
getProperty(SMTTermBinOp.Op op) |
java.util.List<SMTTermVariable> |
getQuantVars() |
SMTTerm |
getRight() |
private java.lang.String |
getSymbol(SMTTermBinOp.Op operator,
SMTTerm first) |
java.util.List<SMTTermVariable> |
getUQVars() |
java.util.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(java.lang.String id) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
private java.util.List<java.util.List<SMTTerm>> |
searchChains(java.util.List<SMTTerm> args,
java.util.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) |
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
private static java.util.HashMap<SMTTermBinOp.Op,java.lang.String> bvSymbols
private static java.util.HashMap<SMTTermBinOp.Op,java.lang.String> intSymbols
private SMTTermBinOp.Op operator
private SMTTerm left
private SMTTerm right
public SMTTermBinOp(SMTTermBinOp.Op operator, SMTTerm left, SMTTerm right)
public static SMTTermBinOp.OpProperty getProperty(SMTTermBinOp.Op op)
private static void initMaps()
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()
private void extractArgsLeft(SMTTermBinOp binop, java.util.List<SMTTerm> args)
private void extractArgsRight(SMTTermBinOp binop, java.util.List<SMTTerm> args)
private void extractArgs(SMTTermBinOp binop, java.util.List<SMTTerm> args)
public boolean isChainableBinOp(SMTTerm t)
private java.util.List<java.util.List<SMTTerm>> searchChains(java.util.List<SMTTerm> args, java.util.List<SMTTermBinOp.Op> ops)
private java.util.List<SMTTerm> extractChain(int start, java.util.List<SMTTerm> args, java.util.List<SMTTermBinOp.Op> ops, java.util.List<SMTTerm> chainables)
private java.util.List<java.lang.String> checkChainable(int nestPos, java.util.List<SMTTerm> args)
nestPos
- args
- private java.lang.String getSymbol(SMTTermBinOp.Op operator, SMTTerm first)