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 HashMap<SMTTermBinOp.Op,String> |
bvSymbols |
private static HashMap<SMTTermBinOp.Op,String> |
intSymbols |
private SMTTerm |
left |
private SMTTermBinOp.Op |
operator |
private SMTTerm |
right |
Constructor and Description |
---|
SMTTermBinOp(SMTTermBinOp.Op operator,
SMTTerm left,
SMTTerm right) |
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 HashMap<SMTTermBinOp.Op,String> bvSymbols
private static HashMap<SMTTermBinOp.Op,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 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 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(SMTTermBinOp bt)
public String toSting()
private void extractArgsLeft(SMTTermBinOp binop, List<SMTTerm> args)
private void extractArgsRight(SMTTermBinOp binop, List<SMTTerm> args)
private void extractArgs(SMTTermBinOp binop, List<SMTTerm> args)
public boolean isChainableBinOp(SMTTerm t)
private List<List<SMTTerm>> searchChains(List<SMTTerm> args, List<SMTTermBinOp.Op> ops)
private List<SMTTerm> extractChain(int start, List<SMTTerm> args, List<SMTTermBinOp.Op> ops, List<SMTTerm> chainables)
private List<String> checkChainable(int nestPos, List<SMTTerm> args)
nestPos
- args
- private String getSymbol(SMTTermBinOp.Op operator, SMTTerm first)