de.uka.ilkd.key.smt

Class SMTObjTranslator.ConstantCounter

java.lang.Object

de.uka.ilkd.key.smt.SMTObjTranslator.ConstantCounter

Enclosing class:

SMTObjTranslator

public class SMTObjTranslator.ConstantCounter
extends java.lang.Object

Class for counting constants of different types appearing in the proof obligation.

Author:

mihai

Field Summary

Fields

Modifier and Type	Field and Description
(package private) java.util.Set<java.lang.String>	fields
(package private) java.util.Set<java.lang.String>	heaps
(package private) java.util.Set<java.lang.String>	locsets

Constructor Summary

Constructors

Constructor and Description
ConstantCounter()

Method Summary

Modifier and Type	Method and Description
void	countConstants(Term t)
java.util.Set<java.lang.String>	getFields()
java.util.Set<java.lang.String>	getHeaps()
java.util.Set<java.lang.String>	getLocsets()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

locsets

java.util.Set<java.lang.String> locsets

heaps

java.util.Set<java.lang.String> heaps

fields

java.util.Set<java.lang.String> fields

Constructor Detail

ConstantCounter

public ConstantCounter()

Method Detail

countConstants

public void countConstants(Term t)

getLocsets

public java.util.Set<java.lang.String> getLocsets()

Returns:

the locsets

getHeaps

public java.util.Set<java.lang.String> getHeaps()

Returns:

the heaps

getFields

public java.util.Set<java.lang.String> getFields()

Returns:

the fields