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 |
---|---|
protected SMTTermMultOp.Op |
operator |
protected java.util.List<SMTTerm> |
subs |
Constructor and Description |
---|
SMTTermMultOp(SMTTermMultOp.Op operator,
java.util.List<SMTTerm> subs) |
Modifier and Type | Method and Description |
---|---|
SMTTermMultOp |
copy() |
boolean |
equals(java.lang.Object term) |
java.util.List<SMTTermVariable> |
getEQVars() |
SMTTermMultOp.Op |
getOperator() |
static SMTTermMultOp.OpProperty |
getProperty(SMTTermMultOp.Op op) |
java.util.List<SMTTermVariable> |
getQuantVars() |
java.util.List<SMTTerm> |
getSubs() |
java.util.List<SMTTermVariable> |
getUQVars() |
java.util.List<SMTTermVariable> |
getVars() |
int |
hashCode() |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
mkChain() |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(java.lang.String id) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
void |
setOperator(SMTTermMultOp.Op operator) |
void |
setSubs(java.util.List<SMTTerm> subs) |
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, 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
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)
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
public java.lang.String toSting()
public SMTTerm mkChain()
Copyright © 2003-2019 The KeY-Project.