public class SMTTermMultOp extends SMTTerm
Modifier and Type | Class and Description |
---|---|
static class |
SMTTermMultOp.Op |
static class |
SMTTermMultOp.OpProperty |
SMTTerm.False, SMTTerm.True
Modifier and Type | Field and Description |
---|---|
private static java.util.HashMap<SMTTermMultOp.Op,java.lang.String> |
bvSymbols |
private static java.util.HashMap<SMTTermMultOp.Op,java.lang.String> |
intSymbols |
protected SMTTermMultOp.Op |
operator |
protected java.util.List<SMTTerm> |
subs |
Constructor and Description |
---|
SMTTermMultOp(SMTTermMultOp.Op operator,
java.util.List<SMTTerm> subs) |
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, 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<SMTTermMultOp.Op,java.lang.String> bvSymbols
private static java.util.HashMap<SMTTermMultOp.Op,java.lang.String> intSymbols
protected java.util.List<SMTTerm> subs
protected SMTTermMultOp.Op operator
public SMTTermMultOp(SMTTermMultOp.Op operator, java.util.List<SMTTerm> subs)
public static SMTTermMultOp.OpProperty getProperty(SMTTermMultOp.Op op)
private static void initMaps()
public void setSubs(java.util.List<SMTTerm> subs)
public SMTTermMultOp.Op getOperator()
public void setOperator(SMTTermMultOp.Op operator)
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 SMTTermMultOp copy()
public boolean equals(java.lang.Object term)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
private java.lang.String getSymbol(SMTTermMultOp.Op operator, SMTTerm first)
public java.lang.String toSting()
public SMTTerm mkChain()