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 HashMap<SMTTermMultOp.Op,String> |
bvSymbols |
private static HashMap<SMTTermMultOp.Op,String> |
intSymbols |
protected SMTTermMultOp.Op |
operator |
protected List<SMTTerm> |
subs |
Constructor and Description |
---|
SMTTermMultOp(SMTTermMultOp.Op operator,
List<SMTTerm> subs) |
Modifier and Type | Method and Description |
---|---|
SMTTermMultOp |
copy() |
boolean |
equals(Object term) |
List<SMTTermVariable> |
getEQVars() |
SMTTermMultOp.Op |
getOperator() |
static SMTTermMultOp.OpProperty |
getProperty(SMTTermMultOp.Op op) |
List<SMTTermVariable> |
getQuantVars() |
List<SMTTerm> |
getSubs() |
private String |
getSymbol(SMTTermMultOp.Op operator,
SMTTerm first) |
List<SMTTermVariable> |
getUQVars() |
List<SMTTermVariable> |
getVars() |
int |
hashCode() |
private static void |
initMaps() |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
SMTTerm |
mkChain() |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(String id) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
void |
setOperator(SMTTermMultOp.Op operator) |
void |
setSubs(List<SMTTerm> subs) |
SMTSort |
sort() |
SMTTerm |
substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
substitute(SMTTermVariable a,
SMTTerm b) |
String |
toSting() |
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
private static HashMap<SMTTermMultOp.Op,String> bvSymbols
private static HashMap<SMTTermMultOp.Op,String> intSymbols
protected SMTTermMultOp.Op operator
public SMTTermMultOp(SMTTermMultOp.Op operator, List<SMTTerm> subs)
public static SMTTermMultOp.OpProperty getProperty(SMTTermMultOp.Op op)
private static void initMaps()
public SMTTermMultOp.Op getOperator()
public void setOperator(SMTTermMultOp.Op operator)
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 SMTTermMultOp copy()
private String getSymbol(SMTTermMultOp.Op operator, SMTTerm first)
public String toSting()
public SMTTerm mkChain()