de.uka.ilkd.key.smt.lang

Class SMTTermBinOp

java.lang.Object

de.uka.ilkd.key.smt.lang.SMTTerm

de.uka.ilkd.key.smt.lang.SMTTermBinOp

public class SMTTermBinOp
extends SMTTerm

Author:

Aboubakr Achraf El Ghazi

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	SMTTermBinOp.Op
static class	SMTTermBinOp.OpProperty

Nested classes/interfaces inherited from class de.uka.ilkd.key.smt.lang.SMTTerm

SMTTerm.False, SMTTerm.True

Field Summary

Fields

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

Fields inherited from class de.uka.ilkd.key.smt.lang.SMTTerm

comment, FALSE, TRUE, upp

Constructor Summary

Constructors

Constructor and Description
SMTTermBinOp(SMTTermBinOp.Op operator, SMTTerm left, SMTTerm right)

Method Summary

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)

Methods inherited from class de.uka.ilkd.key.smt.lang.SMTTerm

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

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

bvSymbols

private static java.util.HashMap<SMTTermBinOp.Op,java.lang.String> bvSymbols

intSymbols

private static java.util.HashMap<SMTTermBinOp.Op,java.lang.String> intSymbols

operator

private SMTTermBinOp.Op operator

left

private SMTTerm left

right

private SMTTerm right

Constructor Detail

SMTTermBinOp

public SMTTermBinOp(SMTTermBinOp.Op operator,
                    SMTTerm left,
                    SMTTerm right)

Method Detail

getProperty

public static SMTTermBinOp.OpProperty getProperty(SMTTermBinOp.Op op)

initMaps

private static void initMaps()

getQuantVars

public java.util.List<SMTTermVariable> getQuantVars()

Overrides:

getQuantVars in class SMTTerm

getUQVars

public java.util.List<SMTTermVariable> getUQVars()

Overrides:

getUQVars in class SMTTerm

getEQVars

public java.util.List<SMTTermVariable> getEQVars()

Overrides:

getEQVars in class SMTTerm

getVars

public java.util.List<SMTTermVariable> getVars()

Overrides:

getVars in class SMTTerm

sort

public SMTSort sort()

Specified by:

sort in class SMTTerm

occurs

public boolean occurs(SMTTermVariable a)

Specified by:

occurs in class SMTTerm

occurs

public boolean occurs(java.lang.String id)

Specified by:

occurs in class SMTTerm

substitute

public SMTTerm substitute(SMTTermVariable a,
                          SMTTerm b)

Specified by:

substitute in class SMTTerm

substitute

public SMTTerm substitute(SMTTerm a,
                          SMTTerm b)

Specified by:

substitute in class SMTTerm

replace

public SMTTerm replace(SMTTermCall a,
                       SMTTerm b)

Specified by:

replace in class SMTTerm

instantiate

public SMTTerm instantiate(SMTTermVariable a,
                           SMTTerm b)

Specified by:

instantiate in class SMTTerm

getOperator

public SMTTermBinOp.Op getOperator()

setOperator

public void setOperator(SMTTermBinOp.Op operator)

getLeft

public SMTTerm getLeft()

setLeft

public void setLeft(SMTTerm left)

getRight

public SMTTerm getRight()

setRight

public void setRight(SMTTerm right)

copy

public SMTTermBinOp copy()

Specified by:

copy in class SMTTerm

equals

public boolean equals(java.lang.Object term)

Overrides:

equals in class java.lang.Object

equals

public boolean equals(SMTTermBinOp bt)

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toSting

public java.lang.String toSting()

extractArgsLeft

private void extractArgsLeft(SMTTermBinOp binop,
                             java.util.List<SMTTerm> args)

extractArgsRight

private void extractArgsRight(SMTTermBinOp binop,
                              java.util.List<SMTTerm> args)

extractArgs

private void extractArgs(SMTTermBinOp binop,
                         java.util.List<SMTTerm> args)

isChainableBinOp

public boolean isChainableBinOp(SMTTerm t)

toString

public java.lang.String toString(int nestPos)

Overrides:

toString in class SMTTerm

searchChains

private java.util.List<java.util.List<SMTTerm>> searchChains(java.util.List<SMTTerm> args,
                                                             java.util.List<SMTTermBinOp.Op> ops)

extractChain

private java.util.List<SMTTerm> extractChain(int start,
                                             java.util.List<SMTTerm> args,
                                             java.util.List<SMTTermBinOp.Op> ops,
                                             java.util.List<SMTTerm> chainables)

checkChainable

private java.util.List<java.lang.String> checkChainable(int nestPos,
                                                        java.util.List<SMTTerm> args)

Parameters:

nestPos -

args -

Returns:

getSymbol

private java.lang.String getSymbol(SMTTermBinOp.Op operator,
                                   SMTTerm first)

Returns: